#
0c840916 |
|
29-Sep-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
Some technical improvements: * HOL-side - All is now tail recursive and most uses less RAM - Undocumented feature allows skipping CNF conversion (still WIP) - General refactoring preparatory to adding proof replay for ZChaff * Solver-side - Proof log now indexes root clauses, and writes sign info for pivots - Proof::compress has been implemented - Folded in miscellaneous upstream deltas PS: None of the above applies to defCNF stuff. Still a black box to me.
|
#
cde2941e |
|
19-Mar-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
HolSatLib refactoring and additions. * MiniSat-p v1.14 added as a "built-in" SAT-solver * A new function SAT_TAUT_PROVE uses MiniSat to prove propositional tautologies within HOL * HolSatLib refactored into satTools and dimacsTools * Local documentation removed; it was folded into the Description some time ago. * The HolSatLib interface remains the same, save for the addition of SAT_TAUT_PROVE. * Two minor additions to defCNF: a global ref for the variable name prefix used by DEF_CNF_VECTOR_CONV (defaulting to the current setting), and a global ref for the number of new vars introduced by definitional CNF.
|