New translator features: expand define-funs and combine assertions.

diff --git a/examples/translator.cpp b/examples/translator.cpp
index b7e6f618ab6d390a5746011f4b4bbe19b0785079..7aa969e06a143fcb6cf509c4be3ae874828260d4 100644 (file)
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -21,6 +21,7 @@
 #include <cstring>
 #include <cstdlib>
 #include <cerrno>
+#include "smt/smt_engine.h"
 #include "util/language.h"
 #include "expr/command.h"
 #include "expr/expr.h"
@@ -38,11 +39,15 @@ enum {
   OUTPUT_FILE = 'o',
   HELP = 'h',
   DEFAULT_DAG_THRESH,
+  EXPAND_DEFINITIONS,
+  COMBINE_ASSERTIONS,
 };/* enum */
 
 const struct option longopts[] = {
   { "output-lang", required_argument, NULL, OUTPUT_LANG },
   { "output-language", required_argument, NULL, OUTPUT_LANG },
+  { "expand-definitions", no_argument, NULL, EXPAND_DEFINITIONS },
+  { "combine-assertions", no_argument, NULL, COMBINE_ASSERTIONS },
   { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
   { "lang", required_argument, NULL, INPUT_LANG },
   { "language", required_argument, NULL, INPUT_LANG },
@@ -57,6 +62,8 @@ static void showHelp() {
        << "  --input-language | -L   set input language (default auto)" << endl
        << "  --out | -o              set output file (- for stdout)" << endl
        << "  --default-dag-thresh=N  set DAG threshold" << endl
+       << "  --expand-definitions    expand define-funs" << endl
+       << "  --combine-assertions    combine all assertions into one" << endl
        << "  --help | -h             this help" << endl
        << "Options and input filenames can be intermixed, and order is important." << endl
        << "For instance, \"-O smt2 x -O cvc4 y\" reads file x in smt2 format and"
@@ -65,7 +72,7 @@ static void showHelp() {
        << "Comments and formatting are not preserved." << endl;
 }
 
-static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, ostream* out) {
+static void readFile(const char* filename, InputLanguage fromLang, OutputLanguage toLang, bool expand_definitions, bool combine_assertions, ostream* out) {
   if(fromLang == input::LANG_AUTO) {
     unsigned len = strlen(filename);
     if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
@@ -100,15 +107,87 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag
     parserBuilder.withLineBufferedStreamInput(cin);
   }
   Parser *parser = parserBuilder.build();
+  // we only use the SmtEngine to do definition expansion for us
+  SmtEngine *smt = expand_definitions ? new SmtEngine(&exprMgr) : NULL;
+  // store up the assertions into one big conjunction
+  std::vector<Expr> assertions;
   while(Command* cmd = parser->nextCommand()) {
-    *out << cmd << endl;
+    if(expand_definitions && dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
+      // tell the SmtEngine about the definition, but don't print it
+      cmd->invoke(smt);
+    } else {
+      // have to switch on the command and expand definitions inside it
+      if(expand_definitions && dynamic_cast<AssertCommand*>(cmd) != NULL) {
+        Expr e = static_cast<AssertCommand*>(cmd)->getExpr();
+        delete cmd;
+        cmd = new AssertCommand(smt->expandDefinitions(e));
+      } else if(expand_definitions && dynamic_cast<QueryCommand*>(cmd) != NULL) {
+        Expr e = static_cast<QueryCommand*>(cmd)->getExpr();
+        delete cmd;
+        cmd = new QueryCommand(smt->expandDefinitions(e));
+      } else if(expand_definitions && dynamic_cast<CheckSatCommand*>(cmd) != NULL) {
+        Expr e = static_cast<CheckSatCommand*>(cmd)->getExpr();
+        delete cmd;
+        cmd = new CheckSatCommand(smt->expandDefinitions(e));
+      } else if(expand_definitions && dynamic_cast<SimplifyCommand*>(cmd) != NULL) {
+        Expr e = static_cast<SimplifyCommand*>(cmd)->getTerm();
+        delete cmd;
+        cmd = new SimplifyCommand(smt->expandDefinitions(e));
+      } else if(expand_definitions && dynamic_cast<ExpandDefinitionsCommand*>(cmd) != NULL) {
+        Expr e = static_cast<ExpandDefinitionsCommand*>(cmd)->getTerm();
+        delete cmd;
+        cmd = new ExpandDefinitionsCommand(smt->expandDefinitions(e));
+      } else if(expand_definitions && dynamic_cast<GetValueCommand*>(cmd) != NULL) {
+        vector<Expr> terms = static_cast<GetValueCommand*>(cmd)->getTerms();
+        delete cmd;
+        for(size_t i = 0; i < terms.size(); ++i) {
+          terms[i] = smt->expandDefinitions(terms[i]);
+        }
+        cmd = new GetValueCommand(terms);
+      }
+
+      if(combine_assertions && dynamic_cast<AssertCommand*>(cmd) != NULL) {
+        // store up the assertion, don't print it yet
+        assertions.push_back(static_cast<AssertCommand*>(cmd)->getExpr());
+      } else {
+        if(combine_assertions &&
+           ( dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
+             dynamic_cast<QueryCommand*>(cmd) != NULL ||
+             dynamic_cast<PushCommand*>(cmd) != NULL ||
+             dynamic_cast<PopCommand*>(cmd) != NULL ||
+             dynamic_cast<SimplifyCommand*>(cmd) != NULL ||
+             dynamic_cast<QuitCommand*>(cmd) != NULL )) {
+          // combine all the stored assertions and print them at this point
+          if(!assertions.empty()) {
+            if(assertions.size() > 1) {
+              *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl;
+            } else {
+              *out << AssertCommand(assertions[0]) << endl;
+            }
+            assertions.clear();
+          }
+        }
+
+        // now print the cmd we just parsed
+        *out << cmd << endl;
+      }
+    }
     if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
       delete cmd;
       break;
     }
     delete cmd;
   }
+  if(!assertions.empty()) {
+    if(assertions.size() > 1) {
+      *out << AssertCommand(exprMgr.mkExpr(kind::AND, assertions)) << endl;
+    } else {
+      *out << AssertCommand(assertions[0]) << endl;
+    }
+    assertions.clear();
+  }
   *out << flush;
+  delete smt;
   delete parser;
 }
 
@@ -121,6 +200,8 @@ int main(int argc, char* argv[]) {
   OutputLanguage toLang = output::LANG_SMTLIB_V2;
   size_t files = 0;
   int dag_thresh = 1;
+  bool expand_definitions = false;
+  bool combine_assertions = false;
 
   try {
     int c;
@@ -129,7 +210,7 @@ int main(int argc, char* argv[]) {
       case 1:
         ++files;
         *out << Expr::dag(dag_thresh);
-        readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, out);
+        readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out);
         break;
       case INPUT_LANG:
         if(!strcmp(optarg, "help")) {
@@ -173,6 +254,12 @@ int main(int argc, char* argv[]) {
           dag_thresh = ul > INT_MAX ? INT_MAX : int(ul);
         }
         break;
+      case EXPAND_DEFINITIONS:
+        expand_definitions = true;
+        break;
+      case COMBINE_ASSERTIONS:
+        combine_assertions = true;
+        break;
       case 'h':
         showHelp();
         exit(0);
@@ -188,7 +275,7 @@ int main(int argc, char* argv[]) {
 
     if(files == 0) {
       *out << Expr::dag(dag_thresh);
-      readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, out);
+      readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out);
       exit(0);
     }
   } catch(Exception& e) {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 28a45206f80be3a7f0f86dc7dc3b84c7f4e4a372..f82fc86edcc5dd1b33c64d2e660d812482a760df 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -528,7 +528,7 @@ public:
   /**
    * Expand definitions in n.
    */
-  Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
+  Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false)
     throw(TypeCheckingException, LogicException);
 
   /**
@@ -1501,10 +1501,7 @@ void SmtEngine::defineFunction(Expr func,
   d_definedFunctions->insert(funcNode, def);
 }
 
-
-
-
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
+Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
   throw(TypeCheckingException, LogicException) {
 
   stack< triple<Node, Node, bool> > worklist;
@@ -1586,12 +1583,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
                                       n.begin(), n.end());
         Debug("expand") << "made : " << instance << endl;
 
-        Node expanded = expandDefinitions(instance, cache);
+        Node expanded = expandDefinitions(instance, cache, expandOnly);
         cache[n] = (n == expanded ? Node::null() : expanded);
         result.push(expanded);
         continue;
 
-      } else {
+      } else if(! expandOnly) {
+        // do not do any theory stuff if expandOnly is true
+
         theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
 
         Assert(t != NULL);
@@ -3478,7 +3477,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
     Dump("benchmark") << ExpandDefinitionsCommand(e);
   }
   hash_map<Node, Node, NodeHashFunction> cache;
-  Node n = d_private->expandDefinitions(Node::fromExpr(e), cache);
+  Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
   n = postprocess(n, TypeNode::fromType(e.getType()));
 
   return n.toExpr();