25368527405

Committed 05 May 2026 09:28AM UTC coverage: 66.87% (+0.2%) from 66.687%

Build # 25368527405

Build Type

Pull #611

github

Committed by

disteph

Commit Message

Merge branch 'master' into mcsat-supplement-cdclt

Conflicts resolved with a hybrid of both sides:

- tests/regress/run_test.sh: keep this branch's explicit --dpllt for
  the non-mcsat side of /both/ tests (symmetric with --mcsat), because
  yices' default solver path is heuristically chosen and is not
  guaranteed to be DPLL(T) for every logic. Also adopt master's new
  per-mode .mcsat.gold / .dpllt.gold override mechanism so tests that
  intentionally differ between the two solvers can supply separate
  gold files.

- tests/regress/both/README.md: document the symmetric --mcsat /
  --dpllt pair and the per-mode gold-override convention in one place.

Pull Request Pull Request #611: Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

Coverage Stats

690 of 1006 new or added lines in 15 files covered. (68.59%)

2 existing lines in 2 files now uncovered.

84342 of 126128 relevant lines covered (66.87%)

1634859.8 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

63.78

/src/terms/term_explorer.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/>.
 */

#include <assert.h>

#include "terms/bv64_constants.h"
#include "terms/term_explorer.h"


/*
 * Tables indexed by term_kind (defined in terms.h)
 */
static const uint8_t atomic_term_flag[NUM_TERM_KINDS] = {
  false, // UNUSED_TERM
  false, // RESERVED_TERM
  true,  // CONSTANT_TERM
  true,  // ARITH_CONSTANT
  true,  // ARITH_FF_CONSTANT
  true,  // BV64_CONSTANT
  true,  // BV_CONSTANT
  true,  // VARIABLE
  true,  // UNINTERPRETED_TERM
  false, // ARITH_EQ_ATOM
  false, // ARITH_GE_ATOM
  false, // ARITH_IS_INT_ATOM
  false, // ARITH_FLOOR
  false, // ARITH_CEIL
  false, // ARITH_ABS
  false, // ARITH_ROOT_ATOM
  false, // ARITH_FF_EQ_ATOM
  false, // ITE_TERM
  false, // ITE_SPECIAL
  false, // APP_TERM
  false, // UPDATE_TERM
  false, // TUPLE_TERM
  false, // EQ_TERM
  false, // DISTINCT_TERM
  false, // FORALL_TERM
  false, // LAMBDA_TERM
  false, // OR_TERM
  false, // XOR_TERM
  false, // ARITH_BINEQ_ATOM
  false, // ARITH_RDIV
  false, // ARITH_IDIV
  false, // ARITH_MOD
  false, // ARITH_DIVIDES
  false, // ARITH_FF_BINEQ_ATOM
  false, // BV_ARRAY
  false, // BV_DIV
  false, // BV_REM
  false, // BV_SDIV
  false, // BV_SREM
  false, // BV_SMOD
  false, // BV_SHL
  false, // BV_LSHR
  false, // BV_ASHR
  false, // BV_EQ_ATOM
  false, // BV_GE_ATOM
  false, // BV_SGE_ATOM
  false, // SELECT_TERM
  false, // BIT_TERM
  false, // POWER_PRODUCT
  false, // ARITH_POLY
  false, // ARITH_FF_POLY
  false, // BV64_POLY
  false, // BV_POLY
};

static const uint8_t composite_term_flag[NUM_TERM_KINDS] = {
  false, // UNUSED_TERM
  false, // RESERVED_TERM
  false, // CONSTANT_TERM
  false, // ARITH_CONSTANT
  false, // ARITH_FF_CONSTANT
  false, // BV64_CONSTANT
  false, // BV_CONSTANT
  false, // VARIABLE
  false, // UNINTERPRETED_TERM
  true,  // ARITH_EQ_ATOM
  true,  // ARITH_GE_ATOM
  true,  // ARITH_IS_INT_ATOM
  true,  // ARITH_FLOOR
  true,  // ARITH_CEIL
  true,  // ARITH_ABS
  true,  // ARITH_ROOT_ATOM
  true,  // ARITH_FF_EQ_ATOM
  true,  // ITE_TERM
  true,  // ITE_SPECIAL
  true,  // APP_TERM
  true,  // UPDATE_TERM
  true,  // TUPLE_TERM
  true,  // EQ_TERM
  true,  // DISTINCT_TERM
  true,  // FORALL_TERM
  true,  // LAMBDA_TERM
  true,  // OR_TERM
  true,  // XOR_TERM
  true,  // ARITH_BINEQ_ATOM
  true,  // ARITH_RDIV
  true,  // ARITH_IDIV
  true,  // ARITH_MOD
  true,  // ARITH_DIVIDES
  true,  // ARITH_FF_BINEQ_ATOM
  true,  // BV_ARRAY
  true,  // BV_DIV
  true,  // BV_REM
  true,  // BV_SDIV
  true,  // BV_SREM
  true,  // BV_SMOD
  true,  // BV_SHL
  true,  // BV_LSHR
  true,  // BV_ASHR
  true,  // BV_EQ_ATOM
  true,  // BV_GE_ATOM
  true,  // BV_SGE_ATOM
  false, // SELECT_TERM
  false, // BIT_TERM
  false, // POWER_PRODUCT
  false, // ARITH_POLY
  false, // ARITH_FF_POLY
  false, // BV64_POLY
  false, // BV_POLY
};

// term_kind --> term_constructor
static const term_constructor_t constructor_term_table[NUM_TERM_KINDS] = {
  YICES_CONSTRUCTOR_ERROR,  // UNUSED_TERM
  YICES_CONSTRUCTOR_ERROR,  // RESERVED_TERM
  YICES_SCALAR_CONSTANT,    // CONSTANT_TERM
  YICES_ARITH_CONSTANT,     // ARITH_CONSTANT
  YICES_FF_CONSTANT,        // ARITH_FF_CONSTANT
  YICES_BV_CONSTANT,        // BV64_CONSTANT
  YICES_BV_CONSTANT,        // BV_CONSTANT
  YICES_VARIABLE,           // VARIABLE
  YICES_UNINTERPRETED_TERM, // UNINTERPRETED_TERM
  YICES_EQ_TERM,            // ARITH_EQ_ATOM
  YICES_ARITH_GE_ATOM,      // ARITH_GE_ATOM
  YICES_IS_INT_ATOM,        // ARITH_IS_INT_ATOM
  YICES_FLOOR,              // ARITH_FLOOR
  YICES_CEIL,               // ARITH_CEIL
  YICES_ABS,                // ARITH_ABS
  YICES_ARITH_ROOT_ATOM,    // ARITH_ROOT_ATOM
  YICES_EQ_TERM,            // ARITH_FF_EQ_ATOM
  YICES_ITE_TERM,           // ITE_TERM
  YICES_ITE_TERM,           // ITE_SPECIAL
  YICES_APP_TERM,           // APP_TERM
  YICES_UPDATE_TERM,        // UPDATE_TERM
  YICES_TUPLE_TERM,         // TUPLE_TERM
  YICES_EQ_TERM,            // EQ_TERM
  YICES_DISTINCT_TERM,      // DISTINCT_TERM
  YICES_FORALL_TERM,        // FORALL_TERM
  YICES_LAMBDA_TERM,        // LAMBDA_TERM
  YICES_OR_TERM,            // OR_TERM
  YICES_XOR_TERM,           // XOR_TERM
  YICES_EQ_TERM,            // ARITH_BINEQ_ATOM
  YICES_RDIV,               // ARITH_RDIV
  YICES_IDIV,               // ARITH_IDIV
  YICES_IMOD,               // ARITH_MOD
  YICES_DIVIDES_ATOM,       // ARITH_DIVIDES_ATOM
  YICES_EQ_TERM,            // ARITH_FF_BINEQ_ATOM
  YICES_BV_ARRAY,           // BV_ARRAY
  YICES_BV_DIV,             // BV_DIV
  YICES_BV_REM,             // BV_REM
  YICES_BV_SDIV,            // BV_SDIV
  YICES_BV_SREM,            // BV_SREM
  YICES_BV_SMOD,            // BV_SMOD
  YICES_BV_SHL,             // BV_SHL
  YICES_BV_LSHR,            // BV_LSHR
  YICES_BV_ASHR,            // BV_ASHR
  YICES_EQ_TERM,            // BV_EQ_ATOM
  YICES_BV_GE_ATOM,         // BV_GE_ATOM
  YICES_BV_SGE_ATOM,        // BV_SGE_ATOM
  YICES_SELECT_TERM,        // SELECT_TERM
  YICES_BIT_TERM,           // BIT_TERM
  YICES_POWER_PRODUCT,      // POWER_PRODUCT
  YICES_ARITH_SUM,          // ARITH_POLY
  YICES_FF_SUM,             // ARITH_FF_POLY
  YICES_BV_SUM,             // BV64_POLY
  YICES_BV_SUM,             // BV_POLY
};


/*
 * Check the class of term t
 * - t must be a valid term in table
 * 
 * Note: negative terms are composite, except false_term
 */
bool term_is_atomic(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  if (index_of(t) == bool_const) {
    assert(t == false_term || t == true_term);
    return true;
  }

  kind = term_kind(table, t);
  return is_pos_term(t) && atomic_term_flag[kind];
}

bool term_is_composite(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  if (index_of(t) == bool_const) {
    assert(t == false_term || t == true_term);
    return false;
  }

  kind = term_kind(table, t);
  return is_neg_term(t) || composite_term_flag[kind];
}

bool term_is_projection(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  kind = term_kind(table, t);
  return is_pos_term(t) && (kind == SELECT_TERM || kind == BIT_TERM);
}

bool term_is_sum(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  kind = term_kind(table, t);
  return is_pos_term(t) && kind == ARITH_POLY;
}

bool term_is_bvsum(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  kind = term_kind(table, t);
  return is_pos_term(t) && (kind == BV_POLY || kind == BV64_POLY);
}

bool term_is_product(term_table_t *table, term_t t) {
  term_kind_t kind;

  assert(good_term(table, t));

  kind = term_kind(table, t);
  return is_pos_term(t) && kind == POWER_PRODUCT;
}


/*
 * Constructor code for term t
 * - t must be valid in table
 * - the constructor codes are defined in yices_types.h
 */
term_constructor_t term_constructor(term_table_t *table, term_t t) {
  term_kind_t kind;
  term_constructor_t result;

  assert(good_term(table, t));

  if (index_of(t) == bool_const) {
    assert(t == false_term || t == true_term);
    result = YICES_BOOL_CONSTANT;
  } else if (is_neg_term(t)) {
    result = YICES_NOT_TERM;
  } else {
    kind = term_kind(table, t);
    result = constructor_term_table[kind];
  }

  return result;
}


/*
 * Number of children of t (this is no more than YICES_MAX_ARITY)
 * - for a sum, this returns the number of summands
 * - for a product, this returns the number of factors
 */
uint32_t term_num_children(term_table_t *table, term_t t) {
  uint32_t result;

  assert(good_term(table, t));

  result = 0; // prevents bogus GCC warning

  if (index_of(t) == bool_const) {
    assert(t == false_term || t == true_term);
    result = 0;
  } else if (is_neg_term(t)) {
    result = 1;
  } else {

    switch (term_kind(table, t)) {
    case UNUSED_TERM:   // should not happen
    case RESERVED_TERM: // should not happen either
      assert(false);    // fall through to prevent compile-time warning
    case CONSTANT_TERM:
    case ARITH_CONSTANT:
    case ARITH_FF_CONSTANT:
    case BV64_CONSTANT:
    case BV_CONSTANT:
    case VARIABLE:
    case UNINTERPRETED_TERM:
      result = 0;
      break;

    case ARITH_EQ_ATOM:
    case ARITH_FF_EQ_ATOM:
    case ARITH_GE_ATOM:
      // internally, these are terms of the form t==0 or t >= 0
      // to be uniform, we report them as binary operators
      result = 2;
      break;

    case ARITH_ROOT_ATOM:
      // internally, these are terms of the form x r p for root index k
      // to be uniform, we report them as binary operators
      result = 2;
      break;

    case ARITH_IS_INT_ATOM:
    case ARITH_FLOOR:
    case ARITH_CEIL:
    case ARITH_ABS:
      result = 1;
      break;

    case ITE_TERM:
    case ITE_SPECIAL:
    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_FF_BINEQ_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:
      result = composite_term_arity(table, t);      
      break;

    case SELECT_TERM:
    case BIT_TERM:
      result = 1;
      break;

    case POWER_PRODUCT:
      result = pprod_term_desc(table, t)->len;
      break;

    case ARITH_POLY:
      result = poly_term_desc(table, t)->nterms;
      break;

    case ARITH_FF_POLY:
      result = finitefield_poly_term_desc(table, t)->nterms;
      break;

    case BV64_POLY:
      result = bvpoly64_term_desc(table, t)->nterms;
      break;

    case BV_POLY:
      result = bvpoly_term_desc(table, t)->nterms;
      break;
    }
  }

  return result;
}


/*
 * First and second child of a root atom
 *
 * Internally, a root atom is of the form  (x r root(k, p)) for root index k
 * - where both x and p are terms
 * - r is an binary comparison (i.e., ==, <, <=, >=, >, !=)
 * - k is an index
 *
 * We return x as first child and p as second child
 */
static term_t arith_root_atom_child(const root_atom_t *a, uint32_t i) {
  assert(a != NULL && i < 2);
  return (i == 0) ? a->x : a->p;
}

/*
 * i-th child of term t:
 * - t must be valid term in table
 * - t must be a composite term
 * - if n is term_num_children(table, t) then i must be in [0 ... n-1]
 */
term_t term_child(term_table_t *table, term_t t, uint32_t i) {
  term_t result;

  assert(term_is_composite(table, t) && i < term_num_children(table, t));

  if (is_neg_term(t)) {
    assert(i == 0);
    result = opposite_term(t); // (not t)
  } else {
    switch (term_kind(table, t)) {
    case ARITH_EQ_ATOM:
    case ARITH_GE_ATOM:
      assert(i < 2);
      if (i == 0) {
        result = arith_atom_arg(table, t);
      } else {
        result = zero_term; // second child is always zero
      }
      break;

    case ARITH_FF_EQ_ATOM:
      assert(i < 2);
      if (i == 0) {
        result = arith_ff_eq_arg(table, t);
      } else {
        result = ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t)));
      }
      break;

    case ARITH_IS_INT_ATOM:
    case ARITH_FLOOR:
    case ARITH_CEIL:
    case ARITH_ABS:
      assert(i == 0);
      result = unary_term_arg(table, t);
      break;

    case ARITH_ROOT_ATOM:
      // internally, these are terms of the form x r p for root index k
      // to be uniform, we report them as binary operators
      // x is the first child
      // p is the second child
      result = arith_root_atom_child(arith_root_atom_desc(table, t), i);
      break;

    default:
      result = composite_term_arg(table, t, i);
      break;
    }
  }

  return result;
}


/*
 * All children of t:
 * - t must be a valid term in table
 * - t must be a composite term
 *.- the children of t are added to vector v
 */
void get_term_children(term_table_t *table, term_t t, ivector_t *v) {
  root_atom_t *a;
  composite_term_t *c;
  uint32_t i, n;

  assert(term_is_composite(table, t));

  if (is_neg_term(t)) {
    ivector_push(v, opposite_term(t)); // not(t)
  } else {
    switch (term_kind(table, t)) {
    case ARITH_EQ_ATOM:
    case ARITH_GE_ATOM:
      // t == 0 or t >= 0
      // treat them like binary terms
      ivector_push(v, arith_atom_arg(table, t));
      ivector_push(v, zero_term);
      break;

    case ARITH_FF_EQ_ATOM:
      // t == 0 over finite fields: expose both sides uniformly
      ivector_push(v, arith_ff_eq_arg(table, t));
      ivector_push(v, ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t))));
      break;

    case ARITH_IS_INT_ATOM:
    case ARITH_FLOOR:
    case ARITH_CEIL:
    case ARITH_ABS:
      ivector_push(v, unary_term_arg(table, t));
      break;

    case ARITH_ROOT_ATOM:
      a = arith_root_atom_desc(table, t);
      ivector_push(v, a->x); // a->x == child 0
      ivector_push(v, a->p); // a->p == child 1
      break;

    default:
      c = composite_term_desc(table, t);
      n = c->arity;
      for (i=0; i<n; i++) {
        ivector_push(v, c->arg[i]);
      }
      break;
    }
  }
}



/*
 * Components of a projection
 * - t must be a valid term in table and it must be either a SELECT_TERM
 *   or a BIT_TERM
 */
int32_t proj_term_index(term_table_t *table, term_t t) {
  assert(term_is_projection(table, t));
  return select_for_idx(table, index_of(t))->idx;
}

term_t proj_term_arg(term_table_t *table, term_t t) {
  assert(term_is_projection(table, t));
  return select_for_idx(table, index_of(t))->arg;
}

/*
 * Components of an arithmetic sum
 * - t must be a valid ARITH_POLY term in table
 * - i must be an index in [0 ... n-1] where n = term_num_children(table, t)
 * - the component is a pair (coeff, child): coeff is copied into q
 * - q must be initialized
 */
void sum_term_component(term_table_t *table, term_t t, uint32_t i, mpq_t q, term_t *child) {
  polynomial_t *p;
  term_t v;

  assert(is_pos_term(t) && term_kind(table, t) == ARITH_POLY);
  p = poly_term_desc(table, t);
  assert(i < p->nterms);

  v = p->mono[i].var;
  if (v == const_idx) {
    v = NULL_TERM;
  }
  *child = v;
  q_get_mpq(&p->mono[i].coeff, q);
}


/*
 * Components of a bitvector sum
 * - t must be a valid BV_POLY or BV64_POLY term in table
 * - i must be an index in [0 ... n-1] where n = term_num_children(table, t)
 * - the component is a pair (coeff, child):
 *   coeff is a bitvector constant
 *   child is a bitvector term 
 * The coeff is returned in array a
 * - a must be large enough to store nbits integers, where nbits = number of bits in t
 *   a[0] = lower order bit of the constant
 *   a[nbits-1] = higher order bit
 */
void bvsum_term_component(term_table_t *table, term_t t, uint32_t i, int32_t a[], term_t *child) {
  bvpoly_t *p;
  bvpoly64_t *q;
  term_t v;

  assert(is_pos_term(t));

  switch (term_kind(table, t)) {
  case BV64_POLY:
    q = bvpoly64_term_desc(table, t);
    assert(i < q->nterms);
    v = q->mono[i].var;
    if (v == const_idx) {
      v = NULL_TERM;
    }
    *child = v;
    bvconst64_get_array(q->mono[i].coeff, a, q->bitsize);
    break;

  case BV_POLY:
    p = bvpoly_term_desc(table, t);
    assert(i < p->nterms);
    v = p->mono[i].var;
    if (v == const_idx) {
      v = NULL_TERM;
    }
    *child = v;
    bvconst_get_array(p->mono[i].coeff, a, p->bitsize);    
    break;

  default:
    assert(false);
    break;
  }
}


/*
 * Components of a power-product
 * - t must be a valid POWER_PRODUCT term in table
 * - i must be an index in [0 .. n-1] where n = term_num_children(table, t)
 * - the component is a pair (child, exponent)
 *   child is a term (arithmetic or bitvector term)
 *   exponent is a positive integer
 */
void product_term_component(term_table_t *table, term_t t, uint32_t i, term_t *child, uint32_t *exp) {
  pprod_t *p;

  assert(is_pos_term(t) && term_kind(table, t) == POWER_PRODUCT);
  p = pprod_term_desc(table, t);
  assert(i < p->len);
  *child = p->prod[i].var;
  *exp = p->prod[i].exp;
}






/*
 * Value of constant terms
 * - t must be a constant term of appropriate type
 * - generic_const_value(table, t) works for any constant 
 *   term t of scalar or uninterpreted type
 */
bool bool_const_value(term_table_t *table, term_t t) {
  assert(t == true_term || t == false_term);
  return is_pos_term(t);
}

void arith_const_value(term_table_t *table, term_t t, mpq_t q) {
  assert(is_pos_term(t));
  q_get_mpq(rational_term_desc(table, t), q);
}

void arith_ff_const_value(term_table_t *table, term_t t, mpz_t z) {
  assert(is_pos_term(t));
  q_get_mpz(finitefield_term_desc(table, t), z);
}

void bv_const_value(term_table_t *table, term_t t, int32_t a[]) {
  bvconst64_term_t *bv64;
  bvconst_term_t *bv;

  switch (term_kind(table, t)) {
  case BV64_CONSTANT:
    bv64 = bvconst64_term_desc(table, t);
    bvconst64_get_array(bv64->value, a, bv64->bitsize);
    break;

  case BV_CONSTANT:
    bv = bvconst_term_desc(table, t);
    bvconst_get_array(bv->data, a, bv->bitsize);
    break;

  default:
    assert(false);
    break;
  }
}

// constant of uninterpreted or scalar type (not Boolean)
int32_t generic_const_value(term_table_t *table, term_t t) {
  assert(is_pos_term(t) && t != true_term);
  return constant_term_index(table, t);
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	#include <assert.h>
20
21	#include "terms/bv64_constants.h"
22	#include "terms/term_explorer.h"
23
24
25	/*
26	* Tables indexed by term_kind (defined in terms.h)
27	*/
28	static const uint8_t atomic_term_flag[NUM_TERM_KINDS] = {
29	false, // UNUSED_TERM
30	false, // RESERVED_TERM
31	true, // CONSTANT_TERM
32	true, // ARITH_CONSTANT
33	true, // ARITH_FF_CONSTANT
34	true, // BV64_CONSTANT
35	true, // BV_CONSTANT
36	true, // VARIABLE
37	true, // UNINTERPRETED_TERM
38	false, // ARITH_EQ_ATOM
39	false, // ARITH_GE_ATOM
40	false, // ARITH_IS_INT_ATOM
41	false, // ARITH_FLOOR
42	false, // ARITH_CEIL
43	false, // ARITH_ABS
44	false, // ARITH_ROOT_ATOM
45	false, // ARITH_FF_EQ_ATOM
46	false, // ITE_TERM
47	false, // ITE_SPECIAL
48	false, // APP_TERM
49	false, // UPDATE_TERM
50	false, // TUPLE_TERM
51	false, // EQ_TERM
52	false, // DISTINCT_TERM
53	false, // FORALL_TERM
54	false, // LAMBDA_TERM
55	false, // OR_TERM
56	false, // XOR_TERM
57	false, // ARITH_BINEQ_ATOM
58	false, // ARITH_RDIV
59	false, // ARITH_IDIV
60	false, // ARITH_MOD
61	false, // ARITH_DIVIDES
62	false, // ARITH_FF_BINEQ_ATOM
63	false, // BV_ARRAY
64	false, // BV_DIV
65	false, // BV_REM
66	false, // BV_SDIV
67	false, // BV_SREM
68	false, // BV_SMOD
69	false, // BV_SHL
70	false, // BV_LSHR
71	false, // BV_ASHR
72	false, // BV_EQ_ATOM
73	false, // BV_GE_ATOM
74	false, // BV_SGE_ATOM
75	false, // SELECT_TERM
76	false, // BIT_TERM
77	false, // POWER_PRODUCT
78	false, // ARITH_POLY
79	false, // ARITH_FF_POLY
80	false, // BV64_POLY
81	false, // BV_POLY
82	};
83
84	static const uint8_t composite_term_flag[NUM_TERM_KINDS] = {
85	false, // UNUSED_TERM
86	false, // RESERVED_TERM
87	false, // CONSTANT_TERM
88	false, // ARITH_CONSTANT
89	false, // ARITH_FF_CONSTANT
90	false, // BV64_CONSTANT
91	false, // BV_CONSTANT
92	false, // VARIABLE
93	false, // UNINTERPRETED_TERM
94	true, // ARITH_EQ_ATOM
95	true, // ARITH_GE_ATOM
96	true, // ARITH_IS_INT_ATOM
97	true, // ARITH_FLOOR
98	true, // ARITH_CEIL
99	true, // ARITH_ABS
100	true, // ARITH_ROOT_ATOM
101	true, // ARITH_FF_EQ_ATOM
102	true, // ITE_TERM
103	true, // ITE_SPECIAL
104	true, // APP_TERM
105	true, // UPDATE_TERM
106	true, // TUPLE_TERM
107	true, // EQ_TERM
108	true, // DISTINCT_TERM
109	true, // FORALL_TERM
110	true, // LAMBDA_TERM
111	true, // OR_TERM
112	true, // XOR_TERM
113	true, // ARITH_BINEQ_ATOM
114	true, // ARITH_RDIV
115	true, // ARITH_IDIV
116	true, // ARITH_MOD
117	true, // ARITH_DIVIDES
118	true, // ARITH_FF_BINEQ_ATOM
119	true, // BV_ARRAY
120	true, // BV_DIV
121	true, // BV_REM
122	true, // BV_SDIV
123	true, // BV_SREM
124	true, // BV_SMOD
125	true, // BV_SHL
126	true, // BV_LSHR
127	true, // BV_ASHR
128	true, // BV_EQ_ATOM
129	true, // BV_GE_ATOM
130	true, // BV_SGE_ATOM
131	false, // SELECT_TERM
132	false, // BIT_TERM
133	false, // POWER_PRODUCT
134	false, // ARITH_POLY
135	false, // ARITH_FF_POLY
136	false, // BV64_POLY
137	false, // BV_POLY
138	};
139
140	// term_kind --> term_constructor
141	static const term_constructor_t constructor_term_table[NUM_TERM_KINDS] = {
142	YICES_CONSTRUCTOR_ERROR, // UNUSED_TERM
143	YICES_CONSTRUCTOR_ERROR, // RESERVED_TERM
144	YICES_SCALAR_CONSTANT, // CONSTANT_TERM
145	YICES_ARITH_CONSTANT, // ARITH_CONSTANT
146	YICES_FF_CONSTANT, // ARITH_FF_CONSTANT
147	YICES_BV_CONSTANT, // BV64_CONSTANT
148	YICES_BV_CONSTANT, // BV_CONSTANT
149	YICES_VARIABLE, // VARIABLE
150	YICES_UNINTERPRETED_TERM, // UNINTERPRETED_TERM
151	YICES_EQ_TERM, // ARITH_EQ_ATOM
152	YICES_ARITH_GE_ATOM, // ARITH_GE_ATOM
153	YICES_IS_INT_ATOM, // ARITH_IS_INT_ATOM
154	YICES_FLOOR, // ARITH_FLOOR
155	YICES_CEIL, // ARITH_CEIL
156	YICES_ABS, // ARITH_ABS
157	YICES_ARITH_ROOT_ATOM, // ARITH_ROOT_ATOM
158	YICES_EQ_TERM, // ARITH_FF_EQ_ATOM
159	YICES_ITE_TERM, // ITE_TERM
160	YICES_ITE_TERM, // ITE_SPECIAL
161	YICES_APP_TERM, // APP_TERM
162	YICES_UPDATE_TERM, // UPDATE_TERM
163	YICES_TUPLE_TERM, // TUPLE_TERM
164	YICES_EQ_TERM, // EQ_TERM
165	YICES_DISTINCT_TERM, // DISTINCT_TERM
166	YICES_FORALL_TERM, // FORALL_TERM
167	YICES_LAMBDA_TERM, // LAMBDA_TERM
168	YICES_OR_TERM, // OR_TERM
169	YICES_XOR_TERM, // XOR_TERM
170	YICES_EQ_TERM, // ARITH_BINEQ_ATOM
171	YICES_RDIV, // ARITH_RDIV
172	YICES_IDIV, // ARITH_IDIV
173	YICES_IMOD, // ARITH_MOD
174	YICES_DIVIDES_ATOM, // ARITH_DIVIDES_ATOM
175	YICES_EQ_TERM, // ARITH_FF_BINEQ_ATOM
176	YICES_BV_ARRAY, // BV_ARRAY
177	YICES_BV_DIV, // BV_DIV
178	YICES_BV_REM, // BV_REM
179	YICES_BV_SDIV, // BV_SDIV
180	YICES_BV_SREM, // BV_SREM
181	YICES_BV_SMOD, // BV_SMOD
182	YICES_BV_SHL, // BV_SHL
183	YICES_BV_LSHR, // BV_LSHR
184	YICES_BV_ASHR, // BV_ASHR
185	YICES_EQ_TERM, // BV_EQ_ATOM
186	YICES_BV_GE_ATOM, // BV_GE_ATOM
187	YICES_BV_SGE_ATOM, // BV_SGE_ATOM
188	YICES_SELECT_TERM, // SELECT_TERM
189	YICES_BIT_TERM, // BIT_TERM
190	YICES_POWER_PRODUCT, // POWER_PRODUCT
191	YICES_ARITH_SUM, // ARITH_POLY
192	YICES_FF_SUM, // ARITH_FF_POLY
193	YICES_BV_SUM, // BV64_POLY
194	YICES_BV_SUM, // BV_POLY
195	};
196
197
198	/*
199	* Check the class of term t
200	* - t must be a valid term in table
201	*
202	* Note: negative terms are composite, except false_term
203	*/
204	bool term_is_atomic(term_table_t *table, term_t t) {	79,068✔
205	term_kind_t kind;
206
207	assert(good_term(table, t));
208
209	if (index_of(t) == bool_const) {	79,068✔
210	assert(t == false_term \|\| t == true_term);
211	return true;	×
212	}
213
214	kind = term_kind(table, t);	79,068✔
215	return is_pos_term(t) && atomic_term_flag[kind];	79,068✔
216	}
217
218	bool term_is_composite(term_table_t *table, term_t t) {	502,996✔
219	term_kind_t kind;
220
221	assert(good_term(table, t));
222
223	if (index_of(t) == bool_const) {	502,996✔
224	assert(t == false_term \|\| t == true_term);
225	return false;	9,274✔
226	}
227
228	kind = term_kind(table, t);	493,722✔
229	return is_neg_term(t) \|\| composite_term_flag[kind];	493,722✔
230	}
231
232	bool term_is_projection(term_table_t *table, term_t t) {	826,149✔
233	term_kind_t kind;
234
235	assert(good_term(table, t));
236
237	kind = term_kind(table, t);	826,149✔
238	return is_pos_term(t) && (kind == SELECT_TERM \|\| kind == BIT_TERM);	826,149✔
239	}
240
241	bool term_is_sum(term_table_t *table, term_t t) {	473,542✔
242	term_kind_t kind;
243
244	assert(good_term(table, t));
245
246	kind = term_kind(table, t);	473,542✔
247	return is_pos_term(t) && kind == ARITH_POLY;	473,542✔
248	}
249
250	bool term_is_bvsum(term_table_t *table, term_t t) {	468,951✔
251	term_kind_t kind;
252
253	assert(good_term(table, t));
254
255	kind = term_kind(table, t);	468,951✔
256	return is_pos_term(t) && (kind == BV_POLY \|\| kind == BV64_POLY);	468,951✔
257	}
258
259	bool term_is_product(term_table_t *table, term_t t) {	463,119✔
260	term_kind_t kind;
261
262	assert(good_term(table, t));
263
264	kind = term_kind(table, t);	463,119✔
265	return is_pos_term(t) && kind == POWER_PRODUCT;	463,119✔
266	}
267
268
269	/*
270	* Constructor code for term t
271	* - t must be valid in table
272	* - the constructor codes are defined in yices_types.h
273	*/
274	term_constructor_t term_constructor(term_table_t *table, term_t t) {	2,180✔
275	term_kind_t kind;
276	term_constructor_t result;
277
278	assert(good_term(table, t));
279
280	if (index_of(t) == bool_const) {	2,180✔
281	assert(t == false_term \|\| t == true_term);
282	result = YICES_BOOL_CONSTANT;	20✔
283	} else if (is_neg_term(t)) {	2,160✔
284	result = YICES_NOT_TERM;	×
285	} else {
286	kind = term_kind(table, t);	2,160✔
287	result = constructor_term_table[kind];	2,160✔
288	}
289
290	return result;	2,180✔
291	}
292
293
294	/*
295	* Number of children of t (this is no more than YICES_MAX_ARITY)
296	* - for a sum, this returns the number of summands
297	* - for a product, this returns the number of factors
298	*/
299	uint32_t term_num_children(term_table_t *table, term_t t) {	353,886✔
300	uint32_t result;
301
302	assert(good_term(table, t));
303
304	result = 0; // prevents bogus GCC warning	353,886✔
305
306	if (index_of(t) == bool_const) {	353,886✔
307	assert(t == false_term \|\| t == true_term);
308	result = 0;	62✔
309	} else if (is_neg_term(t)) {	353,824✔
310	result = 1;	15,699✔
311	} else {
312
313	switch (term_kind(table, t)) {	338,125✔
314	case UNUSED_TERM: // should not happen	4,892✔
315	case RESERVED_TERM: // should not happen either
316	assert(false); // fall through to prevent compile-time warning
317	case CONSTANT_TERM:
318	case ARITH_CONSTANT:
319	case ARITH_FF_CONSTANT:
320	case BV64_CONSTANT:
321	case BV_CONSTANT:
322	case VARIABLE:
323	case UNINTERPRETED_TERM:
324	result = 0;	4,892✔
325	break;	4,892✔
326
327	case ARITH_EQ_ATOM:	8,394✔
328	case ARITH_FF_EQ_ATOM:
329	case ARITH_GE_ATOM:
330	// internally, these are terms of the form t==0 or t >= 0
331	// to be uniform, we report them as binary operators
332	result = 2;	8,394✔
333	break;	8,394✔
334
335	case ARITH_ROOT_ATOM:	×
336	// internally, these are terms of the form x r p for root index k
337	// to be uniform, we report them as binary operators
338	result = 2;	×
339	break;	×
340
341	case ARITH_IS_INT_ATOM:	2✔
342	case ARITH_FLOOR:
343	case ARITH_CEIL:
344	case ARITH_ABS:
345	result = 1;	2✔
346	break;	2✔
347
348	case ITE_TERM:	314,341✔
349	case ITE_SPECIAL:
350	case APP_TERM:
351	case UPDATE_TERM:
352	case TUPLE_TERM:
353	case EQ_TERM:
354	case DISTINCT_TERM:
355	case FORALL_TERM:
356	case LAMBDA_TERM:
357	case OR_TERM:
358	case XOR_TERM:
359	case ARITH_BINEQ_ATOM:
360	case ARITH_RDIV:
361	case ARITH_IDIV:
362	case ARITH_MOD:
363	case ARITH_DIVIDES_ATOM:
364	case ARITH_FF_BINEQ_ATOM:
365	case BV_ARRAY:
366	case BV_DIV:
367	case BV_REM:
368	case BV_SDIV:
369	case BV_SREM:
370	case BV_SMOD:
371	case BV_SHL:
372	case BV_LSHR:
373	case BV_ASHR:
374	case BV_EQ_ATOM:
375	case BV_GE_ATOM:
376	case BV_SGE_ATOM:
377	result = composite_term_arity(table, t);	314,341✔
378	break;	314,341✔
379
380	case SELECT_TERM:	×
381	case BIT_TERM:
382	result = 1;	×
383	break;	×
384
385	case POWER_PRODUCT:	66✔
386	result = pprod_term_desc(table, t)->len;	66✔
387	break;	66✔
388
389	case ARITH_POLY:	4,591✔
390	result = poly_term_desc(table, t)->nterms;	4,591✔
391	break;	4,591✔
392
393	case ARITH_FF_POLY:	7✔
394	result = finitefield_poly_term_desc(table, t)->nterms;	7✔
395	break;	7✔
396
397	case BV64_POLY:	5,658✔
398	result = bvpoly64_term_desc(table, t)->nterms;	5,658✔
399	break;	5,658✔
400
401	case BV_POLY:	174✔
402	result = bvpoly_term_desc(table, t)->nterms;	174✔
403	break;	174✔
404	}
405	}
406
407	return result;	353,886✔
408	}
409
410
411	/*
412	* First and second child of a root atom
413	*
414	* Internally, a root atom is of the form (x r root(k, p)) for root index k
415	* - where both x and p are terms
416	* - r is an binary comparison (i.e., ==, <, <=, >=, >, !=)
417	* - k is an index
418	*
419	* We return x as first child and p as second child
420	*/
421	static term_t arith_root_atom_child(const root_atom_t *a, uint32_t i) {	×
422	assert(a != NULL && i < 2);
423	return (i == 0) ? a->x : a->p;	×
424	}
425
426	/*
427	* i-th child of term t:
428	* - t must be valid term in table
429	* - t must be a composite term
430	* - if n is term_num_children(table, t) then i must be in [0 ... n-1]
431	*/
432	term_t term_child(term_table_t *table, term_t t, uint32_t i) {	1,495,566✔
433	term_t result;
434
435	assert(term_is_composite(table, t) && i < term_num_children(table, t));
436
437	if (is_neg_term(t)) {	1,495,566✔
438	assert(i == 0);
439	result = opposite_term(t); // (not t)	30✔
440	} else {
441	switch (term_kind(table, t)) {	1,495,536✔
442	case ARITH_EQ_ATOM:	13,743✔
443	case ARITH_GE_ATOM:
444	assert(i < 2);
445	if (i == 0) {	13,743✔
446	result = arith_atom_arg(table, t);	6,874✔
447	} else {
448	result = zero_term; // second child is always zero	6,869✔
449	}
450	break;	13,743✔
451
NEW 452	case ARITH_FF_EQ_ATOM:	×
453	assert(i < 2);
NEW 454	if (i == 0) {	×
NEW 455	result = arith_ff_eq_arg(table, t);	×
456	} else {
NEW 457	result = ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t)));	×
458	}
NEW 459	break;	×
460
461	case ARITH_IS_INT_ATOM:	1✔
462	case ARITH_FLOOR:
463	case ARITH_CEIL:
464	case ARITH_ABS:
465	assert(i == 0);
466	result = unary_term_arg(table, t);	1✔
467	break;	1✔
468
469	case ARITH_ROOT_ATOM:	×
470	// internally, these are terms of the form x r p for root index k
471	// to be uniform, we report them as binary operators
472	// x is the first child
473	// p is the second child
474	result = arith_root_atom_child(arith_root_atom_desc(table, t), i);	×
475	break;	×
476
477	default:	1,481,792✔
478	result = composite_term_arg(table, t, i);	1,481,792✔
479	break;	1,481,792✔
480	}
481	}
482
483	return result;	1,495,566✔
484	}
485
486
487	/*
488	* All children of t:
489	* - t must be a valid term in table
490	* - t must be a composite term
491	*.- the children of t are added to vector v
492	*/
493	void get_term_children(term_table_t table, term_t t, ivector_t v) {	×
494	root_atom_t *a;
495	composite_term_t *c;
496	uint32_t i, n;
497
498	assert(term_is_composite(table, t));
499
500	if (is_neg_term(t)) {	×
501	ivector_push(v, opposite_term(t)); // not(t)	×
502	} else {
503	switch (term_kind(table, t)) {	×
504	case ARITH_EQ_ATOM:	×
505	case ARITH_GE_ATOM:
506	// t == 0 or t >= 0
507	// treat them like binary terms
508	ivector_push(v, arith_atom_arg(table, t));	×
509	ivector_push(v, zero_term);	×
510	break;	×
511
NEW 512	case ARITH_FF_EQ_ATOM:	×
513	// t == 0 over finite fields: expose both sides uniformly
NEW 514	ivector_push(v, arith_ff_eq_arg(table, t));	×
NEW 515	ivector_push(v, ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t))));	×
NEW 516	break;	×
517
UNCOV 518	case ARITH_IS_INT_ATOM:	×
519	case ARITH_FLOOR:
520	case ARITH_CEIL:
521	case ARITH_ABS:
522	ivector_push(v, unary_term_arg(table, t));	×
523	break;	×
524
525	case ARITH_ROOT_ATOM:	×
526	a = arith_root_atom_desc(table, t);	×
527	ivector_push(v, a->x); // a->x == child 0	×
528	ivector_push(v, a->p); // a->p == child 1	×
529	break;	×
530
531	default:	×
532	c = composite_term_desc(table, t);	×
533	n = c->arity;	×
534	for (i=0; i<n; i++) {	×
535	ivector_push(v, c->arg[i]);	×
536	}
537	break;	×
538	}
539	}
540	}	×
541
542
543
544	/*
545	* Components of a projection
546	* - t must be a valid term in table and it must be either a SELECT_TERM
547	* or a BIT_TERM
548	*/
549	int32_t proj_term_index(term_table_t *table, term_t t) {	×
550	assert(term_is_projection(table, t));
551	return select_for_idx(table, index_of(t))->idx;	×
552	}
553
554	term_t proj_term_arg(term_table_t *table, term_t t) {	352,607✔
555	assert(term_is_projection(table, t));
556	return select_for_idx(table, index_of(t))->arg;	352,607✔
557	}
558
559	/*
560	* Components of an arithmetic sum
561	* - t must be a valid ARITH_POLY term in table
562	* - i must be an index in [0 ... n-1] where n = term_num_children(table, t)
563	* - the component is a pair (coeff, child): coeff is copied into q
564	* - q must be initialized
565	*/
566	void sum_term_component(term_table_t table, term_t t, uint32_t i, mpq_t q, term_t child) {	11,947✔
567	polynomial_t *p;
568	term_t v;
569
570	assert(is_pos_term(t) && term_kind(table, t) == ARITH_POLY);
571	p = poly_term_desc(table, t);	11,947✔
572	assert(i < p->nterms);
573
574	v = p->mono[i].var;	11,947✔
575	if (v == const_idx) {	11,947✔
576	v = NULL_TERM;	2,267✔
577	}
578	*child = v;	11,947✔
579	q_get_mpq(&p->mono[i].coeff, q);	11,947✔
580	}	11,947✔
581
582
583	/*
584	* Components of a bitvector sum
585	* - t must be a valid BV_POLY or BV64_POLY term in table
586	* - i must be an index in [0 ... n-1] where n = term_num_children(table, t)
587	* - the component is a pair (coeff, child):
588	* coeff is a bitvector constant
589	* child is a bitvector term
590	* The coeff is returned in array a
591	* - a must be large enough to store nbits integers, where nbits = number of bits in t
592	* a[0] = lower order bit of the constant
593	* a[nbits-1] = higher order bit
594	*/
595	void bvsum_term_component(term_table_t table, term_t t, uint32_t i, int32_t a[], term_t child) {	7,562✔
596	bvpoly_t *p;
597	bvpoly64_t *q;
598	term_t v;
599
600	assert(is_pos_term(t));
601
602	switch (term_kind(table, t)) {	7,562✔
603	case BV64_POLY:	7,214✔
604	q = bvpoly64_term_desc(table, t);	7,214✔
605	assert(i < q->nterms);
606	v = q->mono[i].var;	7,214✔
607	if (v == const_idx) {	7,214✔
608	v = NULL_TERM;	1,178✔
609	}
610	*child = v;	7,214✔
611	bvconst64_get_array(q->mono[i].coeff, a, q->bitsize);	7,214✔
612	break;	7,214✔
613
614	case BV_POLY:	348✔
615	p = bvpoly_term_desc(table, t);	348✔
616	assert(i < p->nterms);
617	v = p->mono[i].var;	348✔
618	if (v == const_idx) {	348✔
619	v = NULL_TERM;	134✔
620	}
621	*child = v;	348✔
622	bvconst_get_array(p->mono[i].coeff, a, p->bitsize);	348✔
623	break;	348✔
624
625	default:	×
626	assert(false);
627	break;	×
628	}
629	}	7,562✔
630
631
632	/*
633	* Components of a power-product
634	* - t must be a valid POWER_PRODUCT term in table
635	* - i must be an index in [0 .. n-1] where n = term_num_children(table, t)
636	* - the component is a pair (child, exponent)
637	* child is a term (arithmetic or bitvector term)
638	* exponent is a positive integer
639	*/
640	void product_term_component(term_table_t table, term_t t, uint32_t i, term_t child, uint32_t *exp) {	130✔
641	pprod_t *p;
642
643	assert(is_pos_term(t) && term_kind(table, t) == POWER_PRODUCT);
644	p = pprod_term_desc(table, t);	130✔
645	assert(i < p->len);
646	*child = p->prod[i].var;	130✔
647	*exp = p->prod[i].exp;	130✔
648	}	130✔
649
650
651
652
653
654
655	/*
656	* Value of constant terms
657	* - t must be a constant term of appropriate type
658	* - generic_const_value(table, t) works for any constant
659	* term t of scalar or uninterpreted type
660	*/
661	bool bool_const_value(term_table_t *table, term_t t) {	×
662	assert(t == true_term \|\| t == false_term);
663	return is_pos_term(t);	×
664	}
665
666	void arith_const_value(term_table_t *table, term_t t, mpq_t q) {	×
667	assert(is_pos_term(t));
668	q_get_mpq(rational_term_desc(table, t), q);	×
669	}	×
670
671	void arith_ff_const_value(term_table_t *table, term_t t, mpz_t z) {	2✔
672	assert(is_pos_term(t));
673	q_get_mpz(finitefield_term_desc(table, t), z);	2✔
674	}	2✔
675
676	void bv_const_value(term_table_t *table, term_t t, int32_t a[]) {	×
677	bvconst64_term_t *bv64;
678	bvconst_term_t *bv;
679
680	switch (term_kind(table, t)) {	×
681	case BV64_CONSTANT:	×
682	bv64 = bvconst64_term_desc(table, t);	×
683	bvconst64_get_array(bv64->value, a, bv64->bitsize);	×
684	break;	×
685
686	case BV_CONSTANT:	×
687	bv = bvconst_term_desc(table, t);	×
688	bvconst_get_array(bv->data, a, bv->bitsize);	×
689	break;	×
690
691	default:	×
692	assert(false);
693	break;	×
694	}
695	}	×
696
697	// constant of uninterpreted or scalar type (not Boolean)
698	int32_t generic_const_value(term_table_t *table, term_t t) {	4✔
699	assert(is_pos_term(t) && t != true_term);
700	return constant_term_index(table, t);	4✔
701	}

SRI-CSL / yices2 / 25368527405

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous