From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Mar 2021 09:40:05 +0000 (-0600)
Subject: Do not process conjunctions as facts in strings (#6065)
X-Git-Tag: cvc5-1.0.0~2142
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=85d00e88892a16e63e520c0c1bde713352316b79;p=cvc5.git

Do not process conjunctions as facts in strings (#6065)

This changes things so we process inferences with AND conclusions as lemmas always.

This fixes #6056, that benchmark times out.
---

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 6d87aa944..dc0cc0cfd 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -56,7 +56,11 @@ bool InferInfo::isFact() const
 {
   Assert(!d_conc.isNull());
   TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc;
-  return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
+  // we could process inferences with conjunctive conclusions as facts, where
+  // the explanation is copied. However, for simplicity, we always send these
+  // as lemmas. This case happens very infrequently.
+  return !atom.isConst() && atom.getKind() != kind::OR
+         && atom.getKind() != kind::AND && d_noExplain.empty();
 }
 
 Node InferInfo::getPremises() const