A | |
| assumption [Plugin_intf] |
Asusmptions made by the core SAT solver.
|
| atom [Dot.Arg] |
The type of atomic formuals
|
| atom [Tseitin_intf.S] |
The type of atomic formulas.
|
| atom [Solver_intf.S] |
The type of atoms given by the module argument for formulas
|
| atom [Solver_types_intf.S] |
Atoms and variables wrap theory formulas.
|
| atom [Res_intf.S] | |
C | |
| clause [Solver_types_intf.S] |
The type of clauses.
|
| clause [Res_intf.S] | |
E | |
| elt [Solver_types_intf.S] | |
| eval_res [Plugin_intf] |
The type of evaluation results for a given formula.
|
F | |
| formula [Dedukti.Arg] | |
| formula [Solver_types_intf.S] | |
| formula [Plugin_intf.S] |
The type of formulas.
|
| formula [Theory_intf.S] |
The type of formulas.
|
L | |
| lemma [Dedukti.Arg] | |
| lemma [Dot.Arg] |
The type of theory-specifi proofs (also called lemmas).
|
| lemma [Res_intf.S] |
Abstract types for atoms, clauses and theory-specific lemmas
|
| level [Plugin_intf.S] |
The type for levels to allow backtracking.
|
| level [Theory_intf.S] |
The type for levels to allow backtracking.
|
| lit [Solver_types_intf.S] |
Wrapper type for literals, i.e.
|
N | |
| negated [Expr_intf] |
This type is used during the normalisation of formulas.
|
| negated [Formula_intf] |
This type is used during the normalisation of formulas.
|
P | |
| premise [Solver_types_intf.S] |
Premises for clauses.
|
| proof [Dedukti.Arg] | |
| proof [Solver_types_intf.S] |
The types of terms, formulas and proofs.
|
| proof [Res_intf.S] |
Lazy type for proof trees.
|
| proof [Expr_intf.S] |
An abstract type for proofs
|
| proof [Plugin_intf.S] |
A custom type for the proofs of lemmas produced by the theory.
|
| proof [Theory_intf.S] |
A custom type for the proofs of lemmas produced by the theory.
|
| proof [Formula_intf.S] |
An abstract type for proofs
|
| proof_node [Res_intf.S] |
A proof can be expanded into a proof node, which show the first step of the proof.
|
R | |
| reason [Solver_types_intf.S] |
Reasons of propagation/decision of atoms.
|
| reason [Plugin_intf] |
The type of reasons for propagations of a formula
f.
|
| res [Solver_intf.S] |
Result type for the solver
|
| res [Plugin_intf] |
Type returned by the theory.
|
| res [Theory_intf] |
Type returned by the theory.
|
S | |
| sat_state [Solver_intf] |
The type of values returned when the solver reaches a SAT state.
|
| slice [Plugin_intf] |
The type for a slice of assertions to assume/propagate in the theory.
|
| slice [Theory_intf] |
The type for a slice.
|
| step [Res_intf.S] |
The type of reasoning steps allowed in a proof.
|
T | |
| t [Backend_intf.S] |
The type of proofs.
|
| t [Tseitin_intf.S] |
The type of arbitrary boolean formulas.
|
| t [Tseitin_intf.Arg] |
Type of atomic formulas.
|
| t [Solver_types_intf.S] |
Decisions and propagations
|
| t [Expr_intf.S.Formula] |
The type of atomic formulas over terms.
|
| t [Expr_intf.S.Term] |
The type of terms
|
| t [Formula_intf.S] |
The type of atomic formulas.
|
| term [Solver_types_intf.S] | |
| term [Plugin_intf.S] |
The type of terms.
|
U | |
| unsat_state [Solver_intf] |
The type of values returned when the solver reaches an UNSAT state.
|
V | |
| var [Solver_types_intf.S] |