7. Solver🔗

Similar to terms, solvers come in typed and untyped flavors, though they do not differ by much. The main differences are

typed Solver.assert requires a Term Bool, instead of a Term for the untyped version, and
typed model/value-retrieval as we will see below.

The rest of this section discusses typed solvers.

Solvers are tied to cvc5's notion of term manager, which means they are manager-scoped with a Cvc.Ω instance just like sorts and terms.

open Cvc Typed
variable [Ω]

7.1. Basics🔗

def

Cvc.Typed.Solver [Cvc.Ω] : Type
Cvc.Typed.Solver [Cvc.Ω] : Type

Documentation and 1 equation

A solver instance.

Equations

Cvc.Typed.Solver = Cvc.Untyped.Solver

Solver creation and virtually all solver functions run in the Env monad.Marginal noteSome run in stronger monads than Env, as we will see very soon.

def

Cvc.Typed.Solver.new [Cvc.Ω] : Cvc.Env Cvc.Typed.Solver
Cvc.Typed.Solver.new [Cvc.Ω] :
  Cvc.Env Cvc.Typed.Solver

Documentation

Creates a new solver.

Some functions such as setLogic are actually defined on Untyped.Solver, but since Typed.Solver is just an alias for the untyped version we can use them on both types.

def

Cvc.Untyped.Solver.setLogic [Cvc.Ω] (s : Cvc.Untyped.Solver)
  (logic : Cvc.Logic) : Cvc.Env Unit
Cvc.Untyped.Solver.setLogic [Cvc.Ω]
  (s : Cvc.Untyped.Solver)
  (logic : Cvc.Logic) : Cvc.Env Unit

Documentation

Set logic.

logic: The logic to set.

def

Cvc.Untyped.Solver.setOption [Cvc.Ω] (s : Cvc.Untyped.Solver)
  (option value : String) : Cvc.Env Unit
Cvc.Untyped.Solver.setOption [Cvc.Ω]
  (s : Cvc.Untyped.Solver)
  (option value : String) : Cvc.Env Unit

Documentation

Set option.

option: The option name.
value: The option value.

Setting options also has a typed version that takes a Solver.Option, an enumeration of most of cvc5's options, and a value of the appropriate type for that option.

def

Cvc.Untyped.Solver.setOpt [Cvc.Ω] (s : Cvc.Untyped.Solver)
  (opt : Cvc.Solver.Option) (val : opt.argType) : Cvc.Env Unit
Cvc.Untyped.Solver.setOpt [Cvc.Ω]
  (s : Cvc.Untyped.Solver)
  (opt : Cvc.Solver.Option)
  (val : opt.argType) : Cvc.Env Unit

Documentation

Sets an option given as data, its value typed: s.setOpt .smt_produceModels true.

logic: QF_LIA
produce-models: true
#eval Env.runIO do
  let solver ← Solver.new
  solver.setLogic .qf_lia
  solver.setOption "produce-models" "true"
  solver.setOpt .smt_produceUnsatCores true
  println! "logic: {← solver.getLogic}"
  let val ← solver.getOption "produce-models"
  println! "produce-models: {val}"

While it is possible to declare function symbols in a solver, it is strictly equivalent to creating a solver-agnostic symbol with Term.mkSymbol/Term.mkSymbolAs. Both simply create a new symbol in the underlying term manager.

assertions:
- (<= 0 (g (f b i) i))
- b
#eval Env.runIO do
  let b ← Term.mkSymbol "b"
  let solver ← Solver.new
  let i ← solver.declareConst "i"
  let f ← Term.mkSymbolAs (Bool → Int → Int) "f"
  let g ← solver.declareFunAs (Int → Int → Int) "g"

  let t ← smt! 0 ≤ g (f b i) i
  solver.assert t
  solver.assert b
  println! "assertions:"
  for a in ← solver.getAssertions do
    -- note that `a : Term Bool`
    println! "- {a}"

assertions:
- (<= 0 (g (f b i) i))
- b

As shown above Solver.assert adds a Term Bool assertion in the solver.

def

Cvc.Typed.Solver.assert [Cvc.Ω] (s : Cvc.Typed.Solver)
  (t : Cvc.Typed.Term Bool) : Cvc.Env Unit
Cvc.Typed.Solver.assert [Cvc.Ω]
  (s : Cvc.Typed.Solver)
  (t : Cvc.Typed.Term Bool) : Cvc.Env Unit

Documentation

Asserts a formula.

The check-sat function is significantly more complex, to see why let us look at the get-value function first.

def

Cvc.Typed.Solver.getValue [Cvc.Ω] (s : Cvc.Typed.Solver) {α : Type}
  [Cvc.Typed.TermToValue α] (term : Cvc.Typed.Term α) : s.EnvSat α
Cvc.Typed.Solver.getValue [Cvc.Ω]
  (s : Cvc.Typed.Solver) {α : Type}
  [Cvc.Typed.TermToValue α]
  (term : Cvc.Typed.Term α) : s.EnvSat α

Documentation

The value the model gives a term, as the Lean value its index describes.

Since retrieving the value of a term is only legal (directly) after a check-sat that returned sat, cvc.lean strongly-types this fact with a modal environment, i.e. a monad specific to a solver being in sat-mode.

def

Cvc.Typed.Solver.EnvSat [Cvc.Ω] (s : Cvc.Typed.Solver) (α : Type) : Type
Cvc.Typed.Solver.EnvSat [Cvc.Ω]
  (s : Cvc.Typed.Solver) (α : Type) : Type

Documentation and 1 equation

Code running where solver last answered sat: the model queries (getValue, …) live here.

Entered only through checkSat's ifSat branch.

Equations

s.EnvSat = Cvc.Untyped.Solver.EnvSat s

Cvc.lean has three of these, the other two being unknown-modeMarginal noteUsually triggered by a timeout or when in an undecidable theory. and unsat-mode.

def

Cvc.Typed.Solver.getUnsatCore [Cvc.Ω] (s : Cvc.Typed.Solver) :
  s.EnvUnsat (Cvc.Typed.Terms Bool)
Cvc.Typed.Solver.getUnsatCore [Cvc.Ω]
  (s : Cvc.Typed.Solver) :
  s.EnvUnsat (Cvc.Typed.Terms Bool)

Documentation

An unsat core: assertions, and assumptions of the check if any, that are unsatisfiable together.

Needs produce-unsat-cores. Unlike SMT-LIB, named and unnamed assertions are not told apart.

(get-unsat-core)

def

Cvc.Typed.Solver.EnvUnsat [Cvc.Ω] (s : Cvc.Typed.Solver) (α : Type) :
  Type
Cvc.Typed.Solver.EnvUnsat [Cvc.Ω]
  (s : Cvc.Typed.Solver) (α : Type) : Type

Documentation and 1 equation

Code running where solver last answered unsat: unsat cores and proofs live here.

Entered only through checkSat's ifUnsat branch.

Equations

s.EnvUnsat = Cvc.Untyped.Solver.EnvUnsat s

def

Cvc.Typed.Solver.getTimeoutCore [Cvc.Ω] (s : Cvc.Typed.Solver) :
  s.EnvUnknown (Cvc.Typed.Result × Cvc.Typed.Terms Bool)
Cvc.Typed.Solver.getTimeoutCore [Cvc.Ω]
  (s : Cvc.Typed.Solver) :
  s.EnvUnknown
    (Cvc.Typed.Result ×
      Cvc.Typed.Terms Bool)

Documentation

A subset of the assertions that makes the solver time out, with the result of checking it.

Each internal check is limited by the timeout-core-timeout option. On an unknown result caused by a timeout, the assertions are a timeout core; on an unsat result, an unsat core; on a sat result, the assertions are satisfiable and the core is empty. Experimental in cvc5.

(get-timeout-core)

def

Cvc.Typed.Solver.EnvUnknown [Cvc.Ω] (s : Cvc.Typed.Solver) (α : Type) :
  Type
Cvc.Typed.Solver.EnvUnknown [Cvc.Ω]
  (s : Cvc.Typed.Solver) (α : Type) : Type

Documentation and 1 equation

Code running where solver last answered unknown: timeout cores live here.

Entered only through checkSat's ifUnknown branch.

Equations

s.EnvUnknown = Cvc.Untyped.Solver.EnvUnknown s

To guarantee modal code is safe to run, cvc.lean does not allow users to directly run it: it must be passed alongside a check-sat query to guarantee that only the appropriate sat/unsat/unknown code runs. Hence the signature of the solver check-sat function:

def

Cvc.Typed.Solver.checkSat {m : Type → Type} [Cvc.Ω] [Monad m]
  [MonadLiftT BaseIO m] (s : Cvc.Typed.Solver)
  (assuming : Option (Cvc.Typed.Terms Bool) := none) {α : Type}
  (ifSat : s.EnvSatT m α :=
    liftM (Cvc.Untyped.Solver.unexpectedSat false))
  (ifUnsat : s.EnvUnsatT m α :=
    liftM (Cvc.Untyped.Solver.unexpectedUnsat false))
  (ifUnknown : Cvc.Unknown.Explanation → s.EnvUnknownT m α :=
    liftM ∘ fun e => Cvc.Untyped.Solver.unexpectedUnknown e false) :
  Cvc.EnvT m α
Cvc.Typed.Solver.checkSat
  {m : Type → Type} [Cvc.Ω] [Monad m]
  [MonadLiftT BaseIO m]
  (s : Cvc.Typed.Solver)
  (assuming :
    Option (Cvc.Typed.Terms Bool) := none)
  {α : Type}
  (ifSat : s.EnvSatT m α :=
    liftM
      (Cvc.Untyped.Solver.unexpectedSat
        false))
  (ifUnsat : s.EnvUnsatT m α :=
    liftM
      (Cvc.Untyped.Solver.unexpectedUnsat
        false))
  (ifUnknown :
    Cvc.Unknown.Explanation →
      s.EnvUnknownT m α :=
    liftM ∘ fun e =>
      Cvc.Untyped.Solver.unexpectedUnknown
        e false) :
  Cvc.EnvT m α

Documentation

Checks satisfiability, under assuming if given, and runs the branch for the answer.

ifSat runs in s.EnvSat, where the model can be read, ifUnsat in s.EnvUnsat (unsat cores, proofs), ifUnknown on cvc5's explanation. An omitted branch throws if its answer comes up.

The only argument left to explain is assuming which is an optional array of Term Bool providing additional assumptions for this check-sat, called check-sat-assuming in SMT-LIB 2.7.

unsat core, not necessarily minimal:
- (not b)
- (= i2 7)
- (<= 0 i1)
- (or b (< i1 0))
model as Lean values:
- b  := true
- i1 := 0
- i2 := 7
model as cvc terms:
- b  := true
- i1 := 0
- i2 := 7
untyped model: #[true, 0, 7]
#eval Env.runIO do
  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  solver.setOpt .smt_produceUnsatCores true
  let b ← Term.mkSymbol "b"
  let i1 ← Term.mkSymbol "i1"
  let i2 ← Term.mkSymbol "i2"
  let not_b ← smt! ¬ b
  smt! i2 = 7 >>= solver.assert
  smt! 0 ≤ i1 >>= solver.assert
  smt! b ∨ i1 < 0 >>= solver.assert

  let core ← solver.checkSat (assuming := #[not_b])
    (ifUnsat := solver.getUnsatCore)
  println! "unsat core, not necessarily minimal:"
  for t in core do println! "- {t}"

  -- `Solver.getValue` extracts lean values
  let (bVal, i1Val, i2Val) ← solver.checkSat
    (ifSat := return (
      ← solver.getValue b,
      -- there's also a `getValue` function on terms
      ← i1.getValue,
      ← solver.getValue i2))
  println! "model as Lean values:\n\
    - b  := {bVal}\n- i1 := {i1Val}\n- i2 := {i2Val}"

  -- `Solver.getValueTerm` extracts (typed) cvc terms
  let (bVal, i1Val, i2Val) ← solver.checkSat
    (ifSat := return (
      ← solver.getValueTerm b,
      -- there's also a `getValueTerm` function on terms
      ← i1.getValueTerm,
      ← solver.getValueTerm i2))
  println! "model as cvc terms:\n\
    - b  := {bVal}\n- i1 := {i1Val}\n- i2 := {i2Val}"

  -- a typed term can always be erased if needed
  let vals ← solver.checkSat
    (ifSat := do
      let bVal ← solver.getValueTerm b
      let i1Val ← solver.getValueTerm i1
      let i2Val ← solver.getValueTerm i2
      return #[ bVal.erase, i1Val.erase, i2Val.erase ])
  println! "untyped model: {vals}"

unsat core, not necessarily minimal:
- (not b)
- (= i2 7)
- (<= 0 i1)
- (or b (< i1 0))
model as Lean values:
- b  := true
- i1 := 0
- i2 := 7
model as cvc terms:
- b  := true
- i1 := 0
- i2 := 7
untyped model: #[true, 0, 7]

7.3. More check-sat functions🔗

For simple check-sat use cases where the only thing that matters is whether the current assertions are satisfiable or not one can simply use Solver.checkIsSat.

def

Cvc.Typed.Solver.checkIsSat [Cvc.Ω] (s : Cvc.Typed.Solver)
  (assuming : Option (Cvc.Typed.Terms Bool) := none) : Cvc.Env Bool
Cvc.Typed.Solver.checkIsSat [Cvc.Ω]
  (s : Cvc.Typed.Solver)
  (assuming :
    Option (Cvc.Typed.Terms Bool) :=
    none) :
  Cvc.Env Bool

Documentation

Checks the satisfiability of the assertions, and of assuming if given, as a raw result.

Oftentimes we want to return a result specific to a sat/unsat result, and nothing otherwise, for instance a model on a sat result and nothing on unsat. In such cases it can be easier to use Solver.checkSat? which lets the caller specify which outcome produces a result and how, the unexpected result producing none by default.Marginal noteOn an unknown outcome, the default throws an error instead of returning none as unknown is considered to never be expected by default.

def

Cvc.Typed.Solver.checkSat? {m : Type → Type} [Cvc.Ω] [Monad m]
  [MonadLiftT BaseIO m] {α : Type} (s : Cvc.Typed.Solver)
  (assuming : Option (Cvc.Typed.Terms Bool) := none)
  (ifSat : s.EnvSatT m (Option α) := pure none)
  (ifUnsat : s.EnvUnsatT m (Option α) := pure none)
  (ifUnknown : Cvc.Unknown.Explanation → s.EnvUnknownT m (Option α) :=
    liftM ∘ fun e => Cvc.Untyped.Solver.unexpectedUnknown e false) :
  Cvc.EnvT m (Option α)
Cvc.Typed.Solver.checkSat?
  {m : Type → Type} [Cvc.Ω] [Monad m]
  [MonadLiftT BaseIO m] {α : Type}
  (s : Cvc.Typed.Solver)
  (assuming :
    Option (Cvc.Typed.Terms Bool) := none)
  (ifSat : s.EnvSatT m (Option α) :=
    pure none)
  (ifUnsat : s.EnvUnsatT m (Option α) :=
    pure none)
  (ifUnknown :
    Cvc.Unknown.Explanation →
      s.EnvUnknownT m (Option α) :=
    liftM ∘ fun e =>
      Cvc.Untyped.Solver.unexpectedUnknown
        e false) :
  Cvc.EnvT m (Option α)

Documentation

checkSat, whose sat and unsat branches default to none.

sat, adding constraint
  i1 := 0, i2 := 0
#eval Env.runIO do
  let b ← Term.mkSymbol "b"
  let i1 ← Term.mkSymbol "i1"
  let i2 ← Term.mkSymbol "i2"
  let Variable name `t1` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _t1

Note: This linter can be disabled with `set_option linter.unusedVariables false`t1 ← smt! b ∧ 0 < i1
  let t2 ← smt! i1 % i2 = i1
  let solver ← Solver.new
  solver.setOpt .smt_produceModels true
  if ← solver.checkIsSat then
    println! "sat, adding constraint"
    let values? ← solver.checkSat? (assuming := #[t2])
      (ifSat := return some (← i1.getValue, ← i2.getValue))
    if let some (i1Val, i2Val) := values?
    then println! "  i1 := {i1Val}, i2 := {i2Val}"
    else println! "  unsat with additional constraints"
  else println! "unsat"

sat, adding constraint
  i1 := 0, i2 := 0

7.4. Defining (recursive) function symbols🔗

Unlike declaring a function symbol, defining one is a solver-specific action as it implies a solver-level constraint to tie the symbol and its definition together.

Defining a function symbol in a solver is very similar to building a lambda: the resulting term must be typed from its bound variables.

def

Cvc.Typed.Solver.defineFun [Cvc.Ω] (s : Cvc.Typed.Solver) {β : Type}
  [Cvc.ToTyp β] (symbol : String) (bvs : Cvc.Typed.BVars)
  (body : Cvc.Typed.Term β) :
  Cvc.Env (Cvc.Typed.Term (Cvc.Typed.BVars.signatureTo β bvs))
Cvc.Typed.Solver.defineFun [Cvc.Ω]
  (s : Cvc.Typed.Solver) {β : Type}
  [Cvc.ToTyp β] (symbol : String)
  (bvs : Cvc.Typed.BVars)
  (body : Cvc.Typed.Term β) :
  Cvc.Env
    (Cvc.Typed.Term
      (Cvc.Typed.BVars.signatureTo β bvs))

Documentation

Defines a function symbol over bound variables bvs defined by body.

saturatingMaxDef := (let ((_let_1 (ite (<= j i) i j))) (ite (< _let_1 upperBound) _let_1 upperBound))
ub := 22
#eval Env.runIO do
  let ub ← Term.mkSymbolAs Int "upperBound"
  let solver ← Solver.new
  solver.setOpt .smt_produceModels true

  let (i, j) := (← BVar.mk "i", ← BVar.mk "j")
  let bVars := BVars.empty.push i |>.push j
  let saturatingMaxDef ← smt!
    let max ← if j ≤ i then i else j;
    if max < ub then max else ub
  println! "saturatingMaxDef := {saturatingMaxDef}"

  let sMax ← solver.defineFun
    "saturatingMax" bVars saturatingMaxDef
  smt! sMax 17 21 < ub >>= solver.assert
  solver.checkSat (ifSat := do
    println! "ub := {← ub.getValue}")

saturatingMaxDef := (let ((_let_1 (ite (<= j i) i j))) (ite (< _let_1 upperBound) _let_1 upperBound))
ub := 22

7.4.1. Mutually recursive function symbols🔗

Cvc.lean does not, currently, expose special functions for defining mutually recursive functions in its typed API. The untyped API does, which is what we present below.

open Cvc Untyped
variable [Ω]

forcing even
  sat, i := 4
forcing odd
  sat, i := 3
#eval Env.runIO do
  let int ← Srt.int
  let bool ← Srt.bool
  let solver ← Solver.new
  solver.setOption "produce-models" "true"
  solver.setOption "fmf-fun" "true"
  let even ← solver.declareFun "even" #[int] bool
  let odd ← solver.declareFun "odd" #[int] bool
  let n ← BVar.mk int "n"
  let m ← BVar.mk int "m"
  solver.defineFunsRec #[even, odd] #[#[n], #[m]] #[
    ← smt! if n ≤ 0 then n = 0 else odd (n - 1),
    ← smt! if m ≤ 0 then false else even (m - 1)]
  let i ← Term.mkSymbol int "i"
  smt! 3 ≤ i >>= solver.assert
  println! "forcing even"
  solver.checkSat (assuming := #[← smt! even i])
    (ifSat := do println! "  sat, i := {← i.getValue}")
  println! "forcing odd"
  solver.checkSat (assuming := #[← smt! odd i])
    (ifSat := do println! "  sat, i := {← i.getValue}")

forcing even
  sat, i := 4
forcing odd
  sat, i := 3

7. Solver🔗

7.1. Basics🔗

7.2. Check-sat and modal environments🔗

7.3. More check-sat functions🔗

7.4. Defining (recursive) function symbols🔗

7.4.1. Mutually recursive function symbols🔗