From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 22 Aug 2020 00:55:06 +0000 (-0500)
Subject: Remove unecessary theory model builder base class (#4933)
X-Git-Tag: cvc5-1.0.0~2964
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=413da163bd36c8a9651308d7249e9aaf811872af;p=cvc5.git

Remove unecessary theory model builder base class (#4933)
---

diff --git a/src/smt/model.h b/src/smt/model.h
index 1f7c5daae..8f4409b07 100644
--- 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 caf8bd6b8..0be92c95c 100644
--- 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
    *