[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 432aa39d0b8baf150da248022242101dbaaba1fd..aabefe74e572141db7810123238f8756a45fabc3 100644 (file)
--- 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