Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

[disteph]

This is a first draft wrapping MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture.

As a Nelson-Oppen theory solver, it is a satellite theory of the e-graph. It completes the CDCL(T) theory support, aligning it with MCSAT's, by covering non-linear arithmetic and finite fields. Technically, the wrapper is called as the last theory solver, just before reconciliation and quantifiers, but after the simplex, so that the simplex has a chance to trigger a backjump without resorting to MCSAT. If we do end up calling MCSAT, it is on a conjunction of literals + equalities/disequalities from the e-graph, and if we get UNSAT, we extract a theory lemma by asking MCSAT to produce an unsat core (this integration relies on the recently added unsat core functionality of MCSAT).

The top-level MCSAT solver is unchanged.

In CDCL(T) mode, formulas that previously failed with FORMULA_NOT_LINEAR / CONTEXT_UNSUPPORTED_THEORY are now detected up front and routed to the dedicated MCSAT satellite context for consistency checking and conflict explanation.

Main Changes

• Added a supplementary MCSAT satellite module:
  • src/solvers/mcsat_satellite.c
  • src/solvers/mcsat_satellite.h
• Added trigger pre-scan for supplemental activation in CDCL(T):
  • finite-field constructs/types
  • ARITH_ROOT_ATOM
  • arithmetic nonlinear terms (degree > 1)
  • non-constant divisor div/mod/divides forms
• Wired a new egraph satellite kind and atom tag for MCSAT-tracked atoms.
• Routed unsupported atoms through the MCSAT satellite instead of old hard error paths when supplemental mode is active.
• Added supplemental check mode parameter:
  • mcsat-supplement-check = both | final-only (default both)
• Added model overlay plumbing so SAT model requests can include supplemental MCSAT values.
• Kept ctx->mcsat semantics pure-MCSAT-only; supplemental path is via egraph satellite state.
• Added SMT2 frontend --dpllt forcing and regression harness support for dual-mode runs in tests/regress/both.

CLI/Option Semantics

• --mcsat and --dpllt are now treated as mutually exclusive top-level architecture selectors in yices_smt2.
• Added debug assertions to catch internal misuse if both flags become true simultaneously.

Test/Regression Notes

• Added tests/regress/both/ scaffold and harness support to run selected tests under both modes.
• Expected behavior under forced CDCL(T):
  • MCSAT-only commands (e.g., check-sat-assuming-model, unsat-model interpolant requests) are rejected early.
  • UNSAT cores may differ from pure MCSAT cores.
  • Some benchmarks may time out in supplemental mode.

Scope / Draft Status

• This is a first draft focused on end-to-end wiring and behavior.
• Pure CTX_ARCH_MCSAT flow remains intact.
• Follow-up cleanup/tightening is expected after review (especially around regression selection and edge-case coverage).

[coveralls]

coverage: 66.728% (+0.2%) from 66.539%
when pulling 4003e85 on mcsat-supplement-cdclt
into 895707f on master.