diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-08-16 06:58:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-16 13:58:43 +0000 |
| commit | 0711ec521f01888b059d152d1c1f20382d5ce432 (patch) | |
| tree | 1e797fc9c1db49571b6c7aa676b3785d5087eb73 | |
| parent | ba2acc2d22b7718b102bfa7c2a699be5a4d87296 (diff) | |
[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.
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 5 |
1 files 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 |