Remove unecessary theory model builder base class (#4933)

diff --git a/src/smt/model.h b/src/smt/model.h
index 1f7c5daae3d0c97587328a69698b2f16a33e8691..8f4409b07731e1b15f60358b243c8ff530bad023 100644 (file)
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -119,13 +119,6 @@ class Model {
   bool d_isKnownSat;
 };/* class Model */
 
-class ModelBuilder {
-public:
-  ModelBuilder() { }
-  virtual ~ModelBuilder() { }
-  virtual bool buildModel(Model* m) = 0;
-};/* class ModelBuilder */
-
 }/* CVC4 namespace */
 
 #endif  /* CVC4__MODEL_H */

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index caf8bd6b828a9a3af8ddc9326a46e9566d62e693..0be92c95c8b6934e10e7fb71766516470e61f302 100644 (file)
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -38,7 +38,7 @@ namespace theory {
  * this will set up the data structures in TheoryModel to represent
  * a model for the current set of assertions.
  */
-class TheoryEngineModelBuilder : public ModelBuilder
+class TheoryEngineModelBuilder
 {
   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
@@ -67,7 +67,7 @@ class TheoryEngineModelBuilder : public ModelBuilder
    * builder in steps (2) or (5), for instance, if the model we
    * are building fails to satisfy a quantified formula.
    */
-  bool buildModel(Model* m) override;
+  bool buildModel(Model* m);
 
   /** postprocess model
    *