From 85d00e88892a16e63e520c0c1bde713352316b79 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Mar 2021 03:40:05 -0600 Subject: [PATCH] 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. --- src/theory/strings/infer_info.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.30.2