diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-04 14:17:55 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-08-04 14:17:55 -0700 |
| commit | 6d87c5719f925a70aaa5f63e7477d10e68701b11 (patch) | |
| tree | ed32d2860689f8d843d30addb0536ea1d173600c | |
| parent | 75f3d9108aebde9ebf8a9b2d82cc7d07be4297e1 (diff) | |
lazy registrationeqNotifyRewrite
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9980beb41..63fb833b3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -918,6 +918,10 @@ void TheoryStrings::checkCodes() cc = Rewriter::rewrite(cc); Assert(cc.isConst()); Node cp = d_termReg.getProxyVariableFor(c); + if (cp.isNull()) { + d_termReg.registerTerm(c, 0); + cp = d_termReg.getProxyVariableFor(c); + } AlwaysAssert(!cp.isNull()); Node vc = nm->mkNode(STRING_TO_CODE, cp); if (!d_state.areEqual(cc, vc)) diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0ad11f30d..1ee6e6adc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -183,7 +183,7 @@ class TheoryStrings : public Theory { void eqNotifyRewrite(TNode t1, TNode t2) override { - d_termReg.registerTerm(t2, 0); + // d_termReg.registerTerm(t2, 0); } private: |