text: /***************************************************************************
  Copyright (c) 2006-2011, Armin Biere, Johannes Kepler University.
  
  Permission is hereby granted, free of charge, to any person obtaining a copy
  of this software and associated documentation files (the "Software"), to
  deal in the Software without restriction, including without limitation the
  rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
  sell copies of the Software, and to permit persons to whom the Software is
  furnished to do so, subject to the following conditions:
  
  The above copyright notice and this permission notice shall be included in
  all copies or substantial portions of the Software.
  
  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL THE
  AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
  IN THE SOFTWARE.
  ***************************************************************************/
  
  #include "simpaig.h"
  
  #include <stdlib.h>
  #include <string.h>
  #include <limits.h>
  #include <assert.h>
  
  #define NEWN(p,n) \
    do { \
      size_t bytes = (n) * sizeof (*(p)); \
      (p) = mgr->malloc (mgr->mem, bytes); \
      memset ((p), 0, bytes); \
    } while (0)
  
  #define REALLOCN(p,m,n) \
    do { \
      size_t mbytes = (m) * sizeof (*(p)); \
      size_t nbytes = (n) * sizeof (*(p)); \
      size_t minbytes = (mbytes < nbytes) ? mbytes : nbytes; \
      void * res = mgr->malloc (mgr->mem, nbytes); \
      memcpy (res, (p), minbytes); \
      if (nbytes > mbytes) \
        memset (((char*)res) + mbytes, 0, nbytes - mbytes); \
      mgr->free (mgr->mem, (p), mbytes); \
      (p) = res; \
    } while (0)
  
  #define ENLARGE(p,s) \
    do { \
      size_t old_size = (s); \
      size_t new_size = old_size ? 2 * old_size : 1; \
      REALLOCN (p,old_size,new_size); \
      (s) = new_size; \
    } while (0)
  
  #define PUSH(p,t,s,l) \
    do { \
      if ((t) == (s)) \
        ENLARGE (p, s); \
      (p)[(t)++] = (l); \
    } while (0)
  
  #define DELETEN(p,n) \
    do { \
      size_t bytes = (n) * sizeof (*(p)); \
      mgr->free (mgr->mem, (p), bytes); \
      (p) = 0; \
    } while (0)
  
  typedef unsigned long WORD;
  
  #define NEW(p) NEWN (p,1)
  #define DELETE(p) DELETEN (p,1)
  
  #define NOT(p) ((simpaig*)(1^(WORD)(p)))
  #define STRIP(p) ((simpaig*)((~1)&(WORD)(p)))
  #define CONSTSTRIP(p) ((const simpaig*)((~1)&(WORD)(p)))
  #define SIGN(p) (1&(WORD)(p))
  #define ISVAR(p) (!SIGN(p) && (p)->var != 0)
  #define ISFALSE(p) (!SIGN (p) && !(p)->var && !(p)->c0)
  #define ISTRUE(p) (SIGN (p) && ISFALSE (NOT(p)))
  #define ISCONST(p) (!STRIP(p)->var && !STRIP(p)->c0)
  #define ISAND(p) (!SIGN(p) && ((p)->c0 != 0))
  
  #define IMPORT(p) \
    (assert (simpaig_valid (p)), ((simpaig *)(p)))
  
  
  #ifndef NDEBUG
  
  static int
  simpaig_valid (const simpaig * aig)
  {
    const simpaig *tmp = CONSTSTRIP (aig);
    return tmp && tmp->ref > 0;
  }
  
  #endif
  
  int
  simpaig_isfalse (const simpaig * aig)
  {
    return ISFALSE (IMPORT (aig));
  }
  
  int
  simpaig_istrue (const simpaig * aig)
  {
    return ISFALSE (NOT (IMPORT (aig)));
  }
  
  int
  simpaig_signed (const simpaig * aig)
  {
    return SIGN (IMPORT (aig));
  }
  
  void *
  simpaig_isvar (const simpaig * aig)
  {
    const simpaig *tmp = IMPORT (aig);
    return ISVAR (tmp) ? tmp->var : 0;
  }
  
  int
  simpaig_slice (const simpaig * aig)
  {
    const simpaig *tmp = IMPORT (aig);
    return ISVAR (tmp) ? aig->slice : 0;
  }
  
  int
  simpaig_isand (const simpaig * aig)
  {
    const simpaig *tmp = STRIP (IMPORT (aig));
    return !tmp->var && tmp->c0;
  }
  
  
  simpaig *
  simpaig_strip (simpaig * aig)
  {
    return STRIP (IMPORT (aig));
  }
  
  simpaig *
  simpaig_not (simpaig * aig)
  {
    return NOT (IMPORT (aig));
  }
  
  simpaig *
  simpaig_child (simpaig * aig, int child)
  {
    aig = STRIP (aig);
    assert (ISAND (aig));
    assert (child == 0 || child == 1);
    return child ? aig->c1 : aig->c0;
  }
  
  static void *
  simpaig_default_malloc (void *state, size_t bytes)
  {
    return malloc (bytes);
  }
  
  static void
  simpaig_default_free (void *state, void *ptr, size_t bytes)
  {
    free (ptr);
  }
  
  simpaigmgr *
  simpaig_init (void)
  {
    return simpaig_init_mem (0, simpaig_default_malloc, simpaig_default_free);
  }
  
  simpaigmgr *
  simpaig_init_mem (void *mem_mgr, simpaig_malloc m, simpaig_free f)
  {
    simpaigmgr *mgr;
    mgr = m (mem_mgr, sizeof (*mgr));
    memset (mgr, 0, sizeof (*mgr));
    mgr->mem = mem_mgr;
    mgr->malloc = m;
    mgr->free = f;
    return mgr;
  }
  
  void
  simpaig_reset (simpaigmgr * mgr)
  {
    simpaig *p, *next;
    unsigned i;
  
    for (i = 0; i < mgr->count_table; i++)
      {
        for (p = mgr->table[i]; p; p = next)
  	{
  	  next = p->next;
  	  DELETE (p);
  	}
      }
  
    DELETEN (mgr->table, mgr->size_table);
    DELETEN (mgr->cached, mgr->size_cached);
    DELETEN (mgr->assigned, mgr->size_assigned);
    DELETEN (mgr->indices, mgr->size_indices);
  
    mgr->free (mgr->mem, mgr, sizeof (*mgr));
  }
  
  
  unsigned
  simpaig_current_nodes (simpaigmgr * mgr)
  {
    return mgr->count_table + mgr->false_aig.ref;
  }
  
  static simpaig *
  inc (simpaig * res)
  {
    simpaig *tmp = STRIP (res);
    if (tmp->ref < UINT_MAX) tmp->ref++;
    return res;
  }
  
  simpaig *
  simpaig_false (simpaigmgr * mgr)
  {
    return inc (&mgr->false_aig);
  }
  
  simpaig *
  simpaig_true (simpaigmgr * mgr)
  {
    return NOT (inc (&mgr->false_aig));
  }
  
  simpaig *
  simpaig_inc (simpaigmgr * mgr, simpaig * res)
  {
    return inc (IMPORT (res));
  }
  
  static unsigned
  simpaig_hash_ptr (void *ptr)
  {
    return (unsigned) (unsigned long)ptr;
  }
  
  static unsigned
  simpaig_hash (simpaigmgr * mgr,
  	      void *var, int slice, simpaig * c0, simpaig * c1)
  {
    unsigned res = 1223683247 * simpaig_hash_ptr (var);
    res += 2221648459u * slice;
    res += 432586151 * simpaig_hash_ptr (c0);
    res += 3333529009u * simpaig_hash_ptr (c1);
    res &= mgr->size_table - 1;
    return res;
  }
  
  static void
  simpaig_enlarge (simpaigmgr * mgr)
  {
    simpaig **old_table, *p, *next;
    unsigned old_size_table, i, h;
  
    old_table = mgr->table;
    old_size_table = mgr->size_table;
  
    mgr->size_table = old_size_table ? 2 * old_size_table : 1;
    NEWN (mgr->table, mgr->size_table);
  
    for (i = 0; i < old_size_table; i++)
      {
        for (p = old_table[i]; p; p = next)
  	{
  	  next = p->next;
  	  h = simpaig_hash (mgr, p->var, p->slice, p->c0, p->c1);
  	  p->next = mgr->table[h];
  	  mgr->table[h] = p;
  	}
      }
  
    DELETEN (old_table, old_size_table);
  }
  
  static simpaig **
  simpaig_find (simpaigmgr * mgr,
  	      void *var, int slice, simpaig * c0, simpaig * c1)
  {
    simpaig **res, *n;
    unsigned h = simpaig_hash (mgr, var, slice, c0, c1);
    for (res = mgr->table + h;
         (n = *res) &&
         (n->var != var || n->slice != slice || n->c0 != c0 || n->c1 != c1);
         res = &n->next)
      ;
    return res;
  }
  
  static void
  dec (simpaigmgr * mgr, simpaig * aig)
  {
    simpaig **p;
  
    aig = STRIP (aig);
  
    assert (aig);
    assert (aig->ref > 0);
  
    if (aig->ref < UINT_MAX) aig->ref--;
  
    if (aig->ref)
      return;
  
    if (ISFALSE (aig))
      return;
  
    if (aig->c0)
      {
        dec (mgr, aig->c0);	/* TODO: derecursify */
        dec (mgr, aig->c1);	/* TODO: derecursify */
      }
  
    p = simpaig_find (mgr, aig->var, aig->slice, aig->c0, aig->c1);
    if (*p != aig)
      p = simpaig_find (mgr, aig->var, aig->slice, aig->c1, aig->c0);
  
    assert (*p == aig);
    *p = aig->next;
    DELETE (aig);
  
    assert (mgr->count_table > 0);
    mgr->count_table--;
  }
  
  void
  simpaig_dec (simpaigmgr * mgr, simpaig * res)
  {
    dec (mgr, IMPORT (res));
  }
  
  simpaig *
  simpaig_var (simpaigmgr * mgr, void *var, int slice)
  {
    simpaig **p, *res;
    assert (var);
    if (mgr->size_table == mgr->count_table)
      simpaig_enlarge (mgr);
  
    p = simpaig_find (mgr, var, slice, 0, 0);
    if (!(res = *p))
      {
        NEW (res);
        res->var = var;
        res->slice = slice;
        mgr->count_table++;
        *p = res;
      }
  
    return inc (res);
  }
  
  simpaig *
  simpaig_and (simpaigmgr * mgr, simpaig * c0, simpaig * c1)
  {
    simpaig **p, *res;
  
    if (ISFALSE (c0) || ISFALSE (c1) || c0 == NOT (c1))
      return simpaig_false (mgr);
  
    if (ISTRUE (c0) || c0 == c1)
      return inc (c1);
  
    if (ISTRUE (c1))
      return inc (c0);
  
    if (mgr->size_table == mgr->count_table)
      simpaig_enlarge (mgr);
  
    p = simpaig_find (mgr, 0, 0, c1, c0);
    if (!(res = *p))
      {
        p = simpaig_find (mgr, 0, 0, c0, c1);
        if (!(res = *p))
  	{
  	  NEW (res);
  	  res->c0 = inc (c0);
  	  res->c1 = inc (c1);
  	  mgr->count_table++;
  	  *p = res;
  	}
      }
  
    return inc (res);
  }
  
  simpaig *
  simpaig_or (simpaigmgr * mgr, simpaig * a, simpaig * b)
  {
    return NOT (simpaig_and (mgr, NOT (a), NOT (b)));
  }
  
  simpaig *
  simpaig_implies (simpaigmgr * mgr, simpaig * a, simpaig * b)
  {
    return NOT (simpaig_and (mgr, a, NOT (b)));
  }
  
  simpaig *
  simpaig_xor (simpaigmgr * mgr, simpaig * a, simpaig * b)
  {
    simpaig *l = simpaig_or (mgr, a, b);
    simpaig *r = simpaig_or (mgr, NOT (a), NOT (b));
    simpaig *res = simpaig_and (mgr, l, r);
    dec (mgr, l);
    dec (mgr, r);
    return res;
  }
  
  simpaig *
  simpaig_xnor (simpaigmgr * mgr, simpaig * a, simpaig * b)
  {
    return simpaig_xor (mgr, a, NOT (b));
  }
  
  simpaig *
  simpaig_ite (simpaigmgr * mgr, simpaig * c, simpaig * t, simpaig * e)
  {
    simpaig *l = simpaig_implies (mgr, c, t);
    simpaig *r = simpaig_implies (mgr, NOT (c), e);
    simpaig *res = simpaig_and (mgr, l, r);
    dec (mgr, l);
    dec (mgr, r);
    return res;
  }
  
  void
  simpaig_assign (simpaigmgr * mgr, simpaig * lhs, simpaig * rhs)
  {
    lhs = IMPORT (lhs);
    rhs = IMPORT (rhs);
  
    assert (ISVAR (lhs));
    assert (!lhs->rhs);
    assert (!lhs->cache);
  
    inc (lhs);
    lhs->rhs = inc (rhs);
    PUSH (mgr->assigned, mgr->count_assigned, mgr->size_assigned, lhs);
  }
  
  static void
  simpaig_reset_assignment (simpaigmgr * mgr)
  {
    simpaig *aig;
    int i;
  
    for (i = 0; i < mgr->count_assigned; i++)
      {
        aig = mgr->assigned[i];
        assert (aig->rhs);
        dec (mgr, aig->rhs);
        aig->rhs = 0;
        dec (mgr, aig);
      }
  
    mgr->count_assigned = 0;
  }
  
  static void
  simpaig_cache (simpaigmgr * mgr, simpaig * lhs, simpaig * rhs)
  {
    assert (!SIGN (lhs));
    assert (!lhs->cache);
    inc (lhs);
    lhs->cache = inc (rhs);
    PUSH (mgr->cached, mgr->count_cached, mgr->size_cached, lhs);
  }
  
  static void
  simpaig_reset_cache (simpaigmgr * mgr)
  {
    simpaig *aig;
    int i;
  
    for (i = 0; i < mgr->count_cached; i++)
      {
        aig = mgr->cached[i];
        assert (aig);
        assert (!SIGN (aig));
        assert (aig->cache);
        dec (mgr, aig->cache);
        aig->cache = 0;
        dec (mgr, aig);
      }
  
    mgr->count_cached = 0;
  }
  
  static simpaig *
  simpaig_substitute_rec (simpaigmgr * mgr, simpaig * node)
  {
    simpaig *res, *l, *r;
    unsigned sign;
  
    sign = SIGN (node);
    if (sign)
      node = NOT (node);
  
    if (node->cache)
      {
        res = inc (node->cache);
      }
    else
      {
        if (ISVAR (node))
  	{
  	  if (node->rhs)
  	    {
  	      if (ISCONST (node->rhs))
  		res = simpaig_inc (mgr, node->rhs);
  	      else
  		res = simpaig_substitute_rec (mgr, node->rhs);
  	    }
  	  else
  	    res = inc (node);
  	}
        else
  	{
  	  l = simpaig_substitute_rec (mgr, node->c0);	/* TODO derecursify */
  	  r = simpaig_substitute_rec (mgr, node->c1);	/* TODO derecursify */
  	  res = simpaig_and (mgr, l, r);
  	  dec (mgr, l);
  	  dec (mgr, r);
  	}
  
        simpaig_cache (mgr, node, res);
      }
  
    if (sign)
      res = NOT (res);
  
    return res;
  }
  
  simpaig *
  simpaig_substitute (simpaigmgr * mgr, simpaig * node)
  {
    simpaig *res;
  
    node = IMPORT (node);
    if (!ISCONST (node))
      {
        assert (!mgr->count_cached);
        res = simpaig_substitute_rec (mgr, node);
        simpaig_reset_cache (mgr);
      }
    else
      res = inc (node);
  
    simpaig_reset_assignment (mgr);
  
    return res;
  }
  
  static simpaig *
  simpaig_shift_rec (simpaigmgr * mgr, simpaig * node, int delta)
  {
    simpaig *res, *l, *r;
    unsigned sign;
  
    sign = SIGN (node);
    if (sign)
      node = NOT (node);
  
    if (node->cache)
      {
        res = inc (node->cache);
      }
    else
      {
        if (ISVAR (node))
  	{
  	  res = simpaig_var (mgr, node->var, node->slice + delta);
  	}
        else
  	{
  	  l = simpaig_shift_rec (mgr, node->c0, delta);
  	  r = simpaig_shift_rec (mgr, node->c1, delta);
  	  res = simpaig_and (mgr, l, r);
  	  dec (mgr, l);
  	  dec (mgr, r);
  	}
  
        simpaig_cache (mgr, node, res);
      }
  
    if (sign)
      res = NOT (res);
  
    return res;
  }
  
  simpaig *
  simpaig_shift (simpaigmgr * mgr, simpaig * node, int delta)
  {
    simpaig *res;
  
    node = IMPORT (node);
    if (ISCONST (node))
      return inc (node);
  
    assert (!mgr->count_cached);
    res = simpaig_shift_rec (mgr, node, delta);
    simpaig_reset_cache (mgr);
  
    return res;
  }
  
  static void
  simpaig_push_index (simpaigmgr * mgr, simpaig * node)
  {
    assert (!SIGN (node));
    assert (!ISFALSE (node));
    assert (!node->idx);
    PUSH (mgr->indices, mgr->count_indices, mgr->size_indices, node);
    node->idx = mgr->count_indices;
    assert (node->idx);
    inc (node);
  }
  
  static void
  simpaig_assign_indices_rec (simpaigmgr * mgr, simpaig * node)
  {
    node = STRIP (node);
    if (node->idx)
      return;
  
    if (!ISVAR (node))
      {
        simpaig_assign_indices_rec (mgr, node->c0);
        simpaig_assign_indices_rec (mgr, node->c1);
      }
  
    simpaig_push_index (mgr, node);
  }
  
  void
  simpaig_assign_indices (simpaigmgr * mgr, simpaig * node)
  {
    if (!ISCONST (node))
      simpaig_assign_indices_rec (mgr, node);
  }
  
  void
  simpaig_reset_indices (simpaigmgr * mgr)
  {
    simpaig *aig;
    int i;
  
    for (i = 0; i < mgr->count_indices; i++)
      {
        aig = mgr->indices[i];
        assert (aig);
        assert (!SIGN (aig));
        assert (aig->idx);
        aig->idx = 0;
        dec (mgr, aig);
      }
  
    mgr->count_indices = 0;
  }
  
  unsigned
  simpaig_index (simpaig * node)
  {
    assert (!SIGN (node));
    return node->idx;
  }
  
  unsigned
  simpaig_max_index (simpaigmgr * mgr)
  {
    return mgr->count_indices;
  }
  
  int
  simpaig_int_index (simpaig * node)
  {
    int sign = SIGN (node) ? -1 : 1;
    int res = simpaig_index (STRIP (node)) + 1;
    res *= sign;
    return res;
  }
  
  unsigned
  simpaig_unsigned_index (simpaig * node)
  {
    unsigned sign = SIGN (node) ? 1 : 0;
    unsigned res = 2 * simpaig_index (STRIP (node));
    res |= sign;
    return res;
  }
  