* Merge convertFormulaToCNFPosAND() from my branch. This speeds up the CVC regression...

* Fix. RunTimes::SendingToSAT was not stopped on one path.
* Fix unitialised values in the ArrayTransformer class.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@333 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index cc41bfdfc7b49dd4ab34634d838a3064e4afd2ea..65238d74e701a546bb2765f8ad9ddee0170517a6 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -30,8 +30,8 @@ namespace BEEV
       }
     if (vc_error_hdlr)
       vc_error_hdlr(str);
+    assert(0); // gdb will stop here giving a stacktrace.
     exit(-1);
-    //assert(0);
   }
 
   void FatalError(const char * str)
@@ -39,8 +39,9 @@ namespace BEEV
     cerr << "Fatal Error: " << str << endl;
     if (vc_error_hdlr)
       vc_error_hdlr(str);
+    assert(0);
     exit(-1);
-    //assert(0);
+
   }
   
   void SortByExprNum(ASTVec& v)

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index ce4e2c6c417be07df80783dd0d5ca07ef4aabf03..e2fd54352298469661ccdb546f301e9c3a1abb05 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -120,7 +120,9 @@ namespace BEEV
       Introduced_SymbolsSet(),
       bm(bm), 
       simp(s), 
-      debug_transform(0)
+      debug_transform(0),
+      TransformMap(NULL),
+      _symbol_count(0)
     {
       Arrayread_IteMap = new ASTNodeMap();
       Arrayname_ReadindicesMap = new ASTNodeToVecMap();

diff --git a/src/AST/RunTimes.cpp b/src/AST/RunTimes.cpp
index cd7f727b72a4df69ba6b8b67b626a8f2c7f15b7a..5bc0e2b44a17d0305451c1959575af0076891712 100644 (file)
--- a/src/AST/RunTimes.cpp
+++ b/src/AST/RunTimes.cpp
@@ -33,7 +33,11 @@ long RunTimes::getCurrentTime()
 void RunTimes::print()
 {
   if (0 !=  category_stack.size())
-    BEEV::FatalError("category stack is not yet emptuy");
+  {
+         std::cerr << "size:" <<  category_stack.size() << std::endl;
+         std::cerr << "top:" << CategoryNames[category_stack.top().first] << std::endl;
+         BEEV::FatalError("category stack is not yet empty!!");
+  }
 
   std::ostringstream result;
   result << "statistics\n";

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 8bcf7866353e7a08d75188f3057ec9b9c871d0c0..2e5c7c12abf068da058c53dedc9c745e6ba84c80 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1030,23 +1030,34 @@ namespace BEEV
   } //End of convertFormulaToCNFPosNOT()
 
   void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, 
-                                         ClauseList* defs)
-  {
+                                         ClauseList* defs) {
     //****************************************
     // (pos) AND ~> UNION
     //****************************************
-    ASTVec::const_iterator it = varphi.GetChildren().begin();
-    convertFormulaToCNF(*it, defs);
-    ClauseList* psi = COPY(*(info[*it]->clausespos));
-    for (it++; it != varphi.GetChildren().end(); it++)
-      {
-        convertFormulaToCNF(*it, defs);
-        INPLACE_UNION(psi, *(info[*it]->clausespos));
-        reduceMemoryFootprintPos(*it);
-      }
 
-    info[varphi]->clausespos = psi;
-  } //End of convertFormulaToCNFPosAND()
+  ASTVec::const_iterator it = varphi.GetChildren().begin();
+       convertFormulaToCNF(*it, defs);
+       ClauseList* psi = COPY(*(info[*it]->clausespos));
+
+       for (it++; it != varphi.GetChildren().end(); it++) {
+               convertFormulaToCNF(*it, defs);
+               CNFInfo* x = info[*it];
+
+               if (sharesPos(*x) == 1) {
+                       psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end());
+                       delete (x->clausespos);
+                       x->clausespos = NULL;
+                       if (x->clausesneg == NULL) {
+                               delete x;
+                               info.erase(*it);
+                       }
+               } else {
+                       INPLACE_UNION(psi, *(x->clausespos));
+                       reduceMemoryFootprintPos(*it);
+               }
+       }
+       info[varphi]->clausespos = psi;
+} //End of convertFormulaToCNFPosAND()
 
   void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, 
                                           ClauseList* defs)

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index f2a363c14ed8c0259b02d0be74357a36386940db..c6714d3d7747dfdccca15a6f0b04cfe275593da0 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -93,7 +93,8 @@ namespace BEEV
            //terminating early 
            //      cout << "Percentage clauses added: " 
            //           << percentage << endl;
-           bm->GetRunTimes()->start(RunTimes::Solving);
+           bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
+               bm->GetRunTimes()->start(RunTimes::Solving);
            newS.solve();
            bm->GetRunTimes()->stop(RunTimes::Solving);
            if(!newS.okay())
@@ -102,10 +103,11 @@ namespace BEEV
              }
            count = 0;
            flag  = 1;
+       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
          }
         if (newS.okay())
           {
-            continue;
+               continue;
           }    
         else
           {