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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index a57a5216da0893455199db72b89cdab46f264a73..7d12dcb60fe5c33f33eed833b2fa646ac5930deb 100644 (file)
--- 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 8f9dceb7cd1a5fe8b818c3e135eb3d7544f69e31..a64557d0b3be800d2d2ddcadc212b79f8c0df37c 100644 (file)
--- 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<ASTVec *>::iterator it = _asserts.begin();
-    vector<ASTVec *>::iterator itend = _asserts.end();
+    vector<IntToASTVecMap *>::iterator it = _asserts.begin();
+    vector<IntToASTVecMap *>::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<ASTVec *>::iterator it = _asserts.begin();
+    //     vector<ASTVec *>::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 c2c8708460546165bfd1eef9aba3ec9bf5afc4d1..dcec9f6cf8269706384a7878c840ce6d1fb7e90b 100644 (file)
--- 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<ASTVec *> _asserts;
+    //std::vector<ASTVec *> _asserts;
+    std::vector<IntToASTVecMap *> _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<ASTVec*>::iterator it    = _asserts.begin();
-      vector<ASTVec*>::iterator itend = _asserts.end();
+      vector<IntToASTVecMap*>::iterator it    = _asserts.begin();
+      vector<IntToASTVecMap*>::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 fd0fc9dc18f8afaff2fc2fa1aa4c1c2350c001c3..2b43b5b452a35452f7d2612d2b9a45d319fdcb2d 100644 (file)
--- 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 f9f70ae0a31bafb29ad4fb969854ed55ab1f1cba..4916b0cd93621eb02621113262246a55defa8920 100644 (file)
--- 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<const ASTNode*>();
@@ -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 ac61d9bce93660cdd743a643ae8767674a066e00..edc7354341ea4115bd5814e1f752436f2da92771 100644 (file)
--- 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);    
 
     //########################################