Fix strings preprocessing for justification heuristic

diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 51ad7b6ca9b33431aa83654c9bc2fe0e3fc8d150..c9c3d6345a87cfe2cea33109c25e77ca4afe058d 100644 (file)
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -83,9 +83,9 @@ assertions\n\
 + Output the assertions after preprocessing and before clausification.\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 rewrite-apply-to-const\n\
-  theory-preprocessing.\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const 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\
@@ -181,6 +181,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       } else if(!strcmp(p, "boolean-terms")) {
       } else if(!strcmp(p, "constrain-subtypes")) {
       } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
       } else if(!strcmp(p, "skolem-quant")) {
       } else if(!strcmp(p, "simplify")) {
       } else if(!strcmp(p, "static-learning")) {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dcca1624db89da6ef3c260823bd583cdfc5696be..ec91e566e697b39402aeab2f1156305c39fa369d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3124,11 +3124,18 @@ void SmtEnginePrivate::processAssertions() {
   // Assertions ARE guaranteed to be rewritten by this point
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+    dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
     CVC4::theory::strings::StringsPreprocess sp;
-    sp.simplify( d_assertionsToPreprocess );
+    std::vector<Node> newNodes;
+    newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
+    sp.simplify( d_assertionsToPreprocess, newNodes );
+    if(newNodes.size() > 1) {
+      d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+    }
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
       d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
     }
+    dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
   }
   if( d_smt.d_logic.isQuantified() ){
     dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 2b0cedd07efd70e85b572c35eb6c190d7a13da3d..b2fa3dcd35f553469b703ee9b64124624e7ea6ef 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -378,11 +378,15 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
        return retNode;
 }
 
-void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
-       std::vector< Node > new_nodes;
+void StringsPreprocess::simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes) {
        for( unsigned i=0; i<vec_node.size(); i++ ){
                vec_node[i] = simplify( vec_node[i], new_nodes );
        }
+}
+
+void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+       std::vector< Node > new_nodes;
+       simplify(vec_node, new_nodes);
        vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
 

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 7aa0a2af841df93d994634c6a46c7c9b9d368f53..c2d5d656a687f39af2871eebd4c73f83d8dd8dd9 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -39,6 +39,7 @@ private:
        void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
        Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
+    void simplify(std::vector< Node > &vec_node, std::vector< Node > &new_nodes);
     void simplify(std::vector< Node > &vec_node);
        StringsPreprocess();
 };