diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.h')
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 8 |
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(); |