22552082017

Committed 01 Mar 2026 08:35PM UTC coverage: 65.387% (+0.07%) from 65.317%

Build # 22552082017

Build Type

push

github

Committed by

web-flow

Commit Message

Mcsat unsat core (#578)

* mcsat unsat core

* update test

* test

* boolean labels

* another test

* update doc

* fix mcsat unsat core issue + tests

* fix

* minor

* Refactor MCSAT assumptions-core support into context layer

* Fix MCSAT check-sat-assuming regressions and assumption cleanup

* Add no-mcsat stub for assumption cleanup

---------

Co-authored-by: Stéphane Graham-Lengrand <stephane.graham-lengrand@csl.sri.com>
Co-authored-by: Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>

Run Details

155 of 202 new or added lines in 5 files covered. (76.73%)

40 existing lines in 2 files now uncovered.

81484 of 124618 relevant lines covered (65.39%)

1708166.98 hits per line

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

71.13

/src/context/context_solver.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/>.
 */

/*
 * SEARCH AND SOLVING PROCEDURES
 *
 * This module implements the check_context function (and variants).
 * It also implements model construction.
 */

#include <stdbool.h>
#include <assert.h>
#include <stdint.h>
#include <inttypes.h>
#include <stdio.h>

#include "context/context.h"
#include "context/internalization_codes.h"
#include "model/models.h"
#include "mcsat/solver.h"
#include "solvers/bv/dimacs_printer.h"
#include "solvers/cdcl/delegate.h"
#include "solvers/funs/fun_solver.h"
#include "solvers/simplex/simplex.h"
#include "terms/term_explorer.h"
#include "terms/term_manager.h"
#include "terms/term_substitution.h"
#include "utils/int_hash_map.h"
#include "utils/int_hash_sets.h"

#include "api/yices_globals.h"
#include "mt/thread_macros.h"



/*
 * TRACE FUNCTIONS
 */

/*
 * Basic statistics
 */
static void trace_stats(smt_core_t *core, const char *when, uint32_t level) {
  trace_printf(core->trace, level,
               "(%-10s %8"PRIu64" %10"PRIu64" %8"PRIu64" %8"PRIu32" %8"PRIu32" %8"PRIu64" %8"PRIu32" %8"PRIu64" %7.1f)\n",
               when, core->stats.conflicts, core->stats.decisions, core->stats.random_decisions,
               num_binary_clauses(core), num_prob_clauses(core), num_prob_literals(core),
               num_learned_clauses(core), num_learned_literals(core), avg_learned_clause_size(core));
#if 0
  fprintf(stderr,
          "(%-10s %8"PRIu64" %10"PRIu64" %8"PRIu64" %8"PRIu32" %8"PRIu32" %8"PRIu64" %8"PRIu32" %8"PRIu64" %7.1f)\n",
          when, core->stats.conflicts, core->stats.decisions, core->stats.random_decisions,
          num_binary_clauses(core), num_prob_clauses(core), num_prob_literals(core),
          num_learned_clauses(core), num_learned_literals(core), avg_learned_clause_size(core));
#endif
}

/*
 * On start_search
 */
static void trace_start(smt_core_t *core) {
  trace_stats(core, "start:", 1);
}


/*
 * On restart
 */
static void trace_restart(smt_core_t *core) {
  trace_stats(core, "restart:", 1);
}

static void trace_inner_restart(smt_core_t *core) {
  trace_stats(core, "inner restart:", 5);
}


/*
 * On reduce clause database
 */
static void trace_reduce(smt_core_t *core, uint64_t deleted) {
  trace_stats(core, "reduce:", 3);
  trace_printf(core->trace, 4, "(%"PRIu64" clauses deleted)\n", deleted);
}



/*
 * End of search
 */
static void trace_done(smt_core_t *core) {
  trace_stats(core, "done:", 1);
  trace_newline(core->trace, 1);
}



/*
 * PROCESS AN ASSUMPTION
 */

/*
 * l = assumption for the current decision level
 * If l is unassigned, we assign it and perform one round of propagation
 * If l is false, we record the conflict. The context is unsat under the
 * current set of assumptions.
 */
static void process_assumption(smt_core_t *core, literal_t l) {
  switch (literal_value(core, l)) {
  case VAL_UNDEF_FALSE:
  case VAL_UNDEF_TRUE:
    decide_literal(core, l);
    smt_process(core);
    break;

  case VAL_TRUE:
    break;

  case VAL_FALSE:
    save_conflicting_assumption(core, l);
    break;
  }
}


/*
 * MAIN SEARCH FUNCTIONS
 */

/*
 * Bounded search with the default branching heuristic (picosat-like)
 * - search until the conflict bound is reached or until the problem is solved.
 * - reduce_threshold: number of learned clauses above which reduce_clause_database is called
 * - r_factor = increment factor for reduce_threshold
 * - use the default branching heuristic implemented by the core
 */
static void search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_threshold, double r_factor) {
  uint64_t max_conflicts;
  uint64_t deletions;
  uint32_t r_threshold;
  literal_t l;

  assert(smt_status(core) == YICES_STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

  max_conflicts = num_conflicts(core) + conflict_bound;
  r_threshold = *reduce_threshold;

  smt_process(core);
  while (smt_status(core) == YICES_STATUS_SEARCHING && num_conflicts(core) <= max_conflicts) {
    // reduce heuristic
    if (num_learned_clauses(core) >= r_threshold) {
      deletions = core->stats.learned_clauses_deleted;
      reduce_clause_database(core);
      r_threshold = (uint32_t) (r_threshold * r_factor);
      trace_reduce(core, core->stats.learned_clauses_deleted - deletions);
    }

    // assumption
    if (core->has_assumptions) {
      l = get_next_assumption(core);
      if (l != null_literal) {
        process_assumption(core, l);
        continue;
      }
    }

    // decision
    l = select_unassigned_literal(core);
    if (l == null_literal) {
      // all variables assigned: Call final_check
      smt_final_check(core);
    } else {
      decide_literal(core, l);
      smt_process(core);
    }
  }

  *reduce_threshold = r_threshold;
}


/*
 * HACK: Variant for Luby restart:
 * - search until the conflict bound is reached or until the problem is solved.
 * - reduce_threshold: number of learned clauses above which reduce_clause_database is called
 * - r_factor = increment factor for reduce_threshold
 * - use the default branching heuristic implemented by the core
 *
 * This uses smt_bounded_process to force more frequent restarts.
 */
static void luby_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_threshold, double r_factor) {
  uint64_t max_conflicts;
  uint64_t deletions;
  uint32_t r_threshold;
  literal_t l;

  assert(smt_status(core) == YICES_STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

  max_conflicts = num_conflicts(core) + conflict_bound;
  r_threshold = *reduce_threshold;

  smt_bounded_process(core, max_conflicts);
  while (smt_status(core) == YICES_STATUS_SEARCHING && num_conflicts(core) < max_conflicts) {
    // reduce heuristic
    if (num_learned_clauses(core) >= r_threshold) {
      deletions = core->stats.learned_clauses_deleted;
      reduce_clause_database(core);
      r_threshold = (uint32_t) (r_threshold * r_factor);
      trace_reduce(core, core->stats.learned_clauses_deleted - deletions);
    }

    // assumption
    if (core->has_assumptions) {
      l = get_next_assumption(core);
      if (l != null_literal) {
        process_assumption(core, l);
        continue;
      }
    }

    // decision
    l = select_unassigned_literal(core);
    if (l == null_literal) {
      // all variables assigned: Call final_check
      smt_final_check(core);
    } else {
      decide_literal(core, l);
      smt_bounded_process(core, max_conflicts);
    }
  }

  *reduce_threshold = r_threshold;
}

/*
 * Polarity selection (implements branching heuristics)
 * - filter is given a literal l + core and must return either l or not l
 */
typedef literal_t (*branching_fun_t)(smt_core_t *core, literal_t l);


/*
 * Bounded search with a non-default branching heuristics
 * - search until the conflict bound is reached or until the problem is solved.
 * - reduce_threshold: number of learned clauses above which reduce_clause_database is called
 * - r_factor = increment factor for reduce_threshold
 * - use the branching heuristic implemented by branch
 */
static void special_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_threshold,
                           double r_factor, branching_fun_t branch) {
  uint64_t max_conflicts;
  uint64_t deletions;
  uint32_t r_threshold;
  literal_t l;

  assert(smt_status(core) == YICES_STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

  max_conflicts = num_conflicts(core) + conflict_bound;
  r_threshold = *reduce_threshold;

  smt_process(core);
  while (smt_status(core) == YICES_STATUS_SEARCHING && num_conflicts(core) <= max_conflicts) {
    // reduce heuristic
    if (num_learned_clauses(core) >= r_threshold) {
      deletions = core->stats.learned_clauses_deleted;
      reduce_clause_database(core);
      r_threshold = (uint32_t) (r_threshold * r_factor);
      trace_reduce(core, core->stats.learned_clauses_deleted - deletions);
    }

    // assumption
    if (core->has_assumptions) {
      l = get_next_assumption(core);
      if (l != null_literal) {
        process_assumption(core, l);
        continue;
      }
    }

    // decision
    l = select_unassigned_literal(core);
    if (l == null_literal) {
      // all variables assigned: call final check
      smt_final_check(core);
    } else {
      // apply the branching heuristic
      l = branch(core, l);
      // propagation
      decide_literal(core, l);
      smt_process(core);
    }
  }

  *reduce_threshold = r_threshold;
}





/*
 * SUPPORTED BRANCHING
 */

/*
 * Simple branching heuristics:
 * - branch to the negative polarity
 * - branch to the positive polarity
 */
static literal_t negative_branch(smt_core_t *core, literal_t l) {
  return l | 1; // force the sign bit to 1
}

static literal_t positive_branch(smt_core_t *core, literal_t l) {
  return l & ~1; // force the sign bit to 0
}


/*
 * For literals with no atom, use the default, otherwise let the theory solver decide
 */
static literal_t theory_branch(smt_core_t *core, literal_t l) {
  if (bvar_has_atom(core, var_of(l))) {
    l =  core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l);
  }
  return l;
}

// variants
static literal_t theory_or_neg_branch(smt_core_t *core, literal_t l) {
  if (bvar_has_atom(core, var_of(l))) {
    return core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l);
  } else {
    return l | 1;
  }
}

static literal_t theory_or_pos_branch(smt_core_t *core, literal_t l) {
  if (bvar_has_atom(core, var_of(l))) {
    return core->th_smt.select_polarity(core->th_solver, get_bvar_atom(core, var_of(l)), l);
  } else {
    return l & ~1;
  }
}





/*
 * CORE SOLVER
 */

/*
 * Full solver:
 * - params: heuristic parameters.
 * - n = number of assumptions
 * - a = array of n assumptions: a[0 ... n-1] must all be literals
 */
static void solve(smt_core_t *core, const param_t *params, uint32_t n, const literal_t *a) {
  bool luby;
  uint32_t c_threshold, d_threshold; // Picosat-style
  uint32_t u, v, period;             // for Luby-style
  uint32_t reduce_threshold;

  c_threshold = params->c_threshold;
  d_threshold = c_threshold; // required by trace_start in slow_restart mode
  luby = false;
  u = 1;
  v = 1;
  period = c_threshold;

  if (params->fast_restart) {
    d_threshold = params->d_threshold;
    // HACK to activate the Luby heuristic:
    // c_factor must be 0.0 and fast_restart must be true
    luby = params->c_factor == 0.0;
  }

  reduce_threshold = (uint32_t) (num_prob_clauses(core) * params->r_fraction);
  if (reduce_threshold < params->r_threshold) {
    reduce_threshold = params->r_threshold;
  }

  // initialize then do a propagation + simplification step.
  start_search(core, n, a);
  trace_start(core);
  if (smt_status(core) == YICES_STATUS_SEARCHING) {
    // loop
    for (;;) {
      switch (params->branching) {
      case BRANCHING_DEFAULT:
        if (luby) {
          luby_search(core, c_threshold, &reduce_threshold, params->r_factor);
        } else {
          search(core, c_threshold, &reduce_threshold, params->r_factor);
        }
        break;
      case BRANCHING_NEGATIVE:
        special_search(core, c_threshold, &reduce_threshold, params->r_factor, negative_branch);
        break;
      case BRANCHING_POSITIVE:
        special_search(core, c_threshold, &reduce_threshold, params->r_factor, positive_branch);
        break;
      case BRANCHING_THEORY:
        special_search(core, c_threshold, &reduce_threshold, params->r_factor, theory_branch);
        break;
      case BRANCHING_TH_NEG:
        special_search(core, c_threshold, &reduce_threshold, params->r_factor, theory_or_neg_branch);
        break;
      case BRANCHING_TH_POS:
        special_search(core, c_threshold, &reduce_threshold, params->r_factor, theory_or_pos_branch);
        break;
      }

      if (smt_status(core) != YICES_STATUS_SEARCHING) break;

      smt_restart(core);
      //      smt_partial_restart_var(core);

      if (luby) {
        // Luby-style restart
        if ((u & -u) == v) {
          u ++;
          v = 1;
        } else {
          v <<= 1;
        }
        c_threshold = v * period;
        trace_restart(core);

      } else {
        // Either Minisat or Picosat-like restart

        // inner restart: increase c_threshold
        c_threshold = (uint32_t) (c_threshold * params->c_factor);

        if (c_threshold >= d_threshold) {
          d_threshold = c_threshold; // Minisat-style
          if (params->fast_restart) {
            // Picosat style
            // outer restart: reset c_threshold and increase d_threshold
            c_threshold = params->c_threshold;
            d_threshold = (uint32_t) (d_threshold * params->d_factor);
          }
          trace_restart(core);
        } else {
          trace_inner_restart(core);
        }
      }
    }
  }

  trace_done(core);
}


/*
 * Initialize the search parameters based on params.
 */
static void context_set_search_parameters(context_t *ctx, const param_t *params) {
  smt_core_t *core;
  egraph_t *egraph;
  simplex_solver_t *simplex;
  fun_solver_t *fsolver;
  uint32_t quota;

  /*
   * Set core parameters
   */
  core = ctx->core;
  set_randomness(core, params->randomness);
  set_random_seed(core, params->random_seed);
  set_var_decay_factor(core, params->var_decay);
  set_clause_decay_factor(core, params->clause_decay);
  if (params->cache_tclauses) {
    enable_theory_cache(core, params->tclause_size);
  } else {
    disable_theory_cache(core);
  }

  /*
   * Set egraph parameters
   */
  egraph = ctx->egraph;
  if (egraph != NULL) {
    if (params->use_optimistic_fcheck) {
      egraph_enable_optimistic_final_check(egraph);
    } else {
      egraph_disable_optimistic_final_check(egraph);
    }
    if (params->use_dyn_ack) {
      egraph_enable_dyn_ackermann(egraph, params->max_ackermann);
      egraph_set_ackermann_threshold(egraph, params->dyn_ack_threshold);
    } else {
      egraph_disable_dyn_ackermann(egraph);
    }
    if (params->use_bool_dyn_ack) {
      egraph_enable_dyn_boolackermann(egraph, params->max_boolackermann);
      egraph_set_boolack_threshold(egraph, params->dyn_bool_ack_threshold);
    } else {
      egraph_disable_dyn_boolackermann(egraph);
    }
    quota = egraph_num_terms(egraph) * params->aux_eq_ratio;
    if (quota < params->aux_eq_quota) {
      quota = params->aux_eq_quota;
    }
    egraph_set_aux_eq_quota(egraph, quota);
    egraph_set_max_interface_eqs(egraph, params->max_interface_eqs);
  }

  /*
   * Set simplex parameters
   */
  if (context_has_simplex_solver(ctx)) {
    simplex = ctx->arith_solver;
    if (params->use_simplex_prop) {
      simplex_enable_propagation(simplex);
      simplex_set_prop_threshold(simplex, params->max_prop_row_size);
    }
    if (params->adjust_simplex_model) {
      simplex_enable_adjust_model(simplex);
    }
    simplex_set_bland_threshold(simplex, params->bland_threshold);
    if (params->integer_check) {
      simplex_enable_periodic_icheck(simplex);
      simplex_set_integer_check_period(simplex, params->integer_check_period);
    }
  }

  /*
   * Set array solver parameters
   */
  if (context_has_fun_solver(ctx)) {
    fsolver = ctx->fun_solver;
    fun_solver_set_max_update_conflicts(fsolver, params->max_update_conflicts);
    fun_solver_set_max_extensionality(fsolver, params->max_extensionality);
  }
}

static smt_status_t _o_call_mcsat_solver(context_t *ctx, const param_t *params) {
  mcsat_solve(ctx->mcsat, params, NULL, 0, NULL);
  return mcsat_status(ctx->mcsat);
}

static smt_status_t call_mcsat_solver(context_t *ctx, const param_t *params) {
  MT_PROTECT(smt_status_t, __yices_globals.lock, _o_call_mcsat_solver(ctx, params));
}

/*
 * Initialize search parameters then call solve
 * - if ctx->status is not IDLE, return the status.
 * - if params is NULL, we use default values.
 */
smt_status_t check_context(context_t *ctx, const param_t *params) {
  smt_core_t *core;
  smt_status_t stat;

  if (params == NULL) {
    params = get_default_params();
  }

  if (ctx->mcsat != NULL) {
    return call_mcsat_solver(ctx, params);
  }

  core = ctx->core;
  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    // clean state: the search can proceed
    context_set_search_parameters(ctx, params);
    solve(core, params, 0, NULL);
    stat = smt_status(core);
  }

  return stat;
}


/*
 * Check with assumptions a[0] ... a[n-1]
 * - if ctx->status is not IDLE, return the status.
 */
smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const literal_t *a) {
  smt_core_t *core;
  smt_status_t stat;

  assert(ctx->mcsat == NULL);

  core = ctx->core;
  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    // clean state
    if (params == NULL) {
      params = get_default_params();
    }
    context_set_search_parameters(ctx, params);
    solve(core, params, n, a);
    stat = smt_status(core);
  }

  return stat;
}

/*
 * Explore term t and collect all Boolean atoms into atoms.
 */
static void collect_boolean_atoms(context_t *ctx, term_t t, int_hset_t *atoms, int_hset_t *visited) {
  term_table_t *terms;
  uint32_t i, nchildren;

  if (t < 0) {
    t = not(t);
  }

  if (int_hset_member(visited, t)) {
    return;
  }
  int_hset_add(visited, t);

  terms = ctx->terms;
  if (term_type(terms, t) == bool_type(terms->types)) {
    int_hset_add(atoms, t);
  }

  if (term_is_projection(terms, t)) {
    collect_boolean_atoms(ctx, proj_term_arg(terms, t), atoms, visited);
  } else if (term_is_sum(terms, t)) {
    nchildren = term_num_children(terms, t);
    for (i=0; i<nchildren; i++) {
      term_t child;
      mpq_t q;
      mpq_init(q);
      sum_term_component(terms, t, i, q, &child);
      collect_boolean_atoms(ctx, child, atoms, visited);
      mpq_clear(q);
    }
  } else if (term_is_bvsum(terms, t)) {
    uint32_t nbits = term_bitsize(terms, t);
    int32_t *aux = (int32_t*) safe_malloc(nbits * sizeof(int32_t));
    nchildren = term_num_children(terms, t);
    for (i=0; i<nchildren; i++) {
      term_t child;
      bvsum_term_component(terms, t, i, aux, &child);
      collect_boolean_atoms(ctx, child, atoms, visited);
    }
    safe_free(aux);
  } else if (term_is_product(terms, t)) {
    nchildren = term_num_children(terms, t);
    for (i=0; i<nchildren; i++) {
      term_t child;
      uint32_t exp;
      product_term_component(terms, t, i, &child, &exp);
      collect_boolean_atoms(ctx, child, atoms, visited);
    }
  } else if (term_is_composite(terms, t)) {
    nchildren = term_num_children(terms, t);
    for (i=0; i<nchildren; i++) {
      collect_boolean_atoms(ctx, term_child(terms, t, i), atoms, visited);
    }
  }
}

/*
 * Extract assumptions whose labels appear in term t.
 */
static void core_from_labeled_interpolant(context_t *ctx, term_t t, const ivector_t *labels, const int_hmap_t *label_map, ivector_t *core) {
  int_hset_t atoms, visited;
  uint32_t i;

  init_int_hset(&atoms, 0);
  init_int_hset(&visited, 0);
  collect_boolean_atoms(ctx, t, &atoms, &visited);

  ivector_reset(core);
  for (i=0; i<labels->size; i++) {
    term_t label = labels->data[i];
    if (int_hset_member(&atoms, label)) {
      int_hmap_pair_t *p = int_hmap_find((int_hmap_t *) label_map, label);
      if (p != NULL) {
        ivector_push(core, p->val);
      }
    }
  }

  delete_int_hset(&visited);
  delete_int_hset(&atoms);
}

/*
 * Cache a core vector in the context.
 */
static void cache_unsat_core(context_t *ctx, const ivector_t *core) {
  if (ctx->unsat_core_cache == NULL) {
    ctx->unsat_core_cache = (ivector_t *) safe_malloc(sizeof(ivector_t));
    init_ivector(ctx->unsat_core_cache, core->size);
  } else {
    ivector_reset(ctx->unsat_core_cache);
  }
  ivector_copy(ctx->unsat_core_cache, core->data, core->size);
}

/*
 * Check under assumptions given as terms.
 * - if MCSAT is enabled, this uses temporary labels + model interpolation.
 * - otherwise terms are converted to literals and handled by the CDCL(T) path.
 *
 * Preconditions:
 * - context status must be IDLE.
 */
smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) {
  smt_status_t stat;
  ivector_t assumptions;
  uint32_t i;

  if (error != NULL) {
    *error = CTX_NO_ERROR;
  }

  context_invalidate_unsat_core_cache(ctx);

  if (ctx->mcsat == NULL) {
    literal_t l;

    init_ivector(&assumptions, n);
    for (i=0; i<n; i++) {
      l = context_add_assumption(ctx, a[i]);
      if (l < 0) {
        if (error != NULL) {
          *error = l;
        }
        delete_ivector(&assumptions);
        return YICES_STATUS_ERROR;
      }
      ivector_push(&assumptions, l);
    }

    stat = check_context_with_assumptions(ctx, params, n, assumptions.data);
    delete_ivector(&assumptions);
    return stat;
  }

  /*
   * MCSAT: create fresh labels b_i, assert (b_i => a_i), then solve with model b_i=true.
   * We extract interpolant/core before cleanup, then restore sticky UNSAT artifacts.
   */
  if (!context_supports_model_interpolation(ctx)) {
    if (error != NULL) {
      *error = CTX_OPERATION_NOT_SUPPORTED;
    }
    return YICES_STATUS_ERROR;
  }

  {
    model_t mdl;               // temporary model: sets all label terms b_i to true
    int_hmap_t label_map;      // map label b_i -> original assumption a_i
    ivector_t mapped_core;     // translated core over original assumptions
    term_t interpolant = NULL_TERM; // raw/substituted interpolant for sticky UNSAT result
    int32_t code;              // return code from assert_formula (negative on internalization error)
    bool pushed;               // whether we pushed a temporary scope and must pop it
    term_manager_t tm;

    init_model(&mdl, ctx->terms, true);
    init_int_hmap(&label_map, 0);
    init_ivector(&assumptions, n);
    init_ivector(&mapped_core, 0);
    init_term_manager(&tm, ctx->terms);
    stat = YICES_STATUS_IDLE;

    pushed = false;
    if (context_supports_pushpop(ctx)) {
      context_push(ctx);
      pushed = true;
    }

    for (i=0; i<n; i++) {
      term_t b = new_uninterpreted_term(ctx->terms, bool_id);
      term_t implication = mk_implies(&tm, b, a[i]);

      int_hmap_add(&label_map, b, a[i]);
      code = assert_formula(ctx, implication);
      if (code < 0) {
        if (error != NULL) {
          *error = code;
        }
        stat = YICES_STATUS_ERROR;
        break;
      }
      model_map_term(&mdl, b, vtbl_mk_bool(&mdl.vtbl, true));
      ivector_push(&assumptions, b);
    }

    if (stat != YICES_STATUS_ERROR) {
      stat = check_context_with_model(ctx, params, &mdl, n, assumptions.data);
      if (stat == YICES_STATUS_UNSAT) {
        term_subst_t subst;

        interpolant = context_get_unsat_model_interpolant(ctx);
        assert(interpolant != NULL_TERM);
        core_from_labeled_interpolant(ctx, interpolant, &assumptions, &label_map, &mapped_core);

        init_term_subst(&subst, &tm, n, assumptions.data, a);
        interpolant = apply_term_subst(&subst, interpolant);
        delete_term_subst(&subst);
      }
    }

    if (pushed) {
      mcsat_cleanup_assumptions(ctx->mcsat);
      context_pop(ctx);
    }
    if (stat == YICES_STATUS_UNSAT) {
      mcsat_set_unsat_result(ctx->mcsat, interpolant);
      cache_unsat_core(ctx, &mapped_core);
    }

    delete_term_manager(&tm);
    delete_ivector(&mapped_core);
    delete_ivector(&assumptions);
    delete_int_hmap(&label_map);
    delete_model(&mdl);

    return stat;
  }
}

/*
 * Check with given model
 * - if mcsat status is not IDLE, return the status
 */
smt_status_t check_context_with_model(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]) {
  smt_status_t stat;

  assert(ctx->mcsat != NULL);

  stat = mcsat_status(ctx->mcsat);
  if (stat == YICES_STATUS_IDLE) {
    mcsat_solve(ctx->mcsat, params, mdl, n, t);
    stat = mcsat_status(ctx->mcsat);

    // BD: this looks wrong. We shouldn't call clear yet.
    // we want the status to remain STATUS_UNSAT until the next call to check or assert.
    //    if (n > 0 && stat == STATUS_UNSAT && context_supports_multichecks(ctx)) {
    //      context_clear(ctx);
    //    }
  }

  return stat;
}

/*
 * Check with given model and hints
 * - set the model hint and call check_context_with_model
 */
smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) {
  assert(m <= n);

  mcsat_set_model_hint(ctx->mcsat, mdl, n, t);

  return check_context_with_model(ctx, params, mdl, m, t);
}


/*
 * Precheck: force generation of clauses and other stuff that's
 * constructed lazily by the solvers. For example, this
 * can be used to convert all the constraints asserted in the
 * bitvector to clauses so that we can export the result to DIMACS.
 *
 * If ctx status is IDLE:
 * - the function calls 'start_search' and does one round of propagation.
 * - if this results in UNSAT, the function returns UNSAT
 * - if the precheck is interrupted, the function returns INTERRUPTED
 * - otherwise the function returns UNKNOWN and sets the status to
 *   UNKNOWN.
 *
 * IMPORTANT: call smt_clear or smt_cleanup to restore the context to
 * IDLE before doing anything else with this context.
 *
 * If ctx status is not IDLE, the function returns it and does nothing
 * else.
 */
smt_status_t precheck_context(context_t *ctx) {
  smt_status_t stat;
  smt_core_t *core;

  core = ctx->core;

  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    start_search(core, 0, NULL);
    smt_process(core);
    stat = smt_status(core);

    assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING ||
           stat == YICES_STATUS_INTERRUPTED);

    if (stat == YICES_STATUS_SEARCHING) {
      end_search_unknown(core);
      stat = YICES_STATUS_UNKNOWN;
    }
  }

  return stat;
}



/*
 * Solve using another SAT solver
 * - sat_solver = name of the solver to use
 * - verbosity = verbosity level (0 means quiet)
 * - this may be used only for BV or pure SAT problems
 * - we perform one round of propagation to convert the problem to CNF
 * - then we call an external SAT solver on the CNF problem
 */
smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity) {
  smt_status_t stat;
  smt_core_t *core;
  delegate_t delegate;
  bvar_t x;
  bval_t v;

  core = ctx->core;

  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    start_search(core, 0, NULL);
    smt_process(core);
    stat = smt_status(core);

    assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING ||
           stat == YICES_STATUS_INTERRUPTED);

    if (stat == YICES_STATUS_SEARCHING) {
      if (smt_easy_sat(core)) {
        stat = YICES_STATUS_SAT;
      } else {
        // call the delegate
        init_delegate(&delegate, sat_solver, num_vars(core));
        delegate_set_verbosity(&delegate, verbosity);

        stat = solve_with_delegate(&delegate, core);
        set_smt_status(core, stat);
        if (stat == YICES_STATUS_SAT) {
          for (x=0; x<num_vars(core); x++) {
            v = delegate_get_value(&delegate, x);
            set_bvar_value(core, x, v);
          }
        }
        delete_delegate(&delegate);
      }
    }
  }

  return stat;
}


/*
 * Bit-blast then export to DIMACS
 * - filename = name of the output file
 * - status = status of the context after bit-blasting
 *
 * If ctx status is IDLE
 * - perform one round of propagation to conver the problem to CNF
 * - export the CNF to DIMACS
 *
 * If ctx status is not IDLE,
 * - store the stauts in *status and do nothing else
 *
 * Return code:
 *  1 if the DIMACS file was created
 *  0 if the problem was solved by the propagation round
 * -1 if there was an error in creating or writing to the file.
 */
int32_t bitblast_then_export_to_dimacs(context_t *ctx, const char *filename, smt_status_t *status) {
  smt_core_t *core;
  FILE *f;
  smt_status_t stat;
  int32_t code;

  core = ctx->core;

  code = 0;
  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    start_search(core, 0, NULL);
    smt_process(core);
    stat = smt_status(core);

    assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING ||
           stat == YICES_STATUS_INTERRUPTED);

    if (stat == YICES_STATUS_SEARCHING) {
      code = 1;
      f = fopen(filename, "w");
      if (f == NULL) {
        code = -1;
      } else {
        dimacs_print_bvcontext(f, ctx);
        if (ferror(f)) code = -1;
        fclose(f);
      }
    }
  }

  *status = stat;

  return code;
}


/*
 * Simplify then export to Dimacs:
 * - filename = name of the output file
 * - status = status of the context after CNF conversion + preprocessing
 *
 * If ctx status is IDLE
 * - perform one round of propagation to convert the problem to CNF
 * - export the CNF to y2sat for extra preprocessing then export that to DIMACS
 *
 * If ctx status is not IDLE, the function stores that in *status
 * If y2sat preprocessing solves the formula, return the status also in *status
 *
 * Return code:
 *  1 if the DIMACS file was created
 *  0 if the problems was solved by preprocessing (or if ctx status is not IDLE)
 * -1 if there was an error creating or writing to the file.
 */
int32_t process_then_export_to_dimacs(context_t *ctx, const char *filename, smt_status_t *status) {
  smt_core_t *core;
  FILE *f;
  smt_status_t stat;
  delegate_t delegate;
  bvar_t x;
  bval_t v;
  int32_t code;

  core = ctx->core;

  code = 0;
  stat = smt_status(core);
  if (stat == YICES_STATUS_IDLE) {
    start_search(core, 0, NULL);
    smt_process(core);
    stat = smt_status(core);

    assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING ||
           stat == YICES_STATUS_INTERRUPTED);

    if (stat == YICES_STATUS_SEARCHING) {
      if (smt_easy_sat(core)) {
        stat = YICES_STATUS_SAT;
      } else {
        // call the delegate
        init_delegate(&delegate, "y2sat", num_vars(core));
        delegate_set_verbosity(&delegate, 0);

        stat = preprocess_with_delegate(&delegate, core);
        set_smt_status(core, stat);
        if (stat == YICES_STATUS_SAT) {
          for (x=0; x<num_vars(core); x++) {
            v = delegate_get_value(&delegate, x);
            set_bvar_value(core, x, v);
          }
        } else if (stat == YICES_STATUS_UNKNOWN) {
          code = 1;
          f = fopen(filename, "w");
          if (f == NULL) {
            code = -1;
          } else {
            export_to_dimacs_with_delegate(&delegate, f);
            if (ferror(f)) code = -1;
            fclose(f);
          }
        }

        delete_delegate(&delegate);
      }
    }
  }

  *status = stat;

  return code;
}



/*
 * MODEL CONSTRUCTION
 */

/*
 * Value of literal l in ctx->core
 */
static value_t bool_value(context_t *ctx, value_table_t *vtbl, literal_t l) {
  value_t v;

  v = null_value; // prevent GCC warning
  switch (literal_value(ctx->core, l)) {
  case VAL_FALSE:
    v = vtbl_mk_false(vtbl);
    break;
  case VAL_UNDEF_FALSE:
  case VAL_UNDEF_TRUE:
    v = vtbl_mk_unknown(vtbl);
    break;
  case VAL_TRUE:
    v = vtbl_mk_true(vtbl);
    break;
  }
  return v;
}


/*
 * Value of arithmetic variable x in ctx->arith_solver
 */
static value_t arith_value(context_t *ctx, value_table_t *vtbl, thvar_t x) {
  rational_t *a;
  value_t v;

  assert(context_has_arith_solver(ctx));

  a = &ctx->aux;
  if (ctx->arith.value_in_model(ctx->arith_solver, x, a)) {
    v = vtbl_mk_rational(vtbl, a);
  } else {
    v = vtbl_mk_unknown(vtbl);
  }

  return v;
}



/*
 * Value of bitvector variable x in ctx->bv_solver
 */
static value_t bv_value(context_t *ctx, value_table_t *vtbl, thvar_t x) {
  bvconstant_t *b;
  value_t v;

  assert(context_has_bv_solver(ctx));

  b = &ctx->bv_buffer;
  if (ctx->bv.value_in_model(ctx->bv_solver, x, b)) {
    v = vtbl_mk_bv_from_constant(vtbl, b);
  } else {
    v = vtbl_mk_unknown(vtbl);
  }

  return v;
}


/*
 * Get a value for term t in the solvers or egraph
 * - attach the mapping from t to that value in model
 * - if we don't have a concrete object for t but t is
 *   mapped to a term u and the model->has_alias is true,
 *   then we store the mapping [t --> u] in the model's
 *   alias map.
 */
static void build_term_value(context_t *ctx, model_t *model, term_t t) {
  value_table_t *vtbl;
  term_t r;
  uint32_t polarity;
  int32_t x;
  type_t tau;
  value_t v;

  /*
   * Get the root of t in the substitution table
   */
  r = intern_tbl_get_root(&ctx->intern, t);
  if (intern_tbl_root_is_mapped(&ctx->intern, r)) {
    /*
     * r is mapped to some object x in egraph/core/or theory solvers
     * - keep track of polarity then force r to positive polarity
     */
    vtbl = model_get_vtbl(model);
    polarity = polarity_of(r);
    r = unsigned_term(r);

    /*
     * Convert x to a concrete value
     */
    x = intern_tbl_map_of_root(&ctx->intern, r);
    if (code_is_eterm(x)) {
      // x refers to an egraph object or true_occ/false_occ
      if (x == bool2code(true)) {
        v = vtbl_mk_true(vtbl);
      } else if (x == bool2code(false)) {
        v = vtbl_mk_false(vtbl);
      } else {
        assert(context_has_egraph(ctx));
        v = egraph_get_value(ctx->egraph, vtbl, code2occ(x));
      }

    } else {
      // x refers to a literal or a theory variable
      tau = term_type(ctx->terms, r);
      switch (type_kind(ctx->types, tau)) {
      case BOOL_TYPE:
        v = bool_value(ctx, vtbl, code2literal(x));
        break;

      case INT_TYPE:
      case REAL_TYPE:
        v = arith_value(ctx, vtbl, code2thvar(x));
        break;

      case BITVECTOR_TYPE:
        v = bv_value(ctx, vtbl, code2thvar(x));
        break;

      default:
        /*
         * This should never happen:
         * scalar, uninterpreted, tuple, function terms
         * are mapped to egraph terms.
         */
        assert(false);
        v = vtbl_mk_unknown(vtbl); // prevent GCC warning
        break;
      }
    }

    /*
     * Restore polarity then add mapping [t --> v] in the model
     */
    if (! object_is_unknown(vtbl, v)) {
      if (object_is_boolean(vtbl, v)) {
        if (polarity) {
          // negate the value
          v = vtbl_mk_not(vtbl, v);
        }
      }
      model_map_term(model, t, v);
    }

  } else {
    /*
     * r is not mapped to anything:
     *
     * 1) If t == r and t is present in the internalization table
     *    then t is relevant. So we should display its value
     *    when we print the model. To do this, we assign an
     *    arbitrary value v to t and store [t := v] in the map.
     *
     * 2) If t != r then we keep the mapping [t --> r] in
     *    the alias table (provided the model supports aliases).
     */
    if (t == r) {
      if (intern_tbl_term_present(&ctx->intern, t)) {
        tau = term_type(ctx->terms, t);
        vtbl = model_get_vtbl(model);
        v = vtbl_make_object(vtbl, tau);
        model_map_term(model, t, v);
      }
    } else if (model->has_alias) {
      // t != r: keep the substitution [t --> r] in the model
      model_add_substitution(model, t, r);
    }
  }
}




/*
 * Build a model for the current context (including all satellite solvers)
 * - the context status must be SAT (or UNKNOWN)
 * - if model->has_alias is true, we store the term substitution
 *   defined by ctx->intern_tbl into the model
 * - cleanup of satellite models needed using clean_solver_models()
 */
void build_model(model_t *model, context_t *ctx) {
  term_table_t *terms;
  uint32_t i, n;
  term_t t;

  assert(smt_status(ctx->core) == YICES_STATUS_SAT || smt_status(ctx->core) == YICES_STATUS_UNKNOWN || mcsat_status(ctx->mcsat) == YICES_STATUS_SAT);

  /*
   * First build assignments in the satellite solvers
   * and get the val_in_model functions for the egraph
   */
  if (context_has_arith_solver(ctx)) {
    ctx->arith.build_model(ctx->arith_solver);
  }
  if (context_has_bv_solver(ctx)) {
    ctx->bv.build_model(ctx->bv_solver);
  }

  /*
   * Construct the egraph model
   */
  if (context_has_egraph(ctx)) {
    egraph_build_model(ctx->egraph, model_get_vtbl(model));
  }

  /*
   * Construct the mcsat model.
   */
  if (context_has_mcsat(ctx)) {
    mcsat_build_model(ctx->mcsat, model);
  }

  // scan the internalization table
  terms = ctx->terms;
  n = intern_tbl_num_terms(&ctx->intern);
  for (i=1; i<n; i++) { // first real term has index 1 (i.e. true_term)
    if (good_term_idx(terms, i)) {
      t = pos_occ(i);
      if (term_kind(terms, t) == UNINTERPRETED_TERM) {
        build_term_value(ctx, model, t);
      }
    }
  }
}


/*
 * Cleanup solver models
 */
void clean_solver_models(context_t *ctx) {
  if (context_has_arith_solver(ctx)) {
    ctx->arith.free_model(ctx->arith_solver);
  }
  if (context_has_bv_solver(ctx)) {
    ctx->bv.free_model(ctx->bv_solver);
  }
  if (context_has_egraph(ctx)) {
    egraph_free_model(ctx->egraph);
  }
}



/*
 * Build a model for the current context
 * - the context status must be SAT (or UNKNOWN)
 * - if model->has_alias is true, we store the term substitution
 *   defined by ctx->intern_tbl into the model
 */
void context_build_model(model_t *model, context_t *ctx) {
  // Build solver models and term values
  build_model(model, ctx);

  // Cleanup
  clean_solver_models(ctx);
}



/*
 * Read the value of a Boolean term t
 * - return VAL_TRUE/VAL_FALSE or VAL_UNDEF_FALSE/VAL_UNDEF_TRUE if t's value is not known
 */
bval_t context_bool_term_value(context_t *ctx, term_t t) {
  term_t r;
  uint32_t polarity;
  int32_t x;
  bval_t v;

  assert(is_boolean_term(ctx->terms, t));

  // default value if t is not in the internalization table
  v = VAL_UNDEF_FALSE;
  r = intern_tbl_get_root(&ctx->intern, t);
  if (intern_tbl_root_is_mapped(&ctx->intern, r)) {
    // r is mapped to some object x
    polarity = polarity_of(r);
    r = unsigned_term(r);

    x  = intern_tbl_map_of_root(&ctx->intern, r);
    if (code_is_eterm(x)) {
      // x must be either true_occ or false_occ
      if (x == bool2code(true)) {
        v = VAL_TRUE;
      } else {
        assert(x == bool2code(false));
        v = VAL_FALSE;
      }
    } else {
      // x refers to a literal in the smt core
      v = literal_value(ctx->core, code2literal(x));
    }

    // negate v if polarity is 1 (cf. smt_core_base_types.h)
    v ^= polarity;
  }

  return v;
}


/*
 * UNSAT CORE
 */

/*
 * Build an unsat core:
 * - store the result in v
 * - first reuse a cached term core if available.
 * - otherwise:
 *   CDCL(T): build from smt_core then cache as terms
 *   MCSAT: return empty unless check-with-term-assumptions populated the cache.
 */
void context_build_unsat_core(context_t *ctx, ivector_t *v) {
  smt_core_t *core;
  uint32_t i, n;
  term_t t;

  if (ctx->unsat_core_cache != NULL) {
    // Fast path: repeated get_unsat_core returns the cached term vector.
    ivector_reset(v);
    ivector_copy(v, ctx->unsat_core_cache->data, ctx->unsat_core_cache->size);
    return;
  }

  if (ctx->mcsat != NULL) {
    // MCSAT core extraction is done in check-with-term-assumptions; without cache
    // there is no generic context-level core structure to rebuild from here.
    ivector_reset(v);
    return;
  }

  core = ctx->core;
  assert(core != NULL && core->status == YICES_STATUS_UNSAT);
  build_unsat_core(core, v);

  // convert from literals to terms
  n = v->size;
  for (i=0; i<n; i++) {
    t = assumption_term_for_literal(&ctx->assumptions, v->data[i]);
    assert(t >= 0);
    v->data[i] = t;
  }

  // Cache the converted term core for subsequent queries.
  cache_unsat_core(ctx, v);
}


/*
 * MODEL INTERPOLANT
 */
term_t context_get_unsat_model_interpolant(context_t *ctx) {
  assert(ctx->mcsat != NULL);
  return mcsat_get_unsat_model_interpolant(ctx->mcsat);
}

SRI-CSL / yices2 / 22552082017

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