Reinstantiate support for conjunctions in facts (#4377)

Fixes #4376. Commit 6255c0356bd78140a9cf075491c1d4608ac27704 removed
support for conjunctions in the conclusion of facts. However,
`F_ENDPOINT_EMP` generates a conjunction in the conclusion of the
inference if multiple components are inferred to be empty. This commit
reinstantiates support for conjunctions in the conclusion of facts.

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 8e68913ac4301a6c5f6a234da9956a791efde4e0..42dc975fae602a066a4312b579d51ea337266f7f 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -279,24 +279,38 @@ void InferenceManager::doPendingFacts()
     // should be added as a normal equality or predicate to the equality engine
     // with no new external assumptions (ii.d_antn).
     Assert(ii.isFact());
-    Node fact = ii.d_conc;
+    Node facts = ii.d_conc;
     Node exp = utils::mkAnd(ii.d_ant);
-    Trace("strings-assert") << "(assert (=> " << exp << " " << fact
+    Trace("strings-assert") << "(assert (=> " << exp << " " << facts
                             << ")) ; fact " << ii.d_id << std::endl;
     // only keep stats if we process it here
-    Trace("strings-lemma") << "Strings::Fact: " << fact << " from " << exp
+    Trace("strings-lemma") << "Strings::Fact: " << facts << " from " << exp
                            << " by " << ii.d_id << std::endl;
     d_statistics.d_inferences << ii.d_id;
     // assert it as a pending fact
-    bool polarity = fact.getKind() != NOT;
-    TNode atom = polarity ? fact : fact[0];
-    // no double negation or double (conjunctive) conclusions
-    Assert(atom.getKind() != NOT && atom.getKind() != AND);
-    assertPendingFact(atom, polarity, exp);
+    if (facts.getKind() == AND)
+    {
+      for (const Node& fact : facts)
+      {
+        bool polarity = fact.getKind() != NOT;
+        TNode atom = polarity ? fact : fact[0];
+        // no double negation or double (conjunctive) conclusions
+        Assert(atom.getKind() != NOT && atom.getKind() != AND);
+        assertPendingFact(atom, polarity, exp);
+      }
+    }
+    else
+    {
+      bool polarity = facts.getKind() != NOT;
+      TNode atom = polarity ? facts : facts[0];
+      // no double negation or double (conjunctive) conclusions
+      Assert(atom.getKind() != NOT && atom.getKind() != AND);
+      assertPendingFact(atom, polarity, exp);
+    }
     // Must reference count the equality and its explanation, which is not done
     // by the equality engine. Notice that we do not need to do this for
     // external assertions, which enter as facts through sendAssumption.
-    d_keep.insert(fact);
+    d_keep.insert(facts);
     d_keep.insert(exp);
     i++;
   }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2b24767d6de6e4727b13ec33eca1c08a35222aa9..ac96110ceb5944f4f641c99becb5af187f117b25 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -947,6 +947,7 @@ set(regress_0_tests
   regress0/strings/issue3497.smt2
   regress0/strings/issue3657-evalLeq.smt2
   regress0/strings/issue4070.smt2
+  regress0/strings/issue4376.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/strings/issue4376.smt2 b/test/regress/regress0/strings/issue4376.smt2
new file mode 100644 (file)
index 0000000..f6dd880
--- /dev/null
+++ b/test/regress/regress0/strings/issue4376.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp --strings-eager
+(set-info :status sat)
+(set-logic QF_SLIA)
+(declare-const i0 Int)
+(declare-const Str1 String)
+(declare-const Str9 String)
+(declare-const Str11 String)
+(declare-const Str15 String)
+(assert (= (str.++ Str1 "ijruldtzyp") Str15))
+(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (int.to.str i0)) Str15 Str9))
+(check-sat)