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 