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.

1 files changed, 23 insertions, 9 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 8e68913ac..42dc975fa 100644
--- 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++;
   }