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

[disteph]

Summary

This branch extends the CDCL(T) solver so it can use MCSAT as an E-graph satellite for arithmetic and finite-field constraints that are outside the simplex solver’s supported fragment.

The main goal is to let CDCL(T) contexts handle nonlinear arithmetic and finite-field arithmetic by delegating the relevant theory checks to an internal MCSAT satellite, while preserving the existing simplex-based CDCL(T) behavior when the supplement is not enabled.

With this PR, the top-level CDCL(T) and MCSAT solvers are essentially covering the same theories / logics: MCSAT can still be used as the top-level solver, while CDCL(T) can now call on MCSAT internally for the fragments it could not previously cover directly. This motivates the symmetric CLI controls: --mcsat forces top-level MCSAT, and --dpllt forces top-level CDCL(T).

This branch adds:

• A supplemental MCSAT satellite owned by the E-graph/CDCL(T) solver, separate from ctx->mcsat.
• Cube-based MCSAT checking from the current CDCL(T) assignment.
• Nonlinear arithmetic and finite-field atom routing to the satellite.
• Observation of linear arithmetic atoms and E-graph arrangement facts by the satellite.
• Simplex relaxation of nonlinear arithmetic atoms, so simplex can still cheaply find some conflicts before MCSAT runs.
• Thread-safety protection around the internal MCSAT calls made by the satellite.
• API and SMT2 test coverage for CDCL(T)+MCSAT supplement behavior.

Objectives And Constraints

The immediate objective of this PR is to extend CDCL(T) with supplemental support for theory fragments currently handled by MCSAT, without changing pure MCSAT mode or the default simplex-only CDCL(T) behavior.

Design constraints:

• Pure MCSAT mode remains unchanged.
• ctx->mcsat keeps its existing meaning: it is used only for pure CTX_ARCH_MCSAT.
• Supplemental MCSAT owns its own internal MCSAT state/context.
• CDCL(T)+simplex behavior remains equivalent to master when the supplement is not configured.
• No recursive assertion pre-scan or other extra term traversal is added to the normal simplex-only hot path.
• MCSAT is used as a theory/satellite checker, not as the top-level Boolean search engine.
• The MCSAT satellite works from the current CDCL(T) assignment cube.
• Conflicts learned from MCSAT are explainable back to CDCL(T).

A secondary design consideration is compatibility with possible future work where the E-graph could host multiple arithmetic-capable satellites with different cost/expressivity tradeoffs. For example, a future difference-logic satellite could detect cheap IDL/RDL conflicts before simplex, while MCSAT handles nonlinear or finite-field constraints after cheaper solvers have had a chance to run. This PR does not require or implement that broader architecture; it just avoids making that direction harder.

Configuration And User-Facing Behavior

This PR adds CDCL(T)-side support for using MCSAT internally as a supplement.

The SMT2 frontend now supports symmetric top-level solver selection:

• --mcsat forces the top-level MCSAT solver.
• --dpllt forces the top-level CDCL(T) solver.
• The two options are mutually exclusive.

This symmetry matters more after this PR because both top-level solvers now cover essentially the same logics: MCSAT covers them directly, while CDCL(T) covers them by combining its existing E-graph/simplex machinery with the supplemental MCSAT satellite.

When CDCL(T) is selected for a logic whose default architecture would normally be MCSAT, the CDCL(T) context can be built with the MCSAT supplement enabled. This lets CDCL(T) delegate nonlinear and finite-field consistency checks to the satellite.

The API configuration also supports explicit control of the supplement. Explicitly disabling the supplement while forcing CDCL(T) for a logic that requires MCSAT support is rejected as an invalid configuration.

Architecture

Separate MCSAT State

The supplemental solver is not stored in ctx->mcsat.

Instead, the CDCL(T) context attaches an MCSAT satellite to the E-graph. The satellite owns its own internal MCSAT context/state. This avoids changing the meaning of existing ctx->mcsat != NULL checks elsewhere in the codebase.

Pure MCSAT mode still uses the existing CTX_ARCH_MCSAT path.

Cube-Based MCSAT Checking

The satellite registers the atoms and arrangement facts that CDCL(T)/E-graph need it to check. At check time, it builds a cube from the current CDCL(T) assignment:

• For a tracked atom A, the satellite creates labels for the positive and negative polarity.
• If the CDCL(T) literal for A is true, the positive label is assumed.
• If the literal is false, the negative label is assumed.
• Unassigned atoms are not included in the cube.
• E-graph equalities, disequalities, and distinct facts are also label-guarded and included when active.

MCSAT is then called on this labeled cube.

This means CDCL(T) remains responsible for Boolean search, while MCSAT checks consistency of the active theory cube.

Atom Ownership And Observation

The branch distinguishes between atom ownership and observation.

For atoms that simplex can handle exactly:

• The atom remains simplex-owned.
• It keeps the normal arithmetic atom tag.
• The MCSAT satellite observes the atom and its CDCL(T) literal.
• MCSAT can include the atom in its cube if needed, but simplex remains the primary solver for it.

For atoms outside simplex’s supported fragment:

• The atom is routed to the MCSAT satellite.
• The satellite owns the CDCL(T) atom through a dedicated MCSAT atom tag.
• Simplex is not asked to internalize unsupported nonlinear or finite-field atoms directly.

This avoids asking simplex to internalize power products or finite-field constructs that would normally raise unsupported-theory or nonlinearity errors.

Arithmetic Observer Interface

This branch adds an arithmetic observer path in the E-graph.

The observer path lets supplemental arithmetic-capable satellites receive:

• Arithmetic term registrations.
• Arithmetic atom/literal observations.
• E-graph equality notifications.
• E-graph disequality notifications.
• E-graph distinct notifications.

The MCSAT satellite uses this path to receive arrangement facts and mappings from E-graph theory variables back to terms. The interface is deliberately narrow: observers receive notifications, and conflicts are reported through their normal propagate/final_check callbacks.

Observers are notification-only. They do not report immediate conflicts through the equality/disequality notification return values.

Check Order

Simplex still runs before MCSAT. If simplex finds a conflict, the search can learn that conflict without invoking MCSAT. If simplex does not find a conflict, MCSAT is run to validate the nonlinear/finite-field portion of the active cube.

This keeps the cheaper existing arithmetic solver in front of the more expressive supplemental solver.

Conflict Learning

MCSAT conflicts are converted into CDCL(T) clauses.

The satellite uses labels to relate MCSAT assumptions back to CDCL(T) literals and E-graph explanations. When MCSAT reports unsat, the satellite extracts the relevant labels from the MCSAT conflict/interpolant and expands them to CDCL(T)-level antecedents.

For E-graph arrangement facts, the satellite stores enough information to ask the E-graph for the explanation of an equality/disequality when needed.

If the MCSAT interpolant contains internal Boolean structure that is not one of the public labels, the implementation falls back to a sound active-cube clause. This is less precise than the ideal label-only explanation, but still sound. Debug assertions are present to catch genuinely unexpandable labels.

Model Construction

CDCL(T) model construction still happens first.

After the standard CDCL(T)/simplex model is built, the MCSAT satellite can overlay missing values needed for nonlinear arithmetic or finite-field terms. The overlay does not change the Boolean assignment chosen by CDCL(T), and it does not overwrite values already assigned by the CDCL(T)+simplex model.

The model path is tested with nonlinear arithmetic examples where the value of a nonlinear term must come from the MCSAT side rather than from the simplex relaxation.

Simplex Relaxation Of Nonlinear Arithmetic

This branch also adds a simplex relaxation layer for MCSAT-owned nonlinear arithmetic atoms.

The idea is:

• If an atom contains nonlinear subterms such as (* x y), the exact atom is still owned by MCSAT.
• A relaxed linear approximation is also created for simplex.
• Unsupported nonlinear subterms are replaced by fresh abstraction terms.
• The original MCSAT atom literal and the relaxed simplex atom literal are tied by equivalence clauses scoped with the atoms.

For example, an atom like this:

(>= (+ (* x y) x) 1)

can be relaxed for simplex as:

(>= (+ p_xy x) 1)

where p_xy is an internal abstraction for (* x y).

The relaxation is an over-approximation:

• If simplex proves the relaxed cube unsat, that conflict is sound for the original problem.
• If simplex says the relaxed cube is sat, that result is not final.
• MCSAT still checks the exact cube.

This lets simplex cheaply detect some conflicts involving nonlinear atoms without making simplex responsible for nonlinear arithmetic semantics.

The abstraction cache is canonicalized by normalized term, so equivalent products such as (* x y) and (* y x) share the same abstraction.

Relaxation abstraction terms are internal implementation details and are not exported as user-visible model values.

Thread Safety

Full top-level MCSAT check-sat calls are protected by the global Yices mutex.

This branch adds equivalent protection around the internal MCSAT operations performed by the supplemental satellite, without locking the whole CDCL(T) check-sat path.

The satellite obtains/releases the global Yices mutex around calls into the internal MCSAT engine, including:

• MCSAT assertion into the internal satellite context.
• MCSAT push/pop.
• MCSAT solve/status/conflict extraction.
• MCSAT model overlay construction.
• MCSAT interpolation-related calls.
• MCSAT GC marking.

To support this safely when the caller already owns the global lock in some paths, the global lock is now initialized as a recursive mutex.

On POSIX this uses PTHREAD_MUTEX_RECURSIVE. On Windows this delegates to CRITICAL_SECTION, which is already recursive for the owning thread.

The CDCL(T) check-sat path itself is not globally locked.

Error Handling

The branch preserves the existing error behavior when the supplement is not configured.

In particular:

• The normal simplex-only CDCL(T) path does not run the new MCSAT routing predicate.
• Unsupported constructs still reach the same error paths as on master.
• Literal division-by-zero policy is not changed by this branch.
• If the supplement is configured, unsupported nonlinear/finite-field atoms are routed to MCSAT rather than causing simplex internalization errors.

The branch also fixes/maintains configuration validation around incompatible top-level solver selections.

Tests

The branch adds and updates tests covering:

• API construction of CDCL(T) contexts with the MCSAT supplement.
• Rejection of invalid configurations that force CDCL(T) while explicitly disabling a required supplement.
• Nonlinear arithmetic SAT/UNSAT behavior through CDCL(T)+MCSAT supplement.
• Finite-field API coverage through the supplemental path.
• SMT2 --dpllt behavior on nonlinear arithmetic.
• Cube-based behavior where MCSAT must refute a mixed linear/nonlinear conflict.
• Incremental push/pop behavior.
• Model construction and nonlinear term value retrieval.
• Simplex relaxation canonicalization.
• Cases where simplex relaxation is satisfiable but the exact MCSAT cube is unsatisfiable.
• Regression behavior for pure MCSAT mode and existing CDCL(T) paths.

Validation run locally included:

git diff --check
make -j4
./build/arm-apple-darwin23.6.0-release/bin/test_cdclt_mcsat_supplement
./build/arm-apple-darwin23.6.0-release/bin/yices_smt2 --dpllt tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2
make check

with make check reporting:

Pass: 1721
Fail: 0

Notes And Follow-Up Work

Potential follow-ups include:

• Choosing a smaller architecture than CTX_ARCH_EGFUNSPLXBV for some supplement-enabled logics.
• Tightening relaxation through arithmetic ITEs instead of abstracting some ITE-containing terms coarsely.
• Improving MCSAT conflict extraction to avoid the active-cube fallback when MCSAT interpolants contain internal Boolean structure.
• Extending the arithmetic observer framework to other arithmetic satellites if we decide to pursue a broader multi-satellite arithmetic architecture.
• Refining solver-selection documentation around combinations of CDCL(T), MCSAT supplement, simplex, and possible future arithmetic satellites.

[coveralls]

coverage: 68.878% (+0.09%) from 68.786% — mcsat-supplement-cdclt into master

[disteph]

Review of PR #611 by Windsurf/Opus4.7: MCSAT supplement for CDCL(T)

Baseline: master at the merge base. Reviewed branch: mcsat-supplement-cdclt at commit cbe97450.

Summary

This PR adds a cube-only MCSAT theory checker as an E-graph satellite inside CDCL(T). The high-level architecture is sound and the implementation is coherent:

• CDCL(T) remains responsible for Boolean search.
• Existing satellites continue to own their supported fragments.
• Nonlinear arithmetic, finite-field atoms, root atoms, and non-constant divisor sites are routed to a supplemental MCSAT satellite.
• Linear arithmetic atoms remain simplex-owned but are observed by the MCSAT satellite so the satellite can build a consistent cube.
• MCSAT checks the active CDCL(T) assignment cube through labeled assumptions.
• Optional simplex relaxation gives simplex an over-approximation of nonlinear arithmetic atoms, while MCSAT remains authoritative for the exact atom.
• The embedded MCSAT engine is serialized with the global Yices mutex without locking the whole CDCL(T) search loop.

I found no soundness blockers. The points below are quality, documentation, and follow-up coverage.

What The PR Adds

The main additions are:

• src/solvers/mcsat_satellite.{c,h}: the supplemental cube-only MCSAT satellite.
• src/context/context.c: atom routing, MCSAT observation hooks, simplex relaxation, and context lifecycle wiring.
• src/context/context_solver.c: CDCL(T) check paths that account for the supplement.
• src/solvers/egraph/*: a new ETYPE_MCSAT satellite slot, MCSAT_ATM_TAG, attach/detach support, and arithmetic observer fan-out.
• src/api/context_config.{c,h}: the mcsat-supplement context configuration.
• src/api/search_parameters.{c,h}: the mcsat-supplement-check parameter.
• src/frontend/yices_smt2.c and src/frontend/smt2/smt2_commands.{c,h}: --dpllt frontend support and supplement attachment when CDCL(T) is forced for MCSAT-default logics.
• src/mt/yices_locks_{posix,win}.c and src/mt/yices_locks.h: recursive global-lock support.
• tests/api/test_cdclt_mcsat_supplement.c: API coverage for nonlinear arithmetic, finite fields, push/pop, assumptions, model construction, simplex relaxation, and reset/reassert behavior.
• tests/regress/both/mcsat_supplement_qf_nia_unsat.smt2: SMT2 regression for --dpllt on a nonlinear arithmetic case requiring the supplement.

Configuration And User-Facing Surface

The configuration surface is well-structured:

• solver-type=mcsat rejects mcsat-supplement=true.
• solver-type=dpllt can enable the supplement for logics whose default backend is MCSAT.
• Explicitly setting mcsat-supplement=false while forcing CDCL(T) for a logic that requires the supplement is rejected.
• --mcsat and --dpllt are mutually exclusive SMT2 frontend flags.
• --dpllt forces CDCL(T) as the top-level solver, but does not imply “no MCSAT”: for logics such as QF_NIA, MCSAT may be attached as a CDCL(T) satellite.

The new mcsat-supplement-check parameter provides useful control over whether the supplement runs both during propagation and final check, or final-check only.

Remaining Notes

• mcsat_supplement_arch_for_logic returns CTX_ARCH_EGFUNSPLXBV for every supplement-enabled logic. This is safe but over-provisioned. A follow-up could choose lighter architectures for logics that exclude UF, arrays, or BV.
• The CLI/help documentation should make clear that --dpllt chooses the top-level CDCL(T) engine; it does not necessarily disable internal use of MCSAT as a satellite.

Atom Routing And Observation

The routing design is solid:

• context_atom_requires_mcsat only applies to Boolean atomic forms.
• The trigger covers finite-field constructs/types, ARITH_ROOT_ATOM, non-constant divisors, and arithmetic nonlinearity.
• Linear arithmetic atoms stay simplex-owned and are registered with the MCSAT satellite only as observations.
• MCSAT-owned atoms receive a dedicated E-graph atom tag.
• Arithmetic E-graph facts are delivered to observers through a notification-only observer interface.

The ownership-vs-observation split is the right design choice. It lets simplex keep doing cheap exact linear reasoning while MCSAT checks the harder exact cube.

Follow-Up Performance Notes

These are not merge blockers:

• context_atom_requires_mcsat allocates and frees a temporary int_hmap_t per atom. A context-level cache or reusable scratch object could reduce overhead in supplement-enabled contexts.
• The bvsum traversal path allocates a temporary bit-vector array only to satisfy the bvsum_term_component signature. A reusable scratch buffer would avoid repeated allocation.

Simplex Relaxation

The simplex relaxation layer is a useful optimization:

• Nonlinear subterms are replaced by fresh internal arithmetic abstraction terms.
• The exact MCSAT atom and relaxed simplex atom are linked by two binary clauses.
• The relaxation is an over-approximation: simplex UNSAT is sound, but simplex SAT is not final; MCSAT still checks the exact cube.
• Abstractions are canonicalized by normalized term, so equivalent products such as (* x y) and (* y x) share the same abstraction.
• Relaxation variables are not reported back to MCSAT as user arithmetic terms.
• Model tests confirm that exact nonlinear term values come from the MCSAT model overlay, not from the simplex abstraction.

The implementation correctly falls back to MCSAT-only ownership when no sound relaxation is available.

Follow-Up Precision Note

Arithmetic ITEs and some opaque arithmetic constructs are relaxed coarsely by abstracting the whole term. This is sound but may lose precision. A future improvement could recursively relax supported substructure inside those terms.

Finite-field atoms have no useful simplex relaxation and remain MCSAT-only, which is the correct policy.

MCSAT Satellite

The satellite implementation has the right shape:

• It owns a thin internal CTX_ARCH_MCSAT context over the shared term table.
• Each tracked atom gets positive and negative Boolean labels.
• Arrangement facts get their own labels.
• The current CDCL(T) assignment is converted into an MCSAT assumption cube.
• MCSAT conflicts are expanded back to CDCL(T) literals or E-graph explanations.
• If precise label expansion is not possible, the code falls back to a sound active-cube clause when possible; if expansion still fails, the satellite returns UNKNOWN rather than learning an unsound conflict.
• internal_error returns UNKNOWN, and scoped errors are cleared on pop when the failing assertion has been removed.
• Push/pop/reset/clear lifecycle handling is present and covered by API tests.
• The model overlay updates existing model entries where needed, which is necessary because CDCL(T) model construction runs first.

The active-cube conflict fallback can produce large clauses on difficult instances. That is a performance/quality concern, not a soundness issue.

E-Graph Integration

The E-graph integration is clean:

• ETYPE_MCSAT adds a dedicated satellite slot.
• MCSAT_ATM_TAG dispatches MCSAT-owned atoms.
• egraph_attach_mcsat_solver and detach support follow existing satellite patterns.
• The arithmetic observer interface is separate from full theory-solver ownership, which keeps observation-only satellites from masquerading as primary arithmetic solvers.
• MCSAT final check runs after the existing cheaper satellites, so simplex and other solvers can report conflicts first.

Compatibility Notes

• MCSAT_ATM_TAG = 3 consumes the last value in the 2-bit atom-tag space. Further atom tags will require widening the tag mask.
• Adding ETYPE_MCSAT shifts internal E-graph enum values. If these headers are treated as externally consumed, this should be noted in release notes or changelog material.

Thread Safety

The thread-safety policy is coherent:

• The global Yices lock is recursive.
• Satellite calls into the embedded MCSAT engine are protected by the global lock.
• Satellite-side term construction reachable from unlocked CDCL(T) search is also protected.
• CDCL(T) search itself remains unlocked, preserving the existing search-loop policy.
• The supplement check wrapper intentionally does not MT_PROTECT the full CDCL(T) check path; the satellite protects only the embedded MCSAT operations.

This relies on the existing Yices invariant that internalized term-table reads during CDCL(T) search are safe while other threads may append under the global lock. The PR does not make that invariant worse; it serializes the new MCSAT mutations that the supplement introduces.

A multi-threaded stress test with two independent supplement-enabled contexts would be a useful follow-up, but I do not consider it required for this PR.

Error Handling

The error-handling behavior is sound:

• Unsupported supplement construction paths are rejected as invalid configurations.
• Pure MCSAT mode remains separate from supplemental MCSAT mode.
• The normal simplex-only CDCL(T) path still reaches the existing unsupported-theory/nonlinearity errors when the supplement is not configured.
• Literal division-by-zero behavior is preserved.
• Internal MCSAT assertion failures produce UNKNOWN, not an unsound empty conflict.

One possible follow-up is to introduce a distinct external error code for the new internalization case that maps to MCSAT_ERROR_UNSUPPORTED_THEORY. The aliasing is acceptable but less informative to API users.

Tests

The API test coverage is strong. It covers:

• Nonlinear arithmetic SAT/UNSAT/model behavior.
• Hidden nonlinear products and push/pop.
• Non-constant divisor handling.
• Both mcsat-supplement-check modes.
• Finite-field SAT/UNSAT/model behavior.
• Assumption-core extraction for finite fields and nonlinear arithmetic.
• Simplex relaxation canonicalization.
• Cases where the relaxation is satisfiable but the exact MCSAT cube is unsatisfiable.
• Exact model values for nonlinear products.
• Literal division-by-zero preservation.
• Invalid configuration rejection.
• Reset/reassert lifecycle behavior.

The SMT2 regression coverage is minimal but meaningful: it exercises a nonlinear arithmetic case through --dpllt that requires the supplement.

Useful follow-up tests:

• SAT + get-value in tests/regress/both.
• Push/pop regression in SMT2.
• QF_NRA/root-atom coverage.
• QF_FF coverage.
• Non-constant divisor regression.
• Multi-threaded API stress test.
• A case that forces conflict expansion through E-graph equality explanations rather than direct source literals.

Open Questions / Follow-Ups

These do not block merge, but are worth tracking:

1. Should mcsat_supplement_arch_for_logic choose smaller architectures per logic instead of always using CTX_ARCH_EGFUNSPLXBV?
2. Should the new internalization error map to a distinct public error code rather than aliasing MCSAT_ERROR_UNSUPPORTED_THEORY?
3. Should SMT_ALL with quantifiers be allowed to attach the supplement, given that other quantified logics are rejected by the support predicate?
4. Should the E-graph enum shift and new CLI/config options be documented in NEWS/CHANGELOG?
5. Should routing-predicate scratch state be hoisted to reduce repeated allocation?

Verdict

The PR is mergeable.

The main architectural choices are sound:

• MCSAT is a separate supplemental satellite, not ctx->mcsat.
• CDCL(T) remains the top-level Boolean search engine.
• MCSAT checks the active assignment cube, not the full Boolean problem.
• Linear arithmetic remains simplex-owned and MCSAT-observed.
• Nonlinear and finite-field atoms are routed to MCSAT.
• Simplex relaxation is an over-approximation with MCSAT as the exact authority.
• Thread safety is handled at the satellite/MCSAT boundary without globally locking the CDCL(T) search loop.

I found no soundness blockers. The remaining items are performance, documentation, and additional regression coverage that can be handled as follow-ups.