Fix case of disjunctive conclusion in strings (#3254)

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 97f9666bd395a6663651cbdce24f3034f06419b9..56a46eed5981ddb2659ca9b87da255acc5286393 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -123,8 +123,9 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
   {
     return;
   }
+  Node atom = eq.getKind() == NOT ? eq[0] : eq;
   // check if we should send a lemma or an inference
-  if (asLemma || eq == d_false || eq.getKind() == OR || !exp_n.empty()
+  if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty()
       || options::stringInferAsLemmas())
   {
     Node eq_exp;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fafff1412f723de9993a5ec56d292281693a04c2..caaded4c3223eaa4ced8bc0243ca8288a93f5136 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2069,32 +2069,37 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef
              i++)
         {
           Node onr = d_extf_info_tmp[nr[0]].d_ctn[opol][i];
-          Node conc =
+          Node concOrig =
               nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]);
-          conc = Rewriter::rewrite(conc);
-          conc = conc.negate();
-          bool do_infer = false;
-          bool pol = conc.getKind() != NOT;
-          Node lit = pol ? conc : conc[0];
-          if (lit.getKind() == EQUAL)
+          Node conc = Rewriter::rewrite(concOrig);
+          // For termination concerns, we only do the inference if the contains
+          // does not rewrite (and thus does not introduce new terms).
+          if (conc == concOrig)
           {
-            do_infer = pol ? !areEqual(lit[0], lit[1])
-                           : !areDisequal(lit[0], lit[1]);
-          }
-          else
-          {
-            do_infer = !areEqual(lit, pol ? d_true : d_false);
-          }
-          if (do_infer)
-          {
-            std::vector<Node> exp_c;
-            exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
-            Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i];
-            Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end());
-            exp_c.insert(exp_c.end(),
-                         d_extf_info_tmp[ofrom].d_exp.begin(),
-                         d_extf_info_tmp[ofrom].d_exp.end());
-            d_im.sendInference(exp_c, conc, "CTN_Trans");
+            bool do_infer = false;
+            conc = conc.negate();
+            bool pol = conc.getKind() != NOT;
+            Node lit = pol ? conc : conc[0];
+            if (lit.getKind() == EQUAL)
+            {
+              do_infer = pol ? !areEqual(lit[0], lit[1])
+                             : !areDisequal(lit[0], lit[1]);
+            }
+            else
+            {
+              do_infer = !areEqual(lit, pol ? d_true : d_false);
+            }
+            if (do_infer)
+            {
+              std::vector<Node> exp_c;
+              exp_c.insert(exp_c.end(), in.d_exp.begin(), in.d_exp.end());
+              Node ofrom = d_extf_info_tmp[nr[0]].d_ctn_from[opol][i];
+              Assert(d_extf_info_tmp.find(ofrom) != d_extf_info_tmp.end());
+              exp_c.insert(exp_c.end(),
+                           d_extf_info_tmp[ofrom].d_exp.begin(),
+                           d_extf_info_tmp[ofrom].d_exp.end());
+              d_im.sendInference(exp_c, conc, "CTN_Trans");
+            }
           }
         }
       }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d4cc9b29309a42eb68bd6e561e445da674cb0183..cdf93384e850510f9b44a5a0faa3aea148bb5f3f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1684,6 +1684,7 @@ set(regress_1_tests
   regress1/sygus/issue3200.smt2
   regress1/sygus/issue3201.smt2
   regress1/sygus/issue3205.smt2
+  regress1/sygus/issue3247.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3247.smt2 b/test/regress/regress1/sygus/issue3247.smt2
new file mode 100644 (file)
index 0000000..6784b87
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3247.smt2
@@ -0,0 +1,23 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-inference --strings-exp
+(set-logic ALL)
+(declare-fun a () String) 
+(declare-fun b () String) 
+(declare-fun c () String)
+(declare-fun d () String)
+(declare-fun f () String)
+(declare-fun e () String)
+(assert
+  (not
+    (=
+      (str.contains
+        c
+        (str.replace d (str.substr b 0 (str.len d)) "A")
+      )
+      (str.contains c "A")
+    )
+  )
+)
+(assert (= a (str.++ c f)))
+(assert (= b (str.++ d e)))
+(check-sat)