From d51c1fa4a8136ad8c39bee251bdbd4857843772d Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Mon, 7 Dec 2009 01:32:20 +0000 Subject: [PATCH] minor edit git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@470 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/UsefulDefs.h | 2 +- src/to-sat/CallSAT.cpp | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 27e1399..e23c2ff 100644 --- a/src/AST/UsefulDefs.h +++ b/src/AST/UsefulDefs.h @@ -46,7 +46,7 @@ #define HASHMULTISET hash_multiset #define INITIAL_TABLE_SIZE 100 #define CLAUSAL_ABSTRACTION_CUTOFF 0.5 -#define CLAUSAL_BUCKET_LIMIT 3 +#define CLAUSAL_BUCKET_LIMIT 4 using namespace std; namespace BEEV { diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 984b8f4..a0b4be6 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -54,11 +54,11 @@ namespace BEEV for(int count=1;it!=itend;it++, count++) { ClauseList *cl = (*it).second; -// if(CLAUSAL_BUCKET_LIMIT == count) -// { -// sat = toSATandSolve(SatSolver,*cl, false, true); -// } -// else + // if(CLAUSAL_BUCKET_LIMIT == count) + // { + // sat = toSATandSolve(SatSolver,*cl, false, true); + // } + // else { sat = toSATandSolve(SatSolver,*cl); } -- 2.47.3