diff options
author | Liana Hadarean <lianahady@gmail.com> | 2011-10-28 19:24:38 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2011-10-28 19:24:38 +0000 |
commit | b084a7efa9d65ec2f7475caa8486f8fd4cbafbd5 (patch) | |
tree | e118097c88787b7f2899bb8b2cbf865d058ef6bf /src/prop/minisat/simp | |
parent | 9547a48a7cdab8786c080779930de9c39655c52b (diff) |
merged the proofgen3 branch into trunk:
- can now output LFSC checkable resolution proofs
- added configuration option --enable-proof
- added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof.
Diffstat (limited to 'src/prop/minisat/simp')
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.cc | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 8c31dd377..6045fc881 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "mtl/Sort.h" #include "simp/SimpSolver.h" #include "utils/System.h" - +#include "proof/proof.h" using namespace Minisat; using namespace CVC4; @@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con , asymm_lits (0) , eliminated_vars (0) , elimorder (1) - , use_simplification (!enableIncremental) + , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially , occurs (ClauseDeleted(ca)) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) @@ -702,10 +702,11 @@ void SimpSolver::relocAll(ClauseAllocator& to) // for (int i = 0; i < subsumption_queue.size(); i++) ca.reloc(subsumption_queue[i], to); - + // TODO reloc now takes the proof form the core solver // Temporary clause: // ca.reloc(bwdsub_tmpunit, to); + // TODO reloc now takes the proof form the core solver } @@ -723,4 +724,5 @@ void SimpSolver::garbageCollect() printf("| Garbage collection: %12d bytes => %12d bytes |\n", ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); + // TODO: proof.finalizeUpdateId(); } |