merge from fmf-devel branch. more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

1 files changed, 31 insertions, 11 deletions

diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 344b731e0..1366a7650 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -27,20 +27,29 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-//the model builder
+/** model builder class
+  *  This class is capable of building candidate models based on the current quantified formulas
+  *  that are asserted.  Use:
+  *  (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel
+  *  (2) if candidate model is determined to be a real model,
+           then call ModelEngineBuilder::buildModel( m, true );
+  */
 class ModelEngineBuilder : public TheoryEngineModelBuilder
 {
 protected:
   //quantifiers engine
   QuantifiersEngine* d_qe;
+  //the model we are working with
+  context::CDO< FirstOrderModel* > d_curr_model;
   //map from operators to model preference data
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf
   std::map< Node, bool > d_uf_model_constructed;
+protected:
   /** process build model */
-  void processBuildModel( TheoryModel* m );
+  void processBuildModel( TheoryModel* m, bool fullModel );
   /** choose representative for unconstrained equivalence class */
-  Node chooseRepresentative( TheoryModel* m, Node eqc );
+  Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
   /** bad representative */
   bool isBadRepresentative( Node n );
 protected:
@@ -49,23 +58,30 @@ protected:
   //analyze quantifiers
   void analyzeQuantifiers( FirstOrderModel* fm );
   //build model
-  void finishBuildModel( FirstOrderModel* fm );
+  void constructModel( FirstOrderModel* fm );
   //theory-specific build models
-  void finishBuildModelUf( FirstOrderModel* fm, Node op );
+  void constructModelUf( FirstOrderModel* fm, Node op );
   //do InstGen techniques for quantifier, return number of lemmas produced
   int doInstGen( FirstOrderModel* fm, Node f );
 public:
-  ModelEngineBuilder( QuantifiersEngine* qe );
+  ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
   virtual ~ModelEngineBuilder(){}
-  /** finish model */
-  void finishProcessBuildModel( TheoryModel* m );
-public:
   /** number of lemmas generated while building model */
   int d_addedLemmas;
+  //consider axioms
+  bool d_considerAxioms;
+private:    ///information for InstGen
   //map from quantifiers to if are constant SAT
   std::map< Node, bool > d_quant_sat;
-  //map from quantifiers to the instantiation literals that their model is dependent upon
-  std::map< Node, std::vector< Node > > d_quant_selection_lits;
+  //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;
 public:
   //map from quantifiers to model basis match
   std::map< Node, InstMatch > d_quant_basis_match;
@@ -73,6 +89,8 @@ public:
   bool optUseModel();
   bool optInstGen();
   bool optOneQuantPerRoundInstGen();
+  // set effort
+  void setEffort( int effort );
   /** statistics class */
   class Statistics {
   public:
@@ -82,6 +100,8 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
+  // is quantifier active?
+  bool isQuantifierActive( Node f );
 };/* class ModelEngineBuilder */
 
 }/* CVC4::theory::quantifiers namespace */