1 files changed, 0 insertions, 157 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index b34f1e580..b73716169 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -56,163 +56,6 @@ public:
   unsigned getNumTriedLemmas() { return d_triedLemmas; }
 };
 
-class TermArgBasisTrie {
-public:
-  /** the data */
-  std::map< Node, TermArgBasisTrie > d_data;
-  /** add term to the trie */
-  bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0);
-};/* class TermArgBasisTrie */
-
-/** model builder class
-  *  This class is capable of building candidate models based on the current quantified formulas
-  *  that are asserted.  Use:
-  *  (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
-  *  (2) if candidate model is determined to be a real model,
-           then call QModelBuilder::buildModel( m, true );
-  */
-class QModelBuilderIG : public QModelBuilder
-{
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-
- protected:
-  /**
-   * This class stores temporary information useful to model engine for
-   * constructing models for uninterpreted functions.
-   */
-  class UfModelPreferenceData
-  {
-   public:
-    UfModelPreferenceData() {}
-    virtual ~UfModelPreferenceData() {}
-    /** any constant value of the type */
-    Node d_const_val;
-    /** list of possible default values */
-    std::vector<Node> d_values;
-    /**
-     * Map from values to the set of quantified formulas that are (pro, con)
-     * that value. A quantified formula may be "pro" a particular default
-     * value of an uninterpreted function if that value is likely to satisfy
-     * many points in its domain. For example, forall x. P( f( x ) ) may be
-     * "pro" the default value true for P.
-     */
-    std::map<Node, std::vector<Node> > d_value_pro_con[2];
-    /** set that quantified formula q is pro/con the default value of r */
-    void setValuePreference(Node q, Node r, bool isPro);
-    /** get best default value */
-    Node getBestDefaultValue(Node defaultTerm, TheoryModel* m);
-  };
-  /** map from operators to model preference data */
-  std::map<Node, UfModelPreferenceData> d_uf_prefs;
-  //built model uf
-  std::map< Node, bool > d_uf_model_constructed;
-  //whether inst gen was done
-  bool d_didInstGen;
-  /** process build model */
-  bool processBuildModel(TheoryModel* m) override;
-
- protected:
-  //reset
-  virtual void reset( FirstOrderModel* fm ) = 0;
-  //initialize quantifiers, return number of lemmas produced
-  virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm);
-  //analyze model
-  virtual void analyzeModel( FirstOrderModel* fm );
-  //analyze quantifiers
-  virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0;
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
-  //theory-specific build models
-  virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
-
- protected:
-  //map from quantifiers to if are SAT
-  //std::map< Node, bool > d_quant_sat;
-  //which quantifiers have been initialized
-  std::map< Node, bool > d_quant_basis_match_added;
-  //map from quantifiers to model basis match
-  std::map< Node, InstMatch > d_quant_basis_match;
-
- protected:  // helper functions
-  /** term has constant definition */
-  bool hasConstantDefinition( Node n );
-
- public:
-  QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
-
- public:
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_num_quants_init;
-    IntStat d_num_partial_quants_init;
-    IntStat d_init_inst_gen_lemmas;
-    IntStat d_inst_gen_lemmas;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
-  // is term selected
-  virtual bool isTermSelected( Node n ) { return false; }
-  /** quantifier has inst-gen definition */
-  virtual bool hasInstGen( Node f ) = 0;
-  /** did inst gen this round? */
-  bool didInstGen() { return d_didInstGen; }
-  // is quantifier active?
-  bool isQuantifierActive( Node f );
-  //do exhaustive instantiation
-  int doExhaustiveInstantiation(FirstOrderModel* fm,
-                                Node f,
-                                int effort) override;
-
-  //temporary stats
-  int d_numQuantSat;
-  int d_numQuantInstGen;
-  int d_numQuantNoInstGen;
-  int d_numQuantNoSelForm;
-  //temporary stat
-  int d_instGenMatches;
-};/* class QModelBuilder */
-
-
-class QModelBuilderDefault : public QModelBuilderIG
-{
- private:  /// information for (old) InstGen
-  // map from quantifiers to their selection literals
-  std::map< Node, Node > d_quant_selection_lit;
-  std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
-  //map from quantifiers to their selection literal terms
-  std::map< Node, std::vector< Node > > d_quant_selection_lit_terms;
-  //map from terms to the selection literals they exist in
-  std::map< Node, Node > d_term_selection_lit;
-  //map from operators to terms that appear in selection literals
-  std::map< Node, std::vector< Node > > d_op_selection_terms;
-  //get selection score
-  int getSelectionScore( std::vector< Node >& uf_terms );
-
- protected:
-  //reset
-  void reset(FirstOrderModel* fm) override;
-  //analyze quantifier
-  void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
-  //do InstGen techniques for quantifier, return number of lemmas produced
-  int doInstGen(FirstOrderModel* fm, Node f) override;
-  //theory-specific build models
-  void constructModelUf(FirstOrderModel* fm, Node op) override;
-
- protected:
-  std::map< Node, QuantPhaseReq > d_phase_reqs;
-
- public:
-  QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
-
-  //has inst gen
-  bool hasInstGen(Node f) override
-  {
-    return !d_quant_selection_lit[f].isNull();
-  }
-};
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */