I | |
| Insuficient_hyps [Res_intf.S] |
Raised when a complete resolution derivation cannot be found using the current hypotheses.
|
U | |
| UndecidedLit [Internal.Make] | |
| UndecidedLit [Solver_intf.S] |
Exception raised by the evaluating functions when a literal
has not yet been assigned a value.
|
| Unsat [Internal.Make] |