From 0711ec521f01888b059d152d1c1f20382d5ce432 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 16 Aug 2021 06:58:43 -0700 Subject: [PATCH] [Strings] Make fact detection more robust (#7007) Currently, our check for whether an inference is a fact or a lemma involves checking whether the kind of the conclusion is a conjunction or a disjunction. However, this does not take into account inferences of other kinds such as ites, which is a problem because they require a decision from the SAT solver. This commit changes the condition to check the theory of the conclusion. If the conclusion belongs to the theory of strings, it considers it as a fact. --- src/theory/strings/infer_info.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 432aa39d0..aabefe74e 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -17,6 +17,7 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/theory.h" namespace cvc5 { namespace theory { @@ -60,8 +61,8 @@ bool InferInfo::isFact() const // 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(); + return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS + && d_noExplain.empty(); } Node InferInfo::getPremises() const -- 2.30.2