merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

1 files changed, 71 insertions, 295 deletions

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index cf6691918..b01139826 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Instantiation Engine classes
+ ** \brief Model Engine classes
  **/
 
 #include "cvc4_private.h"
@@ -21,6 +21,9 @@
 
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
@@ -31,312 +34,87 @@ namespace uf{
 
 namespace quantifiers {
 
-/** this class stores a representative alphabet */
-class RepAlphabet {
-public:
-  RepAlphabet(){}
-  RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe );
-  ~RepAlphabet(){}
-  std::map< TypeNode, std::vector< Node > > d_type_reps;
-  std::map< Node, int > d_tmap;
-  /** clear the alphabet */
-  void clear(){
-    d_type_reps.clear();
-    d_tmap.clear();
-  }
-  /** set the representatives for type */
-  void set( TypeNode t, std::vector< Node >& reps );
-  /** returns index in d_type_reps for node n */
-  int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }
-  /** debug print */
-  void debugPrint( const char* c, QuantifiersEngine* qe );
-};
-
-class ModelEngine;
-
-/** this class iterates over a RepAlphabet */
-class RepAlphabetIterator {
-private:
-  void initialize( QuantifiersEngine* qe, Node f, ModelEngine* model );
-public:
-  RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model );
-  RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder );
-  ~RepAlphabetIterator(){}
-  //pointer to quantifier
-  Node d_f;
-  //pointer to model
-  ModelEngine* d_model;
-  //index we are considering
-  std::vector< int > d_index;
-  //ordering for variables we are indexing over
-  //  for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
-  //    then we consider instantiations in this order:
-  //      a/x a/y a/z
-  //      a/x b/y a/z
-  //      b/x a/y a/z
-  //      b/x b/y a/z
-  //      ...
-  std::vector< int > d_index_order;
-  //variables to index they are considered at
-  //  for example, if d_index_order = { 2, 0, 1 }
-  //    then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
-  std::map< int, int > d_var_order;
-  //the instantiation constants of d_f
-  std::vector< Node > d_ic;
-  //the current terms we are considering
-  std::vector< Node > d_terms;
-public:
-  /** increment the iterator */
-  void increment2( QuantifiersEngine* qe, int counter ); 
-  void increment( QuantifiersEngine* qe );
-  /** is the iterator finished? */
-  bool isFinished();
-  /** produce the match that this iterator represents */
-  void getMatch( QuantifiersEngine* qe, InstMatch& m );
-  /** get the i_th term we are considering */
-  Node getTerm( int i );
-  /** get the number of terms we are considering */
-  int getNumTerms() { return d_f[0].getNumChildren(); }
-  /** refresh d_term to be current with d_index */
-  void calculateTerms( QuantifiersEngine* qe );
-  /** debug print */
-  void debugPrint( const char* c );
-  void debugPrintSmall( const char* c );
-  //for debugging
-  int d_inst_tried;
-  int d_inst_tests;
-};
-
-
-class UfModelTree
-{
-public:
-  UfModelTree(){}
-  /** the data */
-  std::map< Node, UfModelTree > d_data;
-  /** the value of this tree node (if all paths lead to same value) */
-  Node d_value;
-public:
-  //is this model tree empty?
-  bool isEmpty() { return d_data.empty(); }
-  //clear
-  void clear(){
-    d_data.clear();
-    d_value = Node::null();
-  }
-  /** setValue function
-    *
-    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false
-    *
-    */
-  void setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
-  /**  getValue function
-    *
-    *  returns $val, the value of ground term n
-    *  Say n is f( t_0...t_n )
-    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to $val
-    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
-    *      then g( a, a, a ) would return b with depIndex = 1
-    *  If ground = true, we are asking whether the term n is constant (assumes that all non-model basis arguments are ground)
-    *
-    */
-  Node getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
-  ///** getConstant Value function
-  //  *
-  //  * given term n, where n may contain model basis arguments
-  //  * if n is constant for its entire domain, then this function returns the value of its domain
-  //  * otherwise, it returns null
-  //  * for example, if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
-  //  *   then f( a, e ) would return b, while f( e, a ) would return null
-  //  *
-  //  */
-  Node getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex );
-  /** simplify function */
-  void simplify( Node op, Node defaultVal, int argIndex );
-  // is total ?
-  bool isTotal( Node op, int argIndex );
-public:
-  void debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );
-};
 
-class UfModelTreeOrdered
+//the model builder
+class ModelEngineBuilder : public TheoryEngineModelBuilder
 {
-private:
-  Node d_op;
-  std::vector< int > d_index_order;
-  UfModelTree d_tree;
-public:
-  UfModelTreeOrdered(){}
-  UfModelTreeOrdered( Node op ) : d_op( op ){
-    TypeNode tn = d_op.getType();
-    for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){
-      d_index_order.push_back( i );
-    }
-  }
-  UfModelTreeOrdered( Node op, std::vector< int >& indexOrder ) : d_op( op ){
-    d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
-  }
-  bool isEmpty() { return d_tree.isEmpty(); }
-  void clear() { d_tree.clear(); }
-  void setValue( QuantifiersEngine* qe, Node n, Node v, bool ground = true ){
-    d_tree.setValue( qe, n, v, d_index_order, ground, 0 );
-  }
-  Node getValue( QuantifiersEngine* qe, Node n, int& depIndex ){
-    return d_tree.getValue( qe, n, d_index_order, depIndex, 0 );
-  }
-  Node getConstantValue( QuantifiersEngine* qe, Node n ) { 
-    return d_tree.getConstantValue( qe, n, d_index_order, 0 ); 
-  }
-  void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
-  bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
-public:
-  void debugPrint( const char* c, QuantifiersEngine* qe, int ind = 0 ){
-    d_tree.debugPrint( c, qe, d_index_order, ind );
-  }
-};
-
-class UfModel
-{
-//public:
-  //std::map< Node, std::vector< Node > > d_reqs[2];
-  //std::map< Node, std::map< Node, std::vector< Node > > > d_eq_reqs[2];
-  ///** add requirement */
-  //void addRequirement( Node f, Node p, bool phase ) { d_reqs[ phase ? 1 : 0 ][ f ].push_back( p ); }
-  ///** add equality requirement */
-  //void addEqRequirement( Node f, Node t, Node te, bool phase ) { d_eq_reqs[ phase ? 1 : 0 ][ f ][ t ].push_back( te ); }
-private:
-  Node d_op;
-  ModelEngine* d_me;
-  std::vector< Node > d_ground_asserts;
-  std::vector< Node > d_ground_asserts_reps;
-  bool d_model_constructed;
-  //store for set values
-  std::map< Node, Node > d_set_values[2];
-  // preferences for default values
-  std::vector< Node > d_values;
-  std::map< Node, std::vector< Node > > d_value_pro_con[2];
-  /** set value */
-  void setValue( Node n, Node v, bool ground = true );
-  /** set model */
-  void setModel();
-  /** clear model */
-  void clearModel();
-public:
-  UfModel(){}
-  UfModel( Node op, ModelEngine* qe );
-  ~UfModel(){}
-  //data structure that stores the model
-  UfModelTreeOrdered d_tree;
-  //quantifiers that are satisfied because of the constant definition of d_op
-  bool d_reconsider_model;
-public:
-  /** debug print */
-  void debugPrint( const char* c );
-  /** get constant value */
-  Node getConstantValue( QuantifiersEngine* qe, Node n );
-  /** is empty */
-  bool isEmpty() { return d_ground_asserts.empty(); }
-  /** is constant */
-  bool isConstant();
-public:
-  /** build model */
-  void buildModel();
-  /** make model */
-  void makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree );
-public:
-  /** set value preference */
-  void setValuePreference( Node f, Node n, bool isPro );
+protected:
+  //quantifiers engine
+  QuantifiersEngine* d_qe;
+  //map from operators to model preference data
+  std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
+  /** choose representative */
+  Node chooseRepresentative( TheoryModel* tm, Node eqc );
+  /** use constants for representatives */
+  void processBuildModel( TheoryModel* m );
+  //analyze quantifiers
+  void analyzeQuantifiers( FirstOrderModel* fm );
+  //build model
+  void finishBuildModel( FirstOrderModel* fm );
+  //theory-specific build models
+  void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model );
+  //do InstGen techniques for quantifier, return number of lemmas produced
+  int doInstGen( FirstOrderModel* fm, Node f );
+public:
+  ModelEngineBuilder( QuantifiersEngine* qe );
+  virtual ~ModelEngineBuilder(){}
+public:
+  /** number of lemmas generated while building model */
+  int d_addedLemmas;
+  //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;
+public:
+  //map from quantifiers to model basis match
+  std::map< Node, InstMatch > d_quant_basis_match;
+  //options
+  bool optUseModel();
+  bool optInstGen();
+  bool optOneQuantPerRoundInstGen();
+  /** statistics class */
+  class Statistics {
+  public:
+    IntStat d_pre_sat_quant;
+    IntStat d_pre_nsat_quant;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
 };
 
-
-
-
 class ModelEngine : public QuantifiersModule
 {
-  friend class UfModel;
-  friend class RepAlphabetIterator;
+  friend class uf::UfModel;
+  friend class RepSetIterator;
 private:
-  TheoryQuantifiers* d_th;
-  QuantifiersEngine* d_quantEngine;
-  uf::StrongSolverTheoryUf* d_ss;
+  /** builder class */
+  ModelEngineBuilder d_builder;
+private:    //data maintained globally:
   //which quantifiers have been initialized
   std::map< Node, bool > d_quant_init;
-  //map from ops to model basis terms
-  std::map< Node, Node > d_model_basis_term;
-  //map from instantiation terms to their model basis equivalent
-  std::map< Node, Node > d_model_basis;
-  //the model we are working with
-  RepAlphabet d_ra;
-  std::map< Node, UfModel > d_uf_model;
-  ////map from model basis terms to quantifiers that are pro/con their definition
-  //std::map< Node, std::vector< Node > > d_quant_pro_con[2];
-  //map from quantifiers to model basis terms that are pro the definition of
-  std::map< Node, std::vector< Node > > d_pro_con_quant[2];
-  //map from quantifiers to if are constant SAT
-  std::map< Node, bool > d_quant_sat;
+private:    //analysis of current model:
+  //relevant domain
+  RelevantDomain d_rel_domain;
 private:
-  int evaluate( RepAlphabetIterator* rai, Node n, int& depIndex );
-  int evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps );
-  Node evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps );
-  //temporary storing which literals have failed
-  void clearEvalFailed( int index );
-  std::map< Node, bool > d_eval_failed;
-  std::map< int, std::vector< Node > > d_eval_failed_lits;
-  ////temporary storing for values/free variable dependencies
-  //std::map< Node, Node > d_eval_term_vals;
-  //std::map< Node, std::map< Node, std::vector< Node > > > d_eval_term_fv_deps;
+  //options
+  bool optOneInstPerQuantRound();
+  bool optUseRelevantDomain();
+  bool optOneQuantPerRound();
 private:
-  //map from terms to the models used to calculate their value
-  std::map< Node, UfModelTreeOrdered > d_eval_term_model;
-  std::map< Node, bool > d_eval_term_use_default_model;
-  void makeEvalTermModel( Node n );
-  //index ordering to use for each term
-  std::map< Node, std::vector< int > > d_eval_term_index_order;
-  int getMaxVariableNum( int n );
-  void makeEvalTermIndexOrder( Node n );
-public:
-  void increment( RepAlphabetIterator* rai );
+  //initialize quantifiers, return number of lemmas produced
+  int initializeQuantifier( Node f );
+  //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
+  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
 private:
-  //queries about equality
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-private:
-  bool useModel();
-private:
-  //initialize quantifiers, return false if lemma needed to be added
-  bool initializeQuantifier( Node f );
-  //build representatives
-  void buildRepresentatives();
-  //initialize model
-  void initializeModel();
-  //analyze quantifiers
-  void analyzeQuantifiers();
-  //instantiate quantifier, return number of lemmas produced
-  int instantiateQuantifier( Node f );
-private:
-  //register instantiation terms with their corresponding model basis terms
-  void registerModelBasis( Node n, Node gn );
-  //for building UF model
-  void initializeUf( Node n );
-  void collectUfTerms( Node n, std::vector< Node >& terms );
-  void initializeUfModel( Node op );
-  //void processPredicate( Node f, Node p, bool phase );
-  //void processEquality( Node f, Node eq, bool phase );
+  //temporary statistics
+  int d_triedLemmas;
+  int d_testLemmas;
+  int d_totalLemmas;
+  int d_relevantLemmas;
 public:
-  ModelEngine( TheoryQuantifiers* th );
+  ModelEngine( QuantifiersEngine* qe );
   ~ModelEngine(){}
-  //get quantifiers engine
-  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  //get representatives
-  RepAlphabet* getReps() { return &d_ra; }
-  //get arbitrary element
-  Node getArbitraryElement( TypeNode tn, std::vector< Node >& exclude );
-  //get model basis term
-  Node getModelBasisTerm( TypeNode tn, int i = 0 );
-  //get model basis term for op
-  Node getModelBasisApplyUfTerm( Node op );
-  //is model basis term for op
-  bool isModelBasisTerm( Node op, Node n );
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );
@@ -349,8 +127,6 @@ public:
   class Statistics {
   public:
     IntStat d_inst_rounds;
-    IntStat d_pre_sat_quant;
-    IntStat d_pre_nsat_quant;
     IntStat d_eval_formulas;
     IntStat d_eval_eqs;
     IntStat d_eval_uf_terms;