* When printing in CVC format, traverse the nodes looking for symbols rather than...

* Fix the SMTLIB printer, convert NAND to NOT(AND(.., typo on extrapred, convert pluses with >2 arguments into nested 2 argument pluses.
* Bugfix. Call print-back with the correct input function.

Note. GDL print-back isn't printing out the entire input expression. I'm not sure why.

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 09e54467966de9901828309b20958966aefa2cb2..ac9e8292b712de389b56c2729b45a33c0b084ace 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -27,7 +27,6 @@ namespace BEEV
   bool isAtomic(Kind k);
   bool isCommutative(const Kind k);
 
-
   // If (a > b) in the termorder, then return 1 elseif (a < b) in the
   // termorder, then return -1 else return 0
   int TermOrder(const ASTNode& a, const ASTNode& b);
@@ -104,5 +103,7 @@ namespace BEEV
 
   // Function to dump contents of ASTNodeMap
   ostream &operator<<(ostream &os, const ASTNodeMap &nmap);
+
+  void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,ASTNodeSet& symbols);
 }; // end namespace BEEV
 #endif

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 1f6b9afb417da4a921137ef0a82e8250d730ae58..b700eb5f79436e8e956999ec4ca4df4594fdeb25 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -112,6 +112,22 @@ namespace BEEV
     return true;
   }
 
+  void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,
+               ASTNodeSet& symbols)
+  {
+       if (visited.find(n) != visited.end())
+               return; // already visited.
+
+       visited.insert(n);
+
+       if (n.GetKind() == SYMBOL)
+       {
+               symbols.insert(n);
+       }
+
+       for (unsigned i = 0; i < n.GetChildren().size(); i++)
+               buildListOfSymbols(n[i], visited, symbols);
+  }
 
 
   /* FUNCTION: Typechecker for terms and formulas

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index c5a53b13092da12e4a86b4a8e5c269310d809f5d..dc34c200d49e56c0469c0b71559bb5998e7ab5e7 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -371,7 +371,7 @@ namespace BEEV
     void ASTNodeStats(const char * c, const ASTNode& a);
 
     // Print variable to the input stream
-    void printVarDeclsToStream(ostream &os);
+    void printVarDeclsToStream(ostream &os, ASTNodeSet& symbols);
 
     // Print assertions to the input stream
     void printAssertsToStream(ostream &os, int simplify);

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d1615b63f2cc3c4e804170975479aa8d9b50f698..251add57de9702d8d1f5ed819fc2c6058d83e0f5 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -344,6 +344,11 @@ int main(int argc, char ** argv) {
   if (onePrintBack)
   {
 
+    ASTNode original_input = bm->CreateNode(AND,
+               bm->CreateNode(NOT, query),
+               asserts);
+
+
   if(bm->UserFlags.print_STPinput_back_flag)
     {
       if(bm->UserFlags.smtlib_parser_flag)
@@ -354,27 +359,28 @@ int main(int argc, char ** argv) {
 
   if (bm->UserFlags.print_STPinput_back_CVC_flag)
   {
+         //needs just the query. Reads the asserts out of the data structure.
          print_STPInput_Back(query);
   }
 
   if (bm->UserFlags.print_STPinput_back_SMTLIB_flag)
     {
-         printer::SMTLIB_PrintBack(cout, asserts);
+         printer::SMTLIB_PrintBack(cout, original_input);
     }
 
   if (bm->UserFlags.print_STPinput_back_C_flag)
     {
-         printer::C_Print(cout, asserts);
+         printer::C_Print(cout, original_input);
     }
 
   if (bm->UserFlags.print_STPinput_back_GDL_flag)
     {
-         printer::GDL_Print(cout, asserts);
+         printer::GDL_Print(cout, original_input);
     }
 
   if (bm->UserFlags.print_STPinput_back_dot_flag)
     {
-         printer::Dot_Print(cout, asserts);
+         printer::Dot_Print(cout, original_input);
     }
 
   return 0;

diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp
index d332bbf243ff59e2c413f680293efc10f0839dbe..4bd690a009d8c33fa39726b649bc425b6c3cccc3 100644 (file)
--- a/src/printer/AssortedPrinters.cpp
+++ b/src/printer/AssortedPrinters.cpp
@@ -86,8 +86,8 @@ namespace BEEV
   //     cout << endl;
   //   } //end of Convert_MINISATVar_To_ASTNode_Print()
 
-  void STPMgr::printVarDeclsToStream(ostream &os) {
-    for(ASTVec::iterator 
+  void STPMgr::printVarDeclsToStream(ostream &os, ASTNodeSet& ListOfDeclaredVars) {
+    for(ASTNodeSet::iterator
           i = ListOfDeclaredVars.begin(),iend=ListOfDeclaredVars.end();
         i!=iend;i++) 
       {
@@ -113,8 +113,6 @@ namespace BEEV
       }
   } //printVarDeclsToStream
 
-
-
   void STPMgr::printAssertsToStream(ostream &os, int simplify_print) {
     ASTVec v = GetAsserts();
     for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
@@ -130,7 +128,16 @@ namespace BEEV
   }
 
   void print_STPInput_Back(const ASTNode& query) {
-    (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout);
+
+         // Determine the symbols in the query and asserts.
+         ASTNodeSet visited;
+         ASTNodeSet symbols;
+         buildListOfSymbols(query,  visited, symbols);
+      ASTVec v = (BEEV::GlobalSTP->bm)->GetAsserts();
+      for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++)
+       buildListOfSymbols(*i,  visited, symbols);
+
+       (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout, symbols);
     (BEEV::GlobalSTP->bm)->printAssertsToStream(cout,0);
     cout << "QUERY(";
     query.PL_Print(cout);

diff --git a/src/printer/GDLPrinter.cpp b/src/printer/GDLPrinter.cpp
index 4ec51f342b6f430ac65eeaf2336b41e912f6ca04..89e4c3ef95dc339dc564c9f4146183bc21c6518f 100644 (file)
--- a/src/printer/GDLPrinter.cpp
+++ b/src/printer/GDLPrinter.cpp
@@ -51,14 +51,14 @@ namespace printer
     os << "\"}" << endl;
 
     // print the edges to each child.
-    ASTVec ch = n.GetChildren();
-    ASTVec::iterator itend = ch.end();
+    const ASTVec ch = n.GetChildren();
+    const ASTVec::const_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++)
+    for (ASTVec::const_iterator it = ch.begin(); it < itend; it++)
       {
        std::stringstream label;
 
@@ -91,7 +91,7 @@ namespace printer
       }
 
     // print each of the children.
-    for (ASTVec::iterator it = ch.begin(); it < itend; it++)
+    for (ASTVec::const_iterator it = ch.begin(); it < itend; it++)
       {
        if (!it->isConstant())
                GDL_Print1(os, *it, alreadyOutput,annotate);

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 929611126ca6a17da2f01adff0e0a7dda6f1cad5..bc5ba0097e0140725e05cff1eb98280c72a20088 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -45,23 +45,6 @@ std::vector<pair<ASTNode, ASTNode> > NodeLetVarVec;
 //correctly print shared subterms inside the LET itself
 ASTNodeMap NodeLetVarMap1;
 
-void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,
-               ASTNodeSet& symbols)
-{
-       if (visited.find(n) != visited.end())
-               return; // already visited.
-
-       visited.insert(n);
-
-       if (n.GetKind() == SYMBOL)
-       {
-               symbols.insert(n);
-       }
-
-       for (unsigned i = 0; i < n.GetChildren().size(); i++)
-               buildListOfSymbols(n[i], visited, symbols);
-}
-
   // Initial version intended to print the whole thing back.
 void SMTLIB_PrintBack(ostream &os, const ASTNode& n)
 {
@@ -102,7 +85,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         os << ":" << a.GetValueWidth() << "] ))" << endl;
         break;
       case BEEV::BOOLEAN_TYPE:
-        os << ":extrapred (( ";
+        os << ":extrapreds (( ";
         a.nodeprint(os);
         os << "))" << endl;
         break;
@@ -184,6 +167,15 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
       case FALSE:
         os << "false";
         break;
+      case NAND: // No NAND in smtlib format.
+         assert(c.size() ==2);
+         os << "(" << "not ";
+         os << "(" << "and ";
+         SMTLIB_Print1(os, c[0], 0, letize);
+         os << " " ;
+         SMTLIB_Print1(os, c[1], 0, letize);
+         os << "))";
+         break;
       case TRUE:
         os << "true";
         break;
@@ -211,19 +203,38 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
           os << ")";
         }
         break;
-      default:
-        {
-          os << "(" << functionToSMTLIBName(kind);
-
-          ASTVec::const_iterator iend = c.end();
-          for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
-            {
-              os << " ";
-              SMTLIB_Print1(os, *i, 0, letize);
-            }
-
-          os << ")";
-        }
+       default:
+       {
+               // SMT-LIB only allows arithmetic functions to have two parameters.
+               if (BVPLUS == kind && n.Degree() > 2)
+               {
+                       string close = "";
+
+                       for (int i =0; i < c.size()-1; i++)
+                       {
+                               os << "(" << functionToSMTLIBName(kind);
+                               os << " ";
+                               SMTLIB_Print1(os, c[i], 0, letize);
+                               os << " ";
+                               close += ")";
+                       }
+                       SMTLIB_Print1(os, c[c.size()-1], 0, letize);
+                       os << close;
+               }
+               else
+               {
+                       os << "(" << functionToSMTLIBName(kind);
+
+                       ASTVec::const_iterator iend = c.end();
+                       for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
+                       {
+                               os << " ";
+                               SMTLIB_Print1(os, *i, 0, letize);
+                       }
+
+                       os << ")";
+               }
+       }
       }
   }