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

21 files changed, 3660 insertions, 3663 deletions

diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 49da2f851..7a574fac1 100644
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -1,70 +1,70 @@
-/*********************                                                        */

-/*! \file theory_arrays_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 theory_arrays_model class

- **/

-

-#include "theory/theory_engine.h"

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

-#include "theory/quantifiers/first_order_model.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::arrays;

-

-ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){

-  Assert( arr.getKind()!=STORE );

-  //look at ground assertions

-  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );

-  Node sel_op = sel.getOperator();  //FIXME: easier way to do this?

-  for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){

-    Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];

-    Assert( n.getKind()==SELECT );

-    if( m->areEqual( n[0], arr ) ){

-      //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );

-      //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){

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

-        Node i = d_model->getRepresentative( n[1] );

-        d_values[i] = r;

-      //}

-    }

-  }

-}

-

-Node ArrayModel::getValue( Node n ){

-  Assert( n.getKind()==SELECT );

-  Assert( n[0]==d_arr );

-  std::map< Node, Node >::iterator it = d_values.find( n[0] );

-  if( it!=d_values.end() ){

-    return it->second;

-  }else{

-    return n;

-    //return d_default_value;   TODO: guarentee I can return this here

-  }

-}

-

-void ArrayModel::setDefaultValue( Node v ){

-  d_default_value = v;

-}

-

-Node ArrayModel::getArrayValue(){

-  Node curr = d_arr;    //TODO: make constant default

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

-    curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );

-  }

-  return curr;

-}

+/*********************                                                        */
+/*! \file theory_arrays_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 theory_arrays_model class
+ **/
+
+#include "theory/theory_engine.h"
+#include "theory/arrays/theory_arrays_model.h"
+#include "theory/quantifiers/first_order_model.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::arrays;
+
+ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
+  Assert( arr.getKind()!=STORE );
+  //look at ground assertions
+  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
+  Node sel_op = sel.getOperator();  //FIXME: easier way to do this?
+  for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
+    Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
+    Assert( n.getKind()==SELECT );
+    if( m->areEqual( n[0], arr ) ){
+      //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );
+      //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+        Node r = d_model->getRepresentative( n );
+        Node i = d_model->getRepresentative( n[1] );
+        d_values[i] = r;
+      //}
+    }
+  }
+}
+
+Node ArrayModel::getValue( Node n ){
+  Assert( n.getKind()==SELECT );
+  Assert( n[0]==d_arr );
+  std::map< Node, Node >::iterator it = d_values.find( n[0] );
+  if( it!=d_values.end() ){
+    return it->second;
+  }else{
+    return n;
+    //return d_default_value;   TODO: guarentee I can return this here
+  }
+}
+
+void ArrayModel::setDefaultValue( Node v ){
+  d_default_value = v;
+}
+
+Node ArrayModel::getArrayValue(){
+  Node curr = d_arr;    //TODO: make constant default
+  for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
+    curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
+  }
+  return curr;
+}
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
index 3895388e3..28852296d 100644
--- a/src/theory/arrays/theory_arrays_model.h
+++ b/src/theory/arrays/theory_arrays_model.h
@@ -1,62 +1,62 @@
-/*********************                                                        */

-/*! \file theory_arrays_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 for theory of arrays

- **/

-

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY_ARRAYS_MODEL_H

-#define __CVC4__THEORY_ARRAYS_MODEL_H

-

-#include "theory/quantifiers_engine.h"

-

-namespace CVC4 {

-namespace theory {

-

-namespace quantifiers{

-  class FirstOrderModel;

-}

-

-namespace arrays {

-

-class ArrayModel{

-protected:

-  /** reference to model */

-  quantifiers::FirstOrderModel* d_model;

-  /** the array this model is for */

-  Node d_arr;

-public:

-  ArrayModel(){}

-  ArrayModel( Node arr, quantifiers::FirstOrderModel* m );

-  ~ArrayModel() {}

-public:

-  /** pre-defined values */

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

-  /** default value */

-  Node d_default_value;

-  /** get value, return arguments that the value depends on */

-  Node getValue( Node n );

-  /** set default */

-  void setDefaultValue( Node v );

-public:

-  /** get array value */

-  Node getArrayValue();

-};/* class ArrayModel */

-

-}

-}

-}

-

+/*********************                                                        */
+/*! \file theory_arrays_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 for theory of arrays
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
+#define __CVC4__THEORY_ARRAYS_MODEL_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace quantifiers{
+  class FirstOrderModel;
+}
+
+namespace arrays {
+
+class ArrayModel{
+protected:
+  /** reference to model */
+  quantifiers::FirstOrderModel* d_model;
+  /** the array this model is for */
+  Node d_arr;
+public:
+  ArrayModel(){}
+  ArrayModel( Node arr, quantifiers::FirstOrderModel* m );
+  ~ArrayModel() {}
+public:
+  /** pre-defined values */
+  std::map< Node, Node > d_values;
+  /** default value */
+  Node d_default_value;
+  /** get value, return arguments that the value depends on */
+  Node getValue( Node n );
+  /** set default */
+  void setDefaultValue( Node v );
+public:
+  /** get array value */
+  Node getArrayValue();
+};/* class ArrayModel */
+
+}
+}
+}
+
 #endif
\ No newline at end of file
diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp
index ffecaa8da..a0f303c21 100644
--- a/src/theory/candidate_generator.cpp
+++ b/src/theory/candidate_generator.cpp
@@ -1,255 +1,255 @@
-/*********************                                                        */

-/*! \file theory_uf_candidate_generator.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 theory uf candidate generator class

- **/

-

-#include "theory/candidate_generator.h"

-#include "theory/theory_engine.h"

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

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

-#include "theory/inst_match.h"

-#include "theory/quantifiers_engine.h"

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::inst;

-

-bool CandidateGenerator::isLegalCandidate( Node n ){

-  return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) );

-}

-

-void CandidateGeneratorQueue::addCandidate( Node n ) {

-  if( isLegalCandidate( n ) ){

-    d_candidates.push_back( n );

-  }

-}

-

-void CandidateGeneratorQueue::reset( Node eqc ){

-  if( d_candidate_index>0 ){

-    d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );

-    d_candidate_index = 0;

-  }

-  if( !eqc.isNull() ){

-    d_candidates.push_back( eqc );

-  }

-}

-Node CandidateGeneratorQueue::getNextCandidate(){

-  if( d_candidate_index<(int)d_candidates.size() ){

-    Node n = d_candidates[d_candidate_index];

-    d_candidate_index++;

-    return n;

-  }else{

-    d_candidate_index = 0;

-    d_candidates.clear();

-    return Node::null();

-  }

-}

-

-#if 0

-

-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :

-  d_op( op ), d_qe( qe ), d_term_iter( -2 ){

-  Assert( !d_op.isNull() );

-}

-void CandidateGeneratorQE::resetInstantiationRound(){

-  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();

-}

-

-void CandidateGeneratorQE::reset( Node eqc ){

-  if( eqc.isNull() ){

-    d_term_iter = 0;

-  }else{

-    //create an equivalence class iterator in eq class eqc

-    if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){

-      eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc );

-      d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() );

-      d_retNode = Node::null();

-    }else{

-      d_retNode = eqc;

-    }

-    d_term_iter = -1;

-  }

-}

-

-Node CandidateGeneratorQE::getNextCandidate(){

-  if( d_term_iter>=0 ){

-    //get next candidate term in the uf term database

-    while( d_term_iter<d_term_iter_limit ){

-      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];

-      d_term_iter++;

-      if( isLegalCandidate( n ) ){

-        return n;

-      }

-    }

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

-    if( d_retNode.isNull() ){

-      //get next candidate term in equivalence class

-      while( !d_eqc.isFinished() ){

-        Node n = (*d_eqc);

-        ++d_eqc;

-        if( n.hasOperator() && n.getOperator()==d_op ){

-          if( isLegalCandidate( n ) ){

-            return n;

-          }

-        }

-      }

-    }else{

-      Node ret;

-      if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){

-        ret = d_retNode;

-      }

-      d_term_iter = -2; //done returning matches

-      return ret;

-    }

-  }

-  return Node::null();

-}

-

-#else

-

-

-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :

-  d_op( op ), d_qe( qe ), d_term_iter( -1 ){

-  Assert( !d_op.isNull() );

-}

-void CandidateGeneratorQE::resetInstantiationRound(){

-  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();

-}

-

-void CandidateGeneratorQE::reset( Node eqc ){

-  d_term_iter = 0;

-  if( eqc.isNull() ){

-    d_using_term_db = true;

-  }else{

-    //create an equivalence class iterator in eq class eqc

-    d_eqc.clear();

-    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );

-    d_using_term_db = false;

-  }

-}

-

-Node CandidateGeneratorQE::getNextCandidate(){

-  if( d_term_iter>=0 ){

-    if( d_using_term_db ){

-      //get next candidate term in the uf term database

-      while( d_term_iter<d_term_iter_limit ){

-        Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];

-        d_term_iter++;

-        if( isLegalCandidate( n ) ){

-          return n;

-        }

-      }

-    }else{

-      while( d_term_iter<(int)d_eqc.size() ){

-        Node n = d_eqc[d_term_iter];

-        d_term_iter++;

-        if( n.hasOperator() && n.getOperator()==d_op ){

-          if( isLegalCandidate( n ) ){

-            return n;

-          }

-        }

-      }

-    }

-  }

-  return Node::null();

-}

-

-#endif

-

-//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :

-//  d_qe( qe ), d_eq_class( eqc ){

-//  d_eci = NULL;

-//}

-//void CandidateGeneratorQEDisequal::resetInstantiationRound(){

-//

-//}

-////we will iterate over all terms that are disequal from eqc

-//void CandidateGeneratorQEDisequal::reset( Node eqc ){

-//  //Assert( !eqc.isNull() );

-//  ////begin iterating over equivalence classes that are disequal from eqc

-//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );

-//  //if( d_eci ){

-//  //  d_eqci_iter = d_eci->d_disequal.begin();

-//  //}

-//}

-//Node CandidateGeneratorQEDisequal::getNextCandidate(){

-//  //if( d_eci ){

-//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){

-//  //    if( (*d_eqci_iter).second ){

-//  //      //we have an equivalence class that is disequal from eqc

-//  //      d_cg->reset( (*d_eqci_iter).first );

-//  //      Node n = d_cg->getNextCandidate();

-//  //      //if there is a candidate in this equivalence class, return it

-//  //      if( !n.isNull() ){

-//  //        return n;

-//  //      }

-//  //    }

-//  //    ++d_eqci_iter;

-//  //  }

-//  //}

-//  return Node::null();

-//}

-

-

-CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :

-  d_match_pattern( mpat ), d_qe( qe ){

-

-}

-void CandidateGeneratorQELitEq::resetInstantiationRound(){

-

-}

-void CandidateGeneratorQELitEq::reset( Node eqc ){

-  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );

-}

-Node CandidateGeneratorQELitEq::getNextCandidate(){

-  while( d_eq.isFinished() ){

-    Node n = (*d_eq);

-    ++d_eq;

-    if( n.getType()==d_match_pattern[0].getType() ){

-      //an equivalence class with the same type as the pattern, return reflexive equality

-      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );

-    }

-  }

-  return Node::null();

-}

-

-

-CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :

-  d_match_pattern( mpat ), d_qe( qe ){

-

-}

-void CandidateGeneratorQELitDeq::resetInstantiationRound(){

-

-}

-void CandidateGeneratorQELitDeq::reset( Node eqc ){

-  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );

-  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );

-}

-Node CandidateGeneratorQELitDeq::getNextCandidate(){

-  //get next candidate term in equivalence class

-  while( !d_eqc_false.isFinished() ){

-    Node n = (*d_eqc_false);

-    ++d_eqc_false;

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

-      //found an iff or equality, try to match it

-      //DO_THIS: cache to avoid redundancies?

-      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?

-      return n;

-    }

-  }

-  return Node::null();

-}

+/*********************                                                        */
+/*! \file theory_uf_candidate_generator.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 theory uf candidate generator class
+ **/
+
+#include "theory/candidate_generator.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/inst_match.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::inst;
+
+bool CandidateGenerator::isLegalCandidate( Node n ){
+  return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) );
+}
+
+void CandidateGeneratorQueue::addCandidate( Node n ) {
+  if( isLegalCandidate( n ) ){
+    d_candidates.push_back( n );
+  }
+}
+
+void CandidateGeneratorQueue::reset( Node eqc ){
+  if( d_candidate_index>0 ){
+    d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index );
+    d_candidate_index = 0;
+  }
+  if( !eqc.isNull() ){
+    d_candidates.push_back( eqc );
+  }
+}
+Node CandidateGeneratorQueue::getNextCandidate(){
+  if( d_candidate_index<(int)d_candidates.size() ){
+    Node n = d_candidates[d_candidate_index];
+    d_candidate_index++;
+    return n;
+  }else{
+    d_candidate_index = 0;
+    d_candidates.clear();
+    return Node::null();
+  }
+}
+
+#if 0
+
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
+  d_op( op ), d_qe( qe ), d_term_iter( -2 ){
+  Assert( !d_op.isNull() );
+}
+void CandidateGeneratorQE::resetInstantiationRound(){
+  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
+}
+
+void CandidateGeneratorQE::reset( Node eqc ){
+  if( eqc.isNull() ){
+    d_term_iter = 0;
+  }else{
+    //create an equivalence class iterator in eq class eqc
+    if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){
+      eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc );
+      d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() );
+      d_retNode = Node::null();
+    }else{
+      d_retNode = eqc;
+    }
+    d_term_iter = -1;
+  }
+}
+
+Node CandidateGeneratorQE::getNextCandidate(){
+  if( d_term_iter>=0 ){
+    //get next candidate term in the uf term database
+    while( d_term_iter<d_term_iter_limit ){
+      Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+      d_term_iter++;
+      if( isLegalCandidate( n ) ){
+        return n;
+      }
+    }
+  }else if( d_term_iter==-1 ){
+    if( d_retNode.isNull() ){
+      //get next candidate term in equivalence class
+      while( !d_eqc.isFinished() ){
+        Node n = (*d_eqc);
+        ++d_eqc;
+        if( n.hasOperator() && n.getOperator()==d_op ){
+          if( isLegalCandidate( n ) ){
+            return n;
+          }
+        }
+      }
+    }else{
+      Node ret;
+      if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){
+        ret = d_retNode;
+      }
+      d_term_iter = -2; //done returning matches
+      return ret;
+    }
+  }
+  return Node::null();
+}
+
+#else
+
+
+CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
+  d_op( op ), d_qe( qe ), d_term_iter( -1 ){
+  Assert( !d_op.isNull() );
+}
+void CandidateGeneratorQE::resetInstantiationRound(){
+  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
+}
+
+void CandidateGeneratorQE::reset( Node eqc ){
+  d_term_iter = 0;
+  if( eqc.isNull() ){
+    d_using_term_db = true;
+  }else{
+    //create an equivalence class iterator in eq class eqc
+    d_eqc.clear();
+    d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc );
+    d_using_term_db = false;
+  }
+}
+
+Node CandidateGeneratorQE::getNextCandidate(){
+  if( d_term_iter>=0 ){
+    if( d_using_term_db ){
+      //get next candidate term in the uf term database
+      while( d_term_iter<d_term_iter_limit ){
+        Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter];
+        d_term_iter++;
+        if( isLegalCandidate( n ) ){
+          return n;
+        }
+      }
+    }else{
+      while( d_term_iter<(int)d_eqc.size() ){
+        Node n = d_eqc[d_term_iter];
+        d_term_iter++;
+        if( n.hasOperator() && n.getOperator()==d_op ){
+          if( isLegalCandidate( n ) ){
+            return n;
+          }
+        }
+      }
+    }
+  }
+  return Node::null();
+}
+
+#endif
+
+//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) :
+//  d_qe( qe ), d_eq_class( eqc ){
+//  d_eci = NULL;
+//}
+//void CandidateGeneratorQEDisequal::resetInstantiationRound(){
+//
+//}
+////we will iterate over all terms that are disequal from eqc
+//void CandidateGeneratorQEDisequal::reset( Node eqc ){
+//  //Assert( !eqc.isNull() );
+//  ////begin iterating over equivalence classes that are disequal from eqc
+//  //d_eci = d_ith->getEquivalenceClassInfo( eqc );
+//  //if( d_eci ){
+//  //  d_eqci_iter = d_eci->d_disequal.begin();
+//  //}
+//}
+//Node CandidateGeneratorQEDisequal::getNextCandidate(){
+//  //if( d_eci ){
+//  //  while( d_eqci_iter != d_eci->d_disequal.end() ){
+//  //    if( (*d_eqci_iter).second ){
+//  //      //we have an equivalence class that is disequal from eqc
+//  //      d_cg->reset( (*d_eqci_iter).first );
+//  //      Node n = d_cg->getNextCandidate();
+//  //      //if there is a candidate in this equivalence class, return it
+//  //      if( !n.isNull() ){
+//  //        return n;
+//  //      }
+//  //    }
+//  //    ++d_eqci_iter;
+//  //  }
+//  //}
+//  return Node::null();
+//}
+
+
+CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
+  d_match_pattern( mpat ), d_qe( qe ){
+
+}
+void CandidateGeneratorQELitEq::resetInstantiationRound(){
+
+}
+void CandidateGeneratorQELitEq::reset( Node eqc ){
+  d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+}
+Node CandidateGeneratorQELitEq::getNextCandidate(){
+  while( d_eq.isFinished() ){
+    Node n = (*d_eq);
+    ++d_eq;
+    if( n.getType()==d_match_pattern[0].getType() ){
+      //an equivalence class with the same type as the pattern, return reflexive equality
+      return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+    }
+  }
+  return Node::null();
+}
+
+
+CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
+  d_match_pattern( mpat ), d_qe( qe ){
+
+}
+void CandidateGeneratorQELitDeq::resetInstantiationRound(){
+
+}
+void CandidateGeneratorQELitDeq::reset( Node eqc ){
+  Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) );
+  d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() );
+}
+Node CandidateGeneratorQELitDeq::getNextCandidate(){
+  //get next candidate term in equivalence class
+  while( !d_eqc_false.isFinished() ){
+    Node n = (*d_eqc_false);
+    ++d_eqc_false;
+    if( n.getKind()==d_match_pattern.getKind() ){
+      //found an iff or equality, try to match it
+      //DO_THIS: cache to avoid redundancies?
+      //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
+      return n;
+    }
+  }
+  return Node::null();
+}
diff --git a/src/theory/candidate_generator.h b/src/theory/candidate_generator.h
index 2152f1ef6..134b0e1b7 100644
--- a/src/theory/candidate_generator.h
+++ b/src/theory/candidate_generator.h
@@ -1,187 +1,187 @@
-/*********************                                                        */

-/*! \file candidate_generator.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: none

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

- ** 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 Theory uf candidate generator

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__CANDIDATE_GENERATOR_H

-#define __CVC4__CANDIDATE_GENERATOR_H

-

-#include "theory/theory.h"

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

-

-namespace CVC4 {

-namespace theory {

-

-class QuantifiersEngine;

-

-namespace inst {

-

-/** base class for generating candidates for matching */

-class CandidateGenerator {

-public:

-  CandidateGenerator(){}

-  ~CandidateGenerator(){}

-

-  /** Get candidates functions.  These set up a context to get all match candidates.

-      cg->reset( eqc );

-      do{

-        Node cand = cg->getNextCandidate();

-        //.......

-      }while( !cand.isNull() );

-

-      eqc is the equivalence class you are searching in

-  */

-  virtual void reset( Node eqc ) = 0;

-  virtual Node getNextCandidate() = 0;

-  /** add candidate to list of nodes returned by this generator */

-  virtual void addCandidate( Node n ) {}

-  /** call this at the beginning of each instantiation round */

-  virtual void resetInstantiationRound() = 0;

-public:

-  /** legal candidate */

-  static bool isLegalCandidate( Node n );

-};/* class CandidateGenerator */

-

-/** candidate generator queue (for manual candidate generation) */

-class CandidateGeneratorQueue : public CandidateGenerator {

-private:

-  std::vector< Node > d_candidates;

-  int d_candidate_index;

-public:

-  CandidateGeneratorQueue() : d_candidate_index( 0 ){}

-  ~CandidateGeneratorQueue(){}

-

-  void addCandidate( Node n );

-

-  void resetInstantiationRound(){}

-  void reset( Node eqc );

-  Node getNextCandidate();

-};/* class CandidateGeneratorQueue */

-

-class CandidateGeneratorQEDisequal;

-

-#if 0

-

-class CandidateGeneratorQE : public CandidateGenerator

-{

-  friend class CandidateGeneratorQEDisequal;

-private:

-  //operator you are looking for

-  Node d_op;

-  //instantiator pointer

-  QuantifiersEngine* d_qe;

-  //the equality class iterator

-  eq::EqClassIterator d_eqc;

-  int d_term_iter;

-  int d_term_iter_limit;

-private:

-  Node d_retNode;

-public:

-  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );

-  ~CandidateGeneratorQE(){}

-

-  void resetInstantiationRound();

-  void reset( Node eqc );

-  Node getNextCandidate();

-};

-

-#else

-

-class CandidateGeneratorQE : public CandidateGenerator

-{

-  friend class CandidateGeneratorQEDisequal;

-private:

-  //operator you are looking for

-  Node d_op;

-  //instantiator pointer

-  QuantifiersEngine* d_qe;

-  //the equality class iterator

-  std::vector< Node > d_eqc;

-  int d_term_iter;

-  int d_term_iter_limit;

-  bool d_using_term_db;

-public:

-  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );

-  ~CandidateGeneratorQE(){}

-

-  void resetInstantiationRound();

-  void reset( Node eqc );

-  Node getNextCandidate();

-};

-

-#endif

-

-//class CandidateGeneratorQEDisequal : public CandidateGenerator

-//{

-//private:

-//  //equivalence class

-//  Node d_eq_class;

-//  //equivalence class info

-//  EqClassInfo* d_eci;

-//  //equivalence class iterator

-//  EqClassInfo::BoolMap::const_iterator d_eqci_iter;

-//  //instantiator pointer

-//  QuantifiersEngine* d_qe;

-//public:

-//  CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc );

-//  ~CandidateGeneratorQEDisequal(){}

-//

-//  void resetInstantiationRound();

-//  void reset( Node eqc );   //should be what you want to be disequal from

-//  Node getNextCandidate();

-//};

-

-class CandidateGeneratorQELitEq : public CandidateGenerator

-{

-private:

-  //the equality classes iterator

-  eq::EqClassesIterator d_eq;

-  //equality you are trying to match equalities for

-  Node d_match_pattern;

-  //einstantiator pointer

-  QuantifiersEngine* d_qe;

-public:

-  CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );

-  ~CandidateGeneratorQELitEq(){}

-

-  void resetInstantiationRound();

-  void reset( Node eqc );

-  Node getNextCandidate();

-};

-

-class CandidateGeneratorQELitDeq : public CandidateGenerator

-{

-private:

-  //the equality class iterator for false

-  eq::EqClassIterator d_eqc_false;

-  //equality you are trying to match disequalities for

-  Node d_match_pattern;

-  //einstantiator pointer

-  QuantifiersEngine* d_qe;

-public:

-  CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );

-  ~CandidateGeneratorQELitDeq(){}

-

-  void resetInstantiationRound();

-  void reset( Node eqc );

-  Node getNextCandidate();

-};

-

-}/* CVC4::theory::inst namespace */

-}/* CVC4::theory namespace */

-}/* CVC4 namespace */

-

-#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */

+/*********************                                                        */
+/*! \file candidate_generator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** 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 Theory uf candidate generator
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CANDIDATE_GENERATOR_H
+#define __CVC4__CANDIDATE_GENERATOR_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace inst {
+
+/** base class for generating candidates for matching */
+class CandidateGenerator {
+public:
+  CandidateGenerator(){}
+  ~CandidateGenerator(){}
+
+  /** Get candidates functions.  These set up a context to get all match candidates.
+      cg->reset( eqc );
+      do{
+        Node cand = cg->getNextCandidate();
+        //.......
+      }while( !cand.isNull() );
+
+      eqc is the equivalence class you are searching in
+  */
+  virtual void reset( Node eqc ) = 0;
+  virtual Node getNextCandidate() = 0;
+  /** add candidate to list of nodes returned by this generator */
+  virtual void addCandidate( Node n ) {}
+  /** call this at the beginning of each instantiation round */
+  virtual void resetInstantiationRound() = 0;
+public:
+  /** legal candidate */
+  static bool isLegalCandidate( Node n );
+};/* class CandidateGenerator */
+
+/** candidate generator queue (for manual candidate generation) */
+class CandidateGeneratorQueue : public CandidateGenerator {
+private:
+  std::vector< Node > d_candidates;
+  int d_candidate_index;
+public:
+  CandidateGeneratorQueue() : d_candidate_index( 0 ){}
+  ~CandidateGeneratorQueue(){}
+
+  void addCandidate( Node n );
+
+  void resetInstantiationRound(){}
+  void reset( Node eqc );
+  Node getNextCandidate();
+};/* class CandidateGeneratorQueue */
+
+class CandidateGeneratorQEDisequal;
+
+#if 0
+
+class CandidateGeneratorQE : public CandidateGenerator
+{
+  friend class CandidateGeneratorQEDisequal;
+private:
+  //operator you are looking for
+  Node d_op;
+  //instantiator pointer
+  QuantifiersEngine* d_qe;
+  //the equality class iterator
+  eq::EqClassIterator d_eqc;
+  int d_term_iter;
+  int d_term_iter_limit;
+private:
+  Node d_retNode;
+public:
+  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
+  ~CandidateGeneratorQE(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+#else
+
+class CandidateGeneratorQE : public CandidateGenerator
+{
+  friend class CandidateGeneratorQEDisequal;
+private:
+  //operator you are looking for
+  Node d_op;
+  //instantiator pointer
+  QuantifiersEngine* d_qe;
+  //the equality class iterator
+  std::vector< Node > d_eqc;
+  int d_term_iter;
+  int d_term_iter_limit;
+  bool d_using_term_db;
+public:
+  CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
+  ~CandidateGeneratorQE(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+#endif
+
+//class CandidateGeneratorQEDisequal : public CandidateGenerator
+//{
+//private:
+//  //equivalence class
+//  Node d_eq_class;
+//  //equivalence class info
+//  EqClassInfo* d_eci;
+//  //equivalence class iterator
+//  EqClassInfo::BoolMap::const_iterator d_eqci_iter;
+//  //instantiator pointer
+//  QuantifiersEngine* d_qe;
+//public:
+//  CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc );
+//  ~CandidateGeneratorQEDisequal(){}
+//
+//  void resetInstantiationRound();
+//  void reset( Node eqc );   //should be what you want to be disequal from
+//  Node getNextCandidate();
+//};
+
+class CandidateGeneratorQELitEq : public CandidateGenerator
+{
+private:
+  //the equality classes iterator
+  eq::EqClassesIterator d_eq;
+  //equality you are trying to match equalities for
+  Node d_match_pattern;
+  //einstantiator pointer
+  QuantifiersEngine* d_qe;
+public:
+  CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
+  ~CandidateGeneratorQELitEq(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+class CandidateGeneratorQELitDeq : public CandidateGenerator
+{
+private:
+  //the equality class iterator for false
+  eq::EqClassIterator d_eqc_false;
+  //equality you are trying to match disequalities for
+  Node d_match_pattern;
+  //einstantiator pointer
+  QuantifiersEngine* d_qe;
+public:
+  CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
+  ~CandidateGeneratorQELitDeq(){}
+
+  void resetInstantiationRound();
+  void reset( Node eqc );
+  Node getNextCandidate();
+};
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY_UF_INSTANTIATOR_H */
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp
index c90483fa3..bad7e34cb 100644
--- a/src/theory/inst_match.cpp
+++ b/src/theory/inst_match.cpp
@@ -272,9 +272,6 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
 
   Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
 
-  //get the equality engine
-  Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF );
-  uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
   //create candidate generator
   if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
     Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index aa2c2d938..feedc0c31 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -1,615 +1,615 @@
-/*********************                                                        */

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

- **/

-

-#include "theory/model.h"

-#include "theory/quantifiers_engine.h"

-#include "theory/theory_engine.h"

-#include "util/datatype.h"

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

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-

-void RepSet::clear(){

-  d_type_reps.clear();

-  d_tmap.clear();

-}

-

-void RepSet::add( Node n ){

-  TypeNode t = n.getType();

-  d_tmap[ n ] = (int)d_type_reps[t].size();

-  d_type_reps[t].push_back( n );

-}

-

-void RepSet::set( TypeNode t, std::vector< Node >& reps ){

-  for( size_t i=0; i<reps.size(); i++ ){

-    d_tmap[ reps[i] ] = i;

-  }

-  d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() );

-}

-

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

-#if 0

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

-    out << it->first << " : " << std::endl;

-    for( int i=0; i<(int)it->second.size(); i++ ){

-      out << "   " << i << ": " << it->second[i] << std::endl;

-    }

-  }

-#else

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

-    if( !it->first.isFunction() && !it->first.isPredicate() ){

-      out << "(" << it->first << " " << it->second.size();

-      out << " (";

-      for( int i=0; i<(int)it->second.size(); i++ ){

-        if( i>0 ){ out << " "; }

-        out << it->second[i];

-      }

-      out << ")";

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

-    }

-  }

-#endif

-}

-

-TheoryModel::TheoryModel( context::Context* c, std::string name ) :

-d_equalityEngine( c, name ){

-  d_true = NodeManager::currentNM()->mkConst( true );

-  d_false = NodeManager::currentNM()->mkConst( false );

-}

-

-void TheoryModel::reset(){

-  d_reps.clear();

-  d_rep_set.clear();

-}

-

-void TheoryModel::addDefineFunction( Node n ){

-  d_define_funcs.push_back( n );

-  d_defines.push_back( 0 );

-}

-

-void TheoryModel::addDefineType( TypeNode tn ){

-  d_define_types.push_back( tn );

-  d_defines.push_back( 1 );

-}

-

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

-  out << "(" << n;

-  out << " : " << n.getType();

-  out << " ";

-  Node value = getValue( n );

-  /*

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

-    int index = d_rep_set.getIndexFor( value );

-    if( index!=-1 ){

-      out << value.getType() << "_" << index;

-    }else{

-      out << value;

-    }

-  }else{

-  */

-  out << value;

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

-}

-

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

-  out << "(" << tn;

-  if( tn.isSort() ){

-    if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){

-      out << " " << d_rep_set.d_type_reps[tn].size();

-      //out << " (";

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

-      //  if( i>0 ){ out << " "; }

-      //  out << d_rep_set.d_type_reps[tn][i];

-      //}

-      //out << ")";

-    }

-  }

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

-}

-

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

-  /*//for debugging

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

-  while( !eqcs_i.isFinished() ){

-    Node eqc = (*eqcs_i);

-    Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl;

-    out << "   ";

-    //add terms to model

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

-    while( !eqc_i.isFinished() ){

-      out << (*eqc_i) << " ";

-      ++eqc_i;

-    }

-    out << std::endl;

-    ++eqcs_i;

-  }

-  */

-  int funcIndex = 0;

-  int typeIndex = 0;

-  for( size_t i=0; i<d_defines.size(); i++ ){

-    if( d_defines[i]==0 ){

-      toStreamFunction( d_define_funcs[funcIndex], out );

-      funcIndex++;

-    }else if( d_defines[i]==1 ){

-      toStreamType( d_define_types[typeIndex], out );

-      typeIndex++;

-    }

-  }

-}

-

-Node TheoryModel::getValue( TNode n ){

-  Debug("model") << "TheoryModel::getValue " << n << std::endl;

-

-  kind::MetaKind metakind = n.getMetaKind();

-

-  //// special case: prop engine handles boolean vars

-  //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) {

-  //  Debug("model") << "-> Propositional variable." << std::endl;

-  //  return d_te->getPropEngine()->getValue( n );

-  //}

-

-  // special case: value of a constant == itself

-  if(metakind == kind::metakind::CONSTANT) {

-    Debug("model") << "-> Constant." << std::endl;

-    return n;

-  }

-

-  Node nn;

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

-    std::vector< Node > children;

-    if( metakind == kind::metakind::PARAMETERIZED ){

-      Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;

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

-    }

-    //evaluate the children

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

-      Node val = getValue( n[i] );

-      Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;

-      Assert( !val.isNull() );

-      children.push_back( val );

-    }

-    Debug("model-debug") << "Done eval children" << std::endl;

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

-  }else{

-    nn = n;

-  }

-  //interpretation is the rewritten form

-  nn = Rewriter::rewrite( nn );

-

-  // special case: value of a constant == itself

-  if(metakind == kind::metakind::CONSTANT) {

-    Debug("model") << "-> Theory-interpreted term." << std::endl;

-    return nn;

-  }else{

-    Debug("model") << "-> Model-interpreted term." << std::endl;

-    //otherwise, get the interpreted value in the model

-    return getInterpretedValue( nn );

-  }

-}

-

-Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){

-  if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){

-    //try to find a pre-existing arbitrary element

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

-      if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){

-        return d_rep_set.d_type_reps[tn][i];

-      }

-    }

-  }

-  return Node::null();

-}

-

-//FIXME: use the theory enumerator to generate constants here

-Node TheoryModel::getNewDomainValue( TypeNode tn ){

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

-    if( d_rep_set.d_type_reps[tn].empty() ){

-      return d_false;

-    }else if( d_rep_set.d_type_reps[tn].size()==1 ){

-      return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) );

-    }else{

-      return Node::null();

-    }

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

-    int val = 0;

-    do{

-      Node r = NodeManager::currentNM()->mkConst( Rational(val) );

-      if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() &&

-          !d_equalityEngine.hasTerm( r ) ){

-        return r;

-      }

-      val++;

-    }while( true );

-  }else{

-    //otherwise must make a variable  FIXME: how to make constants for other sorts?

-    //return NodeManager::currentNM()->mkVar( tn );

-    return Node::null();

-  }

-}

-

-/** assert equality */

-void TheoryModel::assertEquality( Node a, Node b, bool polarity ){

-  d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );

-}

-

-/** assert predicate */

-void TheoryModel::assertPredicate( Node a, bool polarity ){

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

-    d_equalityEngine.assertEquality( a, polarity, Node::null() );

-  }else{

-    d_equalityEngine.assertPredicate( a, polarity, Node::null() );

-  }

-}

-

-/** assert equality engine */

-void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){

-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );

-  while( !eqcs_i.isFinished() ){

-    Node eqc = (*eqcs_i);

-    bool predicate = false;

-    bool predPolarity = false;

-    if( eqc.getType()==NodeManager::currentNM()->booleanType() ){

-      predicate = true;

-      predPolarity = ee->areEqual( eqc, d_true );

-      //FIXME: do we guarentee that all boolean equivalence classes contain either d_true or d_false?

-    }

-    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );

-    while( !eqc_i.isFinished() ){

-      if( predicate ){

-        assertPredicate( *eqc_i, predPolarity );

-      }else{

-        assertEquality( *eqc_i, eqc, true );

-      }

-      ++eqc_i;

-    }

-    ++eqcs_i;

-  }

-}

-

-bool TheoryModel::hasTerm( Node a ){

-  return d_equalityEngine.hasTerm( a );

-}

-

-Node TheoryModel::getRepresentative( Node a ){

-  if( d_equalityEngine.hasTerm( a ) ){

-    Node r = d_equalityEngine.getRepresentative( a );

-    return d_reps[ r ];

-  }else{

-    return a;

-  }

-}

-

-bool TheoryModel::areEqual( Node a, Node b ){

-  if( a==b ){

-    return true;

-  }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){

-    return d_equalityEngine.areEqual( a, b );

-  }else{

-    return false;

-  }

-}

-

-bool TheoryModel::areDisequal( Node a, Node b ){

-  if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){

-    return d_equalityEngine.areDisequal( a, b, false );

-  }else{

-    return false;

-  }

-}

-

-//for debugging

-void TheoryModel::printRepresentativeDebug( const char* c, Node r ){

-  if( r.isNull() ){

-    Debug( c ) << "null";

-  }else if( r.getType()==NodeManager::currentNM()->booleanType() ){

-    if( areEqual( r, d_true ) ){

-      Debug( c ) << "true";

-    }else{

-      Debug( c ) << "false";

-    }

-  }else{

-    Debug( c ) << getRepresentative( r );

-  }

-}

-

-void TheoryModel::printRepresentative( std::ostream& out, Node r ){

-  Assert( !r.isNull() );

-  if( r.isNull() ){

-    out << "null";

-  }else if( r.getType()==NodeManager::currentNM()->booleanType() ){

-    if( areEqual( r, d_true ) ){

-      out  << "true";

-    }else{

-      out  << "false";

-    }

-  }else{

-    out << getRepresentative( r );

-  }

-}

-

-DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) :

-TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){

-

-}

-

-void DefaultModel::addTerm( Node n ){

-  //must collect UF terms

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

-    d_uf_terms[ n.getOperator() ].push_back( n );

-  }

-}

-

-void DefaultModel::reset(){

-  d_uf_terms.clear();

-  d_uf_models.clear();

-  TheoryModel::reset();

-}

-

-Node DefaultModel::getInterpretedValue( TNode n ){

-  TypeNode type = n.getType();

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

-    //for function models

-    if( d_enableFuncModels ){

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

-        uf::UfModelTree ufmt( n );

-        Node default_v;

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

-          Node un = d_uf_terms[n][i];

-          Node v = getRepresentative( un );

-          ufmt.setValue( this, un, v );

-          default_v = v;

-        }

-        if( default_v.isNull() ){

-          default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) );

-        }

-        ufmt.setDefaultValue( this, default_v );

-        ufmt.simplify();

-        d_uf_models[n] = ufmt.getFunctionValue();

-      }

-      return d_uf_models[n];

-    }else{

-      return n;

-    }

-  }else{

-    //first, see if the representative is defined

-    if( d_equalityEngine.hasTerm( n ) ){

-      n = d_equalityEngine.getRepresentative( n );

-      //this check is required since d_equalityEngine.hasTerm( n )

-      // does not ensure that n is in an equivalence class in d_equalityEngine

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

-        return d_reps[n];

-      }

-    }

-    //second, try to choose an existing term as value

-    std::vector< Node > v_emp;

-    Node n2 = getDomainValue( type, v_emp );

-    if( !n2.isNull() ){

-      return n2;

-    }else{

-      //otherwise, choose new value

-      n2 = getNewDomainValue( type );

-      if( !n2.isNull() ){

-        return n2;

-      }else{

-        //otherwise, just return itself

-        return n;

-      }

-    }

-  }

-}

-

-TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){

-

-}

-

-void TheoryEngineModelBuilder::buildModel( Model* m ){

-  TheoryModel* tm = (TheoryModel*)m;

-  //reset representative information

-  tm->reset();

-  //collect model info from the theory engine

-  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Collect model info..." << std::endl;

-  d_te->collectModelInfo( tm );

-  //unresolved equivalence classes

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

-  std::map< TypeNode, bool > unresolved_types;

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

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

-  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Build representatives..." << std::endl;

-  //populate term database, store constant representatives

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

-  while( !eqcs_i.isFinished() ){

-    Node eqc = (*eqcs_i);

-    TypeNode eqct = eqc.getType();

-    //initialize unresolved type information

-    initializeType( eqct, unresolved_types );

-    //add terms to model, get constant rep if possible

-    Node const_rep;

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

-    while( !eqc_i.isFinished() ){

-      Node n = *eqc_i;

-      //check if this is constant, if so, we will use it as representative

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

-        const_rep = n;

-      }

-      //theory-specific information needed

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

-        selects[ n[0] ].push_back( n );

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

-        apply_constructors[ eqc ] = n;

-      }

-      //model-specific processing of the term, this will include

-      tm->addTerm( n );

-      ++eqc_i;

-    }

-    //store representative in representative set

-    if( !const_rep.isNull() ){

-      //Message() << "Constant rep " << const_rep << " for " << eqc << std::endl;

-      tm->d_reps[ eqc ] = const_rep;

-      tm->d_rep_set.add( const_rep );

-    }else{

-      //Message() << "** unresolved eqc " << eqc << std::endl;

-      unresolved_eqc[ eqc ] = true;

-      unresolved_types[ eqct ] = true;

-    }

-    ++eqcs_i;

-  }

-  //choose representatives for unresolved equivalence classes

-  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Complete model..." << std::endl;

-  bool fixedPoint;

-  do{

-    fixedPoint = true;

-    //for calculating unresolved types

-    std::map< TypeNode, bool > unresolved_types_next;

-    for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){

-      unresolved_types_next[ it->first ] = false;

-    }

-    //try to resolve each unresolved equivalence class

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

-      if( it->second ){

-        Node n = it->first;

-        TypeNode tn = n.getType();

-        Node rep;

-        bool mkRep = true;

-        if( tn.isArray() ){

-          TypeNode index_t = tn.getArrayIndexType();

-          TypeNode elem_t = tn.getArrayConstituentType();

-          if( !unresolved_types[ index_t ] && !unresolved_types[ elem_t ] ){

-            //collect all relevant set values of n

-            std::vector< Node > arr_selects;

-            std::vector< Node > arr_select_values;

-            Node nbase = n;

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

-              arr_selects.push_back( tm->getRepresentative( nbase[1] ) );

-              arr_select_values.push_back( tm->getRepresentative( nbase[2] ) );

-              nbase = nbase[0];

-            }

-            eq::EqClassIterator eqc_i = eq::EqClassIterator( n, &tm->d_equalityEngine );

-            while( !eqc_i.isFinished() ){

-              for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){

-                Node r = tm->getRepresentative( selects[ *eqc_i ][i][1] );

-                if( std::find( arr_selects.begin(), arr_selects.end(), r )==arr_selects.end() ){

-                  arr_selects.push_back( r );

-                  arr_select_values.push_back( tm->getRepresentative( selects[ *eqc_i ][i] ) );

-                }

-              }

-              ++eqc_i;

-            }

-            //now, construct based on select/value pairs

-            //TODO: make this a constant

-            rep = chooseRepresentative( tm, nbase );

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

-              rep = NodeManager::currentNM()->mkNode( STORE, rep, arr_selects[i], arr_select_values[i] );

-            }

-          }

-          mkRep = false;

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

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

-            Node ac = apply_constructors[n];

-            std::vector< Node > children;

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

-            for( size_t i = 0; i<ac.getNumChildren(); i++ ){

-              Node acir = ac[i];

-              if( tm->d_equalityEngine.hasTerm( acir ) ){

-                acir = tm->d_equalityEngine.getRepresentative( acir );

-              }

-              if( unresolved_eqc.find( acir )==unresolved_eqc.end() ){

-                Message() << "TheoryEngineModelBuilder::buildModel : Datatype argument does not exist in the model " << acir << std::endl;

-                acir = Node::null();

-              }

-              if( acir.isNull() || unresolved_eqc[ acir ] ){

-                mkRep = false;

-                break;

-              }else{

-                children.push_back( tm->getRepresentative( acir ) );

-              }

-            }

-            if( mkRep ){

-              rep = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );

-            }

-          }else{

-            Message() << "TheoryEngineModelBuilder::buildModel : Do not know how to resolve datatype equivalence class " << n << std::endl;

-          }

-          mkRep = false;

-        }

-        if( mkRep ){

-          rep = chooseRepresentative( tm, n );

-        }

-        if( !rep.isNull() ){

-          tm->assertEquality( n, rep, true );

-          tm->d_reps[ n ] = rep;

-          tm->d_rep_set.add( rep );

-          unresolved_eqc[ n ] = false;

-          fixedPoint = false;

-        }else{

-          unresolved_types_next[ tn ] = true;

-        }

-      }

-    }

-    //for calculating unresolved types

-    for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){

-      unresolved_types[ it->first ] = unresolved_types_next[ it->first ];

-    }

-  }while( !fixedPoint );

-

-  //for all unresolved equivalence classes, just get new domain value

-  //  this should typically never happen (all equivalence classes should be resolved at this point)

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

-    if( it->second ){

-      Node n = it->first;

-      Node rep = chooseRepresentative( tm, n );

-      tm->assertEquality( n, rep, true );

-      tm->d_reps[ n ] = rep;

-      tm->d_rep_set.add( rep );

-      //FIXME: Assertion failure here?

-      Message() << "Warning : Unresolved eqc, assigning " << rep << " for eqc( " << n << " ), type = " << n.getType() << std::endl;

-    }

-  }

-

-  //model-specific initialization

-  processBuildModel( tm );

-}

-

-void TheoryEngineModelBuilder::initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ){

-  if( unresolved_types.find( tn )==unresolved_types.end() ){

-    unresolved_types[tn] = false;

-    if( tn.isArray() ){

-      initializeType( tn.getArrayIndexType(), unresolved_types );

-      initializeType( tn.getArrayConstituentType(), unresolved_types );

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

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

-      for( size_t i = 0; i<dt.getNumConstructors(); i++ ){

-        for( size_t j = 0; j<dt[i].getNumArgs(); j++ ){

-          initializeType( TypeNode::fromType( dt[i][j].getType() ), unresolved_types );

-        }

-      }

-    }

-  }

-}

-

-Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){

-  //try to get a new domain value

-  Node rep = m->getNewDomainValue( eqc.getType() );

-  if( !rep.isNull() ){

-    return rep;

-  }else{

-    //if we can't get new domain value, just return eqc itself (this typically should not happen)

-    //FIXME: Assertion failure here?

-    return eqc;

-  }

-}

+/*********************                                                        */
+/*! \file 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 class
+ **/
+
+#include "theory/model.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "util/datatype.h"
+#include "theory/uf/theory_uf_model.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+
+void RepSet::clear(){
+  d_type_reps.clear();
+  d_tmap.clear();
+}
+
+void RepSet::add( Node n ){
+  TypeNode t = n.getType();
+  d_tmap[ n ] = (int)d_type_reps[t].size();
+  d_type_reps[t].push_back( n );
+}
+
+void RepSet::set( TypeNode t, std::vector< Node >& reps ){
+  for( size_t i=0; i<reps.size(); i++ ){
+    d_tmap[ reps[i] ] = i;
+  }
+  d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() );
+}
+
+void RepSet::toStream(std::ostream& out){
+#if 0
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
+    out << it->first << " : " << std::endl;
+    for( int i=0; i<(int)it->second.size(); i++ ){
+      out << "   " << i << ": " << it->second[i] << std::endl;
+    }
+  }
+#else
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
+    if( !it->first.isFunction() && !it->first.isPredicate() ){
+      out << "(" << it->first << " " << it->second.size();
+      out << " (";
+      for( int i=0; i<(int)it->second.size(); i++ ){
+        if( i>0 ){ out << " "; }
+        out << it->second[i];
+      }
+      out << ")";
+      out << ")" << std::endl;
+    }
+  }
+#endif
+}
+
+TheoryModel::TheoryModel( context::Context* c, std::string name ) :
+d_equalityEngine( c, name ){
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+void TheoryModel::reset(){
+  d_reps.clear();
+  d_rep_set.clear();
+}
+
+void TheoryModel::addDefineFunction( Node n ){
+  d_define_funcs.push_back( n );
+  d_defines.push_back( 0 );
+}
+
+void TheoryModel::addDefineType( TypeNode tn ){
+  d_define_types.push_back( tn );
+  d_defines.push_back( 1 );
+}
+
+void TheoryModel::toStreamFunction( Node n, std::ostream& out ){
+  out << "(" << n;
+  out << " : " << n.getType();
+  out << " ";
+  Node value = getValue( n );
+  /*
+  if( n.getType().isSort() ){
+    int index = d_rep_set.getIndexFor( value );
+    if( index!=-1 ){
+      out << value.getType() << "_" << index;
+    }else{
+      out << value;
+    }
+  }else{
+  */
+  out << value;
+  out << ")" << std::endl;
+}
+
+void TheoryModel::toStreamType( TypeNode tn, std::ostream& out ){
+  out << "(" << tn;
+  if( tn.isSort() ){
+    if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
+      out << " " << d_rep_set.d_type_reps[tn].size();
+      //out << " (";
+      //for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
+      //  if( i>0 ){ out << " "; }
+      //  out << d_rep_set.d_type_reps[tn][i];
+      //}
+      //out << ")";
+    }
+  }
+  out << ")" << std::endl;
+}
+
+void TheoryModel::toStream( std::ostream& out ){
+  /*//for debugging
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    Debug("get-model-debug") << eqc << " : " << eqc.getType() << " : " << std::endl;
+    out << "   ";
+    //add terms to model
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      out << (*eqc_i) << " ";
+      ++eqc_i;
+    }
+    out << std::endl;
+    ++eqcs_i;
+  }
+  */
+  int funcIndex = 0;
+  int typeIndex = 0;
+  for( size_t i=0; i<d_defines.size(); i++ ){
+    if( d_defines[i]==0 ){
+      toStreamFunction( d_define_funcs[funcIndex], out );
+      funcIndex++;
+    }else if( d_defines[i]==1 ){
+      toStreamType( d_define_types[typeIndex], out );
+      typeIndex++;
+    }
+  }
+}
+
+Node TheoryModel::getValue( TNode n ){
+  Debug("model") << "TheoryModel::getValue " << n << std::endl;
+
+  kind::MetaKind metakind = n.getMetaKind();
+
+  //// special case: prop engine handles boolean vars
+  //if(metakind == kind::metakind::VARIABLE && n.getType().isBoolean()) {
+  //  Debug("model") << "-> Propositional variable." << std::endl;
+  //  return d_te->getPropEngine()->getValue( n );
+  //}
+
+  // special case: value of a constant == itself
+  if(metakind == kind::metakind::CONSTANT) {
+    Debug("model") << "-> Constant." << std::endl;
+    return n;
+  }
+
+  Node nn;
+  if( n.getNumChildren()>0 ){
+    std::vector< Node > children;
+    if( metakind == kind::metakind::PARAMETERIZED ){
+      Debug("model-debug") << "get operator: " << n.getOperator() << std::endl;
+      children.push_back( n.getOperator() );
+    }
+    //evaluate the children
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      Node val = getValue( n[i] );
+      Debug("model-debug") << i << " : " << n[i] << " -> " << val << std::endl;
+      Assert( !val.isNull() );
+      children.push_back( val );
+    }
+    Debug("model-debug") << "Done eval children" << std::endl;
+    nn = NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }else{
+    nn = n;
+  }
+  //interpretation is the rewritten form
+  nn = Rewriter::rewrite( nn );
+
+  // special case: value of a constant == itself
+  if(metakind == kind::metakind::CONSTANT) {
+    Debug("model") << "-> Theory-interpreted term." << std::endl;
+    return nn;
+  }else{
+    Debug("model") << "-> Model-interpreted term." << std::endl;
+    //otherwise, get the interpreted value in the model
+    return getInterpretedValue( nn );
+  }
+}
+
+Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
+  if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){
+    //try to find a pre-existing arbitrary element
+    for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){
+      if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){
+        return d_rep_set.d_type_reps[tn][i];
+      }
+    }
+  }
+  return Node::null();
+}
+
+//FIXME: use the theory enumerator to generate constants here
+Node TheoryModel::getNewDomainValue( TypeNode tn ){
+  if( tn==NodeManager::currentNM()->booleanType() ){
+    if( d_rep_set.d_type_reps[tn].empty() ){
+      return d_false;
+    }else if( d_rep_set.d_type_reps[tn].size()==1 ){
+      return NodeManager::currentNM()->mkConst( areEqual( d_rep_set.d_type_reps[tn][0], d_false ) );
+    }else{
+      return Node::null();
+    }
+  }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+    int val = 0;
+    do{
+      Node r = NodeManager::currentNM()->mkConst( Rational(val) );
+      if( std::find( d_rep_set.d_type_reps[tn].begin(), d_rep_set.d_type_reps[tn].end(), r )==d_rep_set.d_type_reps[tn].end() &&
+          !d_equalityEngine.hasTerm( r ) ){
+        return r;
+      }
+      val++;
+    }while( true );
+  }else{
+    //otherwise must make a variable  FIXME: how to make constants for other sorts?
+    //return NodeManager::currentNM()->mkVar( tn );
+    return Node::null();
+  }
+}
+
+/** assert equality */
+void TheoryModel::assertEquality( Node a, Node b, bool polarity ){
+  d_equalityEngine.assertEquality( a.eqNode(b), polarity, Node::null() );
+}
+
+/** assert predicate */
+void TheoryModel::assertPredicate( Node a, bool polarity ){
+  if( a.getKind()==EQUAL ){
+    d_equalityEngine.assertEquality( a, polarity, Node::null() );
+  }else{
+    d_equalityEngine.assertPredicate( a, polarity, Node::null() );
+  }
+}
+
+/** assert equality engine */
+void TheoryModel::assertEqualityEngine( eq::EqualityEngine* ee ){
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    bool predicate = false;
+    bool predPolarity = false;
+    if( eqc.getType()==NodeManager::currentNM()->booleanType() ){
+      predicate = true;
+      predPolarity = ee->areEqual( eqc, d_true );
+      //FIXME: do we guarentee that all boolean equivalence classes contain either d_true or d_false?
+    }
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );
+    while( !eqc_i.isFinished() ){
+      if( predicate ){
+        assertPredicate( *eqc_i, predPolarity );
+      }else{
+        assertEquality( *eqc_i, eqc, true );
+      }
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+}
+
+bool TheoryModel::hasTerm( Node a ){
+  return d_equalityEngine.hasTerm( a );
+}
+
+Node TheoryModel::getRepresentative( Node a ){
+  if( d_equalityEngine.hasTerm( a ) ){
+    Node r = d_equalityEngine.getRepresentative( a );
+    return d_reps[ r ];
+  }else{
+    return a;
+  }
+}
+
+bool TheoryModel::areEqual( Node a, Node b ){
+  if( a==b ){
+    return true;
+  }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
+    return d_equalityEngine.areEqual( a, b );
+  }else{
+    return false;
+  }
+}
+
+bool TheoryModel::areDisequal( Node a, Node b ){
+  if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
+    return d_equalityEngine.areDisequal( a, b, false );
+  }else{
+    return false;
+  }
+}
+
+//for debugging
+void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
+  if( r.isNull() ){
+    Debug( c ) << "null";
+  }else if( r.getType()==NodeManager::currentNM()->booleanType() ){
+    if( areEqual( r, d_true ) ){
+      Debug( c ) << "true";
+    }else{
+      Debug( c ) << "false";
+    }
+  }else{
+    Debug( c ) << getRepresentative( r );
+  }
+}
+
+void TheoryModel::printRepresentative( std::ostream& out, Node r ){
+  Assert( !r.isNull() );
+  if( r.isNull() ){
+    out << "null";
+  }else if( r.getType()==NodeManager::currentNM()->booleanType() ){
+    if( areEqual( r, d_true ) ){
+      out  << "true";
+    }else{
+      out  << "false";
+    }
+  }else{
+    out << getRepresentative( r );
+  }
+}
+
+DefaultModel::DefaultModel( context::Context* c, std::string name, bool enableFuncModels ) :
+TheoryModel( c, name ), d_enableFuncModels( enableFuncModels ){
+
+}
+
+void DefaultModel::addTerm( Node n ){
+  //must collect UF terms
+  if( d_enableFuncModels && n.getKind()==APPLY_UF ){
+    d_uf_terms[ n.getOperator() ].push_back( n );
+  }
+}
+
+void DefaultModel::reset(){
+  d_uf_terms.clear();
+  d_uf_models.clear();
+  TheoryModel::reset();
+}
+
+Node DefaultModel::getInterpretedValue( TNode n ){
+  TypeNode type = n.getType();
+  if( type.isFunction() || type.isPredicate() ){
+    //for function models
+    if( d_enableFuncModels ){
+      if( d_uf_models.find( n )==d_uf_models.end() ){
+        uf::UfModelTree ufmt( n );
+        Node default_v;
+        for( size_t i=0; i<d_uf_terms[n].size(); i++ ){
+          Node un = d_uf_terms[n][i];
+          Node v = getRepresentative( un );
+          ufmt.setValue( this, un, v );
+          default_v = v;
+        }
+        if( default_v.isNull() ){
+          default_v = getInterpretedValue( NodeManager::currentNM()->mkVar( type.getRangeType() ) );
+        }
+        ufmt.setDefaultValue( this, default_v );
+        ufmt.simplify();
+        d_uf_models[n] = ufmt.getFunctionValue();
+      }
+      return d_uf_models[n];
+    }else{
+      return n;
+    }
+  }else{
+    //first, see if the representative is defined
+    if( d_equalityEngine.hasTerm( n ) ){
+      n = d_equalityEngine.getRepresentative( n );
+      //this check is required since d_equalityEngine.hasTerm( n )
+      // does not ensure that n is in an equivalence class in d_equalityEngine
+      if( d_reps.find( n )!=d_reps.end() ){
+        return d_reps[n];
+      }
+    }
+    //second, try to choose an existing term as value
+    std::vector< Node > v_emp;
+    Node n2 = getDomainValue( type, v_emp );
+    if( !n2.isNull() ){
+      return n2;
+    }else{
+      //otherwise, choose new value
+      n2 = getNewDomainValue( type );
+      if( !n2.isNull() ){
+        return n2;
+      }else{
+        //otherwise, just return itself
+        return n;
+      }
+    }
+  }
+}
+
+TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
+
+}
+
+void TheoryEngineModelBuilder::buildModel( Model* m ){
+  TheoryModel* tm = (TheoryModel*)m;
+  //reset representative information
+  tm->reset();
+  //collect model info from the theory engine
+  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
+  d_te->collectModelInfo( tm );
+  //unresolved equivalence classes
+  std::map< Node, bool > unresolved_eqc;
+  std::map< TypeNode, bool > unresolved_types;
+  std::map< Node, std::vector< Node > > selects;
+  std::map< Node, Node > apply_constructors;
+  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Build representatives..." << std::endl;
+  //populate term database, store constant representatives
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &tm->d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    TypeNode eqct = eqc.getType();
+    //initialize unresolved type information
+    initializeType( eqct, unresolved_types );
+    //add terms to model, get constant rep if possible
+    Node const_rep;
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &tm->d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      Node n = *eqc_i;
+      //check if this is constant, if so, we will use it as representative
+      if( n.getMetaKind()==kind::metakind::CONSTANT ){
+        const_rep = n;
+      }
+      //theory-specific information needed
+      if( n.getKind()==SELECT ){
+        selects[ n[0] ].push_back( n );
+      }else if( n.getKind()==APPLY_CONSTRUCTOR ){
+        apply_constructors[ eqc ] = n;
+      }
+      //model-specific processing of the term, this will include
+      tm->addTerm( n );
+      ++eqc_i;
+    }
+    //store representative in representative set
+    if( !const_rep.isNull() ){
+      //Message() << "Constant rep " << const_rep << " for " << eqc << std::endl;
+      tm->d_reps[ eqc ] = const_rep;
+      tm->d_rep_set.add( const_rep );
+    }else{
+      //Message() << "** unresolved eqc " << eqc << std::endl;
+      unresolved_eqc[ eqc ] = true;
+      unresolved_types[ eqct ] = true;
+    }
+    ++eqcs_i;
+  }
+  //choose representatives for unresolved equivalence classes
+  Debug( "model-builder" ) << "TheoryEngineModelBuilder: Complete model..." << std::endl;
+  bool fixedPoint;
+  do{
+    fixedPoint = true;
+    //for calculating unresolved types
+    std::map< TypeNode, bool > unresolved_types_next;
+    for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){
+      unresolved_types_next[ it->first ] = false;
+    }
+    //try to resolve each unresolved equivalence class
+    for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){
+      if( it->second ){
+        Node n = it->first;
+        TypeNode tn = n.getType();
+        Node rep;
+        bool mkRep = true;
+        if( tn.isArray() ){
+          TypeNode index_t = tn.getArrayIndexType();
+          TypeNode elem_t = tn.getArrayConstituentType();
+          if( !unresolved_types[ index_t ] && !unresolved_types[ elem_t ] ){
+            //collect all relevant set values of n
+            std::vector< Node > arr_selects;
+            std::vector< Node > arr_select_values;
+            Node nbase = n;
+            while( nbase.getKind()==STORE ){
+              arr_selects.push_back( tm->getRepresentative( nbase[1] ) );
+              arr_select_values.push_back( tm->getRepresentative( nbase[2] ) );
+              nbase = nbase[0];
+            }
+            eq::EqClassIterator eqc_i = eq::EqClassIterator( n, &tm->d_equalityEngine );
+            while( !eqc_i.isFinished() ){
+              for( int i=0; i<(int)selects[ *eqc_i ].size(); i++ ){
+                Node r = tm->getRepresentative( selects[ *eqc_i ][i][1] );
+                if( std::find( arr_selects.begin(), arr_selects.end(), r )==arr_selects.end() ){
+                  arr_selects.push_back( r );
+                  arr_select_values.push_back( tm->getRepresentative( selects[ *eqc_i ][i] ) );
+                }
+              }
+              ++eqc_i;
+            }
+            //now, construct based on select/value pairs
+            //TODO: make this a constant
+            rep = chooseRepresentative( tm, nbase );
+            for( int i=0; i<(int)arr_selects.size(); i++ ){
+              rep = NodeManager::currentNM()->mkNode( STORE, rep, arr_selects[i], arr_select_values[i] );
+            }
+          }
+          mkRep = false;
+        }else if( tn.isDatatype() ){
+          if( apply_constructors.find( n )!=apply_constructors.end() ){
+            Node ac = apply_constructors[n];
+            std::vector< Node > children;
+            children.push_back( ac.getOperator() );
+            for( size_t i = 0; i<ac.getNumChildren(); i++ ){
+              Node acir = ac[i];
+              if( tm->d_equalityEngine.hasTerm( acir ) ){
+                acir = tm->d_equalityEngine.getRepresentative( acir );
+              }
+              if( unresolved_eqc.find( acir )==unresolved_eqc.end() ){
+                Message() << "TheoryEngineModelBuilder::buildModel : Datatype argument does not exist in the model " << acir << std::endl;
+                acir = Node::null();
+              }
+              if( acir.isNull() || unresolved_eqc[ acir ] ){
+                mkRep = false;
+                break;
+              }else{
+                children.push_back( tm->getRepresentative( acir ) );
+              }
+            }
+            if( mkRep ){
+              rep = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+            }
+          }else{
+            Message() << "TheoryEngineModelBuilder::buildModel : Do not know how to resolve datatype equivalence class " << n << std::endl;
+          }
+          mkRep = false;
+        }
+        if( mkRep ){
+          rep = chooseRepresentative( tm, n );
+        }
+        if( !rep.isNull() ){
+          tm->assertEquality( n, rep, true );
+          tm->d_reps[ n ] = rep;
+          tm->d_rep_set.add( rep );
+          unresolved_eqc[ n ] = false;
+          fixedPoint = false;
+        }else{
+          unresolved_types_next[ tn ] = true;
+        }
+      }
+    }
+    //for calculating unresolved types
+    for( std::map< TypeNode, bool >::iterator it = unresolved_types.begin(); it != unresolved_types.end(); ++it ){
+      unresolved_types[ it->first ] = unresolved_types_next[ it->first ];
+    }
+  }while( !fixedPoint );
+
+  //for all unresolved equivalence classes, just get new domain value
+  //  this should typically never happen (all equivalence classes should be resolved at this point)
+  for( std::map< Node, bool >::iterator it = unresolved_eqc.begin(); it != unresolved_eqc.end(); ++it ){
+    if( it->second ){
+      Node n = it->first;
+      Node rep = chooseRepresentative( tm, n );
+      tm->assertEquality( n, rep, true );
+      tm->d_reps[ n ] = rep;
+      tm->d_rep_set.add( rep );
+      //FIXME: Assertion failure here?
+      Message() << "Warning : Unresolved eqc, assigning " << rep << " for eqc( " << n << " ), type = " << n.getType() << std::endl;
+    }
+  }
+
+  //model-specific initialization
+  processBuildModel( tm );
+}
+
+void TheoryEngineModelBuilder::initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types ){
+  if( unresolved_types.find( tn )==unresolved_types.end() ){
+    unresolved_types[tn] = false;
+    if( tn.isArray() ){
+      initializeType( tn.getArrayIndexType(), unresolved_types );
+      initializeType( tn.getArrayConstituentType(), unresolved_types );
+    }else if( tn.isDatatype() ){
+      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+      for( size_t i = 0; i<dt.getNumConstructors(); i++ ){
+        for( size_t j = 0; j<dt[i].getNumArgs(); j++ ){
+          initializeType( TypeNode::fromType( dt[i][j].getType() ), unresolved_types );
+        }
+      }
+    }
+  }
+}
+
+Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){
+  //try to get a new domain value
+  Node rep = m->getNewDomainValue( eqc.getType() );
+  if( !rep.isNull() ){
+    return rep;
+  }else{
+    //if we can't get new domain value, just return eqc itself (this typically should not happen)
+    //FIXME: Assertion failure here?
+    return eqc;
+  }
+}
diff --git a/src/theory/model.h b/src/theory/model.h
index 415b008ef..940a2f527 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -1,191 +1,191 @@
-/*********************                                                        */

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

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY_MODEL_H

-#define __CVC4__THEORY_MODEL_H

-

-#include "util/model.h"

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

-

-namespace CVC4 {

-namespace theory {

-

-class QuantifiersEngine;

-

-/** this class stores a representative set */

-class RepSet {

-public:

-  RepSet(){}

-  ~RepSet(){}

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

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

-  /** clear the set */

-  void clear();

-  /** has type */

-  bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }

-  /** add representative for type */

-  void add( Node n );

-  /** set the representatives for type */

-  void set( TypeNode t, std::vector< Node >& reps );

-  /** returns index in d_type_reps for node n */

-  int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }

-  /** debug print */

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

-};

-

-//representative domain

-typedef std::vector< int > RepDomain;

-

-class TheoryEngineModelBuilder;

-

-/** Theory Model class

- *    For Model m, should call m.initialize() before using

- */

-class TheoryModel : public Model

-{

-  friend class TheoryEngineModelBuilder;

-protected:

-  /** add term function

-    *   This should be called on all terms that exist in the model.

-    *   addTerm( n ) will do any model-specific processing necessary for n,

-    *   such as contraining the interpretation of uninterpretted functions.

-    */

-  virtual void addTerm( Node n ) {}

-private:

-  /** List of definitions that the user has given

-    *  This is necessary for supporting the get-model command.

-    */

-  std::vector< Node > d_define_funcs;

-  std::vector< TypeNode > d_define_types;

-  std::vector< int > d_defines;

-protected:

-  /** print the value of the function n to stream */

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

-  /** print the value of the type tn to stream */

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

-public:

-  TheoryModel( context::Context* c, std::string name );

-  virtual ~TheoryModel(){}

-  /** equality engine containing all known equalities/disequalities */

-  eq::EqualityEngine d_equalityEngine;

-  /** map of representatives of equality engine to used representatives in representative set */

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

-  /** stores set of representatives for each type */

-  RepSet d_rep_set;

-  /** true/false nodes */

-  Node d_true;

-  Node d_false;

-public:

-  /** reset the model */

-  virtual void reset();

-  /** get interpreted value

-    *  This function is called when the value of the node cannot be determined by the theory rewriter

-    *  This should function should return a representative in d_reps

-    */

-  virtual Node getInterpretedValue( TNode n ) = 0;

-public:

-  /** add defined function (for get-model) */

-  void addDefineFunction( Node n );

-  /** add defined type (for get-model) */

-  void addDefineType( TypeNode tn );

-  /**

-   * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)

-   * on this model.

-   */

-  Node getValue( TNode n );

-  /** get existing domain value, with possible exclusions

-    *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude

-    */

-  Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );

-  /** get new domain value

-    *   This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]

-    *   If it cannot find such a node, it returns null.

-    */

-  Node getNewDomainValue( TypeNode tn );

-public:

-  /** assert equality holds in the model */

-  void assertEquality( Node a, Node b, bool polarity );

-  /** assert predicate holds in the model */

-  void assertPredicate( Node a, bool polarity );

-  /** assert all equalities/predicates in equality engine hold in the model */

-  void assertEqualityEngine( eq::EqualityEngine* ee );

-public:

-  /** general queries */

-  bool hasTerm( Node a );

-  Node getRepresentative( Node a );

-  bool areEqual( Node a, Node b );

-  bool areDisequal( Node a, Node b );

-public:

-  /** print representative debug function */

-  void printRepresentativeDebug( const char* c, Node r );

-  /** print representative function */

-  void printRepresentative( std::ostream& out, Node r );

-  /** to stream function */

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

-};

-

-/** Default model class

-  *   The getInterpretedValue function will choose an existing value arbitrarily.

-  *   If none are found, then it will create a new value.

-  */

-class DefaultModel : public TheoryModel

-{

-protected:

-  /** whether function models are enabled */

-  bool d_enableFuncModels;

-  /** add term */

-  void addTerm( Node n );

-public:

-  DefaultModel( context::Context* c, std::string name, bool enableFuncModels );

-  virtual ~DefaultModel(){}

-  //necessary information for function models

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

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

-public:

-  void reset();

-  Node getInterpretedValue( TNode n );

-};

-

-/** TheoryEngineModelBuilder class

-  *    This model builder will consult all theories in a theory engine for

-  *    collectModelInfo( ... ) when building a model.

-  */

-class TheoryEngineModelBuilder : public ModelBuilder

-{

-protected:

-  /** pointer to theory engine */

-  TheoryEngine* d_te;

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

-  void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types );

-  /** process build model */

-  virtual void processBuildModel( TheoryModel* m ){}

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

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

-public:

-  TheoryEngineModelBuilder( TheoryEngine* te );

-  virtual ~TheoryEngineModelBuilder(){}

-  /** Build model function.

-   *    Should be called only on TheoryModels m

-   */

-  void buildModel( Model* m );

-};

-

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file 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 class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_MODEL_H
+#define __CVC4__THEORY_MODEL_H
+
+#include "util/model.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+/** this class stores a representative set */
+class RepSet {
+public:
+  RepSet(){}
+  ~RepSet(){}
+  std::map< TypeNode, std::vector< Node > > d_type_reps;
+  std::map< Node, int > d_tmap;
+  /** clear the set */
+  void clear();
+  /** has type */
+  bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }
+  /** add representative for type */
+  void add( Node n );
+  /** set the representatives for type */
+  void set( TypeNode t, std::vector< Node >& reps );
+  /** returns index in d_type_reps for node n */
+  int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }
+  /** debug print */
+  void toStream(std::ostream& out);
+};
+
+//representative domain
+typedef std::vector< int > RepDomain;
+
+class TheoryEngineModelBuilder;
+
+/** Theory Model class
+ *    For Model m, should call m.initialize() before using
+ */
+class TheoryModel : public Model
+{
+  friend class TheoryEngineModelBuilder;
+protected:
+  /** add term function
+    *   This should be called on all terms that exist in the model.
+    *   addTerm( n ) will do any model-specific processing necessary for n,
+    *   such as contraining the interpretation of uninterpretted functions.
+    */
+  virtual void addTerm( Node n ) {}
+private:
+  /** List of definitions that the user has given
+    *  This is necessary for supporting the get-model command.
+    */
+  std::vector< Node > d_define_funcs;
+  std::vector< TypeNode > d_define_types;
+  std::vector< int > d_defines;
+protected:
+  /** print the value of the function n to stream */
+  virtual void toStreamFunction( Node n, std::ostream& out );
+  /** print the value of the type tn to stream */
+  virtual void toStreamType( TypeNode tn, std::ostream& out );
+public:
+  TheoryModel( context::Context* c, std::string name );
+  virtual ~TheoryModel(){}
+  /** equality engine containing all known equalities/disequalities */
+  eq::EqualityEngine d_equalityEngine;
+  /** map of representatives of equality engine to used representatives in representative set */
+  std::map< Node, Node > d_reps;
+  /** stores set of representatives for each type */
+  RepSet d_rep_set;
+  /** true/false nodes */
+  Node d_true;
+  Node d_false;
+public:
+  /** reset the model */
+  virtual void reset();
+  /** get interpreted value
+    *  This function is called when the value of the node cannot be determined by the theory rewriter
+    *  This should function should return a representative in d_reps
+    */
+  virtual Node getInterpretedValue( TNode n ) = 0;
+public:
+  /** add defined function (for get-model) */
+  void addDefineFunction( Node n );
+  /** add defined type (for get-model) */
+  void addDefineType( TypeNode tn );
+  /**
+   * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
+   * on this model.
+   */
+  Node getValue( TNode n );
+  /** get existing domain value, with possible exclusions
+    *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
+    */
+  Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );
+  /** get new domain value
+    *   This function returns a constant term of type tn that is not in d_rep_set.d_type_reps[tn]
+    *   If it cannot find such a node, it returns null.
+    */
+  Node getNewDomainValue( TypeNode tn );
+public:
+  /** assert equality holds in the model */
+  void assertEquality( Node a, Node b, bool polarity );
+  /** assert predicate holds in the model */
+  void assertPredicate( Node a, bool polarity );
+  /** assert all equalities/predicates in equality engine hold in the model */
+  void assertEqualityEngine( eq::EqualityEngine* ee );
+public:
+  /** general queries */
+  bool hasTerm( Node a );
+  Node getRepresentative( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+public:
+  /** print representative debug function */
+  void printRepresentativeDebug( const char* c, Node r );
+  /** print representative function */
+  void printRepresentative( std::ostream& out, Node r );
+  /** to stream function */
+  void toStream( std::ostream& out );
+};
+
+/** Default model class
+  *   The getInterpretedValue function will choose an existing value arbitrarily.
+  *   If none are found, then it will create a new value.
+  */
+class DefaultModel : public TheoryModel
+{
+protected:
+  /** whether function models are enabled */
+  bool d_enableFuncModels;
+  /** add term */
+  void addTerm( Node n );
+public:
+  DefaultModel( context::Context* c, std::string name, bool enableFuncModels );
+  virtual ~DefaultModel(){}
+  //necessary information for function models
+  std::map< Node, std::vector< Node > > d_uf_terms;
+  std::map< Node, Node > d_uf_models;
+public:
+  void reset();
+  Node getInterpretedValue( TNode n );
+};
+
+/** TheoryEngineModelBuilder class
+  *    This model builder will consult all theories in a theory engine for
+  *    collectModelInfo( ... ) when building a model.
+  */
+class TheoryEngineModelBuilder : public ModelBuilder
+{
+protected:
+  /** pointer to theory engine */
+  TheoryEngine* d_te;
+  /** choose representative for unresolved equivalence class */
+  void initializeType( TypeNode tn, std::map< TypeNode, bool >& unresolved_types );
+  /** process build model */
+  virtual void processBuildModel( TheoryModel* m ){}
+  /** choose representative for unconstrained equivalence class */
+  virtual Node chooseRepresentative( TheoryModel* m, Node eqc );
+public:
+  TheoryEngineModelBuilder( TheoryEngine* te );
+  virtual ~TheoryEngineModelBuilder(){}
+  /** Build model function.
+   *    Should be called only on TheoryModels m
+   */
+  void buildModel( Model* m );
+};
+
+}
+}
+
+#endif
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
diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp
index 287f7475a..21a309610 100644
--- a/src/theory/rr_inst_match.cpp
+++ b/src/theory/rr_inst_match.cpp
@@ -958,7 +958,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){
         arithmetic pattern */
     std::map< Node, Node > d_arith_coeffs;
     if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
-      std::cout << "(?) Unknown matching pattern is " << pat << std::endl;
+      Message() << "(?) Unknown matching pattern is " << pat << std::endl;
       Unimplemented("pattern not implemented");
       return new DumbMatcher();
     }else{
@@ -1010,7 +1010,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){
     std::map< Node, Node > d_arith_coeffs;
     if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){
       Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl;
-      std::cout << "(?) Unknown matching pattern is " << pat << std::endl;
+      Message() << "(?) Unknown matching pattern is " << pat << std::endl;
       return new DumbPatMatcher();
     }else{
       Debug("matching-arith") << "Generated arithmetic pattern for " << pat << ": " << std::endl;
diff --git a/src/theory/rr_trigger.cpp b/src/theory/rr_trigger.cpp
index 52e7efcc2..ece68d137 100644
--- a/src/theory/rr_trigger.cpp
+++ b/src/theory/rr_trigger.cpp
@@ -75,156 +75,156 @@ d_quantEngine( qe ), d_f( f ){
     }else{
       ++(qe->d_statistics.d_simple_triggers);
     }
-  }else{

+  }else{
     Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl;
     //std::cout << "Multi-trigger for " << f << " : " << std::endl;
     //std::cout << "   " << (*this) << std::endl;
     ++(qe->d_statistics.d_multi_triggers);
   }
-}

-void Trigger::computeVarContains( Node n ) {

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

-    d_var_contains[n].clear();

-    computeVarContains2( n, n );

-  }

-}

-

-void Trigger::computeVarContains2( Node n, Node parent ){

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

-    if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){

-      d_var_contains[parent].push_back( n );

-    }

-  }else{

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

-      computeVarContains2( n[i], parent );

-    }

-  }

 }
-

-void Trigger::resetInstantiationRound(){

-  d_mg->resetInstantiationRound( d_quantEngine );

-}

-

+void Trigger::computeVarContains( Node n ) {
+  if( d_var_contains.find( n )==d_var_contains.end() ){
+    d_var_contains[n].clear();
+    computeVarContains2( n, n );
+  }
+}
+
+void Trigger::computeVarContains2( Node n, Node parent ){
+  if( n.getKind()==INST_CONSTANT ){
+    if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){
+      d_var_contains[parent].push_back( n );
+    }
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      computeVarContains2( n[i], parent );
+    }
+  }
+}
+
+void Trigger::resetInstantiationRound(){
+  d_mg->resetInstantiationRound( d_quantEngine );
+}
 
-bool Trigger::getNextMatch(){

-  bool retVal = d_mg->getNextMatch( d_quantEngine );

-  //m.makeInternal( d_quantEngine->getEqualityQuery() );

-  return retVal;

-}

+
+bool Trigger::getNextMatch(){
+  bool retVal = d_mg->getNextMatch( d_quantEngine );
+  //m.makeInternal( d_quantEngine->getEqualityQuery() );
+  return retVal;
+}
 
 // bool Trigger::getMatch( Node t, InstMatch& m ){
 //   //FIXME: this assumes d_mg is an inst match generator
 //   return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine );
 // }
-

 
-int Trigger::addInstantiations( InstMatch& baseMatch ){

+
+int Trigger::addInstantiations( InstMatch& baseMatch ){
   int addedLemmas = d_mg->addInstantiations( baseMatch,
                                              d_nodes[0].getAttribute(InstConstantAttribute()),
-                                             d_quantEngine);

-  if( addedLemmas>0 ){

+                                             d_quantEngine);
+  if( addedLemmas>0 ){
     Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
     for( int i=0; i<(int)d_nodes.size(); i++ ){
       Debug("inst-trigger") << d_nodes[i] << " ";
     }
-    Debug("inst-trigger") << std::endl;

-  }

-  return addedLemmas;

-}

-

-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,

-                             bool smartTriggers ){

-  std::vector< Node > trNodes;

-  if( !keepAll ){

-    //only take nodes that contribute variables to the trigger when added

-    std::vector< Node > temp;

-    temp.insert( temp.begin(), nodes.begin(), nodes.end() );

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

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

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

-      bool foundVar = false;

-      computeVarContains( temp[i] );

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

-        Node v = d_var_contains[ temp[i] ][j];

-        if( v.getAttribute(InstConstantAttribute())==f ){

-          if( vars.find( v )==vars.end() ){

-            vars[ v ] = true;

-            foundVar = true;

-          }

-        }

-      }

-      if( foundVar ){

-        trNodes.push_back( temp[i] );

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

-          Node v = d_var_contains[ temp[i] ][j];

-          patterns[ v ].push_back( temp[i] );

-        }

-      }

-    }

-    //now, minimalize the trigger

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

-      bool keepPattern = false;

-      Node n = trNodes[i];

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

-        Node v = d_var_contains[ n ][j];

-        if( patterns[v].size()==1 ){

-          keepPattern = true;

-          break;

-        }

-      }

-      if( !keepPattern ){

-        //remove from pattern vector

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

-          Node v = d_var_contains[ n ][j];

-          for( int k=0; k<(int)patterns[v].size(); k++ ){

-            if( patterns[v][k]==n ){

-              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );

-              break;

-            }

-          }

-        }

-        //remove from trigger nodes

-        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );

-        i--;

-      }

-    }

-  }else{

-    trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );

-  }

-

-  //check for duplicate?

-  if( trOption==TR_MAKE_NEW ){

-    //static int trNew = 0;

-    //static int trOld = 0;

-    //Trigger* t = d_tr_trie.getTrigger( trNodes );

-    //if( t ){

-    //  trOld++;

-    //}else{

-    //  trNew++;

-    //}

-    //if( (trNew+trOld)%100==0 ){

-    //  std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;

-    //}

-  }else{

-    Trigger* t = d_tr_trie.getTrigger( trNodes );

-    if( t ){

-      if( trOption==TR_GET_OLD ){

-        //just return old trigger

-        return t;

-      }else{

-        return NULL;

-      }

-    }

-  }

-  Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );

-  d_tr_trie.addTrigger( trNodes, t );

-  return t;

-}

-Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){

-  std::vector< Node > nodes;

-  nodes.push_back( n );

-  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );

-}

+    Debug("inst-trigger") << std::endl;
+  }
+  return addedLemmas;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool keepAll, int trOption,
+                             bool smartTriggers ){
+  std::vector< Node > trNodes;
+  if( !keepAll ){
+    //only take nodes that contribute variables to the trigger when added
+    std::vector< Node > temp;
+    temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+    std::map< Node, bool > vars;
+    std::map< Node, std::vector< Node > > patterns;
+    for( int i=0; i<(int)temp.size(); i++ ){
+      bool foundVar = false;
+      computeVarContains( temp[i] );
+      for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
+        Node v = d_var_contains[ temp[i] ][j];
+        if( v.getAttribute(InstConstantAttribute())==f ){
+          if( vars.find( v )==vars.end() ){
+            vars[ v ] = true;
+            foundVar = true;
+          }
+        }
+      }
+      if( foundVar ){
+        trNodes.push_back( temp[i] );
+        for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){
+          Node v = d_var_contains[ temp[i] ][j];
+          patterns[ v ].push_back( temp[i] );
+        }
+      }
+    }
+    //now, minimalize the trigger
+    for( int i=0; i<(int)trNodes.size(); i++ ){
+      bool keepPattern = false;
+      Node n = trNodes[i];
+      for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
+        Node v = d_var_contains[ n ][j];
+        if( patterns[v].size()==1 ){
+          keepPattern = true;
+          break;
+        }
+      }
+      if( !keepPattern ){
+        //remove from pattern vector
+        for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){
+          Node v = d_var_contains[ n ][j];
+          for( int k=0; k<(int)patterns[v].size(); k++ ){
+            if( patterns[v][k]==n ){
+              patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+              break;
+            }
+          }
+        }
+        //remove from trigger nodes
+        trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+        i--;
+      }
+    }
+  }else{
+    trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
+  }
+
+  //check for duplicate?
+  if( trOption==TR_MAKE_NEW ){
+    //static int trNew = 0;
+    //static int trOld = 0;
+    //Trigger* t = d_tr_trie.getTrigger( trNodes );
+    //if( t ){
+    //  trOld++;
+    //}else{
+    //  trNew++;
+    //}
+    //if( (trNew+trOld)%100==0 ){
+    //  std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl;
+    //}
+  }else{
+    Trigger* t = d_tr_trie.getTrigger( trNodes );
+    if( t ){
+      if( trOption==TR_GET_OLD ){
+        //just return old trigger
+        return t;
+      }else{
+        return NULL;
+      }
+    }
+  }
+  Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers );
+  d_tr_trie.addTrigger( trNodes, t );
+  return t;
+}
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){
+  std::vector< Node > nodes;
+  nodes.push_back( n );
+  return mkTrigger( qe, f, nodes, matchOption, keepAll, trOption, smartTriggers );
+}
 
 bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
   for( int i=0; i<(int)nodes.size(); i++ ){
@@ -233,25 +233,25 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){
     }
   }
   return true;
-}

-

-bool Trigger::isUsable( Node n, Node f ){

-  if( n.getAttribute(InstConstantAttribute())==f ){

-    if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){

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

-      return getPatternArithmetic( f, n, coeffs );

-    }else{

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

-        if( !isUsable( n[i], f ) ){

-          return false;

-        }

-      }

-      return true;

-    }

-  }else{

-    return true;

-  }

-}

+}
+
+bool Trigger::isUsable( Node n, Node f ){
+  if( n.getAttribute(InstConstantAttribute())==f ){
+    if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){
+      std::map< Node, Node > coeffs;
+      return getPatternArithmetic( f, n, coeffs );
+    }else{
+      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        if( !isUsable( n[i], f ) ){
+          return false;
+        }
+      }
+      return true;
+    }
+  }else{
+    return true;
+  }
+}
 
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
@@ -293,67 +293,67 @@ void Trigger::filterInstances( std::vector< Node >& nodes ){
 }
 
 
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){

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

-    patMap[ n ] = false;

-    if( tstrt==TS_MIN_TRIGGER ){

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

-#ifdef NESTED_PATTERN_SELECTION

-        //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );

-        return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );

-#else

-        return false;

-#endif

-      }else{

-        bool retVal = false;

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

-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){

-            retVal = true;

-          }

-        }

-        if( retVal ){

-          return true;

-        }else if( isUsableTrigger( n, f ) ){

-          patMap[ n ] = true;

-          return true;

-        }else{

-          return false;

-        }

-      }

-    }else{

-      bool retVal = false;

-      if( isUsableTrigger( n, f ) ){

-        patMap[ n ] = true;

-        if( tstrt==TS_MAX_TRIGGER ){

-          return true;

-        }else{

-          retVal = true;

-        }

-      }

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

-#ifdef NESTED_PATTERN_SELECTION

-        //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){

-        //  retVal = true;

-        //}

-        if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){

-          retVal = true;

-        }

-#endif

-      }else{

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

-          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){

-            retVal = true;

-          }

-        }

-      }

-      return retVal;

-    }

-  }else{

-    return patMap[ n ];

-  }

+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
+  if( patMap.find( n )==patMap.end() ){
+    patMap[ n ] = false;
+    if( tstrt==TS_MIN_TRIGGER ){
+      if( n.getKind()==FORALL ){
+#ifdef NESTED_PATTERN_SELECTION
+        //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
+        return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
+#else
+        return false;
+#endif
+      }else{
+        bool retVal = false;
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+            retVal = true;
+          }
+        }
+        if( retVal ){
+          return true;
+        }else if( isUsableTrigger( n, f ) ){
+          patMap[ n ] = true;
+          return true;
+        }else{
+          return false;
+        }
+      }
+    }else{
+      bool retVal = false;
+      if( isUsableTrigger( n, f ) ){
+        patMap[ n ] = true;
+        if( tstrt==TS_MAX_TRIGGER ){
+          return true;
+        }else{
+          retVal = true;
+        }
+      }
+      if( n.getKind()==FORALL ){
+#ifdef NESTED_PATTERN_SELECTION
+        //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
+        //  retVal = true;
+        //}
+        if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
+          retVal = true;
+        }
+#endif
+      }else{
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+            retVal = true;
+          }
+        }
+      }
+      return retVal;
+    }
+  }else{
+    return patMap[ n ];
+  }
 }
 
-void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){

+void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){
   std::map< Node, bool > patMap;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
@@ -387,10 +387,10 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto
     }
   }
   collectPatTerms2( qe, f, n, patMap, tstrt );
-  for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){

-    if( it->second ){

-      patTerms.push_back( it->first );

-    }

+  for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
+    if( it->second ){
+      patTerms.push_back( it->first );
+    }
   }
 }
 
@@ -469,15 +469,15 @@ void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node,
     }
   }
 }
-

-void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){

-  computeVarContains( n );

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

-    if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){

-      varContains.push_back( d_var_contains[n][j] );

-    }

-  }

-}

+
+void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){
+  computeVarContains( n );
+  for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+    if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){
+      varContains.push_back( d_var_contains[n][j] );
+    }
+  }
+}
 
 bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){
   if( n.getKind()==PLUS ){
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index f68ab1429..0082f4840 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -1,421 +1,421 @@
-/*********************                                                        */

-/*! \file theory_uf_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 Theory UF Model

- **/

-

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

-#include "theory/theory_engine.h"

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

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

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

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

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

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

-

-#define RECONSIDER_FUNC_DEFAULT_VALUE

-#define USE_PARTIAL_DEFAULT_VALUES

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::uf;

-

-//clear

-void UfModelTreeNode::clear(){

-  d_data.clear();

-  d_value = Node::null();

-}

-

-bool UfModelTreeNode::hasConcreteArgumentDefinition(){

-  if( d_data.size()>1 ){

-    return true;

-  }else if( d_data.empty() ){

-    return false;

-  }else{

-    Node r;

-    return d_data.find( r )==d_data.end();

-  }

-}

-

-//set value function

-void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){

-  if( d_data.empty() ){

-    d_value = v;

-  }else if( !d_value.isNull() && d_value!=v ){

-    d_value = Node::null();

-  }

-  if( argIndex<(int)indexOrder.size() ){

-    //take r = null when argument is the model basis

-    Node r;

-    if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){

-      r = m->getRepresentative( n[ indexOrder[argIndex] ] );

-    }

-    d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );

-  }

-}

-

-//get value function

-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){

-  if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){

-    //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;

-    depIndex = argIndex;

-    return d_value;

-  }else{

-    Node val;

-    int childDepIndex[2] = { argIndex, argIndex };

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

-      //first check the argument, then check default

-      Node r;

-      if( i==0 ){

-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );

-      }

-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

-      if( it!=d_data.end() ){

-        val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );

-        if( !val.isNull() ){

-          break;

-        }

-      }else{

-        //argument is not a defined argument: thus, it depends on this argument

-        childDepIndex[i] = argIndex+1;

-      }

-    }

-    //update depIndex

-    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];

-    //Notice() << "Return " << val << ", depIndex = " << depIndex;

-    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;

-    return val;

-  }

-}

-

-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){

-  if( argIndex==(int)indexOrder.size() ){

-    return d_value;

-  }else{

-    Node val;

-    bool depArg = false;

-    //will try concrete value first, then default

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

-      Node r;

-      if( i==0 ){

-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );

-      }

-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

-      if( it!=d_data.end() ){

-        val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );

-        //we have found a value

-        if( !val.isNull() ){

-          if( i==0 ){

-            depArg = true;

-          }

-          break;

-        }

-      }

-    }

-    //it depends on this argument if we found it via concrete argument value,

-    // or if found by default/disequal from some concrete argument value(s).

-    if( depArg || hasConcreteArgumentDefinition() ){

-      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){

-        depIndex.push_back( indexOrder[argIndex] );

-      }

-    }

-    return val;

-  }

-}

-

-Node UfModelTreeNode::getFunctionValue(){

-  if( !d_data.empty() ){

-    Node defaultValue;

-    std::vector< Node > caseValues;

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

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

-        defaultValue = it->second.getFunctionValue();

-      }else{

-        caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );

-      }

-    }

-    if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){

-      return defaultValue;

-    }else{

-      std::vector< Node > children;

-      if( !caseValues.empty() ){

-        children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );

-      }

-      if( !defaultValue.isNull() ){

-        children.push_back( defaultValue );

-      }

-      return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );

-    }

-  }else{

-    Assert( !d_value.isNull() );

-    return d_value;

-  }

-}

-

-//simplify function

-void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){

-  if( argIndex<(int)op.getType().getNumChildren()-1 ){

-    std::vector< Node > eraseData;

-    //first process the default argument

-    Node r;

-    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

-    if( it!=d_data.end() ){

-      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){

-        eraseData.push_back( r );

-      }else{

-        it->second.simplify( op, defaultVal, argIndex+1 );

-        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){

-          defaultVal = it->second.d_value;

-        }else{

-          defaultVal = Node::null();

-          if( it->second.isEmpty() ){

-            eraseData.push_back( r );

-          }

-        }

-      }

-    }

-    //now see if any children can be removed, and simplify the ones that cannot

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

-      if( !it->first.isNull() ){

-        if( !defaultVal.isNull() && it->second.d_value==defaultVal ){

-          eraseData.push_back( it->first );

-        }else{

-          it->second.simplify( op, defaultVal, argIndex+1 );

-          if( it->second.isEmpty() ){

-            eraseData.push_back( it->first );

-          }

-        }

-      }

-    }

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

-      d_data.erase( eraseData[i] );

-    }

-  }

-}

-

-//is total function

-bool UfModelTreeNode::isTotal( Node op, int argIndex ){

-  if( argIndex==(int)(op.getType().getNumChildren()-1) ){

-    return !d_value.isNull();

-  }else{

-    Node r;

-    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );

-    if( it!=d_data.end() ){

-      return it->second.isTotal( op, argIndex+1 );

-    }else{

-      return false;

-    }

-  }

-}

-

-Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){

-  return d_value;

-}

-

-void indent( std::ostream& out, int ind ){

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

-    out << " ";

-  }

-}

-

-void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){

-  if( !d_data.empty() ){

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

-      if( !it->first.isNull() ){

-        indent( out, ind );

-        out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;

-        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );

-      }

-    }

-    if( d_data.find( Node::null() )!=d_data.end() ){

-      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );

-    }

-  }else{

-    indent( out, ind );

-    out << "return ";

-    m->printRepresentative( out, d_value );

-    out << std::endl;

-  }

-}

-

-

-Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){

-  if( fm_node.getKind()==FUNCTION_MODEL ){

-    if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){

-      Node retNode;

-      Node childDefaultNode = defaultNode;

-      //get new default

-      if( fm_node.getNumChildren()==2 ){

-        childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );

-      }

-      retNode = childDefaultNode;

-      for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){

-        Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );

-        retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );

-      }

-      return retNode;

-    }else{

-      return toIte2( fm_node[0], args, index+1, defaultNode );

-    }

-  }else{

-    return fm_node;

-  }

-}

-

-

-Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){

-  //Notice() << "Get intersection " << n1 << " " << n2 << std::endl;

-  isGround = true;

-  std::vector< Node > children;

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

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

-    if( n1[i]==n2[i] ){

-      if( n1[i].getAttribute(ModelBasisAttribute()) ){

-        isGround = false;

-      }

-      children.push_back( n1[i] );

-    }else if( n1[i].getAttribute(ModelBasisAttribute()) ){

-      children.push_back( n2[i] );

-    }else if( n2[i].getAttribute(ModelBasisAttribute()) ){

-      children.push_back( n1[i] );

-    }else if( m->areEqual( n1[i], n2[i] ) ){

-      children.push_back( n1[i] );

-    }else{

-      return Node::null();

-    }

-  }

-  return NodeManager::currentNM()->mkNode( APPLY_UF, children );

-}

-

-void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){

-  Assert( !n.isNull() );

-  Assert( !v.isNull() );

-  d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;

-  if( optUsePartialDefaults() ){

-    if( !ground ){

-      int defSize = (int)d_defaults.size();

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

-        bool isGround;

-        //for soundness, to allow variable order-independent function interpretations,

-        //  we must ensure that the intersection of all default terms

-        //  is also defined.

-        //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,

-        //  then we must define f( b, a ).

-        Node ni = getIntersection( m, n, d_defaults[i], isGround );

-        if( !ni.isNull() ){

-          //if the intersection exists, and is not already defined

-          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&

-              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){

-            //use the current value

-            setValue( m, ni, v, isGround, false );

-          }

-        }

-      }

-      d_defaults.push_back( n );

-    }

-    if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){

-      d_set_values[0][ ground ? 1 : 0 ].erase( n );

-    }

-  }

-}

-

-void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){

-  for( int j=0; j<2; j++ ){

-    for( int k=0; k<2; k++ ){

-      for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){

-        tree.setValue( m, it->first, it->second, k==1 );

-      }

-    }

-  }

-  if( !d_default_value.isNull() ){

-    tree.setDefaultValue( m, d_default_value );

-  }

-  tree.simplify();

-}

-

-bool UfModelTreeGenerator::optUsePartialDefaults(){

-#ifdef USE_PARTIAL_DEFAULT_VALUES

-  return true;

-#else

-  return false;

-#endif

-}

-

-void UfModelTreeGenerator::clear(){

-  d_default_value = Node::null();

-  for( int j=0; j<2; j++ ){

-    for( int k=0; k<2; k++ ){

-      d_set_values[j][k].clear();

-    }

-  }

-  d_defaults.clear();

-}

-

-

-void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){

-  if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){

-    d_values.push_back( r );

-  }

-  int index = isPro ? 0 : 1;

-  if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){

-    d_value_pro_con[index][r].push_back( f );

-  }

-  d_term_pro_con[index][n].push_back( f );

-}

-

-Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){

-  Node defaultVal;

-  double maxScore = -1;

-  for( size_t i=0; i<d_values.size(); i++ ){

-    Node v = d_values[i];

-    double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );

-    Debug("fmf-model-cons") << "  - score( ";

-    m->printRepresentativeDebug( "fmf-model-cons", v );

-    Debug("fmf-model-cons") << " ) = " << score << std::endl;

-    if( score>maxScore ){

-      defaultVal = v;

-      maxScore = score;

-    }

-  }

-#ifdef RECONSIDER_FUNC_DEFAULT_VALUE

-  if( maxScore<1.0 ){

-    //consider finding another value, if possible

-    Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;

-    TypeNode tn = defaultTerm.getType();

-    Node newDefaultVal = m->getDomainValue( tn, d_values );

-    if( !newDefaultVal.isNull() ){

-      defaultVal = newDefaultVal;

-      Debug("fmf-model-cons-debug") << "-> Change default value to ";

-      m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal );

-      Debug("fmf-model-cons-debug") << std::endl;

-    }else{

-      Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;

-      Debug("fmf-model-cons-debug") << "      Excluding: ";

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

-        Debug("fmf-model-cons-debug") << d_values[i] << " ";

-      }

-      Debug("fmf-model-cons-debug") << std::endl;

-    }

-  }

-#endif

-  //get the default term (this term must be defined non-ground in model)

-  Debug("fmf-model-cons") << "  Choose ";

-  m->printRepresentativeDebug("fmf-model-cons", defaultVal );

-  Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;

-  Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;

-  Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;

-  return defaultVal;

+/*********************                                                        */
+/*! \file theory_uf_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 Theory UF Model
+ **/
+
+#include "theory/quantifiers/model_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_strong_solver.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+
+#define RECONSIDER_FUNC_DEFAULT_VALUE
+#define USE_PARTIAL_DEFAULT_VALUES
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+//clear
+void UfModelTreeNode::clear(){
+  d_data.clear();
+  d_value = Node::null();
+}
+
+bool UfModelTreeNode::hasConcreteArgumentDefinition(){
+  if( d_data.size()>1 ){
+    return true;
+  }else if( d_data.empty() ){
+    return false;
+  }else{
+    Node r;
+    return d_data.find( r )==d_data.end();
+  }
+}
+
+//set value function
+void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
+  if( d_data.empty() ){
+    d_value = v;
+  }else if( !d_value.isNull() && d_value!=v ){
+    d_value = Node::null();
+  }
+  if( argIndex<(int)indexOrder.size() ){
+    //take r = null when argument is the model basis
+    Node r;
+    if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
+      r = m->getRepresentative( n[ indexOrder[argIndex] ] );
+    }
+    d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
+  }
+}
+
+//get value function
+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
+  if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
+    //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
+    depIndex = argIndex;
+    return d_value;
+  }else{
+    Node val;
+    int childDepIndex[2] = { argIndex, argIndex };
+    for( int i=0; i<2; i++ ){
+      //first check the argument, then check default
+      Node r;
+      if( i==0 ){
+        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
+      }
+      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
+      if( it!=d_data.end() ){
+        val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );
+        if( !val.isNull() ){
+          break;
+        }
+      }else{
+        //argument is not a defined argument: thus, it depends on this argument
+        childDepIndex[i] = argIndex+1;
+      }
+    }
+    //update depIndex
+    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
+    //Notice() << "Return " << val << ", depIndex = " << depIndex;
+    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
+    return val;
+  }
+}
+
+Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
+  if( argIndex==(int)indexOrder.size() ){
+    return d_value;
+  }else{
+    Node val;
+    bool depArg = false;
+    //will try concrete value first, then default
+    for( int i=0; i<2; i++ ){
+      Node r;
+      if( i==0 ){
+        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
+      }
+      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
+      if( it!=d_data.end() ){
+        val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );
+        //we have found a value
+        if( !val.isNull() ){
+          if( i==0 ){
+            depArg = true;
+          }
+          break;
+        }
+      }
+    }
+    //it depends on this argument if we found it via concrete argument value,
+    // or if found by default/disequal from some concrete argument value(s).
+    if( depArg || hasConcreteArgumentDefinition() ){
+      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){
+        depIndex.push_back( indexOrder[argIndex] );
+      }
+    }
+    return val;
+  }
+}
+
+Node UfModelTreeNode::getFunctionValue(){
+  if( !d_data.empty() ){
+    Node defaultValue;
+    std::vector< Node > caseValues;
+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      if( it->first.isNull() ){
+        defaultValue = it->second.getFunctionValue();
+      }else{
+        caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );
+      }
+    }
+    if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){
+      return defaultValue;
+    }else{
+      std::vector< Node > children;
+      if( !caseValues.empty() ){
+        children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );
+      }
+      if( !defaultValue.isNull() ){
+        children.push_back( defaultValue );
+      }
+      return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );
+    }
+  }else{
+    Assert( !d_value.isNull() );
+    return d_value;
+  }
+}
+
+//simplify function
+void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
+  if( argIndex<(int)op.getType().getNumChildren()-1 ){
+    std::vector< Node > eraseData;
+    //first process the default argument
+    Node r;
+    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
+    if( it!=d_data.end() ){
+      if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
+        eraseData.push_back( r );
+      }else{
+        it->second.simplify( op, defaultVal, argIndex+1 );
+        if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
+          defaultVal = it->second.d_value;
+        }else{
+          defaultVal = Node::null();
+          if( it->second.isEmpty() ){
+            eraseData.push_back( r );
+          }
+        }
+      }
+    }
+    //now see if any children can be removed, and simplify the ones that cannot
+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      if( !it->first.isNull() ){
+        if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
+          eraseData.push_back( it->first );
+        }else{
+          it->second.simplify( op, defaultVal, argIndex+1 );
+          if( it->second.isEmpty() ){
+            eraseData.push_back( it->first );
+          }
+        }
+      }
+    }
+    for( int i=0; i<(int)eraseData.size(); i++ ){
+      d_data.erase( eraseData[i] );
+    }
+  }
+}
+
+//is total function
+bool UfModelTreeNode::isTotal( Node op, int argIndex ){
+  if( argIndex==(int)(op.getType().getNumChildren()-1) ){
+    return !d_value.isNull();
+  }else{
+    Node r;
+    std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
+    if( it!=d_data.end() ){
+      return it->second.isTotal( op, argIndex+1 );
+    }else{
+      return false;
+    }
+  }
+}
+
+Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
+  return d_value;
+}
+
+void indent( std::ostream& out, int ind ){
+  for( int i=0; i<ind; i++ ){
+    out << " ";
+  }
+}
+
+void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
+  if( !d_data.empty() ){
+    for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      if( !it->first.isNull() ){
+        indent( out, ind );
+        out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
+        it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
+      }
+    }
+    if( d_data.find( Node::null() )!=d_data.end() ){
+      d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
+    }
+  }else{
+    indent( out, ind );
+    out << "return ";
+    m->printRepresentative( out, d_value );
+    out << std::endl;
+  }
+}
+
+
+Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){
+  if( fm_node.getKind()==FUNCTION_MODEL ){
+    if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){
+      Node retNode;
+      Node childDefaultNode = defaultNode;
+      //get new default
+      if( fm_node.getNumChildren()==2 ){
+        childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );
+      }
+      retNode = childDefaultNode;
+      for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){
+        Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );
+        retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );
+      }
+      return retNode;
+    }else{
+      return toIte2( fm_node[0], args, index+1, defaultNode );
+    }
+  }else{
+    return fm_node;
+  }
+}
+
+
+Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
+  //Notice() << "Get intersection " << n1 << " " << n2 << std::endl;
+  isGround = true;
+  std::vector< Node > children;
+  children.push_back( n1.getOperator() );
+  for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+    if( n1[i]==n2[i] ){
+      if( n1[i].getAttribute(ModelBasisAttribute()) ){
+        isGround = false;
+      }
+      children.push_back( n1[i] );
+    }else if( n1[i].getAttribute(ModelBasisAttribute()) ){
+      children.push_back( n2[i] );
+    }else if( n2[i].getAttribute(ModelBasisAttribute()) ){
+      children.push_back( n1[i] );
+    }else if( m->areEqual( n1[i], n2[i] ) ){
+      children.push_back( n1[i] );
+    }else{
+      return Node::null();
+    }
+  }
+  return NodeManager::currentNM()->mkNode( APPLY_UF, children );
+}
+
+void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){
+  Assert( !n.isNull() );
+  Assert( !v.isNull() );
+  d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v;
+  if( optUsePartialDefaults() ){
+    if( !ground ){
+      int defSize = (int)d_defaults.size();
+      for( int i=0; i<defSize; i++ ){
+        bool isGround;
+        //for soundness, to allow variable order-independent function interpretations,
+        //  we must ensure that the intersection of all default terms
+        //  is also defined.
+        //for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
+        //  then we must define f( b, a ).
+        Node ni = getIntersection( m, n, d_defaults[i], isGround );
+        if( !ni.isNull() ){
+          //if the intersection exists, and is not already defined
+          if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+              d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+            //use the current value
+            setValue( m, ni, v, isGround, false );
+          }
+        }
+      }
+      d_defaults.push_back( n );
+    }
+    if( isReq && d_set_values[0][ ground ? 1 : 0 ].find( n )!=d_set_values[0][ ground ? 1 : 0 ].end()){
+      d_set_values[0][ ground ? 1 : 0 ].erase( n );
+    }
+  }
+}
+
+void UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){
+  for( int j=0; j<2; j++ ){
+    for( int k=0; k<2; k++ ){
+      for( std::map< Node, Node >::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){
+        tree.setValue( m, it->first, it->second, k==1 );
+      }
+    }
+  }
+  if( !d_default_value.isNull() ){
+    tree.setDefaultValue( m, d_default_value );
+  }
+  tree.simplify();
+}
+
+bool UfModelTreeGenerator::optUsePartialDefaults(){
+#ifdef USE_PARTIAL_DEFAULT_VALUES
+  return true;
+#else
+  return false;
+#endif
+}
+
+void UfModelTreeGenerator::clear(){
+  d_default_value = Node::null();
+  for( int j=0; j<2; j++ ){
+    for( int k=0; k<2; k++ ){
+      d_set_values[j][k].clear();
+    }
+  }
+  d_defaults.clear();
+}
+
+
+void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){
+  if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){
+    d_values.push_back( r );
+  }
+  int index = isPro ? 0 : 1;
+  if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){
+    d_value_pro_con[index][r].push_back( f );
+  }
+  d_term_pro_con[index][n].push_back( f );
+}
+
+Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){
+  Node defaultVal;
+  double maxScore = -1;
+  for( size_t i=0; i<d_values.size(); i++ ){
+    Node v = d_values[i];
+    double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() );
+    Debug("fmf-model-cons") << "  - score( ";
+    m->printRepresentativeDebug( "fmf-model-cons", v );
+    Debug("fmf-model-cons") << " ) = " << score << std::endl;
+    if( score>maxScore ){
+      defaultVal = v;
+      maxScore = score;
+    }
+  }
+#ifdef RECONSIDER_FUNC_DEFAULT_VALUE
+  if( maxScore<1.0 ){
+    //consider finding another value, if possible
+    Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl;
+    TypeNode tn = defaultTerm.getType();
+    Node newDefaultVal = m->getDomainValue( tn, d_values );
+    if( !newDefaultVal.isNull() ){
+      defaultVal = newDefaultVal;
+      Debug("fmf-model-cons-debug") << "-> Change default value to ";
+      m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal );
+      Debug("fmf-model-cons-debug") << std::endl;
+    }else{
+      Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl;
+      Debug("fmf-model-cons-debug") << "      Excluding: ";
+      for( int i=0; i<(int)d_values.size(); i++ ){
+        Debug("fmf-model-cons-debug") << d_values[i] << " ";
+      }
+      Debug("fmf-model-cons-debug") << std::endl;
+    }
+  }
+#endif
+  //get the default term (this term must be defined non-ground in model)
+  Debug("fmf-model-cons") << "  Choose ";
+  m->printRepresentativeDebug("fmf-model-cons", defaultVal );
+  Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl;
+  Debug("fmf-model-cons") << "     # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl;
+  Debug("fmf-model-cons") << "     # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl;
+  return defaultVal;
 }
\ No newline at end of file
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 47b149867..9dba16608 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -1,199 +1,199 @@
-/*********************                                                        */

-/*! \file theory_uf_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 for Theory UF

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY_UF_MODEL_H

-#define __CVC4__THEORY_UF_MODEL_H

-

-#include "theory/model.h"

-

-namespace CVC4 {

-namespace theory {

-namespace uf {

-

-class UfModelTreeNode

-{

-public:

-  UfModelTreeNode(){}

-  /** the data */

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

-  /** the value of this tree node (if all paths lead to same value) */

-  Node d_value;

-  /** has concrete argument defintion */

-  bool hasConcreteArgumentDefinition();

-public:

-  //is this model tree empty?

-  bool isEmpty() { return d_data.empty() && d_value.isNull(); }

-  //clear

-  void clear();

-  /** setValue function */

-  void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );

-  /**  getValue function */

-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );

-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );

-  /** getConstant Value function */

-  Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );

-  /** getFunctionValue */

-  Node getFunctionValue();

-  /** simplify function */

-  void simplify( Node op, Node defaultVal, int argIndex );

-  /** is total ? */

-  bool isTotal( Node op, int argIndex );

-public:

-  void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );

-};

-

-class UfModelTree

-{

-private:

-  //the op this model is for

-  Node d_op;

-  //the order we will treat the arguments

-  std::vector< int > d_index_order;

-  //the data

-  UfModelTreeNode d_tree;

-public:

-  //constructors

-  UfModelTree(){}

-  UfModelTree( Node op ) : d_op( op ){

-    TypeNode tn = d_op.getType();

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

-      d_index_order.push_back( i );

-    }

-  }

-  UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){

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

-  }

-  /** clear/reset the function */

-  void clear() { d_tree.clear(); }

-  /** setValue function

-    *

-    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false

-    *

-    */

-  void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){

-    d_tree.setValue( m, n, v, d_index_order, ground, 0 );

-  }

-  /** setDefaultValue function */

-  void setDefaultValue( TheoryModel* m, Node v ){

-    d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );

-  }

-  /**  getValue function

-    *

-    *  returns val, the value of ground term n

-    *  Say n is f( t_0...t_n )

-    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val

-    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,

-    *      then g( a, a, a ) would return b with depIndex = 1

-    *

-    */

-  Node getValue( TheoryModel* m, Node n, int& depIndex ){

-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );

-  }

-  /** -> implementation incomplete */

-  Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){

-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );

-  }

-  /** getConstantValue function

-    *

-    * given term n, where n may contain "all value" arguments, aka model basis arguments

-    *   if n is null, then every argument of n is considered "all value"

-    * if n is constant for the entire domain specified by n, then this function returns the value of its domain

-    * otherwise, it returns null

-    * for example, say the term e represents "all values"

-    *   if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,

-    *     then f( a, e ) would return b, while f( e, a ) would return null

-    *  -> implementation incomplete

-    */

-  Node getConstantValue( TheoryModel* m, Node n ) {

-    return d_tree.getConstantValue( m, n, d_index_order, 0 );

-  }

-  /** getFunctionValue

-    *   Returns a compact representation of this function, of kind FUNCTION_MODEL.

-    *   See documentation in theory/uf/kinds

-    */

-  Node getFunctionValue(){

-    return d_tree.getFunctionValue();

-  }

-  /** simplify the tree */

-  void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }

-  /** is this tree total? */

-  bool isTotal() { return d_tree.isTotal( d_op, 0 ); }

-  /** is this function constant? */

-  bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }

-  /** is this tree empty? */

-  bool isEmpty() { return d_tree.isEmpty(); }

-public:

-  void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){

-    d_tree.debugPrint( out, m, d_index_order, ind );

-  }

-private:

-  //helper for to ITE function.

-  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );

-public:

-  /** to ITE function for function model nodes */

-  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }

-};

-

-class UfModelTreeGenerator

-{

-private:

-  //store for set values

-  Node d_default_value;

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

-  // defaults

-  std::vector< Node > d_defaults;

-  Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround );

-public:

-  UfModelTreeGenerator(){}

-  ~UfModelTreeGenerator(){}

-  /** set default value */

-  void setDefaultValue( Node v ) { d_default_value = v; }

-  /** set value */

-  void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true );

-  /** make model */

-  void makeModel( TheoryModel* m, UfModelTree& tree );

-  /** uses partial default values */

-  bool optUsePartialDefaults();

-  /** reset */

-  void clear();

-};

-

-//this class stores temporary information useful to model engine for constructing model

-class UfModelPreferenceData

-{

-public:

-  UfModelPreferenceData() : d_reconsiderModel( false ){}

-  virtual ~UfModelPreferenceData(){}

-  Node d_const_val;

-  // preferences for default values

-  std::vector< Node > d_values;

-  std::map< Node, std::vector< Node > > d_value_pro_con[2];

-  std::map< Node, std::vector< Node > > d_term_pro_con[2];

-  bool d_reconsiderModel;

-  /** set value preference */

-  void setValuePreference( Node f, Node n, Node r, bool isPro );

-  /** get best default value */

-  Node getBestDefaultValue( Node defaultTerm, TheoryModel* m );

-};

-

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file theory_uf_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 for Theory UF
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_UF_MODEL_H
+#define __CVC4__THEORY_UF_MODEL_H
+
+#include "theory/model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class UfModelTreeNode
+{
+public:
+  UfModelTreeNode(){}
+  /** the data */
+  std::map< Node, UfModelTreeNode > d_data;
+  /** the value of this tree node (if all paths lead to same value) */
+  Node d_value;
+  /** has concrete argument defintion */
+  bool hasConcreteArgumentDefinition();
+public:
+  //is this model tree empty?
+  bool isEmpty() { return d_data.empty() && d_value.isNull(); }
+  //clear
+  void clear();
+  /** setValue function */
+  void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
+  /**  getValue function */
+  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
+  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );
+  /** getConstant Value function */
+  Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
+  /** getFunctionValue */
+  Node getFunctionValue();
+  /** simplify function */
+  void simplify( Node op, Node defaultVal, int argIndex );
+  /** is total ? */
+  bool isTotal( Node op, int argIndex );
+public:
+  void debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind = 0, int arg = 0 );
+};
+
+class UfModelTree
+{
+private:
+  //the op this model is for
+  Node d_op;
+  //the order we will treat the arguments
+  std::vector< int > d_index_order;
+  //the data
+  UfModelTreeNode d_tree;
+public:
+  //constructors
+  UfModelTree(){}
+  UfModelTree( Node op ) : d_op( op ){
+    TypeNode tn = d_op.getType();
+    for( int i=0; i<(int)(tn.getNumChildren()-1); i++ ){
+      d_index_order.push_back( i );
+    }
+  }
+  UfModelTree( Node op, std::vector< int >& indexOrder ) : d_op( op ){
+    d_index_order.insert( d_index_order.end(), indexOrder.begin(), indexOrder.end() );
+  }
+  /** clear/reset the function */
+  void clear() { d_tree.clear(); }
+  /** setValue function
+    *
+    * For each argument of n with ModelBasisAttribute() set to true will be considered default arguments if ground=false
+    *
+    */
+  void setValue( TheoryModel* m, Node n, Node v, bool ground = true ){
+    d_tree.setValue( m, n, v, d_index_order, ground, 0 );
+  }
+  /** setDefaultValue function */
+  void setDefaultValue( TheoryModel* m, Node v ){
+    d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
+  }
+  /**  getValue function
+    *
+    *  returns val, the value of ground term n
+    *  Say n is f( t_0...t_n )
+    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val
+    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
+    *      then g( a, a, a ) would return b with depIndex = 1
+    *
+    */
+  Node getValue( TheoryModel* m, Node n, int& depIndex ){
+    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
+  }
+  /** -> implementation incomplete */
+  Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){
+    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
+  }
+  /** getConstantValue function
+    *
+    * given term n, where n may contain "all value" arguments, aka model basis arguments
+    *   if n is null, then every argument of n is considered "all value"
+    * if n is constant for the entire domain specified by n, then this function returns the value of its domain
+    * otherwise, it returns null
+    * for example, say the term e represents "all values"
+    *   if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
+    *     then f( a, e ) would return b, while f( e, a ) would return null
+    *  -> implementation incomplete
+    */
+  Node getConstantValue( TheoryModel* m, Node n ) {
+    return d_tree.getConstantValue( m, n, d_index_order, 0 );
+  }
+  /** getFunctionValue
+    *   Returns a compact representation of this function, of kind FUNCTION_MODEL.
+    *   See documentation in theory/uf/kinds
+    */
+  Node getFunctionValue(){
+    return d_tree.getFunctionValue();
+  }
+  /** simplify the tree */
+  void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
+  /** is this tree total? */
+  bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
+  /** is this function constant? */
+  bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }
+  /** is this tree empty? */
+  bool isEmpty() { return d_tree.isEmpty(); }
+public:
+  void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){
+    d_tree.debugPrint( out, m, d_index_order, ind );
+  }
+private:
+  //helper for to ITE function.
+  static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode );
+public:
+  /** to ITE function for function model nodes */
+  static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }
+};
+
+class UfModelTreeGenerator
+{
+private:
+  //store for set values
+  Node d_default_value;
+  std::map< Node, Node > d_set_values[2][2];
+  // defaults
+  std::vector< Node > d_defaults;
+  Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround );
+public:
+  UfModelTreeGenerator(){}
+  ~UfModelTreeGenerator(){}
+  /** set default value */
+  void setDefaultValue( Node v ) { d_default_value = v; }
+  /** set value */
+  void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true );
+  /** make model */
+  void makeModel( TheoryModel* m, UfModelTree& tree );
+  /** uses partial default values */
+  bool optUsePartialDefaults();
+  /** reset */
+  void clear();
+};
+
+//this class stores temporary information useful to model engine for constructing model
+class UfModelPreferenceData
+{
+public:
+  UfModelPreferenceData() : d_reconsiderModel( false ){}
+  virtual ~UfModelPreferenceData(){}
+  Node d_const_val;
+  // preferences for default values
+  std::vector< Node > d_values;
+  std::map< Node, std::vector< Node > > d_value_pro_con[2];
+  std::map< Node, std::vector< Node > > d_term_pro_con[2];
+  bool d_reconsiderModel;
+  /** set value preference */
+  void setValuePreference( Node f, Node n, Node r, bool isPro );
+  /** get best default value */
+  Node getBestDefaultValue( Node defaultTerm, TheoryModel* m );
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/util/model.cpp b/src/util/model.cpp
index 081624c5d..50683fdff 100644
--- a/src/util/model.cpp
+++ b/src/util/model.cpp
@@ -1,15 +1,15 @@
-/*********************                                                        */

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

+/*********************                                                        */
+/*! \file 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 class
  **/
\ No newline at end of file
diff --git a/src/util/model.h b/src/util/model.h
index 7e0f5a723..60f1ab23f 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -1,42 +1,42 @@
-/*********************                                                        */

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

- **/

-

-#include "cvc4_public.h"

-

-#ifndef __CVC4__MODEL_H

-#define __CVC4__MODEL_H

-

-#include <iostream>

-

-namespace CVC4 {

-

-class Model

-{

-public:

-  virtual void toStream(std::ostream& out) = 0;

-};/* class Model */

-

-class ModelBuilder

-{

-public:

-  ModelBuilder(){}

-  virtual ~ModelBuilder(){}

-  virtual void buildModel( Model* m ) = 0;

-};/* class ModelBuilder */

-

-}/* CVC4 namespace */

-

-#endif  /* __CVC4__MODEL_H */

+/*********************                                                        */
+/*! \file 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 class
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+class Model
+{
+public:
+  virtual void toStream(std::ostream& out) = 0;
+};/* class Model */
+
+class ModelBuilder
+{
+public:
+  ModelBuilder(){}
+  virtual ~ModelBuilder(){}
+  virtual void buildModel( Model* m ) = 0;
+};/* class ModelBuilder */
+
+}/* CVC4 namespace */
+
+#endif  /* __CVC4__MODEL_H */