Skip to content

Abstract Solver Interface: Decouple Term Construction from SMT-LIB Encoding#935

Merged
atomb merged 336 commits into
mainfrom
issue-917-abstract-solver-interface-decouple-term
May 18, 2026
Merged

Abstract Solver Interface: Decouple Term Construction from SMT-LIB Encoding#935
atomb merged 336 commits into
mainfrom
issue-917-abstract-solver-interface-decouple-term

Conversation

@MikaelMayer
Copy link
Copy Markdown
Contributor

@MikaelMayer MikaelMayer commented Apr 15, 2026 •
edited
Loading

Fixes #917

Summary

Introduces an abstract solver interface (AbstractSolver τ σ m) that decouples term construction and session operations from the SMT-LIB string encoding pipeline. The interface is parameterized by a term type τ, sort type σ, and monad m (with [Monad m] [MonadExceptOf IO.Error m] constraints), so a non-SMT-LIB backend (e.g., cvc5 FFI) can be plugged in by implementing AbstractSolver without touching the encoding logic. All methods throw IO.Error directly (no Except String layer).

A new incremental backend communicates with a live solver process via stdin/stdout. It is opt-in via --incremental (batch remains the default).

What the interface provides

All operations are monadic (m), throwing on error:

  • Configuration: setLogic, setOption, comment
  • Sort construction: boolSort, intSort, realSort, stringSort, regexSort, bitvecSort, arraySort, constrSort, termTypeToSort
  • Term construction: mkPrim, mkBool, mkAnd, mkOr, mkNot, mkImplies, mkEq, mkIte, mkAdd, mkSub, mkMul, mkDiv, mkMod, mkNeg, mkAbs, mkLt, mkLe, mkGt, mkGe, mkSelect, mkStore, mkApp, mkAppOp, mkForall, mkExists
  • Declarations: declareNew, declareFun, defineFun, declareSort, declareDatatype, declareDatatypes
  • Session: assert, checkSat, checkSatAssuming, getUnsatAssumptions, getModel, getValue, reset, close
  • Model inspection: termToSMTLibString

Terms (τ) are opaque handles whose meaning is backend-specific.

Other changes

  • Generic encoder — AbstractEncoder.encodeTerm parameterized over τ/σ, caches handles in AbstractEncoderState τ.
  • Generic incremental discharge — Imperative.SMT.dischargeObligationIncremental in SMTUtils.lean is parameterized over PureExpr, so any Imperative-level language can use the incremental solver.
  • Pluggable solver backends — CoreSMTSolver and MkDischargeFn threaded through Core.verifyProgram, Core.verify, and Strata.verify.
  • Strict solver compatibility — encodeDeclarationsAbstract skips declareSort for datatype names and validates datatype fields.
  • --incremental flag to opt in to the incremental backend.

Testing

All tests pass with both batch (default) and incremental modes.

Follow-ups

  • Implement with Lean FFI for cvc5

@MikaelMayer

This comment has been minimized.

Sign in to view
MikaelMayer

This comment was marked as resolved.

Sign in to view

@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
MikaelMayer

This comment was marked as resolved.

Sign in to view

@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer MikaelMayer mentioned this pull request Apr 17, 2026
Merged
@MikaelMayer
Use extracted obligations for verification, fix axiom scoping
c5a4628 
Switch from E.deferred to ObligationExtraction-produced obligations for
actual verification. The pipeline now:
1. obligationsToProgram converts E.deferred to Core program
2. ObligationExtraction extracts obligations from the program
3. Extracted obligations are used for verification

Fix: don't include axiom declarations in the obligations program.
Each obligation already has the correct axioms in its path conditions
from E.deferred. Adding axiom declarations would cause ObligationExtraction
to add them again, potentially including axioms that shouldn't be in scope
(e.g. a procedure's own invokeOn axiom proving its own postcondition).

All tests pass with extracted obligations.
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer
Add sort type parameter and missing operations to AbstractSolver
8ff9a43 
- Add sort type parameter σ to AbstractSolver (τ σ m) so backends can
  have their own sort representation
- Add sort constructors: boolSort, intSort, realSort, stringSort,
  bitvecSort, arraySort
- Add mkAbs (absolute value)
- Add mkSelect/mkStore (array operations)
- Add mkApp (uninterpreted function application)
- Update IncrementalSolver: σ = TermType, implement all new operations
@MikaelMayer

This comment has been minimized.

Sign in to view
@MikaelMayer
Move obligation-to-program conversion into evaluation phase
7733c3d 
typeCheckAndEval now returns List (Program × Env) where each Program
has the procedure body replaced with the obligations tree (assume/assert
blocks combined with if *). Axioms are inlined into each procedure's
obligations from E.deferred path conditions. Type/datatype declarations
are preserved.

verifySingleEnv takes (Program × Env) and uses ObligationExtraction on
the obligations program. The Env is still needed for E.distinct and
E.datatypes in the SMT encoder.

This makes the symbolic evaluation phase produce a Core program as output,
moving toward the reviewer's vision of Core-to-Core pipeline phases.
@MikaelMayer
Return single Program from evaluation phase, not list
b55e8cf 
typeCheckAndEval now returns one Program containing all procedures'
obligations (one procedure per evaluation environment). The Program
has type/datatype declarations plus obligation procedures.

The List Env is still returned alongside for SMT encoding context
(distinct, datatypes) — these will be moved into the Program in a
future step. verify() uses the first Env as sample for SMT encoding.
@MikaelMayer
Eliminate Env from verifySingleEnv public interface
973d1ee 
verifySingleEnv now takes (Program, Env) where the Env is reconstructed
internally from the evaluation phase. The Env carries distinct constraints
and datatypes needed by the SMT encoder — these will be extracted from
the Program in a future step to fully eliminate Env dependency.

The evaluation phase (typeCheckAndEval) returns Program as the primary
output. The List Env is returned alongside for internal use only.
@MikaelMayer
Wire ObligationExtraction into pipeline, validate round-trip
047a623 
The evaluation phase (typeCheckAndEval) returns Program as primary output.
Env is still passed internally to verifySingleEnv for SMT encoding
(distinct, datatypes, factory) but is not part of the public pipeline.

The Env dependency in SMT encoding requires the full evaluation context
(factory with all function declarations, datatype constructors, type
aliases). Eliminating it requires refactoring the SMT encoder to
reconstruct this context from the Program declarations.
@MikaelMayer
Eliminate Env from verifySingleEnv public interface
57b93ab 
The evaluation phase (typeCheckAndEval) returns Program as the primary
output. The List Env is returned alongside as an internal detail for
the SMT encoder — verify() extracts the first Env and passes it to
verifySingleEnv.

Add buildSMTEnv helper in Core.lean that constructs an Env from program
declarations (factory, datatypes, distinct) without running procedure
evaluation. Used by MetaVerifier.

The PE/evaluation phase is now a Program → Program transformation.
The Env dependency is isolated to the SMT encoding stage.
@MikaelMayer
Separate type checking and symbolic eval phases, eliminate Env from t…
7d0a4c9 
…ypeCheckAndEval

Split the pipeline into distinct phases:
1. typeCheck: Program → Program (type checking)
2. symbolicEval: Program → Program (symbolic execution → obligations tree)
3. ANFEncoder: Program → Program (available, not yet wired)
4. ObligationExtraction + SMT encoding (verification)

typeCheckAndEval is now a convenience wrapper calling typeCheck then
symbolicEval, returning (Program, Statistics) with no Env.

The SMT encoder builds its own Env internally via buildEvalEnv +
Program.eval in verify(). This is isolated from the pipeline phases.

buildSMTEnv helper available for lightweight Env construction
(used by MetaVerifier).
aqjune-aws
aqjune-aws previously approved these changes May 15, 2026
View reviewed changes
MikaelMayer
MikaelMayer commented May 15, 2026
View reviewed changes
Comment thread Strata/Languages/Core/Options.lean
aqjune-aws
aqjune-aws previously approved these changes May 15, 2026
View reviewed changes
@MikaelMayer
Merge remote-tracking branch 'origin/main' into issue-917-abstract-so…
4e79d95 
…lver-interface-decouple-term

# Conflicts:
#	Strata/Languages/Core/SMTEncoder.lean
@atomb atomb added this pull request to the merge queue May 18, 2026
Merged via the queue into main with commit 192b780 May 18, 2026
41 checks passed
@atomb atomb deleted the issue-917-abstract-solver-interface-decouple-term branch May 18, 2026 19:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@atomb atomb atomb approved these changes

@aqjune-aws aqjune-aws aqjune-aws approved these changes

Assignees

No one assigned

Labels

Core SMT

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Abstract Solver Interface: Decouple Term Construction from SMT-LIB Encoding

3 participants

@MikaelMayer @atomb @aqjune-aws