Modes

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

class cvc5.BlockModelsMode(*values)

The BlockModelsMode enum

LITERALS = 0

VALUES = 1

class cvc5.LearnedLitType(*values)

The LearnedLitType enum

CONSTANT_PROP = 4

INPUT = 2

INTERNAL = 5

PREPROCESS = 1

PREPROCESS_SOLVED = 0

SOLVABLE = 3

UNKNOWN = 6

class cvc5.OptionCategory(*values)

The OptionCategory enum

COMMON = 2

EXPERT = 1

REGULAR = 0

UNDOCUMENTED = 3

class cvc5.ProofComponent(*values)

The ProofComponent enum

FULL = 4

PREPROCESS = 1

RAW_PREPROCESS = 0

SAT = 2

THEORY_LEMMAS = 3

class cvc5.ProofFormat(*values)

The ProofFormat enum

ALETHE = 3

CPC = 4

DEFAULT = 5

DOT = 1

LFSC = 2

NONE = 0

class cvc5.FindSynthTarget(*values)

The FindSynthTarget enum

ENUM = 0

QUERY = 4

REWRITE = 1

REWRITE_INPUT = 3

REWRITE_UNSOUND = 2