1 files changed, 33 insertions, 4 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index b819b883d..8df5a8535 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -15,9 +15,11 @@
  **/
 
 #include "theory/builtin/theory_builtin.h"
-#include "theory/valuation.h"
+
 #include "expr/kind.h"
+#include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/valuation.h"
 
 using namespace std;
 
@@ -25,6 +27,33 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory */
-}/* CVC4 namespace */
+TheoryBuiltin::TheoryBuiltin(context::Context* c,
+                             context::UserContext* u,
+                             OutputChannel& out,
+                             Valuation valuation,
+                             const LogicInfo& logicInfo)
+    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo)
+{
+}
+
+std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter());
+}
+
+std::string TheoryBuiltin::identify() const
+{
+  return std::string("TheoryBuiltin");
+}
+
+void TheoryBuiltin::finishInit()
+{
+  // choice nodes are not evaluated in getModelValue
+  TheoryModel* theoryModel = d_valuation.getModel();
+  Assert(theoryModel != nullptr);
+  theoryModel->setUnevaluatedKind(kind::CHOICE);
+}
+
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC4