Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

1 files changed, 369 insertions, 0 deletions

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
new file mode 100644
index 000000000..4031efdf9
--- /dev/null
+++ b/src/theory/quantifiers/model_engine.h
@@ -0,0 +1,369 @@
+/*********************                                                        */
+/*! \file instantiation_engine.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Instantiation Engine classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MODEL_ENGINE_H
+#define __CVC4__MODEL_ENGINE_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace uf{
+  class StrongSolverTheoryUf;
+}
+
+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
+{
+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 );
+};
+
+
+
+
+class ModelEngine : public QuantifiersModule
+{
+  friend class UfModel;
+  friend class RepAlphabetIterator;
+private:
+  TheoryQuantifiers* d_th;
+  QuantifiersEngine* d_quantEngine;
+  uf::StrongSolverTheoryUf* d_ss;
+  //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:
+  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;
+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 );
+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 );
+public:
+  ModelEngine( TheoryQuantifiers* th );
+  ~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 );
+  void assertNode( Node f );
+  Node explain(TNode n){ return Node::null(); }
+  void propagate( Theory::Effort level ){}
+  void debugPrint( const char* c );
+public:
+  /** statistics class */
+  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;
+    IntStat d_num_quants_init;
+    IntStat d_num_quants_init_fail;
+    Statistics();
+    ~Statistics();
+  };
+  Statistics d_statistics;
+};
+
+}
+}
+}
+
+#endif