xref: /dports/math/yices/yices-2.6.2/src/terms/terms.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * INTERNAL TERM REPRESENTATION AND HASH CONSING
 */

/*
 * The internal terms include:
 * 1) constants:
 *    - constants of uninterpreted/scalar
 *    - global uninterpreted constants
 * 2) generic terms
 *    - ite c t1 t2
 *    - eq t1 t2
 *    - apply f t1 ... t_n
 *    - mk-tuple t1 ... t_n
 *    - select i tuple
 *    - update f t1 ... t_n v
 *    - distinct t1 ... t_n
 * 3) variables and quantifiers
 *    - variables are identified by their type and an integer index.
 *    - quantified formulas are of the form (forall v_1 ... v_n term)
 *      where each v_i is a variable
 *    - lambda terms: same thing
 * 4) boolean operators
 *    - or t1 ... t_n
 *    - xor t1 ... t_n
 *    - bit i u (extract bit i of a bitvector term u)
 * 6) arithmetic terms and atoms
 *    - terms are either rational constants, power products, or
 *      polynomials with rational coefficients
 *    - atoms are either of the form (t == 0) or (t >= 0)
 *      where t is a term.
 *    - atoms a x - a y == 0 are rewritten to (x = y)
 * 7) bitvector terms and atoms
 *    - bitvector constants
 *    - power products
 *    - polynomials
 *    - bit arrays
 *    - other operations: divisions/shift
 *    - atoms: three binary predicates
 *      bv_eq t1 t2
 *      bv_ge t1 t2 (unsigned comparison: t1 >= t2)
 *      bv_sge t1 t2 (signed comparison: t1 >= t2)
 *
 * 8) more arithmetic operators (defined in SMTLIB2)
 *    - floor x
 *    - ceil x
 *    - abs x
 *    - div x y
 *    - mod x y
 *    - divides x y: y is a multiple of y
 *    - is_int x: true if x is an integer
 *    - rdiv x y: (/ x y)
 *
 * Every term is an index t in a global term table,
 * where 0 <= t <= 2^30. The two term occurrences
 * t+ and t- are encoded on 32bits (signed integer) with
 * - bit[31] = sign bit = 0
 * - bits[30 ... 1] = t
 * - bit[0] = polarity bit: 0 means t+, 1 means t-
 *
 * For a boolean term t, the occurrence t+ means p
 * and t- means (not p). All occurrences of a
 * non-boolean term t are positive.
 *
 * For every term, we keep:
 * - type[t] (index in the type table)
 * - kind[t] (what kind of term it is)
 * - desc[t] = descriptor that depends on the kind
 *
 * It is possible to attach names to term occurrences (but not directly
 * to terms). This is required to deal properly with booleans. For example,
 * we want to allow the user to give different names to t and (not t).
 */

#include "terms/bv64_constants.h"
#include "terms/terms.h"
#include "utils/hash_functions.h"
#include "utils/memalloc.h"
#include "utils/refcount_strings.h"


/*
 * Finalizer for term names in the symbol table.
 * All symbols must be generated by the clone function, and have
 * a reference counter (cf. refcount_strings.h).
 */
static void term_name_finalizer(stbl_rec_t *r) {
  string_decref(r->string);
}


/*
 * Default finalizer for special terms
 */
static void default_special_finalizer(special_term_t *s, term_kind_t tag) {
  safe_free(s->extra);
}


/*
 * Initialize table, with initial size n.
 * - ttbl = attached type table.
 * - ptbl = attached power-product table.
 */
static void term_table_init(term_table_t *table, uint32_t n, type_table_t *ttbl, pprod_table_t *ptbl) {
  // abort if n is too large
  if (n > YICES_MAX_TERMS) {
    out_of_memory();
  }

  table->kind = (unsigned char *) safe_malloc(n * sizeof(unsigned char));
  table->type = (type_t *) safe_malloc(n * sizeof(type_t));
  table->desc = (term_desc_t *) safe_malloc(n * sizeof(term_desc_t));
  table->mark = allocate_bitvector(n);

  table->size = n;
  table->nelems = 0;
  table->free_idx = -1; // empty free list
  table->live_terms = 0;

  table->types = ttbl;
  table->pprods = ptbl;
  table->finalize = default_special_finalizer;

  // initialize tables with default initial size
  init_int_htbl(&table->htbl, 0);
  init_stbl(&table->stbl, 0);
  init_ptr_hmap(&table->ntbl, 0);
  init_int_hmap(&table->utbl, 0);

  // attach the name finalizer to stbl
  stbl_set_finalizer(&table->stbl, term_name_finalizer);

  // buffers
  init_ivector(&table->ibuffer, 20);
  init_pvector(&table->pbuffer, 20);

}


/*
 * Extend the table: make it 50% larger
 */
static void term_table_extend(term_table_t *table) {
  uint32_t n;

  n = table->size + 1;
  n += n >> 1;

  // force abort if n is too large
  if (n > YICES_MAX_TERMS) {
    out_of_memory();
  }

  table->kind = (unsigned char *) safe_realloc(table->kind, n * sizeof(unsigned char));
  table->type = (type_t *) safe_realloc(table->type, n * sizeof(type_t));
  table->desc = (term_desc_t *) safe_realloc(table->desc, n * sizeof(term_desc_t));
  table->mark = extend_bitvector(table->mark, n);
  table->size = n;
}



/*
 * TERM ALLOCATION
 */

/*
 * Allocate a new term id
 * - clear its mark. Nothing else is initialized.
 */
static int32_t allocate_term_id(term_table_t *table) {
  int32_t i;

  i = table->free_idx;
  if (i >= 0) {
    table->free_idx = table->desc[i].integer;
  } else {
    i = table->nelems;
    table->nelems ++;
    if (i == table->size) {
      term_table_extend(table);
    }
    assert(i < table->size);
  }
  clr_bit(table->mark, i);
  table->live_terms ++;

  return i;
}



/*
 * Terms with integer descriptor
 * - tag = kind
 * - tau = type
 * - id = index
 */
static int32_t new_integer_term(term_table_t *table, term_kind_t tag, type_t tau, int32_t id) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = tag;
  table->type[i] = tau;
  table->desc[i].integer = id;

  return i;
}


/*
 * Terms with pointer descriptor
 * - tag = kind
 * - tau = type
 * - d = descriptor
 */
static int32_t new_ptr_term(term_table_t *table, term_kind_t tag, type_t tau, void *d) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = tag;
  table->type[i] = tau;
  table->desc[i].ptr = d;

  return i;
}


/*
 * Rational descriptors
 * - tag = kind
 * - tau = type
 * - a = value
 */
static int32_t new_rational_term(term_table_t *table, term_kind_t tag, type_t tau, rational_t *a) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = tag;
  table->type[i] = tau;
  q_init(&table->desc[i].rational);
  q_set(&table->desc[i].rational, a);

  return i;
}


/*
 * Select k t: for tuple projection or bitvector selection.
 * - tag = kind
 * - tau = type
 * - k = select index
 * - t = select argument
 */
static int32_t new_select_term(term_table_t *table, term_kind_t tag, type_t tau, uint32_t k, term_t t) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = tag;
  table->type[i] = tau;
  table->desc[i].select.idx = k;
  table->desc[i].select.arg = t;

  return i;
}


/*
 * Root object:
 * - k = root index
 * - x = variable
 * - p = polynomial in x
 * - r = relation
 */
static root_atom_t* new_root_atom(term_table_t *table, uint32_t k, term_t x, term_t p, root_atom_rel_t r) {
  root_atom_t *atom;

  atom = (root_atom_t *) safe_malloc(sizeof(root_atom_t));
  atom->k = k;
  atom->x = x;
  atom->p = p;
  atom->r = r;

  return atom;
}




/*
 * TERM DESCRIPTORS
 */

/*
 * Limit on n when allocating a composite term descriptor of arity n.
 * If n <= MAX_COMPOSITE_TERM_ARITY then we can compute the descriptor
 * size without overflow (on 32bit).
 */
#define MAX_COMPOSITE_TERM_ARITY ((UINT32_MAX-sizeof(composite_term_t))/sizeof(term_t))


/*
 * Generic n-ary term:
 * - n = arity
 * - a[0 ... n-1] = components
 */
static composite_term_t *new_composite_term(uint32_t n, const term_t *a) {
  composite_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY);

  d = (composite_term_t *) safe_malloc(sizeof(composite_term_t) + n * sizeof(term_t));
  d->arity = n;
  for (j=0; j<n; j++) {
    d->arg[j] = a[j];
  }

  return d;
}


/*
 * Function application
 * - f = function (as a term)
 * - n = arity
 * - a[0 ... n-1] = arguments to f
 */
static composite_term_t *new_app_term(term_t f, uint32_t n, const term_t *a) {
  composite_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY - 1);

  d = (composite_term_t *) safe_malloc(sizeof(composite_term_t) + (n+1) * sizeof(term_t));
  d->arity = n+1;
  d->arg[0] = f;
  for (j=0; j<n; j++) {
    d->arg[j + 1] = a[j];
  }

  return d;
}


/*
 * Function update: (update f a[0] ... a[n-1] v)
 */
static composite_term_t *new_update_term(term_t f, uint32_t n, const term_t *a, term_t v) {
  composite_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY - 2);

  d = (composite_term_t *) safe_malloc(sizeof(composite_term_t) + (n+2) * sizeof(term_t));
  d->arity = n+2;
  d->arg[0] = f;
  for (j=0; j<n; j++) {
    d->arg[j + 1] = a[j];
  }
  d->arg[j + 1] = v;

  return d;
}


/*
 * Quantified term: (forall v[0] ... v[n-1] p)
 */
static composite_term_t *new_forall_term(uint32_t n, const term_t *v, term_t p) {
  composite_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY - 1);

  d = (composite_term_t *) safe_malloc(sizeof(composite_term_t) + (n+1) * sizeof(term_t));
  d->arity = n+1;
  for (j=0; j<n; j++) {
    d->arg[j] = v[j];
  }
  d->arg[j] = p;

  return d;
}


/*
 * Lambda term: (lambda v[0] ... v[n-1] t)
 */
static composite_term_t *new_lambda_term(uint32_t n, const term_t *v, term_t t) {
  composite_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY - 1);

  d = (composite_term_t *) safe_malloc(sizeof(composite_term_t) + (n+1) * sizeof(term_t));
  d->arity = n+1;
  for (j=0; j<n; j++) {
    d->arg[j] = v[j];
  }
  d->arg[j] = t;

  return d;
}


/*
 * Bit-vector constant:
 * - v = array of k words where k = ceil(bitsize/32).
 */
static bvconst_term_t *new_bvconst_term(uint32_t bitsize, const uint32_t *v) {
  bvconst_term_t *d;
  uint32_t k;

  assert(bitsize > 64);

  k = (bitsize + 31) >> 5;
  d = (bvconst_term_t *) safe_malloc(sizeof(bvconst_term_t) + k * sizeof(uint32_t));
  d->bitsize = bitsize;
  bvconst_set(d->data, k, v);

  return d;
}


/*
 * Small bitvector constant
 */
static bvconst64_term_t *new_bvconst64_term(uint32_t bitsize, uint64_t v) {
  bvconst64_term_t *d;

  assert(1 <= bitsize && bitsize <= 64 && v == norm64(v, bitsize));

  d = (bvconst64_term_t *) safe_malloc(sizeof(bvconst64_term_t));
  d->bitsize = bitsize;
  d->value = v;

  return d;
}



/*
 * Special term:
 * - allocate a special_term_descriptor
 * - set the extra field to NULL
 * - fill in the rest as a composite of arity n
 * - a[0 ... n-1] = components
 */
static composite_term_t *new_special_term(uint32_t n, const term_t *a) {
  special_term_t *d;
  uint32_t j;

  assert(n <= MAX_COMPOSITE_TERM_ARITY);
  d = (special_term_t *) safe_malloc(sizeof(special_term_t) + n * sizeof(term_t));
  d->extra = NULL;
  d->body.arity = n;
  for (j=0; j<n; j++) {
    d->body.arg[j] = a[j];
  }

  return &d->body;
}



/*
 * HASH CODES
 */

/*
 * Hash functions for polynomials, bv_polynomials, and bv64_polynomials are
 * defined in polynomials.c, bv_polynomials.c, and bv64_polynomials.c.
 * The following functions deal with the other term descriptors.
 */

/*
 * Indexed term defined by (tag, tau, id)
 */
static inline uint32_t hash_integer_term(term_kind_t tag, type_t tau, int32_t id) {
  return jenkins_hash_triple(tag, tau, id, 0x2839adee);
}

/*
 * Rational term defined by (tag, tau, value)
 */
static uint32_t hash_rational_term(term_kind_t tag, type_t tau, rational_t *a) {
  uint32_t num, den;

  q_hash_decompose(a, &num, &den);
  return jenkins_hash_quad(tag, tau, num, den, 0xf9e34ab9);
}

/*
 * Generic composite term: (tag, arity, arg[0] ... arg[n-1])
 */
static uint32_t hash_composite_term(term_kind_t tag, uint32_t n, const term_t *a) {
  return jenkins_hash_array((uint32_t *) a, n, (uint32_t) (0x8ede2341 + tag));
}


/*
 * Function application: (f, n, a[0] ... a[n-1])
 */
static uint32_t hash_app_term(term_t f, uint32_t n, const term_t *a) {
  uint32_t h;

  h = jenkins_hash_intarray(a, n);
  return jenkins_hash_pair(f, h, 0x2a3efb23);
}


/*
 * Function update: (update f a[0] ... a[n-1] v)
 */
static uint32_t hash_update_term(term_t f, uint32_t n, const term_t *a, term_t v) {
  uint32_t h;

  h = jenkins_hash_intarray(a, n);
  return jenkins_hash_triple(f, v, h, 0x18abe185);
}


/*
 * Quantified term: (forall v[0] ... v[n-1] p)
 */
static uint32_t hash_forall_term(uint32_t n, const term_t *v, term_t p) {
  uint32_t h;

  h = jenkins_hash_intarray(v, n);
  return jenkins_hash_pair(p, h, 0xfe3a2788);
}


/*
 * Lambda term: (lambda v[0] ... v[n-1] t)
 */
static uint32_t hash_lambda_term(uint32_t n, const term_t *v, term_t t) {
  uint32_t h;

  h = jenkins_hash_intarray(v, n);
  return jenkins_hash_pair(t, h, 0xabdaabda);
}


/*
 * Projection/bit selection: (tag, k, t)
 */
static inline uint32_t hash_select_term(term_kind_t tag, uint32_t k, term_t t) {
  return jenkins_hash_triple(tag, k, t, 0x98ab3342);
}


/*
 * Root atoms: (k, x, p, r)
 */
static inline uint32_t hash_root_atom(uint32_t k, term_t x, term_t p, root_atom_rel_t r) {
  return jenkins_hash_quad(k, x, p, r, 0xdededede);
}


/*
 * Power product: since the pprod-table already does hash consing,
 * a power product r is uniquely identified by its address.
 */
static inline uint32_t hash_power_product(const pprod_t *r) {
  return jenkins_hash_ptr(r);
}


/*
 * For bitvector constant, we can use bvconst_hash defined in bv_constants.c
 */
static inline uint32_t hash_bvconst_term(uint32_t bitsize, const uint32_t *bv) {
  return bvconst_hash(bv, bitsize);
}


/*
 * 64bit constants
 */
static inline uint32_t hash_bvconst64_term(uint32_t bitsize, uint64_t v) {
  assert(v == norm64(v, bitsize));
  return jenkins_hash_mix3((uint32_t)(v >> 32), (uint32_t) v, 0xdeadbeef + bitsize);
}



/*
 * HASH CONSING
 */

/*
 * Objects for interfacing with int_hash_table
 * - each object type corresponds to a term kind
 * - it starts with a method descriptor m
 *   with three fields:
 *     m.hash: hash function
 *     m.eq: check for equality
 *     m.build: construct fresh term
 * - other fields are a term table, and all the
 *   subcomponents for the term kind.
 * - for an object o,
 *    o->m.hash(o) = hash code for o
 *    o->m.eq(o, i): check whether o equals term i
 *    o->m.build(o): add o to the term table and return its index
 */

/*
 * Terms with integer id
 * - tag = term kind
 * - tau = type
 * - id
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  term_kind_t tag;
  type_t tau;
  int32_t id;
} integer_term_hobj_t;

/*
 * Rational terms
 * - tag = term kind
 * - tau = type
 * - a = value
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  term_kind_t tag;
  type_t tau;
  rational_t *a;
} rational_term_hobj_t;


/*
 * Generic composite
 * - tag = term kind
 * - tau = type
 * - arity = n
 * - arg = array of n term occurrences
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  term_kind_t tag;
  type_t tau;
  uint32_t arity;
  const term_t *arg;
} composite_term_hobj_t;


/*
 * Function application
 * - tau = type of (f arg[0] ... arg[n-1])
 * - f = function
 * - n = number of arguments
 * - arg = array of n arguments
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  term_t f;
  uint32_t n;
  const term_t *arg;
} app_term_hobj_t;


/*
 * Function update
 * - tau = result type
 * - f = function
 * - n = number of arguments
 * - arg = array of n arguments
 * - v = new value
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  term_t f;
  term_t v;
  uint32_t n;
  const term_t *arg;
} update_term_hobj_t;

/*
 * Quantified formula: (forall v[0] ... v[n-1] p)
 * - p = body
 * - n = number of variables
 * - v = array of n variables
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  term_t p;
  uint32_t n;
  const term_t *v;
} forall_term_hobj_t;

/*
 * Lambda term: (lambda v[0] ... v[n-1] t)
 * - tau = type
 * - t = body
 * - n = number of variables
 * - v = array of n variables
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  term_t t;
  uint32_t n;
  const term_t *v;
} lambda_term_hobj_t;


/*
 * Select term
 * - tag = term kind
 * - tau = type
 * - k = index in projection/bitselect
 * - arg = term
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  term_kind_t tag;
  type_t tau;
  uint32_t k;
  term_t arg;
} select_term_hobj_t;


/*
 * Root atom
 * - k = root index
 * - x = main variable
 * - p = the polynomial (in x) whose root is being compared
 * - r = the relation
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  uint32_t k;
  term_t x;
  term_t p;
  root_atom_rel_t r;
} root_atom_hobj_t;


/*
 * Power product
 * - tau = type (can be int, real, or bitvector)
 * - r = power product
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  pprod_t *r;
} pprod_term_hobj_t;



/*
 * Polynomial
 * - a polynomial is constructed from a buffer b
 *   and an array of term indices v
 * - tau can be int or real
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  rba_buffer_t *b;
  int32_t *v;
} poly_term_hobj_t;


/*
 * Bit-vector polynomials
 * - tau = bitvector type
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  bvarith_buffer_t *b;
  int32_t *v;
} bvpoly_term_hobj_t;


/*
 * Bit vector polynomials with small coefficients.
 * - tau = bitvector type
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  bvarith64_buffer_t *b;
  int32_t *v;
} bvpoly64_term_hobj_t;


/*
 * Bit vector polynomial constructed from a bvpoly_buffer
 * - this handles both small and large coefficients.
 * - tau = bitvector type
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  bvpoly_buffer_t *b;
} bvpoly_buffer_hobj_t;


/*
 * Bit vector constants
 * - v = value stored as an array of words
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  uint32_t bitsize;
  const uint32_t *v;
} bvconst_term_hobj_t;


/*
 * Small bit vector constants
 */
typedef struct {
  int_hobj_t m;
  term_table_t *tbl;
  type_t tau;
  uint32_t bitsize;
  uint64_t v;
} bvconst64_term_hobj_t;



/*
 * Hash functions for these objects
 */
static uint32_t hash_integer_hobj(integer_term_hobj_t *o) {
  return hash_integer_term(o->tag, o->tau, o->id);
}

static uint32_t hash_rational_hobj(rational_term_hobj_t *o) {
  return hash_rational_term(o->tag, o->tau, o->a);
}

static uint32_t hash_composite_hobj(composite_term_hobj_t *o) {
  return hash_composite_term(o->tag, o->arity, o->arg);
}

static uint32_t hash_app_hobj(app_term_hobj_t *o) {
  return hash_app_term(o->f, o->n, o->arg);
}

static uint32_t hash_update_hobj(update_term_hobj_t *o) {
  return hash_update_term(o->f, o->n, o->arg, o->v);
}

static uint32_t hash_forall_hobj(forall_term_hobj_t *o) {
  return hash_forall_term(o->n, o->v, o->p);
}

static uint32_t hash_lambda_hobj(lambda_term_hobj_t *o) {
  return hash_lambda_term(o->n, o->v, o->t);
}

static uint32_t hash_select_hobj(select_term_hobj_t *o) {
  return hash_select_term(o->tag, o->k, o->arg);
}

static uint32_t hash_root_atom_hobj(root_atom_hobj_t *o) {
  return hash_root_atom(o->k, o->x, o->p, o->r);
}

static uint32_t hash_pprod_hobj(pprod_term_hobj_t *o) {
  return hash_power_product(o->r);
}

static uint32_t hash_poly_hobj(poly_term_hobj_t *o) {
  return hash_rba_buffer(o->b, o->v);
}

static uint32_t hash_bvpoly_hobj(bvpoly_term_hobj_t *o) {
  return hash_bvarith_buffer(o->b, o->v);
}

static uint32_t hash_bvpoly64_hobj(bvpoly64_term_hobj_t *o) {
  return hash_bvarith64_buffer(o->b, o->v);
}

static uint32_t hash_bvpoly_buffer_hobj(bvpoly_buffer_hobj_t *o) {
  if (o->b->bitsize <= 64) {
    return bvpoly_buffer_hash64(o->b);
  } else {
    return bvpoly_buffer_hash(o->b);
  }
}

static uint32_t hash_bvconst_hobj(bvconst_term_hobj_t *o) {
  return hash_bvconst_term(o->bitsize, o->v);
}

static uint32_t hash_bvconst64_hobj(bvconst64_term_hobj_t *o) {
  return hash_bvconst64_term(o->bitsize, o->v);
}


/*
 * Equality test: o = hash object, i = index of a term in o->tbl
 */
static bool eq_integer_hobj(integer_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  return table->kind[i] == o->tag && table->type[i] == o->tau
    && table->desc[i].integer == o->id;
}

static bool eq_rational_hobj(rational_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  return table->kind[i] == o->tag && q_eq(&table->desc[i].rational, o->a);
}


// test whether arrays a and b of size n are equal
static bool eq_term_arrays(const term_t *a, const term_t *b, uint32_t n) {
  uint32_t i;

  for (i=0; i<n; i++) {
    if (a[i] != b[i]) return false;
  }
  return true;
}

static bool eq_composite_hobj(composite_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  composite_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != o->tag) return false;

  d = table->desc[i].ptr;
  n = d->arity;
  return n == o->arity && eq_term_arrays(o->arg, d->arg, n);
}

static bool eq_app_hobj(app_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  composite_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != APP_TERM) return false;

  d = table->desc[i].ptr;
  n = o->n;
  return d->arity == n+1 && d->arg[0] == o->f &&
    eq_term_arrays(o->arg, d->arg + 1, n);
}

static bool eq_update_hobj(update_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  composite_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != UPDATE_TERM) return false;

  d = table->desc[i].ptr;
  n = o->n;
  return d->arity == n+2 && d->arg[0] == o->f &&
    d->arg[n + 1] == o->v &&
    eq_term_arrays(o->arg, d->arg + 1, n);
}

static bool eq_forall_hobj(forall_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  composite_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != FORALL_TERM) return false;

  d = table->desc[i].ptr;
  n = o->n;
  return d->arity == n+1 && d->arg[n] == o->p &&
    eq_term_arrays(o->v, d->arg, n);
}

static bool eq_lambda_hobj(lambda_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  composite_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != LAMBDA_TERM) return false;

  d = table->desc[i].ptr;
  n = o->n;
  return d->arity == n+1 && d->arg[n] == o->t && eq_term_arrays(o->v, d->arg, n);
}

static bool eq_select_hobj(select_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  select_term_t *d;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != o->tag) return false;

  d = &table->desc[i].select;
  return d->idx == o->k && d->arg == o->arg;
}

static bool eq_root_atom_hobj(root_atom_hobj_t *o, int32_t i) {
  term_table_t *table;
  root_atom_t *r;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != ARITH_ROOT_ATOM) return false;

  r = table->desc[i].ptr;
  return r->k == o->k && r->p == o->p && r->r == o->r && r->x == o->x;
}


static bool eq_pprod_hobj(pprod_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));
  return table->kind[i] == POWER_PRODUCT && table->desc[i].ptr == o->r;
}

static bool eq_poly_hobj(poly_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  return table->kind[i] == ARITH_POLY &&
    rba_buffer_equal_poly(o->b, o->v, table->desc[i].ptr);
}

static bool eq_bvpoly_hobj(bvpoly_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  return table->kind[i] == BV_POLY &&
    bvarith_buffer_equal_bvpoly(o->b, o->v, table->desc[i].ptr);
}

static bool eq_bvpoly64_hobj(bvpoly64_term_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  return table->kind[i] == BV64_POLY &&
    bvarith64_buffer_equal_bvpoly(o->b, o->v, table->desc[i].ptr);
}

static bool eq_bvpoly_buffer_hobj(bvpoly_buffer_hobj_t *o, int32_t i) {
  term_table_t *table;

  table = o->tbl;
  assert(good_term_idx(table, i));

  switch (table->kind[i]) {
  case BV64_POLY:
    return bvpoly_buffer_equal_poly64(o->b, table->desc[i].ptr);

  case BV_POLY:
    return bvpoly_buffer_equal_poly(o->b, table->desc[i].ptr);

  default:
    return false;
  }
}

static bool eq_bvconst_hobj(bvconst_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  bvconst_term_t *d;
  uint32_t n;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != BV_CONSTANT) return false;

  d = table->desc[i].ptr;
  n = d->bitsize;
  return n == o->bitsize && bvconst_eq(d->data, o->v, (n + 31) >> 5);
}

static bool eq_bvconst64_hobj(bvconst64_term_hobj_t *o, int32_t i) {
  term_table_t *table;
  bvconst64_term_t *d;

  table = o->tbl;
  assert(good_term_idx(table, i));

  if (table->kind[i] != BV64_CONSTANT) return false;

  d = table->desc[i].ptr;
  return d->bitsize == o->bitsize && d->value == o->v;
}


/*
 * Build functions: add a new term to o->tbl and return its index
 */
static int32_t build_integer_hobj(integer_term_hobj_t *o) {
  return new_integer_term(o->tbl, o->tag, o->tau, o->id);
}

static int32_t build_rational_hobj(rational_term_hobj_t *o) {
  return new_rational_term(o->tbl, o->tag, o->tau, o->a);
}

static int32_t build_composite_hobj(composite_term_hobj_t *o) {
  composite_term_t *d;

  d = new_composite_term(o->arity, o->arg);
  return new_ptr_term(o->tbl, o->tag, o->tau, d);
}

static int32_t build_special_hobj(composite_term_hobj_t *o) {
  composite_term_t *d;

  d = new_special_term(o->arity, o->arg);
  return new_ptr_term(o->tbl, o->tag, o->tau, d);
}

static int32_t build_app_hobj(app_term_hobj_t *o) {
  composite_term_t *d;

  d = new_app_term(o->f, o->n, o->arg);
  return new_ptr_term(o->tbl, APP_TERM, o->tau, d);
}

static int32_t build_update_hobj(update_term_hobj_t *o) {
  composite_term_t *d;

  d = new_update_term(o->f, o->n, o->arg, o->v);
  return new_ptr_term(o->tbl, UPDATE_TERM, o->tau, d);
}

static int32_t build_forall_hobj(forall_term_hobj_t *o) {
  composite_term_t *d;

  d = new_forall_term(o->n, o->v, o->p);
  return new_ptr_term(o->tbl, FORALL_TERM, bool_id, d);
}

static int32_t build_lambda_hobj(lambda_term_hobj_t *o) {
  composite_term_t *d;

  d = new_lambda_term(o->n, o->v, o->t);
  return new_ptr_term(o->tbl, LAMBDA_TERM, o->tau, d);
}

static int32_t build_select_hobj(select_term_hobj_t *o) {
  return new_select_term(o->tbl, o->tag, o->tau, o->k, o->arg);
}

static int32_t build_root_atom_hobj(root_atom_hobj_t *o) {
  root_atom_t* r;

  r = new_root_atom(o->tbl, o->k, o->x, o->p, o->r);
  return new_ptr_term(o->tbl, ARITH_ROOT_ATOM, bool_type(o->tbl->types), r);
}

static int32_t build_pprod_hobj(pprod_term_hobj_t *o) {
  return new_ptr_term(o->tbl, POWER_PRODUCT, o->tau, o->r);
}

static int32_t build_poly_hobj(poly_term_hobj_t *o) {
  polynomial_t *p;

  p = rba_buffer_get_poly(o->b, o->v);
  return new_ptr_term(o->tbl, ARITH_POLY, o->tau, p);
}

static int32_t build_bvpoly_hobj(bvpoly_term_hobj_t *o) {
  bvpoly_t *p;

  p = bvarith_buffer_get_bvpoly(o->b, o->v);
  return new_ptr_term(o->tbl, BV_POLY, o->tau, p);
}

static int32_t build_bvpoly64_hobj(bvpoly64_term_hobj_t *o) {
  bvpoly64_t *p;

  p = bvarith64_buffer_get_bvpoly(o->b, o->v);
  return new_ptr_term(o->tbl, BV64_POLY, o->tau, p);
}

static int32_t build_bvpoly_buffer_hobj(bvpoly_buffer_hobj_t *o) {
  bvpoly_buffer_t *b;
  term_kind_t tag;
  void *p;

  b = o->b;
  if (b->bitsize <= 64) {
    p = bvpoly_buffer_getpoly64(b);
    tag = BV64_POLY;
  } else {
    p = bvpoly_buffer_getpoly(b);
    tag = BV_POLY;
  }

  return new_ptr_term(o->tbl, tag, o->tau, p);
}

static int32_t build_bvconst_hobj(bvconst_term_hobj_t *o) {
  bvconst_term_t *c;

  c = new_bvconst_term(o->bitsize, o->v);
  return new_ptr_term(o->tbl, BV_CONSTANT, o->tau, c);
}

static int32_t build_bvconst64_hobj(bvconst64_term_hobj_t *o) {
  bvconst64_term_t *c;

  c = new_bvconst64_term(o->bitsize, o->v);
  return new_ptr_term(o->tbl, BV64_CONSTANT, o->tau, c);
}


/*
 * UNIT TABLE
 */

/*
 * Get the representative of type tau in the unit table
 * - tau must be a unit type
 * - return NULL_TERM (-1) if there's no representative
 */
term_t unit_type_rep(term_table_t *table, type_t tau) {
  int_hmap_pair_t *p;

  assert(is_unit_type(table->types, tau));
  p = int_hmap_find(&table->utbl, tau);
  if (p == NULL) {
    return NULL_TERM;
  }
  assert(good_term(table, p->val) && term_type(table, p->val) == tau);

  return p->val;
}


/*
 * Store t as the unique term of type tau:
 * - tau must be a singleton type
 * - t must be a valid term occurrence of type tau
 * - there mustn't be a representative for tau already
 */
void add_unit_type_rep(term_table_t *table, type_t tau, term_t t) {
  int_hmap_pair_t *p;

  assert(is_unit_type(table->types, tau) && good_term(table, t) &&
         term_type(table, t) == tau);

  p = int_hmap_get(&table->utbl, tau);
  assert(p->val == EMPTY_KEY); // i.e., -1
  p->val = t;
}


/*
 * Store t as the unique term of type tau:
 * - tau must be a singleton type
 * - t must be a valid term occurrence of type tau
 * - there mustn't be a representative for tau already or
 *   the representative must be equal to t
 */
void store_unit_type_rep(term_table_t *table, type_t tau, term_t t) {
  int_hmap_pair_t *p;

  assert(is_unit_type(table->types, tau) && good_term(table, t) &&
         term_type(table, t) == tau);

  p = int_hmap_get(&table->utbl, tau);
  if (p->val == EMPTY_KEY) {
    p->val = t;
  }
  assert(p->val == t);
}


/*
 * Remove the representative of type tau from the table.
 * - tau must be a singleton type
 * - no effect if tau has no representative
 */
static void remove_unit_type_rep(term_table_t *table, type_t tau) {
  int_hmap_pair_t *p;

  assert(is_unit_type(table->types, tau));
  p = int_hmap_find(&table->utbl, tau);
  if (p != NULL) {
    int_hmap_erase(&table->utbl, p);
  }
}


/*
 * For debugging, check that the representative for type
 * tau is equal to t.
 */
#ifndef NDEBUG
static bool is_unit_type_rep(term_table_t *table, type_t tau, term_t t) {
  term_t rep;

  rep = unit_type_rep(table, tau);
  return rep == NULL_TERM || rep == t;
}
#endif







/*
 * TERM NAMES
 */

/*
 * Get the base name of term occurrence t
 * - return NULL if t has no base name
 */
char *term_name(term_table_t *table, term_t t) {
  ptr_hmap_pair_t *p;

  assert(live_term(table, t));
  p = ptr_hmap_find(&table->ntbl, t);
  if (p == NULL) {
    return NULL;
  }

  assert(p->val != NULL);
  return p->val;

}


/*
 * Assign name to term occurrence t.
 *
 * If name is already mapped to another term t' then the previous mapping
 * is hidden. The next calls to get_term_by_name will return t. After a
 * call to remove_term_name, the mapping [name --> t] is removed and
 * the previous mapping [name --> t'] is revealed.
 *
 * If t does not have a base name already, then 'name' is stored as the
 * base name for t. That's what's printed for t by the pretty printer.
 *
 * Warning: name is stored as a pointer, no copy is made; name must be
 * created via the clone_string function.
 */
void set_term_name(term_table_t *table, term_t t, char *name) {
  ptr_hmap_pair_t *p;

  assert(good_term(table, t) && name != NULL);

  // if t doesn't have a base name then
  // add mapping t --> name in ntbl
  p = ptr_hmap_get(&table->ntbl, t);
  assert(p != NULL);
  if (p->val == NULL) {
    p->val = name;
    string_incref(name);
  }

  // add mapping name --> t in the symbol table
  stbl_add(&table->stbl, name, t);
  string_incref(name);
}


/*
 * Assign name as the base name for term t
 * - if t already has a base name, then it's replaced by 'name'
 *   and the previous name's reference counter is decremented
 */
void set_term_base_name(term_table_t *table, term_t t, char *name) {
  ptr_hmap_pair_t *p;

  assert(good_term(table, t) && name != NULL);

  p = ptr_hmap_get(&table->ntbl, t);
  assert(p != NULL);
  if (p->val != NULL) {
    string_decref(p->val);
  }
  p->val = name;
  string_incref(name);
}


/*
 * Get term occurrence with the given name (or NULL_TERM)
 */
term_t get_term_by_name(term_table_t *table, const char *name) {
  // NULL_TERM = -1 and stbl_find returns -1 if name is absent
  return stbl_find(&table->stbl, name);
}


/*
 * Remove a name from the symbol table
 * - if name is not in the symbol table, nothing is done
 * - if name is mapped to a term t, then the mapping [name -> t]
 *   is removed. If name was mapped to a previous term t' then
 *   that mapping is restored.
 *
 * If name is the base name of a term t, then that remains unchanged.
 */
void remove_term_name(term_table_t *table, const char *name) {
  stbl_remove(&table->stbl, name);
}


/*
 * Clear name: remove t's base name if any.
 * - If t has name 'xxx' then 'xxx' is first removed from the symbol
 *   table (using remove_term_name) then t's base name is erased.
 * - If t doesn't have a base name, nothing is done.
 */
void clear_term_name(term_table_t *table, term_t t) {
  ptr_hmap_pair_t *p;
  char *name;

  assert(good_term(table, t));
  p = ptr_hmap_find(&table->ntbl, t);
  if (p != NULL) {
    name = p->val;
    assert(name != NULL);

    // remove the mapping t --> name from ntbl
    ptr_hmap_erase(&table->ntbl, p);

    // check whether the mapping name --> t still exists
    // in the symbol table.
    if (stbl_find(&table->stbl, name) == t) {
      stbl_remove(&table->stbl, name);
    }
    string_decref(name);
  }
}





/*
 * TERM DELETION
 */

/*
 * Delete term i:
 * - remove pos_term(i) from the unit table
 * - remove pos_term(i) and neg_term(i) from the name table
 * - free the descriptor if needed
 * - remove i from the hash table
 * - then add i to the free list
 *
 * IMPORTANT: i must not be accessible via the symbol table.
 * No name in the symbol table must refer to pos_term(i)
 * or neg_term(i).
 */
static void delete_term(term_table_t *table, int32_t i) {
  composite_term_t *d;
  select_term_t *s;
  root_atom_t* r;
  bvconst_term_t *c;
  bvconst64_term_t *c64;
  uint32_t h, n;
  type_t tau;

  assert(good_term_idx(table, i));

  // make sure the reserved and primitive terms are
  // never deleted
  if (i <= zero_const) return;

  // deal with unit types
  tau = table->type[i];
  if (is_unit_type(table->types, tau)) {
    assert(is_unit_type_rep(table, tau, pos_term(i)));
    remove_unit_type_rep(table, tau);
  }

  // remove the default name for pos_term(i)
  // and for neg_term(i) if i has boolean type
  clear_term_name(table, pos_term(i));
  if (is_boolean_type(tau)) {
    clear_term_name(table, neg_term(i));
  }

  h = 0;   // stops GCC warning

  // compute hash and free descriptor
  switch (table->kind[i]) {
  case UNINTERPRETED_TERM:
    // No descriptor, no hash consing
    goto recycle;

  case CONSTANT_TERM:
  case VARIABLE:
  case ARITH_EQ_ATOM:
  case ARITH_GE_ATOM:
  case ARITH_IS_INT_ATOM:
  case ARITH_FLOOR:
  case ARITH_CEIL:
  case ARITH_ABS:
    // The descriptor is an integer nothing to delete.
    h = hash_integer_term(table->kind[i], table->type[i], table->desc[i].integer);
    break;

  case ITE_TERM:
  case TUPLE_TERM:
  case EQ_TERM:
  case DISTINCT_TERM:
  case OR_TERM:
  case XOR_TERM:
  case ARITH_BINEQ_ATOM:
  case ARITH_RDIV:
  case ARITH_IDIV:
  case ARITH_MOD:
  case ARITH_DIVIDES_ATOM:
  case BV_ARRAY:
  case BV_DIV:
  case BV_REM:
  case BV_SDIV:
  case BV_SREM:
  case BV_SMOD:
  case BV_SHL:
  case BV_LSHR:
  case BV_ASHR:
  case BV_EQ_ATOM:
  case BV_GE_ATOM:
  case BV_SGE_ATOM:
    // Generic composite
    d = table->desc[i].ptr;
    h = hash_composite_term(table->kind[i], d->arity, d->arg);
    safe_free(d);
    break;

  case ITE_SPECIAL:
    // Special composite:
    // call the finalizer before deleting the descriptor
    d = table->desc[i].ptr;
    h = hash_composite_term(table->kind[i], d->arity, d->arg);
    table->finalize(special_desc(d), ITE_SPECIAL);
    safe_free(special_desc(d));
    break;

  case APP_TERM:
    d = table->desc[i].ptr;
    n = d->arity;
    assert(n >= 2);
    h = hash_app_term(d->arg[0], n-1, d->arg + 1);
    safe_free(d);
    break;

  case UPDATE_TERM:
    d = table->desc[i].ptr;
    n = d->arity;
    assert(n >= 3);
    h = hash_update_term(d->arg[0], n-2, d->arg + 1, d->arg[n-1]);
    safe_free(d);
    break;

  case FORALL_TERM:
    d = table->desc[i].ptr;
    n = d->arity;
    assert(n >= 2);
    h = hash_forall_term(n-1, d->arg, d->arg[n-1]);
    safe_free(d);
    break;

  case LAMBDA_TERM:
    d = table->desc[i].ptr;
    n = d->arity;
    assert(n >= 2);
    h = hash_lambda_term(n-1, d->arg, d->arg[n-1]);
    safe_free(d);
    break;

  case SELECT_TERM:
  case BIT_TERM:
    // Select terms: nothing to delete.
    s = &table->desc[i].select;
    h = hash_select_term(table->kind[i], s->idx, s->arg);
    break;

  case ARITH_ROOT_ATOM:
    // Root atoms
    r = table->desc[i].ptr;
    h = hash_root_atom(r->k, r->x, r->p, r->r);
    safe_free(r);
    break;

  case POWER_PRODUCT:
    // Power products are deleted in garbage collection of pprod.
    h = hash_power_product(table->desc[i].ptr);
    break;

  case ARITH_CONSTANT:
    // Free the rational
    h = hash_rational_term(ARITH_CONSTANT, table->type[i], &table->desc[i].rational);
    q_clear(&table->desc[i].rational);
    break;

  case ARITH_POLY:
    h = hash_polynomial(table->desc[i].ptr);
    free_polynomial(table->desc[i].ptr);
    break;

  case BV64_CONSTANT:
    c64 = table->desc[i].ptr;
    h = hash_bvconst64_term(c64->bitsize, c64->value);
    safe_free(c64);
    break;

  case BV_CONSTANT:
    c = table->desc[i].ptr;
    h = hash_bvconst_term(c->bitsize, c->data);
    safe_free(c);
    break;

  case BV64_POLY:
    h = hash_bvpoly64(table->desc[i].ptr);
    free_bvpoly64(table->desc[i].ptr);
    break;

  case BV_POLY:
    h = hash_bvpoly(table->desc[i].ptr);
    free_bvpoly(table->desc[i].ptr);
    break;

  case UNUSED_TERM:
  case RESERVED_TERM:
  default:
    assert(false);
    break;
  }

  // Remove the record [h, i] from the hash-consing table
  int_htbl_erase_record(&table->htbl, h, i);

  // Put i in the free list
 recycle:
  table->desc[i].integer = table->free_idx;
  table->free_idx = i;
  table->kind[i] = UNUSED_TERM;

  assert(table->live_terms > 0);
  table->live_terms --;
}







/*
 * TABLE INITIALIZATION
 */

/*
 * Build a dummy term at index 0 (to make sure nothing collides
 * with the const_idx used in rationals and bitvector polynomials).
 *
 * Add the boolean constant and the zero constant
 */
static void add_primitive_terms(term_table_t *table) {
  rational_t q;
  int32_t i;

  i = allocate_term_id(table);
  assert(i == const_idx);
  table->kind[i] = RESERVED_TERM;
  table->type[i] = NULL_TYPE;
  table->desc[i].ptr = NULL;

  i = constant_term(table, bool_type(table->types), 0);
  assert(i == true_term);

  q_init(&q);
  i = arith_constant(table, &q);
  assert(i == zero_term && term_type(table, i) == int_type(table->types));
  q_clear(&q);
}


/*
 * Initialize table with initial size = n.
 * Create the built-in constants and reserved term
 */
void init_term_table(term_table_t *table, uint32_t n, type_table_t *ttbl, pprod_table_t *ptbl) {
  term_table_init(table, n, ttbl, ptbl);
  add_primitive_terms(table);
}





/*
 * TABLE DELETION
 */

/*
 * Delete the name table: call decref on all strings.
 */
static void delete_name_table(ptr_hmap_t *table) {
  ptr_hmap_pair_t *p;

  p = ptr_hmap_first_record(table);
  while (p != NULL) {
    assert(p->val != NULL);
    string_decref(p->val);
    p = ptr_hmap_next_record(table, p);
  }

  delete_ptr_hmap(table);
}


/*
 * Delete all the term descriptors
 */
static void delete_term_descriptors(term_table_t *table) {
  uint32_t i, n;

  n = table->nelems;
  for (i=0; i<n; i++) {
    switch (table->kind[i]) {
    case UNUSED_TERM:
    case RESERVED_TERM:
    case CONSTANT_TERM:
    case UNINTERPRETED_TERM:
    case VARIABLE:
    case POWER_PRODUCT:
    case ARITH_EQ_ATOM:
    case ARITH_GE_ATOM:
    case ARITH_IS_INT_ATOM:
    case ARITH_FLOOR:
    case ARITH_CEIL:
    case ARITH_ABS:
    case SELECT_TERM:
    case BIT_TERM:
      break;

    case ITE_TERM:
    case APP_TERM:
    case UPDATE_TERM:
    case TUPLE_TERM:
    case EQ_TERM:
    case DISTINCT_TERM:
    case FORALL_TERM:
    case LAMBDA_TERM:
    case OR_TERM:
    case XOR_TERM:
    case ARITH_BINEQ_ATOM:
    case ARITH_RDIV:
    case ARITH_IDIV:
    case ARITH_MOD:
    case ARITH_DIVIDES_ATOM:
    case ARITH_ROOT_ATOM:
    case BV64_CONSTANT:
    case BV_CONSTANT:
    case BV_ARRAY:
    case BV_DIV:
    case BV_REM:
    case BV_SDIV:
    case BV_SREM:
    case BV_SMOD:
    case BV_SHL:
    case BV_LSHR:
    case BV_ASHR:
    case BV_EQ_ATOM:
    case BV_GE_ATOM:
    case BV_SGE_ATOM:
      safe_free(table->desc[i].ptr);
      break;

    case ITE_SPECIAL:
      table->finalize(special_desc(table->desc[i].ptr), ITE_SPECIAL);
      safe_free(special_desc(table->desc[i].ptr));
      break;

    case ARITH_CONSTANT:
      // Free the rational
      q_clear(&table->desc[i].rational);
      break;

    case ARITH_POLY:
      free_polynomial(table->desc[i].ptr);
      break;

    case BV64_POLY:
      free_bvpoly64(table->desc[i].ptr);
      break;

    case BV_POLY:
      free_bvpoly(table->desc[i].ptr);
      break;

    default:
      assert(false);
      break;
    }
  }
}



/*
 * Delete table
 */
void delete_term_table(term_table_t *table) {
  delete_name_table(&table->ntbl);
  delete_term_descriptors(table);
  delete_int_hmap(&table->utbl);
  delete_int_htbl(&table->htbl);
  delete_stbl(&table->stbl);

  delete_ivector(&table->ibuffer);
  delete_pvector(&table->pbuffer);

  safe_free(table->kind);
  safe_free(table->type);
  safe_free(table->desc);
  delete_bitvector(table->mark);

  table->kind = NULL;
  table->type = NULL;
  table->desc = NULL;
  table->mark = NULL;


}


/*
 * RESET
 */

/*
 * Reset the name table: first call decref on all strings
 */
static void reset_name_table(ptr_hmap_t *table) {
  ptr_hmap_pair_t *p;

  p = ptr_hmap_first_record(table);
  while (p != NULL) {
    assert(p->val != NULL);
    string_decref(p->val);
    p = ptr_hmap_next_record(table, p);
  }
  ptr_hmap_reset(table);
}


/*
 * Full reset: delete all terms, reset the symbol table,
 * and all internal structures.
 */
void reset_term_table(term_table_t *table) {
  reset_name_table(&table->ntbl);
  delete_term_descriptors(table);
  int_hmap_reset(&table->utbl);
  reset_int_htbl(&table->htbl);
  reset_stbl(&table->stbl);

  ivector_reset(&table->ibuffer);
  pvector_reset(&table->pbuffer);

  table->nelems = 0;
  table->free_idx = -1;
  table->live_terms = 0;

  add_primitive_terms(table);
}


/*
 * TYPE COMPUTATIONS
 */

/*
 * Type of (tuple arg[0] ... arg[n-1])
 */
static type_t type_of_tuple(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t *v;
  type_t tau;
  uint32_t j;

  // build the type using ibuffer
  assert(table->ibuffer.size == 0);
  resize_ivector(&table->ibuffer, n);
  v = table->ibuffer.data;
  for (j=0; j<n; j++) {
    v[j] = term_type(table, arg[j]);
  }
  tau = tuple_type(table->types, n, v);

  ivector_reset(&table->ibuffer);

  return tau;
}

/*
 * Type of (lambda v[0] ... v[n-1] t)
 */
static type_t type_of_lambda(term_table_t *table, uint32_t n, const term_t *v, term_t t) {
  int32_t *dom;
  type_t tau;
  uint32_t j;

  // use ibuffer;
  assert(table->ibuffer.size == 0);
  resize_ivector(&table->ibuffer, n);
  dom = table->ibuffer.data;
  for (j=0; j<n; j++) {
    dom[j] = term_type(table, v[j]);
  }
  tau = term_type(table, t); // range type
  tau = function_type(table->types, tau, n, dom);

  ivector_reset(&table->ibuffer);

  return tau;
}


/*
 * Power product r
 * - r must not be a tagged variable or empty_pp or end_pp
 * - we assume r is well formed:
 *   either all variables of r are bitvectors of the same type
 *   or all variables of r are integer or real.
 * - type of r = int if all variables are integer
 *             = real if one variable is real
 *             = type of the first variable otherwise
 */
static type_t type_of_pprod(term_table_t *table, pprod_t *r) {
  uint32_t i, n;
  type_t tau;

  n = r->len;
  tau = term_type(table, r->prod[0].var);

  if (is_integer_type(tau)) {
    // check whether all variables of r are integer
    for (i=1; i<n; i++) {
      tau = term_type(table, r->prod[i].var);
      if (! is_integer_type(tau)) break;
    }
  }

  return tau;
}




/*
 * TERM CONSTRUCTORS
 */

/*
 * Constant of the given type and index.
 * - tau must be uninterpreted or scalar
 * - if tau is scalar of cardinality n, then index must be between 0 and n-1
 */
term_t constant_term(term_table_t *table, type_t tau, int32_t index) {
  int32_t i;
  integer_term_hobj_t integer_hobj;

  integer_hobj.m.hash = (hobj_hash_t) hash_integer_hobj;
  integer_hobj.m.eq = (hobj_eq_t) eq_integer_hobj;
  integer_hobj.m.build = (hobj_build_t) build_integer_hobj;
  integer_hobj.tbl = table;
  integer_hobj.tag = CONSTANT_TERM;
  integer_hobj.tau = tau;
  integer_hobj.id = index;

  i = int_htbl_get_obj(&table->htbl, &integer_hobj.m);

  return pos_term(i);
}


/*
 * Declare a new uninterpreted constant of type tau.
 * - this always creates a fresh term
 */
term_t new_uninterpreted_term(term_table_t *table, type_t tau) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = UNINTERPRETED_TERM;
  table->type[i] = tau;
  table->desc[i].ptr = NULL;

  return pos_term(i);
}


/*
 * New variable of type tau.
 * - create a fresh term
 */
term_t new_variable(term_table_t *table, type_t tau) {
  int32_t i;

  i = allocate_term_id(table);
  table->kind[i] = VARIABLE;
  table->type[i] = tau;
  table->desc[i].integer = i;

  return pos_term(i);
}



/*
 * Negation: just flip the polarity bit
 * - p must be boolean
 */
term_t not_term(term_table_t *table, term_t p) {
  assert(is_boolean_term(table, p));
  return opposite_term(p);
}


/*
 * Check whether (ite ? left right) should be a special if-then-else:
 * - i.e., left and right are both constant or special.
 */
static bool special_or_constant(term_kind_t tag) {
  return tag == ITE_SPECIAL || is_const_kind(tag);
}

static bool make_special_ite(term_table_t *table, term_t left, term_t right) {
  return special_or_constant(term_kind(table, left)) && special_or_constant(term_kind(table, right));
}


/*
 * If-then-else term (if cond then left else right)
 * - tau must be the super type of left/right.
 * - if left and right are both constant or special if-then-else
 *   we build a special if-then-else term.
 */
term_t ite_term(term_table_t *table, type_t tau, term_t cond, term_t left, term_t right) {
  term_t aux[3];
  int32_t i;

  aux[0] = cond;
  aux[1] = left;
  aux[2] = right;

  if (make_special_ite(table, left, right)) {
    composite_term_hobj_t special_hobj;

    special_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
    special_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
    special_hobj.m.build = (hobj_build_t) build_special_hobj;
    special_hobj.tbl = table;
    special_hobj.tag = ITE_SPECIAL;
    special_hobj.tau = tau;
    special_hobj.arity = 3;
    special_hobj.arg = aux;

    i = int_htbl_get_obj(&table->htbl, &special_hobj.m);

  } else {
    composite_term_hobj_t composite_hobj;

    composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
    composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
    composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
    composite_hobj.tbl = table;
    composite_hobj.tag = ITE_TERM;
    composite_hobj.tau = tau;
    composite_hobj.arity = 3;
    composite_hobj.arg = aux;

    i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);
  }

  return pos_term(i);
}


/*
 * Function application: (fun arg[0] ... arg[n-1])
 */
term_t app_term(term_table_t *table, term_t fun, uint32_t n, const term_t arg[]) {
  type_t tau;
  int32_t i;
  app_term_hobj_t app_hobj;

  tau = term_type(table, fun);

  app_hobj.m.hash = (hobj_hash_t) hash_app_hobj;
  app_hobj.m.eq = (hobj_eq_t) eq_app_hobj;
  app_hobj.m.build = (hobj_build_t) build_app_hobj;
  app_hobj.tbl = table;
  app_hobj.tau = function_type_range(table->types, tau); // range of fun
  app_hobj.f = fun;
  app_hobj.n = n;
  app_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &app_hobj.m);

  return pos_term(i);
}


/*
 * Function update: (update fun arg[0] ... arg[n-1] new_v)
 * - new_v must be in the range of fun (not in a supertype)
 * - the result has the same type as fun
 */
term_t update_term(term_table_t *table, term_t fun, uint32_t n, const term_t arg[], term_t new_v) {
  type_t tau;
  int32_t i;
  update_term_hobj_t update_hobj;

  tau = term_type(table, fun);

  update_hobj.m.hash = (hobj_hash_t) hash_update_hobj;
  update_hobj.m.eq = (hobj_eq_t) eq_update_hobj;
  update_hobj.m.build = (hobj_build_t) build_update_hobj;
  update_hobj.tbl = table;
  update_hobj.tau = tau;
  update_hobj.f = fun;
  update_hobj.v = new_v;
  update_hobj.n = n;
  update_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &update_hobj.m);

  return pos_term(i);
}


/*
 * (tuple arg[0] .. arg[n-1])
 */
term_t tuple_term(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t i;
  composite_term_hobj_t composite_hobj;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = TUPLE_TERM;
  composite_hobj.tau = type_of_tuple(table, n, arg);
  composite_hobj.arity = n;
  composite_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}


/*
 * Tuple projection (select index tuple)
 */
term_t select_term(term_table_t *table, uint32_t index, term_t tuple) {
  type_t tau;
  int32_t i;
  select_term_hobj_t select_hobj;

  tau = term_type(table, tuple);

  select_hobj.m.hash = (hobj_hash_t) hash_select_hobj;
  select_hobj.m.eq = (hobj_eq_t) eq_select_hobj;
  select_hobj.m.build = (hobj_build_t) build_select_hobj;
  select_hobj.tbl = table;
  select_hobj.tag = SELECT_TERM;
  select_hobj.tau = tuple_type_component(table->types, tau, index);;
  select_hobj.k = index;
  select_hobj.arg = tuple;

  i = int_htbl_get_obj(&table->htbl, &select_hobj.m);

  return pos_term(i);
}


/*
 * Binary term defined by (tag, tau, left, right)
 */
static term_t binary_term(term_table_t *table, term_kind_t tag, type_t tau, term_t left, term_t right) {
  term_t aux[2];
  int32_t i;
  composite_term_hobj_t composite_hobj;

  aux[0] = left;
  aux[1] = right;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = tag;
  composite_hobj.tau = tau;
  composite_hobj.arity = 2;
  composite_hobj.arg = aux;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}


/*
 * One-argument term: defined by (tag, tau, t)
 */
static term_t unary_term(term_table_t *table, term_kind_t tag, type_t tau, term_t t) {
  int32_t i;
  integer_term_hobj_t integer_hobj;

  integer_hobj.m.hash = (hobj_hash_t) hash_integer_hobj;
  integer_hobj.m.eq = (hobj_eq_t) eq_integer_hobj;
  integer_hobj.m.build = (hobj_build_t) build_integer_hobj;
  integer_hobj.tbl = table;
  integer_hobj.tag = tag;
  integer_hobj.tau = tau;
  integer_hobj.id = t;

  i = int_htbl_get_obj(&table->htbl, &integer_hobj.m);

  return pos_term(i);
}


/*
 * Equality (eq left right)
 */
term_t eq_term(term_table_t *table, term_t left, term_t right) {
  return binary_term(table, EQ_TERM, bool_type(table->types), left, right);
}


/*
 * (distinct arg[0] ... arg[n-1])
 */
term_t distinct_term(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t i;
  composite_term_hobj_t composite_hobj;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = DISTINCT_TERM;
  composite_hobj.tau = bool_type(table->types);
  composite_hobj.arity = n;
  composite_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}


/*
 * (forall var[0] ... var[n-1] body)
 */
term_t forall_term(term_table_t *table, uint32_t n, const term_t var[], term_t body) {
  int32_t i;
  forall_term_hobj_t forall_hobj;

  forall_hobj.m.hash = (hobj_hash_t) hash_forall_hobj;
  forall_hobj.m.eq = (hobj_eq_t) eq_forall_hobj;
  forall_hobj.m.build = (hobj_build_t) build_forall_hobj;
  forall_hobj.tbl = table;
  forall_hobj.p = body;
  forall_hobj.n = n;
  forall_hobj.v = var;

  i = int_htbl_get_obj(&table->htbl, &forall_hobj.m);

  return pos_term(i);
}


/*
 * (lambda var[0] ... var[n-1] body)
 */
term_t lambda_term(term_table_t *table, uint32_t n, const term_t var[], term_t body) {
  int32_t i;
  lambda_term_hobj_t lambda_hobj;

  lambda_hobj.m.hash = (hobj_hash_t) hash_lambda_hobj;
  lambda_hobj.m.eq = (hobj_eq_t) eq_lambda_hobj;
  lambda_hobj.m.build = (hobj_build_t) build_lambda_hobj;
  lambda_hobj.tbl = table;
  lambda_hobj.tau = type_of_lambda(table, n, var, body);
  lambda_hobj.t = body;
  lambda_hobj.n = n;
  lambda_hobj.v = var;

  i = int_htbl_get_obj(&table->htbl, &lambda_hobj.m);

  return pos_term(i);
}


/*
 * (or arg[0] ... arg[n-1])
 */
term_t or_term(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t i;
  composite_term_hobj_t composite_hobj;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = OR_TERM;
  composite_hobj.tau = bool_type(table->types);
  composite_hobj.arity = n;
  composite_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}


/*
 * (xor arg[0] ... arg[n-1])
 */
term_t xor_term(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t i;
  composite_term_hobj_t composite_hobj;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = XOR_TERM;
  composite_hobj.tau = bool_type(table->types);
  composite_hobj.arity = n;
  composite_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}


/*
 * Bit-select: get bit k of bit-vector bv
 */
term_t bit_term(term_table_t *table, uint32_t k, term_t bv) {
  int32_t i;
  select_term_hobj_t select_hobj;

  select_hobj.m.hash = (hobj_hash_t) hash_select_hobj;
  select_hobj.m.eq = (hobj_eq_t) eq_select_hobj;
  select_hobj.m.build = (hobj_build_t) build_select_hobj;
  select_hobj.tbl = table;
  select_hobj.tag = BIT_TERM;
  select_hobj.tau = bool_type(table->types);
  select_hobj.k = k;
  select_hobj.arg = bv;

  i = int_htbl_get_obj(&table->htbl, &select_hobj.m);

  return pos_term(i);
}


/*
 * Power product: r must be valid in table->ptbl, and must not be a tagged
 * variable or empty_pp.
 * - each variable index x_i in r must be a term defined in table
 * - the x_i's must have compatible types: either they are all arithmetic
 *   terms (type int or real) or they are all bit-vector terms of the
 *   same type.
 * The type of the result is determined from the x_i's types:
 * - if all x_i's are int, the result is int
 * - if some x_i's are int, some are real, the result is real
 * - if all x_i's have type (bitvector k), the result has type (bitvector k)
 */
term_t pprod_term(term_table_t *table, pprod_t *r) {
  int32_t i;
  pprod_term_hobj_t pprod_hobj;

  pprod_hobj.m.hash = (hobj_hash_t) hash_pprod_hobj;
  pprod_hobj.m.eq = (hobj_eq_t) eq_pprod_hobj;
  pprod_hobj.m.build = (hobj_build_t) build_pprod_hobj;
  pprod_hobj.tbl = table;
  pprod_hobj.tau = type_of_pprod(table, r);
  pprod_hobj.r = r;

  i = int_htbl_get_obj(&table->htbl, &pprod_hobj.m);

  return pos_term(i);
}


/*
 * Rational constant: the result has type int if a is an integer or real otherwise
 */
term_t arith_constant(term_table_t *table, rational_t *a) {
  type_t tau;
  int32_t i;
  rational_term_hobj_t rational_hobj;

  tau = real_type(table->types);
  if (q_is_integer(a)) {
    tau = int_type(table->types);
  }

  rational_hobj.m.hash = (hobj_hash_t) hash_rational_hobj;
  rational_hobj.m.eq = (hobj_eq_t) eq_rational_hobj;
  rational_hobj.m.build = (hobj_build_t) build_rational_hobj;
  rational_hobj.tbl = table;
  rational_hobj.tag = ARITH_CONSTANT;
  rational_hobj.tau = tau;
  rational_hobj.a = a;

  i = int_htbl_get_obj(&table->htbl, &rational_hobj.m);

  return pos_term(i);
}


/*
 * Atom t == 0 for an arithmetic term t
 */
term_t arith_eq_atom(term_table_t *table, term_t t) {
  return unary_term(table, ARITH_EQ_ATOM, bool_type(table->types), t);
}


/*
 * Atom (t >= 0) for an arithmetic term t
 */
term_t arith_geq_atom(term_table_t *table, term_t t) {
  return unary_term(table, ARITH_GE_ATOM, bool_type(table->types), t);
}


/*
 * Equality between two arithmetic terms (left == right)
 */
term_t arith_bineq_atom(term_table_t *table, term_t left, term_t right) {
  return binary_term(table, ARITH_BINEQ_ATOM, bool_type(table->types), left, right);
}


/*
 * Test for integrality: (is_int x)
 */
term_t arith_is_int(term_table_t *table, term_t x) {
  return unary_term(table, ARITH_IS_INT_ATOM, bool_type(table->types), x);
}

/*
 * Floor and ceiling: the result has type int
 */
term_t arith_floor(term_table_t *table, term_t x) {
  return unary_term(table, ARITH_FLOOR, int_type(table->types), x);
}

term_t arith_ceil(term_table_t *table, term_t x) {
  return unary_term(table, ARITH_CEIL, int_type(table->types), x);
}

/*
 * Absolute value: the result has the same type as x
 */
term_t arith_abs(term_table_t *table, term_t x) {
  type_t tau;

  tau = term_type(table, x);
  return unary_term(table, ARITH_ABS, tau, x);
}

/*
 * (div x y): the result has type int
 */
term_t arith_idiv(term_table_t *table, term_t x, term_t y) {
  return binary_term(table, ARITH_IDIV, int_type(table->types), x, y);
}

/*
 * (mod x y) = x - y * (div x y)
 * So the result has type int if both x and y are integers
 */
term_t arith_mod(term_table_t *table, term_t x, term_t y) {
  type_t tau;

  tau = is_integer_term(table, x) ? term_type(table, y) : real_type(table->types);
  return binary_term(table, ARITH_MOD, tau, x, y);
}

/*
 * Test whether x divides y
 */
term_t arith_divides(term_table_t *table, term_t x, term_t y) {
  return binary_term(table, ARITH_DIVIDES_ATOM, bool_type(table->types), x, y);
}



/*
 * Root constraint x r root_k(p).
 */
term_t arith_root_atom(term_table_t *table, uint32_t k, term_t x, term_t p, root_atom_rel_t r) {
  int32_t i;
  root_atom_hobj_t root_atom_hobj;

  root_atom_hobj.m.hash = (hobj_hash_t) hash_root_atom_hobj;
  root_atom_hobj.m.eq = (hobj_eq_t) eq_root_atom_hobj;
  root_atom_hobj.m.build = (hobj_build_t) build_root_atom_hobj;
  root_atom_hobj.tbl = table;
  root_atom_hobj.k = k;
  root_atom_hobj.x = x;
  root_atom_hobj.p = p;
  root_atom_hobj.r = r;

  i = int_htbl_get_obj(&table->htbl, &root_atom_hobj.m);

  return pos_term(i);
}


/*
 * Real division: the result (/ x y) has type real
 */
term_t arith_rdiv(term_table_t *table, term_t x, term_t y) {
  return binary_term(table, ARITH_RDIV, real_type(table->types), x, y);
}


/*
 * Small bitvector constant
 * - n = bitsize (must be between 1 and 64)
 * - bv = value (must be normalized modulo 2^n)
 */
term_t bv64_constant(term_table_t *table, uint32_t n, uint64_t bv) {
  int32_t i;
  bvconst64_term_hobj_t bvconst64_hobj;

  bvconst64_hobj.m.hash = (hobj_hash_t) hash_bvconst64_hobj;
  bvconst64_hobj.m.eq = (hobj_eq_t) eq_bvconst64_hobj;
  bvconst64_hobj.m.build = (hobj_build_t) build_bvconst64_hobj;
  bvconst64_hobj.tbl = table;
  bvconst64_hobj.tau = bv_type(table->types, n);
  bvconst64_hobj.bitsize = n;
  bvconst64_hobj.v = bv;

  i = int_htbl_get_obj(&table->htbl, &bvconst64_hobj.m);

  return pos_term(i);
}


/*
 * Bitvector constant:
 * - n = bitsize
 * - bv = array of k words (where k = ceil(n/32))
 * The constant must be normalized (modulo 2^n)
 * This constructor should be used only for n > 64.
 */
term_t bvconst_term(term_table_t *table, uint32_t n, const uint32_t *bv) {
  int32_t i;
  bvconst_term_hobj_t bvconst_hobj;

  bvconst_hobj.m.hash = (hobj_hash_t) hash_bvconst_hobj;
  bvconst_hobj.m.eq = (hobj_eq_t) eq_bvconst_hobj;
  bvconst_hobj.m.build = (hobj_build_t) build_bvconst_hobj;
  bvconst_hobj.tbl = table;
  bvconst_hobj.tau = bv_type(table->types, n);
  bvconst_hobj.bitsize = n;
  bvconst_hobj.v = bv;

  i = int_htbl_get_obj(&table->htbl, &bvconst_hobj.m);

  return pos_term(i);
}


/*
 * Bitvector formed of arg[0] ... arg[n-1]
 * - n must be positive and no more than YICES_MAX_BVSIZE
 * - arg[0] ... arg[n-1] must be boolean terms
 */
term_t bvarray_term(term_table_t *table, uint32_t n, const term_t arg[]) {
  int32_t i;
  composite_term_hobj_t composite_hobj;

  composite_hobj.m.hash = (hobj_hash_t) hash_composite_hobj;
  composite_hobj.m.eq = (hobj_eq_t) eq_composite_hobj;
  composite_hobj.m.build = (hobj_build_t) build_composite_hobj;
  composite_hobj.tbl = table;
  composite_hobj.tag = BV_ARRAY;
  composite_hobj.tau = bv_type(table->types, n);
  composite_hobj.arity = n;
  composite_hobj.arg = arg;

  i = int_htbl_get_obj(&table->htbl, &composite_hobj.m);

  return pos_term(i);
}



/*
 * Division and shift operators
 * - the two arguments must be bitvector terms of the same type
 * - in the division/remainder operators, b is the divisor
 * - in the shift operator: a is the bitvector to be shifted
 *   and b is the shift amount
 * - in all cases, the result has the same type as a and b
 */
term_t bvdiv_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_DIV, term_type(table, a), a, b);
}

term_t bvrem_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_REM, term_type(table, a), a, b);
}

term_t bvsdiv_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_SDIV, term_type(table, a), a, b);
}

term_t bvsrem_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_SREM, term_type(table, a), a, b);
}

term_t bvsmod_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_SMOD, term_type(table, a), a, b);
}

term_t bvshl_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_SHL, term_type(table, a), a, b);
}

term_t bvlshr_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_LSHR, term_type(table, a), a, b);
}

term_t bvashr_term(term_table_t *table, term_t a, term_t b) {
  return binary_term(table, BV_ASHR, term_type(table, a), a, b);
}


/*
 * Bitvector atoms: l and r must be bitvector terms of the same type
 *  (bveq l r): l == r
 *  (bvge l r): l >= r unsigned
 *  (bvsge l r): l >= r signed
 */
term_t bveq_atom(term_table_t *table, term_t l, term_t r) {
  return binary_term(table, BV_EQ_ATOM, bool_type(table->types), l, r);
}

term_t bvge_atom(term_table_t *table, term_t l, term_t r) {
  return binary_term(table, BV_GE_ATOM, bool_type(table->types), l, r);
}

term_t bvsge_atom(term_table_t *table, term_t l, term_t r) {
  return binary_term(table, BV_SGE_ATOM, bool_type(table->types), l, r);
}




/*
 * POWER PRODUCT
 */

/*
 * Power product built from a buffer b
 * - b must not be empty
 */
term_t pprod_term_from_buffer(term_table_t *table, pp_buffer_t *b) {
  pprod_t *r;

  r = pprod_from_buffer(table->pprods, b);
  assert(!pp_is_empty(r));

  if (pp_is_var(r)) {
    return var_of_pp(r);
  } else {
    return pprod_term(table, r);
  }
}



/*
 * POLYNOMIAL TERM CONSTRUCTORS
 */

/*
 * Convert power product r to an equivalent integer index
 * - empty_pp --> const_idx
 * - tagged variable x --> x (x must be a term)
 * - otherwise, build a power product term t for r and return t
 */
static int32_t poly_index_for_pprod(term_table_t *table, pprod_t *r) {
  int32_t i;

  assert(r != end_pp);

  if (pp_is_empty(r)) {
    i = const_idx;
  } else if (pp_is_var(r)) {
    i = var_of_pp(r);
  } else {
    i = pprod_term(table, r);
  }

  return i;
}


/*
 * Check whether all terms in array v are integers
 * - skip const_idx if it's in v (it should be first)
 */
static bool all_integer_terms(term_table_t *table, const term_t *v, uint32_t n) {
  uint32_t i;

  if (n > 0) {
    if (v[0] == const_idx) {
      v ++;
      n --;
    }

    for (i=0; i<n; i++) {
      assert(is_arithmetic_term(table, v[i]));
      if (is_real_term(table, v[i])) return false;
    }
  }

  return true;
}


/*
 * Auxiliary function: convert power products of subtree rooted at x
 * to term indices and check whether all coefficients are integer
 * - input: x = node in the buffer b
 *          i = number of nodes in the subtree at the left of x
 *          v = array to store conversion
 * - output: return i + number of nodes in the subtree rooted at x
 *   update *all_int so that it's true if all nodes in x have
 *   integer coefficients and *all_int was true on entry to the function
 *
 * So v[i] will store the conversion of the left-most monomial in x's subtree
 */
static uint32_t convert_rba_tree(term_table_t *table, rba_buffer_t *b, int32_t *v, bool *all_int,
                                 uint32_t i, uint32_t x) {
  assert(x < b->num_nodes);

  if (x != rba_null) {
    i = convert_rba_tree(table, b, v, all_int, i, b->child[x][0]);
    assert(i < b->nterms);
    v[i] = poly_index_for_pprod(table, b->mono[x].prod);
    *all_int = *all_int && q_is_integer(&b->mono[x].coeff);
    i = convert_rba_tree(table, b, v, all_int, i+1, b->child[x][1]);
  }

  return i;
}


/*
 * Arithmetic term
 * - all variables of b must be real or integer terms defined in table
 * - b must be normalized and b->ptbl must be the same as table->ptbl
 * - if b contains a non-linear polynomial then the power products that
 *   occur in p are converted to terms (using pprod_term)
 * - then b is turned into a polynomial object a_1 x_1 + ... + a_n x_n,
 *   where x_i is a term.
 *
 * SIDE EFFECT: b is reset to zero
 */
term_t arith_poly(term_table_t *table, rba_buffer_t *b) {
  int32_t *v;
  type_t tau;
  int32_t i;
  bool all_int;
  uint32_t j, n;
  poly_term_hobj_t poly_hobj;

  assert(b->ptbl == table->pprods);

  n = b->nterms;

  /*
   * convert the power products to indices
   * store the result in ibuffer.
   * also check whether all coefficients are integer.
   */
  assert(table->ibuffer.size == 0);

  resize_ivector(&table->ibuffer, n + 1);
  v = table->ibuffer.data;
  all_int = true;
  j = convert_rba_tree(table, b, v, &all_int, 0, b->root);
  assert(j == n);
  v[j] = max_idx;

  // type of b: either int or real
  tau = real_type(table->types);
  if (all_int && all_integer_terms(table, v, n)) {
    tau = int_type(table->types);
  }

  // hash consing
  poly_hobj.m.hash = (hobj_hash_t) hash_poly_hobj;
  poly_hobj.m.eq = (hobj_eq_t) eq_poly_hobj;
  poly_hobj.m.build = (hobj_build_t) build_poly_hobj;
  poly_hobj.tbl = table;
  poly_hobj.tau = tau;
  poly_hobj.b = b;
  poly_hobj.v = v;

  i = int_htbl_get_obj(&table->htbl, &poly_hobj.m);

  // cleanup ibuffer
  ivector_reset(&table->ibuffer);

  return pos_term(i);
}


/*
 * Bitvector polynomials are constructed from a buffer b
 * - all variables of b must be bitvector terms defined in table
 * - b must be normalized and b->ptbl must be the same as table->ptbl
 * - if b contains non-linear terms, then the power products that
 *   occur in b are converted to terms (using pprod_term) then
 *   a polynomial object is created.
 *
 * SIDE EFFECT: b is reset to zero.
 */
term_t bv64_poly(term_table_t *table, bvarith64_buffer_t *b) {
  bvmlist64_t *q;
  int32_t *v;
  int32_t i;
  uint32_t j, n;
  bvpoly64_term_hobj_t bvpoly64_hobj;

  assert(b->ptbl == table->pprods);

  n = b->nterms;

  /*
   * Convert the power products.
   * Store the results in ibuffer.
   */
  assert(table->ibuffer.size == 0);
  resize_ivector(&table->ibuffer, n + 1);
  v = table->ibuffer.data;
  q = b->list;
  for (j=0; j<n; j++) {
    assert(q->next != NULL);
    v[j] = poly_index_for_pprod(table, q->prod);
    q = q->next;
  }

  assert(q->next == NULL && q->prod == end_pp);
  v[j] = max_idx;

  // hash consing
  bvpoly64_hobj.m.hash = (hobj_hash_t) hash_bvpoly64_hobj;
  bvpoly64_hobj.m.eq = (hobj_eq_t) eq_bvpoly64_hobj;
  bvpoly64_hobj.m.build = (hobj_build_t) build_bvpoly64_hobj ;
  bvpoly64_hobj.tbl = table;
  bvpoly64_hobj.tau = bv_type(table->types, b->bitsize);
  bvpoly64_hobj.b = b;
  bvpoly64_hobj.v = v;

  i = int_htbl_get_obj(&table->htbl, &bvpoly64_hobj.m);

  // cleanup ibuffer
  ivector_reset(&table->ibuffer);

  return pos_term(i);
}


term_t bv_poly(term_table_t *table, bvarith_buffer_t *b) {
  bvmlist_t *q;
  int32_t *v;
  int32_t i;
  uint32_t j, n;
  bvpoly_term_hobj_t bvpoly_hobj;

  assert(b->ptbl == table->pprods);

  n = b->nterms;

  /*
   * Convert the power products.
   * Store the results in ibuffer.
   */
  assert(table->ibuffer.size == 0);
  resize_ivector(&table->ibuffer, n+1);
  v = table->ibuffer.data;
  q = b->list;
  for (j=0; j<n; j++) {
    assert(q->next != NULL);
    v[j] = poly_index_for_pprod(table, q->prod);
    q = q->next;
  }

  assert(q->next == NULL && q->prod == end_pp);
  v[j] = max_idx;

  // hash consing
  bvpoly_hobj.m.hash = (hobj_hash_t) hash_bvpoly_hobj;
  bvpoly_hobj.m.eq = (hobj_eq_t) eq_bvpoly_hobj;
  bvpoly_hobj.m.build = (hobj_build_t) build_bvpoly_hobj;
  bvpoly_hobj.tbl = table;
  bvpoly_hobj.tau = bv_type(table->types, b->bitsize);
  bvpoly_hobj.b = b;
  bvpoly_hobj.v = v;

  i = int_htbl_get_obj(&table->htbl, &bvpoly_hobj.m);

  // cleanup ibuffer
  ivector_reset(&table->ibuffer);

  return pos_term(i);
}


/*
 * Build/return a term equal to bvpoly_buffer b
 * - this works only for linear polynomials
 * - all variables of b must be terms defined in table
 * - b must be normalized
 * - b is not modified
 */
term_t bv_poly_from_buffer(term_table_t *table, bvpoly_buffer_t *b) {
  int32_t i;
  bvpoly_buffer_hobj_t bvbuffer_hobj;

  bvbuffer_hobj.m.hash = (hobj_hash_t) hash_bvpoly_buffer_hobj;
  bvbuffer_hobj.m.eq = (hobj_eq_t) eq_bvpoly_buffer_hobj;
  bvbuffer_hobj.m.build = (hobj_build_t) build_bvpoly_buffer_hobj;
  bvbuffer_hobj.tbl = table;
  bvbuffer_hobj.tau = bv_type(table->types, b->bitsize);
  bvbuffer_hobj.b = b;

  i = int_htbl_get_obj(&table->htbl, &bvbuffer_hobj.m);

  return pos_term(i);
}




/**********************************
 *  CONVERSION TO POWER PRODUCTS  *
 *********************************/

/*
 * Convert term t to a power product:
 * - t must be a term (not a term index) present in the table
 */
pprod_t *pprod_for_term(const term_table_t *table, term_t t) {
  pprod_t *r;
  int32_t i;

  assert(is_pos_term(t) && good_term(table, t));
  assert(is_arithmetic_term(table, t) || is_bitvector_term(table, t));

  r = var_pp(t);
  i = index_of(t);
  if (table->kind[i] == POWER_PRODUCT) {
    r = table->desc[i].ptr;
  }
  return r;
}


/*
 * Degree of x where x = main variable of a polynomial
 */
static uint32_t main_var_degree(const term_table_t *table, int32_t x) {
  uint32_t d;

  d = 1;
  if (x == const_idx) {
    d = 0;
  } else {
    assert(is_pos_term(x) && good_term(table, x));
    x = index_of(x);
    if (table->kind[x] == POWER_PRODUCT) {
      d = pprod_degree(table->desc[x].ptr);
    }
  }

  return d;
}


/*
 * Degree of term t
 * - t must be a good term of arithmetic or bitvector type
 */
uint32_t term_degree(const term_table_t *table, term_t t) {
  uint32_t d;
  int32_t i;

  assert(is_pos_term(t) && good_term(table, t));
  assert(is_arithmetic_term(table, t) || is_bitvector_term(table, t));

  d = 1;
  i = index_of(t);
  switch (table->kind[i]) {
  case POWER_PRODUCT:
    d = pprod_degree(table->desc[i].ptr);
    break;

  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
    d = 0;
    break;

  case ARITH_POLY:
    d = main_var_degree(table, polynomial_main_var(table->desc[i].ptr));
    break;

  case BV64_POLY:
    d = main_var_degree(table, bvpoly64_main_var(table->desc[i].ptr));
    break;

  case BV_POLY:
    d = main_var_degree(table, bvpoly_main_var(table->desc[i].ptr));
    break;
  }

  return d;
}


/*
 * Check whether x has degree 0 or 1 (i.e., x is not a power product)
 */
static bool not_pprod(const term_table_t *table, int32_t x) {
  assert(is_pos_term(x) && good_term(table, x));
  return table->kind[index_of(x)] != POWER_PRODUCT;
}

/*
 * Check whether t is a linear polynomial:
 * - t must be a good term of arithmetic or bitvector type.
 * - returns true if t has tag ARITH_POLY/BV64_POLY or BV_POLY
 *   and if no monomial of t is a power product.
 * - this implies that t has degree 1.
 */
bool is_linear_poly(const term_table_t *table, term_t t) {
  int32_t i;
  bool result;

  assert(is_pos_term(t) && good_term(table, t));
  assert(is_arithmetic_term(table, t) || is_bitvector_term(table, t));

  result = false;
  i = index_of(t);
  switch (table->kind[i]) {
  case ARITH_POLY:
    result = not_pprod(table, polynomial_main_var(table->desc[i].ptr));
    break;

  case BV64_POLY:
    result = not_pprod(table, bvpoly64_main_var(table->desc[i].ptr));
    break;

  case BV_POLY:
    result = not_pprod(table, bvpoly_main_var(table->desc[i].ptr));
    break;

  default:
    break;
  }

  return result;
}


/*
 * Convert all variables of p to power products
 * - store the result in table->pbuffer
 * - return the array of power products
 */
pprod_t **pprods_for_bvpoly64(term_table_t *table, const bvpoly64_t *p) {
  uint32_t i, n;
  void **v;

  n = p->nterms;
  resize_pvector(&table->pbuffer, n+1);
  v = table->pbuffer.data;
  i = 0;

  // the constant is first in p
  if (p->mono[0].var == const_idx) {
    v[0] = empty_pp;
    i = 1;
  }

  // rest of p
  while (i < n) {
    v[i] = pprod_for_term(table, p->mono[i].var);
    i ++;
  }
  // end marker
  assert(p->mono[i].var == max_idx);
  v[i] = end_pp;

  return (pprod_t **) v;
}


/*
 * Convert all variables of p to power products
 * - store the result in table->pbuffer
 * - return the array of power products
 */
pprod_t **pprods_for_bvpoly(term_table_t *table, const bvpoly_t *p) {
  uint32_t i, n;
  void **v;

  n = p->nterms;
  resize_pvector(&table->pbuffer, n+1);
  v = table->pbuffer.data;
  i = 0;

  // the constant is first in p
  if (p->mono[0].var == const_idx) {
    v[0] = empty_pp;
    i = 1;
  }

  // rest of p
  while (i < n) {
    v[i] = pprod_for_term(table, p->mono[i].var);
    i ++;
  }
  // end marker
  assert(p->mono[i].var == max_idx);
  v[i] = end_pp;

  return (pprod_t **) v;
}


/*
 * CHECKS ON TERMS
 */

/*
 * Good term: valid descriptor + polarity = 0 unless
 * t is a Boolean term.
 */
bool good_term(const term_table_t *table, term_t t) {
  return good_term_idx(table, index_of(t)) &&
    (is_pos_term(t) || type_for_idx(table, index_of(t)) == bool_id);
}

/*
 * Convert all variables of p to power products
 * - store the result in table->pbuffer
 * - return the array of power products
 */
pprod_t **pprods_for_poly(term_table_t *table, const polynomial_t *p) {
  uint32_t i, n;
  void **v;

  n = p->nterms;
  resize_pvector(&table->pbuffer, n+1);
  v = table->pbuffer.data;
  i = 0;

  // the constant is first in p
  if (p->mono[0].var == const_idx) {
    v[0] = empty_pp;
    i = 1;
  }

  // rest of p
  while (i < n) {
    v[i] = pprod_for_term(table, p->mono[i].var);
    i ++;
  }
  // end marker
  assert(p->mono[i].var == max_idx);
  v[i] = end_pp;

  return (pprod_t **) v;
}


/***************************
 *  TYPE CHECKING SUPPORT  *
 **************************/

/*
 * Wrapper function: check whether x has integer type
 */
static bool var_is_int(void *aux, int32_t x) {
  term_table_t *table;

  table = aux;
  return is_integer_type(term_type(table, x));
}

/*
 * Check whether b stores an integer polynomial
 */
bool arith_poly_is_integer(const term_table_t *table, rba_buffer_t *b) {
  return rba_buffer_is_int(b, (void*) table, var_is_int);
}



/*******************************
 *  CHECKS ON ATOMS/LITERALS   *
 ******************************/

/*
 * Check whether t is an arithmetic literal (i.e., arithmetic atom
 * or the negation of an arithmetic atom).
 */
bool is_arithmetic_literal(const term_table_t *table, term_t t) {
  switch (term_kind(table, t)) {
  case ARITH_EQ_ATOM:
  case ARITH_GE_ATOM:
  case ARITH_BINEQ_ATOM:
    return true;

  default:
    return false;
  }
}

/*
 * Test whether t is a bitvector literal
 */
bool is_bitvector_literal(const term_table_t *table, term_t t) {
  switch (term_kind(table, t)) {
  case BV_EQ_ATOM:
  case BV_GE_ATOM:
  case BV_SGE_ATOM:
    return true;

  default:
    return false;
  }
}


/********************
 *  CONSTANT TERMS  *
 *******************/

/*
 * Check whether t is a constant tuple.
 *
 * This uses a naive recursion without marking so subterms of t may be
 * visited many times (there's a risk of exponential cost). That
 * should not be a problem in practice unless people use deeply nested
 * tuples of tuples of tuples ...
 */
bool is_constant_tuple(const term_table_t *table, term_t t) {
  composite_term_t *tup;
  term_kind_t tag;
  uint32_t i, n;

  tup = tuple_term_desc(table, t);
  n = tup->arity;

  // first pass: avoid recursive calls
  for (i=0; i<n; i++) {
    tag = term_kind(table, tup->arg[i]);
    if (! is_const_kind(tag) && tag != TUPLE_TERM) {
      return false;
    }
  }

  // second pass: recursively check all subterms
  for (i=0; i<n; i++) {
    if (! is_const_term(table, tup->arg[i]) &&
        ! is_constant_tuple(table, tup->arg[i])) {
      return false;
    }
  }

  return true;
}



/*
 * Generic version: return true if t is an atomic constant
 * or a constant tuple.
 */
bool is_constant_term(const term_table_t *table, term_t t) {
  return is_const_term(table, t) ||
    (term_kind(table, t) == TUPLE_TERM && is_constant_tuple(table, t));
}




/*
 * Check whether the table contains a constant term of type tau and the given index
 * - tau must be uninterpreted or scalar
 * - if tau is scalar, then index must be between 0 and cardinality of tau - 1
 * - return NULL_TERM if there's no such term in table
 */
term_t find_constant_term(term_table_t *table, type_t tau, int32_t index) {
  int32_t i;
  integer_term_hobj_t integer_hobj;

  integer_hobj.m.hash = (hobj_hash_t) hash_integer_hobj;
  integer_hobj.m.eq = (hobj_eq_t) eq_integer_hobj;
  integer_hobj.m.build = (hobj_build_t) build_integer_hobj;
  integer_hobj.tbl = table;
  integer_hobj.tag = CONSTANT_TERM;
  integer_hobj.tau = tau;
  integer_hobj.id = index;

  i = int_htbl_find_obj(&table->htbl, &integer_hobj.m);
  if (i >= 0) {
    i = pos_term(i);
  }

  assert(i == NULL_TERM ||
         (term_kind(table, i) == CONSTANT_TERM && term_type(table, i) == tau
          && constant_term_index(table, i) == index));

  return i;
}





/***********************
 * GARBAGE COLLECTION  *
 **********************/

/*
 * MARKING
 */

/*
 * Mark all descendants of i whose ids are less than ptr
 * - i must be a marked term index and not already deleted.
 *
 * NOTE: check for risks for stack overflow here.
 */
static void mark_reachable_terms(term_table_t *table, int32_t ptr, int32_t i);

// mark i if it's not already marked then explore its children if i < ptr where i = index_of(t)
static void mark_and_explore_term(term_table_t *table, int32_t ptr, term_t t) {
  int32_t i;

  i = index_of(t);
  if (! term_idx_is_marked(table, i)) {
    term_table_set_gc_mark(table, i);
    if (i < ptr) {
      mark_reachable_terms(table, ptr, i);
    }
  }
}

// mark all terms in composite term d
static void mark_composite_term(term_table_t *table, int32_t ptr, composite_term_t *d) {
  uint32_t i, n;

  n = d->arity;
  for (i=0; i<n; i++) {
    mark_and_explore_term(table, ptr, d->arg[i]);
  }
}

// subterm of d
static inline void mark_select_term(term_table_t *table, int32_t ptr, select_term_t *d) {
  mark_and_explore_term(table, ptr, d->arg);
}

// root atoms
static inline void mark_root_atom(term_table_t *table, int32_t ptr, root_atom_t *r) {
  // x should be in p, so no need to explore
  mark_and_explore_term(table, ptr, r->p);
}

// variables in polynomials
static void mark_polynomial(term_table_t *table, int32_t ptr, polynomial_t *p) {
  monomial_t *q;

  q = p->mono;
  // skip constant monomial if any
  if (q->var == const_idx) q ++;

  while (q->var != max_idx) {
    mark_and_explore_term(table, ptr, q->var);
    q ++;
  }
}

static void mark_bvpoly(term_table_t *table, int32_t ptr, bvpoly_t *p) {
  bvmono_t *q;

  q = p->mono;
  // skip constant monomial if any
  if (q->var == const_idx) q ++;

  while (q->var != max_idx) {
    mark_and_explore_term(table, ptr, q->var);
    q ++;
  }
}

static void mark_bvpoly64(term_table_t *table, int32_t ptr, bvpoly64_t *p) {
  bvmono64_t *q;

  q = p->mono;
  // skip constant monomial if any
  if (q->var == const_idx) q ++;

  while (q->var != max_idx) {
    mark_and_explore_term(table, ptr, q->var);
    q ++;
  }
}


// power product r: we mark it in table->pprods, then we explore all variables of r
static void mark_power_product(term_table_t *table, int32_t ptr, pprod_t *r) {
  uint32_t i, n;

  assert(r != empty_pp && r != end_pp && !pp_is_var(r));
  pprod_table_set_gc_mark(table->pprods, r);

  n = r->len;
  for (i=0; i<n; i++) {
    mark_and_explore_term(table, ptr, r->prod[i].var);
  }
}


static void mark_reachable_terms(term_table_t *table, int32_t ptr, int32_t i) {
  assert(term_idx_is_marked(table, i));

  switch (table->kind[i]) {
  case UNUSED_TERM:
  case RESERVED_TERM:
  case CONSTANT_TERM:
  case ARITH_CONSTANT:
  case BV64_CONSTANT:
  case BV_CONSTANT:
  case VARIABLE:
  case UNINTERPRETED_TERM:
    // leaf terms
    break;

  case ARITH_EQ_ATOM:
  case ARITH_GE_ATOM:
  case ARITH_IS_INT_ATOM:
  case ARITH_FLOOR:
  case ARITH_CEIL:
  case ARITH_ABS:
    // i has a single subterm stored in desc[i].integer
    mark_and_explore_term(table, ptr, table->desc[i].integer);
    break;

  case ARITH_ROOT_ATOM:
    // i is a root atom
    mark_root_atom(table, ptr, table->desc[i].ptr);
    break;

  case ITE_TERM:
  case APP_TERM:
  case UPDATE_TERM:
  case TUPLE_TERM:
  case EQ_TERM:
  case DISTINCT_TERM:
  case FORALL_TERM:
  case LAMBDA_TERM:
  case OR_TERM:
  case XOR_TERM:
  case ARITH_BINEQ_ATOM:
  case ARITH_RDIV:
  case ARITH_IDIV:
  case ARITH_MOD:
  case ARITH_DIVIDES_ATOM:
  case BV_ARRAY:
  case BV_DIV:
  case BV_REM:
  case BV_SDIV:
  case BV_SREM:
  case BV_SMOD:
  case BV_SHL:
  case BV_LSHR:
  case BV_ASHR:
  case BV_EQ_ATOM:
  case BV_GE_ATOM:
  case BV_SGE_ATOM:
    // i's descriptor is a composite term
    mark_composite_term(table, ptr, table->desc[i].ptr);
    break;

  case ITE_SPECIAL:
    // TODO: do we need a callback here for scanning the extra component?
    mark_composite_term(table, ptr, table->desc[i].ptr);
    break;

  case SELECT_TERM:
  case BIT_TERM:
    // i's descriptor is a select term
    mark_select_term(table, ptr, &table->desc[i].select);
    break;

  case POWER_PRODUCT:
    mark_power_product(table, ptr, table->desc[i].ptr);
    break;

  case ARITH_POLY:
    mark_polynomial(table, ptr, table->desc[i].ptr);
    break;

  case BV64_POLY:
    mark_bvpoly64(table, ptr, table->desc[i].ptr);
    break;

  case BV_POLY:
    mark_bvpoly(table, ptr, table->desc[i].ptr);
    break;

  default:
    assert(false);
    break;
  }

}


/*
 * Mark all live terms:
 * - on entry: the root terms must be marked
 * - on exit:
 *   every term reachable from a root term is marked
 *   every power product that's live is marked in table->ptbl.
 *   every type that's attached to a live term is marked in table->types
 */
static void mark_live_terms(term_table_t *table) {
  type_table_t *types;
  uint32_t i, n;

  n = table->nelems;
  for (i=0; i<n; i++) {
    if (term_idx_is_marked(table, i)) {
      mark_reachable_terms(table, i, i);
    }
  }

  // propagate the marks to live types
  // skip the reserved term
  types = table->types;
  for (i=1; i<n; i++) {
    if (term_idx_is_marked(table, i) ) {
      type_table_set_gc_mark(types, table->type[i]);
    }
  }
}


/*
 * Iterator to mark the terms accessible from the symbol table
 * - aux must be a pointer to the term table
 * - r is a record in the symbol table: r->value is a term to mark
 */
static void mark_symbol(void *aux, const stbl_rec_t *r) {
  term_table_set_gc_mark(aux, index_of(r->value));
}


/*
 * Filter to remove references to dead terms from the symbol table
 * - aux must be a pointer to the term table
 * - r is a record in the symbol table: if the function returns true,
 *   then r is finalized then removed from the symbol table.
 */
static bool dead_term_symbol(void *aux, const stbl_rec_t *r) {
  return !term_idx_is_marked(aux, index_of(r->value));
}


/*
 * Garbage collector
 * - the roots are all the marked terms + if keep_named is true,
 *   all the terms accessible from the symbol table (i.e., mapped to some name).
 * - every term, type, and power product reachable from these roots
 *   is preserved
 * - delete everything else
 * - clear all the marks
 */
void term_table_gc(term_table_t *table, bool keep_named) {
  uint32_t i, n;

  // mark the terms present in the symbol table
  if (keep_named) {
    stbl_iterate(&table->stbl, table, mark_symbol);
  }

  // mark the primitive terms
  set_bit(table->mark, const_idx);
  set_bit(table->mark, bool_const);
  set_bit(table->mark, zero_const);

  // propagate the marks
  mark_live_terms(table);

  // remove the unmarked terms from the symbol table
  if (!keep_named) {
    stbl_remove_records(&table->stbl, table, dead_term_symbol);
  }

  // force garbage collection in the type and power-product tables
  type_table_gc(table->types, keep_named);
  pprod_table_gc(table->pprods);

  // delete the unmarked terms
  n = table->nelems;
  for (i=0; i<n; i++) {
    if (! term_idx_is_marked(table, i) && table->kind[i] != UNUSED_TERM) {
      delete_term(table, i);
    }
  }

  // clear the marks
  clear_bitvector(table->mark, table->size);
}