* 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 5a9f92835991aaaed1c0af8af05f12aa525a1288..1f6b9afb417da4a921137ef0a82e8250d730ae58 100644 (file)
--- 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 f84d963ba95168279bd55e3580a82771e1c5a4cd..4ec51f342b6f430ac65eeaf2336b41e912f6ca04 100644 (file)
--- 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;
        }