1.2. Solver🔗

Building terms is fun but it's not much use unless we use them in a solver. Like term creation, solver interaction happens in an error/state monad: Smt. For the monad transformer version, see SmtT. Its API is based on the usual SMT-LIB commands, for instance:

def

Cvc.Smt.declare (symbol : String) (α : Type) [IsSrt α] : Smt (Term α)
Cvc.Smt.declare (symbol : String)
  (α : Type) [IsSrt α] : Smt (Term α)

Declares a function symbol.

def

Cvc.Smt.assert (formula : Formula) : Smt Unit
Cvc.Smt.assert (formula : Formula) :
  Smt Unit

Asserts a formula.

Cvc.lean's version of check-sat includes the check-sat-assuming variant. As a reminder, check-sat-assuming allows to check the current assertions while assuming, just for the current check, that some Bool literals are true. It's actually more powerful in that it allows to assume any Term Bool, not just Bool literals.

def

Cvc.Smt.checkSat (assuming : Option (Array Formula) := none) :
  Smt CheckSat
Cvc.Smt.checkSat
  (assuming : Option (Array Formula) :=
    none) :
  Smt CheckSat

Checks the satisfiability of the formulas asserted with Smt.assert.

We will use a different check-sat version in the following, as the results it returns are easier to deal with.

def

Cvc.Smt.checkSat? (assuming : Option (Array Formula) := none) :
  Smt (Option Bool)
Cvc.Smt.checkSat?
  (assuming : Option (Array Formula) :=
    none) :
  Smt (Option Bool)

Simplified Smt.checkSat, returns true/false for sat/unsat, none for unknown/unexpected.

These basic SMT functions are enough to checkSat some constraints. Note that Smt also allows term-building.

open Cvc.Term.Dsl in
open Smt in
asserting (= (+ (* 2 x) y) 5)
asserting (= (+ (- x) y) 2)
check-sat-ing:
→ sat
#eval Cvc.Smt.runIO do
  let x ← declare "x" Int
  let y ← declare "y" Int
  let eq1 ← smt! 2 * x + y = 5
  println! "asserting {eq1}"
  assert eq1

  let eq2 ← smt! (-x) + y = 2
  println! "asserting {eq2}"
  assert eq2

  println! "check-sat-ing:"
  match ← checkSat? with
  | none => println! "→ unknown"
  | some true => println! "→ sat"
  | some false => println! "→ unsat"

asserting (= (+ (* 2 x) y) 5)
asserting (= (+ (- x) y) 2)
check-sat-ing:
→ sat

Nice, but how about retrieving the satisfying assignment for x and y, i.e. the model? Sure enough, there is a get-value-like function in the Smt namespace:

def

Cvc.Smt.Sat.getValue {α : Type} (term : Term α) : Smt.Sat (Value α)
Cvc.Smt.Sat.getValue {α : Type}
  (term : Term α) : Smt.Sat (Value α)

Retrieves the value of a term in Sat mode.

This function is available the following namespaces: Cvc.Term, Cvc.Smt, and Cvc.Smt.Sat.

Let's first note that this function does not return a term but a Value instead. This is just a wrapper around a term but specifies that the term was created by retrieving the value of another term. This means that, if the logics/assertions are simple enough, a Value is often a constant Term such as a Boolean/integer constant.

Moving on, it might be surprising that this function is not in the Smt monad, but instead in Smt.Sat. This is because getting the value of a symbol such as x is only valid right after a check-sat that confirmed the assertions are satisfiable. Smt.Sat is the monad corresponding to this exact context. See also Smt.Unsat/Smt.Unknown for the unsat/unknown equivalent.

def

Cvc.Smt.Sat (α : Type) : Type
Cvc.Smt.Sat (α : Type) : Type

Sat-mode monad, allows running commands such as get-value.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

The only way to run code in this monad is through yet another check-sat variant:

def

Cvc.Smt.checkSatAnd {m : Type → Type} [Monad m] {α : Type}
  (assuming : Option (Array Formula) := none)
  (ifSat : Smt.SatT m α := Smt.Sat.unexpected)
  (ifUnsat : Smt.UnsatT m α := Smt.Unsat.unexpected)
  (ifUnknown : Smt.UnknownT m α := Smt.Unknown.unexpected) : SmtT m α
Cvc.Smt.checkSatAnd {m : Type → Type}
  [Monad m] {α : Type}
  (assuming : Option (Array Formula) :=
    none)
  (ifSat : Smt.SatT m α :=
    Smt.Sat.unexpected)
  (ifUnsat : Smt.UnsatT m α :=
    Smt.Unsat.unexpected)
  (ifUnknown : Smt.UnknownT m α :=
    Smt.Unknown.unexpected) :
  SmtT m α

Performs a check-sat and runs sat/unsat/unknown-specific code.

Its signature is a bit daunting, though we have already discussed the assuming part. All it does is perform a check-sat and immediately run one of the three if<result> continuations depending on the outcome of the check. Their default values are there for convenience and fail by saying that the corresponding outcome was not expected.

Let's now retrieve the model for x and y in the previous example. In order two do so we must activate model production using Smt.setOption with the appropriate Cvc.Option.

open Cvc.Term.Dsl in
open Smt in
asserting (= (+ (* 2 x) y) 5)
asserting (= (+ (- x) y) 2)
check-sat-ing:
→ sat:
  x := 1
  y := 3
  eq1Lhs: 5
  eq2Lhs: 2
#eval Cvc.Smt.runIO do
  setOption .produceModels
  let x ← declare "x" Int
  let y ← declare "y" Int
  let eq1 ← smt! 2 * x + y = 5
  println! "asserting {eq1}"
  assert eq1

  let eq2 ← smt! (-x) + y = 2
  println! "asserting {eq2}"
  assert eq2

  println! "check-sat-ing:"
  checkSatAnd
    (ifUnsat := println! "→ unsat 🙀")
    (ifSat := do
      println! "→ sat:"
      let xValue ← getValue x
      println! "  x := {xValue}"
      let yValue ← getValue y
      println! "  y := {yValue}"

      -- we can also build terms in here
      let eq1Lhs ← getValue (← smt! 2 * x + y)
      let eq2Lhs ← getValue (← smt! (-x) + y)
      println! "  eq1Lhs: {eq1Lhs}"
      println! "  eq2Lhs: {eq2Lhs}")
    -- no `ifUnknown` continuation provided

asserting (= (+ (* 2 x) y) 5)
asserting (= (+ (- x) y) 2)
check-sat-ing:
→ sat:
  x := 1
  y := 3
  eq1Lhs: 5
  eq2Lhs: 2