Minor cleanup after today's commits:

* change some uses of "std::cout" to "Message()"

* change some files to use Unix newlines instead of DOS newlines

* fix compiler warning

8 files changed, 1382 insertions, 1382 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 766bd31ae..1c6b47867 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -1,184 +1,184 @@
-/*********************                                                        */

-/*! \file first_order_model.cpp

- ** \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 Implementation of model engine model class

- **/

-

-#include "theory/quantifiers/first_order_model.h"

-#include "theory/quantifiers/rep_set_iterator.h"

-#include "theory/quantifiers/model_engine.h"

-#include "theory/quantifiers/term_database.h"

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-

-FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),

-d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){

-

-}

-

-void FirstOrderModel::reset(){

-  //rebuild models

-  d_uf_model_tree.clear();

-  d_uf_model_gen.clear();

-  d_array_model.clear();

-  DefaultModel::reset();

-}

-

-void FirstOrderModel::addTerm( Node n ){

-  //std::vector< Node > added;

-  //d_term_db->addTerm( n, added, false );

-  DefaultModel::addTerm( n );

-}

-

-void FirstOrderModel::initialize(){

-  //this is called after representatives have been chosen and the equality engine has been built

-  //for each quantifier, collect all operators we care about

-  for( int i=0; i<getNumAssertedQuantifiers(); i++ ){

-    Node f = getAssertedQuantifier( i );

-    //initialize relevant models within bodies of all quantifiers

-    initializeModelForTerm( f[1] );

-  }

-  //for debugging

-  if( Options::current()->printModelEngine ){

-    for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){

-      if( it->first.isSort() ){

-        Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;

-      }

-    }

-  }

-}

-

-void FirstOrderModel::initializeModelForTerm( Node n ){

-  if( n.getKind()==APPLY_UF ){

-    Node op = n.getOperator();

-    if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){

-      TypeNode tn = op.getType();

-      tn = tn[ (int)tn.getNumChildren()-1 ];

-      //only generate models for predicates and functions with uninterpreted range types

-      if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){

-        d_uf_model_tree[ op ] = uf::UfModelTree( op );

-        d_uf_model_gen[ op ].clear();

-      }

-    }

-  }

-  /*

-  if( n.getType().isArray() ){

-    while( n.getKind()==STORE ){

-      n = n[0];

-    }

-    Node nn = getRepresentative( n );

-    if( d_array_model.find( nn )==d_array_model.end() ){

-      d_array_model[nn] = arrays::ArrayModel( nn, this );

-    }

-  }

-  */

-  for( int i=0; i<(int)n.getNumChildren(); i++ ){

-    initializeModelForTerm( n[i] );

-  }

-}

-

-void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){

-  /*

-  if( d_uf_model.find( n )!=d_uf_model.end() ){

-    //d_uf_model[n].toStream( out );

-    Node value = d_uf_model[n].getFunctionValue();

-    out << "(" << n << " " << value << ")";

-  }else if( d_array_model.find( n )!=d_array_model.end() ){

-    Node value = d_array_model[n].getArrayValue();

-    out << "(" << n << " " << value << ")" << std::endl;

-  }

-  */

-  DefaultModel::toStreamFunction( n, out );

-}

-

-void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){

-  DefaultModel::toStreamType( tn, out );

-}

-

-Node FirstOrderModel::getInterpretedValue( TNode n ){

-  Debug("fo-model") << "get interpreted value " << n << std::endl;

-  TypeNode type = n.getType();

-  if( type.isFunction() || type.isPredicate() ){

-    if( d_uf_models.find( n )==d_uf_models.end() ){

-      //use the model tree to generate the model

-      Node fn = d_uf_model_tree[n].getFunctionValue();

-      d_uf_models[n] = fn;

-      return fn;

-    }

-  /*

-  }else if( type.isArray() ){

-    if( d_array_model.find( n )!=d_array_model.end() ){

-      return d_array_model[n].getArrayValue();

-    }else{

-      //std::cout << "no array model generated for " << n << std::endl;

-    }

-  */

-  }else if( n.getKind()==APPLY_UF ){

-    Node op = n.getOperator();

-    if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){

-      //consult the uf model

-      int depIndex;

-      return d_uf_model_tree[ op ].getValue( this, n, depIndex );

-    }

-  }else if( n.getKind()==SELECT ){

-

-  }

-  return DefaultModel::getInterpretedValue( n );

-}

-

-TermDb* FirstOrderModel::getTermDatabase(){

-  return d_term_db;

-}

-

-

-void FirstOrderModel::toStream(std::ostream& out){

-  DefaultModel::toStream( out );

-#if 0

-  out << "---Current Model---" << std::endl;

-  out << "Representatives: " << std::endl;

-  d_rep_set.toStream( out );

-  out << "Functions: " << std::endl;

-  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){

-    it->second.toStream( out );

-    out << std::endl;

-  }

-#elif 0

-  d_rep_set.toStream( out );

-  //print everything not related to UF in equality engine

-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );

-  while( !eqcs_i.isFinished() ){

-    Node eqc = (*eqcs_i);

-    Node rep = getRepresentative( eqc );

-    TypeNode type = rep.getType();

-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );

-    while( !eqc_i.isFinished() ){

-      //do not print things that have interpretations in model

-      if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){

-        out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;

-      }

-      ++eqc_i;

-    }

-    ++eqcs_i;

-  }

-  //print functions

-  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){

-    it->second.toStream( out );

-    out << std::endl;

-  }

-#endif

+/*********************                                                        */
+/*! \file first_order_model.cpp
+ ** \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 Implementation of model engine model class
+ **/
+
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/rep_set_iterator.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),
+d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
+
+}
+
+void FirstOrderModel::reset(){
+  //rebuild models
+  d_uf_model_tree.clear();
+  d_uf_model_gen.clear();
+  d_array_model.clear();
+  DefaultModel::reset();
+}
+
+void FirstOrderModel::addTerm( Node n ){
+  //std::vector< Node > added;
+  //d_term_db->addTerm( n, added, false );
+  DefaultModel::addTerm( n );
+}
+
+void FirstOrderModel::initialize(){
+  //this is called after representatives have been chosen and the equality engine has been built
+  //for each quantifier, collect all operators we care about
+  for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
+    Node f = getAssertedQuantifier( i );
+    //initialize relevant models within bodies of all quantifiers
+    initializeModelForTerm( f[1] );
+  }
+  //for debugging
+  if( Options::current()->printModelEngine ){
+    for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
+      if( it->first.isSort() ){
+        Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      }
+    }
+  }
+}
+
+void FirstOrderModel::initializeModelForTerm( Node n ){
+  if( n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
+      TypeNode tn = op.getType();
+      tn = tn[ (int)tn.getNumChildren()-1 ];
+      //only generate models for predicates and functions with uninterpreted range types
+      if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
+        d_uf_model_tree[ op ] = uf::UfModelTree( op );
+        d_uf_model_gen[ op ].clear();
+      }
+    }
+  }
+  /*
+  if( n.getType().isArray() ){
+    while( n.getKind()==STORE ){
+      n = n[0];
+    }
+    Node nn = getRepresentative( n );
+    if( d_array_model.find( nn )==d_array_model.end() ){
+      d_array_model[nn] = arrays::ArrayModel( nn, this );
+    }
+  }
+  */
+  for( int i=0; i<(int)n.getNumChildren(); i++ ){
+    initializeModelForTerm( n[i] );
+  }
+}
+
+void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){
+  /*
+  if( d_uf_model.find( n )!=d_uf_model.end() ){
+    //d_uf_model[n].toStream( out );
+    Node value = d_uf_model[n].getFunctionValue();
+    out << "(" << n << " " << value << ")";
+  }else if( d_array_model.find( n )!=d_array_model.end() ){
+    Node value = d_array_model[n].getArrayValue();
+    out << "(" << n << " " << value << ")" << std::endl;
+  }
+  */
+  DefaultModel::toStreamFunction( n, out );
+}
+
+void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
+  DefaultModel::toStreamType( tn, out );
+}
+
+Node FirstOrderModel::getInterpretedValue( TNode n ){
+  Debug("fo-model") << "get interpreted value " << n << std::endl;
+  TypeNode type = n.getType();
+  if( type.isFunction() || type.isPredicate() ){
+    if( d_uf_models.find( n )==d_uf_models.end() ){
+      //use the model tree to generate the model
+      Node fn = d_uf_model_tree[n].getFunctionValue();
+      d_uf_models[n] = fn;
+      return fn;
+    }
+  /*
+  }else if( type.isArray() ){
+    if( d_array_model.find( n )!=d_array_model.end() ){
+      return d_array_model[n].getArrayValue();
+    }else{
+      //std::cout << "no array model generated for " << n << std::endl;
+    }
+  */
+  }else if( n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
+      //consult the uf model
+      int depIndex;
+      return d_uf_model_tree[ op ].getValue( this, n, depIndex );
+    }
+  }else if( n.getKind()==SELECT ){
+
+  }
+  return DefaultModel::getInterpretedValue( n );
+}
+
+TermDb* FirstOrderModel::getTermDatabase(){
+  return d_term_db;
+}
+
+
+void FirstOrderModel::toStream(std::ostream& out){
+  DefaultModel::toStream( out );
+#if 0
+  out << "---Current Model---" << std::endl;
+  out << "Representatives: " << std::endl;
+  d_rep_set.toStream( out );
+  out << "Functions: " << std::endl;
+  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
+    it->second.toStream( out );
+    out << std::endl;
+  }
+#elif 0
+  d_rep_set.toStream( out );
+  //print everything not related to UF in equality engine
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    Node rep = getRepresentative( eqc );
+    TypeNode type = rep.getType();
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      //do not print things that have interpretations in model
+      if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){
+        out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
+      }
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+  //print functions
+  for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
+    it->second.toStream( out );
+    out << std::endl;
+  }
+#endif
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 825518ed0..afa8dab79 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -1,89 +1,89 @@
-/*********************                                                        */

-/*! \file first_order_model.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 Model extended classes

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__FIRST_ORDER_MODEL_H

-#define __CVC4__FIRST_ORDER_MODEL_H

-

-#include "theory/model.h"

-#include "theory/uf/theory_uf_model.h"

-#include "theory/arrays/theory_arrays_model.h"

-

-namespace CVC4 {

-namespace theory {

-

-struct ModelBasisAttributeId {};

-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;

-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,

-//                    0 : term has no direct child with model basis attribute.

-struct ModelBasisArgAttributeId {};

-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;

-

-class QuantifiersEngine;

-

-namespace quantifiers{

-

-class TermDb;

-

-class FirstOrderModel : public DefaultModel

-{

-private:

-  //pointer to term database

-  TermDb* d_term_db;

-  //add term function

-  void addTerm( Node n );

-  //for initialize model

-  void initializeModelForTerm( Node n );

-  /** to stream functions */

-  void toStreamFunction( Node n, std::ostream& out );

-  void toStreamType( TypeNode tn, std::ostream& out );

-public: //for Theory UF:

-  //models for each UF operator

-  std::map< Node, uf::UfModelTree > d_uf_model_tree;

-  //model generators

-  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;

-public: //for Theory Arrays:

-  //default value for each non-store array

-  std::map< Node, arrays::ArrayModel > d_array_model;

-public: //for Theory Quantifiers:

-  /** list of quantifiers asserted in the current context */

-  context::CDList<Node> d_forall_asserts;

-  /** get number of asserted quantifiers */

-  int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }

-  /** get asserted quantifier */

-  Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }

-public:

-  FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );

-  virtual ~FirstOrderModel(){}

-  // reset the model

-  void reset();

-  /** get interpreted value */

-  Node getInterpretedValue( TNode n );

-public:

-  // initialize the model

-  void initialize();

-  /** get term database */

-  TermDb* getTermDatabase();

-  /** to stream function */

-  void toStream( std::ostream& out );

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file first_order_model.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 Model extended classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__FIRST_ORDER_MODEL_H
+#define __CVC4__FIRST_ORDER_MODEL_H
+
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/arrays/theory_arrays_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+struct ModelBasisAttributeId {};
+typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
+//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+//                    0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId {};
+typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
+
+class QuantifiersEngine;
+
+namespace quantifiers{
+
+class TermDb;
+
+class FirstOrderModel : public DefaultModel
+{
+private:
+  //pointer to term database
+  TermDb* d_term_db;
+  //add term function
+  void addTerm( Node n );
+  //for initialize model
+  void initializeModelForTerm( Node n );
+  /** to stream functions */
+  void toStreamFunction( Node n, std::ostream& out );
+  void toStreamType( TypeNode tn, std::ostream& out );
+public: //for Theory UF:
+  //models for each UF operator
+  std::map< Node, uf::UfModelTree > d_uf_model_tree;
+  //model generators
+  std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
+public: //for Theory Arrays:
+  //default value for each non-store array
+  std::map< Node, arrays::ArrayModel > d_array_model;
+public: //for Theory Quantifiers:
+  /** list of quantifiers asserted in the current context */
+  context::CDList<Node> d_forall_asserts;
+  /** get number of asserted quantifiers */
+  int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+  /** get asserted quantifier */
+  Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+public:
+  FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
+  virtual ~FirstOrderModel(){}
+  // reset the model
+  void reset();
+  /** get interpreted value */
+  Node getInterpretedValue( TNode n );
+public:
+  // initialize the model
+  void initialize();
+  /** get term database */
+  TermDb* getTermDatabase();
+  /** to stream function */
+  void toStream( std::ostream& out );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 13d500d8e..05eb8f55f 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -1,91 +1,91 @@
-/*********************                                                        */

-/*! \file model_builder.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: mdeters

- ** Minor contributors (to current version): none

- ** This file is part of the CVC4 prototype.

- ** Copyright (c) 2009-2012  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 Model Builder class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H

-#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H

-

-#include "theory/quantifiers_engine.h"

-#include "theory/model.h"

-#include "theory/uf/theory_uf_model.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-//the model builder

-class ModelEngineBuilder : public TheoryEngineModelBuilder

-{

-protected:

-  //quantifiers engine

-  QuantifiersEngine* d_qe;

-  //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;

-  /** process build model */

-  void processBuildModel( TheoryModel* m );

-  /** choose representative for unconstrained equivalence class */

-  Node chooseRepresentative( TheoryModel* m, Node eqc );

-  /** bad representative */

-  bool isBadRepresentative( Node n );

-protected:

-  //analyze model

-  void analyzeModel( FirstOrderModel* fm );

-  //analyze quantifiers

-  void analyzeQuantifiers( FirstOrderModel* fm );

-  //build model

-  void finishBuildModel( FirstOrderModel* fm );

-  //theory-specific build models

-  void finishBuildModelUf( FirstOrderModel* fm, Node op );

-  //do InstGen techniques for quantifier, return number of lemmas produced

-  int doInstGen( FirstOrderModel* fm, Node f );

-public:

-  ModelEngineBuilder( QuantifiersEngine* qe );

-  virtual ~ModelEngineBuilder(){}

-  /** finish model */

-  void finishProcessBuildModel( TheoryModel* m );

-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;

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file model_builder.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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 Model Builder class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H
+#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//the model builder
+class ModelEngineBuilder : public TheoryEngineModelBuilder
+{
+protected:
+  //quantifiers engine
+  QuantifiersEngine* d_qe;
+  //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;
+  /** process build model */
+  void processBuildModel( TheoryModel* m );
+  /** choose representative for unconstrained equivalence class */
+  Node chooseRepresentative( TheoryModel* m, Node eqc );
+  /** bad representative */
+  bool isBadRepresentative( Node n );
+protected:
+  //analyze model
+  void analyzeModel( FirstOrderModel* fm );
+  //analyze quantifiers
+  void analyzeQuantifiers( FirstOrderModel* fm );
+  //build model
+  void finishBuildModel( FirstOrderModel* fm );
+  //theory-specific build models
+  void finishBuildModelUf( FirstOrderModel* fm, Node op );
+  //do InstGen techniques for quantifier, return number of lemmas produced
+  int doInstGen( FirstOrderModel* fm, Node f );
+public:
+  ModelEngineBuilder( QuantifiersEngine* qe );
+  virtual ~ModelEngineBuilder(){}
+  /** finish model */
+  void finishProcessBuildModel( TheoryModel* m );
+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;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 12206e148..1563a3d1d 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -1,173 +1,173 @@
-/*********************                                                        */

-/*! \file relevant_domain.cpp

- ** \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 Implementation of relevant domain class

- **/

-

-#include "theory/quantifiers_engine.h"

-#include "theory/quantifiers/relevant_domain.h"

-#include "theory/quantifiers/term_database.h"

-#include "theory/quantifiers/first_order_model.h"

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-

-RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){

-

-}

-

-void RelevantDomain::compute(){

-  d_quant_inst_domain.clear();

-  for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){

-    Node f = d_model->getAssertedQuantifier( i );

-    d_quant_inst_domain[f].resize( f[0].getNumChildren() );

-  }

-  //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)

-  for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();

-       it != d_model->d_uf_model_tree.end(); ++it ){

-    Node op = it->first;

-    for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){

-      Node n = d_model->d_uf_terms[op][i];

-      //add arguments to domain

-      for( int j=0; j<(int)n.getNumChildren(); j++ ){

-        if( d_model->d_rep_set.hasType( n[j].getType() ) ){

-          Node ra = d_model->getRepresentative( n[j] );

-          int raIndex = d_model->d_rep_set.getIndexFor( ra );

-          Assert( raIndex!=-1 );

-          if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){

-            d_active_domain[op][j].push_back( raIndex );

-          }

-        }

-      }

-      //add to range

-      Node r = d_model->getRepresentative( n );

-      int raIndex = d_model->d_rep_set.getIndexFor( r );

-      Assert( raIndex!=-1 );

-      if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){

-        d_active_range[op].push_back( raIndex );

-      }

-    }

-  }

-  //find fixed point for relevant domain computation

-  bool success;

-  do{

-    success = true;

-    for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){

-      Node f = d_model->getAssertedQuantifier( i );

-      //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)

-      if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){

-        success = false;

-      }

-      //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)

-      RepDomain range;

-      if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){

-        success = false;

-      }

-    }

-  }while( !success );

-}

-

-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){

-  bool domainChanged = false;

-  if( n.getKind()==INST_CONSTANT ){

-    bool domainSet = false;

-    int vi = n.getAttribute(InstVarNumAttribute());

-    Assert( !parent.isNull() );

-    if( parent.getKind()==APPLY_UF ){

-      //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument

-      Node op = parent.getOperator();

-      if( d_active_domain.find( op )!=d_active_domain.end() ){

-        for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){

-          int d = d_active_domain[op][arg][i];

-          if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){

-            rd[vi].push_back( d );

-            domainChanged = true;

-          }

-        }

-        domainSet = true;

-      }

-    }

-    if( !domainSet ){

-      //otherwise, we must consider the entire domain

-      TypeNode tn = n.getType();

-      if( d_model->d_rep_set.hasType( tn ) ){

-        if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){

-          rd[vi].clear();

-          for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){

-            rd[vi].push_back( i );

-            domainChanged = true;

-          }

-        }

-      }else{

-        //infinite domain?

-      }

-    }

-  }else{

-    for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){

-        domainChanged = true;

-      }

-    }

-  }

-  return domainChanged;

-}

-

-bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){

-  if( n.getKind()==INST_CONSTANT ){

-    Node f = n.getAttribute(InstConstantAttribute());

-    int var = n.getAttribute(InstVarNumAttribute());

-    range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );

-    return false;

-  }else{

-    Node op;

-    if( n.getKind()==APPLY_UF ){

-      op = n.getOperator();

-    }

-    bool domainChanged = false;

-    for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      RepDomain childRange;

-      if( extendFunctionDomains( n[i], childRange ) ){

-        domainChanged = true;

-      }

-      if( n.getKind()==APPLY_UF ){

-        if( d_active_domain.find( op )!=d_active_domain.end() ){

-          for( int j=0; j<(int)childRange.size(); j++ ){

-            int v = childRange[j];

-            if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){

-              d_active_domain[op][i].push_back( v );

-              domainChanged = true;

-            }

-          }

-        }else{

-          //do this?

-        }

-      }

-    }

-    //get the range

-    if( n.hasAttribute(InstConstantAttribute()) ){

-      if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){

-        range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );

-      }else{

-        //infinite range?

-      }

-    }else{

-      Node r = d_model->getRepresentative( n );

-      range.push_back( d_model->d_rep_set.getIndexFor( r ) );

-    }

-    return domainChanged;

-  }

+/*********************                                                        */
+/*! \file relevant_domain.cpp
+ ** \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 Implementation of relevant domain class
+ **/
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){
+
+}
+
+void RelevantDomain::compute(){
+  d_quant_inst_domain.clear();
+  for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
+    Node f = d_model->getAssertedQuantifier( i );
+    d_quant_inst_domain[f].resize( f[0].getNumChildren() );
+  }
+  //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
+  for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
+       it != d_model->d_uf_model_tree.end(); ++it ){
+    Node op = it->first;
+    for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){
+      Node n = d_model->d_uf_terms[op][i];
+      //add arguments to domain
+      for( int j=0; j<(int)n.getNumChildren(); j++ ){
+        if( d_model->d_rep_set.hasType( n[j].getType() ) ){
+          Node ra = d_model->getRepresentative( n[j] );
+          int raIndex = d_model->d_rep_set.getIndexFor( ra );
+          Assert( raIndex!=-1 );
+          if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
+            d_active_domain[op][j].push_back( raIndex );
+          }
+        }
+      }
+      //add to range
+      Node r = d_model->getRepresentative( n );
+      int raIndex = d_model->d_rep_set.getIndexFor( r );
+      Assert( raIndex!=-1 );
+      if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){
+        d_active_range[op].push_back( raIndex );
+      }
+    }
+  }
+  //find fixed point for relevant domain computation
+  bool success;
+  do{
+    success = true;
+    for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
+      Node f = d_model->getAssertedQuantifier( i );
+      //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
+      if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){
+        success = false;
+      }
+      //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
+      RepDomain range;
+      if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){
+        success = false;
+      }
+    }
+  }while( !success );
+}
+
+bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){
+  bool domainChanged = false;
+  if( n.getKind()==INST_CONSTANT ){
+    bool domainSet = false;
+    int vi = n.getAttribute(InstVarNumAttribute());
+    Assert( !parent.isNull() );
+    if( parent.getKind()==APPLY_UF ){
+      //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
+      Node op = parent.getOperator();
+      if( d_active_domain.find( op )!=d_active_domain.end() ){
+        for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
+          int d = d_active_domain[op][arg][i];
+          if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){
+            rd[vi].push_back( d );
+            domainChanged = true;
+          }
+        }
+        domainSet = true;
+      }
+    }
+    if( !domainSet ){
+      //otherwise, we must consider the entire domain
+      TypeNode tn = n.getType();
+      if( d_model->d_rep_set.hasType( tn ) ){
+        if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){
+          rd[vi].clear();
+          for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
+            rd[vi].push_back( i );
+            domainChanged = true;
+          }
+        }
+      }else{
+        //infinite domain?
+      }
+    }
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){
+        domainChanged = true;
+      }
+    }
+  }
+  return domainChanged;
+}
+
+bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
+  if( n.getKind()==INST_CONSTANT ){
+    Node f = n.getAttribute(InstConstantAttribute());
+    int var = n.getAttribute(InstVarNumAttribute());
+    range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
+    return false;
+  }else{
+    Node op;
+    if( n.getKind()==APPLY_UF ){
+      op = n.getOperator();
+    }
+    bool domainChanged = false;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      RepDomain childRange;
+      if( extendFunctionDomains( n[i], childRange ) ){
+        domainChanged = true;
+      }
+      if( n.getKind()==APPLY_UF ){
+        if( d_active_domain.find( op )!=d_active_domain.end() ){
+          for( int j=0; j<(int)childRange.size(); j++ ){
+            int v = childRange[j];
+            if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
+              d_active_domain[op][i].push_back( v );
+              domainChanged = true;
+            }
+          }
+        }else{
+          //do this?
+        }
+      }
+    }
+    //get the range
+    if( n.hasAttribute(InstConstantAttribute()) ){
+      if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
+        range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
+      }else{
+        //infinite range?
+      }
+    }else{
+      Node r = d_model->getRepresentative( n );
+      range.push_back( d_model->d_rep_set.getIndexFor( r ) );
+    }
+    return domainChanged;
+  }
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 362a39d6a..8c8ea6a42 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -1,54 +1,54 @@
-/*********************                                                        */

-/*! \file relevant_domain.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 relevant domain class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__RELEVANT_DOMAIN_H

-#define __CVC4__RELEVANT_DOMAIN_H

-

-#include "theory/quantifiers/first_order_model.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class RelevantDomain

-{

-private:

-  FirstOrderModel* d_model;

-

-  //the domain of the arguments for each operator

-  std::map< Node, std::map< int, RepDomain > > d_active_domain;

-  //the range for each operator

-  std::map< Node, RepDomain > d_active_range;

-  //for computing relevant instantiation domain, return true if changed

-  bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );

-  //for computing extended

-  bool extendFunctionDomains( Node n, RepDomain& range );

-public:

-  RelevantDomain( FirstOrderModel* m );

-  virtual ~RelevantDomain(){}

-  //compute the relevant domain

-  void compute();

-  //relevant instantiation domain for each quantifier

-  std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file relevant_domain.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 relevant domain class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__RELEVANT_DOMAIN_H
+#define __CVC4__RELEVANT_DOMAIN_H
+
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class RelevantDomain
+{
+private:
+  FirstOrderModel* d_model;
+
+  //the domain of the arguments for each operator
+  std::map< Node, std::map< int, RepDomain > > d_active_domain;
+  //the range for each operator
+  std::map< Node, RepDomain > d_active_range;
+  //for computing relevant instantiation domain, return true if changed
+  bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
+  //for computing extended
+  bool extendFunctionDomains( Node n, RepDomain& range );
+public:
+  RelevantDomain( FirstOrderModel* m );
+  virtual ~RelevantDomain(){}
+  //compute the relevant domain
+  void compute();
+  //relevant instantiation domain for each quantifier
+  std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
index 516f85857..9c1c4c89e 100644
--- a/src/theory/quantifiers/rep_set_iterator.cpp
+++ b/src/theory/quantifiers/rep_set_iterator.cpp
@@ -1,517 +1,517 @@
-/*********************                                                        */

-/*! \file rep_set_iterator.cpp

- ** \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 Implementation of relevant domain class

- **/

-

-#include "theory/quantifiers/rep_set_iterator.h"

-#include "theory/quantifiers/model_engine.h"

-#include "theory/quantifiers/term_database.h"

-

-#define USE_INDEX_ORDERING

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-

-RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){

-  //store instantiation constants

-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){

-    d_index.push_back( 0 );

-  }

-  for( size_t i=0; i<f[0].getNumChildren(); i++ ){

-    //store default index order

-    d_index_order.push_back( i );

-    d_var_order[i] = i;

-    //store default domain

-    d_domain.push_back( RepDomain() );

-    TypeNode tn = d_f[0][i].getType();

-    if( tn.isSort() ){

-      if( d_model->d_rep_set.hasType( tn ) ){

-        for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){

-          d_domain[i].push_back( j );

-        }

-      }else{

-        Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");

-      }

-    }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){

-      Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");

-    }else if( tn.isDatatype() ){

-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();

-      //if finite, then use type enumerator

-      if( dt.isFinite() ){

-        //DO_THIS: use type enumerator

-        Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");

-      }else{

-        Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");

-      }

-    }else{

-      Unimplemented("Cannot create instantiation iterator for quantifier");

-    }

-  }

-}

-

-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){

-  d_index_order.clear();

-  d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );

-  //make the d_var_order mapping

-  for( int i=0; i<(int)d_index_order.size(); i++ ){

-    d_var_order[d_index_order[i]] = i;

-  }

-}

-

-void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){

-  d_domain.clear();

-  d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );

-  //we are done if a domain is empty

-  for( int i=0; i<(int)d_domain.size(); i++ ){

-    if( d_domain[i].empty() ){

-      d_index.clear();

-    }

-  }

-}

-

-void RepSetIterator::increment2( int counter ){

-  Assert( !isFinished() );

-#ifdef DISABLE_EVAL_SKIP_MULTIPLE

-  counter = (int)d_index.size()-1;

-#endif

-  //increment d_index

-  while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){

-    counter--;

-  }

-  if( counter==-1 ){

-    d_index.clear();

-  }else{

-    for( int i=(int)d_index.size()-1; i>counter; i-- ){

-      d_index[i] = 0;

-      //d_model->clearEvalFailed( i );

-    }

-    d_index[counter]++;

-    //d_model->clearEvalFailed( counter );

-  }

-}

-

-void RepSetIterator::increment(){

-  if( !isFinished() ){

-    increment2( (int)d_index.size()-1 );

-  }

-}

-

-bool RepSetIterator::isFinished(){

-  return d_index.empty();

-}

-

-void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){

-  for( int i=0; i<(int)d_index.size(); i++ ){

-    m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));

-  }

-}

-

-Node RepSetIterator::getTerm( int i ){

-  TypeNode tn = d_f[0][d_index_order[i]].getType();

-  Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );

-  int index = d_index_order[i];

-  return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];

-}

-

-void RepSetIterator::debugPrint( const char* c ){

-  for( int i=0; i<(int)d_index.size(); i++ ){

-    Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;

-  }

-}

-

-void RepSetIterator::debugPrintSmall( const char* c ){

-  Debug( c ) << "RI: ";

-  for( int i=0; i<(int)d_index.size(); i++ ){

-    Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";

-  }

-  Debug( c ) << std::endl;

-}

-

-RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){

-  d_eval_formulas = 0;

-  d_eval_uf_terms = 0;

-  d_eval_lits = 0;

-  d_eval_lits_unknown = 0;

-}

-

-//if evaluate( n ) = eVal,

-// let n' = d_riter * n be the formula n instantiated with the current values in r_iter

-// if eVal = 1, then n' is true, if eVal = -1, then n' is false,

-// if eVal = 0, then n' cannot be proven to be equal to phaseReq

-// if eVal is not 0, then

-//   each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model

-int RepSetEvaluator::evaluate( Node n, int& depIndex ){

-  ++d_eval_formulas;

-  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;

-  //Notice() << "Eval " << n << std::endl;

-  if( n.getKind()==NOT ){

-    int val = evaluate( n[0], depIndex );

-    return val==1 ? -1 : ( val==-1 ? 1 : 0 );

-  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){

-    int baseVal = n.getKind()==AND ? 1 : -1;

-    int eVal = baseVal;

-    int posDepIndex = d_riter->getNumTerms();

-    int negDepIndex = -1;

-    for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      //evaluate subterm

-      int childDepIndex;

-      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];

-      int eValT = evaluate( nn, childDepIndex );

-      if( eValT==baseVal ){

-        if( eVal==baseVal ){

-          if( childDepIndex>negDepIndex ){

-            negDepIndex = childDepIndex;

-          }

-        }

-      }else if( eValT==-baseVal ){

-        eVal = -baseVal;

-        if( childDepIndex<posDepIndex ){

-          posDepIndex = childDepIndex;

-          if( posDepIndex==-1 ){

-            break;

-          }

-        }

-      }else if( eValT==0 ){

-        if( eVal==baseVal ){

-          eVal = 0;

-        }

-      }

-    }

-    if( eVal!=0 ){

-      depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;

-      return eVal;

-    }else{

-      return 0;

-    }

-  }else if( n.getKind()==IFF || n.getKind()==XOR ){

-    int depIndex1;

-    int eVal = evaluate( n[0], depIndex1 );

-    if( eVal!=0 ){

-      int depIndex2;

-      int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );

-      if( eVal2!=0 ){

-        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-        return eVal==eVal2 ? 1 : -1;

-      }

-    }

-    return 0;

-  }else if( n.getKind()==ITE ){

-    int depIndex1, depIndex2;

-    int eVal = evaluate( n[0], depIndex1 );

-    if( eVal==0 ){

-      //evaluate children to see if they are the same value

-      int eval1 = evaluate( n[1], depIndex1 );

-      if( eval1!=0 ){

-        int eval2 = evaluate( n[1], depIndex2 );

-        if( eval1==eval2 ){

-          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-          return eval1;

-        }

-      }

-    }else{

-      int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );

-      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-      return eValT;

-    }

-    return 0;

-  }else if( n.getKind()==FORALL ){

-    return 0;

-  }else{

-    ++d_eval_lits;

-    ////if we know we will fail again, immediately return

-    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){

-    //  if( d_eval_failed[n] ){

-    //    return -1;

-    //  }

-    //}

-    //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;

-    int retVal = 0;

-    depIndex = d_riter->getNumTerms()-1;

-    Node val = evaluateTerm( n, depIndex );

-    if( !val.isNull() ){

-      if( d_model->areEqual( val, d_model->d_true ) ){

-        retVal = 1;

-      }else if( d_model->areEqual( val, d_model->d_false ) ){

-        retVal = -1;

-      }else{

-        if( val.getKind()==EQUAL ){

-          if( d_model->areEqual( val[0], val[1] ) ){

-            retVal = 1;

-          }else if( d_model->areDisequal( val[0], val[1] ) ){

-            retVal = -1;

-          }

-        }

-      }

-    }

-    if( retVal!=0 ){

-      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;

-    }else{

-      ++d_eval_lits_unknown;

-      Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;

-      //std::cout << "Neither true nor false : " << n << std::endl;

-      //std::cout << "  Value : " << val << std::endl;

-      //for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;

-      //}

-    }

-    return retVal;

-  }

-}

-

-Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){

-  //Message() << "Eval term " << n << std::endl;

-  if( !n.hasAttribute(InstConstantAttribute()) ){

-    //if evaluating a ground term, just consult the standard getValue functionality

-    depIndex = -1;

-    return d_model->getValue( n );

-  }else{

-    Node val;

-    depIndex = d_riter->getNumTerms()-1;

-    //check the type of n

-    if( n.getKind()==INST_CONSTANT ){

-      int v = n.getAttribute(InstVarNumAttribute());

-      depIndex = d_riter->d_var_order[ v ];

-      val = d_riter->getTerm( v );

-    }else if( n.getKind()==ITE ){

-      int depIndex1, depIndex2;

-      int eval = evaluate( n[0], depIndex1 );

-      if( eval==0 ){

-        //evaluate children to see if they are the same

-        Node val1 = evaluateTerm( n[ 1 ], depIndex1 );

-        Node val2 = evaluateTerm( n[ 2 ], depIndex2 );

-        if( val1==val2 ){

-          val = val1;

-          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-        }else{

-          return Node::null();

-        }

-      }else{

-        val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );

-        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;

-      }

-    }else{

-      std::vector< int > children_depIndex;

-      //for select, pre-process read over writes

-      if( n.getKind()==SELECT ){

-#if 1

-        //std::cout << "Evaluate " << n << std::endl;

-        Node sel = evaluateTerm( n[1], depIndex );

-        if( sel.isNull() ){

-          depIndex = d_riter->getNumTerms()-1;

-          return Node::null();

-        }

-        Node arr = d_model->getRepresentative( n[0] );

-        //if( n[0]!=d_model->getRepresentative( n[0] ) ){

-        //  std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;

-        //}

-        int tempIndex;

-        int eval = 1;

-        while( arr.getKind()==STORE && eval!=0 ){

-          eval = evaluate( sel.eqNode( arr[1] ), tempIndex );

-          depIndex = tempIndex > depIndex ? tempIndex : depIndex;

-          if( eval==1 ){

-            val = evaluateTerm( arr[2], tempIndex );

-            depIndex = tempIndex > depIndex ? tempIndex : depIndex;

-            return val;

-          }else if( eval==-1 ){

-            arr = arr[0];

-          }

-        }

-        arr = evaluateTerm( arr, tempIndex );

-        depIndex = tempIndex > depIndex ? tempIndex : depIndex;

-        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );

-#else

-        val = evaluateTermDefault( n, depIndex, children_depIndex );

-#endif

-      }else{

-        //default term evaluate : evaluate all children, recreate the value

-        val = evaluateTermDefault( n, depIndex, children_depIndex );

-      }

-      if( !val.isNull() ){

-        bool setVal = false;

-        //custom ways of evaluating terms

-        if( n.getKind()==APPLY_UF ){

-          Node op = n.getOperator();

-          //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;

-          //if it is a defined UF, then consult the interpretation

-          if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){

-            ++d_eval_uf_terms;

-            int argDepIndex = 0;

-            //make the term model specifically for n

-            makeEvalUfModel( n );

-            //now, consult the model

-            if( d_eval_uf_use_default[n] ){

-              val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );

-            }else{

-              val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );

-            }

-            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;

-            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );

-            Assert( !val.isNull() );

-            //recalculate the depIndex

-            depIndex = -1;

-            for( int i=0; i<argDepIndex; i++ ){

-              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];

-              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;

-              if( children_depIndex[index]>depIndex ){

-                depIndex = children_depIndex[index];

-              }

-            }

-            setVal = true;

-          }

-        }else if( n.getKind()==SELECT ){

-          //we are free to interpret this term however we want

-        }

-        //if not set already, rewrite and consult model for interpretation

-        if( !setVal ){

-          val = Rewriter::rewrite( val );

-          if( val.getMetaKind()!=kind::metakind::CONSTANT ){

-            //FIXME: we cannot do this until we trust all theories collectModelInfo!

-            //val = d_model->getInterpretedValue( val );

-            //val = d_model->getRepresentative( val );

-          }

-        }

-        Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";

-        d_model->printRepresentativeDebug( "fmf-eval-debug", val );

-        Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;

-      }

-    }

-    return val;

-  }

-}

-

-Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){

-  depIndex = -1;

-  if( n.getNumChildren()==0 ){

-    return n;

-  }else{

-    //first we must evaluate the arguments

-    std::vector< Node > children;

-    if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){

-      children.push_back( n.getOperator() );

-    }

-    //for each argument, calculate its value, and the variables its value depends upon

-    for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      childDepIndex.push_back( -1 );

-      Node nn = evaluateTerm( n[i], childDepIndex[i] );

-      if( nn.isNull() ){

-        depIndex = d_riter->getNumTerms()-1;

-        return nn;

-      }else{

-        children.push_back( nn );

-        if( childDepIndex[i]>depIndex ){

-          depIndex = childDepIndex[i];

-        }

-      }

-    }

-    //recreate the value

-    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );

-    return val;

-  }

-}

-

-void RepSetEvaluator::clearEvalFailed( int index ){

-  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){

-    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;

-  }

-  d_eval_failed_lits[index].clear();

-}

-

-void RepSetEvaluator::makeEvalUfModel( Node n ){

-  if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){

-    makeEvalUfIndexOrder( n );

-    if( !d_eval_uf_use_default[n] ){

-      Node op = n.getOperator();

-      d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );

-      d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );

-      //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;

-      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );

-    }

-  }

-}

-

-struct sortGetMaxVariableNum {

-  std::map< Node, int > d_max_var_num;

-  int computeMaxVariableNum( Node n ){

-    if( n.getKind()==INST_CONSTANT ){

-      return n.getAttribute(InstVarNumAttribute());

-    }else if( n.hasAttribute(InstConstantAttribute()) ){

-      int maxVal = -1;

-      for( int i=0; i<(int)n.getNumChildren(); i++ ){

-        int val = getMaxVariableNum( n[i] );

-        if( val>maxVal ){

-          maxVal = val;

-        }

-      }

-      return maxVal;

-    }else{

-      return -1;

-    }

-  }

-  int getMaxVariableNum( Node n ){

-    std::map< Node, int >::iterator it = d_max_var_num.find( n );

-    if( it==d_max_var_num.end() ){

-      int num = computeMaxVariableNum( n );

-      d_max_var_num[n] = num;

-      return num;

-    }else{

-      return it->second;

-    }

-  }

-  bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}

-};

-

-void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){

-  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){

-#ifdef USE_INDEX_ORDERING

-    //sort arguments in order of least significant vs. most significant variable in default ordering

-    std::map< Node, std::vector< int > > argIndex;

-    std::vector< Node > args;

-    for( int i=0; i<(int)n.getNumChildren(); i++ ){

-      if( argIndex.find( n[i] )==argIndex.end() ){

-        args.push_back( n[i] );

-      }

-      argIndex[n[i]].push_back( i );

-    }

-    sortGetMaxVariableNum sgmvn;

-    std::sort( args.begin(), args.end(), sgmvn );

-    for( int i=0; i<(int)args.size(); i++ ){

-      for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){

-        d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );

-      }

-    }

-    bool useDefault = true;

-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){

-      if( i!=d_eval_term_index_order[n][i] ){

-        useDefault = false;

-        break;

-      }

-    }

-    d_eval_uf_use_default[n] = useDefault;

-    Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";

-    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){

-      Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";

-    }

-    Debug("fmf-index-order") << std::endl;

-#else

-    d_eval_uf_use_default[n] = true;

-#endif

-  }

-}

-

-

+/*********************                                                        */
+/*! \file rep_set_iterator.cpp
+ ** \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 Implementation of relevant domain class
+ **/
+
+#include "theory/quantifiers/rep_set_iterator.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+#define USE_INDEX_ORDERING
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){
+  //store instantiation constants
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    d_index.push_back( 0 );
+  }
+  for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+    //store default index order
+    d_index_order.push_back( i );
+    d_var_order[i] = i;
+    //store default domain
+    d_domain.push_back( RepDomain() );
+    TypeNode tn = d_f[0][i].getType();
+    if( tn.isSort() ){
+      if( d_model->d_rep_set.hasType( tn ) ){
+        for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){
+          d_domain[i].push_back( j );
+        }
+      }else{
+        Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");
+      }
+    }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+      Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");
+    }else if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      //if finite, then use type enumerator
+      if( dt.isFinite() ){
+        //DO_THIS: use type enumerator
+        Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");
+      }else{
+        Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");
+      }
+    }else{
+      Unimplemented("Cannot create instantiation iterator for quantifier");
+    }
+  }
+}
+
+void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
+  d_index_order.clear();
+  d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
+  //make the d_var_order mapping
+  for( int i=0; i<(int)d_index_order.size(); i++ ){
+    d_var_order[d_index_order[i]] = i;
+  }
+}
+
+void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
+  d_domain.clear();
+  d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
+  //we are done if a domain is empty
+  for( int i=0; i<(int)d_domain.size(); i++ ){
+    if( d_domain[i].empty() ){
+      d_index.clear();
+    }
+  }
+}
+
+void RepSetIterator::increment2( int counter ){
+  Assert( !isFinished() );
+#ifdef DISABLE_EVAL_SKIP_MULTIPLE
+  counter = (int)d_index.size()-1;
+#endif
+  //increment d_index
+  while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
+    counter--;
+  }
+  if( counter==-1 ){
+    d_index.clear();
+  }else{
+    for( int i=(int)d_index.size()-1; i>counter; i-- ){
+      d_index[i] = 0;
+      //d_model->clearEvalFailed( i );
+    }
+    d_index[counter]++;
+    //d_model->clearEvalFailed( counter );
+  }
+}
+
+void RepSetIterator::increment(){
+  if( !isFinished() ){
+    increment2( (int)d_index.size()-1 );
+  }
+}
+
+bool RepSetIterator::isFinished(){
+  return d_index.empty();
+}
+
+void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
+  for( int i=0; i<(int)d_index.size(); i++ ){
+    m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));
+  }
+}
+
+Node RepSetIterator::getTerm( int i ){
+  TypeNode tn = d_f[0][d_index_order[i]].getType();
+  Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );
+  int index = d_index_order[i];
+  return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];
+}
+
+void RepSetIterator::debugPrint( const char* c ){
+  for( int i=0; i<(int)d_index.size(); i++ ){
+    Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
+  }
+}
+
+void RepSetIterator::debugPrintSmall( const char* c ){
+  Debug( c ) << "RI: ";
+  for( int i=0; i<(int)d_index.size(); i++ ){
+    Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
+  }
+  Debug( c ) << std::endl;
+}
+
+RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){
+  d_eval_formulas = 0;
+  d_eval_uf_terms = 0;
+  d_eval_lits = 0;
+  d_eval_lits_unknown = 0;
+}
+
+//if evaluate( n ) = eVal,
+// let n' = d_riter * n be the formula n instantiated with the current values in r_iter
+// if eVal = 1, then n' is true, if eVal = -1, then n' is false,
+// if eVal = 0, then n' cannot be proven to be equal to phaseReq
+// if eVal is not 0, then
+//   each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
+int RepSetEvaluator::evaluate( Node n, int& depIndex ){
+  ++d_eval_formulas;
+  //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+  //Notice() << "Eval " << n << std::endl;
+  if( n.getKind()==NOT ){
+    int val = evaluate( n[0], depIndex );
+    return val==1 ? -1 : ( val==-1 ? 1 : 0 );
+  }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
+    int baseVal = n.getKind()==AND ? 1 : -1;
+    int eVal = baseVal;
+    int posDepIndex = d_riter->getNumTerms();
+    int negDepIndex = -1;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      //evaluate subterm
+      int childDepIndex;
+      Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
+      int eValT = evaluate( nn, childDepIndex );
+      if( eValT==baseVal ){
+        if( eVal==baseVal ){
+          if( childDepIndex>negDepIndex ){
+            negDepIndex = childDepIndex;
+          }
+        }
+      }else if( eValT==-baseVal ){
+        eVal = -baseVal;
+        if( childDepIndex<posDepIndex ){
+          posDepIndex = childDepIndex;
+          if( posDepIndex==-1 ){
+            break;
+          }
+        }
+      }else if( eValT==0 ){
+        if( eVal==baseVal ){
+          eVal = 0;
+        }
+      }
+    }
+    if( eVal!=0 ){
+      depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
+      return eVal;
+    }else{
+      return 0;
+    }
+  }else if( n.getKind()==IFF || n.getKind()==XOR ){
+    int depIndex1;
+    int eVal = evaluate( n[0], depIndex1 );
+    if( eVal!=0 ){
+      int depIndex2;
+      int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
+      if( eVal2!=0 ){
+        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+        return eVal==eVal2 ? 1 : -1;
+      }
+    }
+    return 0;
+  }else if( n.getKind()==ITE ){
+    int depIndex1, depIndex2;
+    int eVal = evaluate( n[0], depIndex1 );
+    if( eVal==0 ){
+      //evaluate children to see if they are the same value
+      int eval1 = evaluate( n[1], depIndex1 );
+      if( eval1!=0 ){
+        int eval2 = evaluate( n[1], depIndex2 );
+        if( eval1==eval2 ){
+          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+          return eval1;
+        }
+      }
+    }else{
+      int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );
+      depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+      return eValT;
+    }
+    return 0;
+  }else if( n.getKind()==FORALL ){
+    return 0;
+  }else{
+    ++d_eval_lits;
+    ////if we know we will fail again, immediately return
+    //if( d_eval_failed.find( n )!=d_eval_failed.end() ){
+    //  if( d_eval_failed[n] ){
+    //    return -1;
+    //  }
+    //}
+    //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
+    int retVal = 0;
+    depIndex = d_riter->getNumTerms()-1;
+    Node val = evaluateTerm( n, depIndex );
+    if( !val.isNull() ){
+      if( d_model->areEqual( val, d_model->d_true ) ){
+        retVal = 1;
+      }else if( d_model->areEqual( val, d_model->d_false ) ){
+        retVal = -1;
+      }else{
+        if( val.getKind()==EQUAL ){
+          if( d_model->areEqual( val[0], val[1] ) ){
+            retVal = 1;
+          }else if( d_model->areDisequal( val[0], val[1] ) ){
+            retVal = -1;
+          }
+        }
+      }
+    }
+    if( retVal!=0 ){
+      Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
+    }else{
+      ++d_eval_lits_unknown;
+      Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
+      //std::cout << "Neither true nor false : " << n << std::endl;
+      //std::cout << "  Value : " << val << std::endl;
+      //for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      //  std::cout << "   " << i << " : " << n[i].getType() << std::endl;
+      //}
+    }
+    return retVal;
+  }
+}
+
+Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
+  //Message() << "Eval term " << n << std::endl;
+  if( !n.hasAttribute(InstConstantAttribute()) ){
+    //if evaluating a ground term, just consult the standard getValue functionality
+    depIndex = -1;
+    return d_model->getValue( n );
+  }else{
+    Node val;
+    depIndex = d_riter->getNumTerms()-1;
+    //check the type of n
+    if( n.getKind()==INST_CONSTANT ){
+      int v = n.getAttribute(InstVarNumAttribute());
+      depIndex = d_riter->d_var_order[ v ];
+      val = d_riter->getTerm( v );
+    }else if( n.getKind()==ITE ){
+      int depIndex1, depIndex2;
+      int eval = evaluate( n[0], depIndex1 );
+      if( eval==0 ){
+        //evaluate children to see if they are the same
+        Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
+        Node val2 = evaluateTerm( n[ 2 ], depIndex2 );
+        if( val1==val2 ){
+          val = val1;
+          depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+        }else{
+          return Node::null();
+        }
+      }else{
+        val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );
+        depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
+      }
+    }else{
+      std::vector< int > children_depIndex;
+      //for select, pre-process read over writes
+      if( n.getKind()==SELECT ){
+#if 1
+        //std::cout << "Evaluate " << n << std::endl;
+        Node sel = evaluateTerm( n[1], depIndex );
+        if( sel.isNull() ){
+          depIndex = d_riter->getNumTerms()-1;
+          return Node::null();
+        }
+        Node arr = d_model->getRepresentative( n[0] );
+        //if( n[0]!=d_model->getRepresentative( n[0] ) ){
+        //  std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;
+        //}
+        int tempIndex;
+        int eval = 1;
+        while( arr.getKind()==STORE && eval!=0 ){
+          eval = evaluate( sel.eqNode( arr[1] ), tempIndex );
+          depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+          if( eval==1 ){
+            val = evaluateTerm( arr[2], tempIndex );
+            depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+            return val;
+          }else if( eval==-1 ){
+            arr = arr[0];
+          }
+        }
+        arr = evaluateTerm( arr, tempIndex );
+        depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+        val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
+#else
+        val = evaluateTermDefault( n, depIndex, children_depIndex );
+#endif
+      }else{
+        //default term evaluate : evaluate all children, recreate the value
+        val = evaluateTermDefault( n, depIndex, children_depIndex );
+      }
+      if( !val.isNull() ){
+        bool setVal = false;
+        //custom ways of evaluating terms
+        if( n.getKind()==APPLY_UF ){
+          Node op = n.getOperator();
+          //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+          //if it is a defined UF, then consult the interpretation
+          if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){
+            ++d_eval_uf_terms;
+            int argDepIndex = 0;
+            //make the term model specifically for n
+            makeEvalUfModel( n );
+            //now, consult the model
+            if( d_eval_uf_use_default[n] ){
+              val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );
+            }else{
+              val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
+            }
+            //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+            //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
+            Assert( !val.isNull() );
+            //recalculate the depIndex
+            depIndex = -1;
+            for( int i=0; i<argDepIndex; i++ ){
+              int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+              Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+              if( children_depIndex[index]>depIndex ){
+                depIndex = children_depIndex[index];
+              }
+            }
+            setVal = true;
+          }
+        }else if( n.getKind()==SELECT ){
+          //we are free to interpret this term however we want
+        }
+        //if not set already, rewrite and consult model for interpretation
+        if( !setVal ){
+          val = Rewriter::rewrite( val );
+          if( val.getMetaKind()!=kind::metakind::CONSTANT ){
+            //FIXME: we cannot do this until we trust all theories collectModelInfo!
+            //val = d_model->getInterpretedValue( val );
+            //val = d_model->getRepresentative( val );
+          }
+        }
+        Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
+        d_model->printRepresentativeDebug( "fmf-eval-debug", val );
+        Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
+      }
+    }
+    return val;
+  }
+}
+
+Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
+  depIndex = -1;
+  if( n.getNumChildren()==0 ){
+    return n;
+  }else{
+    //first we must evaluate the arguments
+    std::vector< Node > children;
+    if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
+      children.push_back( n.getOperator() );
+    }
+    //for each argument, calculate its value, and the variables its value depends upon
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      childDepIndex.push_back( -1 );
+      Node nn = evaluateTerm( n[i], childDepIndex[i] );
+      if( nn.isNull() ){
+        depIndex = d_riter->getNumTerms()-1;
+        return nn;
+      }else{
+        children.push_back( nn );
+        if( childDepIndex[i]>depIndex ){
+          depIndex = childDepIndex[i];
+        }
+      }
+    }
+    //recreate the value
+    Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
+    return val;
+  }
+}
+
+void RepSetEvaluator::clearEvalFailed( int index ){
+  for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
+    d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
+  }
+  d_eval_failed_lits[index].clear();
+}
+
+void RepSetEvaluator::makeEvalUfModel( Node n ){
+  if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
+    makeEvalUfIndexOrder( n );
+    if( !d_eval_uf_use_default[n] ){
+      Node op = n.getOperator();
+      d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
+      d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );
+      //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
+      //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+    }
+  }
+}
+
+struct sortGetMaxVariableNum {
+  std::map< Node, int > d_max_var_num;
+  int computeMaxVariableNum( Node n ){
+    if( n.getKind()==INST_CONSTANT ){
+      return n.getAttribute(InstVarNumAttribute());
+    }else if( n.hasAttribute(InstConstantAttribute()) ){
+      int maxVal = -1;
+      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        int val = getMaxVariableNum( n[i] );
+        if( val>maxVal ){
+          maxVal = val;
+        }
+      }
+      return maxVal;
+    }else{
+      return -1;
+    }
+  }
+  int getMaxVariableNum( Node n ){
+    std::map< Node, int >::iterator it = d_max_var_num.find( n );
+    if( it==d_max_var_num.end() ){
+      int num = computeMaxVariableNum( n );
+      d_max_var_num[n] = num;
+      return num;
+    }else{
+      return it->second;
+    }
+  }
+  bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
+};
+
+void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){
+  if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
+#ifdef USE_INDEX_ORDERING
+    //sort arguments in order of least significant vs. most significant variable in default ordering
+    std::map< Node, std::vector< int > > argIndex;
+    std::vector< Node > args;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( argIndex.find( n[i] )==argIndex.end() ){
+        args.push_back( n[i] );
+      }
+      argIndex[n[i]].push_back( i );
+    }
+    sortGetMaxVariableNum sgmvn;
+    std::sort( args.begin(), args.end(), sgmvn );
+    for( int i=0; i<(int)args.size(); i++ ){
+      for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
+        d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
+      }
+    }
+    bool useDefault = true;
+    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+      if( i!=d_eval_term_index_order[n][i] ){
+        useDefault = false;
+        break;
+      }
+    }
+    d_eval_uf_use_default[n] = useDefault;
+    Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
+    for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
+      Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
+    }
+    Debug("fmf-index-order") << std::endl;
+#else
+    d_eval_uf_use_default[n] = true;
+#endif
+  }
+}
+
+
diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h
index f6312ae5c..a5ec266a9 100644
--- a/src/theory/quantifiers/rep_set_iterator.h
+++ b/src/theory/quantifiers/rep_set_iterator.h
@@ -1,120 +1,120 @@
-/*********************                                                        */

-/*! \file rep_set_iterator.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 rep_set_iterator class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__REP_SET_ITERATOR_H

-#define __CVC4__REP_SET_ITERATOR_H

-

-#include "theory/quantifiers_engine.h"

-#include "theory/quantifiers/first_order_model.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-/** this class iterates over a RepSet */

-class RepSetIterator {

-public:

-  RepSetIterator( Node f, FirstOrderModel* model );

-  ~RepSetIterator(){}

-  //pointer to quantifier

-  Node d_f;

-  //pointer to model

-  FirstOrderModel* d_model;

-  //index we are considering

-  std::vector< int > d_index;

-  //domain we are considering

-  std::vector< RepDomain > d_domain;

-  //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:

-  /** set index order */

-  void setIndexOrder( std::vector< int >& indexOrder );

-  /** set domain */

-  void setDomain( std::vector< RepDomain >& domain );

-  /** increment the iterator */

-  void increment2( int counter );

-  void increment();

-  /** 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(); }

-  /** debug print */

-  void debugPrint( const char* c );

-  void debugPrintSmall( const char* c );

-};

-

-class RepSetEvaluator

-{

-private:

-  FirstOrderModel* d_model;

-  RepSetIterator* d_riter;

-private: //for Theory UF:

-  //map from terms to the models used to calculate their value

-  std::map< Node, bool > d_eval_uf_use_default;

-  std::map< Node, uf::UfModelTree > d_eval_uf_model;

-  void makeEvalUfModel( 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 makeEvalUfIndexOrder( Node n );

-private:

-  //default evaluate term function

-  Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );

-  //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;

-public:

-  RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );

-  virtual ~RepSetEvaluator(){}

-  /** evaluate functions */

-  int evaluate( Node n, int& depIndex );

-  Node evaluateTerm( Node n, int& depIndex );

-public:

-  //statistics

-  int d_eval_formulas;

-  int d_eval_uf_terms;

-  int d_eval_lits;

-  int d_eval_lits_unknown;

-};

-

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file rep_set_iterator.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 rep_set_iterator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__REP_SET_ITERATOR_H
+#define __CVC4__REP_SET_ITERATOR_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** this class iterates over a RepSet */
+class RepSetIterator {
+public:
+  RepSetIterator( Node f, FirstOrderModel* model );
+  ~RepSetIterator(){}
+  //pointer to quantifier
+  Node d_f;
+  //pointer to model
+  FirstOrderModel* d_model;
+  //index we are considering
+  std::vector< int > d_index;
+  //domain we are considering
+  std::vector< RepDomain > d_domain;
+  //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:
+  /** set index order */
+  void setIndexOrder( std::vector< int >& indexOrder );
+  /** set domain */
+  void setDomain( std::vector< RepDomain >& domain );
+  /** increment the iterator */
+  void increment2( int counter );
+  void increment();
+  /** 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(); }
+  /** debug print */
+  void debugPrint( const char* c );
+  void debugPrintSmall( const char* c );
+};
+
+class RepSetEvaluator
+{
+private:
+  FirstOrderModel* d_model;
+  RepSetIterator* d_riter;
+private: //for Theory UF:
+  //map from terms to the models used to calculate their value
+  std::map< Node, bool > d_eval_uf_use_default;
+  std::map< Node, uf::UfModelTree > d_eval_uf_model;
+  void makeEvalUfModel( 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 makeEvalUfIndexOrder( Node n );
+private:
+  //default evaluate term function
+  Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );
+  //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;
+public:
+  RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );
+  virtual ~RepSetEvaluator(){}
+  /** evaluate functions */
+  int evaluate( Node n, int& depIndex );
+  Node evaluateTerm( Node n, int& depIndex );
+public:
+  //statistics
+  int d_eval_formulas;
+  int d_eval_uf_terms;
+  int d_eval_lits;
+  int d_eval_lits_unknown;
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1ebba49b5..2af6992f7 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -1,156 +1,156 @@
-/**********************/

-/*! \file term_database.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 term database class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H

-#define __CVC4__QUANTIFIERS_TERM_DATABASE_H

-

-#include "theory/theory.h"

-

-#include <map>

-

-namespace CVC4 {

-namespace theory {

-

-class QuantifiersEngine;

-

-namespace quantifiers {

-

-class TermArgTrie {

-private:

-  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );

-public:

-  /** the data */

-  std::map< Node, TermArgTrie > d_data;

-public:

-  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }

-};/* class TermArgTrie */

-

-class TermDb {

-  friend class ::CVC4::theory::QuantifiersEngine;

-private:

-  /** reference to the quantifiers engine */

-  QuantifiersEngine* d_quantEngine;

-  /** calculated no match terms */

-  bool d_matching_active;

-  /** terms processed */

-  std::hash_set< Node, NodeHashFunction > d_processed;

-public:

-  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}

-  ~TermDb(){}

-  /** map from APPLY_UF operators to ground terms for that operator */

-  std::map< Node, std::vector< Node > > d_op_map;

-  /** map from APPLY_UF functions to trie */

-  std::map< Node, TermArgTrie > d_func_map_trie;

-  /** map from APPLY_UF predicates to trie */

-  std::map< Node, TermArgTrie > d_pred_map_trie[2];

-  /** map from type nodes to terms of that type */

-  std::map< TypeNode, std::vector< Node > > d_type_map;

-  /** add a term to the database */

-  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );

-  /** reset (calculate which terms are active) */

-  void reset( Theory::Effort effort );

-  /** set active */

-  void setMatchingActive( bool a ) { d_matching_active = a; }

-  /** get active */

-  bool getMatchingActive() { return d_matching_active; }

-private:

-  /** for efficient e-matching */

-  void addTermEfficient( Node n, std::set< Node >& added);

-public:

-  /** parent structure (for efficient E-matching):

-      n -> op -> index -> L

-      map from node "n" to a list of nodes "L", where each node n' in L

-        has operator "op", and n'["index"] = n.

-      for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }

-  */

-  /* Todo replace int by size_t */

-  std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction  > , NodeHashFunction > d_parents;

-  const std::vector<Node> & getParents(TNode n, TNode f, int arg);

-private:

-  //map from types to model basis terms

-  std::map< TypeNode, Node > d_model_basis_term;

-  //map from ops to model basis terms

-  std::map< Node, Node > d_model_basis_op_term;

-  //map from instantiation terms to their model basis equivalent

-  std::map< Node, Node > d_model_basis;

-public:

-  //get model basis term

-  Node getModelBasisTerm( TypeNode tn, int i = 0 );

-  //get model basis term for op

-  Node getModelBasisOpTerm( Node op );

-  // compute model basis arg

-  void computeModelBasisArgAttribute( Node n );

-  //register instantiation terms with their corresponding model basis terms

-  void registerModelBasis( Node n, Node gn );

-  //get model basis

-  Node getModelBasis( Node n ) { return d_model_basis[n]; }

-private:

-  /** map from universal quantifiers to the list of variables */

-  std::map< Node, std::vector< Node > > d_vars;

-  /** map from universal quantifiers to the list of skolem constants */

-  std::map< Node, std::vector< Node > > d_skolem_constants;

-  /** map from universal quantifiers to their skolemized body */

-  std::map< Node, Node > d_skolem_body;

-  /** instantiation constants to universal quantifiers */

-  std::map< Node, Node > d_inst_constants_map;

-  /** map from universal quantifiers to their counterexample body */

-  std::map< Node, Node > d_counterexample_body;

-  /** free variable for instantiation constant type */

-  std::map< TypeNode, Node > d_free_vars;

-private:

-  /** make instantiation constants for */

-  void makeInstantiationConstantsFor( Node f );

-public:

-  /** map from universal quantifiers to the list of instantiation constants */

-  std::map< Node, std::vector< Node > > d_inst_constants;

-  /** set instantiation level attr */

-  void setInstantiationLevelAttr( Node n, uint64_t level );

-  /** set instantiation constant attr */

-  void setInstantiationConstantAttr( Node n, Node f );

-  /** get the i^th instantiation constant of f */

-  Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }

-  /** get number of instantiation constants for f */

-  int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }

-  /** get the ce body f[e/x] */

-  Node getCounterexampleBody( Node f );

-  /** get the skolemized body f[e/x] */

-  Node getSkolemizedBody( Node f );

-  /** returns node n with bound vars of f replaced by instantiation constants of f

-      node n : is the futur pattern

-      node f : is the quantifier containing which bind the variable

-      return a pattern where the variable are replaced by variable for

-      instantiation.

-   */

-  Node getSubstitutedNode( Node n, Node f );

-  /** same as before but node f is just linked to the new pattern by the

-      applied attribute

-      vars the bind variable

-      nvars the same variable but with an attribute

-  */

-  Node convertNodeToPattern( Node n, Node f,

-                             const std::vector<Node> & vars,

-                             const std::vector<Node> & nvars);

-  /** get free variable for instantiation constant */

-  Node getFreeVariableForInstConstant( Node n );

-};/* class TermDb */

-

-}

-}

-}

-

-#endif

+/**********************/
+/*! \file term_database.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 term database class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H
+#define __CVC4__QUANTIFIERS_TERM_DATABASE_H
+
+#include "theory/theory.h"
+
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+class TermArgTrie {
+private:
+  bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+public:
+  /** the data */
+  std::map< Node, TermArgTrie > d_data;
+public:
+  bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+};/* class TermArgTrie */
+
+class TermDb {
+  friend class ::CVC4::theory::QuantifiersEngine;
+private:
+  /** reference to the quantifiers engine */
+  QuantifiersEngine* d_quantEngine;
+  /** calculated no match terms */
+  bool d_matching_active;
+  /** terms processed */
+  std::hash_set< Node, NodeHashFunction > d_processed;
+public:
+  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
+  ~TermDb(){}
+  /** map from APPLY_UF operators to ground terms for that operator */
+  std::map< Node, std::vector< Node > > d_op_map;
+  /** map from APPLY_UF functions to trie */
+  std::map< Node, TermArgTrie > d_func_map_trie;
+  /** map from APPLY_UF predicates to trie */
+  std::map< Node, TermArgTrie > d_pred_map_trie[2];
+  /** map from type nodes to terms of that type */
+  std::map< TypeNode, std::vector< Node > > d_type_map;
+  /** add a term to the database */
+  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
+  /** reset (calculate which terms are active) */
+  void reset( Theory::Effort effort );
+  /** set active */
+  void setMatchingActive( bool a ) { d_matching_active = a; }
+  /** get active */
+  bool getMatchingActive() { return d_matching_active; }
+private:
+  /** for efficient e-matching */
+  void addTermEfficient( Node n, std::set< Node >& added);
+public:
+  /** parent structure (for efficient E-matching):
+      n -> op -> index -> L
+      map from node "n" to a list of nodes "L", where each node n' in L
+        has operator "op", and n'["index"] = n.
+      for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
+  */
+  /* Todo replace int by size_t */
+  std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node >  >, NodeHashFunction  > , NodeHashFunction > d_parents;
+  const std::vector<Node> & getParents(TNode n, TNode f, int arg);
+private:
+  //map from types to model basis terms
+  std::map< TypeNode, Node > d_model_basis_term;
+  //map from ops to model basis terms
+  std::map< Node, Node > d_model_basis_op_term;
+  //map from instantiation terms to their model basis equivalent
+  std::map< Node, Node > d_model_basis;
+public:
+  //get model basis term
+  Node getModelBasisTerm( TypeNode tn, int i = 0 );
+  //get model basis term for op
+  Node getModelBasisOpTerm( Node op );
+  // compute model basis arg
+  void computeModelBasisArgAttribute( Node n );
+  //register instantiation terms with their corresponding model basis terms
+  void registerModelBasis( Node n, Node gn );
+  //get model basis
+  Node getModelBasis( Node n ) { return d_model_basis[n]; }
+private:
+  /** map from universal quantifiers to the list of variables */
+  std::map< Node, std::vector< Node > > d_vars;
+  /** map from universal quantifiers to the list of skolem constants */
+  std::map< Node, std::vector< Node > > d_skolem_constants;
+  /** map from universal quantifiers to their skolemized body */
+  std::map< Node, Node > d_skolem_body;
+  /** instantiation constants to universal quantifiers */
+  std::map< Node, Node > d_inst_constants_map;
+  /** map from universal quantifiers to their counterexample body */
+  std::map< Node, Node > d_counterexample_body;
+  /** free variable for instantiation constant type */
+  std::map< TypeNode, Node > d_free_vars;
+private:
+  /** make instantiation constants for */
+  void makeInstantiationConstantsFor( Node f );
+public:
+  /** map from universal quantifiers to the list of instantiation constants */
+  std::map< Node, std::vector< Node > > d_inst_constants;
+  /** set instantiation level attr */
+  void setInstantiationLevelAttr( Node n, uint64_t level );
+  /** set instantiation constant attr */
+  void setInstantiationConstantAttr( Node n, Node f );
+  /** get the i^th instantiation constant of f */
+  Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
+  /** get number of instantiation constants for f */
+  int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
+  /** get the ce body f[e/x] */
+  Node getCounterexampleBody( Node f );
+  /** get the skolemized body f[e/x] */
+  Node getSkolemizedBody( Node f );
+  /** returns node n with bound vars of f replaced by instantiation constants of f
+      node n : is the futur pattern
+      node f : is the quantifier containing which bind the variable
+      return a pattern where the variable are replaced by variable for
+      instantiation.
+   */
+  Node getSubstitutedNode( Node n, Node f );
+  /** same as before but node f is just linked to the new pattern by the
+      applied attribute
+      vars the bind variable
+      nvars the same variable but with an attribute
+  */
+  Node convertNodeToPattern( Node n, Node f,
+                             const std::vector<Node> & vars,
+                             const std::vector<Node> & nvars);
+  /** get free variable for instantiation constant */
+  Node getFreeVariableForInstConstant( Node n );
+};/* class TermDb */
+
+}
+}
+}
+
+#endif