This file defines a simple interface to an SMT solver running in a separate process. Callers communicate with the solver by issuing commands with s-expressions encoded as strings. The interface is based on lean-smt.

Currently, we support only CVC5. The function cvc5 creates a fresh CVC5 solver process. This function assumes that the environment variable CVC5 contains the absolute path to the CVC5 executable.

inductive Cedar.SymCC.Decision : Type

• sat : Decision
• unsat : Decision
• unknown : Decision

instance Cedar.SymCC.instDecidableEqDecision : DecidableEq Decision

Equations

• Cedar.SymCC.instDecidableEqDecision x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cedar.SymCC.instReprDecision.repr : Decision → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.SymCC.instReprDecision.repr Cedar.SymCC.Decision.sat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.SymCC.Decision.sat")).group prec✝

instance Cedar.SymCC.instReprDecision : Repr Decision

Equations

• Cedar.SymCC.instReprDecision = { reprPrec := Cedar.SymCC.instReprDecision.repr }

instance Cedar.SymCC.instToJsonDecision : Lean.ToJson Decision

Equations

• One or more equations did not get rendered due to their size.

structure Cedar.SymCC.Solver : Type

A Solver is an interpreter for SMTLib scripts, which are passed to the solver via its smtLibInput stream. Solvers optionally have an smtLibOutput stream to which they print the results of executing the commands received on the input stream. We assume that both the input and output streams conform to the SMTLib standard: the inputs are SMTLib script commands encoded as s-expressions, and the outputs are the s-expressions whose shape is determined by the standard for each command. We don't have an error stream here, since we configure solvers to run in quiet mode and not print anything to the error stream.

• smtLibInput : IO.FS.Stream
• smtLibOutput : Option IO.FS.Stream

@[reducible, inline]

abbrev Cedar.SymCC.SolverM (α : Type) : Type

Equations

• Cedar.SymCC.SolverM α = ReaderT Cedar.SymCC.Solver IO α

def Cedar.SymCC.SolverM.run {α : Type} (solver : Solver) (x : SolverM α) : IO α

Equations

• Cedar.SymCC.SolverM.run solver x = ReaderT.run x solver

def Cedar.SymCC.Solver.spawn (path : String) (args : Array String) : IO Solver

Returns a Solver for the given path and arguments. This function expects path to point to an SMT solver executable, and args to specify valid arguments to that solver.

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.cvc5 : IO Solver

Returns an instance of the CVC5 solver that is backed by the executable specified in the environment variable "CVC5".

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.streamWriter (s : IO.FS.Stream) : IO Solver

Returns a solver that writes all issued commands to the given stream s. Commands that produce output, such as checkSat, write the command to s and return values that are sound according to the SMTLib spec (but generally not useful). For example, Solver.checkSat returns Decision.unknown. This function expects s to be write-enabled.

Equations

• Cedar.SymCC.Solver.streamWriter s = pure { smtLibInput := s, smtLibOutput := none }

def Cedar.SymCC.Solver.fileWriter (h : IO.FS.Handle) : IO Solver

Returns a solver that writes all issued commands to the given file handle h. Commands that produce output, such as checkSat, write the command to h and return values that are sound according to the SMTLib spec (but generally not useful). For example, Solver.checkSat returns Decision.unknown. This function expects h to be write-enabled.

Equations

• Cedar.SymCC.Solver.fileWriter h = pure { smtLibInput := IO.FS.Stream.ofHandle h, smtLibOutput := none }

def Cedar.SymCC.Solver.bufferWriter (b : IO.Ref IO.FS.Stream.Buffer) : IO Solver

Returns a solver that writes all issued commands to the given buffer b. Commands that produce output, such as checkSat, write the command to b and return values that are sound according to the SMTLib spec (but generally not useful). For example, Solver.checkSat returns Decision.unknown.

Equations

• Cedar.SymCC.Solver.bufferWriter b = pure { smtLibInput := IO.FS.Stream.ofBuffer b, smtLibOutput := none }

def Cedar.SymCC.Solver.dummy : IO Solver

Returns a solver that drops/ignores all issued commands. Commands that produce output, such as checkSat, return values that are sound according to the SMTLib spec (but generally not useful). For example, Solver.checkSat returns Decision.unknown.

Equations

• Cedar.SymCC.Solver.dummy = do let __do_lift ← IO.FS.Handle.mk { toString := "/dev/null" } IO.FS.Mode.write pure { smtLibInput := IO.FS.Stream.ofHandle __do_lift, smtLibOutput := none }

def Cedar.SymCC.Solver.setLogic (logic : String) : SolverM Unit

Equations

• Cedar.SymCC.Solver.setLogic logic = Cedar.SymCC.Solver.emitln✝ (toString "(set-logic " ++ toString logic ++ toString ")")

def Cedar.SymCC.Solver.setOption (opt val : String) : SolverM Unit

Equations

• Cedar.SymCC.Solver.setOption opt val = Cedar.SymCC.Solver.emitln✝ (toString "(set-option " ++ toString opt ++ toString " " ++ toString val ++ toString ")")

def Cedar.SymCC.Solver.setOptionProduceModels (b : Bool) : SolverM Unit

Equations

• Cedar.SymCC.Solver.setOptionProduceModels b = Cedar.SymCC.Solver.setOption ":produce-models" (if b = true then "true" else "false")

def Cedar.SymCC.Solver.comment (comment : String) : SolverM Unit

Equations

• Cedar.SymCC.Solver.comment comment = Cedar.SymCC.Solver.emitln✝ (toString "; " ++ toString (comment.replace "\n" " "))

def Cedar.SymCC.Solver.assert (expr : String) : SolverM Unit

Equations

• Cedar.SymCC.Solver.assert expr = Cedar.SymCC.Solver.emitln✝ (toString "(assert " ++ toString expr ++ toString ")")

def Cedar.SymCC.Solver.defineFun (id : String) (args : List (String × String)) (type expr : String) : SolverM Unit

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.declareConst (id type : String) : SolverM Unit

Equations

• Cedar.SymCC.Solver.declareConst id type = Cedar.SymCC.Solver.emitln✝ (toString "(declare-const " ++ toString id ++ toString " " ++ toString type ++ toString ")")

def Cedar.SymCC.Solver.declareFun (id : String) (args : List String) (type : String) : SolverM Unit

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.declareDatatype (id : String) (params constructors : List String) : SolverM Unit

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.checkSat : SolverM Decision

Equations

• One or more equations did not get rendered due to their size.

def Cedar.SymCC.Solver.reset : SolverM Unit

Equations

• Cedar.SymCC.Solver.reset = Cedar.SymCC.Solver.emitln✝ "(reset)"

def Cedar.SymCC.Solver.exit : SolverM Unit

Equations

• Cedar.SymCC.Solver.exit = Cedar.SymCC.Solver.emitln✝ "(exit)"

def Cedar.SymCC.Solver.getModel : SolverM String

Returns the model from the SMT solver, assuming that checkSat produced a .sat decision. Note that this model extraction procedure assumes that the model strings follow the CVC5 format, where the model is enclosed in parentheses that are on a single line by themselves, i.e., opens with the line (\n and closes with the line )\n.

Equations

• One or more equations did not get rendered due to their size.