C | |
| CLAUSE_SET [ProofState_intf.S] | |
P | |
| PARAMETERS [Ctx] | |
| PAYLOAD [Bool_lit] | |
S | |
| S [Fool] | |
| S [Heuristics] | |
| S [Arith_rat] | |
| S [Arith_int] | |
| S [EnumTypes] | |
| S [Superposition_intf] | |
| S [Superposition] | |
| S [Induction_intf] | |
| S [Induction] | |
| S [Avatar_intf] | |
| S [Avatar] | |
| S [Sat_solver_intf] | |
| S [Bool_lit_intf] | |
| S [Bool_lit] | |
| S [ClauseQueue_intf] |
A priority queue of clauses, purely functional
|
| S [ProofState_intf] |
Set of active clauses
|
| S [Env_intf] | |
| S [Clause_intf] | |
| S [Ctx_intf] | |
| S [Env] |
Signature
|
| S [AC_intf] | |
| S [AC] | |
| S [Saturate] | |
| S [ProofState] | |
| S [Ctx] |
Context for a Proof
|
| S [Clause] | |
| S [ClauseQueue] |