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.

enumerator
LITERALS
¶

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 toplevel 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 toplevel 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 producelearnedliterals is not set.

enumerator
LEARNED_LIT_PREPROCESS_SOLVED
¶

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.

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

enum
BlockModelsMode
¶