Modes ¶

namespace modes ¶

Enums

enum BlockModelsMode ¶

Mode for blocking models.

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

Values:

enumerator LITERALS ¶

Block models based on the SAT skeleton.

enumerator VALUES ¶

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

enum LearnedLitType ¶

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 LEARNED_LIT_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 LEARNED_LIT_PREPROCESS ¶

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

enumerator LEARNED_LIT_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 LEARNED_LIT_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 LEARNED_LIT_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 LEARNED_LIT_INTERNAL ¶

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

enumerator LEARNED_LIT_UNKNOWN ¶

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

enum ProofComponent ¶

Components to include in a proof.

Values:

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

Functions

std :: ostream & operator << ( std :: ostream & out , LearnedLitType ltype ) ¶

Writes a learned literal type to a stream.

std :: ostream & operator << ( std :: ostream & out , ProofComponent pc ) ¶

Writes a proof component identifier to a stream.