From 2d0730c6afa2c7810c0f6d089b4df1265144bab9 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Mon, 16 Nov 2009 23:13:05 +0000 Subject: [PATCH] added code to facilitate user-guided abstraction-refinement git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@409 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 4 +- src/STPManager/STPManager.cpp | 113 ++++++++++++++++++++++++++-------- src/STPManager/STPManager.h | 13 ++-- src/parser/CVC.lex | 4 +- src/to-sat/ToCNF.cpp | 51 ++++++++++++--- src/to-sat/ToCNF.h | 2 + 6 files changed, 141 insertions(+), 46 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index a57a521..7d12dcb 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -97,8 +97,8 @@ namespace BEEV typedef MAP< int, - ASTVec, - ltint> UserGuided_AbsRefine_Asserts; + ASTVec *, + ltint> IntToASTVecMap; // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 8f9dceb..a64557d 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -491,7 +491,7 @@ namespace BEEV } //add an assertion to the current logical context - void STPMgr::AddAssert(const ASTNode& assert) + void STPMgr::AddAssert(const ASTNode& assert, int assertion_bucket_key) { if (!(is_Form_kind(assert.GetKind()) && BOOLEAN_TYPE == assert.GetType())) @@ -499,30 +499,57 @@ namespace BEEV FatalError("AddAssert:Trying to assert a non-formula:", assert); } - ASTVec * v; - //if the stack of ASTVec is not empty, then take the top ASTVec - //and add the input assert to it - if (!_asserts.empty()) + 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()) { - v = _asserts.back(); - //v->push_back(TransformFormula(assert)); - v->push_back(assert); + AssertsMap = _asserts.back(); } 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); + AssertsMap = new IntToASTVecMap(); + _asserts.push_back(AssertsMap); + } + + 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); + // } } void STPMgr::Push(void) { - ASTVec * v; - v = new ASTVec(); + // ASTVec * v; + // v = new ASTVec(); + IntToASTVecMap * v; + v = new IntToASTVecMap(); _asserts.push_back(v); } @@ -530,12 +557,24 @@ namespace BEEV { if (!_asserts.empty()) { - 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(); + 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(); } } @@ -560,16 +599,36 @@ namespace BEEV 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++) { - if (!(*it)->empty()) - v.insert(v.end(), (*it)->begin(), (*it)->end()); + 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()); + } + } } + 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; } // //Create a new variable of ValueWidth 'n' diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index c2c8708..dcec9f6 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -78,7 +78,8 @@ 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; + std::vector _asserts; // Memo table that tracks terms already seen ASTNodeMap TermsAlreadySeenMap; @@ -315,9 +316,9 @@ namespace BEEV const ASTNode PopQuery(); const ASTNode GetQuery(); const ASTVec GetAsserts(void); + //add a query/assertion to the current logical context void AddQuery(const ASTNode& q); - //add an assertion to the current logical context - void AddAssert(const ASTNode& assert); + void AddAssert(const ASTNode& assert, int userguided_absrefine=0); /**************************************************************** * Toplevel printing and stats functions * @@ -384,11 +385,11 @@ namespace BEEV { ClearAllTables(); - vector::iterator it = _asserts.begin(); - vector::iterator itend = _asserts.end(); + vector::iterator it = _asserts.begin(); + vector::iterator itend = _asserts.end(); for(;it!=itend;it++) { - ASTVec * j = (*it); + IntToASTVecMap * j = (*it); j->clear(); delete j; } diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index fd0fc9d..2b43b5b 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -117,8 +117,8 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "LET" { return LET_TOK;} "COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK;} "COUNTERMODEL" { return COUNTEREXAMPLE_TOK;} - "PUSH" { return PUSH_TOK;} - "POP" { return POP_TOK;} +"PUSH" { return PUSH_TOK;} +"POP" { return POP_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { BEEV::ASTNode nptr = (BEEV::ParserBM)->CreateSymbol(yytext); diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index f9f70ae..4916b0c 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -837,10 +837,43 @@ namespace BEEV //######################################## x->clausespos = SINGLETON(psi); + //x->clausesneg = SINGLETON(psi); setWasRenamedPos(*x); }//End of doRenamingPos + void CNFMgr::doRenamingNegXor(const ASTNode& varphi) + { + CNFInfo* x = info[varphi]; + //######################################## + // step 1, calc new variable + //######################################## + + ostringstream oss; + oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; + ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + + //######################################## + // step 2, add defs + //######################################## + + // ClauseList* cl1; + // cl1 = SINGLETON(bm->CreateNode(NOT, psi)); + // ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1); + // defs->insert(defs->end(), cl2->begin(), cl2->end()); + // DELETE(info[varphi]->clausespos); + // DELETE(cl1); + // delete cl2; + + //######################################## + // step 3, update info[varphi] + //######################################## + + //x->clausesneg = SINGLETON(bm->CreateNode(NOT,psi)); + x->clausespos = SINGLETON(bm->CreateNode(NOT,psi)); + setWasRenamedPos(*x); + }//End of doRenamingPos + void CNFMgr::doRenamingNeg(const ASTNode& varphi, ClauseList* defs) { CNFInfo* x = info[varphi]; @@ -1650,13 +1683,13 @@ namespace BEEV { #ifdef FALSE //#ifdef CRYPTOMINISAT - // CNFInfo * xx = info[varphi]; - // if(NULL != xx - // && sharesPos(*xx) > 0 - // && sharesNeg(*xx) > 0) - // { - // return; - // } + CNFInfo * xx = info[varphi]; + if(NULL != xx + && sharesPos(*xx) > 0 + && sharesNeg(*xx) > 0) + { + return; + } ASTVec::const_iterator it = varphi.GetChildren().begin(); ClausePtr xor_clause = new vector(); @@ -1672,10 +1705,10 @@ namespace BEEV ((*(info[*it]->clausespos))[0])->begin(), ((*(info[*it]->clausespos))[0])->end()); } - doRenamingPosXor(varphi); + doRenamingNegXor(varphi); //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); //info[varphi]->clausespos = psi; - ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausespos); + ASTNode varXorNode = GetNodeFrom_SINGLETON(info[varphi]->clausesneg); ASTNode NotVarXorNode = bm->CreateNode(NOT, varXorNode); xor_clause->push_back(ASTNodeToASTNodePtr(NotVarXorNode)); clausesxor->push_back(xor_clause); diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h index ac61d9b..edc7354 100644 --- a/src/to-sat/ToCNF.h +++ b/src/to-sat/ToCNF.h @@ -168,6 +168,8 @@ namespace BEEV void doRenamingPosXor(const ASTNode& varphi); + void doRenamingNegXor(const ASTNode& varphi); + void doRenamingNeg(const ASTNode& varphi, ClauseList* defs); //######################################## -- 2.47.3