diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-09 15:11:01 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-09 15:11:01 -0500 |
| commit | 9a939deab1a788b29b573ae7fb72a6088a1d7edf (patch) | |
| tree | d403a57bac514c9e1320cdc171597c977b952ee0 /src/theory/strings/term_registry.cpp | |
| parent | 060eedcd5fdb0316d323c4528402034629285b97 (diff) | |
(proof-new) Generalize single step helper in eager proof generator (#5046)
This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 3e6f66b73..080349f73 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -52,7 +52,11 @@ TermRegistry::TermRegistry(SolverState& s, d_proxyVar(s.getUserContext()), d_proxyVarToLength(s.getUserContext()), d_lengthLemmaTermsCache(s.getUserContext()), - d_epg(nullptr) + d_epg(pnm ? new EagerProofGenerator( + pnm, + s.getUserContext(), + "strings::TermRegistry::EagerProofGenerator") + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -282,7 +286,7 @@ void TermRegistry::registerTerm(Node n, int effort) if (d_epg != nullptr) { regTermLem = d_epg->mkTrustNode( - eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {n}); + eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n}); } else { @@ -384,7 +388,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) // it is a simple rewrite to justify this if (d_epg != nullptr) { - return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {ret}); + return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret}); } return TrustNode::mkTrustLemma(ret, nullptr); } @@ -508,7 +512,7 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma( if (d_epg != nullptr) { - return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {n}); + return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n}); } return TrustNode::mkTrustLemma(lenLemma, nullptr); } |