From: trevor_hansen Date: Tue, 24 Jan 2012 01:25:17 +0000 (+0000) Subject: Clean up. I think this is just a refactor, but aren't sure. The c_interface set remov... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0981f5050753a4696d9a0e0d1127ec0eca22b654;p=francis%2Fstp.git Clean up. I think this is just a refactor, but aren't sure. The c_interface set removewrites to true sometimes. It was the only place in the code that set it... git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1519 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 68f13e5..47d29ec 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -268,8 +268,8 @@ namespace BEEV { //DAG is minimized as much as possibly, and ideally should //garuntee that all liketerms in BVPLUSes have been combined. bm->SimplifyWrites_InPlace_Flag = false; - bm->Begin_RemoveWrites = false; - bm->start_abstracting = false; + //bm->Begin_RemoveWrites = false; + //bm->start_abstracting = false; bm->TermsAlreadySeenMap_Clear(); do { @@ -419,9 +419,9 @@ namespace BEEV { bm->TermsAlreadySeenMap_Clear(); - bm->start_abstracting = false; + //bm->start_abstracting = false; bm->SimplifyWrites_InPlace_Flag = false; - bm->Begin_RemoveWrites = false; + //bm->Begin_RemoveWrites = false; long final_difficulty_score = difficulty.score(simplified_solved_InputToSAT); if (bm->UserFlags.stats_flag) diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index e47541a..db071c2 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -637,14 +637,14 @@ namespace BEEV { if (READ == term.GetKind() && WRITE == term[0].GetKind() - && !GetRemoveWritesFlag()) + /*&& !GetRemoveWritesFlag()*/) { return false; } if (READ == term.GetKind() && WRITE == term[0].GetKind() - && GetRemoveWritesFlag()) + /*&& GetRemoveWritesFlag()*/) { return true; } @@ -680,7 +680,7 @@ namespace BEEV return false; }//End of VarSeenInTerm - + ASTNode STPMgr::NewParameterized_BooleanVar(const ASTNode& var, const ASTNode& constant) { @@ -697,6 +697,7 @@ namespace BEEV return CurrentSymbol; } // End of NewParameterized_BooleanVar() + //If ASTNode remain with references (somewhere), this will segfault. STPMgr::~STPMgr() { @@ -712,7 +713,7 @@ namespace BEEV ASTTrue = ASTNode(0); ASTUndefined = ASTNode(0); _current_query = ASTNode(0); - dummy_node = ASTNode(0); + //dummy_node = ASTNode(0); zeroes.clear(); ones.clear(); diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 8542ad0..03576ce 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -54,11 +54,13 @@ namespace BEEV ASTBVConst::ASTBVConstHasher, ASTBVConst::ASTBVConstEqual> ASTBVConstSet; +#if 0 typedef HASHMAP< ASTNode, ASTNodeSet, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeToSetMap; +#endif // Unique node tables that enables common subexpression sharing ASTInteriorSet _interior_unique_table; @@ -72,8 +74,8 @@ namespace BEEV // Global for assigning new node numbers. int _max_node_num; - ASTNode dummy_node; - + uint8_t last_iteration; + public: HashingNodeFactory* hashingNodeFactory; NodeFactory *defaultNodeFactory; @@ -81,8 +83,6 @@ namespace BEEV //frequently used nodes ASTNode ASTFalse, ASTTrue, ASTUndefined; - uint8_t last_iteration; - // No nodes should already have the iteration number that is returned from here. // This never returns zero. uint8_t getNextIteration() @@ -118,7 +118,6 @@ namespace BEEV // logical context is represented by a ptr to a vector of // assertions in that logical context. Logical contexts are // created by PUSH/POP - //std::vector _asserts; std::vector _asserts; // Memo table that tracks terms already seen @@ -194,8 +193,8 @@ namespace BEEV // Flags indicates that counterexample will now be checked by the // counterexample checker, and hence simplifyterm must switch off // certain optimizations. In particular, array write optimizations - bool start_abstracting; - bool Begin_RemoveWrites; + //bool start_abstracting; + //bool Begin_RemoveWrites; bool SimplifyWrites_InPlace_Flag; //count is used in the creation of new variables @@ -220,12 +219,12 @@ namespace BEEV { _max_node_num = 0; - Begin_RemoveWrites = false; + //Begin_RemoveWrites = false; ValidFlag = false; bvdiv_exception_occured = false; counterexample_checking_during_refinement = false; - start_abstracting = false; - Begin_RemoveWrites = false; + //start_abstracting = false; + //Begin_RemoveWrites = false; SimplifyWrites_InPlace_Flag = false; // Need to initiate the node factories before any nodes are created. @@ -245,6 +244,7 @@ namespace BEEV return runTimes; } +#if 0 void SetRemoveWritesFlag(bool in) { Begin_RemoveWrites = in; @@ -254,6 +254,7 @@ namespace BEEV { return Begin_RemoveWrites; } +#endif int NewNodeNum() { diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 165c8d9..0d282d8 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -208,14 +208,14 @@ static void vc_printAssertsToStream(VC vc, ostream &os, int simplify_print) { BEEV::ASTVec v = b->GetAsserts(); BEEV::Simplifier * simp = new BEEV::Simplifier(b); for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { - b->Begin_RemoveWrites = true; + //b->Begin_RemoveWrites = true; BEEV::ASTNode q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(*i,false) : *i; q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(q,false) : q; - b->Begin_RemoveWrites = false; + //b->Begin_RemoveWrites = false; os << "ASSERT( "; q.PL_Print(os); os << ");" << endl; @@ -243,12 +243,12 @@ void vc_printQueryStateToBuffer(VC vc, Expr e, vc_printAssertsToStream(vc, os, simplify_print); os << "%----------------------------------------------------" << endl; os << "QUERY( "; - b->Begin_RemoveWrites = true; + //b->Begin_RemoveWrites = true; BEEV::ASTNode q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(*((nodestar)e),false) : *(nodestar)e; - b->Begin_RemoveWrites = false; + //b->Begin_RemoveWrites = false; q.PL_Print(os); os << " );" << endl; @@ -1417,21 +1417,21 @@ Expr vc_simplify(VC vc, Expr e) { { nodestar round1 = new node(simp->SimplifyFormula_TopLevel(*a,false)); - b->Begin_RemoveWrites = true; + //b->Begin_RemoveWrites = true; nodestar output = new node(simp->SimplifyFormula_TopLevel(*round1,false)); //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = false; + //b->Begin_RemoveWrites = false; delete round1; return output; } else { nodestar round1 = new node(simp->SimplifyTerm(*a)); - b->Begin_RemoveWrites = true; + //b->Begin_RemoveWrites = true; nodestar output = new node(simp->SimplifyTerm(*round1)); //if(cinterface_exprdelete_on) created_exprs.push_back(output); - b->Begin_RemoveWrites = false; + //b->Begin_RemoveWrites = false; delete round1; return output; } diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h index 3b2f3af..5b7e4a9 100644 --- a/src/cpp_interface/cpp_interface.h +++ b/src/cpp_interface/cpp_interface.h @@ -21,6 +21,34 @@ namespace BEEV //boost::object_pool node_pool; bool alreadyWarned; bool print_success; + + // Used to cache prior queries. + struct Entry + { + explicit + Entry(SOLVER_RETURN_TYPE result_) + { + result = result_; + } + + SOLVER_RETURN_TYPE result; + ASTNode node; + + void + print() + { + if (result == SOLVER_UNSATISFIABLE) + cerr << "u"; + else if (result == SOLVER_SATISFIABLE) + cerr << "s"; + else if (result == SOLVER_UNDECIDED) + cerr << "?"; + } + }; + vector cache; + vector > symbols; + + public: LETMgr letMgr; NodeFactory* nf; @@ -35,6 +63,16 @@ namespace BEEV print_success = false; } + void + startup() + { + CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); + if(0 != c) { + cout << CONSTANTBV::BitVector_Error(c) << endl; + FatalError("Bad startup"); + } + } + const ASTVec GetAsserts(void) { @@ -176,31 +214,6 @@ namespace BEEV //node_pool.destroy(n); } - struct Entry - { - explicit - Entry(SOLVER_RETURN_TYPE result_) - { - result = result_; - } - - SOLVER_RETURN_TYPE result; - ASTNode node; - - void - print() - { - if (result == SOLVER_UNSATISFIABLE) - cerr << "u"; - else if (result == SOLVER_SATISFIABLE) - cerr << "s"; - else if (result == SOLVER_UNDECIDED) - cerr << "?"; - } - }; - vector cache; - vector > symbols; - void addSymbol(ASTNode &s) { @@ -270,4 +283,4 @@ namespace BEEV }; } -#endif /* PARSERINTERFACE_H_ */ +#endif diff --git a/src/main/main.cpp b/src/main/main.cpp index f043fe5..d40acb4 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -410,11 +410,6 @@ int main(int argc, char ** argv) { //want to print the output always from the commandline. bm->UserFlags.print_output_flag = true; ASTVec * AssertsQuery = new ASTVec; - CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); - if(0 != c) { - cout << CONSTANTBV::BitVector_Error(c) << endl; - return 0; - } bm->GetRunTimes()->start(RunTimes::Parsing); { @@ -433,6 +428,8 @@ int main(int argc, char ** argv) { else parserInterface = &piTypeCheckSimp; + parserInterface->startup(); + if (onePrintBack) { if (bm->UserFlags.smtlib2_parser_flag) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index fa3c59b..1afbb20 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -219,7 +219,7 @@ namespace BEEV ASTNode Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - _bm->Begin_RemoveWrites = false; + //_bm->Begin_RemoveWrites = false; ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); return out; }