diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-15 06:06:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-15 06:06:28 -0500 |
| commit | 3b230077d51c8445328f0b5d5ff94bbd988d1c83 (patch) | |
| tree | 70d9eb305857c3c36d71cf42382bee7a6633b908 /src/theory/strings/theory_strings.cpp | |
| parent | 42cd0a7bcbe993870d76d8cc9db7acc0a9ae70f9 (diff) | |
(proof-new) Add the strings proof checker (#4858)
It also adds enumeration for two new rules that have been recently added.
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 54c4759a8..142b0006b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -97,6 +97,13 @@ TheoryStrings::TheoryStrings(context::Context* c, d_false = NodeManager::currentNM()->mkConst( false ); d_cardSize = utils::getAlphabetCardinality(); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_sProofChecker.registerTo(pc); + } } TheoryStrings::~TheoryStrings() { |