26150511973

Committed 20 May 2026 08:06AM UTC coverage: 67.598% (+0.1%) from 67.453%

Build # 26150511973

Build Type

Pull #611

github

Committed by

disteph

Commit Message

Merge branch 'master' into mcsat-supplement-cdclt

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

Coverage Stats

682 of 994 new or added lines in 15 files covered. (68.61%)

2 existing lines in 2 files now uncovered.

86598 of 128107 relevant lines covered (67.6%)

1614128.85 hits per line

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

77.32

/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 <string.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/mcsat_satellite.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 "utils/memalloc.h"

#include "api/yices_globals.h"
#include "api/yices_api_lock_free.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);
  }

  if (ctx->mcsat_supplement_active && egraph != NULL && egraph->th[ETYPE_MCSAT] != NULL) {
    mcsat_satellite_set_search_parameters((mcsat_satellite_t *) egraph->th[ETYPE_MCSAT], params);
  }

  /*
   * 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) {
  smt_status_t stat;

  mcsat_solve(ctx->mcsat, params, NULL, 0, NULL);
  stat = mcsat_status(ctx->mcsat);

  /*
   * For plain UNSAT results (without explicit model assumptions), keep the
   * interpolant API usable by providing the canonical false interpolant.
   */
  if (stat == YICES_STATUS_UNSAT &&
      context_supports_model_interpolation(ctx) &&
      mcsat_get_unsat_model_interpolant(ctx->mcsat) == NULL_TERM) {
    mcsat_set_unsat_result_from_labeled_interpolant(ctx->mcsat, false_term, 0, NULL, NULL);
  }

  return stat;
}

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;
  mcsat_satellite_t *sat;

  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);
  }

  sat = NULL;
  if (ctx->mcsat_supplement_active &&
      ctx->egraph != NULL &&
      ctx->egraph->th[ETYPE_MCSAT] != NULL) {
    sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT];
  }
  if (stat == YICES_STATUS_UNSAT &&
      sat != NULL &&
      context_supports_model_interpolation(ctx) &&
      mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) {
    mcsat_satellite_set_unsat_model_interpolant(sat, false_term);
  }

  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;
  mcsat_satellite_t *sat;

  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);
  }

  sat = NULL;
  if (ctx->mcsat_supplement_active &&
      ctx->egraph != NULL &&
      ctx->egraph->th[ETYPE_MCSAT] != NULL) {
    sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT];
  }
  if (stat == YICES_STATUS_UNSAT &&
      sat != NULL &&
      context_supports_model_interpolation(ctx) &&
      mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) {
    mcsat_satellite_set_unsat_model_interpolant(sat, false_term);
  }

  return stat;
}

typedef struct sat_delegate_state_s {
  delegate_t delegate;
  sat_delegate_t mode;
  sat_delegate_incremental_mode_t exec_mode;
  bool live;
  bool stale;
  bool true_forwarded;
  bool checked_once;
  uint32_t delegate_nvars;
  uint32_t size;
  bvar_t *act_var;
  uint32_t *fwd_units;
  uint32_t *fwd_bins;
  uint32_t *fwd_clauses;
  ivector_t assumptions;
  ivector_t failed;
} sat_delegate_state_t;

void context_reset_sat_delegate_stats(context_t *ctx) {
  ctx->sat_delegate_stats.rebuild_checks = 0;
  ctx->sat_delegate_stats.append_checks = 0;
  ctx->sat_delegate_stats.selector_frame_checks = 0;
  ctx->sat_delegate_stats.delegate_initializations = 0;
  ctx->sat_delegate_stats.delegate_reinitializations = 0;
  ctx->sat_delegate_stats.selector_variables = 0;
  ctx->sat_delegate_stats.selector_assumptions = 0;
  ctx->sat_delegate_stats.selector_retirements = 0;
  ctx->sat_delegate_stats.post_check_clause_forwards = 0;
}

void context_get_sat_delegate_stats(const context_t *ctx, sat_delegate_stats_t *stats) {
  *stats = ctx->sat_delegate_stats;
}

void context_sat_delegate_state_cleanup(context_t *ctx) {
  sat_delegate_state_t *st;

  st = (sat_delegate_state_t *) ctx->sat_delegate_state;
  if (st == NULL) {
    return;
  }

  if (st->live) {
    delete_delegate(&st->delegate);
    st->live = false;
  }
  safe_free(st->act_var);
  safe_free(st->fwd_units);
  safe_free(st->fwd_bins);
  safe_free(st->fwd_clauses);
  delete_ivector(&st->assumptions);
  delete_ivector(&st->failed);
  safe_free(st);
  ctx->sat_delegate_state = NULL;
}

static sat_delegate_state_t *context_get_sat_delegate_state(context_t *ctx) {
  sat_delegate_state_t *st;

  st = (sat_delegate_state_t *) ctx->sat_delegate_state;
  if (st == NULL) {
    st = (sat_delegate_state_t *) safe_malloc(sizeof(sat_delegate_state_t));
    st->mode = SAT_DELEGATE_NONE;
    st->exec_mode = SAT_DELEGATE_MODE_REBUILD;
    st->live = false;
    st->stale = false;
    st->true_forwarded = false;
    st->checked_once = false;
    st->delegate_nvars = 0;
    st->size = 0;
    st->act_var = NULL;
    st->fwd_units = NULL;
    st->fwd_bins = NULL;
    st->fwd_clauses = NULL;
    init_ivector(&st->assumptions, 0);
    init_ivector(&st->failed, 0);
    ctx->sat_delegate_state = st;
  }
  return st;
}

static void sat_delegate_state_reset_cursors(sat_delegate_state_t *st) {
  uint32_t i;

  st->true_forwarded = false;
  for (i=0; i<st->size; i++) {
    st->act_var[i] = 0;
    st->fwd_units[i] = 0;
    st->fwd_bins[i] = 0;
    st->fwd_clauses[i] = 0;
  }
}

static void sat_delegate_state_grow(sat_delegate_state_t *st, uint32_t min_size) {
  uint32_t old_size, new_size, i;

  if (st->size > min_size) {
    return;
  }

  old_size = st->size;
  new_size = old_size == 0 ? 8 : old_size;
  while (new_size <= min_size) {
    new_size <<= 1;
  }

  st->act_var = (bvar_t *) safe_realloc(st->act_var, new_size * sizeof(bvar_t));
  st->fwd_units = (uint32_t *) safe_realloc(st->fwd_units, new_size * sizeof(uint32_t));
  st->fwd_bins = (uint32_t *) safe_realloc(st->fwd_bins, new_size * sizeof(uint32_t));
  st->fwd_clauses = (uint32_t *) safe_realloc(st->fwd_clauses, new_size * sizeof(uint32_t));
  for (i=old_size; i<new_size; i++) {
    st->act_var[i] = 0;
    st->fwd_units[i] = 0;
    st->fwd_bins[i] = 0;
    st->fwd_clauses[i] = 0;
  }
  st->size = new_size;
}

static void context_import_delegate_model(smt_core_t *core, delegate_t *d) {
  bvar_t x;

  for (x=0; x<num_vars(core); x++) {
    set_bvar_value(core, x, delegate_get_value(d, x));
  }
}

static void set_delegate_assumption_state(smt_core_t *core, uint32_t n, const literal_t *assumptions,
                                          smt_status_t stat, const ivector_t *failed) {
  if (n == 0) {
    core->has_assumptions = false;
    core->num_assumptions = 0;
    core->assumption_index = 0;
    core->assumptions = NULL;
    core->bad_assumption = null_literal;
    return;
  }

  core->has_assumptions = true;
  core->num_assumptions = n;
  core->assumption_index = n;
  core->assumptions = NULL;
  core->bad_assumption = null_literal;

  if (stat == YICES_STATUS_UNSAT && failed != NULL && failed->size > 0) {
    core->bad_assumption = failed->data[0];
  }
}

static void delegate_add_clause_with_guard(delegate_t *delegate, const clause_t *c, literal_t guard) {
  uint32_t i;
  literal_t l;

  ivector_reset(&delegate->buffer);
  if (guard != true_literal) {
    ivector_push(&delegate->buffer, guard);
  }
  i = 0;
  l = c->cl[0];
  while (l >= 0) {
    ivector_push(&delegate->buffer, l);
    i ++;
    l = c->cl[i];
  }
  delegate->add_clause(delegate->solver, delegate->buffer.size, delegate->buffer.data);
}

static void delegate_forward_clause_range(sat_delegate_state_t *st, smt_core_t *core, sat_delegate_stats_t *stats,
                                          uint32_t level,
                                          uint32_t end_units, uint32_t end_bins, uint32_t end_clauses,
                                          literal_t guard) {
  uint32_t i;
  bool forwarded;

  if (!st->true_forwarded) {
    st->delegate.add_unit_clause(st->delegate.solver, true_literal);
    st->true_forwarded = true;
  }

  forwarded = (core->inconsistent && st->fwd_units[level] == 0 && st->fwd_bins[level] == 0 && st->fwd_clauses[level] == 0) ||
              st->fwd_units[level] < end_units ||
              st->fwd_bins[level] < end_bins ||
              st->fwd_clauses[level] < end_clauses;
  if (st->checked_once && forwarded) {
    stats->post_check_clause_forwards ++;
  }

  if (core->inconsistent && st->fwd_units[level] == 0 && st->fwd_bins[level] == 0 && st->fwd_clauses[level] == 0) {
    if (guard == true_literal) {
      st->delegate.add_empty_clause(st->delegate.solver);
    } else {
      st->delegate.add_unit_clause(st->delegate.solver, guard);
    }
  }

  for (i=st->fwd_units[level]; i<end_units; i++) {
    if (guard == true_literal) {
      st->delegate.add_unit_clause(st->delegate.solver, core->stack.lit[i]);
    } else {
      st->delegate.add_binary_clause(st->delegate.solver, guard, core->stack.lit[i]);
    }
  }
  st->fwd_units[level] = end_units;

  for (i=st->fwd_bins[level]; i<end_bins; i += 2) {
    if (guard == true_literal) {
      st->delegate.add_binary_clause(st->delegate.solver, core->binary_clauses.data[i], core->binary_clauses.data[i+1]);
    } else {
      st->delegate.add_ternary_clause(st->delegate.solver, guard, core->binary_clauses.data[i], core->binary_clauses.data[i+1]);
    }
  }
  st->fwd_bins[level] = end_bins;

  if (level == 0 && st->fwd_clauses[level] > end_clauses) {
    st->fwd_clauses[level] = end_clauses;
  }
  for (i=st->fwd_clauses[level]; i<end_clauses; i++) {
    delegate_add_clause_with_guard(&st->delegate, core->problem_clauses[i], guard);
  }
  st->fwd_clauses[level] = end_clauses;
}

static void sat_delegate_state_close(sat_delegate_state_t *st) {
  if (st->live) {
    delete_delegate(&st->delegate);
    st->live = false;
  }
  st->mode = SAT_DELEGATE_NONE;
  st->exec_mode = SAT_DELEGATE_MODE_REBUILD;
  st->stale = false;
  st->checked_once = false;
  st->delegate_nvars = 0;
  sat_delegate_state_reset_cursors(st);
}

static bool context_prepare_append_delegate(context_t *ctx, sat_delegate_state_t *st, const char *sat_solver,
                                            uint32_t verbosity) {
  smt_core_t *core;
  uint32_t nvars;
  uint32_t nnew;

  core = ctx->core;
  nvars = num_vars(core);

  if (st->live && (st->mode != ctx->sat_delegate || st->exec_mode != SAT_DELEGATE_MODE_APPEND)) {
    sat_delegate_state_close(st);
  }

  if (!st->live || st->stale) {
    if (st->live) {
      ctx->sat_delegate_stats.delegate_reinitializations ++;
      sat_delegate_state_close(st);
    }
    sat_delegate_state_grow(st, 0);
    if (!init_delegate_incremental(&st->delegate, sat_solver, nvars)) {
      return false;
    }
    ctx->sat_delegate_stats.delegate_initializations ++;
    delegate_set_verbosity(&st->delegate, verbosity);
    st->mode = ctx->sat_delegate;
    st->exec_mode = SAT_DELEGATE_MODE_APPEND;
    st->stale = false;
    st->delegate_nvars = nvars;
    st->live = true;
    sat_delegate_state_reset_cursors(st);
  }

  if (st->delegate_nvars < nvars) {
    nnew = nvars - st->delegate_nvars;
    delegate_add_vars(&st->delegate, nnew);
    st->delegate_nvars = nvars;
  }

  sat_delegate_state_grow(st, 0);
  delegate_forward_clause_range(st, core, &ctx->sat_delegate_stats, 0, core->nb_unit_clauses,
                                (uint32_t) core->binary_clauses.size,
                                (uint32_t) get_cv_size(core->problem_clauses),
                                true_literal);

  return true;
}

static bool context_prepare_selector_delegate(context_t *ctx, sat_delegate_state_t *st, const char *sat_solver,
                                              uint32_t verbosity) {
  smt_core_t *core;
  uint32_t d, k, nvars, nnew;
  uint32_t end_units, end_bins, end_clauses;
  trail_t *trail_data;
  literal_t guard;

  core = ctx->core;
  nvars = num_vars(core);
  d = smt_base_level(core);
  trail_data = core->trail_stack.data;

  if (st->live && (st->mode != ctx->sat_delegate || st->exec_mode != SAT_DELEGATE_MODE_SELECTOR_FRAMES)) {
    sat_delegate_state_close(st);
  }

  if (!st->live) {
    sat_delegate_state_grow(st, d);
    if (!init_delegate_incremental(&st->delegate, sat_solver, nvars)) {
      return false;
    }
    ctx->sat_delegate_stats.delegate_initializations ++;
    delegate_set_verbosity(&st->delegate, verbosity);
    st->mode = ctx->sat_delegate;
    st->exec_mode = SAT_DELEGATE_MODE_SELECTOR_FRAMES;
    st->stale = false;
    st->delegate_nvars = nvars;
    st->live = true;
    sat_delegate_state_reset_cursors(st);
  }

  if (st->delegate_nvars < nvars) {
    nnew = nvars - st->delegate_nvars;
    delegate_add_vars(&st->delegate, nnew);
    st->delegate_nvars = nvars;
  }

  sat_delegate_state_grow(st, d);
  for (k=1; k<=d; k++) {
    if (st->act_var[k] == 0) {
      /*
       * Selectors must live in the SMT core's variable namespace too:
       * otherwise a later bit-blasted assertion could reuse the same bvar.
       */
      do {
        st->act_var[k] = create_boolean_variable(core);
      } while (st->act_var[k] < st->delegate_nvars);
      delegate_add_vars(&st->delegate, st->act_var[k] + 1 - st->delegate_nvars);
      delegate_freeze_literal(&st->delegate, pos_lit(st->act_var[k]));
      ctx->sat_delegate_stats.selector_variables ++;
      st->delegate_nvars = st->act_var[k] + 1;
      st->fwd_units[k] = trail_data[k-1].nunits;
      st->fwd_bins[k] = trail_data[k-1].nbins;
      st->fwd_clauses[k] = trail_data[k-1].nclauses;
    }
  }

  for (k=0; k<=d; k++) {
    guard = (k == 0) ? true_literal : neg_lit(st->act_var[k]);
    end_units = (k < d) ? trail_data[k].nunits : core->nb_unit_clauses;
    end_bins = (k < d) ? trail_data[k].nbins : (uint32_t) core->binary_clauses.size;
    end_clauses = (k < d) ? trail_data[k].nclauses : (uint32_t) get_cv_size(core->problem_clauses);
    delegate_forward_clause_range(st, core, &ctx->sat_delegate_stats, k, end_units, end_bins, end_clauses, guard);
  }

  return true;
}

void context_sat_delegate_state_pop(context_t *ctx, uint32_t level) {
  sat_delegate_state_t *st;

  st = (sat_delegate_state_t *) ctx->sat_delegate_state;
  if (st == NULL || !st->live) {
    return;
  }

  if (st->exec_mode == SAT_DELEGATE_MODE_APPEND) {
    st->stale = true;
  } else if (st->exec_mode == SAT_DELEGATE_MODE_SELECTOR_FRAMES) {
    if (level < st->size && st->act_var[level] != 0) {
      delegate_melt_literal(&st->delegate, pos_lit(st->act_var[level]));
      st->delegate.add_unit_clause(st->delegate.solver, neg_lit(st->act_var[level]));
      ctx->sat_delegate_stats.selector_retirements ++;
      st->act_var[level] = 0;
    }
  }
}

static smt_status_t check_with_persistent_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity,
                                                   sat_delegate_incremental_mode_t exec_mode,
                                                   uint32_t n, const literal_t *assumptions, ivector_t *failed) {
  smt_status_t stat;
  smt_core_t *core;
  sat_delegate_state_t *st;
  ivector_t visible_failed;
  uint32_t i;

  core = ctx->core;
  stat = smt_status(core);
  if (stat != YICES_STATUS_IDLE) {
    return stat;
  }

  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) {
    return stat;
  }

  if (n == 0 && smt_easy_sat(core)) {
    stat = YICES_STATUS_SAT;
    set_smt_status(core, stat);
    return stat;
  }

  st = context_get_sat_delegate_state(ctx);
  if (exec_mode == SAT_DELEGATE_MODE_APPEND) {
    if (!context_prepare_append_delegate(ctx, st, sat_solver, verbosity)) {
      return YICES_STATUS_UNKNOWN;
    }
  } else {
    assert(exec_mode == SAT_DELEGATE_MODE_SELECTOR_FRAMES);
    if (!context_prepare_selector_delegate(ctx, st, sat_solver, verbosity)) {
      return YICES_STATUS_UNKNOWN;
    }
  }

  if (n > 0 && !delegate_supports_assumptions(&st->delegate)) {
    return YICES_STATUS_UNKNOWN;
  }

  init_ivector(&visible_failed, 0);
  ivector_reset(&st->assumptions);
  ivector_reset(&st->failed);
  if (exec_mode == SAT_DELEGATE_MODE_SELECTOR_FRAMES) {
    uint32_t k, d;
    d = smt_base_level(core);
    for (k=1; k<=d; k++) {
      if (k < st->size && st->act_var[k] != 0) {
        ivector_push(&st->assumptions, pos_lit(st->act_var[k]));
        ctx->sat_delegate_stats.selector_assumptions ++;
      }
    }
  }
  for (i=0; i<n; i++) {
    ivector_push(&st->assumptions, assumptions[i]);
  }

  if (st->assumptions.size == 0) {
    stat = st->delegate.check(st->delegate.solver);
  } else if (delegate_supports_assumptions(&st->delegate)) {
    stat = delegate_check_with_assumptions(&st->delegate, st->assumptions.size,
                                           (literal_t *) st->assumptions.data, &st->failed);
    if (stat == YICES_STATUS_UNSAT) {
      for (i=0; i<st->failed.size; i++) {
        literal_t l = st->failed.data[i];
        uint32_t j;
        for (j=0; j<n; j++) {
          if (l == assumptions[j]) {
            ivector_push(&visible_failed, l);
            break;
          }
        }
      }
      if (failed != NULL) {
        ivector_reset(failed);
        ivector_add(failed, visible_failed.data, visible_failed.size);
      }
    }
  } else {
    stat = YICES_STATUS_UNKNOWN;
  }

  set_smt_status(core, stat);
  set_delegate_assumption_state(core, n, assumptions, stat, &visible_failed);
  if (stat == YICES_STATUS_SAT) {
    context_import_delegate_model(core, &st->delegate);
  }
  st->checked_once = true;

  delete_ivector(&visible_failed);
  return stat;
}

static smt_status_t check_with_delegate_assumptions(context_t *ctx, const char *sat_solver, uint32_t verbosity,
                                                    uint32_t n, const literal_t *assumptions, ivector_t *failed);

smt_status_t check_with_sat_delegate(context_t *ctx, const char *sat_solver,
                                     sat_delegate_incremental_mode_t mode,
                                     uint32_t verbosity, uint32_t n,
                                     const literal_t *assumptions, ivector_t *failed) {
  switch (mode) {
  case SAT_DELEGATE_MODE_REBUILD:
    ctx->sat_delegate_stats.rebuild_checks ++;
    if (n == 0) {
      return check_with_delegate(ctx, sat_solver, verbosity);
    } else {
      return check_with_delegate_assumptions(ctx, sat_solver, verbosity, n, assumptions, failed);
    }

  case SAT_DELEGATE_MODE_APPEND:
    ctx->sat_delegate_stats.append_checks ++;
    return check_with_persistent_delegate(ctx, sat_solver, verbosity, SAT_DELEGATE_MODE_APPEND,
                                          n, assumptions, failed);

  case SAT_DELEGATE_MODE_SELECTOR_FRAMES:
    ctx->sat_delegate_stats.selector_frame_checks ++;
    return check_with_persistent_delegate(ctx, sat_solver, verbosity, SAT_DELEGATE_MODE_SELECTOR_FRAMES,
                                          n, assumptions, failed);

  default:
    return YICES_STATUS_UNKNOWN;
  }
}

/*
 * 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);
}

static void cache_failed_assumptions_core(context_t *ctx, uint32_t n, const term_t *a,
                                          const ivector_t *assumption_literals,
                                          const ivector_t *failed_literals) {
  ivector_t core_terms;
  int_hset_t failed;
  uint32_t i;

  init_ivector(&core_terms, 0);
  init_int_hset(&failed, 0);
  for (i=0; i<failed_literals->size; i++) {
    int_hset_add(&failed, failed_literals->data[i]);
  }
  for (i=0; i<n; i++) {
    if (int_hset_member(&failed, assumption_literals->data[i])) {
      ivector_push(&core_terms, a[i]);
    }
  }
  cache_unsat_core(ctx, &core_terms);
  delete_int_hset(&failed);
  delete_ivector(&core_terms);
}

/*
 * MCSAT variant of check_context_with_term_assumptions.
 * Caller must hold __yices_globals.lock.
 */
static smt_status_t _o_check_context_with_term_assumptions_mcsat(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;

  /*
   * 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 = _o_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) {
        interpolant = context_get_unsat_model_interpolant(ctx);
        assert(interpolant != NULL_TERM);
        core_from_labeled_interpolant(ctx, interpolant, &assumptions, &label_map, &mapped_core);
      }
    }

    if (pushed) {
      mcsat_cleanup_assumptions(ctx->mcsat);
      context_pop(ctx);
    }
    if (stat == YICES_STATUS_UNSAT) {
      mcsat_set_unsat_result_from_labeled_interpolant(ctx->mcsat, interpolant, n, assumptions.data, a);
      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;
  }
}

static smt_status_t check_context_with_term_assumptions_mcsat(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) {
  MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_mcsat(ctx, params, n, a, error));
}

/*
 * Supplemental-MCSAT variant for term assumptions in CDCL(T) mode.
 * We encode assumptions via fresh labels b_i with implications (b_i => a_i),
 * then solve under assumptions b_i = true.
 *
 * Labels are kept in the context (no push/pop) so the regular context status
 * and multicheck protocol remain unchanged.
 */
static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) {
  smt_status_t stat;
  ivector_t assumptions;
  term_t interpolant;
  uint32_t i;
  literal_t l;
  mcsat_satellite_t *sat;

  init_ivector(&assumptions, n);

  stat = YICES_STATUS_IDLE;
  interpolant = NULL_TERM;
  sat = NULL;

  if (ctx->mcsat_supplement_active &&
      ctx->egraph != NULL &&
      ctx->egraph->th[ETYPE_MCSAT] != NULL) {
    sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT];
  }

  for (i=0; i<n; i++) {
    l = context_add_assumption(ctx, a[i]);
    if (l < 0) {
      if (error != NULL) {
        *error = l;
      }
      stat = YICES_STATUS_ERROR;
      break;
    }

    ivector_push(&assumptions, l);
  }

  if (stat != YICES_STATUS_ERROR) {
    stat = check_context_with_assumptions(ctx, params, assumptions.size, (const literal_t *) assumptions.data);
    if (stat == YICES_STATUS_UNSAT) {
      if (sat != NULL) {
        interpolant = mcsat_satellite_compute_unsat_model_interpolant(sat, params, n, a);
      }
      if (interpolant == NULL_TERM && context_supports_model_interpolation(ctx)) {
        interpolant = context_get_unsat_model_interpolant(ctx);
      }
      if (interpolant == NULL_TERM && context_supports_model_interpolation(ctx)) {
        interpolant = false_term;
      }
    }
  }

  if (stat == YICES_STATUS_UNSAT && interpolant != NULL_TERM && sat != NULL) {
    mcsat_satellite_set_unsat_model_interpolant(sat, interpolant);
  }

  delete_ivector(&assumptions);

  return stat;
}

static smt_status_t check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) {
  MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_supplement(ctx, params, n, a, error));
}

/*
 * 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) {
  if (error != NULL) {
    *error = CTX_NO_ERROR;
  }

  /*
   * Clear any prior term-assumption core before all paths below. Delegate
   * checks cache a new core only on UNSAT.
   */
  context_invalidate_unsat_core_cache(ctx);

  if (ctx->mcsat == NULL) {
    if (ctx->mcsat_supplement_active) {
      return check_context_with_term_assumptions_supplement(ctx, params, n, a, error);
    }
    smt_status_t stat;
    sat_delegate_t mode;
    sat_delegate_incremental_mode_t exec_mode;
    bool one_shot;
    const char *delegate;
    bool unknown;
    ivector_t assumptions;
    ivector_t failed;
    uint32_t i;
    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);
    }

    mode = effective_sat_delegate_mode(ctx->sat_delegate, params, &one_shot);
    delegate = sat_delegate_name(mode);
    if (delegate == NULL) {
      stat = check_context_with_assumptions(ctx, params, n, assumptions.data);
      delete_ivector(&assumptions);
      return stat;
    }

    if (ctx->logic != QF_BV) {
      if (error != NULL) {
        *error = CTX_OPERATION_NOT_SUPPORTED;
      }
      delete_ivector(&assumptions);
      return YICES_STATUS_ERROR;
    }

    if (!supported_delegate(delegate, &unknown)) {
      if (error != NULL) {
        *error = unknown ? CTX_UNKNOWN_DELEGATE : CTX_DELEGATE_NOT_AVAILABLE;
      }
      delete_ivector(&assumptions);
      return YICES_STATUS_ERROR;
    }

    if (!delegate_supports_assumptions_name(delegate)) {
      if (error != NULL) {
        *error = CTX_OPERATION_NOT_SUPPORTED;
      }
      delete_ivector(&assumptions);
      return YICES_STATUS_ERROR;
    }

    init_ivector(&failed, 0);
    if (!effective_sat_delegate_incremental_mode(mode, ctx->sat_delegate_incremental_mode,
                                                ctx->sat_delegate_incremental_mode_set,
                                                ctx->mode == CTX_MODE_ONECHECK,
                                                one_shot, &exec_mode)) {
      if (error != NULL) {
        *error = CTX_OPERATION_NOT_SUPPORTED;
      }
      delete_ivector(&failed);
      delete_ivector(&assumptions);
      return YICES_STATUS_ERROR;
    }
    stat = check_with_sat_delegate(ctx, delegate, exec_mode, 0, n, assumptions.data, &failed);
    if (stat == YICES_STATUS_UNSAT) {
      cache_failed_assumptions_core(ctx, n, a, &assumptions, &failed);
    }
    delete_ivector(&failed);
    delete_ivector(&assumptions);
    return stat;
  }

  return check_context_with_term_assumptions_mcsat(ctx, params, n, a, error);
}

/*
 * 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));
        ctx->sat_delegate_stats.delegate_initializations ++;
        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;
}

/*
 * One-shot check with delegate and assumptions.
 * - assumptions are literals in core encoding.
 * - if failed != NULL and result is UNSAT, failed assumptions are appended to *failed.
 */
static smt_status_t check_with_delegate_assumptions(context_t *ctx, const char *sat_solver, uint32_t verbosity,
                                                    uint32_t n, const literal_t *assumptions, ivector_t *failed) {
  smt_status_t stat;
  smt_core_t *core;
  delegate_t delegate;

  core = ctx->core;

  stat = smt_status(core);
  if (stat != YICES_STATUS_IDLE) {
    return stat;
  }

  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) {
    return stat;
  }

  if (!init_delegate(&delegate, sat_solver, num_vars(core))) {
    return YICES_STATUS_UNKNOWN;
  }
  ctx->sat_delegate_stats.delegate_initializations ++;
  delegate_set_verbosity(&delegate, verbosity);

  stat = solve_with_delegate_assumptions(&delegate, core, n, assumptions, failed);
  set_smt_status(core, stat);
  set_delegate_assumption_state(core, n, assumptions, stat, failed);
  if (stat == YICES_STATUS_SAT) {
    context_import_delegate_model(core, &delegate);
  }

  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 ||
         (context_has_mcsat(ctx) && 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);
      }
    }
  }

  /*
   * Supplemental MCSAT values are an overlay: apply them after the regular
   * CDCL(T) model is fully built so nonlinear/FF values are not overwritten.
   */
  if (ctx->mcsat_supplement_active && context_has_egraph(ctx) && ctx->egraph->th[ETYPE_MCSAT] != NULL) {
    mcsat_satellite_build_model((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT], model);
  }
}


/*
 * 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) {
  if (ctx->mcsat != NULL) {
    return mcsat_get_unsat_model_interpolant(ctx->mcsat);
  }

  if (ctx->mcsat_supplement_active && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) {
    return mcsat_satellite_get_unsat_model_interpolant((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]);
  }

  if (context_supports_model_interpolation(ctx) &&
      ctx->core != NULL &&
      smt_status(ctx->core) == YICES_STATUS_UNSAT) {
    return false_term;
  }

  return NULL_TERM;
}

SRI-CSL / yices2 / 26150511973

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