Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.

1 files changed, 2 insertions, 6 deletions

diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index f41392eee..715612975 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -33,8 +33,6 @@ protected:
   context::CDO< FirstOrderModel* > d_curr_model;
   //quantifiers engine
   QuantifiersEngine* d_qe;
-  /** get current model value */
-  virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0;
 public:
   QModelBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilder(){}
@@ -50,8 +48,8 @@ public:
   bool d_considerAxioms;
   /** exist instantiation ? */
   virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
-  /** get current model value */
-  Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false );
+  //debug model
+  void debugModel( FirstOrderModel* fm );
 };
 
 
@@ -123,8 +121,6 @@ protected:  //helper functions
 public:
   QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
   virtual ~QModelBuilderIG(){}
-  //debug model
-  void debugModel( FirstOrderModel* fm );
 public:
   //whether to add inst-gen lemmas
   virtual bool optInstGen();