From 2dba99d28c1911c07871162beaf3265206afafaa Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 28 Apr 2010 12:33:15 +0000 Subject: [PATCH] Bugfix. Refactoring of ToCNF broke some ifdef CRYPTOMINISAT2 code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@733 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/ToCNF.cpp | 9 +++++---- src/to-sat/ToSAT.cpp | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index b5ea9cb..7d67fe8 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -1163,8 +1163,8 @@ namespace BEEV //doRenamingPos(*it, defs); doRenamingNeg(*it, defs); xor_clause->insert(xor_clause->end(), - ((*(info[*it]->clausespos))[0])->begin(), - ((*(info[*it]->clausespos))[0])->end()); + ((*(info[*it]->clausespos)).asList()->front())->begin(), + ((*(info[*it]->clausespos)).asList()->front())->end()); if(renameAllSiblings) { assert(info[*it]->clausespos->size() ==1); @@ -1542,9 +1542,10 @@ namespace BEEV //XOR node doRenamingPos(*it, defs); //doRenamingPos(*it, defs); doRenamingNeg(*it, defs); + xor_clause->insert(xor_clause->end(), - ((*(info[*it]->clausespos))[0])->begin(), - ((*(info[*it]->clausespos))[0])->end()); + ((*(info[*it]->clausespos)).asList()->front())->begin(), + ((*(info[*it]->clausespos)).asList()->front())->end()); } doRenamingPosXor(varphi); //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index dc7952d..8c95135 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -338,7 +338,7 @@ namespace BEEV } #if defined CRYPTOMINISAT2 - if(!xorcl->empty()) + if(!xorcl->asList()->empty()) { sat = toSATandSolve(SatSolver, *xorcl, true); } -- 2.47.3