Bugfix. Prevent *TrueDummy* being output in the counter example.

This is a nicer way of stopping it being output.

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

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 1bb7ffc4e05b0c4a004d565073545886f81abc20..6342f5ac95747a3ad1c09a03c95e9ce218f86c77 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -911,14 +911,13 @@ namespace BEEV
                                            ClauseList* defs)
   {
     ASTNode dummy_false_var = 
-      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0));
+      bm->CreateNode(NOT, dummy_true_var);
     info[varphi]->clausespos = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFPosFALSE()
 
   void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, 
                                           ClauseList* defs)
   {
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     info[varphi]->clausespos = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFPosTRUE
 
@@ -1285,7 +1284,6 @@ namespace BEEV
   void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, 
                                            ClauseList* defs)
   {
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     info[varphi]->clausesneg = SINGLETON(dummy_true_var);
   } //End of convertFormulaToCNFNegFALSE()
 
@@ -1293,7 +1291,7 @@ namespace BEEV
                                           ClauseList* defs)
   {
     ASTNode dummy_false_var = 
-      bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0));
+      bm->CreateNode(NOT, dummy_true_var);
     info[varphi]->clausesneg = SINGLETON(dummy_false_var);
   } //End of convertFormulaToCNFNegTRUE()
 
@@ -1743,6 +1741,7 @@ namespace BEEV
     bm = bmgr;
     clausesxor = new ClauseList();
     renameAllSiblings = bm->UserFlags.renameAllInCNF_flag;
+    dummy_true_var = bmgr->CreateFreshVariable(0,0,"*TrueDummy*");
   }
 
   //########################################
@@ -1766,7 +1765,6 @@ namespace BEEV
   {
     bm->GetRunTimes()->start(RunTimes::CNFConversion);
     scanFormula(varphi, true, false);
-    ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0);
     ClauseList* defs = SINGLETON(dummy_true_var);
     convertFormulaToCNF(varphi, defs);
     ClauseList* top = info[varphi]->clausespos;

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index 865ca7afd3fa954432ae9ac2234060a4ce45ad6f..7c9d25d74f67ef3a9d81924538507a7e706722a3 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -236,6 +236,8 @@ namespace BEEV
 
     void cleanup(const ASTNode& varphi);    
 
+    ASTNode dummy_true_var;
+
   public:
 
     //########################################