From cd0fe0d27e74cf19c837fd75b08a7c2840a0e28d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 7 Mar 2010 14:31:11 +0000 Subject: [PATCH] Removing unused inputs to the ToSAT class. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@628 e59a4935-1847-0410-ae03-e826735625c1 --- src/absrefine_counterexample/CounterExample.cpp | 3 +-- src/c_interface/c_interface.cpp | 2 +- src/main/main.cpp | 2 +- src/to-sat/ToSAT.cpp | 6 +++--- src/to-sat/ToSAT.h | 14 ++++---------- 5 files changed, 10 insertions(+), 17 deletions(-) diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 80f92b3..35796be 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -993,8 +993,7 @@ namespace BEEV const ASTNode& original_input) { bool sat = tosat->CallSAT(SatSolver, - modified_input, - original_input); + modified_input); if (!sat) { //PrintOutput(true); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index caae185..363a9cb 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -158,7 +158,7 @@ VC vc_createValidityChecker(void) { BEEV::STPMgr * bm = new BEEV::STPMgr(); BEEV::Simplifier * simp = new BEEV::Simplifier(bm); BEEV::BVSolver* bvsolver = new BEEV::BVSolver(bm, simp); - BEEV::ToSAT * tosat = new BEEV::ToSAT(bm, simp); + BEEV::ToSAT * tosat = new BEEV::ToSAT(bm); BEEV::ArrayTransformer * arrayTransformer = new BEEV::ArrayTransformer(bm, simp); BEEV::AbsRefine_CounterExample * Ctr_Example = diff --git a/src/main/main.cpp b/src/main/main.cpp index 8158a5f..1122d0c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -56,7 +56,7 @@ int main(int argc, char ** argv) { Simplifier * simp = new Simplifier(bm); BVSolver* bvsolver = new BVSolver(bm, simp); ArrayTransformer * arrayTransformer = new ArrayTransformer(bm, simp); - ToSAT * tosat = new ToSAT(bm, simp); + ToSAT * tosat = new ToSAT(bm); AbsRefine_CounterExample * Ctr_Example = new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat); itimerval timeout; diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index d5146d2..794a833 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -256,15 +256,14 @@ namespace BEEV //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or //SOLVER_UNDECIDED bool ToSAT::CallSAT(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) + const ASTNode& input) { bm->GetRunTimes()->start(RunTimes::BitBlasting); BitBlasterNew BB(bm); BBNodeSet set; - ASTNode BBFormula = BB.BBForm(modified_input,set); + ASTNode BBFormula = BB.BBForm(input,set); assert(set.size() == 0); // doesn't yet work. bm->ASTNodeStats("after bitblasting: ", BBFormula); @@ -298,6 +297,7 @@ namespace BEEV } #endif + cm->DELETE(cl); cm->DELETE(xorcl); delete cm; diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index 8446129..dfc0667 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -51,9 +51,6 @@ namespace BEEV // Ptr to STPManager STPMgr * bm; - // Ptr to Simplifier - Simplifier * simp; - #if 0 // Memo table to check the functioning of bitblaster and CNF // converter @@ -105,9 +102,8 @@ namespace BEEV ****************************************************************/ // Constructor - ToSAT(STPMgr * bm, Simplifier * s) : - bm(bm), - simp(s) + ToSAT(STPMgr * bm) : + bm(bm) #if 0 ,CheckBBandCNFMemo() #endif @@ -119,8 +115,7 @@ namespace BEEV // Bitblasts, CNF conversion and calls toSATandSolve() bool CallSAT(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input); + const ASTNode& input); //print the STP solver output void PrintOutput(SOLVER_RETURN_TYPE ret); @@ -138,12 +133,11 @@ namespace BEEV ~ToSAT() { - _ASTNode_to_SATVar_Map.clear(); + ClearAllTables(); #if 0 RepLitMap.clear(); CheckBBandCNFMemo.clear(); #endif - _SATVar_to_AST_Vector.clear(); } }; //end of class ToSAT }; //end of namespace -- 2.47.3