From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 21 Oct 2009 13:20:42 +0000 (+0000)
Subject: * Merge convertFormulaToCNFPosAND() from my branch. This speeds up the CVC regression... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=413bc81ab1c5248689fd118c1b0851cf9ee697c7;p=francis%2Fstp.git

* Merge convertFormulaToCNFPosAND() from my branch. This speeds up the CVC regression tests by 25%.
* 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 cc41bfd..65238d7 100644
--- 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 ce4e2c6..e2fd543 100644
--- 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 cd7f727..5bc0e2b 100644
--- 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 8bcf786..2e5c7c1 100644
--- 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 f2a363c..c6714d3 100644
--- 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
           {