From: trevor_hansen Date: Thu, 26 Jan 2012 04:23:02 +0000 (+0000) Subject: Cleanup. This removes some of the code for the user controlled abstraction-refinement... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f7eac78d33f49f5dd7c6155931a6d086769cc8a6;p=francis%2Fstp.git Cleanup. This removes some of the code for the user controlled abstraction-refinement. I don't know if this code worked or not. There aren't any test cases that use it, so it might be broken. Removing this makes some changes I'm trying to make much easier. Sorry if you use it. Let me know. Trev. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1524 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index db071c2..4592366 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -434,7 +434,7 @@ namespace BEEV } //add an assertion to the current logical context - void STPMgr::AddAssert(const ASTNode& assert, int assertion_bucket_key) + void STPMgr::AddAssert(const ASTNode& assert) { if (!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) @@ -442,83 +442,28 @@ namespace BEEV FatalError("AddAssert:Trying to assert a non-formula:", assert); } - IntToASTVecMap * AssertsMap; - //if the stack of assertion contexts is not empty, then take the - //top ASTVec and add the input assert to it - if(!_asserts.empty()) - { - AssertsMap = _asserts.back(); - } - else - { - AssertsMap = new IntToASTVecMap(); - _asserts.push_back(AssertsMap); - } + if(_asserts.empty()) + _asserts.push_back(new ASTVec()); - ASTVec * v; - if(AssertsMap->find(assertion_bucket_key) != AssertsMap->end()) - { - v = (*AssertsMap)[assertion_bucket_key]; - v->push_back(assert); - } - else - { - v = new ASTVec(); - v->push_back(assert); - (*AssertsMap)[assertion_bucket_key] = v; - } - - // //if the stack of ASTVec is not empty, then take the top ASTVec - // //and add the input assert to it - // if (!_asserts.empty()) - // { - // v = _asserts.back(); - // //v->push_back(TransformFormula(assert)); - // v->push_back(assert); - // } - // else - // { - // //else create a logical context, and add it to the top of the - // //stack - // v = new ASTVec(); - // //v->push_back(TransformFormula(assert)); - // v->push_back(assert); - // _asserts.push_back(v); - // } + ASTVec& v = *_asserts.back(); + v.push_back(assert); } void STPMgr::Push(void) { - // ASTVec * v; - // v = new ASTVec(); - IntToASTVecMap * v; - v = new IntToASTVecMap(); - _asserts.push_back(v); + _asserts.push_back(new ASTVec()); } - void STPMgr::Pop(void) + void + STPMgr::Pop(void) { - if (!_asserts.empty()) - { - IntToASTVecMap * c = _asserts.back(); - IntToASTVecMap::iterator it = c->begin(), itend = c->end(); - for(;it!=itend;it++) - { - ASTVec * cc = (*it).second; - cc->clear(); - delete cc; - } - delete c; - _asserts.pop_back(); - - // ASTVec * c = _asserts.back(); - // //by calling the clear function we ensure that the - // ref count is //decremented for the ASTNodes stored - // in c - // c->clear(); - // delete c; - // _asserts.pop_back(); - } + if (_asserts.empty()) + FatalError("POP on empty."); + + ASTVec * c = _asserts.back(); + c->clear(); + delete c; + _asserts.pop_back(); } void STPMgr::AddQuery(const ASTNode& q) @@ -540,74 +485,21 @@ namespace BEEV return _current_query; } - const ASTVec STPMgr::GetAsserts(void) + const ASTVec + STPMgr::GetAsserts(void) { - vector::iterator it = _asserts.begin(); - vector::iterator itend = _asserts.end(); + vector::iterator it = _asserts.begin(); + vector::iterator itend = _asserts.end(); ASTVec v; - for(; it != itend; it++) + for (; it != itend; it++) { - IntToASTVecMap::iterator jt = (*it)->begin(); - IntToASTVecMap::iterator jtend = (*it)->end(); - - for(; jt != jtend; jt++) - { - ASTVec * cc = (*jt).second; - if(NULL != cc && !cc->empty()) - { - v.insert(v.end(), cc->begin(), cc->end()); - } - } + if (!(*it)->empty()) + v.insert(v.end(), (*it)->begin(), (*it)->end()); } - return v; - // vector::iterator it = _asserts.begin(); - // vector::iterator itend = _asserts.end(); - - // ASTVec v; - // for (; it != itend; it++) - // { - // if (!(*it)->empty()) - // v.insert(v.end(), (*it)->begin(), (*it)->end()); - // } - // return v; } - const ASTVec STPMgr::GetAsserts_WithKey(int key) - { - vector::iterator it = _asserts.begin(); - vector::iterator itend = _asserts.end(); - - ASTVec v; - for(; it != itend; it++) - { - IntToASTVecMap * assert_map = (*it); - ASTVec * cc = (*assert_map)[key]; - if(!cc->empty()) - { - v.insert(v.end(), cc->begin(), cc->end()); - } - } - - return v; - } - - // //Create a new variable of ValueWidth 'n' - // ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value) - // { - // std::string c("v"); - // char d[32]; - // sprintf(d, "%d", _symbol_count++); - // std::string ccc(d); - // c += "_writearray_" + ccc; - - // ASTNode CurrentSymbol = CreateSymbol(c.c_str()); - // CurrentSymbol.SetValueWidth(value); - // CurrentSymbol.SetIndexWidth(index); - // return CurrentSymbol; - // } //end of NewArrayVar() - //prints statistics for the ASTNode void STPMgr::ASTNodeStats(const char * c, const ASTNode& a) { @@ -726,15 +618,11 @@ namespace BEEV _symbol_unique_table.clear(); _bvconst_unique_table.clear(); - vector::iterator it = _asserts.begin(); - vector::iterator itend = _asserts.end(); + vector::iterator it = _asserts.begin(); + vector::iterator itend = _asserts.end(); for (; it != itend; it++) { - IntToASTVecMap * j = (*it); - for (IntToASTVecMap::iterator it2 = j->begin(); it2 != j->end(); it2++) { - it2->second->clear(); - delete (it2->second); - } + ASTVec * j = (*it); j->clear(); delete j; } diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index a329728..937e2cb 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -120,7 +120,7 @@ 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 ASTNodeMap TermsAlreadySeenMap; @@ -389,11 +389,10 @@ namespace BEEV const ASTNode PopQuery(); const ASTNode GetQuery(); const ASTVec GetAsserts(void); - const ASTVec GetAsserts_WithKey(int key); //add a query/assertion to the current logical context void AddQuery(const ASTNode& q); - void AddAssert(const ASTNode& assert, int userguided_absrefine=0); + void AddAssert(const ASTNode& assert); /**************************************************************** * Toplevel printing and stats functions * diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index aaba6b2..5034c39 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -399,7 +399,7 @@ Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue) { ///////////////////////////////////////////////////////////////////////////// //! Assert a new formula in the current context. /*! The formula must have Boolean type. */ -void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) { +void vc_assertFormula(VC vc, Expr e) { nodestar a = (nodestar)e; bmstar b = (bmstar)(((stpstar)vc)->bm); @@ -407,7 +407,7 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) { BEEV::FatalError("Trying to assert a NON formula: ",*a); assert(BVTypeCheck(*a)); - b->AddAssert(*a, absrefine_bucket_num); + b->AddAssert(*a); } void soft_time_out(int ignored) diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index de0dbd5..2184727 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -198,7 +198,7 @@ extern "C" { //! Assert a new formula in the current context. /*! The formula must have Boolean type. */ - void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num _CVCL_DEFAULT_ARG(0)); + void vc_assertFormula(VC vc, Expr e); //! Simplify e with respect to the current context Expr vc_simplify(VC vc, Expr e);