Add notions of evaluated kinds in TheoryModel (#1947)

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;