QF_BV context delegates (#453): config/param selection, incremental state, assumptions, and delegate regressions

[disteph]

This PR implements Level 1 and Level 2 of context-level SAT delegate support for QF_BV as laid out in #453.

• Adds delegate selection to search parameters (delegate) and context config (sat-delegate).
• Adds context config flag sat-delegate-selector-frames for incremental delegate frame handling.
• Routes yices_check_context through the selected delegate when applicable.
• Adds persistent delegate solver state for incremental delegates (cadical, cryptominisat) across checks.
• Adds delegate-based handling for yices_check_context_with_assumptions on QF_BV contexts.
• Keeps non-incremental delegates (y2sat, kissat) usable in config/params, but check-sat-assuming returns CTX_OPERATION_NOT_SUPPORTED.
• Updates SMT2 frontend so --delegate=... is applied through search params and works with incremental mode.
• Extends regress and API testing for delegate behavior.

Key Behavior

• No new public check-sat function was added.
• Delegate can be set in:
  • context config: sat-delegate
  • params: delegate (per-check override)
• Params override is treated as one-shot if it differs from context delegate.
• QF_BV guard is enforced for delegate use in context checks.
• sat-delegate-selector-frames is only relevant for incremental delegates and ignored for non-incremental delegates.
• check_context_with_assumptions:
  • cadical/cryptominisat: supported, with unsat-core mapping from failed assumptions.
  • y2sat/kissat: YICES_STATUS_ERROR + CTX_OPERATION_NOT_SUPPORTED.

Implementation Notes

• context_t now tracks:
  • selected delegate/config flag
  • mutation counter
  • lazily allocated delegate runtime state
• Delegate runtime state is cleaned on reset/delete and refreshed on context mutation.
• Added delegate-side hooks for:
  • assumptions solve
  • failed-assumptions extraction
  • variable growth for incremental usage
  • guarded clause export (for selector-frame mode)
• Fixed CryptoMiniSat failed-assumption normalization so unsat-core mapping is stable.

CLI and Regress

• Removed SMT2 CLI guard that previously blocked --incremental with --delegate.
• Added delegate-only regress modes and targets:
  • make delegate-regress
  • make static-delegate-regress
• Regress script now runs extra QF_BV delegate passes automatically when delegates are installed.
• Added a dedicated incremental y2sat regression case to validate non-incremental delegate behavior in incremental sessions.

Tests Run

• make check-api
  • Result: Total: 24, Pass: 24, Fail: 0
• make delegate-regress
  • Result: Pass: 249, Fail: 0

Scope

• This PR covers Level 1 and Level 2 for QF_BV contexts.
• Level 3 (mixed-theory delegate integration with incrementality) is out of scope.

[coveralls]

coverage: 67.254% (+0.03%) from 67.22% — context_delegates into master

[disteph]

Context-level QF_BV delegates (Levels 1 and 2 of #453)

Summary

This PR lifts Yices' existing third-party SAT-solver (delegate) support out of the one-shot yices_check_formula[s] API and into the regular context API, so that a delegate can be used for every variant of check-sat on a QF_BV context — including incremental use (push/pop, multiple check-sat calls) and checking under assumptions with unsat-core extraction.

Closes issue #453, Levels 1 and 2 (configurable SAT back-end per context, with and without incrementality). Level 3 of #453 (mixed-theory contexts with external SAT back-end) remains out of scope for this PR.

What's new for users

1. sat-delegate context-configuration option (API + SMT2 frontend)

A QF_BV context can now be bound to a specific SAT back-end at construction time:

ctx_config_t *cfg = yices_new_config();
yices_default_config_for_logic(cfg, "QF_BV");
yices_set_config(cfg, "mode", "push-pop");
yices_set_config(cfg, "sat-delegate", "cadical");   /* <-- new */
context_t *ctx = yices_new_context(cfg);
yices_free_config(cfg);

Accepted values: "none" (default), "y2sat", "cadical", "cryptominisat", "kissat".

Any subsequent yices_check_context, yices_check_context_with_assumptions, or yices_check_context_with_model call now bit-blasts the bit-vector problem to CNF as before, but hands the resulting CNF to the selected delegate instead of the internal Yices CDCL SAT solver. Bit-blasting itself, and the smt-core's clause set, are unchanged — the only change is which SAT engine consumes them.

2. sat-delegate-selector-frames context-configuration option

yices_set_config(cfg, "sat-delegate-selector-frames", "true");

Controls how push/pop is realised against the delegate:

• "false" (default): on every mutation (new assertion, push, pop), the delegate is rebuilt from the current bit-blasted problem. Simpler, works with every delegate, loses learned clauses between checks.
• "true": the delegate is kept live across checks; each incremental frame's clauses are guarded by a fresh selector literal. Pops retract by switching selectors. Preserves learned clauses; supported by incremental back-ends only.

Ignored for non-incremental delegates.

3. delegate per-check parameter

The same back-ends can be selected (or overridden one-shot) via a param_t:

param_t *p = yices_new_param_record();
yices_set_param(p, "delegate", "y2sat");
smt_status_t s = yices_check_context(ctx, p);

Intended for one-off experiments: a delegate value in param_t that differs from the context's configured sat-delegate forces a one-shot rebuild for that check and does not mutate the persistent delegate state of the context.

4. --incremental --delegate=<solver> in yices-smt2

Previously, the --delegate= CLI option was silently ignored under --incremental. It now routes every (check-sat) through the selected delegate. For y2sat and Kissat (non-incremental) this means the delegate is rebuilt per check; for CaDiCaL and CryptoMiniSat the incremental path is used.

Delegate capability matrix

Delegate	Availability	Incremental push/pop	check-sat-assuming	Unsat core from assumptions
y2sat	always	rebuild per check	rebuild per check	—
kissat	optional (build flag)	rebuild per check	rebuild per check	—
cadical	optional (build flag)	yes (selector frames)	yes	yes
cryptominisat	optional (build flag)	yes (selector frames)	yes	yes

yices_has_delegate("<name>") returns 1 if the current Yices build includes the back-end.

Assumptions and unsat cores

yices_check_context_with_assumptions now works with a configured delegate:

• For cadical/cryptominisat, the delegate's native assumption interface is used; the unsat core is filtered back into the caller's term space and accessible via yices_get_unsat_core.
• For y2sat/kissat, the delegate is rebuilt with the assumptions included; no unsat-core extraction (the error MCSAT_ERROR_... path is unchanged from before).

Model import

On SAT, the delegate's boolean model is imported into the smt-core so that yices_get_model / yices_formula_true_in_model work exactly as they do for the native solver.

Non-goals / limitations

• Logics other than QF_BV: the delegate is only consulted when the context has been configured for QF_BV. For any other logic, sat-delegate is ignored (and yices_check_context returns the usual error if the param-level delegate is set on a non-QF_BV context). Mixed-theory delegate support (Level 3 of Feature request: making delegates available when solving from a Yices context #453) is not in this PR.
• Selector-frames mode re-feeds the full clause set on each mutation. It preserves the delegate's learned clauses (this is the win), but the input CNF is replayed on each push/assert — no clause-delta plumbing between the smt-core and the delegate. Users of very large incremental problems should benchmark both sat-delegate-selector-frames=true and =false against the native solver.
• DIMACS export unchanged — the existing yices-smt2 --dimacs=... --delegate=y2sat behaviour is preserved.

Implementation notes

• New file: src/api/search_parameters.{h,c} gains shared helpers sat_delegate_name, parse_sat_delegate, effective_sat_delegate_mode (used by both context_config and context_solver).
• New functions: check_with_incremental_delegate (selector-frames path) and context_prepare_incremental_delegate in src/context/context_solver.c. Persistent state is held in delegate_state_t, lifecycle-managed by the context (delete_context, reset_context, push/pop).
• Generalised clause export: the existing copy_problem_clauses is refactored into the public add_problem_clauses_to_delegate(delegate, core, guard_literal) so the one-shot and the selector-frames paths share the export code.
• New capability hooks on delegate_t: check_assuming, collect_failed_assumptions, add_vars. Predicates incremental_delegate(...) and delegate_supports_assumptions(...) provide uniform dispatch.

Tests

tests/api/context_delegate.c is the main new test file. It parameterises every case over every delegate installed in the current build:

• One-shot SAT / UNSAT shapes (bvadd, bvand, extract, concat).
• Push/pop incremental, nested push/pop, branching push/pop.
• sat-delegate via config and via per-check param.
• sat-delegate-selector-frames="true" with growing CNF variable count across checks, and with assumptions.
• Failed-assumption → unsat-core mapping under cadical and cryptominisat.
• Negative cases: unknown delegate name, delegate not compiled in, wrong logic (QF_LIA).
• Interaction with assert_formula_true_in_context_model on every SAT case.

Regression integration: tests/regress/check.sh now opportunistically re-runs every QF_BV regression under each installed delegate (filtered by is_qf_bv_delegate_candidate to skip tests that depend on model/core printing). New top-level targets: make delegate-regress and make static-delegate-regress.

Follow-up documentation

• User manual (doc/manual/manual.tex): expand §"Third-Party SAT Solvers" and the --delegate option paragraph to describe the new API-level configuration, the selector-frames option, and the capability matrix above.
• Website (doc/sphinx/source/): add rows for sat-delegate and sat-delegate-selector-frames in the configuration table in context-operations.rst, add a delegate entry in parameters.rst, and cross-reference from formula-operations.rst.
• yices.h: expand the comment blocks at the declarations of yices_set_config and yices_set_param so the header carries the same capability matrix.

[disteph]

Code Review by Codex/GPT5.5 : context_delegates including 29fc55e against master

Findings

No blocking or non-blocking findings.

Open Questions

None blocking.

The selector-frame path intentionally preserves delegate solver state and learned clauses while re-feeding the full current clause set under a fresh selector after each mutation. The docs describe this as selector-guarded incremental delegate behavior rather than true clause-delta incrementality, which is accurate.

Summary

The PR is correctly scoped for QF_BV context delegates. It adds per-check delegate selection via search parameters and persistent context-configured delegates, with selector-frame support for incremental CaDiCaL/CryptoMiniSat use and rebuild semantics for y2sat/Kissat.

The delegate abstraction is clean: solver capabilities such as assumptions, failed-assumption collection, dynamic variable addition, and clause export are represented explicitly instead of being inferred ad hoc. The shared delegate parsing/name/effective-selection helpers remove duplicate control flow between API and context code.

The correctness-sensitive paths look sound: selector variables are kept beyond real core variables, failed assumption cores filter out the internal selector literal, delegate state is cleaned up on reset/delete, and mutation counts are updated on assertion, push/pop, and blocking-clause changes.

Test coverage is strong. tests/api/context_delegate.c covers one-shot SAT/UNSAT, push/pop, nested and branching push/pop, configured delegates, rebuild mode, selector-frame growth, selector-frame assumptions, model agreement, wrong-logic errors, unavailable delegates, and unsupported assumption delegates. The regression harness also keeps delegate fan-out available through explicit opt-in modes.

Tests Run

Not run for this rewrite; worktree was left untouched.