diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/bv | |
parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2041b0805..107cb9672 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -187,6 +187,16 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) { Unreachable(); } +void TheoryBV::finishInit() +{ + // these kinds are semi-evaluated in getModelValue (applications of this + // kind are treated as variables) + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV); + tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM); +} + Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 13469d562..603823ff0 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -66,6 +66,8 @@ public: void setMasterEqualityEngine(eq::EqualityEngine* eq) override; + void finishInit() override; + Node expandDefinition(LogicRequest& logicRequest, Node node) override; void preRegisterTerm(TNode n) override; |