Modes
Some API functions require a configuration mode argument, e.g.,
cvc5_block_model().
The following enum classes define such configuration modes.
-
enum Cvc5BlockModelsMode
Mode for blocking models.
Specifies how models are blocked in Solver::blockModel and Solver::blockModelValues.
Values:
-
enumerator CVC5_BLOCK_MODELS_MODE_LITERALS
Block models based on the SAT skeleton.
-
enumerator CVC5_BLOCK_MODELS_MODE_VALUES
Block models based on the concrete model values for the free variables.
-
enumerator CVC5_BLOCK_MODELS_MODE_LAST
-
enumerator CVC5_BLOCK_MODELS_MODE_LITERALS
-
const char *cvc5_modes_block_models_mode_to_string(Cvc5BlockModelsMode mode)
Get a string representation of a Cvc5BlockModelsMode.
- Parameters:
mode – The mode.
- Returns:
The string representation.
-
enum Cvc5LearnedLitType
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.
Values:
-
enumerator CVC5_LEARNED_LIT_TYPE_PREPROCESS_SOLVED
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.
-
enumerator CVC5_LEARNED_LIT_TYPE_PREPROCESS
A top-level literal (unit clause) from the preprocessed set of input formulas.
-
enumerator CVC5_LEARNED_LIT_TYPE_INPUT
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.
-
enumerator CVC5_LEARNED_LIT_TYPE_SOLVABLE
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.
-
enumerator CVC5_LEARNED_LIT_TYPE_CONSTANT_PROP
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).
-
enumerator CVC5_LEARNED_LIT_TYPE_INTERNAL
Any internal literal that does not fall into the above categories.
-
enumerator CVC5_LEARNED_LIT_TYPE_UNKNOWN
Special case for when produce-learned-literals is not set.
-
enumerator CVC5_LEARNED_LIT_TYPE_LAST
-
enumerator CVC5_LEARNED_LIT_TYPE_PREPROCESS_SOLVED
-
const char *cvc5_modes_learned_lit_type_to_string(Cvc5LearnedLitType type)
Get a string representation of a Cvc5LearnedLitType.
- Parameters:
type – The learned literal type.
- Returns:
The string representation.
-
enum Cvc5ProofComponent
Components to include in a proof.
Values:
-
enumerator CVC5_PROOF_COMPONENT_RAW_PREPROCESS
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.
-
enumerator CVC5_PROOF_COMPONENT_PREPROCESS
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.
-
enumerator CVC5_PROOF_COMPONENT_SAT
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.
-
enumerator CVC5_PROOF_COMPONENT_THEORY_LEMMAS
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.
-
enumerator CVC5_PROOF_COMPONENT_FULL
A proof of false whose free assumptions are a subset of the input formulas F1), … Fm.
Only valid immediately after an unsat response.
-
enumerator CVC5_PROOF_COMPONENT_LAST
-
enumerator CVC5_PROOF_COMPONENT_RAW_PREPROCESS
-
const char *cvc5_modes_proof_component_to_string(Cvc5ProofComponent pc)
Get a string representation of a Cvc5ProofComponent.
- Parameters:
pc – The proof component.
- Returns:
The string representation.
-
enum Cvc5ProofFormat
Proof format used for proof printing.
Values:
-
enumerator CVC5_PROOF_FORMAT_NONE
Do not translate proof output.
-
enumerator CVC5_PROOF_FORMAT_DOT
Output DOT proof.
-
enumerator CVC5_PROOF_FORMAT_LFSC
Output LFSC proof.
-
enumerator CVC5_PROOF_FORMAT_ALETHE
Output Alethe proof.
-
enumerator CVC5_PROOF_FORMAT_CPC
Output Cooperating Proof Calculus proof based on Eunoia signatures.
-
enumerator CVC5_PROOF_FORMAT_DEFAULT
Use the proof format mode set in the solver options.
-
enumerator CVC5_PROOF_FORMAT_LAST
-
enumerator CVC5_PROOF_FORMAT_NONE
-
const char *cvc5_modes_proof_format_to_string(Cvc5ProofFormat format)
Get a string representation of a Cvc5ProofFormat.
- Parameters:
format – The proof format.
- Returns:
The string representation.
-
enum Cvc5FindSynthTarget
Find synthesis targets, used as an argument to Solver::findSynth. These specify various kinds of terms that can be found by this method.
Values:
-
enumerator CVC5_FIND_SYNTH_TARGET_ENUM
Find the next term in the enumeration of the target grammar.
-
enumerator CVC5_FIND_SYNTH_TARGET_REWRITE
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.
-
enumerator CVC5_FIND_SYNTH_TARGET_REWRITE_UNSOUND
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.
-
enumerator CVC5_FIND_SYNTH_TARGET_REWRITE_INPUT
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.
-
enumerator CVC5_FIND_SYNTH_TARGET_QUERY
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.
-
enumerator CVC5_FIND_SYNTH_TARGET_LAST
-
enumerator CVC5_FIND_SYNTH_TARGET_ENUM
-
const char *cvc5_modes_find_synth_target_to_string(Cvc5FindSynthTarget target)
Get a string representation of a Cvc5FindSynthTarget.
- Parameters:
target – The synthesis find target.
- Returns:
The string representation.