Abstract Solver Interface

Defines AbstractSolver τ σ m, a generic solver interface parameterized by an opaque term type τ, an opaque sort type σ, and a monad m. All operations that can fail throw IO.Error via MonadExceptOf. The monad m captures any state or effects the backend needs.

For the incremental SMT-LIB backend, τ = SMT.Term, σ = SMT.TermType, m = StateT IncrementalSolverState IO.

Design

• declareNew allows shadowing: declaring the same name twice creates two distinct variables. The backend handles disambiguation internally.
• Models return keys as (String × Nat) where Nat is the shadow depth (0 = most recently declared).
• Quantifier bound variables are scoped via a callback pattern.
• Terms (τ) are opaque handles whose meaning is backend-specific. They may be internal addresses and should not be assumed valid across sessions.
• Sorts are first-class: backends can create and pass their own sort representations via intSort, boolSort, bitvecSort, arraySort, etc.

structure Strata.SMT.DatatypeConstructorHandles (τ : Type) : Type

Handles for a single datatype constructor returned by declareDatatype.

• constr is the constructor function (use with mkApp to build values)
• tester is the recognizer predicate (use with mkApp to test membership)
• selectors are the field accessors in declaration order

• constr : τ
• tester : τ
• selectors : List τ

structure Strata.SMT.DatatypeInfo (τ σ : Type) : Type

Result of declaring a datatype: the sort and handles for each constructor.

• sort : σ
• constructors : List (DatatypeConstructorHandles τ)

structure Strata.SMT.AbstractSolver (τ σ : Type) (m : Type → Type) [Monad m] [MonadExceptOf IO.Error m] : Type

Abstract solver interface parameterized by term type τ, sort type σ, and monad m.

All term constructors are fallible. Solvers might not accept certain constructs (e.g., wrong sorts, unsupported combinations) and we need to surface the issue precisely via MonadExceptOf IO.Error.

• setLogic : String → m Unit
• setOption : String → String → m Unit
• comment : String → m Unit
• boolSort : m σ
• intSort : m σ
• realSort : m σ
• stringSort : m σ
• regexSort : m σ
• bitvecSort : Nat → m σ
• arraySort : σ → σ → m σ
• constrSort : String → List σ → m σ

  Construct a sort for a named type (datatype or user-defined sort) with the given type arguments.

• mkBool : Bool → m τ
• mkInt : Int → m τ
• mkPrim : TermPrim → m τ
• mkAppOp : Op → List τ → σ → m τ

  Fallback for operations not covered by specific mk* methods (e.g. bitvectors, strings, regex). The backend receives the raw Op, the already-encoded arguments, and the result sort.

• mkAnd : List τ → m τ
• mkOr : List τ → m τ
• mkNot : τ → m τ
• mkImplies : τ → τ → m τ
• mkAdd : List τ → m τ
• mkSub : List τ → m τ
• mkMul : List τ → m τ
• mkDiv : τ → τ → m τ
• mkMod : τ → τ → m τ
• mkNeg : τ → m τ
• mkAbs : τ → m τ
• mkEq : List τ → m τ
• mkLt : List τ → m τ
• mkLe : List τ → m τ
• mkGt : List τ → m τ
• mkGe : List τ → m τ
• mkIte : τ → τ → τ → m τ
• mkSelect : τ → τ → m τ
• mkStore : τ → τ → τ → m τ
• mkApp : τ → List τ → m τ
• mkForall : List (String × σ) → (List τ → m (τ × List (List τ))) → m τ

  Construct a universally quantified term. Takes name-sort pairs for bound variables and a monadic callback that receives the bound variable terms and returns the body and trigger groups. The callback is monadic so callers can encode sub-terms using the bound variable handles. Bound variables cannot escape the quantifier scope.

• mkExists : List (String × σ) → (List τ → m (τ × List (List τ))) → m τ

  Construct an existentially quantified term. Same callback pattern as mkForall.

• declareNew : String → σ → m τ

  Declare a new variable. Shadowing is allowed: declaring the same name twice creates two distinct variables. The backend handles disambiguation internally.

• declareFun : String → List σ → σ → m τ

  Declare an uninterpreted function.

• mkParam : String → σ → m τ

  A parameter of a function about to be defined with defineFun, by the name it is given there. It declares nothing, so a body built from it refers to that parameter, where a variable from declareNew would be a global the body captures instead.

• defineFun : String → List (String × σ) → σ → τ → m Unit

  Define an interpreted function with a body term.

• defineFunRec : String → List (String × σ) → σ → τ → m Unit

  Define a recursive function (define-fun-rec): the body may refer to the function being defined. Only used under VerifyOptions.recursiveFnsAsDefineFunRec; backends without support keep the default, which fails.

• declareSort : String → Nat → m σ

  Declare a new sort with the given arity. Returns the declared sort.

• declareDatatype : String → List String → (σ → List σ → Except String (List (String × List (String × σ)))) → m (DatatypeInfo τ σ)

  Declare an algebraic datatype. Takes the datatype name, type parameter names, and a callback that receives (selfSort, typeParamSorts) and returns the constructors. Returns the declared sort and constructor/tester/selector handles. This callback pattern (like mkForall) allows recursive and parametric datatypes: the sort being declared does not exist yet when selectors need to reference it.

• declareDatatypes : List (String × List String) → (List σ → List (List σ) → Except String (List (List (String × List (String × σ))))) → m (List (DatatypeInfo τ σ))

  Declare mutually recursive algebraic datatypes. Takes a list of (name, typeParams) and a callback that receives (selfSorts, typeParamSorts) and returns constructors for each datatype. Returns the declared sorts and constructor/tester/selector handles.

• assert : τ → m Unit

  Assert a term (must be Bool-typed).

• checkSat : m Decision

  Check satisfiability of the current assertions.

• checkSatAssuming : List τ → m Decision

  Check satisfiability under additional assumptions.

• getUnsatAssumptions : m (List τ)

  After an unsat result from checkSatAssuming, retrieve the subset of assumptions that contributed to unsatisfiability.

• getModel : m (List ((String × Nat) × τ))

  Retrieve the model after a sat result. Keys are (name, shadow_depth) where 0 = most recently declared.

• getModelText : List τ → m String

  The values of the given terms as text, for reporting a counterexample. A consumer working against an abstract term type cannot take a model apart, and each backend already knows how to render its own: the SMT-LIB one returns the solver's reply to get-value verbatim, which is what parseModelDDM reads.

  Defaulted to a refusal, the way getModel is, so that a backend which cannot produce a model says so: empty text would read as a counterexample with no values in it. A backend that can render one overrides this.

• getValue : List τ → m (List (τ × τ))

  Get values of specific terms in the current model.

• termToSMTLibString : τ → m String

  Convert a term to its SMT-LIB string representation, making model values inspectable. The returned string must be valid SMT-LIB syntax.

• reset : m Unit

  Reset the solver session to its initial state.

• close : m Unit

  Close the solver session and release resources.