Cvc5 options.

inductive Cvc.Option.SimpMode : Type

(De)activates non-clausal simplification.

• none : SimpMode

  Do not perform non-clausal simplification.

• batch : SimpMode

  Save up all assertions; run non-clausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (checkSat or query or predicate subtype declaration).

def Cvc.Option.SimpMode.toString : SimpMode → String

Equations

• Cvc.Option.SimpMode.none.toString = "none"
• Cvc.Option.SimpMode.batch.toString = "batch"

instance Cvc.Option.SimpMode.instToString : ToString SimpMode

Equations

• Cvc.Option.SimpMode.instToString = { toString := Cvc.Option.SimpMode.toString }

inductive Cvc.Option.ModelCoresMode : Type

Mode for producing model cores.

• none : ModelCoresMode

  Do not compute model cores.

• simple : ModelCoresMode

  Only include a subset of variales whose values are sufficient to show the input formula is satsified by the given model.

• nonImplied : ModelCoresMode

  Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model.

def Cvc.Option.ModelCoresMode.toString : ModelCoresMode → String

Equations

• Cvc.Option.ModelCoresMode.none.toString = "none"
• Cvc.Option.ModelCoresMode.simple.toString = "simple"
• Cvc.Option.ModelCoresMode.nonImplied.toString = "non-implied"

instance Cvc.Option.ModelCoresMode.instToString : ToString ModelCoresMode

Equations

• Cvc.Option.ModelCoresMode.instToString = { toString := Cvc.Option.ModelCoresMode.toString }

inductive Cvc.Option.ProofMode : Type

Proof modes.

• off : ProofMode

  Do not produce proofs.

• ppOnly : ProofMode

  Only produce proofs for preprocessing.

• satProof : ProofMode

  Produce proofs for preprocessing and for the SAT solver.

• fullProof : ProofMode

  Produce full proofs of preprocessing, SAT and theory lemmas.

• fullProofStrict : ProofMode

  Produce full proofs of preprocessing, SAT and theory lemmas.

  Additionally disable techniques that will lead to incomplete proofs.

def Cvc.Option.ProofMode.toString : ProofMode → String

Equations

• Cvc.Option.ProofMode.off.toString = "off"
• Cvc.Option.ProofMode.ppOnly.toString = "pp-only"
• Cvc.Option.ProofMode.satProof.toString = "sat-proof"
• Cvc.Option.ProofMode.fullProof.toString = "full-proof"
• Cvc.Option.ProofMode.fullProofStrict.toString = "full-proof-strict"

instance Cvc.Option.ProofMode.instToString : ToString ProofMode

Equations

• Cvc.Option.ProofMode.instToString = { toString := Cvc.Option.ProofMode.toString }

inductive Cvc.Option.UnsatCoresMode : Type

Unsat core modes.

• off : UnsatCoresMode

  Do not produce unsat cores.

• satProof : UnsatCoresMode

  Produce unsat cores from the SAT proof and preprocessing proofs.

• assumptions : UnsatCoresMode

  Produce unsat cores using solving under assumptions and preprocessing proofs.

def Cvc.Option.UnsatCoresMode.toString : UnsatCoresMode → String

Equations

• Cvc.Option.UnsatCoresMode.off.toString = "off"
• Cvc.Option.UnsatCoresMode.satProof.toString = "sat-proof"
• Cvc.Option.UnsatCoresMode.assumptions.toString = "assumptions"

instance Cvc.Option.UnsatCoresMode.instToString : ToString UnsatCoresMode

Equations

• Cvc.Option.UnsatCoresMode.instToString = { toString := Cvc.Option.UnsatCoresMode.toString }

inductive Cvc.Option.ExtRewPrepMode : Type

Extended rewriter preprocessing pass modes.

• off : ExtRewPrepMode

  Do not use extended rewriter as a preprocessing pass.

• use : ExtRewPrepMode

  Use extended rewriter as a preprocessing pass.

• agg : ExtRewPrepMode

  Use aggressive extended rewriter as a preprocessing pass.

def Cvc.Option.ExtRewPrepMode.toString : ExtRewPrepMode → String

Equations

• Cvc.Option.ExtRewPrepMode.off.toString = "off"
• Cvc.Option.ExtRewPrepMode.use.toString = "use"
• Cvc.Option.ExtRewPrepMode.agg.toString = "agg"

instance Cvc.Option.ExtRewPrepMode.instToString : ToString ExtRewPrepMode

Equations

• Cvc.Option.ExtRewPrepMode.instToString = { toString := Cvc.Option.ExtRewPrepMode.toString }

inductive Cvc.Option.InterpolantsMode : Type

Interpolants grammar mode.

• default : InterpolantsMode

  Use the default grammar for the theory or the user-defined grammar if given.

• assumptions : InterpolantsMode

  Use only operators that occur in the assumptions.

• conjecture : InterpolantsMode

  Use only operators that occur in the conjecture.

• shared : InterpolantsMode

  Use only operators that occur both in the assumptions and the conjecture.

• all : InterpolantsMode

  Use only operators that occur either in the assumptions or the conjecture.

def Cvc.Option.InterpolantsMode.toString : InterpolantsMode → String

Equations

• Cvc.Option.InterpolantsMode.default.toString = "default"
• Cvc.Option.InterpolantsMode.assumptions.toString = "assumptions"
• Cvc.Option.InterpolantsMode.conjecture.toString = "conjecture"
• Cvc.Option.InterpolantsMode.shared.toString = "shared"
• Cvc.Option.InterpolantsMode.all.toString = "all"

instance Cvc.Option.InterpolantsMode.instToString : ToString InterpolantsMode

Equations

• Cvc.Option.InterpolantsMode.instToString = { toString := Cvc.Option.InterpolantsMode.toString }

inductive Cvc.Option.DifficultyMode : Type

Difficulty output modes.

• lemmaLiteral : DifficultyMode

  Difficulty of an assertion is how many lemmas (at full effort) use a literal that the assertion depends on to be satisfied.

• lemmaLiteralAll : DifficultyMode

  Difficulty of an assertion is how many lemmas use a literal that the assertion depends on to be satisfied.

• modelCheck : DifficultyMode

  Difficulty of an assertion is how many times it was not satisfied in a candidate model.

def Cvc.Option.DifficultyMode.toString : DifficultyMode → String

Equations

• Cvc.Option.DifficultyMode.lemmaLiteral.toString = "lemma-literal"
• Cvc.Option.DifficultyMode.lemmaLiteralAll.toString = "lemal-literal-all"
• Cvc.Option.DifficultyMode.modelCheck.toString = "model-check"

instance Cvc.Option.DifficultyMode.instToString : ToString DifficultyMode

Equations

• Cvc.Option.DifficultyMode.instToString = { toString := Cvc.Option.DifficultyMode.toString }

inductive Cvc.Option.Common : Type

• produceModels (active : Bool) : Common

  Support the getValue and getModel commands, default false.

• checkModels (active : Bool) : Common

  After sat/invalid/unknown, check that the generated model satisfies user assertions, default false.

def Cvc.Option.Common.keyVal : Common → String × String

Equations

• (Cvc.Option.Common.produceModels active).keyVal = ("produce-models", toString active)
• (Cvc.Option.Common.checkModels active).keyVal = ("check-models", toString active)

inductive Cvc.Option.Regular : Type

• ackermann (active : Bool) : Regular

  Eliminate functions by ackermannization, default false.

• simpMode (mode : SimpMode) : Regular

  Simplification mode, default SimpMode.batch.

• staticLearning (active : Bool) : Regular

  Use static learning, default true.

• learnedRewrite (active : Bool) : Regular

  Rewrite the input based on learned literals, default false.

• modelCoresMode (mode : ModelCoresMode) : Regular

  Model cores modes, default ModelCoresMode.none.

• produceLearnedLiterals (active : Bool) : Regular

  Produce learned literals, support getLearnedLiterals, default false.

• produceProofs (active : Bool) : Regular

  Produce proofs, support checkProofs and getProof, default false.

• checkProofs (active : Bool) : Regular

  After unsat/invalid, check the generated proof (with proof), default false.

• produceUnsatCores (active : Bool) : Regular

  Turn on unsat core generation, default false.

  Unless otherwise specified, cores will be produced using SAT solving under assumptions and preprocessing proofs.

• printCoresFull (active : Bool) : Regular

  Print all formulas regardless of whether they are named, e.g. in unsat cores, default false.

• checkUnsatCores (active : Bool) : Regular

  After unsat/valid, produce and check an unsat core (expensive), default false.

• produceUnsatAssumptions (active : Bool) : Regular

  Turn on unsat assumptions generation, default false.

• produceDifficulty (active : Bool) : Regular

  Enable tracking of difficulty, default false.

• checkSynthSol (active : Bool) : Regular

  Checks whether produced solutions to functions-to-synthesize satisfy the conjecture, default false.

• produceAssignments (active : Bool) : Regular

  Support the getAssignment command, default false.

• produceAssertions (active : Bool) : Regular

  Keep an assertions list, default true.

  Note that this option is always enabled.

• extRewPrep (mode : ExtRewPrepMode) : Regular

  Extended rewriter preprocessing pass modes, default ExtRewPrepMode.off.

• unconstrainedSimp (active : Bool) : Regular

  Turn on unconstrained simplification, see Bruttomesso/Brummayer PhD thesis.

  Fully supported only in (subsets of) the logic QF_ABV.

• sortInference (active : Bool) : Regular

  Calculate sort inference of input problem, convert the input based on monotonic sorts.

• produceInterpolants (active : Bool) : Regular

  Turn on interpolation generation.

• interpolantsMode (mode : InterpolantsMode) : Regular

  Interpolants grammar mode.

def Cvc.Option.Regular.keyVal : Regular → String × String

Equations

• (Cvc.Option.Regular.ackermann b).keyVal = ("ackermann", toString b)
• (Cvc.Option.Regular.simpMode m).keyVal = ("simplification-mode", toString m)
• (Cvc.Option.Regular.staticLearning b).keyVal = ("static-learning", toString b)
• (Cvc.Option.Regular.learnedRewrite b).keyVal = ("learned-rewrite", toString b)
• (Cvc.Option.Regular.modelCoresMode m).keyVal = ("model-cores", toString m)
• (Cvc.Option.Regular.produceLearnedLiterals b).keyVal = ("produce-learned-literals", toString b)
• (Cvc.Option.Regular.produceProofs b).keyVal = ("produce-proofs", toString b)
• (Cvc.Option.Regular.checkProofs b).keyVal = ("check-proofs", toString b)
• (Cvc.Option.Regular.produceUnsatCores b).keyVal = ("produce-unsat-cores", toString b)
• (Cvc.Option.Regular.printCoresFull b).keyVal = ("print-cores-full", toString b)
• (Cvc.Option.Regular.checkUnsatCores b).keyVal = ("check-unsat-cores", toString b)
• (Cvc.Option.Regular.produceUnsatAssumptions b).keyVal = ("produce-unsat-assumptions", toString b)
• (Cvc.Option.Regular.produceDifficulty b).keyVal = ("produce-difficulty", toString b)
• (Cvc.Option.Regular.checkSynthSol b).keyVal = ("check-synth-sol", toString b)
• (Cvc.Option.Regular.produceAssignments b).keyVal = ("produce-assignments", toString b)
• (Cvc.Option.Regular.produceAssertions b).keyVal = ("produce-assertions", toString b)
• (Cvc.Option.Regular.extRewPrep b).keyVal = ("ext-rew-prep", toString b)
• (Cvc.Option.Regular.unconstrainedSimp b).keyVal = ("unconstrained-simp", toString b)
• (Cvc.Option.Regular.sortInference b).keyVal = ("sort-inference", toString b)
• (Cvc.Option.Regular.produceInterpolants b).keyVal = ("produce-interpolants", toString b)
• (Cvc.Option.Regular.interpolantsMode m).keyVal = ("interpolants-mode", toString m)

inductive Cvc.Option.Expert : Type

• simpBoolConstProp (active : Bool) : Expert

  Apply boolean constant propagation as a substitution during simplification, default false.

• debugCheckModels (active : Bool) : Expert

  After sat/invalid/unknown, check that the generated model satisfies user and internal assertions, default false.

• modelVarElimUneval (active : Bool) : Expert

  Allow variable elimination based on unevaluatable terms to variables, default true.

• proofMode (mode : ProofMode) : Expert

  Proof mode, default ProofMode.off.

• unsatCoresMode (mode : UnsatCoresMode) : Expert

  Unsat cores mode, default UnsatCoresMode.off.

• minimalUnsatCores (active : Bool) : Expert

  If an unsat core is produced, it is reduced to a minimal unsat core, default false.

• difficultyMode (mode : DifficultyMode) : Expert

  Difficulty mode, default DifficultyMode.lemmaLiteralAll.

• doIteSimp (active : Bool) : Expert

  Turn on if-then-else simplification, default false.

  See Kim (and Somenzi) et al., SAT 2009.

• doIteSimpOnRepeat (active : Bool) : Expert

  Do the if-then-else simplification pass again if repeating simplification, default false.

• simplifyWithCareEnabled (active : Bool) : Expert

  Enables simplify-with-care in if-then-else simplification.

• compressItes (active : Bool) : Expert

  Enables compressing if-then-else-s after if-then-else simplification.

• earlyIteRemoval (active : Bool) : Expert

  Remove if-then-else-s early in preprocessing.

• repeatSimp (active : Bool) : Expert

  Make multiple passes with nonclausal simplifier.

• abstractValues (active : Bool) : Expert

  In models, output arrays using abstract values, as required by the SMT-LIB standard.

  This may support more than arrays in the future.

def Cvc.Option.Expert.keyVal : Expert → String × String

Equations

• (Cvc.Option.Expert.simpBoolConstProp b).keyVal = ("simplification-bcp", toString b)
• (Cvc.Option.Expert.debugCheckModels b).keyVal = ("debug-check-models", toString b)
• (Cvc.Option.Expert.modelVarElimUneval b).keyVal = ("model-var-elim-uneval", toString b)
• (Cvc.Option.Expert.proofMode m).keyVal = ("proof-mode", toString m)
• (Cvc.Option.Expert.unsatCoresMode m).keyVal = ("unsat-cores-mode", toString m)
• (Cvc.Option.Expert.minimalUnsatCores b).keyVal = ("minimal-unsat-cores", toString b)
• (Cvc.Option.Expert.difficultyMode m).keyVal = ("difficulty-mode", toString m)
• (Cvc.Option.Expert.doIteSimp b).keyVal = ("ite-simp", toString b)
• (Cvc.Option.Expert.doIteSimpOnRepeat b).keyVal = ("on-repeat-ite-simp", toString b)
• (Cvc.Option.Expert.simplifyWithCareEnabled b).keyVal = ("simp-with-care", toString b)
• (Cvc.Option.Expert.compressItes b).keyVal = ("simp-ite-compress", toString b)
• (Cvc.Option.Expert.earlyIteRemoval b).keyVal = ("early-ite-removal", toString b)
• (Cvc.Option.Expert.repeatSimp b).keyVal = ("repeat-simp", toString b)
• (Cvc.Option.Expert.abstractValues b).keyVal = ("abstract-values", toString b)

inductive Cvc.Option : Type

• common (c : Common) : Cvc.Option
• regular (r : Regular) : Cvc.Option
• expert (e : Expert) : Cvc.Option

instance Cvc.Option.instCoeCommon : Coe Common Cvc.Option

Equations

• Cvc.Option.instCoeCommon = { coe := Cvc.Option.common }

instance Cvc.Option.instCoeRegular : Coe Regular Cvc.Option

Equations

• Cvc.Option.instCoeRegular = { coe := Cvc.Option.regular }

instance Cvc.Option.instCoeExpert : Coe Expert Cvc.Option

Equations

• Cvc.Option.instCoeExpert = { coe := Cvc.Option.expert }

def Cvc.Option.produceModels (active : Bool := true) : Cvc.Option

Support the getValue and getModel commands, default false.

Equations

• Cvc.Option.produceModels active = Cvc.Option.common (Cvc.Option.Common.produceModels active)

def Cvc.Option.produceProofs (active : Bool := true) : Cvc.Option

Produce proofs, support checkProofs and getProof, default false.

Equations

• Cvc.Option.produceProofs active = Cvc.Option.regular (Cvc.Option.Regular.produceProofs active)

def Cvc.Option.produceUnsatCores (active : Bool := true) : Cvc.Option

Turn on unsat core generation, default false.

Unless otherwise specified, cores will be produced using SAT solving under assumptions and preprocessing proofs.

Equations

• Cvc.Option.produceUnsatCores active = Cvc.Option.regular (Cvc.Option.Regular.produceUnsatCores active)

def Cvc.Option.produceInterpolants (active : Bool := true) : Cvc.Option

Turn on interpolation generation.

Equations

• Cvc.Option.produceInterpolants active = Cvc.Option.regular (Cvc.Option.Regular.produceInterpolants active)

def Cvc.Option.produceAssignments (active : Bool := true) : Cvc.Option

Support the getAssignment command, default false.

Equations

• Cvc.Option.produceAssignments active = Cvc.Option.regular (Cvc.Option.Regular.produceAssignments active)

def Cvc.Option.produceAssertions (active : Bool := true) : Cvc.Option

Keep an assertions list, default true.

Note that this option is always enabled.

Equations

• Cvc.Option.produceAssertions active = Cvc.Option.regular (Cvc.Option.Regular.produceAssertions active)

def Cvc.Option.keyVal : Cvc.Option → String × String

Equations

• (Cvc.Option.common c).keyVal = c.keyVal
• (Cvc.Option.regular r).keyVal = r.keyVal
• (Cvc.Option.expert e).keyVal = e.keyVal