From a5fafd0f5e0610fac5e7473319e33d5f7dc371c0 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 2 Jan 2011 13:42:22 +0000
Subject: [PATCH] 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
---
 src/to-sat/ToCNF.cpp | 8 +++-----
 src/to-sat/ToCNF.h   | 2 ++
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 1bb7ffc..6342f5a 100644
--- 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 865ca7a..7c9d25d 100644
--- 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:
 
     //########################################
-- 
2.47.3