inductive cvc5.UnknownExplanation : Type

The different reasons for returning an "unknown" result.

• REQUIRES_FULL_CHECK : UnknownExplanation

  Full satisfiability check required (e.g., if only preprocessing was performed).

• INCOMPLETE : UnknownExplanation

  Incomplete theory solver.

• TIMEOUT : UnknownExplanation

  Time limit reached.

• RESOURCEOUT : UnknownExplanation

  Resource limit reached.

• MEMOUT : UnknownExplanation

  Memory limit reached.

• INTERRUPTED : UnknownExplanation

  Solver was interrupted.

• UNSUPPORTED : UnknownExplanation

  Unsupported feature encountered.

• OTHER : UnknownExplanation

  Other reason.

• REQUIRES_CHECK_AGAIN : UnknownExplanation

  Requires another satisfiability check

• UNKNOWN_REASON : UnknownExplanation

  No specific reason given.

instance cvc5.instInhabitedUnknownExplanation : Inhabited UnknownExplanation

Equations

• cvc5.instInhabitedUnknownExplanation = { default := cvc5.UnknownExplanation.REQUIRES_FULL_CHECK }

instance cvc5.instReprUnknownExplanation : Repr UnknownExplanation

Equations

• cvc5.instReprUnknownExplanation = { reprPrec := cvc5.reprUnknownExplanation✝ }

instance cvc5.instBEqUnknownExplanation : BEq UnknownExplanation

Equations

• cvc5.instBEqUnknownExplanation = { beq := cvc5.beqUnknownExplanation✝ }

instance cvc5.instDecidableEqUnknownExplanation : DecidableEq UnknownExplanation

Equations

• cvc5.instDecidableEqUnknownExplanation x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.RoundingMode : Type

Rounding modes for floating-point numbers.

For many floating-point operations, infinitely precise results may not be representable with the number of available bits. Thus, the results are rounded in a certain way to one of the representable floating-point numbers.

\verbatim embed:rst:leading-asterisk These rounding modes directly follow the SMT-LIB theory for floating-point arithmetic, which in turn is based on IEEE Standard 754 :cite:IEEE754. The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754. \endverbatim

• ROUND_NEAREST_TIES_TO_EVEN : RoundingMode

  Round to the nearest even number.

  If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with an even least significant digit will be delivered.

• ROUND_TOWARD_POSITIVE : RoundingMode

  Round towards positive infinity (SMT-LIB: +oo).

  The result shall be the format's floating-point number (possibly +oo) closest to and no less than the infinitely precise result.

• ROUND_TOWARD_NEGATIVE : RoundingMode

  Round towards negative infinity (-oo).

  The result shall be the format's floating-point number (possibly -oo) closest to and no less than the infinitely precise result.

• ROUND_TOWARD_ZERO : RoundingMode

  Round towards zero.

  The result shall be the format's floating-point number closest to and no greater in magnitude than the infinitely precise result.

• ROUND_NEAREST_TIES_TO_AWAY : RoundingMode

  Round to the nearest number away from zero.

  If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near), the one with larger magnitude will be selected.

instance cvc5.instInhabitedRoundingMode : Inhabited RoundingMode

Equations

• cvc5.instInhabitedRoundingMode = { default := cvc5.RoundingMode.ROUND_NEAREST_TIES_TO_EVEN }

instance cvc5.instReprRoundingMode : Repr RoundingMode

Equations

• cvc5.instReprRoundingMode = { reprPrec := cvc5.reprRoundingMode✝ }

instance cvc5.instBEqRoundingMode : BEq RoundingMode

Equations

• cvc5.instBEqRoundingMode = { beq := cvc5.beqRoundingMode✝ }

instance cvc5.instDecidableEqRoundingMode : DecidableEq RoundingMode

Equations

• cvc5.instDecidableEqRoundingMode x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.BlockModelsMode : Type

Mode for blocking models.

Specifies how models are blocked in Solver::blockModel and Solver::blockModelValues.

• LITERALS : BlockModelsMode

  Block models based on the SAT skeleton.

• VALUES : BlockModelsMode

  Block models based on the concrete model values for the free variables.

instance cvc5.instInhabitedBlockModelsMode : Inhabited BlockModelsMode

Equations

• cvc5.instInhabitedBlockModelsMode = { default := cvc5.BlockModelsMode.LITERALS }

instance cvc5.instReprBlockModelsMode : Repr BlockModelsMode

Equations

• cvc5.instReprBlockModelsMode = { reprPrec := cvc5.reprBlockModelsMode✝ }

instance cvc5.instBEqBlockModelsMode : BEq BlockModelsMode

Equations

• cvc5.instBEqBlockModelsMode = { beq := cvc5.beqBlockModelsMode✝ }

instance cvc5.instDecidableEqBlockModelsMode : DecidableEq BlockModelsMode

Equations

• cvc5.instDecidableEqBlockModelsMode x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.LearnedLitType : Type

Types of learned literals.

Specifies categories of literals learned for the method Solver::getLearnedLiterals.

Note that a literal may conceptually belong to multiple categories. We classify literals based on the first criteria in this list that they meet.

• PREPROCESS_SOLVED : LearnedLitType

  An equality that was turned into a substitution during preprocessing.

  In particular, literals in this category are of the form (= x t) where x does not occur in t.

• PREPROCESS : LearnedLitType

  A top-level literal (unit clause) from the preprocessed set of input formulas.

• INPUT : LearnedLitType

  A literal from the preprocessed set of input formulas that does not occur at top-level after preprocessing.

  Typically), this is the most interesting category of literals to learn.

• SOLVABLE : LearnedLitType

  An internal literal that is solvable for an input variable.

  In particular, literals in this category are of the form (= x t) where x does not occur in t, the preprocessed set of input formulas contains the term x, but not the literal (= x t).

  Note that solvable literals can be turned into substitutions during preprocessing.

• CONSTANT_PROP : LearnedLitType

  An internal literal that can be made into a constant propagation for an input term.

  In particular, literals in this category are of the form (= t c) where c is a constant, the preprocessed set of input formulas contains the term t, but not the literal (= t c).

• INTERNAL : LearnedLitType

  Any internal literal that does not fall into the above categories.

• UNKNOWN : LearnedLitType

  Special case for when produce-learned-literals is not set.

instance cvc5.instInhabitedLearnedLitType : Inhabited LearnedLitType

Equations

• cvc5.instInhabitedLearnedLitType = { default := cvc5.LearnedLitType.PREPROCESS_SOLVED }

instance cvc5.instReprLearnedLitType : Repr LearnedLitType

Equations

• cvc5.instReprLearnedLitType = { reprPrec := cvc5.reprLearnedLitType✝ }

instance cvc5.instBEqLearnedLitType : BEq LearnedLitType

Equations

• cvc5.instBEqLearnedLitType = { beq := cvc5.beqLearnedLitType✝ }

instance cvc5.instDecidableEqLearnedLitType : DecidableEq LearnedLitType

Equations

• cvc5.instDecidableEqLearnedLitType x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.ProofComponent : Type

Components to include in a proof.

• RAW_PREPROCESS : ProofComponent

  Proofs of G1 ... Gn whose free assumptions are a subset of F1, ... Fm, where:

  • G1, ... Gn are the preprocessed input formulas,
  • F1, ... Fm are the input formulas.

  Note that G1 ... Gn may be arbitrary formulas, not necessarily clauses.

• PREPROCESS : ProofComponent

  Proofs of Gu1 ... Gun whose free assumptions are Fu1, ... Fum, where:

  • Gu1, ... Gun are clauses corresponding to input formulas used in the SAT proof,
  • Fu1, ... Fum is the subset of the input formulas that are used in the SAT proof (i.e. the unsat core).

  Note that Gu1 ... Gun are clauses that are added to the SAT solver before its main search.

  Only valid immediately after an unsat response.

• SAT : ProofComponent

  A proof of false whose free assumptions are Gu1, ... Gun, L1 ... Lk, where:

  • Gu1, ... Gun, is a set of clauses corresponding to input formulas,
  • L1, ..., Lk is a set of clauses corresponding to theory lemmas.

  Only valid immediately after an unsat response.

• THEORY_LEMMAS : ProofComponent

  Proofs of L1 ... Lk where:

  • L1, ..., Lk are clauses corresponding to theory lemmas used in the SAT proof.

  In contrast to proofs given for preprocess, L1 ... Lk are clauses that are added to the SAT solver after its main search.

  Only valid immediately after an unsat response.

• FULL : ProofComponent

  A proof of false whose free assumptions are a subset of the input formulas F1), ... Fm.

  Only valid immediately after an unsat response.

instance cvc5.instInhabitedProofComponent : Inhabited ProofComponent

Equations

• cvc5.instInhabitedProofComponent = { default := cvc5.ProofComponent.RAW_PREPROCESS }

instance cvc5.instReprProofComponent : Repr ProofComponent

Equations

• cvc5.instReprProofComponent = { reprPrec := cvc5.reprProofComponent✝ }

instance cvc5.instBEqProofComponent : BEq ProofComponent

Equations

• cvc5.instBEqProofComponent = { beq := cvc5.beqProofComponent✝ }

instance cvc5.instDecidableEqProofComponent : DecidableEq ProofComponent

Equations

• cvc5.instDecidableEqProofComponent x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.ProofFormat : Type

Proof format used for proof printing.

• NONE : ProofFormat

  Do not translate proof output.

• DOT : ProofFormat

  Output DOT proof.

• LFSC : ProofFormat

  Output LFSC proof.

• ALETHE : ProofFormat

  Output Alethe proof.

• CPC : ProofFormat

  Output Cooperating Proof Calculus proof based on Eunoia signatures.

• DEFAULT : ProofFormat

  Use the proof format mode set in the solver options.

instance cvc5.instInhabitedProofFormat : Inhabited ProofFormat

Equations

• cvc5.instInhabitedProofFormat = { default := cvc5.ProofFormat.NONE }

instance cvc5.instReprProofFormat : Repr ProofFormat

Equations

• cvc5.instReprProofFormat = { reprPrec := cvc5.reprProofFormat✝ }

instance cvc5.instBEqProofFormat : BEq ProofFormat

Equations

• cvc5.instBEqProofFormat = { beq := cvc5.beqProofFormat✝ }

instance cvc5.instDecidableEqProofFormat : DecidableEq ProofFormat

Equations

• cvc5.instDecidableEqProofFormat x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.FindSynthTarget : Type

Find synthesis targets, used as an argument to Solver::findSynth. These specify various kinds of terms that can be found by this method.

• ENUM : FindSynthTarget

  Find the next term in the enumeration of the target grammar.

• REWRITE : FindSynthTarget

  Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE). If so, the equality (= t s) is returned by findSynth.

  This can be used to synthesize rewrite rules. Note if the rewriter is set to none (--sygus-rewrite=none), this indicates a possible rewrite when implementing a rewriter from scratch.

• REWRITE_UNSOUND : FindSynthTarget

  Find a term t in the target grammar which rewrites to a term s that is not equivalent to it. If so, the equality (= t s) is returned by findSynth.

  This can be used to test the correctness of the given rewriter. Any returned rewrite indicates an unsoundness in the given rewriter.

• REWRITE_INPUT : FindSynthTarget

  Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).

  This can be used to synthesize rewrite rules that apply to the current problem.

• QUERY : FindSynthTarget

  Find a query over the given grammar. If the given grammar generates terms that are not Boolean, we consider equalities over terms from the given grammar.

  The algorithm for determining which queries to generate is configured by --sygus-query-gen=MODE. Queries that are internally solved can be filtered by the option --sygus-query-gen-filter-solved.

instance cvc5.instInhabitedFindSynthTarget : Inhabited FindSynthTarget

Equations

• cvc5.instInhabitedFindSynthTarget = { default := cvc5.FindSynthTarget.ENUM }

instance cvc5.instReprFindSynthTarget : Repr FindSynthTarget

Equations

• cvc5.instReprFindSynthTarget = { reprPrec := cvc5.reprFindSynthTarget✝ }

instance cvc5.instBEqFindSynthTarget : BEq FindSynthTarget

Equations

• cvc5.instBEqFindSynthTarget = { beq := cvc5.beqFindSynthTarget✝ }

instance cvc5.instDecidableEqFindSynthTarget : DecidableEq FindSynthTarget

Equations

• cvc5.instDecidableEqFindSynthTarget x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive cvc5.InputLanguage : Type

The different reasons for returning an "unknown" result.

• SMT_LIB_2_6 : InputLanguage

  The SMT-LIB version 2.6 language

• SYGUS_2_1 : InputLanguage

  The SyGuS version 2.1 language.

• UNKNOWN : InputLanguage

  No language given.

instance cvc5.instInhabitedInputLanguage : Inhabited InputLanguage

Equations

• cvc5.instInhabitedInputLanguage = { default := cvc5.InputLanguage.SMT_LIB_2_6 }

instance cvc5.instReprInputLanguage : Repr InputLanguage

Equations

• cvc5.instReprInputLanguage = { reprPrec := cvc5.reprInputLanguage✝ }

instance cvc5.instBEqInputLanguage : BEq InputLanguage

Equations

• cvc5.instBEqInputLanguage = { beq := cvc5.beqInputLanguage✝ }

instance cvc5.instDecidableEqInputLanguage : DecidableEq InputLanguage

Equations

• cvc5.instDecidableEqInputLanguage x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯