diff options
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index c9a2bcd70..2b5338a6a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -16,6 +16,7 @@ #include "expr/kind.h" #include "options/strings_options.h" +#include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings.h" #include "theory/strings/theory_strings_rewriter.h" @@ -625,6 +626,17 @@ void InferenceManager::explain(TNode literal, } } } +void InferenceManager::setIncomplete() { d_out.setIncomplete(); } + +void InferenceManager::markCongruent(Node a, Node b) +{ + Assert(a.getKind() == b.getKind()); + ExtTheory* eth = d_parent.getExtTheory(); + if (eth->hasFunctionKind(a.getKind())) + { + eth->markCongruent(a, b); + } +} } // namespace strings } // namespace theory |