summaryrefslogtreecommitdiff
path: root/src/theory/bv/theory_bv.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-23 15:44:50 -0500
committerGitHub <noreply@github.com>2018-05-23 15:44:50 -0500
commita96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch)
treea3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/bv/theory_bv.h
parent4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff)
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r--src/theory/bv/theory_bv.h2
1 files changed, 2 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback