Documentation

Cvc.SolverOptions

Solver options #

The options a solver accepts, as data rather than as strings. Solver.Option has one variant per category, each wrapping that category's own inductive, and Solver.Option.argType is the type of the value an option expects: Bool for a flag, Nat or Int for a number, and a dedicated inductive for an option taking one of a fixed set of modes. Solver.Option.toStrings produces the flag and value cvc5's string-based setOption wants.

Each option is also an abbreviation on Solver.Option named after its category and itself, so .smt_produceModels can be written for .smt .produceModels. A solver's setOpt sets one: s.setOpt .smt_produceModels true.

The options are cvc5's own, minus three kinds:

those cvc5 reserves for experts;
those of its command-line driver and of its parser (help, version, interactive, force-logic, lang, …), which mean nothing to a solver driven through its API;
quiet and verbose, which only step the verbosity, verbosity setting it directly.

The categories follow cvc5's own modules, with two departures: every sygus-* option is gathered into Solver.Option.Sygus wherever cvc5 declares it, and decision is an SMT-layer option rather than the only member of a category of its own.

inductive Cvc.Solver.Option.Base.Output :

Output tags, each enabling one kind of diagnostic output.

inst : Output
inst: Print instantiations during solving.
instStrategy : Output
inst-strategy: Prints a summary of the instantiation techniques as they are run.
oracles : Output
oracles: Print calls to oracles and responses received.
sygus : Output
sygus: Print enumerated terms and candidates generated by the sygus solver.
sygusGrammar : Output
sygus-grammar: Print grammars automatically generated by the sygus solver.
sygusEnumerator : Output
sygus-enumerator: Print enumerators generated by the sygus solver.
sygusSolGterm : Output
sygus-sol-gterm.
Print annotations for terms in sygus solutions that indicate the grammar used to generate them.
trigger : Output
trigger: Print selected triggers for quantified formulas.
rawBenchmark : Output
raw-benchmark: Print the benchmark back on the output verbatim as it is processed.
learnedLits : Output
learned-lits: Print input literals that hold globally.
subs : Output
subs: Print top-level substitutions learned during preprocessing.
postAsserts : Output
post-asserts.
Print a benchmark corresponding to the assertions of the input problem after preprocessing.
preAsserts : Output
pre-asserts.
Print a benchmark corresponding to the assertions of the input problem before preprocessing.
deepRestart : Output
deep-restart.
Print when cvc5 performs a deep restart along with the literals it has learned.
incomplete : Output
incomplete: Print reason why cvc5 answers unknown for any given check-sat query.
lemmas : Output
lemmas: Print lemmas as they are added to the SAT solver.
trustedProofSteps : Output
trusted-proof-steps: Print formulas corresponding to trusted proof steps in final proofs.
timeoutCoreBenchmark : Output
timeout-core-benchmark.
Print the corresponding benchmark when successfully computing a timeout core.
unsatCoreBenchmark : Output
unsat-core-benchmark.
Print the corresponding benchmark when successfully computing an unsat core.
unsatCoreLemmasBenchmark : Output
unsat-core-lemmas-benchmark.
Print the corresponding benchmark when successfully computing an unsat core with theory lemmas.
unsatCoreLemmas : Output
unsat-core-lemmas.
Print diagnostic information on lemmas that appear in an unsat core with theory lemmas.
portfolio : Output
portfolio: Prints the option strings tried in portfolio mode.
blockModel : Output
block-model: Prints the formulas used when block-model is run.
optionsAuto : Output
options-auto: Prints the options set during automatic configuration.
rareDb : Output
rare-db.
Upon initialization, print the set of (non-expert) RARE rewrite rules as they are defined in the proof signature.
rareDbExpert : Output
rare-db-expert.
Upon initialization, print the set of expert RARE rewrite rules as they are defined in the proof signature.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Base.instInhabitedOutput :

Inhabited Output

Equations

Cvc.Solver.Option.Base.instInhabitedOutput = { default := Cvc.Solver.Option.Base.instInhabitedOutput.default }

@[instance_reducible]

instance Cvc.Solver.Option.Base.instDecidableEqOutput :

DecidableEq Output

Equations

Cvc.Solver.Option.Base.instDecidableEqOutput x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Base.instReprOutput.repr :

Output → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Base.instReprOutput :

Equations

Cvc.Solver.Option.Base.instReprOutput = { reprPrec := Cvc.Solver.Option.Base.instReprOutput.repr }

def Cvc.Solver.Option.Base.Output.toString :

Output → String

The string cvc5 expects for a value of --output.

Equations

Cvc.Solver.Option.Base.Output.inst.toString = "inst"
Cvc.Solver.Option.Base.Output.instStrategy.toString = "inst-strategy"
Cvc.Solver.Option.Base.Output.oracles.toString = "oracles"
Cvc.Solver.Option.Base.Output.sygus.toString = "sygus"
Cvc.Solver.Option.Base.Output.sygusGrammar.toString = "sygus-grammar"
Cvc.Solver.Option.Base.Output.sygusEnumerator.toString = "sygus-enumerator"
Cvc.Solver.Option.Base.Output.sygusSolGterm.toString = "sygus-sol-gterm"
Cvc.Solver.Option.Base.Output.trigger.toString = "trigger"
Cvc.Solver.Option.Base.Output.rawBenchmark.toString = "raw-benchmark"
Cvc.Solver.Option.Base.Output.learnedLits.toString = "learned-lits"
Cvc.Solver.Option.Base.Output.subs.toString = "subs"
Cvc.Solver.Option.Base.Output.postAsserts.toString = "post-asserts"
Cvc.Solver.Option.Base.Output.preAsserts.toString = "pre-asserts"
Cvc.Solver.Option.Base.Output.deepRestart.toString = "deep-restart"
Cvc.Solver.Option.Base.Output.incomplete.toString = "incomplete"
Cvc.Solver.Option.Base.Output.lemmas.toString = "lemmas"
Cvc.Solver.Option.Base.Output.trustedProofSteps.toString = "trusted-proof-steps"
Cvc.Solver.Option.Base.Output.timeoutCoreBenchmark.toString = "timeout-core-benchmark"
Cvc.Solver.Option.Base.Output.unsatCoreBenchmark.toString = "unsat-core-benchmark"
Cvc.Solver.Option.Base.Output.unsatCoreLemmasBenchmark.toString = "unsat-core-lemmas-benchmark"
Cvc.Solver.Option.Base.Output.unsatCoreLemmas.toString = "unsat-core-lemmas"
Cvc.Solver.Option.Base.Output.portfolio.toString = "portfolio"
Cvc.Solver.Option.Base.Output.blockModel.toString = "block-model"
Cvc.Solver.Option.Base.Output.optionsAuto.toString = "options-auto"
Cvc.Solver.Option.Base.Output.rareDb.toString = "rare-db"
Cvc.Solver.Option.Base.Output.rareDbExpert.toString = "rare-db-expert"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Base.instToStringOutput :

ToString Output

Equations

Cvc.Solver.Option.Base.instToStringOutput = { toString := Cvc.Solver.Option.Base.Output.toString }

inductive Cvc.Solver.Option.Base :

Resource limits, verbosity, statistics and incrementality.

incremental : Base
--incremental: Enable incremental solving.
output : Base
--output: Enable output tag.
parseOnly : Base
--parse-only: Exit after parsing input.
preprocessOnly : Base
--preprocess-only: Exit after preprocessing input.
rlimit : Base
--rlimit: Set resource limit.
rlimitPer : Base
--rlimit-per: Set resource limit per query.
stats : Base
--stats: Give statistics on exit.
statsAll : Base
--stats-all: Print unchanged (defaulted) statistics as well.
statsInternal : Base
--stats-internal: Print internal (non-public) statistics as well.
tlimit : Base
--tlimit: Set time limit in milliseconds of wall clock time.
tlimitPer : Base
--tlimit-per: Set time limit per query in milliseconds.
verbosity : Base
--verbosity: The verbosity level of cvc5.
seed : Base
--seed: Seed for random number generator.
statsEveryQuery : Base
--stats-every-query.
In incremental mode, print stats after every satisfiability or validity query.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedBase :

Equations

Cvc.Solver.Option.instInhabitedBase = { default := Cvc.Solver.Option.instInhabitedBase.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqBase :

DecidableEq Base

Equations

Cvc.Solver.Option.instDecidableEqBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprBase :

Equations

Cvc.Solver.Option.instReprBase = { reprPrec := Cvc.Solver.Option.instReprBase.repr }

def Cvc.Solver.Option.instReprBase.repr :

Base → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Base.name :

Base → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Base.incremental.name = "incremental"
Cvc.Solver.Option.Base.output.name = "output"
Cvc.Solver.Option.Base.parseOnly.name = "parse-only"
Cvc.Solver.Option.Base.preprocessOnly.name = "preprocess-only"
Cvc.Solver.Option.Base.rlimit.name = "rlimit"
Cvc.Solver.Option.Base.rlimitPer.name = "rlimit-per"
Cvc.Solver.Option.Base.stats.name = "stats"
Cvc.Solver.Option.Base.statsAll.name = "stats-all"
Cvc.Solver.Option.Base.statsInternal.name = "stats-internal"
Cvc.Solver.Option.Base.tlimit.name = "tlimit"
Cvc.Solver.Option.Base.tlimitPer.name = "tlimit-per"
Cvc.Solver.Option.Base.verbosity.name = "verbosity"
Cvc.Solver.Option.Base.seed.name = "seed"
Cvc.Solver.Option.Base.statsEveryQuery.name = "stats-every-query"

Instances For

def Cvc.Solver.Option.Base.valueString (opt : Base) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Smt.Decision :

Decision modes.

internal : Decision
internal: Use the internal decision heuristics of the SAT solver (the default).
justification : Decision
justification: An ATGP-inspired justification heuristic.
stoponly : Decision
stoponly: Use the justification heuristic only to stop early, not for decisions.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instInhabitedDecision :

Inhabited Decision

Equations

Cvc.Solver.Option.Smt.instInhabitedDecision = { default := Cvc.Solver.Option.Smt.instInhabitedDecision.default }

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instDecidableEqDecision :

DecidableEq Decision

Equations

Cvc.Solver.Option.Smt.instDecidableEqDecision x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Smt.instReprDecision.repr :

Decision → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instReprDecision :

Equations

Cvc.Solver.Option.Smt.instReprDecision = { reprPrec := Cvc.Solver.Option.Smt.instReprDecision.repr }

def Cvc.Solver.Option.Smt.Decision.toString :

Decision → String

The string cvc5 expects for a value of --decision.

Equations

Cvc.Solver.Option.Smt.Decision.internal.toString = "internal"
Cvc.Solver.Option.Smt.Decision.justification.toString = "justification"
Cvc.Solver.Option.Smt.Decision.stoponly.toString = "stoponly"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instToStringDecision :

ToString Decision

Equations

Cvc.Solver.Option.Smt.instToStringDecision = { toString := Cvc.Solver.Option.Smt.Decision.toString }

inductive Cvc.Solver.Option.Smt.InterpolantsMode :

Interpolants grammar mode.

default : InterpolantsMode
default: Use the default grammar for the theory or the user-defined grammar if given.
assumptions : InterpolantsMode
assumptions: Use only operators that occur in the assumptions.
conjecture : InterpolantsMode
conjecture: Use only operators that occur in the conjecture.
shared : InterpolantsMode
shared: Use only operators that occur both in the assumptions and the conjecture.
all : InterpolantsMode
all: Use only operators that occur either in the assumptions or the conjecture.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instInhabitedInterpolantsMode :

Inhabited InterpolantsMode

Equations

Cvc.Solver.Option.Smt.instInhabitedInterpolantsMode = { default := Cvc.Solver.Option.Smt.instInhabitedInterpolantsMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instDecidableEqInterpolantsMode :

DecidableEq InterpolantsMode

Equations

Cvc.Solver.Option.Smt.instDecidableEqInterpolantsMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Smt.instReprInterpolantsMode.repr :

InterpolantsMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instReprInterpolantsMode :

Repr InterpolantsMode

Equations

Cvc.Solver.Option.Smt.instReprInterpolantsMode = { reprPrec := Cvc.Solver.Option.Smt.instReprInterpolantsMode.repr }

def Cvc.Solver.Option.Smt.InterpolantsMode.toString :

InterpolantsMode → String

The string cvc5 expects for a value of --interpolants-mode.

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instToStringInterpolantsMode :

ToString InterpolantsMode

Equations

Cvc.Solver.Option.Smt.instToStringInterpolantsMode = { toString := Cvc.Solver.Option.Smt.InterpolantsMode.toString }

inductive Cvc.Solver.Option.Smt.ModelCores :

Model cores modes.

none : ModelCores
none: Do not compute model cores (the default).
simple : ModelCores
simple.
Only include a subset of variables whose values are sufficient to show the input formula is satisfied by the given model.
nonImplied : ModelCores
non-implied.
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.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instInhabitedModelCores :

Inhabited ModelCores

Equations

Cvc.Solver.Option.Smt.instInhabitedModelCores = { default := Cvc.Solver.Option.Smt.instInhabitedModelCores.default }

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instDecidableEqModelCores :

DecidableEq ModelCores

Equations

Cvc.Solver.Option.Smt.instDecidableEqModelCores x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Smt.instReprModelCores.repr :

ModelCores → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instReprModelCores :

Repr ModelCores

Equations

Cvc.Solver.Option.Smt.instReprModelCores = { reprPrec := Cvc.Solver.Option.Smt.instReprModelCores.repr }

def Cvc.Solver.Option.Smt.ModelCores.toString :

ModelCores → String

The string cvc5 expects for a value of --model-cores.

Equations

Cvc.Solver.Option.Smt.ModelCores.none.toString = "none"
Cvc.Solver.Option.Smt.ModelCores.simple.toString = "simple"
Cvc.Solver.Option.Smt.ModelCores.nonImplied.toString = "non-implied"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instToStringModelCores :

ToString ModelCores

Equations

Cvc.Solver.Option.Smt.instToStringModelCores = { toString := Cvc.Solver.Option.Smt.ModelCores.toString }

inductive Cvc.Solver.Option.Smt.Simplification :

Simplification modes.

none : Simplification
none: Do not perform nonclausal simplification.
batch : Simplification
batch.
Save up all ASSERTions; run nonclausal simplification and clausal (MiniSat) propagation for all of them only after reaching a querying command (CHECKSAT or QUERY or predicate SUBTYPE declaration) (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instInhabitedSimplification :

Inhabited Simplification

Equations

Cvc.Solver.Option.Smt.instInhabitedSimplification = { default := Cvc.Solver.Option.Smt.instInhabitedSimplification.default }

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instDecidableEqSimplification :

DecidableEq Simplification

Equations

Cvc.Solver.Option.Smt.instDecidableEqSimplification x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instReprSimplification :

Repr Simplification

Equations

Cvc.Solver.Option.Smt.instReprSimplification = { reprPrec := Cvc.Solver.Option.Smt.instReprSimplification.repr }

def Cvc.Solver.Option.Smt.instReprSimplification.repr :

Simplification → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Smt.Simplification.toString :

Simplification → String

The string cvc5 expects for a value of --simplification.

Equations

Cvc.Solver.Option.Smt.Simplification.none.toString = "none"
Cvc.Solver.Option.Smt.Simplification.batch.toString = "batch"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instToStringSimplification :

ToString Simplification

Equations

Cvc.Solver.Option.Smt.instToStringSimplification = { toString := Cvc.Solver.Option.Smt.Simplification.toString }

inductive Cvc.Solver.Option.Smt.SolveBvAsInt :

Solve-bv-as-int modes.

off : SolveBvAsInt
off: Do not translate bit-vectors to integers (the default).
sum : SolveBvAsInt
sum.
Generate a sum expression for each bvand instance, based on the value in --solve-bv-as-int-granularity.
iand : SolveBvAsInt
iand: Translate bvand to the iand operator.
bv : SolveBvAsInt
bv: Translate bvand back to bit-vectors.
bitwise : SolveBvAsInt
bitwise: Introduce a UF operator for bvand, and eagerly add bitwise lemmas.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instInhabitedSolveBvAsInt :

Inhabited SolveBvAsInt

Equations

Cvc.Solver.Option.Smt.instInhabitedSolveBvAsInt = { default := Cvc.Solver.Option.Smt.instInhabitedSolveBvAsInt.default }

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instDecidableEqSolveBvAsInt :

DecidableEq SolveBvAsInt

Equations

Cvc.Solver.Option.Smt.instDecidableEqSolveBvAsInt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instReprSolveBvAsInt :

Repr SolveBvAsInt

Equations

Cvc.Solver.Option.Smt.instReprSolveBvAsInt = { reprPrec := Cvc.Solver.Option.Smt.instReprSolveBvAsInt.repr }

def Cvc.Solver.Option.Smt.instReprSolveBvAsInt.repr :

SolveBvAsInt → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Smt.SolveBvAsInt.toString :

SolveBvAsInt → String

The string cvc5 expects for a value of --solve-bv-as-int.

Equations

Cvc.Solver.Option.Smt.SolveBvAsInt.off.toString = "off"
Cvc.Solver.Option.Smt.SolveBvAsInt.sum.toString = "sum"
Cvc.Solver.Option.Smt.SolveBvAsInt.iand.toString = "iand"
Cvc.Solver.Option.Smt.SolveBvAsInt.bv.toString = "bv"
Cvc.Solver.Option.Smt.SolveBvAsInt.bitwise.toString = "bitwise"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Smt.instToStringSolveBvAsInt :

ToString SolveBvAsInt

Equations

Cvc.Solver.Option.Smt.instToStringSolveBvAsInt = { toString := Cvc.Solver.Option.Smt.SolveBvAsInt.toString }

inductive Cvc.Solver.Option.Smt :

The SMT layer: what a check can produce, self-checks, preprocessing.

decision : Smt
--decision: Choose decision mode.
checkAbducts : Smt
--check-abducts: Checks whether produced solutions to get-abduct are correct.
checkInterpolants : Smt
--check-interpolants: Checks whether produced solutions to get-interpolant are correct.
checkModelSubsolver : Smt
--check-model-subsolver.
Use subsolver to compute values when applicable in calls to get-value and check-models.
checkModels : Smt
--check-models.
After SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions.
checkProofs : Smt
--check-proofs: After UNSAT/VALID, check the generated proof (with proof).
checkSynthSol : Smt
--check-synth-sol.
Checks whether produced solutions to functions-to-synthesize satisfy the conjecture.
checkUnsatCores : Smt
--check-unsat-cores: After UNSAT/VALID, produce and check an unsat core (expensive).
debugCheckModels : Smt
--debug-check-models.
After SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions.
produceModels : Smt
--produce-models: Support the get-value and get-model commands.
produceProofs : Smt
--produce-proofs: Produce proofs, support check-proofs and get-proof.
produceUnsatCores : Smt
--produce-unsat-cores.
Turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs.
interpolantsMode : Smt
--interpolants-mode: Choose interpolants production mode.
learnedRewrite : Smt
--learned-rewrite: Rewrite the input based on learned literals.
modelCores : Smt
--model-cores: Mode for producing model cores.
printCoresFull : Smt
--print-cores-full.
Print all formulas regardless of whether they are named, e.g. in unsat cores.
produceAbducts : Smt
--produce-abducts: Support the get-abduct command.
produceAssertions : Smt
--produce-assertions: Keep an assertions list. Note this option is always enabled.
produceAssignments : Smt
--produce-assignments: Support the get-assignment command.
produceDifficulty : Smt
--produce-difficulty: Enable tracking of difficulty.
produceInterpolants : Smt
--produce-interpolants: Turn on interpolation generation.
produceLearnedLiterals : Smt
--produce-learned-literals: Produce learned literals, support get-learned-literals.
produceUnsatAssumptions : Smt
--produce-unsat-assumptions: Turn on unsat assumptions generation.
simplification : Smt
--simplification: Choose simplification mode.
solveBvAsInt : Smt
--solve-bv-as-int: Mode for translating BVAnd to integer.
solveIntAsBv : Smt
--solve-int-as-bv.
Attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental).
solveRealAsInt : Smt
--solve-real-as-int.
Attempt to solve a pure real satisfiable problem as an integer problem (for non-linear).
staticLearning : Smt
--static-learning: Use static learning (on by default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedSmt :

Equations

Cvc.Solver.Option.instInhabitedSmt = { default := Cvc.Solver.Option.instInhabitedSmt.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqSmt :

DecidableEq Smt

Equations

Cvc.Solver.Option.instDecidableEqSmt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprSmt :

Equations

Cvc.Solver.Option.instReprSmt = { reprPrec := Cvc.Solver.Option.instReprSmt.repr }

def Cvc.Solver.Option.instReprSmt.repr :

Smt → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Smt.name :

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Smt.decision.name = "decision"
Cvc.Solver.Option.Smt.checkAbducts.name = "check-abducts"
Cvc.Solver.Option.Smt.checkInterpolants.name = "check-interpolants"
Cvc.Solver.Option.Smt.checkModelSubsolver.name = "check-model-subsolver"
Cvc.Solver.Option.Smt.checkModels.name = "check-models"
Cvc.Solver.Option.Smt.checkProofs.name = "check-proofs"
Cvc.Solver.Option.Smt.checkSynthSol.name = "check-synth-sol"
Cvc.Solver.Option.Smt.checkUnsatCores.name = "check-unsat-cores"
Cvc.Solver.Option.Smt.debugCheckModels.name = "debug-check-models"
Cvc.Solver.Option.Smt.produceModels.name = "produce-models"
Cvc.Solver.Option.Smt.produceProofs.name = "produce-proofs"
Cvc.Solver.Option.Smt.produceUnsatCores.name = "produce-unsat-cores"
Cvc.Solver.Option.Smt.interpolantsMode.name = "interpolants-mode"
Cvc.Solver.Option.Smt.learnedRewrite.name = "learned-rewrite"
Cvc.Solver.Option.Smt.modelCores.name = "model-cores"
Cvc.Solver.Option.Smt.printCoresFull.name = "print-cores-full"
Cvc.Solver.Option.Smt.produceAbducts.name = "produce-abducts"
Cvc.Solver.Option.Smt.produceAssertions.name = "produce-assertions"
Cvc.Solver.Option.Smt.produceAssignments.name = "produce-assignments"
Cvc.Solver.Option.Smt.produceDifficulty.name = "produce-difficulty"
Cvc.Solver.Option.Smt.produceInterpolants.name = "produce-interpolants"
Cvc.Solver.Option.Smt.produceLearnedLiterals.name = "produce-learned-literals"
Cvc.Solver.Option.Smt.produceUnsatAssumptions.name = "produce-unsat-assumptions"
Cvc.Solver.Option.Smt.simplification.name = "simplification"
Cvc.Solver.Option.Smt.solveBvAsInt.name = "solve-bv-as-int"
Cvc.Solver.Option.Smt.solveIntAsBv.name = "solve-int-as-bv"
Cvc.Solver.Option.Smt.solveRealAsInt.name = "solve-real-as-int"
Cvc.Solver.Option.Smt.staticLearning.name = "static-learning"

Instances For

@[reducible]

def Cvc.Solver.Option.Smt.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Smt.valueString (opt : Smt) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Printing.OutputLang :

Output languages.

auto : OutputLang
auto: Match output language to input language (the default).
smtLib : OutputLang
smt2: SMT-LIB format 2.6 with support for the strings standard.
ast : OutputLang
ast: Internal format (simple syntax trees).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instInhabitedOutputLang :

Inhabited OutputLang

Equations

Cvc.Solver.Option.Printing.instInhabitedOutputLang = { default := Cvc.Solver.Option.Printing.instInhabitedOutputLang.default }

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instDecidableEqOutputLang :

DecidableEq OutputLang

Equations

Cvc.Solver.Option.Printing.instDecidableEqOutputLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Printing.instReprOutputLang.repr :

OutputLang → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instReprOutputLang :

Repr OutputLang

Equations

Cvc.Solver.Option.Printing.instReprOutputLang = { reprPrec := Cvc.Solver.Option.Printing.instReprOutputLang.repr }

def Cvc.Solver.Option.Printing.OutputLang.toString :

OutputLang → String

The string cvc5 expects for a value of --output-lang.

Equations

Cvc.Solver.Option.Printing.OutputLang.auto.toString = "auto"
Cvc.Solver.Option.Printing.OutputLang.smtLib.toString = "smt2"
Cvc.Solver.Option.Printing.OutputLang.ast.toString = "ast"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instToStringOutputLang :

ToString OutputLang

Equations

Cvc.Solver.Option.Printing.instToStringOutputLang = { toString := Cvc.Solver.Option.Printing.OutputLang.toString }

inductive Cvc.Solver.Option.Printing.ModelUPrint :

Uninterpreted elements in models printing modes.

declSortAndFun : ModelUPrint
decl-sort-and-fun.
Print uninterpreted elements declare-fun, and also include a declare-sort for the sort.
declFun : ModelUPrint
decl-fun.
Print uninterpreted elements declare-fun, but don't include a declare-sort for the sort.
dt : ModelUPrint
dt: Print uninterpreted elements as a declare-datatype.
none : ModelUPrint
none.
(default) do not print declarations of uninterpreted elements in models (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instInhabitedModelUPrint :

Inhabited ModelUPrint

Equations

Cvc.Solver.Option.Printing.instInhabitedModelUPrint = { default := Cvc.Solver.Option.Printing.instInhabitedModelUPrint.default }

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instDecidableEqModelUPrint :

DecidableEq ModelUPrint

Equations

Cvc.Solver.Option.Printing.instDecidableEqModelUPrint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instReprModelUPrint :

Repr ModelUPrint

Equations

Cvc.Solver.Option.Printing.instReprModelUPrint = { reprPrec := Cvc.Solver.Option.Printing.instReprModelUPrint.repr }

def Cvc.Solver.Option.Printing.instReprModelUPrint.repr :

ModelUPrint → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Printing.ModelUPrint.toString :

ModelUPrint → String

The string cvc5 expects for a value of --model-u-print.

Equations

Cvc.Solver.Option.Printing.ModelUPrint.declSortAndFun.toString = "decl-sort-and-fun"
Cvc.Solver.Option.Printing.ModelUPrint.declFun.toString = "decl-fun"
Cvc.Solver.Option.Printing.ModelUPrint.dt.toString = "dt"
Cvc.Solver.Option.Printing.ModelUPrint.none.toString = "none"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Printing.instToStringModelUPrint :

ToString ModelUPrint

Equations

Cvc.Solver.Option.Printing.instToStringModelUPrint = { toString := Cvc.Solver.Option.Printing.ModelUPrint.toString }

inductive Cvc.Solver.Option.Printing :

How terms and models are printed.

printSuccess : Printing
--print-success: Print the "success" output required of SMT-LIBv2.
dagThresh : Printing
--dag-thresh.
Dagify common subexprs appearing > N times (1 == default, 0 == don't dagify).
exprDepth : Printing
--expr-depth: Print exprs to depth N (0 == default, -1 == no limit).
outputLang : Printing
--output-lang: Force output language.
bvPrintConstsAsIndexedSymbols : Printing
--bv-print-consts-as-indexed-symbols.
Print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x.
modelUPrint : Printing
--model-u-print: Determines how to print uninterpreted elements in models.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedPrinting :

Inhabited Printing

Equations

Cvc.Solver.Option.instInhabitedPrinting = { default := Cvc.Solver.Option.instInhabitedPrinting.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqPrinting :

DecidableEq Printing

Equations

Cvc.Solver.Option.instDecidableEqPrinting x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprPrinting.repr :

Printing → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprPrinting :

Equations

Cvc.Solver.Option.instReprPrinting = { reprPrec := Cvc.Solver.Option.instReprPrinting.repr }

def Cvc.Solver.Option.Printing.name :

Printing → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Printing.printSuccess.name = "print-success"
Cvc.Solver.Option.Printing.dagThresh.name = "dag-thresh"
Cvc.Solver.Option.Printing.exprDepth.name = "expr-depth"
Cvc.Solver.Option.Printing.outputLang.name = "output-lang"
Cvc.Solver.Option.Printing.bvPrintConstsAsIndexedSymbols.name = "bv-print-consts-as-indexed-symbols"
Cvc.Solver.Option.Printing.modelUPrint.name = "model-u-print"

Instances For

@[reducible]

def Cvc.Solver.Option.Printing.argType :

Printing → Type

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Printing.valueString (opt : Printing) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Proof.Check :

Internal proof checking modes.

eager : Check
eager: Check rule applications and proofs from generators eagerly for local debugging.
eagerSimple : Check
eager-simple: Check rule applications during construction.
lazy : Check
lazy: Check rule applications only during final proof construction.
none : Check
none: Do not check rule applications (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instInhabitedCheck :

Inhabited Check

Equations

Cvc.Solver.Option.Proof.instInhabitedCheck = { default := Cvc.Solver.Option.Proof.instInhabitedCheck.default }

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instDecidableEqCheck :

DecidableEq Check

Equations

Cvc.Solver.Option.Proof.instDecidableEqCheck x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Proof.instReprCheck.repr :

Check → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instReprCheck :

Equations

Cvc.Solver.Option.Proof.instReprCheck = { reprPrec := Cvc.Solver.Option.Proof.instReprCheck.repr }

def Cvc.Solver.Option.Proof.Check.toString :

Check → String

The string cvc5 expects for a value of --proof-check.

Equations

Cvc.Solver.Option.Proof.Check.eager.toString = "eager"
Cvc.Solver.Option.Proof.Check.eagerSimple.toString = "eager-simple"
Cvc.Solver.Option.Proof.Check.lazy.toString = "lazy"
Cvc.Solver.Option.Proof.Check.none.toString = "none"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instToStringCheck :

Equations

Cvc.Solver.Option.Proof.instToStringCheck = { toString := Cvc.Solver.Option.Proof.Check.toString }

inductive Cvc.Solver.Option.Proof.Granularity :

Modes for proof granularity.

macro : Granularity
macro: Allow macros. Do not improve the granularity of proofs (the default).
rewrite : Granularity
rewrite: Allow trusted rewrite or substitution steps, expand macros.
theoryRewrite : Granularity
theory-rewrite.
Allow trusted theory rewrite steps, expand macros, rewrite and substitution steps.
dslRewrite : Granularity
dsl-rewrite.
Allow theory and DSL rewrite steps, expand macros, rewrite, substitution, and theory rewrite steps.
dslRewriteStrict : Granularity
dsl-rewrite-strict.
Allow theory and DSL rewrite steps giving preference to DSL rewrite steps.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instInhabitedGranularity :

Inhabited Granularity

Equations

Cvc.Solver.Option.Proof.instInhabitedGranularity = { default := Cvc.Solver.Option.Proof.instInhabitedGranularity.default }

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instDecidableEqGranularity :

DecidableEq Granularity

Equations

Cvc.Solver.Option.Proof.instDecidableEqGranularity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instReprGranularity :

Repr Granularity

Equations

Cvc.Solver.Option.Proof.instReprGranularity = { reprPrec := Cvc.Solver.Option.Proof.instReprGranularity.repr }

def Cvc.Solver.Option.Proof.instReprGranularity.repr :

Granularity → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Proof.Granularity.toString :

Granularity → String

The string cvc5 expects for a value of --proof-granularity.

Equations

Cvc.Solver.Option.Proof.Granularity.macro.toString = "macro"
Cvc.Solver.Option.Proof.Granularity.rewrite.toString = "rewrite"
Cvc.Solver.Option.Proof.Granularity.theoryRewrite.toString = "theory-rewrite"
Cvc.Solver.Option.Proof.Granularity.dslRewrite.toString = "dsl-rewrite"
Cvc.Solver.Option.Proof.Granularity.dslRewriteStrict.toString = "dsl-rewrite-strict"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instToStringGranularity :

ToString Granularity

Equations

Cvc.Solver.Option.Proof.instToStringGranularity = { toString := Cvc.Solver.Option.Proof.Granularity.toString }

inductive Cvc.Solver.Option.Proof.PropProofMode :

Modes for the type of proof generated by the SAT solver.

proof : PropProofMode
proof: A proof computed by the SAT solver (the default).
satExternalProve : PropProofMode
sat-external-prove: A proof containing a step that will be proven externally.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instInhabitedPropProofMode :

Inhabited PropProofMode

Equations

Cvc.Solver.Option.Proof.instInhabitedPropProofMode = { default := Cvc.Solver.Option.Proof.instInhabitedPropProofMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instDecidableEqPropProofMode :

DecidableEq PropProofMode

Equations

Cvc.Solver.Option.Proof.instDecidableEqPropProofMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Proof.instReprPropProofMode.repr :

PropProofMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instReprPropProofMode :

Repr PropProofMode

Equations

Cvc.Solver.Option.Proof.instReprPropProofMode = { reprPrec := Cvc.Solver.Option.Proof.instReprPropProofMode.repr }

def Cvc.Solver.Option.Proof.PropProofMode.toString :

PropProofMode → String

The string cvc5 expects for a value of --prop-proof-mode.

Equations

Cvc.Solver.Option.Proof.PropProofMode.proof.toString = "proof"
Cvc.Solver.Option.Proof.PropProofMode.satExternalProve.toString = "sat-external-prove"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Proof.instToStringPropProofMode :

ToString PropProofMode

Equations

Cvc.Solver.Option.Proof.instToStringPropProofMode = { toString := Cvc.Solver.Option.Proof.PropProofMode.toString }

inductive Cvc.Solver.Option.Proof :

Proof production and checking.

check : Proof
--proof-check: Select internal proof checking mode.
granularity : Proof
--proof-granularity: Modes for proof granularity.
printConclusion : Proof
--proof-print-conclusion: Print conclusion of proof steps when printing AST.
printReference : Proof
--proof-print-reference: Print reference to original file instead of redeclaring.
optResReconstructionSize : Proof
--opt-res-reconstruction-size: Optimize resolution reconstruction to reduce proof size.
chainMRes : Proof
--proof-chain-m-res: Use chain multiset resolution.
rewriteRconsRecLimit : Proof
--proof-rewrite-rcons-rec-limit.
The matching recursion limit for reconstructing proofs of theory rewrites.
rewriteRconsStepLimit : Proof
--proof-rewrite-rcons-step-limit.
The limit of steps considered for reconstructing proofs of theory rewrites.
propProofMode : Proof
--prop-proof-mode: Modes for the type of proof generated by the SAT solver.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedProof :

Inhabited Proof

Equations

Cvc.Solver.Option.instInhabitedProof = { default := Cvc.Solver.Option.instInhabitedProof.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqProof :

DecidableEq Proof

Equations

Cvc.Solver.Option.instDecidableEqProof x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprProof :

Equations

Cvc.Solver.Option.instReprProof = { reprPrec := Cvc.Solver.Option.instReprProof.repr }

def Cvc.Solver.Option.instReprProof.repr :

Proof → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Proof.name :

Proof → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Proof.check.name = "proof-check"
Cvc.Solver.Option.Proof.granularity.name = "proof-granularity"
Cvc.Solver.Option.Proof.printConclusion.name = "proof-print-conclusion"
Cvc.Solver.Option.Proof.printReference.name = "proof-print-reference"
Cvc.Solver.Option.Proof.optResReconstructionSize.name = "opt-res-reconstruction-size"
Cvc.Solver.Option.Proof.chainMRes.name = "proof-chain-m-res"
Cvc.Solver.Option.Proof.rewriteRconsRecLimit.name = "proof-rewrite-rcons-rec-limit"
Cvc.Solver.Option.Proof.rewriteRconsStepLimit.name = "proof-rewrite-rcons-step-limit"
Cvc.Solver.Option.Proof.propProofMode.name = "prop-proof-mode"

Instances For

def Cvc.Solver.Option.Proof.valueString (opt : Proof) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Sat.PreregisterMode :

Modes for when to preregister literals.

eager : PreregisterMode
eager.
Preregister literals when they are registered as literals in the SAT solver (the default).
lazy : PreregisterMode
lazy: Preregister literals when they are asserted by the SAT solver.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sat.instInhabitedPreregisterMode :

Inhabited PreregisterMode

Equations

Cvc.Solver.Option.Sat.instInhabitedPreregisterMode = { default := Cvc.Solver.Option.Sat.instInhabitedPreregisterMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sat.instDecidableEqPreregisterMode :

DecidableEq PreregisterMode

Equations

Cvc.Solver.Option.Sat.instDecidableEqPreregisterMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sat.instReprPreregisterMode :

Repr PreregisterMode

Equations

Cvc.Solver.Option.Sat.instReprPreregisterMode = { reprPrec := Cvc.Solver.Option.Sat.instReprPreregisterMode.repr }

def Cvc.Solver.Option.Sat.instReprPreregisterMode.repr :

PreregisterMode → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sat.PreregisterMode.toString :

PreregisterMode → String

The string cvc5 expects for a value of --preregister-mode.

Equations

Cvc.Solver.Option.Sat.PreregisterMode.eager.toString = "eager"
Cvc.Solver.Option.Sat.PreregisterMode.lazy.toString = "lazy"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sat.instToStringPreregisterMode :

ToString PreregisterMode

Equations

Cvc.Solver.Option.Sat.instToStringPreregisterMode = { toString := Cvc.Solver.Option.Sat.PreregisterMode.toString }

inductive Cvc.Solver.Option.Sat :

The SAT layer.

preregisterMode : Sat
--preregister-mode: Modes for when to preregister literals.
randomSeed : Sat
--sat-random-seed: Sets the random seed for the sat solver.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedSat :

Equations

Cvc.Solver.Option.instInhabitedSat = { default := Cvc.Solver.Option.instInhabitedSat.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqSat :

DecidableEq Sat

Equations

Cvc.Solver.Option.instDecidableEqSat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprSat.repr :

Sat → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprSat :

Equations

Cvc.Solver.Option.instReprSat = { reprPrec := Cvc.Solver.Option.instReprSat.repr }

def Cvc.Solver.Option.Sat.name :

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Sat.preregisterMode.name = "preregister-mode"
Cvc.Solver.Option.Sat.randomSeed.name = "sat-random-seed"

Instances For

@[reducible]

def Cvc.Solver.Option.Sat.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Sat.valueString (opt : Sat) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Theory.DefaultFunctionValueMode :

Defines mode for choosing default values for functions.

first : DefaultFunctionValueMode
first.
The default value is equal to the value of the first application found of that function when applicable, or the first enumerated term otherwise (the default).
firstEnum : DefaultFunctionValueMode
first-enum: The default value is equal to the first enumerated value of its range type.
hole : DefaultFunctionValueMode
hole: The default value is equal to a distinguished variable.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instInhabitedDefaultFunctionValueMode :

Inhabited DefaultFunctionValueMode

Equations

Cvc.Solver.Option.Theory.instInhabitedDefaultFunctionValueMode = { default := Cvc.Solver.Option.Theory.instInhabitedDefaultFunctionValueMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instDecidableEqDefaultFunctionValueMode :

DecidableEq DefaultFunctionValueMode

Equations

Cvc.Solver.Option.Theory.instDecidableEqDefaultFunctionValueMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instReprDefaultFunctionValueMode :

Repr DefaultFunctionValueMode

Equations

Cvc.Solver.Option.Theory.instReprDefaultFunctionValueMode = { reprPrec := Cvc.Solver.Option.Theory.instReprDefaultFunctionValueMode.repr }

def Cvc.Solver.Option.Theory.instReprDefaultFunctionValueMode.repr :

DefaultFunctionValueMode → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Theory.DefaultFunctionValueMode.toString :

DefaultFunctionValueMode → String

The string cvc5 expects for a value of --default-function-value-mode.

Equations

Cvc.Solver.Option.Theory.DefaultFunctionValueMode.first.toString = "first"
Cvc.Solver.Option.Theory.DefaultFunctionValueMode.firstEnum.toString = "first-enum"
Cvc.Solver.Option.Theory.DefaultFunctionValueMode.hole.toString = "hole"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instToStringDefaultFunctionValueMode :

ToString DefaultFunctionValueMode

Equations

Cvc.Solver.Option.Theory.instToStringDefaultFunctionValueMode = { toString := Cvc.Solver.Option.Theory.DefaultFunctionValueMode.toString }

inductive Cvc.Solver.Option.Theory.EeMode :

Defines mode for managing equalities across theory solvers.

distributed : EeMode
distributed: Each theory maintains its own equality engine (the default).
central : EeMode
central: All applicable theories use the central equality engine.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instInhabitedEeMode :

Inhabited EeMode

Equations

Cvc.Solver.Option.Theory.instInhabitedEeMode = { default := Cvc.Solver.Option.Theory.instInhabitedEeMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instDecidableEqEeMode :

DecidableEq EeMode

Equations

Cvc.Solver.Option.Theory.instDecidableEqEeMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instReprEeMode :

Equations

Cvc.Solver.Option.Theory.instReprEeMode = { reprPrec := Cvc.Solver.Option.Theory.instReprEeMode.repr }

def Cvc.Solver.Option.Theory.instReprEeMode.repr :

EeMode → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Theory.EeMode.toString :

EeMode → String

The string cvc5 expects for a value of --ee-mode.

Equations

Cvc.Solver.Option.Theory.EeMode.distributed.toString = "distributed"
Cvc.Solver.Option.Theory.EeMode.central.toString = "central"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Theory.instToStringEeMode :

ToString EeMode

Equations

Cvc.Solver.Option.Theory.instToStringEeMode = { toString := Cvc.Solver.Option.Theory.EeMode.toString }

inductive Cvc.Solver.Option.Theory :

The theory layer, shared by every theory.

condenseFunctionValues : Theory
--condense-function-values.
Condense values for functions in models rather than explicitly representing them.
defaultFunctionValueMode : Theory
--default-function-value-mode: Mode for choosing default values for functions.
eeMode : Theory
--ee-mode: Mode for managing equalities across theory solvers.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedTheory :

Inhabited Theory

Equations

Cvc.Solver.Option.instInhabitedTheory = { default := Cvc.Solver.Option.instInhabitedTheory.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqTheory :

DecidableEq Theory

Equations

Cvc.Solver.Option.instDecidableEqTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprTheory :

Equations

Cvc.Solver.Option.instReprTheory = { reprPrec := Cvc.Solver.Option.instReprTheory.repr }

def Cvc.Solver.Option.instReprTheory.repr :

Theory → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Theory.name :

Theory → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Theory.condenseFunctionValues.name = "condense-function-values"
Cvc.Solver.Option.Theory.defaultFunctionValueMode.name = "default-function-value-mode"
Cvc.Solver.Option.Theory.eeMode.name = "ee-mode"

Instances For

@[reducible]

def Cvc.Solver.Option.Theory.argType :

Theory → Type

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Theory.valueString (opt : Theory) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Arith.NlCovLinearModel :

Modes for the usage of the linear model in non-linear arithmetic.

none : NlCovLinearModel
none: Do not use linear model to seed nonlinear model (the default).
initial : NlCovLinearModel
initial.
Use linear model to seed nonlinear model initially, discard it when it does not work.
persistent : NlCovLinearModel
persistent: Use linear model to seed nonlinear model whenever possible.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instInhabitedNlCovLinearModel :

Inhabited NlCovLinearModel

Equations

Cvc.Solver.Option.Arith.instInhabitedNlCovLinearModel = { default := Cvc.Solver.Option.Arith.instInhabitedNlCovLinearModel.default }

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instDecidableEqNlCovLinearModel :

DecidableEq NlCovLinearModel

Equations

Cvc.Solver.Option.Arith.instDecidableEqNlCovLinearModel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instReprNlCovLinearModel :

Repr NlCovLinearModel

Equations

Cvc.Solver.Option.Arith.instReprNlCovLinearModel = { reprPrec := Cvc.Solver.Option.Arith.instReprNlCovLinearModel.repr }

def Cvc.Solver.Option.Arith.instReprNlCovLinearModel.repr :

NlCovLinearModel → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Arith.NlCovLinearModel.toString :

NlCovLinearModel → String

The string cvc5 expects for a value of --nl-cov-linear-model.

Equations

Cvc.Solver.Option.Arith.NlCovLinearModel.none.toString = "none"
Cvc.Solver.Option.Arith.NlCovLinearModel.initial.toString = "initial"
Cvc.Solver.Option.Arith.NlCovLinearModel.persistent.toString = "persistent"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instToStringNlCovLinearModel :

ToString NlCovLinearModel

Equations

Cvc.Solver.Option.Arith.instToStringNlCovLinearModel = { toString := Cvc.Solver.Option.Arith.NlCovLinearModel.toString }

inductive Cvc.Solver.Option.Arith.NlExt :

Modes for the non-linear linearization.

none : NlExt
none: Disable linearization approach.
light : NlExt
light: Only use a few light-weight lemma schemes.
full : NlExt
full: Use all lemma schemes (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instInhabitedNlExt :

Inhabited NlExt

Equations

Cvc.Solver.Option.Arith.instInhabitedNlExt = { default := Cvc.Solver.Option.Arith.instInhabitedNlExt.default }

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instDecidableEqNlExt :

DecidableEq NlExt

Equations

Cvc.Solver.Option.Arith.instDecidableEqNlExt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instReprNlExt :

Equations

Cvc.Solver.Option.Arith.instReprNlExt = { reprPrec := Cvc.Solver.Option.Arith.instReprNlExt.repr }

def Cvc.Solver.Option.Arith.instReprNlExt.repr :

NlExt → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Arith.NlExt.toString :

NlExt → String

The string cvc5 expects for a value of --nl-ext.

Equations

Cvc.Solver.Option.Arith.NlExt.none.toString = "none"
Cvc.Solver.Option.Arith.NlExt.light.toString = "light"
Cvc.Solver.Option.Arith.NlExt.full.toString = "full"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Arith.instToStringNlExt :

Equations

Cvc.Solver.Option.Arith.instToStringNlExt = { toString := Cvc.Solver.Option.Arith.NlExt.toString }

inductive Cvc.Solver.Option.Arith :

The arithmetic theory.

brab : Arith
--arith-brab: Whether to use simple rounding, similar to a unit-cube test, for integers.
rewriteEqualities : Arith
--arith-rewrite-equalities.
Turns on the preprocessing rewrite turning equalities into a conjunction of inequalities.
staticLearning : Arith
--arith-static-learning.
Do arithmetic static learning for ite terms based on bounds when static learning is enabled.
nlCov : Arith
--nl-cov.
Whether to use the cylindrical algebraic coverings solver for non-linear arithmetic.
nlCovLinearModel : Arith
--nl-cov-linear-model.
Whether to use the linear model as initial guess for the cylindrical algebraic coverings solver.
nlExt : Arith
--nl-ext: Incremental linearization approach to non-linear.
nlExtFactor : Arith
--nl-ext-factor: Use factoring inference in non-linear incremental linearization solver.
nlExtFlattenMon : Arith
--nl-ext-flatten-mon: Use inference schema based on flattening monomials.
nlExtRewrite : Arith
--nl-ext-rewrite.
Do context-dependent simplification based on rewrites in non-linear solver.
nlExtTfTplanes : Arith
--nl-ext-tf-tplanes.
Use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver.
nlExtTplanes : Arith
--nl-ext-tplanes.
Use non-terminating tangent plane strategy for non-linear incremental linearization solver.
nlExtTplanesInterleave : Arith
--nl-ext-tplanes-interleave.
Interleave tangent plane strategy for non-linear incremental linearization solver.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedArith :

Inhabited Arith

Equations

Cvc.Solver.Option.instInhabitedArith = { default := Cvc.Solver.Option.instInhabitedArith.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqArith :

DecidableEq Arith

Equations

Cvc.Solver.Option.instDecidableEqArith x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprArith :

Equations

Cvc.Solver.Option.instReprArith = { reprPrec := Cvc.Solver.Option.instReprArith.repr }

def Cvc.Solver.Option.instReprArith.repr :

Arith → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Arith.name :

Arith → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Arith.brab.name = "arith-brab"
Cvc.Solver.Option.Arith.rewriteEqualities.name = "arith-rewrite-equalities"
Cvc.Solver.Option.Arith.staticLearning.name = "arith-static-learning"
Cvc.Solver.Option.Arith.nlCov.name = "nl-cov"
Cvc.Solver.Option.Arith.nlCovLinearModel.name = "nl-cov-linear-model"
Cvc.Solver.Option.Arith.nlExt.name = "nl-ext"
Cvc.Solver.Option.Arith.nlExtFactor.name = "nl-ext-factor"
Cvc.Solver.Option.Arith.nlExtFlattenMon.name = "nl-ext-flatten-mon"
Cvc.Solver.Option.Arith.nlExtRewrite.name = "nl-ext-rewrite"
Cvc.Solver.Option.Arith.nlExtTfTplanes.name = "nl-ext-tf-tplanes"
Cvc.Solver.Option.Arith.nlExtTplanes.name = "nl-ext-tplanes"
Cvc.Solver.Option.Arith.nlExtTplanesInterleave.name = "nl-ext-tplanes-interleave"

Instances For

def Cvc.Solver.Option.Arith.valueString (opt : Arith) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Arrays :

The theory of arrays.

eagerIndex : Arrays
--arrays-eager-index: Turn on eager index splitting for generated array lemmas.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedArrays :

Inhabited Arrays

Equations

Cvc.Solver.Option.instInhabitedArrays = { default := Cvc.Solver.Option.instInhabitedArrays.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqArrays :

DecidableEq Arrays

Equations

Cvc.Solver.Option.instDecidableEqArrays x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprArrays.repr :

Arrays → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprArrays :

Equations

Cvc.Solver.Option.instReprArrays = { reprPrec := Cvc.Solver.Option.instReprArrays.repr }

def Cvc.Solver.Option.Arrays.name :

Arrays → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Arrays.eagerIndex.name = "arrays-eager-index"

Instances For

@[reducible]

def Cvc.Solver.Option.Arrays.argType :

Arrays → Type

The type of the value the option expects.

Equations

Cvc.Solver.Option.Arrays.eagerIndex.argType = Bool

Instances For

def Cvc.Solver.Option.Arrays.valueString (opt : Arrays) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Cvc.Solver.Option.Arrays.eagerIndex.valueString v = toString v

Instances For

inductive Cvc.Solver.Option.Bv.Bitblast :

Bit-blasting modes.

lazy : Bitblast
lazy.
Separate Boolean structure and term reasoning between the core SAT solver and the bit-vector SAT solver (the default).
eager : Bitblast
eager: Bitblast eagerly to bit-vector SAT solver.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instInhabitedBitblast :

Inhabited Bitblast

Equations

Cvc.Solver.Option.Bv.instInhabitedBitblast = { default := Cvc.Solver.Option.Bv.instInhabitedBitblast.default }

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instDecidableEqBitblast :

DecidableEq Bitblast

Equations

Cvc.Solver.Option.Bv.instDecidableEqBitblast x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Bv.instReprBitblast.repr :

Bitblast → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instReprBitblast :

Equations

Cvc.Solver.Option.Bv.instReprBitblast = { reprPrec := Cvc.Solver.Option.Bv.instReprBitblast.repr }

def Cvc.Solver.Option.Bv.Bitblast.toString :

Bitblast → String

The string cvc5 expects for a value of --bitblast.

Equations

Cvc.Solver.Option.Bv.Bitblast.lazy.toString = "lazy"
Cvc.Solver.Option.Bv.Bitblast.eager.toString = "eager"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instToStringBitblast :

ToString Bitblast

Equations

Cvc.Solver.Option.Bv.instToStringBitblast = { toString := Cvc.Solver.Option.Bv.Bitblast.toString }

inductive Cvc.Solver.Option.Bv.BoolToBv :

BoolToBV preprocessing pass modes.

off : BoolToBv
off: Don't push any booleans to width one bit-vectors (the default).
ite : BoolToBv
ite.
Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula if not all sub-formulas can be turned to bit-vectors.
all : BoolToBv
all.
Force all booleans to be bit-vectors of width one except at the top level. Most aggressive mode.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instInhabitedBoolToBv :

Inhabited BoolToBv

Equations

Cvc.Solver.Option.Bv.instInhabitedBoolToBv = { default := Cvc.Solver.Option.Bv.instInhabitedBoolToBv.default }

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instDecidableEqBoolToBv :

DecidableEq BoolToBv

Equations

Cvc.Solver.Option.Bv.instDecidableEqBoolToBv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instReprBoolToBv :

Equations

Cvc.Solver.Option.Bv.instReprBoolToBv = { reprPrec := Cvc.Solver.Option.Bv.instReprBoolToBv.repr }

def Cvc.Solver.Option.Bv.instReprBoolToBv.repr :

BoolToBv → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Bv.BoolToBv.toString :

BoolToBv → String

The string cvc5 expects for a value of --bool-to-bv.

Equations

Cvc.Solver.Option.Bv.BoolToBv.off.toString = "off"
Cvc.Solver.Option.Bv.BoolToBv.ite.toString = "ite"
Cvc.Solver.Option.Bv.BoolToBv.all.toString = "all"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instToStringBoolToBv :

ToString BoolToBv

Equations

Cvc.Solver.Option.Bv.instToStringBoolToBv = { toString := Cvc.Solver.Option.Bv.BoolToBv.toString }

inductive Cvc.Solver.Option.Bv.SatSolver :

SAT solvers for the bit-blasting backend.

minisat : SatSolver
minisat: MiniSat.
cadical : SatSolver
cadical: CaDiCaL (the default).
cryptominisat : SatSolver
cryptominisat: CryptoMiniSat, only available in a cvc5 built with it.
kissat : SatSolver
kissat: Kissat, only available in a cvc5 built with it.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instInhabitedSatSolver :

Inhabited SatSolver

Equations

Cvc.Solver.Option.Bv.instInhabitedSatSolver = { default := Cvc.Solver.Option.Bv.instInhabitedSatSolver.default }

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instDecidableEqSatSolver :

DecidableEq SatSolver

Equations

Cvc.Solver.Option.Bv.instDecidableEqSatSolver x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instReprSatSolver :

Equations

Cvc.Solver.Option.Bv.instReprSatSolver = { reprPrec := Cvc.Solver.Option.Bv.instReprSatSolver.repr }

def Cvc.Solver.Option.Bv.instReprSatSolver.repr :

SatSolver → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Bv.SatSolver.toString :

SatSolver → String

The string cvc5 expects for a value of --bv-sat-solver.

Equations

Cvc.Solver.Option.Bv.SatSolver.minisat.toString = "minisat"
Cvc.Solver.Option.Bv.SatSolver.cadical.toString = "cadical"
Cvc.Solver.Option.Bv.SatSolver.cryptominisat.toString = "cryptominisat"
Cvc.Solver.Option.Bv.SatSolver.kissat.toString = "kissat"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instToStringSatSolver :

ToString SatSolver

Equations

Cvc.Solver.Option.Bv.instToStringSatSolver = { toString := Cvc.Solver.Option.Bv.SatSolver.toString }

inductive Cvc.Solver.Option.Bv.Solver :

Bit-vector solvers.

bitblast : Solver
bitblast: Enables bitblasting solver (the default).
bitblastInternal : Solver
bitblast-internal: Enables bitblasting to internal SAT solver with proof support.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instInhabitedSolver :

Inhabited Solver

Equations

Cvc.Solver.Option.Bv.instInhabitedSolver = { default := Cvc.Solver.Option.Bv.instInhabitedSolver.default }

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instDecidableEqSolver :

DecidableEq Solver

Equations

Cvc.Solver.Option.Bv.instDecidableEqSolver x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instReprSolver :

Equations

Cvc.Solver.Option.Bv.instReprSolver = { reprPrec := Cvc.Solver.Option.Bv.instReprSolver.repr }

def Cvc.Solver.Option.Bv.instReprSolver.repr :

Solver → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Bv.Solver.toString :

Solver → String

The string cvc5 expects for a value of --bv-solver.

Equations

Cvc.Solver.Option.Bv.Solver.bitblast.toString = "bitblast"
Cvc.Solver.Option.Bv.Solver.bitblastInternal.toString = "bitblast-internal"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Bv.instToStringSolver :

ToString Solver

Equations

Cvc.Solver.Option.Bv.instToStringSolver = { toString := Cvc.Solver.Option.Bv.Solver.toString }

inductive Cvc.Solver.Option.Bv :

The bit-vector theory.

bitblast : Bv
--bitblast: Choose bitblasting mode.
boolToBv : Bv
--bool-to-bv.
Convert booleans to bit-vectors of size 1 at various levels of aggressiveness.
eagerEval : Bv
--bv-eager-eval.
Perform eager context-dependent evaluation for applications of bv kinds in the equality engine.
satSolver : Bv
--bv-sat-solver: Choose which sat solver to use.
solver : Bv
--bv-solver: Choose bit-vector solver.
toBool : Bv
--bv-to-bool: Lift bit-vectors of size 1 to booleans when possible.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedBv :

Equations

Cvc.Solver.Option.instInhabitedBv = { default := Cvc.Solver.Option.instInhabitedBv.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqBv :

Equations

Cvc.Solver.Option.instDecidableEqBv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprBv :

Equations

Cvc.Solver.Option.instReprBv = { reprPrec := Cvc.Solver.Option.instReprBv.repr }

def Cvc.Solver.Option.instReprBv.repr :

Bv → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Bv.name :

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Bv.bitblast.name = "bitblast"
Cvc.Solver.Option.Bv.boolToBv.name = "bool-to-bv"
Cvc.Solver.Option.Bv.eagerEval.name = "bv-eager-eval"
Cvc.Solver.Option.Bv.satSolver.name = "bv-sat-solver"
Cvc.Solver.Option.Bv.solver.name = "bv-solver"
Cvc.Solver.Option.Bv.toBool.name = "bv-to-bool"

Instances For

@[reducible]

def Cvc.Solver.Option.Bv.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Bv.valueString (opt : Bv) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Strings.ReElim :

Regular expression elimination modes.

off : ReElim
off: Do not use regular expression elimination (the default).
on : ReElim
on: Use regular expression elimination.
agg : ReElim
agg: Use aggressive regular expression elimination.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instInhabitedReElim :

Inhabited ReElim

Equations

Cvc.Solver.Option.Strings.instInhabitedReElim = { default := Cvc.Solver.Option.Strings.instInhabitedReElim.default }

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instDecidableEqReElim :

DecidableEq ReElim

Equations

Cvc.Solver.Option.Strings.instDecidableEqReElim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Strings.instReprReElim.repr :

ReElim → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instReprReElim :

Equations

Cvc.Solver.Option.Strings.instReprReElim = { reprPrec := Cvc.Solver.Option.Strings.instReprReElim.repr }

def Cvc.Solver.Option.Strings.ReElim.toString :

ReElim → String

The string cvc5 expects for a value of --re-elim.

Equations

Cvc.Solver.Option.Strings.ReElim.off.toString = "off"
Cvc.Solver.Option.Strings.ReElim.on.toString = "on"
Cvc.Solver.Option.Strings.ReElim.agg.toString = "agg"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instToStringReElim :

ToString ReElim

Equations

Cvc.Solver.Option.Strings.instToStringReElim = { toString := Cvc.Solver.Option.Strings.ReElim.toString }

inductive Cvc.Solver.Option.Strings.ProcessLoopMode :

Loop processing modes.

full : ProcessLoopMode
full: Perform full processing of looping word equations (the default).
simple : ProcessLoopMode
simple: Omit normal loop breaking (default with --strings-fmf).
simpleAbort : ProcessLoopMode
simple-abort: Abort when normal loop breaking is required.
none : ProcessLoopMode
none: Omit loop processing.
abort : ProcessLoopMode
abort: Abort if looping word equations are encountered.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instInhabitedProcessLoopMode :

Inhabited ProcessLoopMode

Equations

Cvc.Solver.Option.Strings.instInhabitedProcessLoopMode = { default := Cvc.Solver.Option.Strings.instInhabitedProcessLoopMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instDecidableEqProcessLoopMode :

DecidableEq ProcessLoopMode

Equations

Cvc.Solver.Option.Strings.instDecidableEqProcessLoopMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Strings.instReprProcessLoopMode.repr :

ProcessLoopMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instReprProcessLoopMode :

Repr ProcessLoopMode

Equations

Cvc.Solver.Option.Strings.instReprProcessLoopMode = { reprPrec := Cvc.Solver.Option.Strings.instReprProcessLoopMode.repr }

def Cvc.Solver.Option.Strings.ProcessLoopMode.toString :

ProcessLoopMode → String

The string cvc5 expects for a value of --strings-process-loop-mode.

Equations

Cvc.Solver.Option.Strings.ProcessLoopMode.full.toString = "full"
Cvc.Solver.Option.Strings.ProcessLoopMode.simple.toString = "simple"
Cvc.Solver.Option.Strings.ProcessLoopMode.simpleAbort.toString = "simple-abort"
Cvc.Solver.Option.Strings.ProcessLoopMode.none.toString = "none"
Cvc.Solver.Option.Strings.ProcessLoopMode.abort.toString = "abort"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Strings.instToStringProcessLoopMode :

ToString ProcessLoopMode

Equations

Cvc.Solver.Option.Strings.instToStringProcessLoopMode = { toString := Cvc.Solver.Option.Strings.ProcessLoopMode.toString }

inductive Cvc.Solver.Option.Strings :

The theory of strings and sequences.

reElim : Strings
--re-elim: Regular expression elimination mode.
checkEntailLen : Strings
--strings-check-entail-len: Check entailment between length terms to reduce splitting.
deqExt : Strings
--strings-deq-ext: Use extensionality for string disequalities.
eagerEval : Strings
--strings-eager-eval.
Perform eager context-dependent evaluation for applications of string kinds in the equality engine.
eagerLenRe : Strings
--strings-eager-len-re: Use regular expressions for eager length conflicts.
eagerSolver : Strings
--strings-eager-solver: Use the eager solver.
exp : Strings
--strings-exp: Experimental features in the theory of strings.
fmf : Strings
--strings-fmf: The finite model finding used by the theory of strings.
lazyPp : Strings
--strings-lazy-pp: Perform string preprocessing lazily.
mbr : Strings
--strings-mbr.
Use models to avoid reductions for extended functions that introduce quantified formulas.
processLoopMode : Strings
--strings-process-loop-mode: Determines how to process looping string equations.
regexpInclusion : Strings
--strings-regexp-inclusion.
Use regular expression inclusion for finding conflicts and avoiding regular expression unfolding.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedStrings :

Inhabited Strings

Equations

Cvc.Solver.Option.instInhabitedStrings = { default := Cvc.Solver.Option.instInhabitedStrings.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqStrings :

DecidableEq Strings

Equations

Cvc.Solver.Option.instDecidableEqStrings x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprStrings.repr :

Strings → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprStrings :

Equations

Cvc.Solver.Option.instReprStrings = { reprPrec := Cvc.Solver.Option.instReprStrings.repr }

def Cvc.Solver.Option.Strings.name :

Strings → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Strings.reElim.name = "re-elim"
Cvc.Solver.Option.Strings.checkEntailLen.name = "strings-check-entail-len"
Cvc.Solver.Option.Strings.deqExt.name = "strings-deq-ext"
Cvc.Solver.Option.Strings.eagerEval.name = "strings-eager-eval"
Cvc.Solver.Option.Strings.eagerLenRe.name = "strings-eager-len-re"
Cvc.Solver.Option.Strings.eagerSolver.name = "strings-eager-solver"
Cvc.Solver.Option.Strings.exp.name = "strings-exp"
Cvc.Solver.Option.Strings.fmf.name = "strings-fmf"
Cvc.Solver.Option.Strings.lazyPp.name = "strings-lazy-pp"
Cvc.Solver.Option.Strings.mbr.name = "strings-mbr"
Cvc.Solver.Option.Strings.processLoopMode.name = "strings-process-loop-mode"
Cvc.Solver.Option.Strings.regexpInclusion.name = "strings-regexp-inclusion"

Instances For

def Cvc.Solver.Option.Strings.valueString (opt : Strings) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Uf.Ss :

Values of --uf-ss.

UF with cardinality options currently supported by the --uf-ss option when combined with finite model finding.

full : Ss
full.
Default, use UF with cardinality to find minimal models for uninterpreted sorts (the default).
noMinimal : Ss
no-minimal: Use UF with cardinality to shrink models, but do no enforce minimality.
none : Ss
none: Do not use UF with cardinality to shrink model sizes.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Uf.instInhabitedSs :

Equations

Cvc.Solver.Option.Uf.instInhabitedSs = { default := Cvc.Solver.Option.Uf.instInhabitedSs.default }

@[instance_reducible]

instance Cvc.Solver.Option.Uf.instDecidableEqSs :

Equations

Cvc.Solver.Option.Uf.instDecidableEqSs x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Uf.instReprSs.repr :

Ss → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Uf.instReprSs :

Equations

Cvc.Solver.Option.Uf.instReprSs = { reprPrec := Cvc.Solver.Option.Uf.instReprSs.repr }

def Cvc.Solver.Option.Uf.Ss.toString :

The string cvc5 expects for a value of --uf-ss.

Equations

Cvc.Solver.Option.Uf.Ss.full.toString = "full"
Cvc.Solver.Option.Uf.Ss.noMinimal.toString = "no-minimal"
Cvc.Solver.Option.Uf.Ss.none.toString = "none"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Uf.instToStringSs :

Equations

Cvc.Solver.Option.Uf.instToStringSs = { toString := Cvc.Solver.Option.Uf.Ss.toString }

inductive Cvc.Solver.Option.Uf :

Uninterpreted functions.

eagerArithBvConv : Uf
--eager-arith-bv-conv.
Eagerly expand bit-vector to arithmetic conversions during preprocessing.
symmetryBreaker : Uf
--symmetry-breaker: Use UF symmetry breaker (Deharbe et al., CADE 2011).
lazyLl : Uf
--uf-lazy-ll: Do lambda lifting lazily.
ss : Uf
--uf-ss: Mode of operation for uf with cardinality solver.
ssAbortCard : Uf
--uf-ss-abort-card.
Tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default).
ssFair : Uf
--uf-ss-fair: Use fair strategy for finite model finding multiple sorts.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedUf :

Equations

Cvc.Solver.Option.instInhabitedUf = { default := Cvc.Solver.Option.instInhabitedUf.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqUf :

Equations

Cvc.Solver.Option.instDecidableEqUf x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprUf.repr :

Uf → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
Cvc.Solver.Option.instReprUf.repr Cvc.Solver.Option.Uf.ss prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cvc.Solver.Option.Uf.ss")).group prec✝

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprUf :

Equations

Cvc.Solver.Option.instReprUf = { reprPrec := Cvc.Solver.Option.instReprUf.repr }

def Cvc.Solver.Option.Uf.name :

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Uf.eagerArithBvConv.name = "eager-arith-bv-conv"
Cvc.Solver.Option.Uf.symmetryBreaker.name = "symmetry-breaker"
Cvc.Solver.Option.Uf.lazyLl.name = "uf-lazy-ll"
Cvc.Solver.Option.Uf.ss.name = "uf-ss"
Cvc.Solver.Option.Uf.ssAbortCard.name = "uf-ss-abort-card"
Cvc.Solver.Option.Uf.ssFair.name = "uf-ss-fair"

Instances For

@[reducible]

def Cvc.Solver.Option.Uf.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Uf.valueString (opt : Uf) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Quant.PrintInst :

Print format for printing instantiations.

list : PrintInst
list.
Print the list of instantiations per quantified formula, when non-empty (the default).
num : PrintInst
num: Print the total number of instantiations per quantified formula, when non-zero.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedPrintInst :

Inhabited PrintInst

Equations

Cvc.Solver.Option.Quant.instInhabitedPrintInst = { default := Cvc.Solver.Option.Quant.instInhabitedPrintInst.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqPrintInst :

DecidableEq PrintInst

Equations

Cvc.Solver.Option.Quant.instDecidableEqPrintInst x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprPrintInst.repr :

PrintInst → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprPrintInst :

Equations

Cvc.Solver.Option.Quant.instReprPrintInst = { reprPrec := Cvc.Solver.Option.Quant.instReprPrintInst.repr }

def Cvc.Solver.Option.Quant.PrintInst.toString :

PrintInst → String

The string cvc5 expects for a value of --print-inst.

Equations

Cvc.Solver.Option.Quant.PrintInst.list.toString = "list"
Cvc.Solver.Option.Quant.PrintInst.num.toString = "num"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringPrintInst :

ToString PrintInst

Equations

Cvc.Solver.Option.Quant.instToStringPrintInst = { toString := Cvc.Solver.Option.Quant.PrintInst.toString }

inductive Cvc.Solver.Option.Quant.CbqiMode :

Quantifier conflict find modes.

conflict : CbqiMode
conflict: Apply QCF algorithm to find conflicts only.
propEq : CbqiMode
prop-eq: Apply QCF algorithm to propagate equalities as well as conflicts (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedCbqiMode :

Inhabited CbqiMode

Equations

Cvc.Solver.Option.Quant.instInhabitedCbqiMode = { default := Cvc.Solver.Option.Quant.instInhabitedCbqiMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqCbqiMode :

DecidableEq CbqiMode

Equations

Cvc.Solver.Option.Quant.instDecidableEqCbqiMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprCbqiMode.repr :

CbqiMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprCbqiMode :

Equations

Cvc.Solver.Option.Quant.instReprCbqiMode = { reprPrec := Cvc.Solver.Option.Quant.instReprCbqiMode.repr }

def Cvc.Solver.Option.Quant.CbqiMode.toString :

CbqiMode → String

The string cvc5 expects for a value of --cbqi-mode.

Equations

Cvc.Solver.Option.Quant.CbqiMode.conflict.toString = "conflict"
Cvc.Solver.Option.Quant.CbqiMode.propEq.toString = "prop-eq"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringCbqiMode :

ToString CbqiMode

Equations

Cvc.Solver.Option.Quant.instToStringCbqiMode = { toString := Cvc.Solver.Option.Quant.CbqiMode.toString }

inductive Cvc.Solver.Option.Quant.Ieval :

Mode for using instantiation evaluation.

off : Ieval
off: Do not use instantiation evaluation.
use : Ieval
use: Use instantiation evaluation (the default).
useLearn : Ieval
use-learn: Use instantiation evaluation, and generalize learning.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedIeval :

Inhabited Ieval

Equations

Cvc.Solver.Option.Quant.instInhabitedIeval = { default := Cvc.Solver.Option.Quant.instInhabitedIeval.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqIeval :

DecidableEq Ieval

Equations

Cvc.Solver.Option.Quant.instDecidableEqIeval x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprIeval :

Equations

Cvc.Solver.Option.Quant.instReprIeval = { reprPrec := Cvc.Solver.Option.Quant.instReprIeval.repr }

def Cvc.Solver.Option.Quant.instReprIeval.repr :

Ieval → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Quant.Ieval.toString :

Ieval → String

The string cvc5 expects for a value of --ieval.

Equations

Cvc.Solver.Option.Quant.Ieval.off.toString = "off"
Cvc.Solver.Option.Quant.Ieval.use.toString = "use"
Cvc.Solver.Option.Quant.Ieval.useLearn.toString = "use-learn"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringIeval :

Equations

Cvc.Solver.Option.Quant.instToStringIeval = { toString := Cvc.Solver.Option.Quant.Ieval.toString }

inductive Cvc.Solver.Option.Quant.InstWhen :

Instantiation modes.

full : InstWhen
full: Run instantiation round at full effort, before theory combination.
fullDelay : InstWhen
full-delay.
Run instantiation round at full effort, before theory combination, after all other theories have finished.
fullLastCall : InstWhen
full-last-call.
Alternate running instantiation rounds at full effort and last call. In other words, interleave instantiation and theory combination (the default).
fullDelayLastCall : InstWhen
full-delay-last-call.
Alternate running instantiation rounds at full effort after all other theories have finished, and last call.
lastCall : InstWhen
last-call.
Run instantiation at last call effort, after theory combination and and theories report sat.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedInstWhen :

Inhabited InstWhen

Equations

Cvc.Solver.Option.Quant.instInhabitedInstWhen = { default := Cvc.Solver.Option.Quant.instInhabitedInstWhen.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqInstWhen :

DecidableEq InstWhen

Equations

Cvc.Solver.Option.Quant.instDecidableEqInstWhen x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprInstWhen :

Equations

Cvc.Solver.Option.Quant.instReprInstWhen = { reprPrec := Cvc.Solver.Option.Quant.instReprInstWhen.repr }

def Cvc.Solver.Option.Quant.instReprInstWhen.repr :

InstWhen → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Quant.InstWhen.toString :

InstWhen → String

The string cvc5 expects for a value of --inst-when.

Equations

Cvc.Solver.Option.Quant.InstWhen.full.toString = "full"
Cvc.Solver.Option.Quant.InstWhen.fullDelay.toString = "full-delay"
Cvc.Solver.Option.Quant.InstWhen.fullLastCall.toString = "full-last-call"
Cvc.Solver.Option.Quant.InstWhen.fullDelayLastCall.toString = "full-delay-last-call"
Cvc.Solver.Option.Quant.InstWhen.lastCall.toString = "last-call"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringInstWhen :

ToString InstWhen

Equations

Cvc.Solver.Option.Quant.instToStringInstWhen = { toString := Cvc.Solver.Option.Quant.InstWhen.toString }

inductive Cvc.Solver.Option.Quant.IteLiftQuant :

ITE lifting modes for quantified formulas.

none : IteLiftQuant
none: Do not lift if-then-else in quantified formulas.
simple : IteLiftQuant
simple.
Lift if-then-else in quantified formulas if results in smaller term size (the default).
all : IteLiftQuant
all: Lift if-then-else in quantified formulas.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedIteLiftQuant :

Inhabited IteLiftQuant

Equations

Cvc.Solver.Option.Quant.instInhabitedIteLiftQuant = { default := Cvc.Solver.Option.Quant.instInhabitedIteLiftQuant.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqIteLiftQuant :

DecidableEq IteLiftQuant

Equations

Cvc.Solver.Option.Quant.instDecidableEqIteLiftQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprIteLiftQuant.repr :

IteLiftQuant → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprIteLiftQuant :

Repr IteLiftQuant

Equations

Cvc.Solver.Option.Quant.instReprIteLiftQuant = { reprPrec := Cvc.Solver.Option.Quant.instReprIteLiftQuant.repr }

def Cvc.Solver.Option.Quant.IteLiftQuant.toString :

IteLiftQuant → String

The string cvc5 expects for a value of --ite-lift-quant.

Equations

Cvc.Solver.Option.Quant.IteLiftQuant.none.toString = "none"
Cvc.Solver.Option.Quant.IteLiftQuant.simple.toString = "simple"
Cvc.Solver.Option.Quant.IteLiftQuant.all.toString = "all"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringIteLiftQuant :

ToString IteLiftQuant

Equations

Cvc.Solver.Option.Quant.instToStringIteLiftQuant = { toString := Cvc.Solver.Option.Quant.IteLiftQuant.toString }

inductive Cvc.Solver.Option.Quant.MacrosQuantMode :

Modes for quantifiers macro expansion.

all : MacrosQuantMode
all: Infer definitions for functions, including those containing quantified formulas.
ground : MacrosQuantMode
ground: Only infer ground definitions for functions.
groundUf : MacrosQuantMode
ground-uf.
Only infer ground definitions for functions that result in triggers for all free variables (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedMacrosQuantMode :

Inhabited MacrosQuantMode

Equations

Cvc.Solver.Option.Quant.instInhabitedMacrosQuantMode = { default := Cvc.Solver.Option.Quant.instInhabitedMacrosQuantMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqMacrosQuantMode :

DecidableEq MacrosQuantMode

Equations

Cvc.Solver.Option.Quant.instDecidableEqMacrosQuantMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprMacrosQuantMode.repr :

MacrosQuantMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprMacrosQuantMode :

Repr MacrosQuantMode

Equations

Cvc.Solver.Option.Quant.instReprMacrosQuantMode = { reprPrec := Cvc.Solver.Option.Quant.instReprMacrosQuantMode.repr }

def Cvc.Solver.Option.Quant.MacrosQuantMode.toString :

MacrosQuantMode → String

The string cvc5 expects for a value of --macros-quant-mode.

Equations

Cvc.Solver.Option.Quant.MacrosQuantMode.all.toString = "all"
Cvc.Solver.Option.Quant.MacrosQuantMode.ground.toString = "ground"
Cvc.Solver.Option.Quant.MacrosQuantMode.groundUf.toString = "ground-uf"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringMacrosQuantMode :

ToString MacrosQuantMode

Equations

Cvc.Solver.Option.Quant.instToStringMacrosQuantMode = { toString := Cvc.Solver.Option.Quant.MacrosQuantMode.toString }

inductive Cvc.Solver.Option.Quant.MiniscopeQuant :

Miniscope quantifiers modes.

off : MiniscopeQuant
off: Do not miniscope quantifiers.
conj : MiniscopeQuant
conj: Use miniscoping of conjunctions only.
fv : MiniscopeQuant
fv: Use free variable miniscoping only.
conjAndFv : MiniscopeQuant
conj-and-fv: Enable both conjunction and free variable miniscoping (the default).
agg : MiniscopeQuant
agg.
Enable aggressive miniscope, which further may rewrite quantified formulas into a form where miniscoping is possible.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedMiniscopeQuant :

Inhabited MiniscopeQuant

Equations

Cvc.Solver.Option.Quant.instInhabitedMiniscopeQuant = { default := Cvc.Solver.Option.Quant.instInhabitedMiniscopeQuant.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqMiniscopeQuant :

DecidableEq MiniscopeQuant

Equations

Cvc.Solver.Option.Quant.instDecidableEqMiniscopeQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprMiniscopeQuant.repr :

MiniscopeQuant → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprMiniscopeQuant :

Repr MiniscopeQuant

Equations

Cvc.Solver.Option.Quant.instReprMiniscopeQuant = { reprPrec := Cvc.Solver.Option.Quant.instReprMiniscopeQuant.repr }

def Cvc.Solver.Option.Quant.MiniscopeQuant.toString :

MiniscopeQuant → String

The string cvc5 expects for a value of --miniscope-quant.

Equations

Cvc.Solver.Option.Quant.MiniscopeQuant.off.toString = "off"
Cvc.Solver.Option.Quant.MiniscopeQuant.conj.toString = "conj"
Cvc.Solver.Option.Quant.MiniscopeQuant.fv.toString = "fv"
Cvc.Solver.Option.Quant.MiniscopeQuant.conjAndFv.toString = "conj-and-fv"
Cvc.Solver.Option.Quant.MiniscopeQuant.agg.toString = "agg"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringMiniscopeQuant :

ToString MiniscopeQuant

Equations

Cvc.Solver.Option.Quant.instToStringMiniscopeQuant = { toString := Cvc.Solver.Option.Quant.MiniscopeQuant.toString }

inductive Cvc.Solver.Option.Quant.PreSkolemQuant :

Modes to apply skolemization eagerly to bodies of quantified formulas.

off : PreSkolemQuant
off: Do not apply Skolemization eagerly (the default).
on : PreSkolemQuant
on: Apply Skolemization eagerly to top-level (negatively asserted) quantified formulas.
agg : PreSkolemQuant
agg: Apply Skolemization eagerly and aggressively during preprocessing.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedPreSkolemQuant :

Inhabited PreSkolemQuant

Equations

Cvc.Solver.Option.Quant.instInhabitedPreSkolemQuant = { default := Cvc.Solver.Option.Quant.instInhabitedPreSkolemQuant.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqPreSkolemQuant :

DecidableEq PreSkolemQuant

Equations

Cvc.Solver.Option.Quant.instDecidableEqPreSkolemQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprPreSkolemQuant.repr :

PreSkolemQuant → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprPreSkolemQuant :

Repr PreSkolemQuant

Equations

Cvc.Solver.Option.Quant.instReprPreSkolemQuant = { reprPrec := Cvc.Solver.Option.Quant.instReprPreSkolemQuant.repr }

def Cvc.Solver.Option.Quant.PreSkolemQuant.toString :

PreSkolemQuant → String

The string cvc5 expects for a value of --pre-skolem-quant.

Equations

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringPreSkolemQuant :

ToString PreSkolemQuant

Equations

Cvc.Solver.Option.Quant.instToStringPreSkolemQuant = { toString := Cvc.Solver.Option.Quant.PreSkolemQuant.toString }

inductive Cvc.Solver.Option.Quant.Dsplit :

Modes for quantifiers splitting.

none : Dsplit
none: Never split quantified formulas.
default : Dsplit
default.
Split quantified formulas over some finite datatypes when finite model finding is enabled.
agg : Dsplit
agg: Aggressively split quantified formulas.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedDsplit :

Inhabited Dsplit

Equations

Cvc.Solver.Option.Quant.instInhabitedDsplit = { default := Cvc.Solver.Option.Quant.instInhabitedDsplit.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqDsplit :

DecidableEq Dsplit

Equations

Cvc.Solver.Option.Quant.instDecidableEqDsplit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprDsplit.repr :

Dsplit → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprDsplit :

Equations

Cvc.Solver.Option.Quant.instReprDsplit = { reprPrec := Cvc.Solver.Option.Quant.instReprDsplit.repr }

def Cvc.Solver.Option.Quant.Dsplit.toString :

Dsplit → String

The string cvc5 expects for a value of --quant-dsplit.

Equations

Cvc.Solver.Option.Quant.Dsplit.none.toString = "none"
Cvc.Solver.Option.Quant.Dsplit.default.toString = "default"
Cvc.Solver.Option.Quant.Dsplit.agg.toString = "agg"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringDsplit :

ToString Dsplit

Equations

Cvc.Solver.Option.Quant.instToStringDsplit = { toString := Cvc.Solver.Option.Quant.Dsplit.toString }

inductive Cvc.Solver.Option.Quant.TermDbMode :

Modes for terms included in the quantifiers term database.

all : TermDbMode
all: Quantifiers module considers all ground terms.
relevant : TermDbMode
relevant.
Quantifiers module considers only ground terms connected to current assertions (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedTermDbMode :

Inhabited TermDbMode

Equations

Cvc.Solver.Option.Quant.instInhabitedTermDbMode = { default := Cvc.Solver.Option.Quant.instInhabitedTermDbMode.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqTermDbMode :

DecidableEq TermDbMode

Equations

Cvc.Solver.Option.Quant.instDecidableEqTermDbMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprTermDbMode.repr :

TermDbMode → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprTermDbMode :

Repr TermDbMode

Equations

Cvc.Solver.Option.Quant.instReprTermDbMode = { reprPrec := Cvc.Solver.Option.Quant.instReprTermDbMode.repr }

def Cvc.Solver.Option.Quant.TermDbMode.toString :

TermDbMode → String

The string cvc5 expects for a value of --term-db-mode.

Equations

Cvc.Solver.Option.Quant.TermDbMode.all.toString = "all"
Cvc.Solver.Option.Quant.TermDbMode.relevant.toString = "relevant"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringTermDbMode :

ToString TermDbMode

Equations

Cvc.Solver.Option.Quant.instToStringTermDbMode = { toString := Cvc.Solver.Option.Quant.TermDbMode.toString }

inductive Cvc.Solver.Option.Quant.TriggerSel :

Trigger selection modes.

min : TriggerSel
min: Consider only minimal subterms that meet criteria for triggers (the default).
max : TriggerSel
max: Consider only maximal subterms that meet criteria for triggers.
minSMax : TriggerSel
min-s-max.
Consider only minimal subterms that meet criteria for single triggers, maximal otherwise.
minSAll : TriggerSel
min-s-all.
Consider only minimal subterms that meet criteria for single triggers, all otherwise.
all : TriggerSel
all: Consider all subterms that meet criteria for triggers.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedTriggerSel :

Inhabited TriggerSel

Equations

Cvc.Solver.Option.Quant.instInhabitedTriggerSel = { default := Cvc.Solver.Option.Quant.instInhabitedTriggerSel.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqTriggerSel :

DecidableEq TriggerSel

Equations

Cvc.Solver.Option.Quant.instDecidableEqTriggerSel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprTriggerSel.repr :

TriggerSel → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprTriggerSel :

Repr TriggerSel

Equations

Cvc.Solver.Option.Quant.instReprTriggerSel = { reprPrec := Cvc.Solver.Option.Quant.instReprTriggerSel.repr }

def Cvc.Solver.Option.Quant.TriggerSel.toString :

TriggerSel → String

The string cvc5 expects for a value of --trigger-sel.

Equations

Cvc.Solver.Option.Quant.TriggerSel.min.toString = "min"
Cvc.Solver.Option.Quant.TriggerSel.max.toString = "max"
Cvc.Solver.Option.Quant.TriggerSel.minSMax.toString = "min-s-max"
Cvc.Solver.Option.Quant.TriggerSel.minSAll.toString = "min-s-all"
Cvc.Solver.Option.Quant.TriggerSel.all.toString = "all"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringTriggerSel :

ToString TriggerSel

Equations

Cvc.Solver.Option.Quant.instToStringTriggerSel = { toString := Cvc.Solver.Option.Quant.TriggerSel.toString }

inductive Cvc.Solver.Option.Quant.UserPat :

Values of --user-pat.

These modes determine how user provided patterns (triggers) are used during E-matching. The modes vary on when instantiation based on user-provided triggers is combined with instantiation based on automatically selected triggers.

use : UserPat
use.
Use both user-provided and auto-generated patterns when patterns are provided for a quantified formula.
trust : UserPat
trust.
When provided, use only user-provided patterns for a quantified formula (the default).
strict : UserPat
strict.
When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques.
resort : UserPat
resort: Use user-provided patterns only after auto-generated patterns saturate.
ignore : UserPat
ignore: Ignore user-provided patterns.
interleave : UserPat
interleave: Alternate between use/resort.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instInhabitedUserPat :

Inhabited UserPat

Equations

Cvc.Solver.Option.Quant.instInhabitedUserPat = { default := Cvc.Solver.Option.Quant.instInhabitedUserPat.default }

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instDecidableEqUserPat :

DecidableEq UserPat

Equations

Cvc.Solver.Option.Quant.instDecidableEqUserPat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Quant.instReprUserPat.repr :

UserPat → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instReprUserPat :

Equations

Cvc.Solver.Option.Quant.instReprUserPat = { reprPrec := Cvc.Solver.Option.Quant.instReprUserPat.repr }

def Cvc.Solver.Option.Quant.UserPat.toString :

UserPat → String

The string cvc5 expects for a value of --user-pat.

Equations

Cvc.Solver.Option.Quant.UserPat.use.toString = "use"
Cvc.Solver.Option.Quant.UserPat.trust.toString = "trust"
Cvc.Solver.Option.Quant.UserPat.strict.toString = "strict"
Cvc.Solver.Option.Quant.UserPat.resort.toString = "resort"
Cvc.Solver.Option.Quant.UserPat.ignore.toString = "ignore"
Cvc.Solver.Option.Quant.UserPat.interleave.toString = "interleave"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Quant.instToStringUserPat :

ToString UserPat

Equations

Cvc.Solver.Option.Quant.instToStringUserPat = { toString := Cvc.Solver.Option.Quant.UserPat.toString }

inductive Cvc.Solver.Option.Quant :

Quantifier instantiation.

enumInst : Quant
--enum-inst.
Enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown.
fullSaturateQuant : Quant
--full-saturate-quant.
Resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation.
printInst : Quant
--print-inst: Print format for printing instantiations.
cbqi : Quant
--cbqi: Enable conflict-based quantifier instantiation.
cbqiAllConflict : Quant
--cbqi-all-conflict.
Add all available conflicting instances during conflict-based instantiation.
cbqiMode : Quant
--cbqi-mode: What effort to apply conflict find mechanism.
cegqi : Quant
--cegqi: Turns on counterexample-based quantifier instantiation.
cegqiBv : Quant
--cegqi-bv.
Use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors.
cegqiInnermost : Quant
--cegqi-innermost.
Only process innermost quantified formulas in counterexample-based quantifier instantiation.
cegqiMidpoint : Quant
--cegqi-midpoint.
Choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation.
cegqiNestedQe : Quant
--cegqi-nested-qe.
Process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation.
eMatching : Quant
--e-matching: Whether to do heuristic E-matching.
elimTautQuant : Quant
--elim-taut-quant: Eliminate tautological disjuncts of quantified formulas.
enumInstInterleave : Quant
--enum-inst-interleave: Interleave enumerative instantiation with other techniques.
enumInstSum : Quant
--enum-inst-sum.
Enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum.
extRewriteQuant : Quant
--ext-rewrite-quant: Apply extended rewriting to bodies of quantified formulas.
finiteModelFind : Quant
--finite-model-find: Use finite model finding heuristic for quantifier instantiation.
fmfBound : Quant
--fmf-bound: Finite model finding on bounded quantification.
fmfTypeCompletionThresh : Quant
--fmf-type-completion-thresh.
The maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted.
ieval : Quant
--ieval: Mode for using instantiation evaluation.
instLocal : Quant
--inst-local: Instantiations are local to the SAT context.
instMaxRounds : Quant
--inst-max-rounds: Maximum number of instantiation rounds (-1 == no limit, default).
instNoEntail : Quant
--inst-no-entail.
Do not consider instances of quantified formulas that are currently entailed.
instWhen : Quant
--inst-when: When to apply instantiation.
iteLiftQuant : Quant
--ite-lift-quant: Ite lifting mode for quantified formulas.
macrosQuant : Quant
--macros-quant: Perform quantifiers macro expansion.
macrosQuantMode : Quant
--macros-quant-mode: Mode for quantifiers macro expansion.
mbqi : Quant
--mbqi: Use model-based quantifier instantiation.
mbqiCheckTimeout : Quant
--mbqi-check-timeout.
Timeout (in milliseconds) for verifying subcalls for model-based instantiation (0 == no limit).
mbqiEnum : Quant
--mbqi-enum: Use fast enumeration to augment instantiations from MBQI.
mbqiOneInstPerRound : Quant
--mbqi-one-inst-per-round: Only add one instantiation per quantifier per round for mbqi.
miniscopeQuant : Quant
--miniscope-quant: Miniscope mode for quantified formulas.
miniscopeQuantUser : Quant
--miniscope-quant-user: Miniscope quantified formulas with user patterns.
multiTriggerCache : Quant
--multi-trigger-cache: Caching version of multi triggers.
multiTriggerLinear : Quant
--multi-trigger-linear.
Implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms.
multiTriggerPriority : Quant
--multi-trigger-priority.
Only try multi triggers if single triggers give no instantiations.
multiTriggerWhenSingle : Quant
--multi-trigger-when-single: Select multi triggers when single triggers exist.
preSkolemQuant : Quant
--pre-skolem-quant.
Modes to apply skolemization eagerly to bodies of quantified formulas.
prenexQuantUser : Quant
--prenex-quant-user: Prenex quantified formulas with user patterns.
printInstFull : Quant
--print-inst-full: Print instantiations for formulas that do not have given identifiers.
alphaEquiv : Quant
--quant-alpha-equiv: Infer alpha equivalence between quantified formulas.
dsplit : Quant
--quant-dsplit: Mode for dynamic quantifiers splitting.
relevantTriggers : Quant
--relevant-triggers: Prefer triggers that are more relevant based on SInE style analysis.
subCbqi : Quant
--sub-cbqi: Enable conflict-based instantiation subsolver strategy.
termDbMode : Quant
--term-db-mode: Which ground terms to consider for instantiation.
triggerSel : Quant
--trigger-sel: Selection mode for triggers.
userPat : Quant
--user-pat: Policy for handling user-provided patterns for quantifier instantiation.
varElimQuant : Quant
--var-elim-quant: Enable simple variable elimination for quantified formulas.
varEntEqElimQuant : Quant
--var-ent-eq-elim-quant.
Enable variable elimination for quantified formulas that infers entailed equalities corresponding to eliminations.
varIneqElimQuant : Quant
--var-ineq-elim-quant.
Enable variable elimination based on infinite projection of unbound arithmetic variables.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedQuant :

Inhabited Quant

Equations

Cvc.Solver.Option.instInhabitedQuant = { default := Cvc.Solver.Option.instInhabitedQuant.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqQuant :

DecidableEq Quant

Equations

Cvc.Solver.Option.instDecidableEqQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.instReprQuant.repr :

Quant → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instReprQuant :

Equations

Cvc.Solver.Option.instReprQuant = { reprPrec := Cvc.Solver.Option.instReprQuant.repr }

def Cvc.Solver.Option.Quant.name :

Quant → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Quant.enumInst.name = "enum-inst"
Cvc.Solver.Option.Quant.fullSaturateQuant.name = "full-saturate-quant"
Cvc.Solver.Option.Quant.printInst.name = "print-inst"
Cvc.Solver.Option.Quant.cbqi.name = "cbqi"
Cvc.Solver.Option.Quant.cbqiAllConflict.name = "cbqi-all-conflict"
Cvc.Solver.Option.Quant.cbqiMode.name = "cbqi-mode"
Cvc.Solver.Option.Quant.cegqi.name = "cegqi"
Cvc.Solver.Option.Quant.cegqiBv.name = "cegqi-bv"
Cvc.Solver.Option.Quant.cegqiInnermost.name = "cegqi-innermost"
Cvc.Solver.Option.Quant.cegqiMidpoint.name = "cegqi-midpoint"
Cvc.Solver.Option.Quant.cegqiNestedQe.name = "cegqi-nested-qe"
Cvc.Solver.Option.Quant.eMatching.name = "e-matching"
Cvc.Solver.Option.Quant.elimTautQuant.name = "elim-taut-quant"
Cvc.Solver.Option.Quant.enumInstInterleave.name = "enum-inst-interleave"
Cvc.Solver.Option.Quant.enumInstSum.name = "enum-inst-sum"
Cvc.Solver.Option.Quant.extRewriteQuant.name = "ext-rewrite-quant"
Cvc.Solver.Option.Quant.finiteModelFind.name = "finite-model-find"
Cvc.Solver.Option.Quant.fmfBound.name = "fmf-bound"
Cvc.Solver.Option.Quant.fmfTypeCompletionThresh.name = "fmf-type-completion-thresh"
Cvc.Solver.Option.Quant.ieval.name = "ieval"
Cvc.Solver.Option.Quant.instLocal.name = "inst-local"
Cvc.Solver.Option.Quant.instMaxRounds.name = "inst-max-rounds"
Cvc.Solver.Option.Quant.instNoEntail.name = "inst-no-entail"
Cvc.Solver.Option.Quant.instWhen.name = "inst-when"
Cvc.Solver.Option.Quant.iteLiftQuant.name = "ite-lift-quant"
Cvc.Solver.Option.Quant.macrosQuant.name = "macros-quant"
Cvc.Solver.Option.Quant.macrosQuantMode.name = "macros-quant-mode"
Cvc.Solver.Option.Quant.mbqi.name = "mbqi"
Cvc.Solver.Option.Quant.mbqiCheckTimeout.name = "mbqi-check-timeout"
Cvc.Solver.Option.Quant.mbqiEnum.name = "mbqi-enum"
Cvc.Solver.Option.Quant.mbqiOneInstPerRound.name = "mbqi-one-inst-per-round"
Cvc.Solver.Option.Quant.miniscopeQuant.name = "miniscope-quant"
Cvc.Solver.Option.Quant.miniscopeQuantUser.name = "miniscope-quant-user"
Cvc.Solver.Option.Quant.multiTriggerCache.name = "multi-trigger-cache"
Cvc.Solver.Option.Quant.multiTriggerLinear.name = "multi-trigger-linear"
Cvc.Solver.Option.Quant.multiTriggerPriority.name = "multi-trigger-priority"
Cvc.Solver.Option.Quant.multiTriggerWhenSingle.name = "multi-trigger-when-single"
Cvc.Solver.Option.Quant.preSkolemQuant.name = "pre-skolem-quant"
Cvc.Solver.Option.Quant.prenexQuantUser.name = "prenex-quant-user"
Cvc.Solver.Option.Quant.printInstFull.name = "print-inst-full"
Cvc.Solver.Option.Quant.alphaEquiv.name = "quant-alpha-equiv"
Cvc.Solver.Option.Quant.dsplit.name = "quant-dsplit"
Cvc.Solver.Option.Quant.relevantTriggers.name = "relevant-triggers"
Cvc.Solver.Option.Quant.subCbqi.name = "sub-cbqi"
Cvc.Solver.Option.Quant.termDbMode.name = "term-db-mode"
Cvc.Solver.Option.Quant.triggerSel.name = "trigger-sel"
Cvc.Solver.Option.Quant.userPat.name = "user-pat"
Cvc.Solver.Option.Quant.varElimQuant.name = "var-elim-quant"
Cvc.Solver.Option.Quant.varEntEqElimQuant.name = "var-ent-eq-elim-quant"
Cvc.Solver.Option.Quant.varIneqElimQuant.name = "var-ineq-elim-quant"

Instances For

@[reducible]

def Cvc.Solver.Option.Quant.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Quant.valueString (opt : Quant) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option.Sygus.Fair :

Modes for enforcing fairness for counterexample guided quantifier instantion.

direct : Fair
direct: Enforce fairness using direct conflict lemmas.
dtSize : Fair
dt-size: Enforce fairness using size operator (the default).
dtHeightBound : Fair
dt-height-bound: Enforce fairness by height bound predicate.
dtSizeBound : Fair
dt-size-bound: Enforce fairness by size bound predicate.
none : Fair
none: Do not enforce fairness.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedFair :

Equations

Cvc.Solver.Option.Sygus.instInhabitedFair = { default := Cvc.Solver.Option.Sygus.instInhabitedFair.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqFair :

DecidableEq Fair

Equations

Cvc.Solver.Option.Sygus.instDecidableEqFair x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprFair.repr :

Fair → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprFair :

Equations

Cvc.Solver.Option.Sygus.instReprFair = { reprPrec := Cvc.Solver.Option.Sygus.instReprFair.repr }

def Cvc.Solver.Option.Sygus.Fair.toString :

Fair → String

The string cvc5 expects for a value of --sygus-fair.

Equations

Cvc.Solver.Option.Sygus.Fair.direct.toString = "direct"
Cvc.Solver.Option.Sygus.Fair.dtSize.toString = "dt-size"
Cvc.Solver.Option.Sygus.Fair.dtHeightBound.toString = "dt-height-bound"
Cvc.Solver.Option.Sygus.Fair.dtSizeBound.toString = "dt-size-bound"
Cvc.Solver.Option.Sygus.Fair.none.toString = "none"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringFair :

Equations

Cvc.Solver.Option.Sygus.instToStringFair = { toString := Cvc.Solver.Option.Sygus.Fair.toString }

inductive Cvc.Solver.Option.Sygus.Rewriter :

Modes for applying rewriting for sygus symmetry breaking.

none : Rewriter
none: Do not use the rewriter.
basic : Rewriter
basic: Use the basic rewriter.
extended : Rewriter
extended: Use the extended rewriter (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedRewriter :

Inhabited Rewriter

Equations

Cvc.Solver.Option.Sygus.instInhabitedRewriter = { default := Cvc.Solver.Option.Sygus.instInhabitedRewriter.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqRewriter :

DecidableEq Rewriter

Equations

Cvc.Solver.Option.Sygus.instDecidableEqRewriter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprRewriter.repr :

Rewriter → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprRewriter :

Equations

Cvc.Solver.Option.Sygus.instReprRewriter = { reprPrec := Cvc.Solver.Option.Sygus.instReprRewriter.repr }

def Cvc.Solver.Option.Sygus.Rewriter.toString :

Rewriter → String

The string cvc5 expects for a value of --sygus-rewriter.

Equations

Cvc.Solver.Option.Sygus.Rewriter.none.toString = "none"
Cvc.Solver.Option.Sygus.Rewriter.basic.toString = "basic"
Cvc.Solver.Option.Sygus.Rewriter.extended.toString = "extended"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringRewriter :

ToString Rewriter

Equations

Cvc.Solver.Option.Sygus.instToStringRewriter = { toString := Cvc.Solver.Option.Sygus.Rewriter.toString }

inductive Cvc.Solver.Option.Sygus.SimpleSymBreak :

Modes for applying simple symmetry breaking based on the grammar for smart enumeration.

none : SimpleSymBreak
none: Do not apply simple symmetry breaking.
basic : SimpleSymBreak
basic: Apply basic simple symmetry breaking.
agg : SimpleSymBreak
agg: Apply aggressive simple symmetry breaking (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedSimpleSymBreak :

Inhabited SimpleSymBreak

Equations

Cvc.Solver.Option.Sygus.instInhabitedSimpleSymBreak = { default := Cvc.Solver.Option.Sygus.instInhabitedSimpleSymBreak.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqSimpleSymBreak :

DecidableEq SimpleSymBreak

Equations

Cvc.Solver.Option.Sygus.instDecidableEqSimpleSymBreak x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprSimpleSymBreak :

Repr SimpleSymBreak

Equations

Cvc.Solver.Option.Sygus.instReprSimpleSymBreak = { reprPrec := Cvc.Solver.Option.Sygus.instReprSimpleSymBreak.repr }

def Cvc.Solver.Option.Sygus.instReprSimpleSymBreak.repr :

SimpleSymBreak → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.SimpleSymBreak.toString :

SimpleSymBreak → String

The string cvc5 expects for a value of --sygus-simple-sym-break.

Equations

Cvc.Solver.Option.Sygus.SimpleSymBreak.none.toString = "none"
Cvc.Solver.Option.Sygus.SimpleSymBreak.basic.toString = "basic"
Cvc.Solver.Option.Sygus.SimpleSymBreak.agg.toString = "agg"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringSimpleSymBreak :

ToString SimpleSymBreak

Equations

Cvc.Solver.Option.Sygus.instToStringSimpleSymBreak = { toString := Cvc.Solver.Option.Sygus.SimpleSymBreak.toString }

inductive Cvc.Solver.Option.Sygus.CegisSample :

Modes for sampling with counterexample-guided inductive synthesis (CEGIS).

none : CegisSample
none: Do not use sampling with CEGIS (the default).
use : CegisSample
use.
Use sampling to accelerate CEGIS. This will rule out solutions for a conjecture when they are not satisfied by a sample point.
trust : CegisSample
trust.
Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedCegisSample :

Inhabited CegisSample

Equations

Cvc.Solver.Option.Sygus.instInhabitedCegisSample = { default := Cvc.Solver.Option.Sygus.instInhabitedCegisSample.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqCegisSample :

DecidableEq CegisSample

Equations

Cvc.Solver.Option.Sygus.instDecidableEqCegisSample x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprCegisSample :

Repr CegisSample

Equations

Cvc.Solver.Option.Sygus.instReprCegisSample = { reprPrec := Cvc.Solver.Option.Sygus.instReprCegisSample.repr }

def Cvc.Solver.Option.Sygus.instReprCegisSample.repr :

CegisSample → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.CegisSample.toString :

CegisSample → String

The string cvc5 expects for a value of --cegis-sample.

Equations

Cvc.Solver.Option.Sygus.CegisSample.none.toString = "none"
Cvc.Solver.Option.Sygus.CegisSample.use.toString = "use"
Cvc.Solver.Option.Sygus.CegisSample.trust.toString = "trust"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringCegisSample :

ToString CegisSample

Equations

Cvc.Solver.Option.Sygus.instToStringCegisSample = { toString := Cvc.Solver.Option.Sygus.CegisSample.toString }

inductive Cvc.Solver.Option.Sygus.Enum :

Modes for sygus enumeration.

smart : Enum
smart: Use smart enumeration based on datatype constraints.
fast : Enum
fast: Use optimized enumerator for sygus enumeration.
random : Enum
random: Use basic random enumerator for sygus enumeration.
varAgnostic : Enum
var-agnostic: Use sygus solver to enumerate terms that are agnostic to variables.
auto : Enum
auto: Internally decide the best policy for each enumerator (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedEnum :

Equations

Cvc.Solver.Option.Sygus.instInhabitedEnum = { default := Cvc.Solver.Option.Sygus.instInhabitedEnum.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqEnum :

DecidableEq Enum

Equations

Cvc.Solver.Option.Sygus.instDecidableEqEnum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprEnum.repr :

Enum → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprEnum :

Equations

Cvc.Solver.Option.Sygus.instReprEnum = { reprPrec := Cvc.Solver.Option.Sygus.instReprEnum.repr }

def Cvc.Solver.Option.Sygus.Enum.toString :

Enum → String

The string cvc5 expects for a value of --sygus-enum.

Equations

Cvc.Solver.Option.Sygus.Enum.smart.toString = "smart"
Cvc.Solver.Option.Sygus.Enum.fast.toString = "fast"
Cvc.Solver.Option.Sygus.Enum.random.toString = "random"
Cvc.Solver.Option.Sygus.Enum.varAgnostic.toString = "var-agnostic"
Cvc.Solver.Option.Sygus.Enum.auto.toString = "auto"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringEnum :

Equations

Cvc.Solver.Option.Sygus.instToStringEnum = { toString := Cvc.Solver.Option.Sygus.Enum.toString }

inductive Cvc.Solver.Option.Sygus.EvalUnfold :

Modes for sygus evaluation unfolding.

none : EvalUnfold
none: Do not use sygus evaluation unfolding.
single : EvalUnfold
single: Do single-step unfolding for all evaluation functions.
singleBool : EvalUnfold
single-bool.
Do single-step unfolding for Boolean functions and ITEs, and multi-step unfolding for all others (the default).
multi : EvalUnfold
multi: Do multi-step unfolding for all evaluation functions.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedEvalUnfold :

Inhabited EvalUnfold

Equations

Cvc.Solver.Option.Sygus.instInhabitedEvalUnfold = { default := Cvc.Solver.Option.Sygus.instInhabitedEvalUnfold.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqEvalUnfold :

DecidableEq EvalUnfold

Equations

Cvc.Solver.Option.Sygus.instDecidableEqEvalUnfold x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprEvalUnfold :

Repr EvalUnfold

Equations

Cvc.Solver.Option.Sygus.instReprEvalUnfold = { reprPrec := Cvc.Solver.Option.Sygus.instReprEvalUnfold.repr }

def Cvc.Solver.Option.Sygus.instReprEvalUnfold.repr :

EvalUnfold → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.EvalUnfold.toString :

EvalUnfold → String

The string cvc5 expects for a value of --sygus-eval-unfold.

Equations

Cvc.Solver.Option.Sygus.EvalUnfold.none.toString = "none"
Cvc.Solver.Option.Sygus.EvalUnfold.single.toString = "single"
Cvc.Solver.Option.Sygus.EvalUnfold.singleBool.toString = "single-bool"
Cvc.Solver.Option.Sygus.EvalUnfold.multi.toString = "multi"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringEvalUnfold :

ToString EvalUnfold

Equations

Cvc.Solver.Option.Sygus.instToStringEvalUnfold = { toString := Cvc.Solver.Option.Sygus.EvalUnfold.toString }

inductive Cvc.Solver.Option.Sygus.GrammarCons :

Modes for default SyGuS grammars.

simple : GrammarCons
simple: Use simple grammar construction (no symbolic terms or constants) (the default).
anyConst : GrammarCons
any-const: Use symoblic constant constructors.
anyTerm : GrammarCons
any-term.
When applicable, use constructors corresponding to any symbolic term. This option enables a sum-of-monomials grammar for arithmetic. For all other types, it enables symbolic constant constructors.
anyTermConcise : GrammarCons
any-term-concise.
When applicable, use constructors corresponding to any symbolic term, favoring conciseness over generality. This option is equivalent to any-term but enables a polynomial grammar for arithmetic when not in a combined theory.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedGrammarCons :

Inhabited GrammarCons

Equations

Cvc.Solver.Option.Sygus.instInhabitedGrammarCons = { default := Cvc.Solver.Option.Sygus.instInhabitedGrammarCons.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqGrammarCons :

DecidableEq GrammarCons

Equations

Cvc.Solver.Option.Sygus.instDecidableEqGrammarCons x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprGrammarCons :

Repr GrammarCons

Equations

Cvc.Solver.Option.Sygus.instReprGrammarCons = { reprPrec := Cvc.Solver.Option.Sygus.instReprGrammarCons.repr }

def Cvc.Solver.Option.Sygus.instReprGrammarCons.repr :

GrammarCons → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.GrammarCons.toString :

GrammarCons → String

The string cvc5 expects for a value of --sygus-grammar-cons.

Equations

Cvc.Solver.Option.Sygus.GrammarCons.simple.toString = "simple"
Cvc.Solver.Option.Sygus.GrammarCons.anyConst.toString = "any-const"
Cvc.Solver.Option.Sygus.GrammarCons.anyTerm.toString = "any-term"
Cvc.Solver.Option.Sygus.GrammarCons.anyTermConcise.toString = "any-term-concise"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringGrammarCons :

ToString GrammarCons

Equations

Cvc.Solver.Option.Sygus.instToStringGrammarCons = { toString := Cvc.Solver.Option.Sygus.GrammarCons.toString }

inductive Cvc.Solver.Option.Sygus.InvTempl :

Template modes for sygus invariant synthesis.

none : InvTempl
none: Synthesize invariant directly.
pre : InvTempl
pre: Synthesize invariant based on weakening of precondition.
post : InvTempl
post: Synthesize invariant based on strengthening of postcondition (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedInvTempl :

Inhabited InvTempl

Equations

Cvc.Solver.Option.Sygus.instInhabitedInvTempl = { default := Cvc.Solver.Option.Sygus.instInhabitedInvTempl.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqInvTempl :

DecidableEq InvTempl

Equations

Cvc.Solver.Option.Sygus.instDecidableEqInvTempl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprInvTempl.repr :

InvTempl → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprInvTempl :

Equations

Cvc.Solver.Option.Sygus.instReprInvTempl = { reprPrec := Cvc.Solver.Option.Sygus.instReprInvTempl.repr }

def Cvc.Solver.Option.Sygus.InvTempl.toString :

InvTempl → String

The string cvc5 expects for a value of --sygus-inv-templ.

Equations

Cvc.Solver.Option.Sygus.InvTempl.none.toString = "none"
Cvc.Solver.Option.Sygus.InvTempl.pre.toString = "pre"
Cvc.Solver.Option.Sygus.InvTempl.post.toString = "post"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringInvTempl :

ToString InvTempl

Equations

Cvc.Solver.Option.Sygus.instToStringInvTempl = { toString := Cvc.Solver.Option.Sygus.InvTempl.toString }

inductive Cvc.Solver.Option.Sygus.Out :

Modes for sygus solution output.

status : Out
status: Print only status for check-synth calls.
statusAndDef : Out
status-and-def: Print status followed by definition corresponding to solution.
sygusStandard : Out
sygus-standard: Print based on SyGuS standard (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedOut :

Equations

Cvc.Solver.Option.Sygus.instInhabitedOut = { default := Cvc.Solver.Option.Sygus.instInhabitedOut.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqOut :

DecidableEq Out

Equations

Cvc.Solver.Option.Sygus.instDecidableEqOut x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprOut.repr :

Out → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprOut :

Equations

Cvc.Solver.Option.Sygus.instReprOut = { reprPrec := Cvc.Solver.Option.Sygus.instReprOut.repr }

def Cvc.Solver.Option.Sygus.Out.toString :

The string cvc5 expects for a value of --sygus-out.

Equations

Cvc.Solver.Option.Sygus.Out.status.toString = "status"
Cvc.Solver.Option.Sygus.Out.statusAndDef.toString = "status-and-def"
Cvc.Solver.Option.Sygus.Out.sygusStandard.toString = "sygus-standard"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringOut :

Equations

Cvc.Solver.Option.Sygus.instToStringOut = { toString := Cvc.Solver.Option.Sygus.Out.toString }

inductive Cvc.Solver.Option.Sygus.Si :

Modes for single invocation techniques.

none : Si
none: Do not use single invocation techniques (the default).
use : Si
use: Use single invocation techniques only if grammar is not restrictive.
all : Si
all: Always use single invocation techniques.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedSi :

Equations

Cvc.Solver.Option.Sygus.instInhabitedSi = { default := Cvc.Solver.Option.Sygus.instInhabitedSi.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqSi :

Equations

Cvc.Solver.Option.Sygus.instDecidableEqSi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprSi.repr :

Si → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprSi :

Equations

Cvc.Solver.Option.Sygus.instReprSi = { reprPrec := Cvc.Solver.Option.Sygus.instReprSi.repr }

def Cvc.Solver.Option.Sygus.Si.toString :

The string cvc5 expects for a value of --sygus-si.

Equations

Cvc.Solver.Option.Sygus.Si.none.toString = "none"
Cvc.Solver.Option.Sygus.Si.use.toString = "use"
Cvc.Solver.Option.Sygus.Si.all.toString = "all"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringSi :

Equations

Cvc.Solver.Option.Sygus.instToStringSi = { toString := Cvc.Solver.Option.Sygus.Si.toString }

inductive Cvc.Solver.Option.Sygus.SiRcons :

Modes for reconstruction solutions while using single invocation techniques.

none : SiRcons
none.
Do not try to reconstruct solutions in the original (user-provided) grammar when using single invocation techniques. In this mode, solutions produced by cvc5 may violate grammar restrictions.
try : SiRcons
try.
Try to reconstruct solutions in the original grammar when using single invocation techniques in an incomplete (fail-fast) manner.
allLimit : SiRcons
all-limit.
Try to reconstruct solutions in the original grammar, but terminate if a maximum number of rounds for reconstruction is exceeded.
all : SiRcons
all.
Try to reconstruct solutions in the original grammar. In this mode, we do not terminate until a solution is successfully reconstructed (the default).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedSiRcons :

Inhabited SiRcons

Equations

Cvc.Solver.Option.Sygus.instInhabitedSiRcons = { default := Cvc.Solver.Option.Sygus.instInhabitedSiRcons.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqSiRcons :

DecidableEq SiRcons

Equations

Cvc.Solver.Option.Sygus.instDecidableEqSiRcons x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cvc.Solver.Option.Sygus.instReprSiRcons.repr :

SiRcons → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprSiRcons :

Equations

Cvc.Solver.Option.Sygus.instReprSiRcons = { reprPrec := Cvc.Solver.Option.Sygus.instReprSiRcons.repr }

def Cvc.Solver.Option.Sygus.SiRcons.toString :

SiRcons → String

The string cvc5 expects for a value of --sygus-si-rcons.

Equations

Cvc.Solver.Option.Sygus.SiRcons.none.toString = "none"
Cvc.Solver.Option.Sygus.SiRcons.try.toString = "try"
Cvc.Solver.Option.Sygus.SiRcons.allLimit.toString = "all-limit"
Cvc.Solver.Option.Sygus.SiRcons.all.toString = "all"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringSiRcons :

ToString SiRcons

Equations

Cvc.Solver.Option.Sygus.instToStringSiRcons = { toString := Cvc.Solver.Option.Sygus.SiRcons.toString }

inductive Cvc.Solver.Option.Sygus.UnifPi :

Modes for piecewise-independent unification.

none : UnifPi
none: Do not use piecewise-independent unification (the default).
complete : UnifPi
complete.
Use complete approach for piecewise-independent unification (see Section 3 of Barbosa et al FMCAD 2019).
condEnum : UnifPi
cond-enum.
Use unconstrained condition enumeration for piecewise-independent unification (see Section 4 of Barbosa et al FMCAD 2019).
condEnumIgain : UnifPi
cond-enum-igain.
Same as cond-enum, but additionally uses an information gain heuristic when doing decision tree learning.

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instInhabitedUnifPi :

Inhabited UnifPi

Equations

Cvc.Solver.Option.Sygus.instInhabitedUnifPi = { default := Cvc.Solver.Option.Sygus.instInhabitedUnifPi.default }

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instDecidableEqUnifPi :

DecidableEq UnifPi

Equations

Cvc.Solver.Option.Sygus.instDecidableEqUnifPi x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instReprUnifPi :

Equations

Cvc.Solver.Option.Sygus.instReprUnifPi = { reprPrec := Cvc.Solver.Option.Sygus.instReprUnifPi.repr }

def Cvc.Solver.Option.Sygus.instReprUnifPi.repr :

UnifPi → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.UnifPi.toString :

UnifPi → String

The string cvc5 expects for a value of --sygus-unif-pi.

Equations

Cvc.Solver.Option.Sygus.UnifPi.none.toString = "none"
Cvc.Solver.Option.Sygus.UnifPi.complete.toString = "complete"
Cvc.Solver.Option.Sygus.UnifPi.condEnum.toString = "cond-enum"
Cvc.Solver.Option.Sygus.UnifPi.condEnumIgain.toString = "cond-enum-igain"

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.Sygus.instToStringUnifPi :

ToString UnifPi

Equations

Cvc.Solver.Option.Sygus.instToStringUnifPi = { toString := Cvc.Solver.Option.Sygus.UnifPi.toString }

inductive Cvc.Solver.Option.Sygus :

Syntax-guided synthesis.

abortSize : Sygus
--sygus-abort-size.
Tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default).
fair : Sygus
--sygus-fair: If and how to apply fairness for sygus.
rewriter : Sygus
--sygus-rewriter: If and how to apply rewriting for sygus symmetry breaking.
simpleSymBreak : Sygus
--sygus-simple-sym-break.
If and how to apply simple symmetry breaking based on the grammar for smart enumeration.
symBreakPbe : Sygus
--sygus-sym-break-pbe: Sygus symmetry breaking lemmas based on pbe conjectures.
cegisSample : Sygus
--cegis-sample.
Mode for using samples in the counterexample-guided inductive synthesis loop.
sygus : Sygus
--sygus: Support SyGuS commands.
addConstGrammar : Sygus
--sygus-add-const-grammar: Statically add constants appearing in conjecture to grammars.
coreConnective : Sygus
--sygus-core-connective.
Use unsat core analysis to construct Boolean connective to sygus conjectures.
enum : Sygus
--sygus-enum: Mode for sygus enumeration.
evalUnfold : Sygus
--sygus-eval-unfold: Modes for sygus evaluation unfolding.
grammarCons : Sygus
--sygus-grammar-cons: Mode for SyGuS grammar construction.
inst : Sygus
--sygus-inst: Enable SyGuS instantiation quantifiers module.
invTempl : Sygus
--sygus-inv-templ.
Template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none).
minGrammar : Sygus
--sygus-min-grammar: Statically minimize sygus grammars.
out : Sygus
--sygus-out: Output mode for sygus.
pbe : Sygus
--sygus-pbe.
Enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures.
repairConst : Sygus
--sygus-repair-const: Use approach to repair constants in sygus candidate solutions.
si : Sygus
--sygus-si: Mode for processing single invocation synthesis conjectures.
siAbort : Sygus
--sygus-si-abort: Abort if synthesis conjecture is not single invocation.
siRcons : Sygus
--sygus-si-rcons: Policy for reconstructing solutions for single invocation conjectures.
stream : Sygus
--sygus-stream.
Enumerate a stream of solutions instead of terminating after the first one.
unifPi : Sygus
--sygus-unif-pi: Mode for synthesis via piecewise-indepedent unification.
verifyTimeout : Sygus
--sygus-verify-timeout.
Timeout (in milliseconds) for verifying satisfiability of synthesized terms (0 == no limit).

Instances For

@[instance_reducible]

instance Cvc.Solver.Option.instInhabitedSygus :

Inhabited Sygus

Equations

Cvc.Solver.Option.instInhabitedSygus = { default := Cvc.Solver.Option.instInhabitedSygus.default }

@[instance_reducible]

instance Cvc.Solver.Option.instDecidableEqSygus :

DecidableEq Sygus

Equations

Cvc.Solver.Option.instDecidableEqSygus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cvc.Solver.Option.instReprSygus :

Equations

Cvc.Solver.Option.instReprSygus = { reprPrec := Cvc.Solver.Option.instReprSygus.repr }

def Cvc.Solver.Option.instReprSygus.repr :

Sygus → Nat → Std.Format

Equations

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

Instances For

def Cvc.Solver.Option.Sygus.name :

Sygus → String

The option's name, as cvc5 spells it.

Equations

Cvc.Solver.Option.Sygus.abortSize.name = "sygus-abort-size"
Cvc.Solver.Option.Sygus.fair.name = "sygus-fair"
Cvc.Solver.Option.Sygus.rewriter.name = "sygus-rewriter"
Cvc.Solver.Option.Sygus.simpleSymBreak.name = "sygus-simple-sym-break"
Cvc.Solver.Option.Sygus.symBreakPbe.name = "sygus-sym-break-pbe"
Cvc.Solver.Option.Sygus.cegisSample.name = "cegis-sample"
Cvc.Solver.Option.Sygus.sygus.name = "sygus"
Cvc.Solver.Option.Sygus.addConstGrammar.name = "sygus-add-const-grammar"
Cvc.Solver.Option.Sygus.coreConnective.name = "sygus-core-connective"
Cvc.Solver.Option.Sygus.enum.name = "sygus-enum"
Cvc.Solver.Option.Sygus.evalUnfold.name = "sygus-eval-unfold"
Cvc.Solver.Option.Sygus.grammarCons.name = "sygus-grammar-cons"
Cvc.Solver.Option.Sygus.inst.name = "sygus-inst"
Cvc.Solver.Option.Sygus.invTempl.name = "sygus-inv-templ"
Cvc.Solver.Option.Sygus.minGrammar.name = "sygus-min-grammar"
Cvc.Solver.Option.Sygus.out.name = "sygus-out"
Cvc.Solver.Option.Sygus.pbe.name = "sygus-pbe"
Cvc.Solver.Option.Sygus.repairConst.name = "sygus-repair-const"
Cvc.Solver.Option.Sygus.si.name = "sygus-si"
Cvc.Solver.Option.Sygus.siAbort.name = "sygus-si-abort"
Cvc.Solver.Option.Sygus.siRcons.name = "sygus-si-rcons"
Cvc.Solver.Option.Sygus.stream.name = "sygus-stream"
Cvc.Solver.Option.Sygus.unifPi.name = "sygus-unif-pi"
Cvc.Solver.Option.Sygus.verifyTimeout.name = "sygus-verify-timeout"

Instances For

@[reducible]

def Cvc.Solver.Option.Sygus.argType :

The type of the value the option expects.

Equations

Instances For

def Cvc.Solver.Option.Sygus.valueString (opt : Sygus) :

opt.argType → String

The value as the string cvc5 expects.

Equations

Instances For

inductive Cvc.Solver.Option :

A solver option, by category.

base (opt : Base) : Option
Resource limits, verbosity, statistics and incrementality.
smt (opt : Smt) : Option
The SMT layer: what a check can produce, self-checks, preprocessing.
printing (opt : Printing) : Option
How terms and models are printed.
proof (opt : Proof) : Option
Proof production and checking.
sat (opt : Sat) : Option
The SAT layer.
theory (opt : Theory) : Option
The theory layer, shared by every theory.
arith (opt : Arith) : Option
The arithmetic theory.
arrays (opt : Arrays) : Option
The theory of arrays.
bv (opt : Bv) : Option
The bit-vector theory.
strings (opt : Strings) : Option
The theory of strings and sequences.
uf (opt : Uf) : Option
Uninterpreted functions.
quant (opt : Quant) : Option
Quantifier instantiation.
sygus (opt : Sygus) : Option
Syntax-guided synthesis.

Instances For

@[instance_reducible]

instance Cvc.Solver.instInhabitedOption :

Inhabited Option

Equations

Cvc.Solver.instInhabitedOption = { default := Cvc.Solver.instInhabitedOption.default }

@[instance_reducible]

instance Cvc.Solver.instDecidableEqOption :

DecidableEq Option

Equations

Cvc.Solver.instDecidableEqOption = Cvc.Solver.instDecidableEqOption.decEq

def Cvc.Solver.instDecidableEqOption.decEq (x✝ x✝¹ : Option) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Cvc.Solver.instReprOption.repr :

Option → Nat → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Cvc.Solver.instReprOption :

Equations

Cvc.Solver.instReprOption = { reprPrec := Cvc.Solver.instReprOption.repr }

def Cvc.Solver.Option.name :

Option → String

The option's name, as cvc5 spells it.

Equations

(Cvc.Solver.Option.base a).name = a.name
(Cvc.Solver.Option.smt a).name = a.name
(Cvc.Solver.Option.printing a).name = a.name
(Cvc.Solver.Option.proof a).name = a.name
(Cvc.Solver.Option.sat a).name = a.name
(Cvc.Solver.Option.theory a).name = a.name
(Cvc.Solver.Option.arith a).name = a.name
(Cvc.Solver.Option.arrays a).name = a.name
(Cvc.Solver.Option.bv a).name = a.name
(Cvc.Solver.Option.strings a).name = a.name
(Cvc.Solver.Option.uf a).name = a.name
(Cvc.Solver.Option.quant a).name = a.name
(Cvc.Solver.Option.sygus a).name = a.name

Instances For

@[reducible]

def Cvc.Solver.Option.argType :

Option → Type

The type of the value the option expects.

Equations

(Cvc.Solver.Option.base opt).argType = opt.argType
(Cvc.Solver.Option.smt opt).argType = opt.argType
(Cvc.Solver.Option.printing opt).argType = opt.argType
(Cvc.Solver.Option.proof opt).argType = opt.argType
(Cvc.Solver.Option.sat opt).argType = opt.argType
(Cvc.Solver.Option.theory opt).argType = opt.argType
(Cvc.Solver.Option.arith opt).argType = opt.argType
(Cvc.Solver.Option.arrays opt).argType = opt.argType
(Cvc.Solver.Option.bv opt).argType = opt.argType
(Cvc.Solver.Option.strings opt).argType = opt.argType
(Cvc.Solver.Option.uf opt).argType = opt.argType
(Cvc.Solver.Option.quant opt).argType = opt.argType
(Cvc.Solver.Option.sygus opt).argType = opt.argType

Instances For

def Cvc.Solver.Option.valueString (opt : Option) :

opt.argType → String

The value as the string cvc5 expects.

Equations

(Cvc.Solver.Option.base opt).valueString v = opt.valueString v
(Cvc.Solver.Option.smt opt).valueString v = opt.valueString v
(Cvc.Solver.Option.printing opt).valueString v = opt.valueString v
(Cvc.Solver.Option.proof opt).valueString v = opt.valueString v
(Cvc.Solver.Option.sat opt).valueString v = opt.valueString v
(Cvc.Solver.Option.theory opt).valueString v = opt.valueString v
(Cvc.Solver.Option.arith opt).valueString v = opt.valueString v
(Cvc.Solver.Option.arrays opt).valueString v = opt.valueString v
(Cvc.Solver.Option.bv opt).valueString v = opt.valueString v
(Cvc.Solver.Option.strings opt).valueString v = opt.valueString v
(Cvc.Solver.Option.uf opt).valueString v = opt.valueString v
(Cvc.Solver.Option.quant opt).valueString v = opt.valueString v
(Cvc.Solver.Option.sygus opt).valueString v = opt.valueString v

Instances For

def Cvc.Solver.Option.toStrings (opt : Option) (v : opt.argType) :

String × String

The flag and the value to hand cvc5's string-based setOption.

Equations

opt.toStrings v = (opt.name, opt.valueString v)

Instances For

Every option at the top level #

One abbreviation per option, named after its category and itself, so that .smt_produceModels stands for .smt .produceModels wherever an Option is expected, patterns included.

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_incremental :

--incremental: Enable incremental solving.

Equations

Cvc.Solver.Option.base_incremental = Cvc.Solver.Option.base Cvc.Solver.Option.Base.incremental

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_output :

--output: Enable output tag.

Equations

Cvc.Solver.Option.base_output = Cvc.Solver.Option.base Cvc.Solver.Option.Base.output

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_parseOnly :

--parse-only: Exit after parsing input.

Equations

Cvc.Solver.Option.base_parseOnly = Cvc.Solver.Option.base Cvc.Solver.Option.Base.parseOnly

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_preprocessOnly :

--preprocess-only: Exit after preprocessing input.

Equations

Cvc.Solver.Option.base_preprocessOnly = Cvc.Solver.Option.base Cvc.Solver.Option.Base.preprocessOnly

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_rlimit :

--rlimit: Set resource limit.

Equations

Cvc.Solver.Option.base_rlimit = Cvc.Solver.Option.base Cvc.Solver.Option.Base.rlimit

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_rlimitPer :

--rlimit-per: Set resource limit per query.

Equations

Cvc.Solver.Option.base_rlimitPer = Cvc.Solver.Option.base Cvc.Solver.Option.Base.rlimitPer

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_stats :

--stats: Give statistics on exit.

Equations

Cvc.Solver.Option.base_stats = Cvc.Solver.Option.base Cvc.Solver.Option.Base.stats

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_statsAll :

--stats-all: Print unchanged (defaulted) statistics as well.

Equations

Cvc.Solver.Option.base_statsAll = Cvc.Solver.Option.base Cvc.Solver.Option.Base.statsAll

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_statsInternal :

--stats-internal: Print internal (non-public) statistics as well.

Equations

Cvc.Solver.Option.base_statsInternal = Cvc.Solver.Option.base Cvc.Solver.Option.Base.statsInternal

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_tlimit :

--tlimit: Set time limit in milliseconds of wall clock time.

Equations

Cvc.Solver.Option.base_tlimit = Cvc.Solver.Option.base Cvc.Solver.Option.Base.tlimit

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_tlimitPer :

--tlimit-per: Set time limit per query in milliseconds.

Equations

Cvc.Solver.Option.base_tlimitPer = Cvc.Solver.Option.base Cvc.Solver.Option.Base.tlimitPer

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_verbosity :

--verbosity: The verbosity level of cvc5.

Equations

Cvc.Solver.Option.base_verbosity = Cvc.Solver.Option.base Cvc.Solver.Option.Base.verbosity

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_seed :

--seed: Seed for random number generator.

Equations

Cvc.Solver.Option.base_seed = Cvc.Solver.Option.base Cvc.Solver.Option.Base.seed

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.base_statsEveryQuery :

--stats-every-query.

In incremental mode, print stats after every satisfiability or validity query.

Equations

Cvc.Solver.Option.base_statsEveryQuery = Cvc.Solver.Option.base Cvc.Solver.Option.Base.statsEveryQuery

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_decision :

--decision: Choose decision mode.

Equations

Cvc.Solver.Option.smt_decision = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.decision

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkAbducts :

--check-abducts: Checks whether produced solutions to get-abduct are correct.

Equations

Cvc.Solver.Option.smt_checkAbducts = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkAbducts

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkInterpolants :

--check-interpolants: Checks whether produced solutions to get-interpolant are correct.

Equations

Cvc.Solver.Option.smt_checkInterpolants = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkInterpolants

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkModelSubsolver :

--check-model-subsolver.

Use subsolver to compute values when applicable in calls to get-value and check-models.

Equations

Cvc.Solver.Option.smt_checkModelSubsolver = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkModelSubsolver

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkModels :

--check-models.

After SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions.

Equations

Cvc.Solver.Option.smt_checkModels = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkModels

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkProofs :

--check-proofs: After UNSAT/VALID, check the generated proof (with proof).

Equations

Cvc.Solver.Option.smt_checkProofs = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkProofs

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkSynthSol :

--check-synth-sol.

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

Equations

Cvc.Solver.Option.smt_checkSynthSol = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkSynthSol

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_checkUnsatCores :

--check-unsat-cores: After UNSAT/VALID, produce and check an unsat core (expensive).

Equations

Cvc.Solver.Option.smt_checkUnsatCores = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.checkUnsatCores

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_debugCheckModels :

--debug-check-models.

After SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions.

Equations

Cvc.Solver.Option.smt_debugCheckModels = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.debugCheckModels

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceModels :

--produce-models: Support the get-value and get-model commands.

Equations

Cvc.Solver.Option.smt_produceModels = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceModels

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceProofs :

--produce-proofs: Produce proofs, support check-proofs and get-proof.

Equations

Cvc.Solver.Option.smt_produceProofs = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceProofs

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceUnsatCores :

--produce-unsat-cores.

Turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs.

Equations

Cvc.Solver.Option.smt_produceUnsatCores = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceUnsatCores

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_interpolantsMode :

--interpolants-mode: Choose interpolants production mode.

Equations

Cvc.Solver.Option.smt_interpolantsMode = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.interpolantsMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_learnedRewrite :

--learned-rewrite: Rewrite the input based on learned literals.

Equations

Cvc.Solver.Option.smt_learnedRewrite = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.learnedRewrite

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_modelCores :

--model-cores: Mode for producing model cores.

Equations

Cvc.Solver.Option.smt_modelCores = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.modelCores

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_printCoresFull :

--print-cores-full.

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

Equations

Cvc.Solver.Option.smt_printCoresFull = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.printCoresFull

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceAbducts :

--produce-abducts: Support the get-abduct command.

Equations

Cvc.Solver.Option.smt_produceAbducts = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceAbducts

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceAssertions :

--produce-assertions: Keep an assertions list. Note this option is always enabled.

Equations

Cvc.Solver.Option.smt_produceAssertions = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceAssertions

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceAssignments :

--produce-assignments: Support the get-assignment command.

Equations

Cvc.Solver.Option.smt_produceAssignments = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceAssignments

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceDifficulty :

--produce-difficulty: Enable tracking of difficulty.

Equations

Cvc.Solver.Option.smt_produceDifficulty = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceDifficulty

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceInterpolants :

--produce-interpolants: Turn on interpolation generation.

Equations

Cvc.Solver.Option.smt_produceInterpolants = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceInterpolants

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceLearnedLiterals :

--produce-learned-literals: Produce learned literals, support get-learned-literals.

Equations

Cvc.Solver.Option.smt_produceLearnedLiterals = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceLearnedLiterals

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_produceUnsatAssumptions :

--produce-unsat-assumptions: Turn on unsat assumptions generation.

Equations

Cvc.Solver.Option.smt_produceUnsatAssumptions = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.produceUnsatAssumptions

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_simplification :

--simplification: Choose simplification mode.

Equations

Cvc.Solver.Option.smt_simplification = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.simplification

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_solveBvAsInt :

--solve-bv-as-int: Mode for translating BVAnd to integer.

Equations

Cvc.Solver.Option.smt_solveBvAsInt = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.solveBvAsInt

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_solveIntAsBv :

--solve-int-as-bv.

Attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental).

Equations

Cvc.Solver.Option.smt_solveIntAsBv = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.solveIntAsBv

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_solveRealAsInt :

--solve-real-as-int.

Attempt to solve a pure real satisfiable problem as an integer problem (for non-linear).

Equations

Cvc.Solver.Option.smt_solveRealAsInt = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.solveRealAsInt

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.smt_staticLearning :

--static-learning: Use static learning (on by default).

Equations

Cvc.Solver.Option.smt_staticLearning = Cvc.Solver.Option.smt Cvc.Solver.Option.Smt.staticLearning

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_printSuccess :

--print-success: Print the "success" output required of SMT-LIBv2.

Equations

Cvc.Solver.Option.printing_printSuccess = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.printSuccess

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_dagThresh :

--dag-thresh.

Dagify common subexprs appearing > N times (1 == default, 0 == don't dagify).

Equations

Cvc.Solver.Option.printing_dagThresh = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.dagThresh

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_exprDepth :

--expr-depth: Print exprs to depth N (0 == default, -1 == no limit).

Equations

Cvc.Solver.Option.printing_exprDepth = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.exprDepth

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_outputLang :

--output-lang: Force output language.

Equations

Cvc.Solver.Option.printing_outputLang = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.outputLang

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_bvPrintConstsAsIndexedSymbols :

--bv-print-consts-as-indexed-symbols.

Print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x.

Equations

Cvc.Solver.Option.printing_bvPrintConstsAsIndexedSymbols = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.bvPrintConstsAsIndexedSymbols

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.printing_modelUPrint :

--model-u-print: Determines how to print uninterpreted elements in models.

Equations

Cvc.Solver.Option.printing_modelUPrint = Cvc.Solver.Option.printing Cvc.Solver.Option.Printing.modelUPrint

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_check :

--proof-check: Select internal proof checking mode.

Equations

Cvc.Solver.Option.proof_check = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.check

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_granularity :

--proof-granularity: Modes for proof granularity.

Equations

Cvc.Solver.Option.proof_granularity = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.granularity

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_printConclusion :

--proof-print-conclusion: Print conclusion of proof steps when printing AST.

Equations

Cvc.Solver.Option.proof_printConclusion = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.printConclusion

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_printReference :

--proof-print-reference: Print reference to original file instead of redeclaring.

Equations

Cvc.Solver.Option.proof_printReference = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.printReference

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_optResReconstructionSize :

--opt-res-reconstruction-size: Optimize resolution reconstruction to reduce proof size.

Equations

Cvc.Solver.Option.proof_optResReconstructionSize = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.optResReconstructionSize

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_chainMRes :

--proof-chain-m-res: Use chain multiset resolution.

Equations

Cvc.Solver.Option.proof_chainMRes = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.chainMRes

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_rewriteRconsRecLimit :

--proof-rewrite-rcons-rec-limit.

The matching recursion limit for reconstructing proofs of theory rewrites.

Equations

Cvc.Solver.Option.proof_rewriteRconsRecLimit = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.rewriteRconsRecLimit

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_rewriteRconsStepLimit :

--proof-rewrite-rcons-step-limit.

The limit of steps considered for reconstructing proofs of theory rewrites.

Equations

Cvc.Solver.Option.proof_rewriteRconsStepLimit = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.rewriteRconsStepLimit

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.proof_propProofMode :

--prop-proof-mode: Modes for the type of proof generated by the SAT solver.

Equations

Cvc.Solver.Option.proof_propProofMode = Cvc.Solver.Option.proof Cvc.Solver.Option.Proof.propProofMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sat_preregisterMode :

--preregister-mode: Modes for when to preregister literals.

Equations

Cvc.Solver.Option.sat_preregisterMode = Cvc.Solver.Option.sat Cvc.Solver.Option.Sat.preregisterMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sat_randomSeed :

--sat-random-seed: Sets the random seed for the sat solver.

Equations

Cvc.Solver.Option.sat_randomSeed = Cvc.Solver.Option.sat Cvc.Solver.Option.Sat.randomSeed

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.theory_condenseFunctionValues :

--condense-function-values.

Condense values for functions in models rather than explicitly representing them.

Equations

Cvc.Solver.Option.theory_condenseFunctionValues = Cvc.Solver.Option.theory Cvc.Solver.Option.Theory.condenseFunctionValues

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.theory_defaultFunctionValueMode :

--default-function-value-mode: Mode for choosing default values for functions.

Equations

Cvc.Solver.Option.theory_defaultFunctionValueMode = Cvc.Solver.Option.theory Cvc.Solver.Option.Theory.defaultFunctionValueMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.theory_eeMode :

--ee-mode: Mode for managing equalities across theory solvers.

Equations

Cvc.Solver.Option.theory_eeMode = Cvc.Solver.Option.theory Cvc.Solver.Option.Theory.eeMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_brab :

--arith-brab: Whether to use simple rounding, similar to a unit-cube test, for integers.

Equations

Cvc.Solver.Option.arith_brab = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.brab

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_rewriteEqualities :

--arith-rewrite-equalities.

Turns on the preprocessing rewrite turning equalities into a conjunction of inequalities.

Equations

Cvc.Solver.Option.arith_rewriteEqualities = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.rewriteEqualities

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_staticLearning :

--arith-static-learning.

Do arithmetic static learning for ite terms based on bounds when static learning is enabled.

Equations

Cvc.Solver.Option.arith_staticLearning = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.staticLearning

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlCov :

--nl-cov.

Whether to use the cylindrical algebraic coverings solver for non-linear arithmetic.

Equations

Cvc.Solver.Option.arith_nlCov = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlCov

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlCovLinearModel :

--nl-cov-linear-model.

Whether to use the linear model as initial guess for the cylindrical algebraic coverings solver.

Equations

Cvc.Solver.Option.arith_nlCovLinearModel = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlCovLinearModel

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExt :

--nl-ext: Incremental linearization approach to non-linear.

Equations

Cvc.Solver.Option.arith_nlExt = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExt

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtFactor :

--nl-ext-factor: Use factoring inference in non-linear incremental linearization solver.

Equations

Cvc.Solver.Option.arith_nlExtFactor = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtFactor

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtFlattenMon :

--nl-ext-flatten-mon: Use inference schema based on flattening monomials.

Equations

Cvc.Solver.Option.arith_nlExtFlattenMon = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtFlattenMon

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtRewrite :

--nl-ext-rewrite.

Do context-dependent simplification based on rewrites in non-linear solver.

Equations

Cvc.Solver.Option.arith_nlExtRewrite = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtRewrite

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtTfTplanes :

--nl-ext-tf-tplanes.

Use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver.

Equations

Cvc.Solver.Option.arith_nlExtTfTplanes = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtTfTplanes

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtTplanes :

--nl-ext-tplanes.

Use non-terminating tangent plane strategy for non-linear incremental linearization solver.

Equations

Cvc.Solver.Option.arith_nlExtTplanes = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtTplanes

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arith_nlExtTplanesInterleave :

--nl-ext-tplanes-interleave.

Interleave tangent plane strategy for non-linear incremental linearization solver.

Equations

Cvc.Solver.Option.arith_nlExtTplanesInterleave = Cvc.Solver.Option.arith Cvc.Solver.Option.Arith.nlExtTplanesInterleave

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.arrays_eagerIndex :

--arrays-eager-index: Turn on eager index splitting for generated array lemmas.

Equations

Cvc.Solver.Option.arrays_eagerIndex = Cvc.Solver.Option.arrays Cvc.Solver.Option.Arrays.eagerIndex

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_bitblast :

--bitblast: Choose bitblasting mode.

Equations

Cvc.Solver.Option.bv_bitblast = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.bitblast

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_boolToBv :

--bool-to-bv.

Convert booleans to bit-vectors of size 1 at various levels of aggressiveness.

Equations

Cvc.Solver.Option.bv_boolToBv = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.boolToBv

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_eagerEval :

--bv-eager-eval.

Perform eager context-dependent evaluation for applications of bv kinds in the equality engine.

Equations

Cvc.Solver.Option.bv_eagerEval = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.eagerEval

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_satSolver :

--bv-sat-solver: Choose which sat solver to use.

Equations

Cvc.Solver.Option.bv_satSolver = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.satSolver

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_solver :

--bv-solver: Choose bit-vector solver.

Equations

Cvc.Solver.Option.bv_solver = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.solver

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.bv_toBool :

--bv-to-bool: Lift bit-vectors of size 1 to booleans when possible.

Equations

Cvc.Solver.Option.bv_toBool = Cvc.Solver.Option.bv Cvc.Solver.Option.Bv.toBool

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_reElim :

--re-elim: Regular expression elimination mode.

Equations

Cvc.Solver.Option.strings_reElim = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.reElim

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_checkEntailLen :

--strings-check-entail-len: Check entailment between length terms to reduce splitting.

Equations

Cvc.Solver.Option.strings_checkEntailLen = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.checkEntailLen

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_deqExt :

--strings-deq-ext: Use extensionality for string disequalities.

Equations

Cvc.Solver.Option.strings_deqExt = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.deqExt

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_eagerEval :

--strings-eager-eval.

Perform eager context-dependent evaluation for applications of string kinds in the equality engine.

Equations

Cvc.Solver.Option.strings_eagerEval = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.eagerEval

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_eagerLenRe :

--strings-eager-len-re: Use regular expressions for eager length conflicts.

Equations

Cvc.Solver.Option.strings_eagerLenRe = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.eagerLenRe

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_eagerSolver :

--strings-eager-solver: Use the eager solver.

Equations

Cvc.Solver.Option.strings_eagerSolver = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.eagerSolver

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_exp :

--strings-exp: Experimental features in the theory of strings.

Equations

Cvc.Solver.Option.strings_exp = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.exp

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_fmf :

--strings-fmf: The finite model finding used by the theory of strings.

Equations

Cvc.Solver.Option.strings_fmf = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.fmf

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_lazyPp :

--strings-lazy-pp: Perform string preprocessing lazily.

Equations

Cvc.Solver.Option.strings_lazyPp = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.lazyPp

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_mbr :

--strings-mbr.

Use models to avoid reductions for extended functions that introduce quantified formulas.

Equations

Cvc.Solver.Option.strings_mbr = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.mbr

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_processLoopMode :

--strings-process-loop-mode: Determines how to process looping string equations.

Equations

Cvc.Solver.Option.strings_processLoopMode = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.processLoopMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.strings_regexpInclusion :

--strings-regexp-inclusion.

Use regular expression inclusion for finding conflicts and avoiding regular expression unfolding.

Equations

Cvc.Solver.Option.strings_regexpInclusion = Cvc.Solver.Option.strings Cvc.Solver.Option.Strings.regexpInclusion

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_eagerArithBvConv :

--eager-arith-bv-conv.

Eagerly expand bit-vector to arithmetic conversions during preprocessing.

Equations

Cvc.Solver.Option.uf_eagerArithBvConv = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.eagerArithBvConv

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_symmetryBreaker :

--symmetry-breaker: Use UF symmetry breaker (Deharbe et al., CADE 2011).

Equations

Cvc.Solver.Option.uf_symmetryBreaker = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.symmetryBreaker

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_lazyLl :

--uf-lazy-ll: Do lambda lifting lazily.

Equations

Cvc.Solver.Option.uf_lazyLl = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.lazyLl

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_ss :

--uf-ss: Mode of operation for uf with cardinality solver.

Equations

Cvc.Solver.Option.uf_ss = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.ss

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_ssAbortCard :

--uf-ss-abort-card.

Tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default).

Equations

Cvc.Solver.Option.uf_ssAbortCard = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.ssAbortCard

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.uf_ssFair :

--uf-ss-fair: Use fair strategy for finite model finding multiple sorts.

Equations

Cvc.Solver.Option.uf_ssFair = Cvc.Solver.Option.uf Cvc.Solver.Option.Uf.ssFair

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_enumInst :

--enum-inst.

Enumerative instantiation: instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown.

Equations

Cvc.Solver.Option.quant_enumInst = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.enumInst

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_fullSaturateQuant :

--full-saturate-quant.

Resort to full effort techniques instead of answering unknown due to limited quantifier reasoning. Currently enables enumerative instantiation.

Equations

Cvc.Solver.Option.quant_fullSaturateQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.fullSaturateQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_printInst :

--print-inst: Print format for printing instantiations.

Equations

Cvc.Solver.Option.quant_printInst = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.printInst

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cbqi :

--cbqi: Enable conflict-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_cbqi = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cbqi

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cbqiAllConflict :

--cbqi-all-conflict.

Add all available conflicting instances during conflict-based instantiation.

Equations

Cvc.Solver.Option.quant_cbqiAllConflict = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cbqiAllConflict

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cbqiMode :

--cbqi-mode: What effort to apply conflict find mechanism.

Equations

Cvc.Solver.Option.quant_cbqiMode = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cbqiMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cegqi :

--cegqi: Turns on counterexample-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_cegqi = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cegqi

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cegqiBv :

--cegqi-bv.

Use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors.

Equations

Cvc.Solver.Option.quant_cegqiBv = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cegqiBv

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cegqiInnermost :

--cegqi-innermost.

Only process innermost quantified formulas in counterexample-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_cegqiInnermost = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cegqiInnermost

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cegqiMidpoint :

--cegqi-midpoint.

Choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_cegqiMidpoint = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cegqiMidpoint

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_cegqiNestedQe :

--cegqi-nested-qe.

Process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_cegqiNestedQe = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.cegqiNestedQe

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_eMatching :

--e-matching: Whether to do heuristic E-matching.

Equations

Cvc.Solver.Option.quant_eMatching = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.eMatching

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_elimTautQuant :

--elim-taut-quant: Eliminate tautological disjuncts of quantified formulas.

Equations

Cvc.Solver.Option.quant_elimTautQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.elimTautQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_enumInstInterleave :

--enum-inst-interleave: Interleave enumerative instantiation with other techniques.

Equations

Cvc.Solver.Option.quant_enumInstInterleave = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.enumInstInterleave

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_enumInstSum :

--enum-inst-sum.

Enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum.

Equations

Cvc.Solver.Option.quant_enumInstSum = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.enumInstSum

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_extRewriteQuant :

--ext-rewrite-quant: Apply extended rewriting to bodies of quantified formulas.

Equations

Cvc.Solver.Option.quant_extRewriteQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.extRewriteQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_finiteModelFind :

--finite-model-find: Use finite model finding heuristic for quantifier instantiation.

Equations

Cvc.Solver.Option.quant_finiteModelFind = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.finiteModelFind

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_fmfBound :

--fmf-bound: Finite model finding on bounded quantification.

Equations

Cvc.Solver.Option.quant_fmfBound = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.fmfBound

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_fmfTypeCompletionThresh :

--fmf-type-completion-thresh.

The maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted.

Equations

Cvc.Solver.Option.quant_fmfTypeCompletionThresh = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.fmfTypeCompletionThresh

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_ieval :

--ieval: Mode for using instantiation evaluation.

Equations

Cvc.Solver.Option.quant_ieval = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.ieval

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_instLocal :

--inst-local: Instantiations are local to the SAT context.

Equations

Cvc.Solver.Option.quant_instLocal = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.instLocal

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_instMaxRounds :

--inst-max-rounds: Maximum number of instantiation rounds (-1 == no limit, default).

Equations

Cvc.Solver.Option.quant_instMaxRounds = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.instMaxRounds

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_instNoEntail :

--inst-no-entail.

Do not consider instances of quantified formulas that are currently entailed.

Equations

Cvc.Solver.Option.quant_instNoEntail = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.instNoEntail

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_instWhen :

--inst-when: When to apply instantiation.

Equations

Cvc.Solver.Option.quant_instWhen = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.instWhen

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_iteLiftQuant :

--ite-lift-quant: Ite lifting mode for quantified formulas.

Equations

Cvc.Solver.Option.quant_iteLiftQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.iteLiftQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_macrosQuant :

--macros-quant: Perform quantifiers macro expansion.

Equations

Cvc.Solver.Option.quant_macrosQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.macrosQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_macrosQuantMode :

--macros-quant-mode: Mode for quantifiers macro expansion.

Equations

Cvc.Solver.Option.quant_macrosQuantMode = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.macrosQuantMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_mbqi :

--mbqi: Use model-based quantifier instantiation.

Equations

Cvc.Solver.Option.quant_mbqi = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.mbqi

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_mbqiCheckTimeout :

--mbqi-check-timeout.

Timeout (in milliseconds) for verifying subcalls for model-based instantiation (0 == no limit).

Equations

Cvc.Solver.Option.quant_mbqiCheckTimeout = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.mbqiCheckTimeout

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_mbqiEnum :

--mbqi-enum: Use fast enumeration to augment instantiations from MBQI.

Equations

Cvc.Solver.Option.quant_mbqiEnum = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.mbqiEnum

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_mbqiOneInstPerRound :

--mbqi-one-inst-per-round: Only add one instantiation per quantifier per round for mbqi.

Equations

Cvc.Solver.Option.quant_mbqiOneInstPerRound = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.mbqiOneInstPerRound

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_miniscopeQuant :

--miniscope-quant: Miniscope mode for quantified formulas.

Equations

Cvc.Solver.Option.quant_miniscopeQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.miniscopeQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_miniscopeQuantUser :

--miniscope-quant-user: Miniscope quantified formulas with user patterns.

Equations

Cvc.Solver.Option.quant_miniscopeQuantUser = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.miniscopeQuantUser

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_multiTriggerCache :

--multi-trigger-cache: Caching version of multi triggers.

Equations

Cvc.Solver.Option.quant_multiTriggerCache = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.multiTriggerCache

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_multiTriggerLinear :

--multi-trigger-linear.

Implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms.

Equations

Cvc.Solver.Option.quant_multiTriggerLinear = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.multiTriggerLinear

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_multiTriggerPriority :

--multi-trigger-priority.

Only try multi triggers if single triggers give no instantiations.

Equations

Cvc.Solver.Option.quant_multiTriggerPriority = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.multiTriggerPriority

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_multiTriggerWhenSingle :

--multi-trigger-when-single: Select multi triggers when single triggers exist.

Equations

Cvc.Solver.Option.quant_multiTriggerWhenSingle = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.multiTriggerWhenSingle

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_preSkolemQuant :

--pre-skolem-quant.

Modes to apply skolemization eagerly to bodies of quantified formulas.

Equations

Cvc.Solver.Option.quant_preSkolemQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.preSkolemQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_prenexQuantUser :

--prenex-quant-user: Prenex quantified formulas with user patterns.

Equations

Cvc.Solver.Option.quant_prenexQuantUser = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.prenexQuantUser

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_printInstFull :

--print-inst-full: Print instantiations for formulas that do not have given identifiers.

Equations

Cvc.Solver.Option.quant_printInstFull = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.printInstFull

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_alphaEquiv :

--quant-alpha-equiv: Infer alpha equivalence between quantified formulas.

Equations

Cvc.Solver.Option.quant_alphaEquiv = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.alphaEquiv

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_dsplit :

--quant-dsplit: Mode for dynamic quantifiers splitting.

Equations

Cvc.Solver.Option.quant_dsplit = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.dsplit

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_relevantTriggers :

--relevant-triggers: Prefer triggers that are more relevant based on SInE style analysis.

Equations

Cvc.Solver.Option.quant_relevantTriggers = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.relevantTriggers

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_subCbqi :

--sub-cbqi: Enable conflict-based instantiation subsolver strategy.

Equations

Cvc.Solver.Option.quant_subCbqi = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.subCbqi

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_termDbMode :

--term-db-mode: Which ground terms to consider for instantiation.

Equations

Cvc.Solver.Option.quant_termDbMode = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.termDbMode

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_triggerSel :

--trigger-sel: Selection mode for triggers.

Equations

Cvc.Solver.Option.quant_triggerSel = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.triggerSel

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_userPat :

--user-pat: Policy for handling user-provided patterns for quantifier instantiation.

Equations

Cvc.Solver.Option.quant_userPat = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.userPat

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_varElimQuant :

--var-elim-quant: Enable simple variable elimination for quantified formulas.

Equations

Cvc.Solver.Option.quant_varElimQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.varElimQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_varEntEqElimQuant :

--var-ent-eq-elim-quant.

Enable variable elimination for quantified formulas that infers entailed equalities corresponding to eliminations.

Equations

Cvc.Solver.Option.quant_varEntEqElimQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.varEntEqElimQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.quant_varIneqElimQuant :

--var-ineq-elim-quant.

Enable variable elimination based on infinite projection of unbound arithmetic variables.

Equations

Cvc.Solver.Option.quant_varIneqElimQuant = Cvc.Solver.Option.quant Cvc.Solver.Option.Quant.varIneqElimQuant

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_abortSize :

--sygus-abort-size.

Tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default).

Equations

Cvc.Solver.Option.sygus_abortSize = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.abortSize

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_fair :

--sygus-fair: If and how to apply fairness for sygus.

Equations

Cvc.Solver.Option.sygus_fair = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.fair

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_rewriter :

--sygus-rewriter: If and how to apply rewriting for sygus symmetry breaking.

Equations

Cvc.Solver.Option.sygus_rewriter = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.rewriter

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_simpleSymBreak :

--sygus-simple-sym-break.

If and how to apply simple symmetry breaking based on the grammar for smart enumeration.

Equations

Cvc.Solver.Option.sygus_simpleSymBreak = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.simpleSymBreak

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_symBreakPbe :

--sygus-sym-break-pbe: Sygus symmetry breaking lemmas based on pbe conjectures.

Equations

Cvc.Solver.Option.sygus_symBreakPbe = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.symBreakPbe

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_cegisSample :

--cegis-sample.

Mode for using samples in the counterexample-guided inductive synthesis loop.

Equations

Cvc.Solver.Option.sygus_cegisSample = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.cegisSample

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_sygus :

--sygus: Support SyGuS commands.

Equations

Cvc.Solver.Option.sygus_sygus = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.sygus

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_addConstGrammar :

--sygus-add-const-grammar: Statically add constants appearing in conjecture to grammars.

Equations

Cvc.Solver.Option.sygus_addConstGrammar = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.addConstGrammar

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_coreConnective :

--sygus-core-connective.

Use unsat core analysis to construct Boolean connective to sygus conjectures.

Equations

Cvc.Solver.Option.sygus_coreConnective = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.coreConnective

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_enum :

--sygus-enum: Mode for sygus enumeration.

Equations

Cvc.Solver.Option.sygus_enum = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.enum

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_evalUnfold :

--sygus-eval-unfold: Modes for sygus evaluation unfolding.

Equations

Cvc.Solver.Option.sygus_evalUnfold = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.evalUnfold

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_grammarCons :

--sygus-grammar-cons: Mode for SyGuS grammar construction.

Equations

Cvc.Solver.Option.sygus_grammarCons = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.grammarCons

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_inst :

--sygus-inst: Enable SyGuS instantiation quantifiers module.

Equations

Cvc.Solver.Option.sygus_inst = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.inst

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_invTempl :

--sygus-inv-templ.

Template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none).

Equations

Cvc.Solver.Option.sygus_invTempl = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.invTempl

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_minGrammar :

--sygus-min-grammar: Statically minimize sygus grammars.

Equations

Cvc.Solver.Option.sygus_minGrammar = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.minGrammar

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_out :

--sygus-out: Output mode for sygus.

Equations

Cvc.Solver.Option.sygus_out = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.out

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_pbe :

--sygus-pbe.

Enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures.

Equations

Cvc.Solver.Option.sygus_pbe = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.pbe

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_repairConst :

--sygus-repair-const: Use approach to repair constants in sygus candidate solutions.

Equations

Cvc.Solver.Option.sygus_repairConst = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.repairConst

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_si :

--sygus-si: Mode for processing single invocation synthesis conjectures.

Equations

Cvc.Solver.Option.sygus_si = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.si

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_siAbort :

--sygus-si-abort: Abort if synthesis conjecture is not single invocation.

Equations

Cvc.Solver.Option.sygus_siAbort = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.siAbort

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_siRcons :

--sygus-si-rcons: Policy for reconstructing solutions for single invocation conjectures.

Equations

Cvc.Solver.Option.sygus_siRcons = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.siRcons

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_stream :

--sygus-stream.

Enumerate a stream of solutions instead of terminating after the first one.

Equations

Cvc.Solver.Option.sygus_stream = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.stream

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_unifPi :

--sygus-unif-pi: Mode for synthesis via piecewise-indepedent unification.

Equations

Cvc.Solver.Option.sygus_unifPi = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.unifPi

Instances For

@[reducible, match_pattern, inline]

abbrev Cvc.Solver.Option.sygus_verifyTimeout :

--sygus-verify-timeout.

Timeout (in milliseconds) for verifying satisfiability of synthesized terms (0 == no limit).

Equations

Cvc.Solver.Option.sygus_verifyTimeout = Cvc.Solver.Option.sygus Cvc.Solver.Option.Sygus.verifyTimeout

Instances For