Frontend support for the choice operator (#4175)

Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue

1 files changed, 18 insertions, 12 deletions

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 8a7d1bf7b..6e99ef040 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -25,17 +25,23 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class TheoryBuiltin : public Theory {
-public:
-  TheoryBuiltin(context::Context* c, context::UserContext* u,
-                OutputChannel& out, Valuation valuation,
-                const LogicInfo& logicInfo)
-      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
-  std::string identify() const override { return std::string("TheoryBuiltin"); }
-};/* class TheoryBuiltin */
-
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+class TheoryBuiltin : public Theory
+{
+ public:
+  TheoryBuiltin(context::Context* c,
+                context::UserContext* u,
+                OutputChannel& out,
+                Valuation valuation,
+                const LogicInfo& logicInfo);
+
+  std::string identify() const override;
+
+  /** finish initialization */
+  void finishInit() override;
+}; /* class TheoryBuiltin */
+
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */