A | |
| assumption [Coq.Arg] | The types of hypotheses, lemmas, and assumptions |
| assumption [Dot.Arg] | The type of theory-specifi proofs (also called lemmas). |
| 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] | Abstract types for atoms, clauses and theory-specific lemmas |
E | |
| elt [Solver_types_intf.S] | Either a lit of a var |
| 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. |
H | |
| hyp [Coq.Arg] | |
| hyp [Dot.Arg] | |
L | |
| lemma [Dedukti.Arg] | |
| lemma [Coq.Arg] | |
| lemma [Dot.Arg] | |
| lemma [Res_intf.S] | |
| 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 |
| 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. |
| seen [Solver_types_intf.S] | |
| 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] |