From e1cf1d50efd537a6d62c7bb4adb1c65a12000e7f Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Wed, 28 Oct 2009 19:51:25 +0000 Subject: [PATCH] did emacs indentation of all files. fixed Makefiles, and ToSAT.cpp to allow for compiling and linking with cyrptominisat git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@354 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile | 17 +- scripts/Makefile.common | 15 +- scripts/Makefile.in | 17 +- src/AST/ArrayTransformer.h | 6 +- src/AST/RunTimes.cpp | 10 +- src/STPManager/STP.h | 2 +- src/STPManager/STPManager.h | 8 +- .../CounterExample.cpp | 18 +- src/main/main.cpp | 4 +- src/sat/Makefile | 6 +- src/sat/core/Solver.h | 10 +- src/sat/sat.h | 12 +- src/to-sat/BitBlast.cpp | 176 +++++++++--------- src/to-sat/BitBlast.h | 2 +- src/to-sat/ToCNF.cpp | 46 ++--- src/to-sat/ToSAT.cpp | 117 ++++++------ 16 files changed, 245 insertions(+), 221 deletions(-) diff --git a/Makefile b/Makefile index 2bce0e0..ebf081e 100644 --- a/Makefile +++ b/Makefile @@ -27,10 +27,19 @@ else endif $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \ - $(SRC)/to-sat/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o \ - $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o \ - $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o + $(AR) rc libstp.a $(SRC)/AST/*.o \ + $(SRC)/STPManager/*.o \ + $(SRC)/printer/*.o \ + $(SRC)/absrefine_counterexample/*.o \ + $(SRC)/to-sat/*.o \ + $(SRC)/sat/*.o \ + $(SRC)/simplifier/*.o \ + $(SRC)/extlib-constbv/*.o \ + $(SRC)/c_interface/*.o \ + $(SRC)/parser/let-funcs.o \ + $(SRC)/parser/parseCVC.o \ + $(SRC)/parser/lexCVC.o \ + $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ diff --git a/scripts/Makefile.common b/scripts/Makefile.common index bd90a59..0e3a07f 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -8,13 +8,14 @@ # * LICENSE: Please view LICENSE file in the home dir of this Program # ********************************************************************/ -#OPTIMIZE = -g -pg # Debugging and gprof-style profiling -OPTIMIZE = -g # Debugging -OPTIMIZE = -O3 -DNDEBUG # Maximum optimization -#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE -CFLAGS_BASE = $(OPTIMIZE) -#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT -#CFLAGS_M32 = -m32 +#OPTIMIZE = -g -pg # Debugging and gprof-style profiling +OPTIMIZE = -g # Debugging +OPTIMIZE = -O3 -DNDEBUG # Maximum optimization +#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE +CFLAGS_BASE = $(OPTIMIZE) +#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT +#CRYPTOMINISAT = true +#CFLAGS_M32 = -m32 SHELL=/bin/bash diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 2bce0e0..ebf081e 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -27,10 +27,19 @@ else endif $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main - $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \ - $(SRC)/to-sat/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o \ - $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o \ - $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o + $(AR) rc libstp.a $(SRC)/AST/*.o \ + $(SRC)/STPManager/*.o \ + $(SRC)/printer/*.o \ + $(SRC)/absrefine_counterexample/*.o \ + $(SRC)/to-sat/*.o \ + $(SRC)/sat/*.o \ + $(SRC)/simplifier/*.o \ + $(SRC)/extlib-constbv/*.o \ + $(SRC)/c_interface/*.o \ + $(SRC)/parser/let-funcs.o \ + $(SRC)/parser/parseCVC.o \ + $(SRC)/parser/lexCVC.o \ + $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @mv libstp.a lib/ diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index dc2773d..779d477 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -143,9 +143,9 @@ namespace BEEV ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin(); ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end(); for(;it!=itend;it++) - { - ((*it).second).clear(); - } + { + ((*it).second).clear(); + } Arrayname_ReadindicesMap->clear(); delete Arrayname_ReadindicesMap; } diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp index 5bc0e2b..24b42a4 100644 --- a/src/AST/RunTimes.cpp +++ b/src/AST/RunTimes.cpp @@ -33,11 +33,11 @@ long RunTimes::getCurrentTime() void RunTimes::print() { if (0 != category_stack.size()) - { - std::cerr << "size:" << category_stack.size() << std::endl; - std::cerr << "top:" << CategoryNames[category_stack.top().first] << std::endl; - BEEV::FatalError("category stack is not yet empty!!"); - } + { + std::cerr << "size:" << category_stack.size() << std::endl; + std::cerr << "top:" << CategoryNames[category_stack.top().first] << std::endl; + BEEV::FatalError("category stack is not yet empty!!"); + } std::ostringstream result; result << "statistics\n"; diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index 9cd6b16..a75f6d8 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -67,7 +67,7 @@ namespace BEEV delete arrayTransformer; delete tosat; delete simp; -// delete bm; + // delete bm; } /**************************************************************** diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 9985e02..a637787 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -383,10 +383,10 @@ namespace BEEV vector::iterator it = _asserts.begin(); vector::iterator itend = _asserts.end(); for(;it!=itend;it++) - { - ASTVec * j = (*it); - j->clear(); - } + { + ASTVec * j = (*it); + j->clear(); + } _asserts.clear(); _interior_unique_table.clear(); diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 83e9b6e..da3aaee 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -469,33 +469,33 @@ namespace BEEV } ASTNode newRead = term; - const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false); + const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false); //iteratively expand read-over-write, and evaluate against the //model at every iteration - ASTNode write = newRead[0]; + ASTNode write = newRead[0]; do { ASTNode writeIndex = TermToConstTermUsingModel(write[1], false); - if (writeIndex == readIndex) + if (writeIndex == readIndex) { //found the write-value. return it - output = TermToConstTermUsingModel(write[2], false); + output = TermToConstTermUsingModel(write[2], false); CounterExampleMap[term] = output; return output; } - write = write[0]; - } while (WRITE == write.GetKind()); + write = write[0]; + } while (WRITE == write.GetKind()); - const unsigned int width = term.GetValueWidth(); - newRead = bm->CreateTerm(READ, width, write, readIndex); + const unsigned int width = term.GetValueWidth(); + newRead = bm->CreateTerm(READ, width, write, readIndex); output = TermToConstTermUsingModel(newRead, arrayread_flag); //memoize CounterExampleMap[term] = output; return output; - } //Expand_ReadOverWrite_UsingModel() + } //Expand_ReadOverWrite_UsingModel() /* FUNCTION: accepts a non-constant formula, and checks if the * formula is ASTTrue or ASTFalse w.r.t to a model diff --git a/src/main/main.cpp b/src/main/main.cpp index b585b3e..370ebd1 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,8 +22,8 @@ extern int cvcparse(void*); // callback for SIGALRM. void handle_time_out(int parameter){ - printf("Timed Out.\n"); - exit(0); + printf("Timed Out.\n"); + exit(0); } diff --git a/src/sat/Makefile b/src/sat/Makefile index 2af86b2..356331f 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -1,23 +1,27 @@ .PHONY: core core: $(MAKE) -C core lib all + mv Solver.or Solver.o .PHONY: simp simp: $(MAKE) -C simp lib all + mv SimpSolver.or SimpSolver.o .PHONY: unsound unsound: $(MAKE) -C unsound lib all + mv UnsoundSimpSolver.or UnsoundSimpSolver.o .PHONY: cryptominisat cryptominisat: $(MAKE) -C cryptominisat cp cryptominisat/libminisat.a . + cp cryptominisat/CMakeFiles/minisat.dir/Solver/*.o . .PHONY: clean clean: - rm -rf *.or *~ libminisat.a + rm -rf *.o *~ libminisat.a $(MAKE) -C core clean $(MAKE) -C simp clean $(MAKE) -C unsound clean diff --git a/src/sat/core/Solver.h b/src/sat/core/Solver.h index db67797..3aa419e 100644 --- a/src/sat/core/Solver.h +++ b/src/sat/core/Solver.h @@ -30,13 +30,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "SolverTypes.h" #ifdef _MSC_VER -#include - + #include #else - -#include -#include -#include + #include + #include + #include #endif namespace MINISAT { diff --git a/src/sat/sat.h b/src/sat/sat.h index 88f7dfb..f9a6bfe 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -2,13 +2,13 @@ #define SAT_H_ #ifdef CRYPTOMINISAT - #include "cryptominisat/Solver/Solver.h" - #include "cryptominisat/Solver/SolverTypes.h" +#include "cryptominisat/Solver/Solver.h" +#include "cryptominisat/Solver/SolverTypes.h" #else - #include "core/Solver.h" - #include "core/SolverTypes.h" - //#include "simp/SimpSolver.h" - //#include "unsound/UnsoundSimpSolver.h" +#include "core/Solver.h" +#include "core/SolverTypes.h" +//#include "simp/SimpSolver.h" +//#include "unsound/UnsoundSimpSolver.h" #endif #endif diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index ff70261..d6ebc21 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -648,18 +648,18 @@ namespace BEEV // FIXME: Don't bother computing i+1 carry, which is discarded. for (int i = 0; i < n; i++) { - ASTNode nextcin; - if(i != n-1) - { - //Compute this only for i=0 to n-2 - nextcin = Majority(sum[i], y[i], cin); - } + ASTNode nextcin; + if(i != n-1) + { + //Compute this only for i=0 to n-2 + nextcin = Majority(sum[i], y[i], cin); + } sum[i] = Sum(sum[i], y[i], cin); - if(i != n-1) - { - //Compute this only for i=0 to n-2 - cin = nextcin; - } + if(i != n-1) + { + //Compute this only for i=0 to n-2 + cin = nextcin; + } } // cout << "----------------" << endl << "Result: " << endl; @@ -731,11 +731,11 @@ namespace BEEV // worth doing explicitly (e.g., a = b, a = ~b, etc.) else { - // return _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(AND, a, b), - // _bm->CreateSimpForm(AND, b, c), - // _bm->CreateSimpForm(AND, a, c)); - return _bm->CreateSimpForm(AND, + // return _bm->CreateSimpForm(OR, + // _bm->CreateSimpForm(AND, a, b), + // _bm->CreateSimpForm(AND, b, c), + // _bm->CreateSimpForm(AND, a, c)); + return _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, a, b), _bm->CreateSimpForm(OR, b, c), _bm->CreateSimpForm(OR, a, c)); @@ -744,28 +744,28 @@ namespace BEEV } ASTNode BitBlaster::Sum(const ASTNode& xi, - const ASTNode& yi, - const ASTNode& cin) + const ASTNode& yi, + const ASTNode& cin) { // For some unexplained reason, XORs are faster than converting // them to cluases at this point ASTNode S0 = _bm->CreateSimpForm(XOR, - _bm->CreateSimpForm(XOR, xi, yi), - cin); + _bm->CreateSimpForm(XOR, xi, yi), + cin); return S0; // ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin); // ASTNode S2 = _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(NOT,xi), - // _bm->CreateSimpForm(NOT,yi), - // cin); + // _bm->CreateSimpForm(NOT,xi), + // _bm->CreateSimpForm(NOT,yi), + // cin); // ASTNode S3 = _bm->CreateSimpForm(OR, - // _bm->CreateSimpForm(NOT,xi), - // yi, - // _bm->CreateSimpForm(NOT,cin)); + // _bm->CreateSimpForm(NOT,xi), + // yi, + // _bm->CreateSimpForm(NOT,cin)); // ASTNode S4 = _bm->CreateSimpForm(OR, - // xi, - // _bm->CreateSimpForm(NOT,yi), - // _bm->CreateSimpForm(NOT,cin)); + // xi, + // _bm->CreateSimpForm(NOT,yi), + // _bm->CreateSimpForm(NOT,cin)); // ASTVec S; // S.push_back(S1); // S.push_back(S2); @@ -926,8 +926,8 @@ namespace BEEV // complementing the result bit. ASTNode BitBlaster::BBBVLE(const ASTVec& left, const ASTVec& right, - bool is_signed, - bool is_bvlt) + bool is_signed, + bool is_bvlt) { ASTVec::const_reverse_iterator lit = left.rbegin(); ASTVec::const_reverse_iterator litend = left.rend(); @@ -945,72 +945,72 @@ namespace BEEV for(lit++, rit++; lit < litend; lit++, rit++) { this_compare_bit = - _bm->CreateSimpForm(AND, _bm->CreateSimpNot(*lit), *rit); - - ASTNode thisbit_output = - _bm->CreateSimpForm(AND, this_compare_bit, prev_eq_bit); - bit_comparisons.push_back(thisbit_output); - - // (neg(lit) OR rit)(lit OR neg(rit)) - ASTNode this_eq_bit = - _bm->CreateSimpForm(AND, - _bm->CreateSimpForm(IFF,*lit,*rit), - prev_eq_bit); - prev_eq_bit = this_eq_bit; + _bm->CreateSimpForm(AND, _bm->CreateSimpNot(*lit), *rit); + + ASTNode thisbit_output = + _bm->CreateSimpForm(AND, this_compare_bit, prev_eq_bit); + bit_comparisons.push_back(thisbit_output); + + // (neg(lit) OR rit)(lit OR neg(rit)) + ASTNode this_eq_bit = + _bm->CreateSimpForm(AND, + _bm->CreateSimpForm(IFF,*lit,*rit), + prev_eq_bit); + prev_eq_bit = this_eq_bit; } if(!is_bvlt) { - bit_comparisons.push_back(prev_eq_bit); + bit_comparisons.push_back(prev_eq_bit); } ASTNode output = _bm->CreateSimpForm(OR, bit_comparisons); return output; -// // "thisbit" represents BVLE of the suffixes of the BVs -// // from that position . if R < L, return TRUE, else if L < R -// // return FALSE, else return BVLE of lower-order bits. MSB is -// // treated separately, because signed comparison is done by -// // complementing the MSB of each BV, then doing an unsigned -// // comparison. -// ASTVec::const_iterator lit = left.rbegin(); -// ASTVec::const_iterator litend = left.rend(); -// ASTVec::const_iterator rit = right.rbegin(); -// ASTNode prevbit = ASTTrue; -// for (; lit < litend - 1; lit++, rit++) -// { -// ASTNode neglit = _bm->CreateSimpNot(*lit); -// ASTNode thisbit = -// _bm->CreateSimpForm(OR, -// _bm->CreateSimpForm(AND, neglit, *rit), -// _bm->CreateSimpForm(AND, -// _bm->CreateSimpForm(OR, -// neglit, -// *rit), -// prevbit)); -// prevbit = thisbit; -// } - -// // Handle MSB -- negate MSBs if signed comparison -// // FIXME: make into refs after it's debugged. -// ASTNode lmsb = *lit; -// ASTNode rmsb = *rit; -// if (is_signed) -// { -// lmsb = _bm->CreateSimpNot(*lit); -// rmsb = _bm->CreateSimpNot(*rit); -// } - -// ASTNode neglmsb = _bm->CreateSimpNot(lmsb); -// ASTNode msb = -// // TRUE if l < r -// _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), -// _bm->CreateSimpForm(AND, -// _bm->CreateSimpForm(OR, -// neglmsb, -// rmsb), -// prevbit)); // else prevbit -// return msb; + // // "thisbit" represents BVLE of the suffixes of the BVs + // // from that position . if R < L, return TRUE, else if L < R + // // return FALSE, else return BVLE of lower-order bits. MSB is + // // treated separately, because signed comparison is done by + // // complementing the MSB of each BV, then doing an unsigned + // // comparison. + // ASTVec::const_iterator lit = left.rbegin(); + // ASTVec::const_iterator litend = left.rend(); + // ASTVec::const_iterator rit = right.rbegin(); + // ASTNode prevbit = ASTTrue; + // for (; lit < litend - 1; lit++, rit++) + // { + // ASTNode neglit = _bm->CreateSimpNot(*lit); + // ASTNode thisbit = + // _bm->CreateSimpForm(OR, + // _bm->CreateSimpForm(AND, neglit, *rit), + // _bm->CreateSimpForm(AND, + // _bm->CreateSimpForm(OR, + // neglit, + // *rit), + // prevbit)); + // prevbit = thisbit; + // } + + // // Handle MSB -- negate MSBs if signed comparison + // // FIXME: make into refs after it's debugged. + // ASTNode lmsb = *lit; + // ASTNode rmsb = *rit; + // if (is_signed) + // { + // lmsb = _bm->CreateSimpNot(*lit); + // rmsb = _bm->CreateSimpNot(*rit); + // } + + // ASTNode neglmsb = _bm->CreateSimpNot(lmsb); + // ASTNode msb = + // // TRUE if l < r + // _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), + // _bm->CreateSimpForm(AND, + // _bm->CreateSimpForm(OR, + // neglmsb, + // rmsb), + // prevbit)); // else prevbit + // return msb; } // Left shift within fixed field inserting zeros at LSB. diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h index 8e818ca..671af69 100644 --- a/src/to-sat/BitBlast.h +++ b/src/to-sat/BitBlast.h @@ -86,7 +86,7 @@ namespace BEEV // Internal bit blasting routines. ASTNode BBBVLE(const ASTVec& x, - const ASTVec& y, bool is_signed, bool is_bvlt = false); + const ASTVec& y, bool is_signed, bool is_bvlt = false); // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. ASTNode BBcompare(const ASTNode& form); diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 2e5c7c1..907e8e0 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -1035,29 +1035,29 @@ namespace BEEV // (pos) AND ~> UNION //**************************************** - ASTVec::const_iterator it = varphi.GetChildren().begin(); - convertFormulaToCNF(*it, defs); - ClauseList* psi = COPY(*(info[*it]->clausespos)); - - for (it++; it != varphi.GetChildren().end(); it++) { - convertFormulaToCNF(*it, defs); - CNFInfo* x = info[*it]; - - if (sharesPos(*x) == 1) { - psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end()); - delete (x->clausespos); - x->clausespos = NULL; - if (x->clausesneg == NULL) { - delete x; - info.erase(*it); - } - } else { - INPLACE_UNION(psi, *(x->clausespos)); - reduceMemoryFootprintPos(*it); - } - } - info[varphi]->clausespos = psi; -} //End of convertFormulaToCNFPosAND() + ASTVec::const_iterator it = varphi.GetChildren().begin(); + convertFormulaToCNF(*it, defs); + ClauseList* psi = COPY(*(info[*it]->clausespos)); + + for (it++; it != varphi.GetChildren().end(); it++) { + convertFormulaToCNF(*it, defs); + CNFInfo* x = info[*it]; + + if (sharesPos(*x) == 1) { + psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end()); + delete (x->clausespos); + x->clausespos = NULL; + if (x->clausesneg == NULL) { + delete x; + info.erase(*it); + } + } else { + INPLACE_UNION(psi, *(x->clausespos)); + reduceMemoryFootprintPos(*it); + } + } + info[varphi]->clausespos = psi; + } //End of convertFormulaToCNFPosAND() void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs) diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 82bdd5c..0449cce 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -52,7 +52,7 @@ namespace BEEV int input_clauselist_size = cll.size(); if (cll.size() == 0) { - FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); + FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); } #ifdef CRYPTOMINISAT @@ -66,13 +66,13 @@ namespace BEEV MINISAT::vec satSolverClause; satSolverClause.capacity((*i)->size()); vector::const_iterator j = (*i)->begin(); - vector::const_iterator jend = (*i)->end(); - //ASTVec clauseVec; + vector::const_iterator jend = (*i)->end(); + //ASTVec clauseVec; //j is a disjunct in the ASTclause (*i) for (; j != jend; j++) - { + { ASTNode node = **j; - //clauseVec.push_back(node); + //clauseVec.push_back(node); bool negate = (NOT == node.GetKind()) ? true : false; ASTNode n = negate ? node[0] : node; MINISAT::Var v = LookupOrCreateSATVar(newS, n); @@ -81,42 +81,45 @@ namespace BEEV } // ASTNode theClause = bm->CreateNode(OR, clauseVec); - // if(flag - // && ASTTrue == CheckBBandCNF(newS, theClause)) - // { - // continue; - // } - - newS.addClause(satSolverClause); - float percentage=0.6; - if(count++ >= input_clauselist_size*percentage) - { - //Arbitrary adding only 60% of the clauses in the hopes of - //terminating early - // cout << "Percentage clauses added: " - // << percentage << endl; - bm->GetRunTimes()->stop(RunTimes::SendingToSAT); - bm->GetRunTimes()->start(RunTimes::Solving); - newS.solve(); - bm->GetRunTimes()->stop(RunTimes::Solving); - if(!newS.okay()) - { - return false; - } - count = 0; - flag = 1; - bm->GetRunTimes()->start(RunTimes::SendingToSAT); - } + // if(flag + // && ASTTrue == CheckBBandCNF(newS, theClause)) + // { + // continue; + // } +#ifdef CRYPTOMINISAT + newS.addClause(satSolverClause,0,"z"); +#else + newS.addClause(satSolverClause); +#endif + float percentage=0.6; + if(count++ >= input_clauselist_size*percentage) + { + //Arbitrary adding only 60% of the clauses in the hopes of + //terminating early + // cout << "Percentage clauses added: " + // << percentage << endl; + bm->GetRunTimes()->stop(RunTimes::SendingToSAT); + bm->GetRunTimes()->start(RunTimes::Solving); + newS.solve(); + bm->GetRunTimes()->stop(RunTimes::Solving); + if(!newS.okay()) + { + return false; + } + count = 0; + flag = 1; + bm->GetRunTimes()->start(RunTimes::SendingToSAT); + } if (newS.okay()) { - continue; - } + continue; + } else { bm->PrintStats(newS); bm->GetRunTimes()->stop(RunTimes::SendingToSAT); return false; - } + } } // End of For-loop adding the clauses bm->GetRunTimes()->stop(RunTimes::SendingToSAT); @@ -167,9 +170,9 @@ namespace BEEV ASTNode ToSAT::CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form) { // cout << "++++++++++++++++" - // << endl - // << "CheckBBandCNF_int form = " - // << form << endl; + // << endl + // << "CheckBBandCNF_int form = " + // << form << endl; ASTNodeMap::iterator memoit = CheckBBandCNFMemo.find(form); if (memoit != CheckBBandCNFMemo.end()) @@ -194,13 +197,13 @@ namespace BEEV { result = SymbolTruthValue(newS, form); - // cout << "================" - // << endl - // << "Checking BB formula:" - // << form << endl; - // cout << "----------------" - // << endl - // << "Result:" << result << endl; + // cout << "================" + // << endl + // << "Checking BB formula:" + // << form << endl; + // cout << "----------------" + // << endl + // << "Result:" << result << endl; break; } default: @@ -215,13 +218,13 @@ namespace BEEV } result = bm->CreateSimpForm(k, eval_children); - // cout << "================" - // << endl - // << "Checking BB formula:" << form << endl; - // cout << "----------------" - // << endl - // << "Result:" << result << endl; - + // cout << "================" + // << endl + // << "Checking BB formula:" << form << endl; + // cout << "----------------" + // << endl + // << "Result:" << result << endl; + ASTNode replit_eval; // Compare with replit, if there is one. ASTNodeMap::iterator replit_it = RepLitMap.find(form); @@ -240,12 +243,12 @@ namespace BEEV bm->CreateSimpNot(SymbolTruthValue(newS, replit[0])); } - // cout << "----------------" - // << endl - // << "Rep lit: " << replit << endl; - // cout << "----------------" - // << endl - // << "Rep lit value: " << replit_eval << endl; + // cout << "----------------" + // << endl + // << "Rep lit: " << replit << endl; + // cout << "----------------" + // << endl + // << "Rep lit value: " << replit_eval << endl; if (result != replit_eval) { -- 2.47.3