Modes

Some API functions require a configuration mode argument, e.g., cvc5.Solver.blockModel(). The following enums define such configuration modes.


class cvc5.BlockModelsMode(value)

The BlockModelsMode enum

LITERALS

Block models based on the SAT skeleton.

VALUES

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


class cvc5.LearnedLitType(value)

The LearnedLitType enum

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).

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.

INTERNAL

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

PREPROCESS

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

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.

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.

UNKNOWN

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


class cvc5.ProofComponent(value)

The ProofComponent enum

FULL

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

Only valid immediately after an unsat response.

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.

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.

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.

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.


class cvc5.ProofFormat(value)

The ProofFormat enum

ALETHE

Output Alethe proof.

CPC

Output Cooperating Proof Calculus proof based on Eunoia signatures.

DEFAULT

Use the proof format mode set in the solver options.

DOT

Output DOT proof.

LFSC

Output LFSC proof.

NONE

Do not translate proof output.


class cvc5.FindSynthTarget(value)

The FindSynthTarget enum

ENUM

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

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.

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.

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.

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.