From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Dec 2013 19:16:24 +0000 (-0500)
Subject: Partial kind branch merge, including new --rewrite-apply-to-const feature.
X-Git-Tag: cvc5-1.0.0~7207
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c378d2955afd4d4085701935db4951d85edefef8;p=cvc5.git

Partial kind branch merge, including new --rewrite-apply-to-const feature.
---

diff --git a/src/smt/options b/src/smt/options
index f3da7a0a7..05a138f60 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -85,6 +85,9 @@ common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
 common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
+expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
+ eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
+
 # --replay is currently broken; don't document it for 1.0
 undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
  replay decisions from file
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index c631b8c84..574ef720f 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -84,7 +84,8 @@ assertions\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
   where PASS is one of the preprocessing passes: definition-expansion\n\
   boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
-  static-learning ite-removal repeat-simplify theory-preprocessing.\n\
+  static-learning ite-removal repeat-simplify rewrite-apply-to-const\n\
+  theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
   \"assertions:pre-everything\") or after all preprocessing completes\n\
@@ -185,6 +186,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       } else if(!strcmp(p, "static-learning")) {
       } else if(!strcmp(p, "ite-removal")) {
       } else if(!strcmp(p, "repeat-simplify")) {
+      } else if(!strcmp(p, "rewrite-apply-to-const")) {
       } else if(!strcmp(p, "theory-preprocessing")) {
       } else if(!strcmp(p, "nonclausal")) {
       } else if(!strcmp(p, "theorypp")) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index eaaa201c3..a2a95d6ca 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -604,6 +604,54 @@ public:
     return val;
   }
 
+  std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache;
+  Node rewriteApplyToConst(TNode n) {
+    Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
+
+    if(n.getMetaKind() == kind::metakind::CONSTANT || n.getMetaKind() == kind::metakind::VARIABLE) {
+      return n;
+    }
+
+    if(rewriteApplyToConstCache.find(n) != rewriteApplyToConstCache.end()) {
+      Trace("rewriteApplyToConst") << "in cache :: " << rewriteApplyToConstCache[n] << std::endl;
+      return rewriteApplyToConstCache[n];
+    }
+    if(n.getKind() == kind::APPLY_UF) {
+      if(n.getNumChildren() == 1 && n[0].isConst() && n[0].getType().isInteger()) {
+        stringstream ss;
+        ss << n.getOperator() << "_";
+        if(n[0].getConst<Rational>() < 0) {
+          ss << "m" << -n[0].getConst<Rational>();
+        } else {
+          ss << n[0];
+        }
+        Node newvar = NodeManager::currentNM()->mkSkolem(ss.str(), n.getType(), "rewriteApplyToConst skolem", NodeManager::SKOLEM_EXACT_NAME);
+        rewriteApplyToConstCache[n] = newvar;
+        Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
+        return newvar;
+      } else {
+        stringstream ss;
+        ss << "The rewrite-apply-to-const preprocessor is currently limited;\n"
+           << "it only works if all function symbols are unary and with Integer\n"
+           << "domain, and all applications are to integer values.\n"
+           << "Found application: " << n;
+        Unhandled(ss.str());
+      }
+    }
+
+    NodeBuilder<> builder(n.getKind());
+    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      builder << n.getOperator();
+    }
+    for(unsigned i = 0; i < n.getNumChildren(); ++i) {
+      builder << rewriteApplyToConst(n[i]);
+    }
+    Node rewr = builder;
+    rewriteApplyToConstCache[n] = rewr;
+    Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl;
+    return rewr;
+  }
+
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -3137,6 +3185,16 @@ void SmtEnginePrivate::processAssertions() {
   }
   dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
 
+  dumpAssertions("pre-rewrite-apply-to-const", d_assertionsToCheck);
+  if(options::rewriteApplyToConst()) {
+    Chat() << "Rewriting applies to constants..." << endl;
+    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
+    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+      d_assertionsToCheck[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertionsToCheck[i]));
+    }
+  }
+  dumpAssertions("post-rewrite-apply-to-const", d_assertionsToCheck);
+
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 #ifdef CVC4_ASSERTIONS