From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 13 Mar 2010 12:32:40 +0000 (+0000)
Subject: * Mark some single argument functions as commutative.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ea38b835180c981fa4b845acc2022d1b014fa4aa;p=francis%2Fstp.git

* Mark some single argument functions as commutative.
* Prevent duplicate constant nodes being created by the GDL printer.



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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 5a9f928..1f6b9af 100644
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -33,6 +33,9 @@ namespace BEEV
 	case NOR:
 	case XOR:
 	case IFF:
+	case BVNEG:
+	case NOT:
+	case BVUMINUS:
 		return true;
 	default:
 		return false;
diff --git a/src/printer/GDLPrinter.cpp b/src/printer/GDLPrinter.cpp
index f84d963..4ec51f3 100644
--- a/src/printer/GDLPrinter.cpp
+++ b/src/printer/GDLPrinter.cpp
@@ -54,6 +54,9 @@ namespace printer
     ASTVec ch = n.GetChildren();
     ASTVec::iterator itend = ch.end();
 
+    //If a node has the child 'TRUE' twice, we only want to output one TRUE node.
+    ASTNodeSet constantOutput;
+
     int i =0;
     for (ASTVec::iterator it = ch.begin(); it < itend; it++)
       {
@@ -62,19 +65,23 @@ namespace printer
     	if (!isCommutative(n.GetKind()))
     		label << " label:\"" << i << "\"";
 
-
     	if (it->isConstant())
     	{
 			std::stringstream ss;
-			os << "node: { title:\"n";
 			ss << n.GetNodeNum() << "_" << it->GetNodeNum();
 
-			os << ss.str() << "\" label: \"";
-			if (it->GetType() == BEEV::BOOLEAN_TYPE)
-				os << _kind_names[it->GetKind()];
-			else
-				outputBitVec(*it, os);
-			os << "\"}" << endl;
+			if (constantOutput.end() == constantOutput.find(*it))
+			{
+				os << "node: { title:\"n";
+
+				os << ss.str() << "\" label: \"";
+				if (it->GetType() == BEEV::BOOLEAN_TYPE)
+					os << _kind_names[it->GetKind()];
+				else
+					outputBitVec(*it, os);
+				os << "\"}" << endl;
+				constantOutput.insert(*it);
+			}
 
 			os << "edge: { source:\"n" << n.GetNodeNum() << "\" target: \"" << "n" << ss.str()  << "\"" << label.str() << "}" << endl;
     	}