From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 16 Aug 2021 13:58:43 +0000 (-0700)
Subject: [Strings] Make fact detection more robust (#7007)
X-Git-Tag: cvc5-1.0.0~1385
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0711ec521f01888b059d152d1c1f20382d5ce432;p=cvc5.git

[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.
---

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