dos2unix conversion for a number of files; this avoids spurious conflicts when merging to master

14 files changed, 2992 insertions, 2992 deletions

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index d3bd6ad03..b5f92c5f8 100755
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -1,298 +1,298 @@
-/*********************                                                        */

-/*! \file inst_gen.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 inst gen classes

- **/

-

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

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

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

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

-

-//#define CHILD_USE_CONSIDER

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-

-

-

-InstGenProcess::InstGenProcess( Node n ) : d_node( n ){

-  Assert( n.hasAttribute(InstConstantAttribute()) );

-  int count = 0;

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

-    if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){

-      d_children.push_back( InstGenProcess( n[i] ) );

-      d_children_index.push_back( i );

-      d_children_map[ i ] = count;

-      count++;

-    }

-  }

-}

-

-void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){

-  if( !qe->existsInstantiation( f, m, true ) ){

-    //make sure no duplicates are produced

-    if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){

-      d_match_values.push_back( val );

-      d_matches.push_back( InstMatch( &m ) );

-      qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;

-    }

-  }

-}

-

-void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){

-  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;

-  //whether we are doing a product or sum or matches

-  bool doProduct = true;

-  //get the model

-  FirstOrderModel* fm = qe->getModel();

-

-  //calculate terms we will consider

-  std::vector< Node > considerTerms;

-  std::vector< std::vector< Node > > newConsiderVal;

-  std::vector< bool > newUseConsider;

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

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

-  newConsiderVal.resize( d_children.size() );

-  newUseConsider.resize( d_children.size(), useConsider );

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

-    Node op = d_node.getOperator();

-    if( useConsider ){

-#ifndef CHILD_USE_CONSIDER

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

-        newUseConsider[i] = false;

-      }

-#endif

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

-        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),

-                                 qe->getEqualityQuery()->getEngine() );

-        while( !eqc.isFinished() ){

-          Node en = (*eqc);

-          if( en.getKind()==APPLY_UF && en.getOperator()==op ){

-              considerTerms.push_back( en );

-          }

-          ++eqc;

-        }

-      }

-    }else{

-      considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );

-    }

-    //for each term we consider, calculate a current match

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

-      Node n = considerTerms[i];

-      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );

-      bool hadSuccess CVC4_UNUSED = false;

-      for( int t=(isSelected ? 0 : 1); t<2; t++ ){

-        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){

-          considerTermsMatch[t][n] = InstMatch();

-          considerTermsSuccess[t][n] = true;

-          for( size_t j=0; j<d_node.getNumChildren(); j++ ){

-            if( d_children_map.find( j )==d_children_map.end() ){

-              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){

-                if( d_node[j].getKind()==INST_CONSTANT ){

-                  if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){

-                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";

-                    Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;

-                    considerTermsSuccess[t][n] = false;

-                    break;

-                  }

-                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){

-                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;

-                  considerTermsSuccess[t][n] = false;

-                  break;

-                }

-              }

-            }

-          }

-          //if successful, store it

-          if( considerTermsSuccess[t][n] ){

-#ifdef CHILD_USE_CONSIDER

-            if( !hadSuccess ){

-              hadSuccess = true;

-              for( size_t k=0; k<d_children.size(); k++ ){

-                if( newUseConsider[k] ){

-                  int childIndex = d_children_index[k];

-                  //determine if we are restricted or not

-                  if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){

-                    Node r = qe->getModel()->getRepresentative( n[childIndex] );

-                    if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){

-                      newConsiderVal[k].push_back( r );

-                      //check if we now need to consider the entire domain

-                      TypeNode tn = r.getType();

-                      if( qe->getModel()->d_rep_set.hasType( tn ) ){

-                        if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){

-                          newConsiderVal[k].clear();

-                          newUseConsider[k] = false;

-                        }

-                      }

-                    }

-                  }else{

-                    //matching against selected term, will need to consider all values

-                    newConsiderVal[k].clear();

-                    newUseConsider[k] = false;

-                  }

-                }

-              }

-            }

-#endif

-          }

-        }

-      }

-    }

-  }else{

-    //the interpretted case

-    if( d_node.getType().isBoolean() ){

-      if( useConsider ){

-        //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }

-        Assert( considerVal.size()==1 );

-        bool reqPol = considerVal[0]==fm->d_true;

-        Node ncv = considerVal[0];

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

-          ncv = reqPol ? fm->d_false : fm->d_true;

-        }

-        if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){

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

-            newConsiderVal[i].push_back( ncv );

-          }

-          //instead we will do a sum

-          if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){

-            doProduct = false;

-          }

-        }else{

-          //do not use consider

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

-            newUseConsider[i] = false;

-          }

-        }

-      }

-    }

-  }

-

-  //calculate all matches for children

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

-    d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );

-    if( doProduct && d_children[i].getNumMatches()==0 ){

-      return;

-    }

-  }

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

-    //if this is an uninterpreted function

-    Node op = d_node.getOperator();

-    //process all values

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

-      Node n = considerTerms[i];

-      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );

-      for( int t=(isSelected ? 0 : 1); t<2; t++ ){

-        //do not consider ground case if it is already congruent to another ground term

-        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){

-          Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;

-          if( considerTermsSuccess[t][n] ){

-            //try to find unifier for d_node = n

-            calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );

-          }

-        }

-      }

-    }

-  }else{

-    //if this is an interpreted function

-    if( doProduct ){

-      //combining children matches

-      InstMatch curr;

-      std::vector< Node > terms;

-      calculateMatchesInterpreted( qe, f, curr, terms, 0 );

-    }else{

-      //summing children matches

-      Assert( considerVal.size()==1 );

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

-        for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){

-          InstMatch m;

-          if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){

-            addMatchValue( qe, f, considerVal[0], m );

-          }

-        }

-      }

-    }

-  }

-  Trace("inst-gen-cm") << "done calculate matches" << std::endl;

-  //can clear information used for finding duplicates

-  d_inst_trie.clear();

-}

-

-bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){

-  //FIXME: is this correct? (query may not be accurate)

-  return m.merge( q, d_matches[i] );

-}

-

-void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){

-  if( childIndex==(int)d_children.size() ){

-    Node val = qe->getModel()->getRepresentative( n );  //FIXME: is this correct?

-    Trace("inst-gen-cm") << "  - u-match : " << val << std::endl;

-    Trace("inst-gen-cm") << "            : " << curr << std::endl;

-    addMatchValue( qe, f, val, curr );

-  }else{

-    Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl;

-    bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) );

-    for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){

-      //FIXME: is this correct?

-      if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){

-        InstMatch next( &curr );

-        if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){

-          calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected );

-        }else{

-          Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl;

-          Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl;

-        }

-      }else{

-        Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl;

-      }

-    }

-  }

-}

-

-void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){

-  FirstOrderModel* fm = qe->getModel();

-  if( argIndex==(int)d_node.getNumChildren() ){

-    Node val;

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

-      val = d_node;

-    }else if( d_node.getKind()==EQUAL ){

-      val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false;

-    }else{

-      val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );

-      val = Rewriter::rewrite( val );

-    }

-    Trace("inst-gen-cm") << "  - i-match : " << d_node << std::endl;

-    Trace("inst-gen-cm") << "            : " << val << std::endl;

-    Trace("inst-gen-cm") << "            : " << curr << std::endl;

-    addMatchValue( qe, f, val, curr );

-  }else{

-    if( d_children_map.find( argIndex )==d_children_map.end() ){

-      terms.push_back( fm->getRepresentative( d_node[argIndex] ) );

-      calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 );

-      terms.pop_back();

-    }else{

-      for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){

-        InstMatch next( &curr );

-        if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){

-          terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) );

-          calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 );

-          terms.pop_back();

-        }

-      }

-    }

-  }

-}

+/*********************                                                        */
+/*! \file inst_gen.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 inst gen classes
+ **/
+
+#include "theory/quantifiers/inst_gen.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+//#define CHILD_USE_CONSIDER
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+
+
+InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
+  Assert( n.hasAttribute(InstConstantAttribute()) );
+  int count = 0;
+  for( size_t i=0; i<n.getNumChildren(); i++ ){
+    if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){
+      d_children.push_back( InstGenProcess( n[i] ) );
+      d_children_index.push_back( i );
+      d_children_map[ i ] = count;
+      count++;
+    }
+  }
+}
+
+void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){
+  if( !qe->existsInstantiation( f, m, true ) ){
+    //make sure no duplicates are produced
+    if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
+      d_match_values.push_back( val );
+      d_matches.push_back( InstMatch( &m ) );
+      qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;
+    }
+  }
+}
+
+void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){
+  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
+  //whether we are doing a product or sum or matches
+  bool doProduct = true;
+  //get the model
+  FirstOrderModel* fm = qe->getModel();
+
+  //calculate terms we will consider
+  std::vector< Node > considerTerms;
+  std::vector< std::vector< Node > > newConsiderVal;
+  std::vector< bool > newUseConsider;
+  std::map< Node, InstMatch > considerTermsMatch[2];
+  std::map< Node, bool > considerTermsSuccess[2];
+  newConsiderVal.resize( d_children.size() );
+  newUseConsider.resize( d_children.size(), useConsider );
+  if( d_node.getKind()==APPLY_UF ){
+    Node op = d_node.getOperator();
+    if( useConsider ){
+#ifndef CHILD_USE_CONSIDER
+      for( size_t i=0; i<newUseConsider.size(); i++ ){
+        newUseConsider[i] = false;
+      }
+#endif
+      for( size_t i=0; i<considerVal.size(); i++ ){
+        eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),
+                                 qe->getEqualityQuery()->getEngine() );
+        while( !eqc.isFinished() ){
+          Node en = (*eqc);
+          if( en.getKind()==APPLY_UF && en.getOperator()==op ){
+              considerTerms.push_back( en );
+          }
+          ++eqc;
+        }
+      }
+    }else{
+      considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );
+    }
+    //for each term we consider, calculate a current match
+    for( size_t i=0; i<considerTerms.size(); i++ ){
+      Node n = considerTerms[i];
+      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+      bool hadSuccess CVC4_UNUSED = false;
+      for( int t=(isSelected ? 0 : 1); t<2; t++ ){
+        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
+          considerTermsMatch[t][n] = InstMatch();
+          considerTermsSuccess[t][n] = true;
+          for( size_t j=0; j<d_node.getNumChildren(); j++ ){
+            if( d_children_map.find( j )==d_children_map.end() ){
+              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
+                if( d_node[j].getKind()==INST_CONSTANT ){
+                  if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
+                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
+                    Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;
+                    considerTermsSuccess[t][n] = false;
+                    break;
+                  }
+                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
+                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
+                  considerTermsSuccess[t][n] = false;
+                  break;
+                }
+              }
+            }
+          }
+          //if successful, store it
+          if( considerTermsSuccess[t][n] ){
+#ifdef CHILD_USE_CONSIDER
+            if( !hadSuccess ){
+              hadSuccess = true;
+              for( size_t k=0; k<d_children.size(); k++ ){
+                if( newUseConsider[k] ){
+                  int childIndex = d_children_index[k];
+                  //determine if we are restricted or not
+                  if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
+                    Node r = qe->getModel()->getRepresentative( n[childIndex] );
+                    if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){
+                      newConsiderVal[k].push_back( r );
+                      //check if we now need to consider the entire domain
+                      TypeNode tn = r.getType();
+                      if( qe->getModel()->d_rep_set.hasType( tn ) ){
+                        if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){
+                          newConsiderVal[k].clear();
+                          newUseConsider[k] = false;
+                        }
+                      }
+                    }
+                  }else{
+                    //matching against selected term, will need to consider all values
+                    newConsiderVal[k].clear();
+                    newUseConsider[k] = false;
+                  }
+                }
+              }
+            }
+#endif
+          }
+        }
+      }
+    }
+  }else{
+    //the interpretted case
+    if( d_node.getType().isBoolean() ){
+      if( useConsider ){
+        //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }
+        Assert( considerVal.size()==1 );
+        bool reqPol = considerVal[0]==fm->d_true;
+        Node ncv = considerVal[0];
+        if( d_node.getKind()==NOT ){
+          ncv = reqPol ? fm->d_false : fm->d_true;
+        }
+        if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){
+          for( size_t i=0; i<newConsiderVal.size(); i++ ){
+            newConsiderVal[i].push_back( ncv );
+          }
+          //instead we will do a sum
+          if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){
+            doProduct = false;
+          }
+        }else{
+          //do not use consider
+          for( size_t i=0; i<newUseConsider.size(); i++ ){
+            newUseConsider[i] = false;
+          }
+        }
+      }
+    }
+  }
+
+  //calculate all matches for children
+  for( int i=0; i<(int)d_children.size(); i++ ){
+    d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );
+    if( doProduct && d_children[i].getNumMatches()==0 ){
+      return;
+    }
+  }
+  if( d_node.getKind()==APPLY_UF ){
+    //if this is an uninterpreted function
+    Node op = d_node.getOperator();
+    //process all values
+    for( size_t i=0; i<considerTerms.size(); i++ ){
+      Node n = considerTerms[i];
+      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+      for( int t=(isSelected ? 0 : 1); t<2; t++ ){
+        //do not consider ground case if it is already congruent to another ground term
+        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
+          Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;
+          if( considerTermsSuccess[t][n] ){
+            //try to find unifier for d_node = n
+            calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );
+          }
+        }
+      }
+    }
+  }else{
+    //if this is an interpreted function
+    if( doProduct ){
+      //combining children matches
+      InstMatch curr;
+      std::vector< Node > terms;
+      calculateMatchesInterpreted( qe, f, curr, terms, 0 );
+    }else{
+      //summing children matches
+      Assert( considerVal.size()==1 );
+      for( int i=0; i<(int)d_children.size(); i++ ){
+        for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){
+          InstMatch m;
+          if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){
+            addMatchValue( qe, f, considerVal[0], m );
+          }
+        }
+      }
+    }
+  }
+  Trace("inst-gen-cm") << "done calculate matches" << std::endl;
+  //can clear information used for finding duplicates
+  d_inst_trie.clear();
+}
+
+bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){
+  //FIXME: is this correct? (query may not be accurate)
+  return m.merge( q, d_matches[i] );
+}
+
+void InstGenProcess::calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected ){
+  if( childIndex==(int)d_children.size() ){
+    Node val = qe->getModel()->getRepresentative( n );  //FIXME: is this correct?
+    Trace("inst-gen-cm") << "  - u-match : " << val << std::endl;
+    Trace("inst-gen-cm") << "            : " << curr << std::endl;
+    addMatchValue( qe, f, val, curr );
+  }else{
+    Trace("inst-gen-cm") << "Consider child index = " << childIndex << ", against ground term argument " << d_children_index[childIndex] << " ... " << n[d_children_index[childIndex]] << std::endl;
+    bool sel = ( isSelected && n[d_children_index[childIndex]].getAttribute(ModelBasisAttribute()) );
+    for( int i=0; i<(int)d_children[ childIndex ].getNumMatches(); i++ ){
+      //FIXME: is this correct?
+      if( sel || qe->getEqualityQuery()->areEqual( d_children[ childIndex ].getMatchValue( i ), n[d_children_index[childIndex]] ) ){
+        InstMatch next( &curr );
+        if( d_children[ childIndex ].getMatch( qe->getEqualityQuery(), i, next ) ){
+          calculateMatchesUninterpreted( qe, f, next, n, childIndex+1, isSelected );
+        }else{
+          Trace("inst-gen-cm") << curr << " not equal to " << d_children[ childIndex ].d_matches[i] << std::endl;
+          Trace("inst-gen-cm") << childIndex << " match " << i << " not equal subs." << std::endl;
+        }
+      }else{
+        Trace("inst-gen-cm") << childIndex << " match " << i << " not equal value." << std::endl;
+      }
+    }
+  }
+}
+
+void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex ){
+  FirstOrderModel* fm = qe->getModel();
+  if( argIndex==(int)d_node.getNumChildren() ){
+    Node val;
+    if( d_node.getNumChildren()==0 ){
+      val = d_node;
+    }else if( d_node.getKind()==EQUAL ){
+      val = qe->getEqualityQuery()->areEqual( terms[0], terms[1] ) ? fm->d_true : fm->d_false;
+    }else{
+      val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );
+      val = Rewriter::rewrite( val );
+    }
+    Trace("inst-gen-cm") << "  - i-match : " << d_node << std::endl;
+    Trace("inst-gen-cm") << "            : " << val << std::endl;
+    Trace("inst-gen-cm") << "            : " << curr << std::endl;
+    addMatchValue( qe, f, val, curr );
+  }else{
+    if( d_children_map.find( argIndex )==d_children_map.end() ){
+      terms.push_back( fm->getRepresentative( d_node[argIndex] ) );
+      calculateMatchesInterpreted( qe, f, curr, terms, argIndex+1 );
+      terms.pop_back();
+    }else{
+      for( int i=0; i<(int)d_children[ d_children_map[argIndex] ].getNumMatches(); i++ ){
+        InstMatch next( &curr );
+        if( d_children[ d_children_map[argIndex] ].getMatch( qe->getEqualityQuery(), i, next ) ){
+          terms.push_back( d_children[ d_children_map[argIndex] ].getMatchValue( i ) );
+          calculateMatchesInterpreted( qe, f, next, terms, argIndex+1 );
+          terms.pop_back();
+        }
+      }
+    }
+  }
+}
diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h
index f6e6a372e..c8de2c642 100755
--- a/src/theory/quantifiers/inst_gen.h
+++ b/src/theory/quantifiers/inst_gen.h
@@ -1,61 +1,61 @@
-/*********************                                                        */

-/*! \file inst_gen.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-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 Inst Gen classes

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H

-#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H

-

-#include "theory/quantifiers_engine.h"

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

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class InstGenProcess

-{

-private:

-  //the node we are processing

-  Node d_node;

-  //the sub children for this node

-  std::vector< InstGenProcess > d_children;

-  std::vector< int > d_children_index;

-  std::map< int, int > d_children_map;

-  //the matches we have produced

-  std::vector< InstMatch > d_matches;

-  std::vector< Node > d_match_values;

-  //add match value

-  std::map< Node, inst::InstMatchTrie > d_inst_trie;

-  void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m );

-private:

-  void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected );

-  void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex );

-public:

-  InstGenProcess( Node n );

-  virtual ~InstGenProcess(){}

-

-  void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider );

-  int getNumMatches() { return d_matches.size(); }

-  bool getMatch( EqualityQuery* q, int i, InstMatch& m );

-  Node getMatchValue( int i ) { return d_match_values[i]; }

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file inst_gen.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-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 Inst Gen classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_GEN_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/inst_match.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class InstGenProcess
+{
+private:
+  //the node we are processing
+  Node d_node;
+  //the sub children for this node
+  std::vector< InstGenProcess > d_children;
+  std::vector< int > d_children_index;
+  std::map< int, int > d_children_map;
+  //the matches we have produced
+  std::vector< InstMatch > d_matches;
+  std::vector< Node > d_match_values;
+  //add match value
+  std::map< Node, inst::InstMatchTrie > d_inst_trie;
+  void addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m );
+private:
+  void calculateMatchesUninterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, Node n, int childIndex, bool isSelected );
+  void calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, InstMatch& curr, std::vector< Node >& terms, int argIndex );
+public:
+  InstGenProcess( Node n );
+  virtual ~InstGenProcess(){}
+
+  void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider );
+  int getNumMatches() { return d_matches.size(); }
+  bool getMatch( EqualityQuery* q, int i, InstMatch& m );
+  Node getMatchValue( int i ) { return d_match_values[i]; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 3b5e594fb..2822597e1 100755
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -1,664 +1,664 @@
-/*********************                                                        */

-/*! \file inst_match_generator.cpp

-** \verbatim

-** Original author: ajreynol

-** Major contributors: bobot

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

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

-** Copyright (c) 2009-2012  New York University and The University of Iowa

-** See the file COPYING in the top-level source directory for licensing

-** information.\endverbatim

-**

-** \brief Implementation of inst match generator class

-**/

-

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

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

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

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

-#include "theory/quantifiers_engine.h"

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-

-namespace CVC4 {

-namespace theory {

-namespace inst {

-

-

-InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){

-  initializePattern( pat, qe );

-}

-

-InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){

-  if( pats.size()==1 ){

-    initializePattern( pats[0], qe );

-  }else{

-    initializePatterns( pats, qe );

-  }

-}

-

-void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){

-  int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;

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

-    d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );

-  }

-  d_pattern = Node::null();

-  d_match_pattern = Node::null();

-  d_cg = NULL;

-}

-

-void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){

-  Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;

-  Assert( pat.hasAttribute(InstConstantAttribute()) );

-  d_pattern = pat;

-  d_match_pattern = pat;

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

-    //we want to add the children of the NOT

-    d_match_pattern = d_pattern[0];

-  }

-  if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){

-    if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){

-      Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );

-      //swap sides

-      d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );

-      d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;

-      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching

-        d_match_pattern = d_match_pattern[1];

-      }else{

-        d_match_pattern = d_pattern[0][0];

-      }

-    }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){

-      Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );

-      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching

-        d_match_pattern = d_match_pattern[0];

-      }

-    }

-  }

-  int childMatchPolicy = MATCH_GEN_DEFAULT;

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

-    if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){

-      if( d_match_pattern[i].getKind()!=INST_CONSTANT ){

-        d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );

-        d_children_index.push_back( i );

-      }

-    }

-  }

-

-  Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;

-

-  //create candidate generator

-  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){

-    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );

-    //we will be producing candidates via literal matching heuristics

-    if( d_pattern.getKind()!=NOT ){

-      //candidates will be all equalities

-      d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );

-    }else{

-      //candidates will be all disequalities

-      d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );

-    }

-  }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){

-    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );

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

-      Unimplemented("Disequal generator unimplemented");

-    }else{

-      Assert( Trigger::isAtomicTrigger( d_match_pattern ) );

-      //we are matching only in a particular equivalence class

-      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );

-      //store the equivalence class that we will call d_cg->reset( ... ) on

-      d_eq_class = d_pattern[1];

-    }

-  }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){

-    //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){

-      //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;

-    //}

-    //we will be scanning lists trying to find d_match_pattern.getOperator()

-    d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );

-  }else{

-    d_cg = new CandidateGeneratorQueue;

-    if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){

-      Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

-      //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;

-      d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;

-    }else{

-      Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;

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

-        Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;

-      }

-      //we will treat this as match gen internal arithmetic

-      d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;

-    }

-  }

-}

-

-/** get match (not modulo equality) */

-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){

-  Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("

-                    << m.size() << ")" << ", " << d_children.size() << std::endl;

-  Assert( !d_match_pattern.isNull() );

-  if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){

-    return true;

-  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){

-    return getMatchArithmetic( t, m, qe );

-  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){

-    return false;

-  }else{

-    EqualityQuery* q = qe->getEqualityQuery();

-    //add m to partial match vector

-    std::vector< InstMatch > partial;

-    partial.push_back( InstMatch( &m ) );

-    //if t is null

-    Assert( !t.isNull() );

-    Assert( !t.hasAttribute(InstConstantAttribute()) );

-    Assert( t.getKind()==d_match_pattern.getKind() );

-    Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );

-    //first, check if ground arguments are not equal, or a match is in conflict

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

-      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){

-        if( d_match_pattern[i].getKind()==INST_CONSTANT ){

-          if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){

-            //match is in conflict

-            Debug("matching-debug") << "Match in conflict " << t[i] << " and "

-                                    << d_match_pattern[i] << " because "

-                                    << partial[0].get(d_match_pattern[i])

-                                    << std::endl;

-            Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;

-            return false;

-          }

-        }

-      }else{

-        if( !q->areEqual( d_match_pattern[i], t[i] ) ){

-          Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;

-          //ground arguments are not equal

-          return false;

-        }

-      }

-    }

-    //now, fit children into match

-    //we will be requesting candidates for matching terms for each child

-    std::vector< Node > reps;

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

-      Node rep = q->getRepresentative( t[ d_children_index[i] ] );

-      reps.push_back( rep );

-      d_children[i]->d_cg->reset( rep );

-    }

-

-    //combine child matches

-    int index = 0;

-    while( index>=0 && index<(int)d_children.size() ){

-      partial.push_back( InstMatch( &partial[index] ) );

-      if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){

-        index++;

-      }else{

-        d_children[index]->d_cg->reset( reps[index] );

-        partial.pop_back();

-        if( !partial.empty() ){

-          partial.pop_back();

-        }

-        index--;

-      }

-    }

-    if( index>=0 ){

-      m = partial.back();

-      return true;

-    }else{

-      return false;

-    }

-  }

-}

-

-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){

-  bool success = false;

-  Node t;

-  do{

-    //get the next candidate term t

-    t = d_cg->getNextCandidate();

-    //if t not null, try to fit it into match m

-    if( !t.isNull() && t.getType()==d_match_pattern.getType() ){

-      success = getMatch( t, m, qe );

-    }

-  }while( !success && !t.isNull() );

-  if (saveMatched) m.d_matched = t;

-  return success;

-}

-

-bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){

-  Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;

-  if( !d_arith_coeffs.empty() ){

-    NodeBuilder<> tb(kind::PLUS);

-    Node ic = Node::null();

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

-      Debug("matching-arith") << it->first << " -> " << it->second << std::endl;

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

-        if( m.find( it->first )==m.end() ){

-          //see if we can choose this to set

-          if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){

-            ic = it->first;

-          }

-        }else{

-          Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;

-          Node tm = m.get( it->first );

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

-            tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );

-          }

-          tb << tm;

-        }

-      }else{

-        tb << it->second;

-      }

-    }

-    if( !ic.isNull() ){

-      Node tm;

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

-        tm = t;

-      }else{

-        tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;

-        tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );

-      }

-      if( !d_arith_coeffs[ ic ].isNull() ){

-        Assert( !ic.getType().isInteger() );

-        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );

-        tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );

-      }

-      m.set( ic, Rewriter::rewrite( tm ));

-      //set the rest to zeros

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

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

-          if( m.find( it->first )==m.end() ){

-            m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );

-          }

-        }

-      }

-      Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;

-      return true;

-    }else{

-      return false;

-    }

-  }else{

-    return false;

-  }

-}

-

-

-/** reset instantiation round */

-void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){

-  if( d_match_pattern.isNull() ){

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

-      d_children[i]->resetInstantiationRound( qe );

-    }

-  }else{

-    if( d_cg ){

-      d_cg->resetInstantiationRound();

-    }

-  }

-}

-

-void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){

-  if( d_match_pattern.isNull() ){

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

-      d_children[i]->reset( eqc, qe );

-    }

-    d_partial.clear();

-  }else{

-    if( !d_eq_class.isNull() ){

-      //we have a specific equivalence class in mind

-      //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term

-      //just look in equivalence class of the RHS

-      d_cg->reset( d_eq_class );

-    }else{

-      d_cg->reset( eqc );

-    }

-  }

-}

-

-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){

-  m.d_matched = Node::null();

-  if( d_match_pattern.isNull() ){

-    int index = (int)d_partial.size();

-    while( index>=0 && index<(int)d_children.size() ){

-      if( index>0 ){

-        d_partial.push_back( InstMatch( &d_partial[index-1] ) );

-      }else{

-        d_partial.push_back( InstMatch() );

-      }

-      if( d_children[index]->getNextMatch( d_partial[index], qe ) ){

-        index++;

-      }else{

-        d_children[index]->reset( Node::null(), qe );

-        d_partial.pop_back();

-        if( !d_partial.empty() ){

-          d_partial.pop_back();

-        }

-        index--;

-      }

-    }

-    if( index>=0 ){

-      m = d_partial.back();

-      d_partial.pop_back();

-      return true;

-    }else{

-      return false;

-    }

-  }else{

-    bool res = getNextMatch2( m, qe, true );

-    Assert(!res || !m.d_matched.isNull());

-    return res;

-  }

-}

-

-

-

-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

-  //now, try to add instantiation for each match produced

-  int addedLemmas = 0;

-  InstMatch m;

-  while( getNextMatch( m, qe ) ){

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

-    m.add( baseMatch );

-    if( qe->addInstantiation( f, m ) ){

-      addedLemmas++;

-      if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){

-        return addedLemmas;

-      }

-    }

-    m.clear();

-  }

-  //return number of lemmas added

-  return addedLemmas;

-}

-

-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){

-  Assert( options::eagerInstQuant() );

-  if( !d_match_pattern.isNull() ){

-    InstMatch m;

-    if( getMatch( t, m, qe ) ){

-      if( qe->addInstantiation( f, m ) ){

-        return 1;

-      }

-    }

-  }else{

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

-      d_children[i]->addTerm( f, t, qe );

-    }

-  }

-  return 0;

-}

-

-/** constructors */

-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :

-d_f( f ){

-  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;

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

-  qe->getTermDatabase()->getVarContains( f, pats, var_contains );

-  //convert to indicies

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

-    Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";

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

-      Debug("smart-multi-trigger") << it->second[i] << " ";

-      int index = it->second[i].getAttribute(InstVarNumAttribute());

-      d_var_contains[ it->first ].push_back( index );

-      d_var_to_node[ index ].push_back( it->first );

-    }

-    Debug("smart-multi-trigger") << std::endl;

-  }

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

-    Node n = pats[i];

-    //make the match generator

-    d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );

-    //compute unique/shared variables

-    std::vector< int > unique_vars;

-    std::map< int, bool > shared_vars;

-    int numSharedVars = 0;

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

-      if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){

-        Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;

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

-      }else{

-        shared_vars[ d_var_contains[n][j] ] = true;

-        numSharedVars++;

-      }

-    }

-    //we use the latest shared variables, then unique variables

-    std::vector< int > vars;

-    int index = i==0 ? (int)(pats.size()-1) : (i-1);

-    while( numSharedVars>0 && index!=i ){

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

-        if( it->second ){

-          if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=

-              d_var_contains[ pats[index] ].end() ){

-            vars.push_back( it->first );

-            shared_vars[ it->first ] = false;

-            numSharedVars--;

-          }

-        }

-      }

-      index = index==0 ? (int)(pats.size()-1) : (index-1);

-    }

-    vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );

-    Debug("smart-multi-trigger") << "   Index[" << i << "]: ";

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

-      Debug("smart-multi-trigger") << vars[i] << " ";

-    }

-    Debug("smart-multi-trigger") << std::endl;

-    //make ordered inst match trie

-    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;

-    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );

-    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );

-  }

-

-}

-

-/** reset instantiation round (call this whenever equivalence classes have changed) */

-void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){

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

-    d_children[i]->resetInstantiationRound( qe );

-  }

-}

-

-/** reset, eqc is the equivalence class to search in (any if eqc=null) */

-void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){

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

-    d_children[i]->reset( eqc, qe );

-  }

-}

-

-int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

-  int addedLemmas = 0;

-  Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;

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

-    Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;

-    std::vector< InstMatch > newMatches;

-    InstMatch m;

-    while( d_children[i]->getNextMatch( m, qe ) ){

-      m.makeRepresentative( qe );

-      newMatches.push_back( InstMatch( &m ) );

-      m.clear();

-    }

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

-      processNewMatch( qe, newMatches[j], i, addedLemmas );

-    }

-  }

-  return addedLemmas;

-}

-

-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){

-  //see if these produce new matches

-  d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );

-  //possibly only do the following if we know that new matches will be produced?

-  //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that

-  // we can safely skip the following lines, even when we have already produced this match.

-  Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;

-  //process new instantiations

-  int childIndex = (fromChildIndex+1)%(int)d_children.size();

-  std::vector< IndexedTrie > unique_var_tries;

-  processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),

-                            unique_var_tries, 0, childIndex, fromChildIndex, true );

-}

-

-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,

-                                                        std::vector< IndexedTrie >& unique_var_tries,

-                                                        int trieIndex, int childIndex, int endChildIndex, bool modEq ){

-  if( childIndex==endChildIndex ){

-    //now, process unique variables

-    processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );

-  }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){

-    int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];

-    Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );

-    if( m.find( curr_ic )==m.end() ){

-      //if( d_var_to_node[ curr_index ].size()==1 ){    //FIXME

-      //  //unique variable(s), defer calculation

-      //  unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );

-      //  int newChildIndex = (childIndex+1)%(int)d_children.size();

-      //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,

-      //                            0, newChildIndex, endChildIndex, modEq );

-      //}else{

-        //shared and non-set variable, add to InstMatch

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

-          InstMatch mn( &m );

-          mn.set( curr_ic, it->first);

-          processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,

-                                    trieIndex+1, childIndex, endChildIndex, modEq );

-        }

-      //}

-    }else{

-      //shared and set variable, try to merge

-      Node n = m.get( curr_ic );

-      std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );

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

-        processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,

-                                  trieIndex+1, childIndex, endChildIndex, modEq );

-      }

-      if( modEq ){

-        //check modulo equality for other possible instantiations

-        if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){

-          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),

-                                   qe->getEqualityQuery()->getEngine() );

-          while( !eqc.isFinished() ){

-            Node en = (*eqc);

-            if( en!=n ){

-              std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );

-              if( itc!=tr->d_data.end() ){

-                processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,

-                                          trieIndex+1, childIndex, endChildIndex, modEq );

-              }

-            }

-            ++eqc;

-          }

-        }

-      }

-    }

-  }else{

-    int newChildIndex = (childIndex+1)%(int)d_children.size();

-    processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,

-                              0, newChildIndex, endChildIndex, modEq );

-  }

-}

-

-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,

-                                                         std::vector< IndexedTrie >& unique_var_tries,

-                                                         int uvtIndex, InstMatchTrie* tr, int trieIndex ){

-  if( uvtIndex<(int)unique_var_tries.size() ){

-    int childIndex = unique_var_tries[uvtIndex].first.first;

-    if( !tr ){

-      tr = unique_var_tries[uvtIndex].second;

-      trieIndex = unique_var_tries[uvtIndex].first.second;

-    }

-    if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){

-      int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];

-      Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );

-      //unique non-set variable, add to InstMatch

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

-        InstMatch mn( &m );

-        mn.set( curr_ic, it->first);

-        processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );

-      }

-    }else{

-      processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );

-    }

-  }else{

-    //m is an instantiation

-    if( qe->addInstantiation( d_f, m ) ){

-      addedLemmas++;

-      Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;

-    }

-  }

-}

-

-int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){

-  Assert( options::eagerInstQuant() );

-  int addedLemmas = 0;

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

-    if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){

-      InstMatch m;

-      //if it produces a match, then process it with the rest

-      if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){

-        processNewMatch( qe, m, i, addedLemmas );

-      }

-    }

-  }

-  return addedLemmas;

-}

-

-int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){

-  InstMatch m;

-  m.add( baseMatch );

-  int addedLemmas = 0;

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

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

-      addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );

-    }

-  }else{

-    addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );

-  }

-  return addedLemmas;

-}

-

-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){

-  if( argIndex==(int)d_match_pattern.getNumChildren() ){

-    //m is an instantiation

-    if( qe->addInstantiation( d_f, m ) ){

-      addedLemmas++;

-      Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;

-    }

-  }else{

-    if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){

-      Node ic = d_match_pattern[argIndex];

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

-        Node t = it->first;

-        if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){

-          Node prev = m.get( ic );

-          m.set( ic, t);

-          addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );

-          m.set( ic, prev);

-        }

-      }

-    }else{

-      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );

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

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

-        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );

-      }

-    }

-  }

-}

-

-int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){

-  Assert( options::eagerInstQuant() );

-  InstMatch m;

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

-    if( d_match_pattern[i].getKind()==INST_CONSTANT ){

-      m.set(d_match_pattern[i], t[i]);

-    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){

-      return 0;

-    }

-  }

-  return qe->addInstantiation( f, m ) ? 1 : 0;

-}

-

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

-}/* CVC4::theory namespace */

-}/* CVC4 namespace */

+/*********************                                                        */
+/*! \file inst_match_generator.cpp
+** \verbatim
+** Original author: ajreynol
+** Major contributors: bobot
+** Minor contributors (to current version): barrett, mdeters
+** This file is part of the CVC4 prototype.
+** Copyright (c) 2009-2012  New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief Implementation of inst match generator class
+**/
+
+#include "theory/quantifiers/inst_match_generator.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+
+InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
+  initializePattern( pat, qe );
+}
+
+InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
+  if( pats.size()==1 ){
+    initializePattern( pats[0], qe );
+  }else{
+    initializePatterns( pats, qe );
+  }
+}
+
+void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
+  int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
+  for( int i=0; i<(int)pats.size(); i++ ){
+    d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );
+  }
+  d_pattern = Node::null();
+  d_match_pattern = Node::null();
+  d_cg = NULL;
+}
+
+void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
+  Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
+  Assert( pat.hasAttribute(InstConstantAttribute()) );
+  d_pattern = pat;
+  d_match_pattern = pat;
+  if( d_match_pattern.getKind()==NOT ){
+    //we want to add the children of the NOT
+    d_match_pattern = d_pattern[0];
+  }
+  if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
+    if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
+      Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
+      //swap sides
+      d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
+      d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
+      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
+        d_match_pattern = d_match_pattern[1];
+      }else{
+        d_match_pattern = d_pattern[0][0];
+      }
+    }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
+      Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
+      if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
+        d_match_pattern = d_match_pattern[0];
+      }
+    }
+  }
+  int childMatchPolicy = MATCH_GEN_DEFAULT;
+  for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
+    if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+      if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
+        d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );
+        d_children_index.push_back( i );
+      }
+    }
+  }
+
+  Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
+
+  //create candidate generator
+  if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
+    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
+    //we will be producing candidates via literal matching heuristics
+    if( d_pattern.getKind()!=NOT ){
+      //candidates will be all equalities
+      d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
+    }else{
+      //candidates will be all disequalities
+      d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
+    }
+  }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
+    Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
+    if( d_pattern.getKind()==NOT ){
+      Unimplemented("Disequal generator unimplemented");
+    }else{
+      Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
+      //we are matching only in a particular equivalence class
+      d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+      //store the equivalence class that we will call d_cg->reset( ... ) on
+      d_eq_class = d_pattern[1];
+    }
+  }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+    //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
+      //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
+    //}
+    //we will be scanning lists trying to find d_match_pattern.getOperator()
+    d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+  }else{
+    d_cg = new CandidateGeneratorQueue;
+    if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
+      Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+      //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+      d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
+    }else{
+      Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;
+      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
+        Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
+      }
+      //we will treat this as match gen internal arithmetic
+      d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;
+    }
+  }
+}
+
+/** get match (not modulo equality) */
+bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
+  Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
+                    << m.size() << ")" << ", " << d_children.size() << std::endl;
+  Assert( !d_match_pattern.isNull() );
+  if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
+    return true;
+  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
+    return getMatchArithmetic( t, m, qe );
+  }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
+    return false;
+  }else{
+    EqualityQuery* q = qe->getEqualityQuery();
+    //add m to partial match vector
+    std::vector< InstMatch > partial;
+    partial.push_back( InstMatch( &m ) );
+    //if t is null
+    Assert( !t.isNull() );
+    Assert( !t.hasAttribute(InstConstantAttribute()) );
+    Assert( t.getKind()==d_match_pattern.getKind() );
+    Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
+    //first, check if ground arguments are not equal, or a match is in conflict
+    for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
+      if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
+        if( d_match_pattern[i].getKind()==INST_CONSTANT ){
+          if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){
+            //match is in conflict
+            Debug("matching-debug") << "Match in conflict " << t[i] << " and "
+                                    << d_match_pattern[i] << " because "
+                                    << partial[0].get(d_match_pattern[i])
+                                    << std::endl;
+            Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;
+            return false;
+          }
+        }
+      }else{
+        if( !q->areEqual( d_match_pattern[i], t[i] ) ){
+          Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
+          //ground arguments are not equal
+          return false;
+        }
+      }
+    }
+    //now, fit children into match
+    //we will be requesting candidates for matching terms for each child
+    std::vector< Node > reps;
+    for( int i=0; i<(int)d_children.size(); i++ ){
+      Node rep = q->getRepresentative( t[ d_children_index[i] ] );
+      reps.push_back( rep );
+      d_children[i]->d_cg->reset( rep );
+    }
+
+    //combine child matches
+    int index = 0;
+    while( index>=0 && index<(int)d_children.size() ){
+      partial.push_back( InstMatch( &partial[index] ) );
+      if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
+        index++;
+      }else{
+        d_children[index]->d_cg->reset( reps[index] );
+        partial.pop_back();
+        if( !partial.empty() ){
+          partial.pop_back();
+        }
+        index--;
+      }
+    }
+    if( index>=0 ){
+      m = partial.back();
+      return true;
+    }else{
+      return false;
+    }
+  }
+}
+
+bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
+  bool success = false;
+  Node t;
+  do{
+    //get the next candidate term t
+    t = d_cg->getNextCandidate();
+    //if t not null, try to fit it into match m
+    if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
+      success = getMatch( t, m, qe );
+    }
+  }while( !success && !t.isNull() );
+  if (saveMatched) m.d_matched = t;
+  return success;
+}
+
+bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){
+  Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;
+  if( !d_arith_coeffs.empty() ){
+    NodeBuilder<> tb(kind::PLUS);
+    Node ic = Node::null();
+    for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
+      Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
+      if( !it->first.isNull() ){
+        if( m.find( it->first )==m.end() ){
+          //see if we can choose this to set
+          if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
+            ic = it->first;
+          }
+        }else{
+          Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
+          Node tm = m.get( it->first );
+          if( !it->second.isNull() ){
+            tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
+          }
+          tb << tm;
+        }
+      }else{
+        tb << it->second;
+      }
+    }
+    if( !ic.isNull() ){
+      Node tm;
+      if( tb.getNumChildren()==0 ){
+        tm = t;
+      }else{
+        tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
+        tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
+      }
+      if( !d_arith_coeffs[ ic ].isNull() ){
+        Assert( !ic.getType().isInteger() );
+        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
+        tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
+      }
+      m.set( ic, Rewriter::rewrite( tm ));
+      //set the rest to zeros
+      for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
+        if( !it->first.isNull() ){
+          if( m.find( it->first )==m.end() ){
+            m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );
+          }
+        }
+      }
+      Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    return false;
+  }
+}
+
+
+/** reset instantiation round */
+void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
+  if( d_match_pattern.isNull() ){
+    for( int i=0; i<(int)d_children.size(); i++ ){
+      d_children[i]->resetInstantiationRound( qe );
+    }
+  }else{
+    if( d_cg ){
+      d_cg->resetInstantiationRound();
+    }
+  }
+}
+
+void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+  if( d_match_pattern.isNull() ){
+    for( int i=0; i<(int)d_children.size(); i++ ){
+      d_children[i]->reset( eqc, qe );
+    }
+    d_partial.clear();
+  }else{
+    if( !d_eq_class.isNull() ){
+      //we have a specific equivalence class in mind
+      //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
+      //just look in equivalence class of the RHS
+      d_cg->reset( d_eq_class );
+    }else{
+      d_cg->reset( eqc );
+    }
+  }
+}
+
+bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
+  m.d_matched = Node::null();
+  if( d_match_pattern.isNull() ){
+    int index = (int)d_partial.size();
+    while( index>=0 && index<(int)d_children.size() ){
+      if( index>0 ){
+        d_partial.push_back( InstMatch( &d_partial[index-1] ) );
+      }else{
+        d_partial.push_back( InstMatch() );
+      }
+      if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
+        index++;
+      }else{
+        d_children[index]->reset( Node::null(), qe );
+        d_partial.pop_back();
+        if( !d_partial.empty() ){
+          d_partial.pop_back();
+        }
+        index--;
+      }
+    }
+    if( index>=0 ){
+      m = d_partial.back();
+      d_partial.pop_back();
+      return true;
+    }else{
+      return false;
+    }
+  }else{
+    bool res = getNextMatch2( m, qe, true );
+    Assert(!res || !m.d_matched.isNull());
+    return res;
+  }
+}
+
+
+
+int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+  //now, try to add instantiation for each match produced
+  int addedLemmas = 0;
+  InstMatch m;
+  while( getNextMatch( m, qe ) ){
+    //m.makeInternal( d_quantEngine->getEqualityQuery() );
+    m.add( baseMatch );
+    if( qe->addInstantiation( f, m ) ){
+      addedLemmas++;
+      if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
+        return addedLemmas;
+      }
+    }
+    m.clear();
+  }
+  //return number of lemmas added
+  return addedLemmas;
+}
+
+int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+  Assert( options::eagerInstQuant() );
+  if( !d_match_pattern.isNull() ){
+    InstMatch m;
+    if( getMatch( t, m, qe ) ){
+      if( qe->addInstantiation( f, m ) ){
+        return 1;
+      }
+    }
+  }else{
+    for( int i=0; i<(int)d_children.size(); i++ ){
+      d_children[i]->addTerm( f, t, qe );
+    }
+  }
+  return 0;
+}
+
+/** constructors */
+InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
+d_f( f ){
+  Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
+  std::map< Node, std::vector< Node > > var_contains;
+  qe->getTermDatabase()->getVarContains( f, pats, var_contains );
+  //convert to indicies
+  for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
+    Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
+    for( int i=0; i<(int)it->second.size(); i++ ){
+      Debug("smart-multi-trigger") << it->second[i] << " ";
+      int index = it->second[i].getAttribute(InstVarNumAttribute());
+      d_var_contains[ it->first ].push_back( index );
+      d_var_to_node[ index ].push_back( it->first );
+    }
+    Debug("smart-multi-trigger") << std::endl;
+  }
+  for( int i=0; i<(int)pats.size(); i++ ){
+    Node n = pats[i];
+    //make the match generator
+    d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );
+    //compute unique/shared variables
+    std::vector< int > unique_vars;
+    std::map< int, bool > shared_vars;
+    int numSharedVars = 0;
+    for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
+      if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
+        Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
+        unique_vars.push_back( d_var_contains[n][j] );
+      }else{
+        shared_vars[ d_var_contains[n][j] ] = true;
+        numSharedVars++;
+      }
+    }
+    //we use the latest shared variables, then unique variables
+    std::vector< int > vars;
+    int index = i==0 ? (int)(pats.size()-1) : (i-1);
+    while( numSharedVars>0 && index!=i ){
+      for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
+        if( it->second ){
+          if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
+              d_var_contains[ pats[index] ].end() ){
+            vars.push_back( it->first );
+            shared_vars[ it->first ] = false;
+            numSharedVars--;
+          }
+        }
+      }
+      index = index==0 ? (int)(pats.size()-1) : (index-1);
+    }
+    vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
+    Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
+    for( int i=0; i<(int)vars.size(); i++ ){
+      Debug("smart-multi-trigger") << vars[i] << " ";
+    }
+    Debug("smart-multi-trigger") << std::endl;
+    //make ordered inst match trie
+    InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
+    imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
+    d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
+  }
+
+}
+
+/** reset instantiation round (call this whenever equivalence classes have changed) */
+void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
+  for( int i=0; i<(int)d_children.size(); i++ ){
+    d_children[i]->resetInstantiationRound( qe );
+  }
+}
+
+/** reset, eqc is the equivalence class to search in (any if eqc=null) */
+void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
+  for( int i=0; i<(int)d_children.size(); i++ ){
+    d_children[i]->reset( eqc, qe );
+  }
+}
+
+int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+  int addedLemmas = 0;
+  Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
+  for( int i=0; i<(int)d_children.size(); i++ ){
+    Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
+    std::vector< InstMatch > newMatches;
+    InstMatch m;
+    while( d_children[i]->getNextMatch( m, qe ) ){
+      m.makeRepresentative( qe );
+      newMatches.push_back( InstMatch( &m ) );
+      m.clear();
+    }
+    for( int j=0; j<(int)newMatches.size(); j++ ){
+      processNewMatch( qe, newMatches[j], i, addedLemmas );
+    }
+  }
+  return addedLemmas;
+}
+
+void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
+  //see if these produce new matches
+  d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
+  //possibly only do the following if we know that new matches will be produced?
+  //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
+  // we can safely skip the following lines, even when we have already produced this match.
+  Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
+  //process new instantiations
+  int childIndex = (fromChildIndex+1)%(int)d_children.size();
+  std::vector< IndexedTrie > unique_var_tries;
+  processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
+                            unique_var_tries, 0, childIndex, fromChildIndex, true );
+}
+
+void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
+                                                        std::vector< IndexedTrie >& unique_var_tries,
+                                                        int trieIndex, int childIndex, int endChildIndex, bool modEq ){
+  if( childIndex==endChildIndex ){
+    //now, process unique variables
+    processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
+  }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
+    int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
+    Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+    if( m.find( curr_ic )==m.end() ){
+      //if( d_var_to_node[ curr_index ].size()==1 ){    //FIXME
+      //  //unique variable(s), defer calculation
+      //  unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
+      //  int newChildIndex = (childIndex+1)%(int)d_children.size();
+      //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
+      //                            0, newChildIndex, endChildIndex, modEq );
+      //}else{
+        //shared and non-set variable, add to InstMatch
+        for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
+          InstMatch mn( &m );
+          mn.set( curr_ic, it->first);
+          processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
+                                    trieIndex+1, childIndex, endChildIndex, modEq );
+        }
+      //}
+    }else{
+      //shared and set variable, try to merge
+      Node n = m.get( curr_ic );
+      std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
+      if( it!=tr->d_data.end() ){
+        processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
+                                  trieIndex+1, childIndex, endChildIndex, modEq );
+      }
+      if( modEq ){
+        //check modulo equality for other possible instantiations
+        if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+          eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                   qe->getEqualityQuery()->getEngine() );
+          while( !eqc.isFinished() ){
+            Node en = (*eqc);
+            if( en!=n ){
+              std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
+              if( itc!=tr->d_data.end() ){
+                processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
+                                          trieIndex+1, childIndex, endChildIndex, modEq );
+              }
+            }
+            ++eqc;
+          }
+        }
+      }
+    }
+  }else{
+    int newChildIndex = (childIndex+1)%(int)d_children.size();
+    processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
+                              0, newChildIndex, endChildIndex, modEq );
+  }
+}
+
+void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
+                                                         std::vector< IndexedTrie >& unique_var_tries,
+                                                         int uvtIndex, InstMatchTrie* tr, int trieIndex ){
+  if( uvtIndex<(int)unique_var_tries.size() ){
+    int childIndex = unique_var_tries[uvtIndex].first.first;
+    if( !tr ){
+      tr = unique_var_tries[uvtIndex].second;
+      trieIndex = unique_var_tries[uvtIndex].first.second;
+    }
+    if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
+      int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
+      Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
+      //unique non-set variable, add to InstMatch
+      for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
+        InstMatch mn( &m );
+        mn.set( curr_ic, it->first);
+        processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
+      }
+    }else{
+      processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
+    }
+  }else{
+    //m is an instantiation
+    if( qe->addInstantiation( d_f, m ) ){
+      addedLemmas++;
+      Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
+    }
+  }
+}
+
+int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+  Assert( options::eagerInstQuant() );
+  int addedLemmas = 0;
+  for( int i=0; i<(int)d_children.size(); i++ ){
+    if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
+      InstMatch m;
+      //if it produces a match, then process it with the rest
+      if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
+        processNewMatch( qe, m, i, addedLemmas );
+      }
+    }
+  }
+  return addedLemmas;
+}
+
+int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+  InstMatch m;
+  m.add( baseMatch );
+  int addedLemmas = 0;
+  if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
+    for( int i=0; i<2; i++ ){
+      addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
+    }
+  }else{
+    addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
+  }
+  return addedLemmas;
+}
+
+void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
+  if( argIndex==(int)d_match_pattern.getNumChildren() ){
+    //m is an instantiation
+    if( qe->addInstantiation( d_f, m ) ){
+      addedLemmas++;
+      Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
+    }
+  }else{
+    if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
+      Node ic = d_match_pattern[argIndex];
+      for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+        Node t = it->first;
+        if( ( m.get( ic ).isNull() || m.get( ic )==t ) && ic.getType()==t.getType() ){
+          Node prev = m.get( ic );
+          m.set( ic, t);
+          addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+          m.set( ic, prev);
+        }
+      }
+    }else{
+      Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
+      std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+      if( it!=tat->d_data.end() ){
+        addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+      }
+    }
+  }
+}
+
+int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
+  Assert( options::eagerInstQuant() );
+  InstMatch m;
+  for( int i=0; i<(int)t.getNumChildren(); i++ ){
+    if( d_match_pattern[i].getKind()==INST_CONSTANT ){
+      m.set(d_match_pattern[i], t[i]);
+    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
+      return 0;
+    }
+  }
+  return qe->addInstantiation( f, m ) ? 1 : 0;
+}
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index af65e809b..dd3663e0a 100755
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -1,192 +1,192 @@
-/*********************                                                        */

-/*! \file inst_match_generator.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: bobot

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief inst match generator class

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H

-#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H

-

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

-#include <map>

-

-namespace CVC4 {

-namespace theory {

-

-class QuantifiersEngine;

-namespace quantifiers{

-  class TermArgTrie;

-}

-

-namespace inst {

-

-/** base class for producing InstMatch objects */

-class IMGenerator {

-public:

-  /** reset instantiation round (call this at beginning of instantiation round) */

-  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;

-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */

-  virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;

-  /** get the next match.  must call reset( eqc ) before this function. */

-  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;

-  /** add instantiations directly */

-  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;

-  /** add ground term t, called when t is added to term db */

-  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;

-};/* class IMGenerator */

-

-class CandidateGenerator;

-

-class InstMatchGenerator : public IMGenerator {

-private:

-  /** candidate generator */

-  CandidateGenerator* d_cg;

-  /** policy to use for matching */

-  int d_matchPolicy;

-  /** children generators */

-  std::vector< InstMatchGenerator* > d_children;

-  std::vector< int > d_children_index;

-  /** partial vector */

-  std::vector< InstMatch > d_partial;

-  /** eq class */

-  Node d_eq_class;

-  /** for arithmetic matching */

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

-  /** initialize pattern */

-  void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );

-  void initializePattern( Node pat, QuantifiersEngine* qe );

-public:

-  enum {

-    //options for producing matches

-    MATCH_GEN_DEFAULT = 0,

-    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers

-    //others (internally used)

-    MATCH_GEN_INTERNAL_ARITHMETIC,

-    MATCH_GEN_INTERNAL_ERROR,

-  };

-private:

-  /** get the next match.  must call d_cg->reset( ... ) before using.

-      only valid for use where !d_match_pattern.isNull().

-  */

-  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );

-  /** for arithmetic */

-  bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );

-public:

-  /** get the match against ground term or formula t.

-      d_match_pattern and t should have the same shape.

-      only valid for use where !d_match_pattern.isNull().

-  */

-  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );

-

-  /** constructors */

-  InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );

-  InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );

-  /** destructor */

-  ~InstMatchGenerator(){}

-  /** The pattern we are producing matches for.

-      If null, this is a multi trigger that is merging matches from d_children.

-  */

-  Node d_pattern;

-  /** match pattern */

-  Node d_match_pattern;

-public:

-  /** reset instantiation round (call this whenever equivalence classes have changed) */

-  void resetInstantiationRound( QuantifiersEngine* qe );

-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */

-  void reset( Node eqc, QuantifiersEngine* qe );

-  /** get the next match.  must call reset( eqc ) before this function. */

-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );

-  /** add instantiations */

-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

-  /** add ground term t */

-  int addTerm( Node f, Node t, QuantifiersEngine* qe );

-};/* class InstMatchGenerator */

-

-/** smart multi-trigger implementation */

-class InstMatchGeneratorMulti : public IMGenerator {

-private:

-  /** indexed trie */

-  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;

-  /** process new match */

-  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );

-  /** process new instantiations */

-  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,

-                                 std::vector< IndexedTrie >& unique_var_tries,

-                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );

-  /** process new instantiations 2 */

-  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,

-                                  std::vector< IndexedTrie >& unique_var_tries,

-                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );

-private:

-  /** var contains (variable indices) for each pattern node */

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

-  /** variable indices contained to pattern nodes */

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

-  /** quantifier to use */

-  Node d_f;

-  /** policy to use for matching */

-  int d_matchPolicy;

-  /** children generators */

-  std::vector< InstMatchGenerator* > d_children;

-  /** inst match tries for each child */

-  std::vector< InstMatchTrieOrdered > d_children_trie;

-  /** calculate matches */

-  void calculateMatches( QuantifiersEngine* qe );

-public:

-  /** constructors */

-  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );

-  /** destructor */

-  ~InstMatchGeneratorMulti(){}

-  /** reset instantiation round (call this whenever equivalence classes have changed) */

-  void resetInstantiationRound( QuantifiersEngine* qe );

-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */

-  void reset( Node eqc, QuantifiersEngine* qe );

-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */

-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }

-  /** add instantiations */

-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

-  /** add ground term t */

-  int addTerm( Node f, Node t, QuantifiersEngine* qe );

-};/* class InstMatchGeneratorMulti */

-

-/** smart (single)-trigger implementation */

-class InstMatchGeneratorSimple : public IMGenerator {

-private:

-  /** quantifier for match term */

-  Node d_f;

-  /** match term */

-  Node d_match_pattern;

-  /** add instantiations */

-  void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );

-public:

-  /** constructors */

-  InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}

-  /** destructor */

-  ~InstMatchGeneratorSimple(){}

-  /** reset instantiation round (call this whenever equivalence classes have changed) */

-  void resetInstantiationRound( QuantifiersEngine* qe ) {}

-  /** reset, eqc is the equivalence class to search in (any if eqc=null) */

-  void reset( Node eqc, QuantifiersEngine* qe ) {}

-  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */

-  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }

-  /** add instantiations */

-  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );

-  /** add ground term t, possibly add instantiations */

-  int addTerm( Node f, Node t, QuantifiersEngine* qe );

-};/* class InstMatchGeneratorSimple */

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file inst_match_generator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief inst match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+
+#include "theory/quantifiers/inst_match.h"
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+namespace quantifiers{
+  class TermArgTrie;
+}
+
+namespace inst {
+
+/** base class for producing InstMatch objects */
+class IMGenerator {
+public:
+  /** reset instantiation round (call this at beginning of instantiation round) */
+  virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
+  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+  virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
+  /** get the next match.  must call reset( eqc ) before this function. */
+  virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
+  /** add instantiations directly */
+  virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
+  /** add ground term t, called when t is added to term db */
+  virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
+};/* class IMGenerator */
+
+class CandidateGenerator;
+
+class InstMatchGenerator : public IMGenerator {
+private:
+  /** candidate generator */
+  CandidateGenerator* d_cg;
+  /** policy to use for matching */
+  int d_matchPolicy;
+  /** children generators */
+  std::vector< InstMatchGenerator* > d_children;
+  std::vector< int > d_children_index;
+  /** partial vector */
+  std::vector< InstMatch > d_partial;
+  /** eq class */
+  Node d_eq_class;
+  /** for arithmetic matching */
+  std::map< Node, Node > d_arith_coeffs;
+  /** initialize pattern */
+  void initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe );
+  void initializePattern( Node pat, QuantifiersEngine* qe );
+public:
+  enum {
+    //options for producing matches
+    MATCH_GEN_DEFAULT = 0,
+    MATCH_GEN_EFFICIENT_E_MATCH,   //generate matches via Efficient E-matching for SMT solvers
+    //others (internally used)
+    MATCH_GEN_INTERNAL_ARITHMETIC,
+    MATCH_GEN_INTERNAL_ERROR,
+  };
+private:
+  /** get the next match.  must call d_cg->reset( ... ) before using.
+      only valid for use where !d_match_pattern.isNull().
+  */
+  bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );
+  /** for arithmetic */
+  bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
+public:
+  /** get the match against ground term or formula t.
+      d_match_pattern and t should have the same shape.
+      only valid for use where !d_match_pattern.isNull().
+  */
+  bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
+
+  /** constructors */
+  InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );
+  InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
+  /** destructor */
+  ~InstMatchGenerator(){}
+  /** The pattern we are producing matches for.
+      If null, this is a multi trigger that is merging matches from d_children.
+  */
+  Node d_pattern;
+  /** match pattern */
+  Node d_match_pattern;
+public:
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  void resetInstantiationRound( QuantifiersEngine* qe );
+  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+  void reset( Node eqc, QuantifiersEngine* qe );
+  /** get the next match.  must call reset( eqc ) before this function. */
+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
+  /** add instantiations */
+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  /** add ground term t */
+  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+};/* class InstMatchGenerator */
+
+/** smart multi-trigger implementation */
+class InstMatchGeneratorMulti : public IMGenerator {
+private:
+  /** indexed trie */
+  typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
+  /** process new match */
+  void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
+  /** process new instantiations */
+  void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
+                                 std::vector< IndexedTrie >& unique_var_tries,
+                                 int trieIndex, int childIndex, int endChildIndex, bool modEq );
+  /** process new instantiations 2 */
+  void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
+                                  std::vector< IndexedTrie >& unique_var_tries,
+                                  int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
+private:
+  /** var contains (variable indices) for each pattern node */
+  std::map< Node, std::vector< int > > d_var_contains;
+  /** variable indices contained to pattern nodes */
+  std::map< int, std::vector< Node > > d_var_to_node;
+  /** quantifier to use */
+  Node d_f;
+  /** policy to use for matching */
+  int d_matchPolicy;
+  /** children generators */
+  std::vector< InstMatchGenerator* > d_children;
+  /** inst match tries for each child */
+  std::vector< InstMatchTrieOrdered > d_children_trie;
+  /** calculate matches */
+  void calculateMatches( QuantifiersEngine* qe );
+public:
+  /** constructors */
+  InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption = 0 );
+  /** destructor */
+  ~InstMatchGeneratorMulti(){}
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  void resetInstantiationRound( QuantifiersEngine* qe );
+  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+  void reset( Node eqc, QuantifiersEngine* qe );
+  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  /** add instantiations */
+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  /** add ground term t */
+  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+};/* class InstMatchGeneratorMulti */
+
+/** smart (single)-trigger implementation */
+class InstMatchGeneratorSimple : public IMGenerator {
+private:
+  /** quantifier for match term */
+  Node d_f;
+  /** match term */
+  Node d_match_pattern;
+  /** add instantiations */
+  void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
+public:
+  /** constructors */
+  InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f ), d_match_pattern( pat ){}
+  /** destructor */
+  ~InstMatchGeneratorSimple(){}
+  /** reset instantiation round (call this whenever equivalence classes have changed) */
+  void resetInstantiationRound( QuantifiersEngine* qe ) {}
+  /** reset, eqc is the equivalence class to search in (any if eqc=null) */
+  void reset( Node eqc, QuantifiersEngine* qe ) {}
+  /** get the next match.  must call reset( eqc ) before this function. (not implemented) */
+  bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
+  /** add instantiations */
+  int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );
+  /** add ground term t, possibly add instantiations */
+  int addTerm( Node f, Node t, QuantifiersEngine* qe );
+};/* class InstMatchGeneratorSimple */
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d79ddee31..aba311500 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -1,403 +1,403 @@
-/*********************                                                        */

-/*! \file inst_strategy_cbqi.cpp

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: none

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Implementation of cbqi instantiation strategies

- **/

-

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

-#include "theory/arith/theory_arith.h"

-#include "theory/theory_engine.h"

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

-using namespace CVC4::theory::arith;

-using namespace CVC4::theory::datatypes;

-

-#define ARITH_INSTANTIATOR_USE_MINUS_DELTA

-

-InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :

-    InstStrategy( ie ), d_th( th ), d_counter( 0 ){

-  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );

-}

-

-bool InstStrategySimplex::calculateShouldProcess( Node f ){

-  //DO_THIS

-  return false;

-}

-

-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){

-  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;

-  d_instRows.clear();

-  d_tableaux_term.clear();

-  d_tableaux.clear();

-  d_ceTableaux.clear();

-  //search for instantiation rows in simplex tableaux

-  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

-    ArithVar x = (*it).first;

-    if( d_th->d_partialModel.hasEitherBound( x ) ){

-      Node n = (*it).second;

-      Node f;

-      NodeBuilder<> t(kind::PLUS);

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

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

-          addTermToRow( x, n[i], f, t );

-        }

-      }else{

-        addTermToRow( x, n, f, t );

-      }

-      if( f!=Node::null() ){

-        d_instRows[f].push_back( x );

-        //this theory has constraints from f

-        Debug("quant-arith") << "Has constraints from " << f << std::endl;

-        //set that we should process it

-        d_quantActive[ f ] = true;

-        //set tableaux term

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

-          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );

-        }else if( t.getNumChildren()==1 ){

-          d_tableaux_term[x] = t.getChild( 0 );

-        }else{

-          d_tableaux_term[x] = t;

-        }

-      }

-    }

-  }

-  //print debug

-  debugPrint( "quant-arith-debug" );

-  d_counter++;

-}

-

-int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){

-  if( e<2 ){

-    return STATUS_UNFINISHED;

-  }else if( e==2 ){

-    //Notice() << f << std::endl;

-    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;

-    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;

-    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;

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

-      ArithVar x = d_instRows[f][j];

-      if( !d_ceTableaux[x].empty() ){

-        Debug("quant-arith-simplex") << "Check row " << x << std::endl;

-        //instantiation row will be A*e + B*t = beta,

-        // where e is a vector of terms , and t is vector of ground terms.

-        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant

-        // We will construct the term ( beta - B*t)/coeff to use for e_i.

-        InstMatch m;

-        //By default, choose the first instantiation constant to be e_i.

-        Node var = d_ceTableaux[x].begin()->first;

-        if( var.getType().isInteger() ){

-          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();

-          //try to find coefficent that is +/- 1

-          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){

-            ++it;

-            if( it==d_ceTableaux[x].end() ){

-              var = Node::null();

-            }else{

-              var = it->first;

-            }

-          }

-          //otherwise, try one that divides all ground term coefficients? DO_THIS

-        }

-        if( !var.isNull() ){

-          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;

-          doInstantiation( f, d_tableaux_term[x], x, m, var );

-        }else{

-          Debug("quant-arith-simplex") << "Could not find var." << std::endl;

-        }

-        ////choose a new variable based on alternation strategy

-        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();

-        //Node var;

-        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){

-        //  if( index==0 ){

-        //    var = it->first;

-        //    break;

-        //  }

-        //  index--;

-        //}

-        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );

-      }

-    }

-  }

-  return STATUS_UNKNOWN;

-}

-

-

-void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){

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

-    if( n[1].hasAttribute(InstConstantAttribute()) ){

-      f = n[1].getAttribute(InstConstantAttribute());

-      if( n[1].getKind()==INST_CONSTANT ){

-        d_ceTableaux[x][ n[1] ] = n[0];

-      }else{

-        d_tableaux_ce_term[x][ n[1] ] = n[0];

-      }

-    }else{

-      d_tableaux[x][ n[1] ] = n[0];

-      t << n;

-    }

-  }else{

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

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

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

-        d_ceTableaux[x][ n ] = Node::null();

-      }else{

-        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

-      }

-    }else{

-      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );

-      t << n;

-    }

-  }

-}

-

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

-  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();

-  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){

-    ArithVar x = (*it).first;

-    Node n = (*it).second;

-    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){

-      Debug(c) << x << " : " << n << ", bounds = ";

-      if( d_th->d_partialModel.hasLowerBound( x ) ){

-        Debug(c) << d_th->d_partialModel.getLowerBound( x );

-      }else{

-        Debug(c) << "-infty";

-      }

-      Debug(c) << " <= ";

-      Debug(c) << d_th->d_partialModel.getAssignment( x );

-      Debug(c) << " <= ";

-      if( d_th->d_partialModel.hasUpperBound( x ) ){

-        Debug(c) << d_th->d_partialModel.getUpperBound( x );

-      }else{

-        Debug(c) << "+infty";

-      }

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

-      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;

-      //Debug(c) << "   ";

-      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){

-      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";

-      //}

-      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){

-      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";

-      //}

-      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){

-      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";

-      //}

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

-    //}

-  }

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

-

-  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){

-    Node f = d_quantEngine->getQuantifier( q );

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

-    Debug(c) << "   Inst constants: ";

-    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){

-      if( i>0 ){

-        Debug( c ) << ", ";

-      }

-      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );

-    }

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

-    Debug(c) << "   Instantiation rows: ";

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

-      if( i>0 ){

-        Debug(c) << ", ";

-      }

-      Debug(c) << d_instRows[f][i];

-    }

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

-  }

-}

-

-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,

-// where var is an instantiation constant from f,

-// t[e] is a vector of terms containing instantiation constants from f,

-// and term is a ground term (c1*t1 + ... + cn*tn).

-// We construct the term ( beta - term )/coeff to use as an instantiation for var.

-bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){

-  //first try +delta

-  if( doInstantiation2( f, term, x, m, var ) ){

-    ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);

-    return true;

-  }else{

-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA

-    //otherwise try -delta

-    if( doInstantiation2( f, term, x, m, var, true ) ){

-      ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);

-      return true;

-    }else{

-      return false;

-    }

-#else

-    return false;

-#endif

-  }

-}

-

-bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){

-  // make term ( beta - term )/coeff

-  Node beta = getTableauxValue( x, minus_delta );

-  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );

-  if( !d_ceTableaux[x][var].isNull() ){

-    if( var.getType().isInteger() ){

-      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );

-      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );

-    }else{

-      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );

-      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );

-    }

-  }

-  instVal = Rewriter::rewrite( instVal );

-  //use as instantiation value for var

-  m.set(var, instVal);

-  Debug("quant-arith") << "Add instantiation " << m << std::endl;

-  return d_quantEngine->addInstantiation( f, m );

-}

-

-Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){

-  if( d_th->d_arithvarNodeMap.hasArithVar(n) ){

-    ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );

-    return getTableauxValue( v, minus_delta );

-  }else{

-    return NodeManager::currentNM()->mkConst( Rational(0) );

-  }

-}

-

-Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){

-  const Rational& delta = d_th->d_partialModel.getDelta();

-  DeltaRational drv = d_th->d_partialModel.getAssignment( v );

-  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );

-  return mkRationalNode(qmodel);

-}

-

-

-InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :

-  InstStrategy( qe ), d_th( th ){

-

-}

-

-bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){

-  //DO_THIS

-  return false;

-}

-

-void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){

-

-}

-

-int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){

-  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;

-  if( e<2 ){

-    return InstStrategy::STATUS_UNFINISHED;

-  }else if( e==2 ){

-    InstMatch m;

-    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){

-      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );

-      if( i.getType().isDatatype() ){

-        Node n = getValueFor( i );

-        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;

-        m.set(i,n);

-      }

-    }

-    //d_quantEngine->addInstantiation( f, m );

-  }

-  return InstStrategy::STATUS_UNKNOWN;

-}

-

-Node InstStrategyDatatypesValue::getValueFor( Node n ){

-  //simply get the ground value for n in the current model, if it exists,

-  //  or return an arbitrary ground term otherwise

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

-    return n;

-  }else{

-    return n;

-  }

-  /*  FIXME

-

-  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;

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

-    return n;

-  }else{

-    Assert( n.getType().isDatatype() );

-    //check if in equivalence class with ground term

-    Node rep = getRepresentative( n );

-    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;

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

-      return rep;

-    }else{

-      if( !n.getType().isDatatype() ){

-        return n.getType().mkGroundTerm();

-      }else{

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

-          std::vector< Node > children;

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

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

-            children.push_back( getValueFor( n[i] ) );

-          }

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

-        }else{

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

-          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;

-          //otherwise, use which constructor the inst constant is current chosen to be

-          if( labels->find( n )!=labels->end() ){

-            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;

-            int tIndex = -1;

-            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){

-              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;

-              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());

-            }else{

-              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;

-              //must find a possible choice

-              vector< bool > possibleCons;

-              possibleCons.resize( dt.getNumConstructors(), true );

-              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {

-                Node leqn = (*j);

-                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;

-              }

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

-                if( possibleCons[j] ){

-                  tIndex = j;

-                  break;

-                }

-              }

-            }

-            Assert( tIndex!=-1 );

-            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );

-            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;

-            std::vector< Node > children;

-            children.push_back( cons );

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

-              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );

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

-                InstConstantAttribute ica;

-                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );

-              }

-              Node snn = getValueFor( sn );

-              children.push_back( snn );

-            }

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

-          }else{

-            return n.getType().mkGroundTerm();

-          }

-        }

-      }

-    }

-  }

-  */

-}

+/*********************                                                        */
+/*! \file inst_strategy_cbqi.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): bobot, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of cbqi instantiation strategies
+ **/
+
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/arith/theory_arith.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.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;
+using namespace CVC4::theory::arith;
+using namespace CVC4::theory::datatypes;
+
+#define ARITH_INSTANTIATOR_USE_MINUS_DELTA
+
+InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
+    InstStrategy( ie ), d_th( th ), d_counter( 0 ){
+  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
+}
+
+bool InstStrategySimplex::calculateShouldProcess( Node f ){
+  //DO_THIS
+  return false;
+}
+
+void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
+  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+  d_instRows.clear();
+  d_tableaux_term.clear();
+  d_tableaux.clear();
+  d_ceTableaux.clear();
+  //search for instantiation rows in simplex tableaux
+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+    ArithVar x = (*it).first;
+    if( d_th->d_partialModel.hasEitherBound( x ) ){
+      Node n = (*it).second;
+      Node f;
+      NodeBuilder<> t(kind::PLUS);
+      if( n.getKind()==PLUS ){
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          addTermToRow( x, n[i], f, t );
+        }
+      }else{
+        addTermToRow( x, n, f, t );
+      }
+      if( f!=Node::null() ){
+        d_instRows[f].push_back( x );
+        //this theory has constraints from f
+        Debug("quant-arith") << "Has constraints from " << f << std::endl;
+        //set that we should process it
+        d_quantActive[ f ] = true;
+        //set tableaux term
+        if( t.getNumChildren()==0 ){
+          d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) );
+        }else if( t.getNumChildren()==1 ){
+          d_tableaux_term[x] = t.getChild( 0 );
+        }else{
+          d_tableaux_term[x] = t;
+        }
+      }
+    }
+  }
+  //print debug
+  debugPrint( "quant-arith-debug" );
+  d_counter++;
+}
+
+int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
+  if( e<2 ){
+    return STATUS_UNFINISHED;
+  }else if( e==2 ){
+    //Notice() << f << std::endl;
+    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
+    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
+    Debug("quant-arith-simplex") << "InstStrategySimplex check " << f << ", rows = " << d_instRows[f].size() << std::endl;
+    for( int j=0; j<(int)d_instRows[f].size(); j++ ){
+      ArithVar x = d_instRows[f][j];
+      if( !d_ceTableaux[x].empty() ){
+        Debug("quant-arith-simplex") << "Check row " << x << std::endl;
+        //instantiation row will be A*e + B*t = beta,
+        // where e is a vector of terms , and t is vector of ground terms.
+        // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+        // We will construct the term ( beta - B*t)/coeff to use for e_i.
+        InstMatch m;
+        //By default, choose the first instantiation constant to be e_i.
+        Node var = d_ceTableaux[x].begin()->first;
+        if( var.getType().isInteger() ){
+          std::map< Node, Node >::iterator it = d_ceTableaux[x].begin();
+          //try to find coefficent that is +/- 1
+          while( !var.isNull() && !d_ceTableaux[x][var].isNull() && d_ceTableaux[x][var]!=d_negOne ){
+            ++it;
+            if( it==d_ceTableaux[x].end() ){
+              var = Node::null();
+            }else{
+              var = it->first;
+            }
+          }
+          //otherwise, try one that divides all ground term coefficients? DO_THIS
+        }
+        if( !var.isNull() ){
+          Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+          doInstantiation( f, d_tableaux_term[x], x, m, var );
+        }else{
+          Debug("quant-arith-simplex") << "Could not find var." << std::endl;
+        }
+        ////choose a new variable based on alternation strategy
+        //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
+        //Node var;
+        //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
+        //  if( index==0 ){
+        //    var = it->first;
+        //    break;
+        //  }
+        //  index--;
+        //}
+        //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
+      }
+    }
+  }
+  return STATUS_UNKNOWN;
+}
+
+
+void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& t ){
+  if( n.getKind()==MULT ){
+    if( n[1].hasAttribute(InstConstantAttribute()) ){
+      f = n[1].getAttribute(InstConstantAttribute());
+      if( n[1].getKind()==INST_CONSTANT ){
+        d_ceTableaux[x][ n[1] ] = n[0];
+      }else{
+        d_tableaux_ce_term[x][ n[1] ] = n[0];
+      }
+    }else{
+      d_tableaux[x][ n[1] ] = n[0];
+      t << n;
+    }
+  }else{
+    if( n.hasAttribute(InstConstantAttribute()) ){
+      f = n.getAttribute(InstConstantAttribute());
+      if( n.getKind()==INST_CONSTANT ){
+        d_ceTableaux[x][ n ] = Node::null();
+      }else{
+        d_tableaux_ce_term[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+      }
+    }else{
+      d_tableaux[x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
+      t << n;
+    }
+  }
+}
+
+void InstStrategySimplex::debugPrint( const char* c ){
+  ArithVarToNodeMap avtnm = d_th->d_arithvarNodeMap.getArithVarToNodeMap();
+  for( ArithVarToNodeMap::iterator it = avtnm.begin(); it != avtnm.end(); ++it ){
+    ArithVar x = (*it).first;
+    Node n = (*it).second;
+    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
+      Debug(c) << x << " : " << n << ", bounds = ";
+      if( d_th->d_partialModel.hasLowerBound( x ) ){
+        Debug(c) << d_th->d_partialModel.getLowerBound( x );
+      }else{
+        Debug(c) << "-infty";
+      }
+      Debug(c) << " <= ";
+      Debug(c) << d_th->d_partialModel.getAssignment( x );
+      Debug(c) << " <= ";
+      if( d_th->d_partialModel.hasUpperBound( x ) ){
+        Debug(c) << d_th->d_partialModel.getUpperBound( x );
+      }else{
+        Debug(c) << "+infty";
+      }
+      Debug(c) << std::endl;
+      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
+      //Debug(c) << "   ";
+      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
+      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
+      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
+      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
+      //}
+      //Debug(c) << std::endl;
+    //}
+  }
+  Debug(c) << std::endl;
+
+  for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){
+    Node f = d_quantEngine->getQuantifier( q );
+    Debug(c) << f << std::endl;
+    Debug(c) << "   Inst constants: ";
+    for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+      if( i>0 ){
+        Debug( c ) << ", ";
+      }
+      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+    }
+    Debug(c) << std::endl;
+    Debug(c) << "   Instantiation rows: ";
+    for( int i=0; i<(int)d_instRows[f].size(); i++ ){
+      if( i>0 ){
+        Debug(c) << ", ";
+      }
+      Debug(c) << d_instRows[f][i];
+    }
+    Debug(c) << std::endl;
+  }
+}
+
+//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
+// where var is an instantiation constant from f,
+// t[e] is a vector of terms containing instantiation constants from f,
+// and term is a ground term (c1*t1 + ... + cn*tn).
+// We construct the term ( beta - term )/coeff to use as an instantiation for var.
+bool InstStrategySimplex::doInstantiation( Node f, Node term, ArithVar x, InstMatch& m, Node var ){
+  //first try +delta
+  if( doInstantiation2( f, term, x, m, var ) ){
+    ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith);
+    return true;
+  }else{
+#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
+    //otherwise try -delta
+    if( doInstantiation2( f, term, x, m, var, true ) ){
+      ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_cbqi_arith_minus);
+      return true;
+    }else{
+      return false;
+    }
+#else
+    return false;
+#endif
+  }
+}
+
+bool InstStrategySimplex::doInstantiation2( Node f, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
+  // make term ( beta - term )/coeff
+  Node beta = getTableauxValue( x, minus_delta );
+  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
+  if( !d_ceTableaux[x][var].isNull() ){
+    if( var.getType().isInteger() ){
+      Assert( d_ceTableaux[x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
+      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[x][var], instVal );
+    }else{
+      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[x][var].getConst<Rational>() );
+      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+    }
+  }
+  instVal = Rewriter::rewrite( instVal );
+  //use as instantiation value for var
+  m.set(var, instVal);
+  Debug("quant-arith") << "Add instantiation " << m << std::endl;
+  return d_quantEngine->addInstantiation( f, m );
+}
+
+Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
+  if( d_th->d_arithvarNodeMap.hasArithVar(n) ){
+    ArithVar v = d_th->d_arithvarNodeMap.asArithVar( n );
+    return getTableauxValue( v, minus_delta );
+  }else{
+    return NodeManager::currentNM()->mkConst( Rational(0) );
+  }
+}
+
+Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
+  const Rational& delta = d_th->d_partialModel.getDelta();
+  DeltaRational drv = d_th->d_partialModel.getAssignment( v );
+  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
+  return mkRationalNode(qmodel);
+}
+
+
+InstStrategyDatatypesValue::InstStrategyDatatypesValue( TheoryDatatypes* th, QuantifiersEngine* qe ) :
+  InstStrategy( qe ), d_th( th ){
+
+}
+
+bool InstStrategyDatatypesValue::calculateShouldProcess( Node f ){
+  //DO_THIS
+  return false;
+}
+
+void InstStrategyDatatypesValue::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){
+  Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
+  if( e<2 ){
+    return InstStrategy::STATUS_UNFINISHED;
+  }else if( e==2 ){
+    InstMatch m;
+    for( int j = 0; j<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+      Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
+      if( i.getType().isDatatype() ){
+        Node n = getValueFor( i );
+        Debug("quant-datatypes-debug") << "Value for " << i << " is " << n << std::endl;
+        m.set(i,n);
+      }
+    }
+    //d_quantEngine->addInstantiation( f, m );
+  }
+  return InstStrategy::STATUS_UNKNOWN;
+}
+
+Node InstStrategyDatatypesValue::getValueFor( Node n ){
+  //simply get the ground value for n in the current model, if it exists,
+  //  or return an arbitrary ground term otherwise
+  if( !n.hasAttribute(InstConstantAttribute()) ){
+    return n;
+  }else{
+    return n;
+  }
+  /*  FIXME
+
+  Debug("quant-datatypes-debug")  << "get value for " << n << std::endl;
+  if( !n.hasAttribute(InstConstantAttribute()) ){
+    return n;
+  }else{
+    Assert( n.getType().isDatatype() );
+    //check if in equivalence class with ground term
+    Node rep = getRepresentative( n );
+    Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl;
+    if( !rep.hasAttribute(InstConstantAttribute()) ){
+      return rep;
+    }else{
+      if( !n.getType().isDatatype() ){
+        return n.getType().mkGroundTerm();
+      }else{
+        if( n.getKind()==APPLY_CONSTRUCTOR ){
+          std::vector< Node > children;
+          children.push_back( n.getOperator() );
+          for( int i=0; i<(int)n.getNumChildren(); i++ ){
+            children.push_back( getValueFor( n[i] ) );
+          }
+          return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+        }else{
+          const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+          TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels;
+          //otherwise, use which constructor the inst constant is current chosen to be
+          if( labels->find( n )!=labels->end() ){
+            TheoryDatatypes::EqList* lbl = (*labels->find( n )).second;
+            int tIndex = -1;
+            if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){
+              Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl;
+              tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr());
+            }else{
+              Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl;
+              //must find a possible choice
+              vector< bool > possibleCons;
+              possibleCons.resize( dt.getNumConstructors(), true );
+              for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
+                Node leqn = (*j);
+                possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
+              }
+              for( unsigned int j=0; j<possibleCons.size(); j++ ) {
+                if( possibleCons[j] ){
+                  tIndex = j;
+                  break;
+                }
+              }
+            }
+            Assert( tIndex!=-1 );
+            Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() );
+            Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl;
+            std::vector< Node > children;
+            children.push_back( cons );
+            for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) {
+              Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n );
+              if( n.hasAttribute(InstConstantAttribute()) ){
+                InstConstantAttribute ica;
+                sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) );
+              }
+              Node snn = getValueFor( sn );
+              children.push_back( snn );
+            }
+            return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+          }else{
+            return n.getType().mkGroundTerm();
+          }
+        }
+      }
+    }
+  }
+  */
+}
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 3ee423fe7..1c9565de6 100755
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -1,110 +1,110 @@
-/*********************                                                        */

-/*! \file inst_strategy_cbqi.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  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief instantiator_arith_instantiator

- **/

-

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__INST_STRATEGT_CBQI_H

-#define __CVC4__INST_STRATEGT_CBQI_H

-

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

-#include "theory/arith/arithvar_node_map.h"

-

-#include "util/statistics_registry.h"

-

-namespace CVC4 {

-namespace theory {

-

-namespace arith {

-  class TheoryArith;

-}

-

-namespace datatypes {

-  class TheoryDatatypes;

-}

-

-namespace quantifiers {

-

-

-class InstStrategySimplex : public InstStrategy{

-protected:

-  /** calculate if we should process this quantifier */

-  bool calculateShouldProcess( Node f );

-private:

-  /** reference to theory arithmetic */

-  arith::TheoryArith* d_th;

-  /** delta */

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

-  /** for each quantifier, simplex rows */

-  std::map< Node, std::vector< arith::ArithVar > > d_instRows;

-  /** tableaux */

-  std::map< arith::ArithVar, Node > d_tableaux_term;

-  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;

-  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;

-  /** ce tableaux */

-  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;

-  /** get value */

-  Node getTableauxValue( Node n, bool minus_delta = false );

-  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );

-  /** do instantiation */

-  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );

-  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );

-  /** add term to row */

-  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );

-  /** print debug */

-  void debugPrint( const char* c );

-private:

-  /** */

-  int d_counter;

-  /** negative one */

-  Node d_negOne;

-  /** process functions */

-  void processResetInstantiationRound( Theory::Effort effort );

-  int process( Node f, Theory::Effort effort, int e );

-public:

-  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );

-  ~InstStrategySimplex(){}

-  /** identify */

-  std::string identify() const { return std::string("Simplex"); }

-};

-

-

-class InstStrategyDatatypesValue : public InstStrategy

-{

-protected:

-  /** calculate if we should process this quantifier */

-  bool calculateShouldProcess( Node f );

-private:

-  /** reference to theory datatypes */

-  datatypes::TheoryDatatypes* d_th;

-  /** get value function */

-  Node getValueFor( Node n );

-public:

-  //constructor

-  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );

-  ~InstStrategyDatatypesValue(){}

-  /** reset instantiation */

-  void processResetInstantiationRound( Theory::Effort effort );

-  /** process method, returns a status */

-  int process( Node f, Theory::Effort effort, int e );

-  /** identify */

-  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }

-

-};/* class InstStrategy */

-

-}

-}

-}

-

+/*********************                                                        */
+/*! \file inst_strategy_cbqi.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  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief instantiator_arith_instantiator
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGT_CBQI_H
+#define __CVC4__INST_STRATEGT_CBQI_H
+
+#include "theory/quantifiers/instantiation_engine.h"
+#include "theory/arith/arithvar_node_map.h"
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace arith {
+  class TheoryArith;
+}
+
+namespace datatypes {
+  class TheoryDatatypes;
+}
+
+namespace quantifiers {
+
+
+class InstStrategySimplex : public InstStrategy{
+protected:
+  /** calculate if we should process this quantifier */
+  bool calculateShouldProcess( Node f );
+private:
+  /** reference to theory arithmetic */
+  arith::TheoryArith* d_th;
+  /** delta */
+  std::map< TypeNode, Node > d_deltas;
+  /** for each quantifier, simplex rows */
+  std::map< Node, std::vector< arith::ArithVar > > d_instRows;
+  /** tableaux */
+  std::map< arith::ArithVar, Node > d_tableaux_term;
+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux_ce_term;
+  std::map< arith::ArithVar, std::map< Node, Node > > d_tableaux;
+  /** ce tableaux */
+  std::map< arith::ArithVar, std::map< Node, Node > > d_ceTableaux;
+  /** get value */
+  Node getTableauxValue( Node n, bool minus_delta = false );
+  Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
+  /** do instantiation */
+  bool doInstantiation( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var );
+  bool doInstantiation2( Node f, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
+  /** add term to row */
+  void addTermToRow( arith::ArithVar x, Node n, Node& f, NodeBuilder<>& t );
+  /** print debug */
+  void debugPrint( const char* c );
+private:
+  /** */
+  int d_counter;
+  /** negative one */
+  Node d_negOne;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
+  ~InstStrategySimplex(){}
+  /** identify */
+  std::string identify() const { return std::string("Simplex"); }
+};
+
+
+class InstStrategyDatatypesValue : public InstStrategy
+{
+protected:
+  /** calculate if we should process this quantifier */
+  bool calculateShouldProcess( Node f );
+private:
+  /** reference to theory datatypes */
+  datatypes::TheoryDatatypes* d_th;
+  /** get value function */
+  Node getValueFor( Node n );
+public:
+  //constructor
+  InstStrategyDatatypesValue( datatypes::TheoryDatatypes* th, QuantifiersEngine* qe );
+  ~InstStrategyDatatypesValue(){}
+  /** reset instantiation */
+  void processResetInstantiationRound( Theory::Effort effort );
+  /** process method, returns a status */
+  int process( Node f, Theory::Effort effort, int e );
+  /** identify */
+  std::string identify() const { return std::string("InstStrategyDatatypesValue"); }
+
+};/* class InstStrategy */
+
+}
+}
+}
+
 #endif
\ No newline at end of file
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 48af334ff..edf9d976c 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -1,379 +1,379 @@
-/*********************                                                        */

-/*! \file inst_strategy_e_matching.cpp

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: mdeters

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Implementation of e matching instantiation strategies

- **/

-

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

-

-#include "theory/theory_engine.h"

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

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

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

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::inst;

-using namespace CVC4::theory::quantifiers;

-

-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

-//#define MULTI_TRIGGER_FULL_EFFORT_HALF

-#define MULTI_MULTI_TRIGGERS

-

-struct sortQuantifiersForSymbol {

-  QuantifiersEngine* d_qe;

-  bool operator() (Node i, Node j) {

-    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );

-    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );

-    if( nqfsi<nqfsj ){

-      return true;

-    }else if( nqfsi>nqfsj ){

-      return false;

-    }else{

-      return false;

-    }

-  }

-};

-

-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){

-  //reset triggers

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

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

-      it->second[i]->resetInstantiationRound();

-      it->second[i]->reset( Node::null() );

-    }

-  }

-}

-

-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){

-  if( e==0 ){

-    return STATUS_UNFINISHED;

-  }else if( e==1 ){

-    d_counter[f]++;

-    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;

-    //Notice() << "Try user-provided patterns..." << std::endl;

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

-      bool processTrigger = true;

-      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){

-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

-//        processTrigger = d_counter[f]%2==0;

-//#endif

-      }

-      if( processTrigger ){

-        //if( d_user_gen[f][i]->isMultiTrigger() )

-          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;

-        InstMatch baseMatch;

-        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );

-        //if( d_user_gen[f][i]->isMultiTrigger() )

-          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;

-        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;

-        if( d_user_gen[f][i]->isMultiTrigger() ){

-          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

-        }

-        //d_quantEngine->d_hasInstantiated[f] = true;

-      }

-    }

-    Debug("quant-uf-strategy") << "done." << std::endl;

-    //Notice() << "done" << std::endl;

-  }

-  return STATUS_UNKNOWN;

-}

-

-void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){

-  //add to generators

-  std::vector< Node > nodes;

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

-    nodes.push_back( pat[i] );

-  }

-  if( Trigger::isUsableTrigger( nodes, f ) ){

-    //extend to literal matching

-    d_quantEngine->getPhaseReqTerms( f, nodes );

-    //check match option

-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

-    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,

-                                                 options::smartTriggers() ) );

-  }

-}

-/*

-InstStrategyUserPatterns::Statistics::Statistics():

-  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)

-{

-  StatisticsRegistry::registerStat(&d_instantiations);

-}

-

-InstStrategyUserPatterns::Statistics::~Statistics(){

-  StatisticsRegistry::unregisterStat(&d_instantiations);

-}

-*/

-

-void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){

-  //reset triggers

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

-    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){

-      itt->first->resetInstantiationRound();

-      itt->first->reset( Node::null() );

-    }

-  }

-}

-

-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){

-  int peffort = f.getNumChildren()==3 ? 2 : 1;

-  //int peffort = f.getNumChildren()==3 ? 2 : 1;

-  //int peffort = 1;

-  if( e<peffort ){

-    return STATUS_UNFINISHED;

-  }else{

-    bool gen = false;

-    if( e==peffort ){

-      if( d_counter.find( f )==d_counter.end() ){

-        d_counter[f] = 0;

-        gen = true;

-      }else{

-        d_counter[f]++;

-        gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;

-      }

-    }else{

-      gen = true;

-    }

-    if( gen ){

-      generateTriggers( f );

-    }

-    Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;

-    //Notice() << "Try auto-generated triggers..." << std::endl;

-    for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){

-      Trigger* tr = itt->first;

-      if( tr ){

-        bool processTrigger = itt->second;

-        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){

-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF

-          processTrigger = d_counter[f]%2==0;

-#endif

-        }

-        if( processTrigger ){

-          //if( tr->isMultiTrigger() )

-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;

-          InstMatch baseMatch;

-          int numInst = tr->addInstantiations( baseMatch );

-          //if( tr->isMultiTrigger() )

-            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;

-          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){

-            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;

-          }else{

-            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;

-          }

-          if( tr->isMultiTrigger() ){

-            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;

-          }

-          //d_quantEngine->d_hasInstantiated[f] = true;

-        }

-      }

-    }

-    Debug("quant-uf-strategy") << "done." << std::endl;

-    //Notice() << "done" << std::endl;

-  }

-  return STATUS_UNKNOWN;

-}

-

-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){

-  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

-  if( d_patTerms[0].find( f )==d_patTerms[0].end() ){

-    //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy

-    d_patTerms[0][f].clear();

-    d_patTerms[1][f].clear();

-    std::vector< Node > patTermsF;

-    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );

-    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;

-    Debug("auto-gen-trigger") << "   ";

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

-      Debug("auto-gen-trigger") << patTermsF[i] << " ";

-    }

-    Debug("auto-gen-trigger") << std::endl;

-    //extend to literal matching (if applicable)

-    d_quantEngine->getPhaseReqTerms( f, patTermsF );

-    //sort into single/multi triggers

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

-    d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );

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

-      if( it->second.size()==f[0].getNumChildren() ){

-        d_patTerms[0][f].push_back( it->first );

-        d_is_single_trigger[ it->first ] = true;

-      }else{

-        d_patTerms[1][f].push_back( it->first );

-        d_is_single_trigger[ it->first ] = false;

-      }

-    }

-    d_made_multi_trigger[f] = false;

-    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;

-    Debug("auto-gen-trigger") << "   ";

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

-      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";

-    }

-    Debug("auto-gen-trigger") << std::endl;

-    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;

-    Debug("auto-gen-trigger") << "   ";

-    for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){

-      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";

-    }

-    Debug("auto-gen-trigger") << std::endl;

-  }

-

-  //populate candidate pattern term vector for the current trigger

-  std::vector< Node > patTerms;

-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER

-  //try to add single triggers first

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

-    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){

-      patTerms.push_back( d_patTerms[0][f][i] );

-    }

-  }

-  //if no single triggers exist, add multi trigger terms

-  if( patTerms.empty() ){

-    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

-  }

-#else

-  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );

-  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );

-#endif

-

-  if( !patTerms.empty() ){

-    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;

-    //sort terms based on relevance

-    if( d_rlv_strategy==RELEVANCE_DEFAULT ){

-      sortQuantifiersForSymbol sqfs;

-      sqfs.d_qe = d_quantEngine;

-      //sort based on # occurrences (this will cause Trigger to select rarer symbols)

-      std::sort( patTerms.begin(), patTerms.end(), sqfs );

-      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;

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

-        Debug("relevant-trigger") << "   " << patTerms[i] << " (";

-        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

-      }

-      //Notice() << "Terms based on relevance: " << std::endl;

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

-      //  Notice() << "   " << patTerms[i] << " (";

-      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;

-      //}

-    }

-    //now, generate the trigger...

-    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;

-    Trigger* tr = NULL;

-    if( d_is_single_trigger[ patTerms[0] ] ){

-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,

-                               options::smartTriggers() );

-      d_single_trigger_gen[ patTerms[0] ] = true;

-    }else{

-      //if we are re-generating triggers, shuffle based on some method

-      if( d_made_multi_trigger[f] ){

-#ifndef MULTI_MULTI_TRIGGERS

-        return;

-#endif

-        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly

-      }else{

-        d_made_multi_trigger[f] = true;

-      }

-      //will possibly want to get an old trigger

-      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,

-                               options::smartTriggers() );

-    }

-    if( tr ){

-      if( tr->isMultiTrigger() ){

-        //disable all other multi triggers

-        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){

-          if( it->first->isMultiTrigger() ){

-            d_auto_gen_trigger[f][ it->first ] = false;

-          }

-        }

-      }

-      //making it during an instantiation round, so must reset

-      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){

-        tr->resetInstantiationRound();

-        tr->reset( Node::null() );

-      }

-      d_auto_gen_trigger[f][tr] = true;

-      //if we are generating additional triggers...

-      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){

-        int index = 0;

-        if( index<(int)patTerms.size() ){

-          //Notice() << "check add additional" << std::endl;

-          //check if similar patterns exist, and if so, add them additionally

-          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );

-          index++;

-          bool success = true;

-          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){

-            success = false;

-            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){

-              d_single_trigger_gen[ patTerms[index] ] = true;

-              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,

-                                                 options::smartTriggers() );

-              if( tr2 ){

-                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;

-                tr2->resetInstantiationRound();

-                tr2->reset( Node::null() );

-                d_auto_gen_trigger[f][tr2] = true;

-              }

-              success = true;

-            }

-            index++;

-          }

-          //Notice() << "done check add additional" << std::endl;

-        }

-      }

-    }

-  }

-}

-/*

-InstStrategyAutoGenTriggers::Statistics::Statistics():

-  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),

-  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)

-{

-  StatisticsRegistry::registerStat(&d_instantiations);

-  StatisticsRegistry::registerStat(&d_instantiations_min);

-}

-

-InstStrategyAutoGenTriggers::Statistics::~Statistics(){

-  StatisticsRegistry::unregisterStat(&d_instantiations);

-  StatisticsRegistry::unregisterStat(&d_instantiations_min);

-}

-*/

-

-void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){

-}

-

-int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){

-  if( e<5 ){

-    return STATUS_UNFINISHED;

-  }else{

-    if( d_guessed.find( f )==d_guessed.end() ){

-      d_guessed[f] = true;

-      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;

-      InstMatch m;

-      if( d_quantEngine->addInstantiation( f, m ) ){

-        ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);

-        //d_quantEngine->d_hasInstantiated[f] = true;

-      }

-    }

-    return STATUS_UNKNOWN;

-  }

-}

-/*

-InstStrategyFreeVariable::Statistics::Statistics():

-  d_instantiations("InstStrategyGuess::Instantiations", 0)

-{

-  StatisticsRegistry::registerStat(&d_instantiations);

-}

-

-InstStrategyFreeVariable::Statistics::~Statistics(){

-  StatisticsRegistry::unregisterStat(&d_instantiations);

-}

-*/

+/*********************                                                        */
+/*! \file inst_strategy_e_matching.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): bobot
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of e matching instantiation strategies
+ **/
+
+#include "theory/quantifiers/inst_strategy_e_matching.h"
+
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/inst_match_generator.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers;
+
+#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
+//#define MULTI_TRIGGER_FULL_EFFORT_HALF
+#define MULTI_MULTI_TRIGGERS
+
+struct sortQuantifiersForSymbol {
+  QuantifiersEngine* d_qe;
+  bool operator() (Node i, Node j) {
+    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
+    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
+    if( nqfsi<nqfsj ){
+      return true;
+    }else if( nqfsi>nqfsj ){
+      return false;
+    }else{
+      return false;
+    }
+  }
+};
+
+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
+  //reset triggers
+  for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
+    for( int i=0; i<(int)it->second.size(); i++ ){
+      it->second[i]->resetInstantiationRound();
+      it->second[i]->reset( Node::null() );
+    }
+  }
+}
+
+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
+  if( e==0 ){
+    return STATUS_UNFINISHED;
+  }else if( e==1 ){
+    d_counter[f]++;
+    Debug("quant-uf-strategy") << "Try user-provided patterns..." << std::endl;
+    //Notice() << "Try user-provided patterns..." << std::endl;
+    for( int i=0; i<(int)d_user_gen[f].size(); i++ ){
+      bool processTrigger = true;
+      if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){
+//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
+//        processTrigger = d_counter[f]%2==0;
+//#endif
+      }
+      if( processTrigger ){
+        //if( d_user_gen[f][i]->isMultiTrigger() )
+          //Notice() << "  Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
+        InstMatch baseMatch;
+        int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
+        //if( d_user_gen[f][i]->isMultiTrigger() )
+          //Notice() << "  Done, numInst = " << numInst << "." << std::endl;
+        d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;
+        if( d_user_gen[f][i]->isMultiTrigger() ){
+          d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+        }
+        //d_quantEngine->d_hasInstantiated[f] = true;
+      }
+    }
+    Debug("quant-uf-strategy") << "done." << std::endl;
+    //Notice() << "done" << std::endl;
+  }
+  return STATUS_UNKNOWN;
+}
+
+void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
+  //add to generators
+  std::vector< Node > nodes;
+  for( int i=0; i<(int)pat.getNumChildren(); i++ ){
+    nodes.push_back( pat[i] );
+  }
+  if( Trigger::isUsableTrigger( nodes, f ) ){
+    //extend to literal matching
+    d_quantEngine->getPhaseReqTerms( f, nodes );
+    //check match option
+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
+                                                 options::smartTriggers() ) );
+  }
+}
+/*
+InstStrategyUserPatterns::Statistics::Statistics():
+  d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyUserPatterns::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
+
+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
+  //reset triggers
+  for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
+    for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+      itt->first->resetInstantiationRound();
+      itt->first->reset( Node::null() );
+    }
+  }
+}
+
+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
+  int peffort = f.getNumChildren()==3 ? 2 : 1;
+  //int peffort = f.getNumChildren()==3 ? 2 : 1;
+  //int peffort = 1;
+  if( e<peffort ){
+    return STATUS_UNFINISHED;
+  }else{
+    bool gen = false;
+    if( e==peffort ){
+      if( d_counter.find( f )==d_counter.end() ){
+        d_counter[f] = 0;
+        gen = true;
+      }else{
+        d_counter[f]++;
+        gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
+      }
+    }else{
+      gen = true;
+    }
+    if( gen ){
+      generateTriggers( f );
+    }
+    Debug("quant-uf-strategy")  << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;
+    //Notice() << "Try auto-generated triggers..." << std::endl;
+    for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){
+      Trigger* tr = itt->first;
+      if( tr ){
+        bool processTrigger = itt->second;
+        if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){
+#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF
+          processTrigger = d_counter[f]%2==0;
+#endif
+        }
+        if( processTrigger ){
+          //if( tr->isMultiTrigger() )
+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Process " << (*tr) << "..." << std::endl;
+          InstMatch baseMatch;
+          int numInst = tr->addInstantiations( baseMatch );
+          //if( tr->isMultiTrigger() )
+            Debug("quant-uf-strategy-auto-gen-triggers") << "  Done, numInst = " << numInst << "." << std::endl;
+          if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;
+          }else{
+            d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+          }
+          if( tr->isMultiTrigger() ){
+            d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+          }
+          //d_quantEngine->d_hasInstantiated[f] = true;
+        }
+      }
+    }
+    Debug("quant-uf-strategy") << "done." << std::endl;
+    //Notice() << "done" << std::endl;
+  }
+  return STATUS_UNKNOWN;
+}
+
+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
+  Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+  if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
+    //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
+    d_patTerms[0][f].clear();
+    d_patTerms[1][f].clear();
+    std::vector< Node > patTermsF;
+    Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );
+    Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;
+    Debug("auto-gen-trigger") << "   ";
+    for( int i=0; i<(int)patTermsF.size(); i++ ){
+      Debug("auto-gen-trigger") << patTermsF[i] << " ";
+    }
+    Debug("auto-gen-trigger") << std::endl;
+    //extend to literal matching (if applicable)
+    d_quantEngine->getPhaseReqTerms( f, patTermsF );
+    //sort into single/multi triggers
+    std::map< Node, std::vector< Node > > varContains;
+    d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains );
+    for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
+      if( it->second.size()==f[0].getNumChildren() ){
+        d_patTerms[0][f].push_back( it->first );
+        d_is_single_trigger[ it->first ] = true;
+      }else{
+        d_patTerms[1][f].push_back( it->first );
+        d_is_single_trigger[ it->first ] = false;
+      }
+    }
+    d_made_multi_trigger[f] = false;
+    Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;
+    Debug("auto-gen-trigger") << "   ";
+    for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
+      Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";
+    }
+    Debug("auto-gen-trigger") << std::endl;
+    Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
+    Debug("auto-gen-trigger") << "   ";
+    for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
+      Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
+    }
+    Debug("auto-gen-trigger") << std::endl;
+  }
+
+  //populate candidate pattern term vector for the current trigger
+  std::vector< Node > patTerms;
+#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER
+  //try to add single triggers first
+  for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
+    if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
+      patTerms.push_back( d_patTerms[0][f][i] );
+    }
+  }
+  //if no single triggers exist, add multi trigger terms
+  if( patTerms.empty() ){
+    patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
+  }
+#else
+  patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );
+  patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
+#endif
+
+  if( !patTerms.empty() ){
+    Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+    //sort terms based on relevance
+    if( d_rlv_strategy==RELEVANCE_DEFAULT ){
+      sortQuantifiersForSymbol sqfs;
+      sqfs.d_qe = d_quantEngine;
+      //sort based on # occurrences (this will cause Trigger to select rarer symbols)
+      std::sort( patTerms.begin(), patTerms.end(), sqfs );
+      Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+      for( int i=0; i<(int)patTerms.size(); i++ ){
+        Debug("relevant-trigger") << "   " << patTerms[i] << " (";
+        Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+      }
+      //Notice() << "Terms based on relevance: " << std::endl;
+      //for( int i=0; i<(int)patTerms.size(); i++ ){
+      //  Notice() << "   " << patTerms[i] << " (";
+      //  Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+      //}
+    }
+    //now, generate the trigger...
+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    Trigger* tr = NULL;
+    if( d_is_single_trigger[ patTerms[0] ] ){
+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
+                               options::smartTriggers() );
+      d_single_trigger_gen[ patTerms[0] ] = true;
+    }else{
+      //if we are re-generating triggers, shuffle based on some method
+      if( d_made_multi_trigger[f] ){
+#ifndef MULTI_MULTI_TRIGGERS
+        return;
+#endif
+        std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+      }else{
+        d_made_multi_trigger[f] = true;
+      }
+      //will possibly want to get an old trigger
+      tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
+                               options::smartTriggers() );
+    }
+    if( tr ){
+      if( tr->isMultiTrigger() ){
+        //disable all other multi triggers
+        for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
+          if( it->first->isMultiTrigger() ){
+            d_auto_gen_trigger[f][ it->first ] = false;
+          }
+        }
+      }
+      //making it during an instantiation round, so must reset
+      if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
+        tr->resetInstantiationRound();
+        tr->reset( Node::null() );
+      }
+      d_auto_gen_trigger[f][tr] = true;
+      //if we are generating additional triggers...
+      if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
+        int index = 0;
+        if( index<(int)patTerms.size() ){
+          //Notice() << "check add additional" << std::endl;
+          //check if similar patterns exist, and if so, add them additionally
+          int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+          index++;
+          bool success = true;
+          while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+            success = false;
+            if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+              d_single_trigger_gen[ patTerms[index] ] = true;
+              Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
+                                                 options::smartTriggers() );
+              if( tr2 ){
+                //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
+                tr2->resetInstantiationRound();
+                tr2->reset( Node::null() );
+                d_auto_gen_trigger[f][tr2] = true;
+              }
+              success = true;
+            }
+            index++;
+          }
+          //Notice() << "done check add additional" << std::endl;
+        }
+      }
+    }
+  }
+}
+/*
+InstStrategyAutoGenTriggers::Statistics::Statistics():
+  d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
+  d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+  StatisticsRegistry::registerStat(&d_instantiations_min);
+}
+
+InstStrategyAutoGenTriggers::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+  StatisticsRegistry::unregisterStat(&d_instantiations_min);
+}
+*/
+
+void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
+}
+
+int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){
+  if( e<5 ){
+    return STATUS_UNFINISHED;
+  }else{
+    if( d_guessed.find( f )==d_guessed.end() ){
+      d_guessed[f] = true;
+      Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
+      InstMatch m;
+      if( d_quantEngine->addInstantiation( f, m ) ){
+        ++(d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_guess);
+        //d_quantEngine->d_hasInstantiated[f] = true;
+      }
+    }
+    return STATUS_UNKNOWN;
+  }
+}
+/*
+InstStrategyFreeVariable::Statistics::Statistics():
+  d_instantiations("InstStrategyGuess::Instantiations", 0)
+{
+  StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyFreeVariable::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index 23f0d8a54..b5ff90a62 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -1,135 +1,135 @@
-/*********************                                                        */

-/*! \file inst_strategy_e_matching.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: none

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief E matching instantiation strategies

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H

-#define __CVC4__INST_STRATEGY_E_MATCHING_H

-

-#include "theory/quantifiers_engine.h"

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

-

-#include "context/context.h"

-#include "context/context_mm.h"

-

-#include "util/statistics_registry.h"

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

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-//instantiation strategies

-

-class InstStrategyUserPatterns : public InstStrategy{

-private:

-  /** explicitly provided patterns */

-  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;

-  /** counter for quantifiers */

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

-  /** process functions */

-  void processResetInstantiationRound( Theory::Effort effort );

-  int process( Node f, Theory::Effort effort, int e );

-public:

-  InstStrategyUserPatterns( QuantifiersEngine* ie ) :

-      InstStrategy( ie ){}

-  ~InstStrategyUserPatterns(){}

-public:

-  /** add pattern */

-  void addUserPattern( Node f, Node pat );

-  /** get num patterns */

-  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }

-  /** get user pattern */

-  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }

-  /** identify */

-  std::string identify() const { return std::string("UserPatterns"); }

-};/* class InstStrategyUserPatterns */

-

-class InstStrategyAutoGenTriggers : public InstStrategy{

-public:

-  enum {

-    RELEVANCE_NONE,

-    RELEVANCE_DEFAULT,

-  };

-private:

-  /** trigger generation strategy */

-  int d_tr_strategy;

-  /** relevance strategy */

-  int d_rlv_strategy;

-  /** regeneration */

-  bool d_regenerate;

-  int d_regenerate_frequency;

-  /** generate additional triggers */

-  bool d_generate_additional;

-  /** triggers for each quantifier */

-  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;

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

-  /** single, multi triggers for each quantifier */

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

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

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

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

-private:

-  /** process functions */

-  void processResetInstantiationRound( Theory::Effort effort );

-  int process( Node f, Theory::Effort effort, int e );

-  /** generate triggers */

-  void generateTriggers( Node f );

-public:

-  /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)

-      rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)

-      rgfr is the frequency at which triggers are generated */

-  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :

-      InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){

-    setRegenerateFrequency( rgfr );

-  }

-  ~InstStrategyAutoGenTriggers(){}

-public:

-  /** get auto-generated trigger */

-  inst::Trigger* getAutoGenTrigger( Node f );

-  /** identify */

-  std::string identify() const { return std::string("AutoGenTriggers"); }

-  /** set regenerate frequency, if fr<0, turn off regenerate */

-  void setRegenerateFrequency( int fr ){

-    if( fr<0 ){

-      d_regenerate = false;

-    }else{

-      d_regenerate_frequency = fr;

-      d_regenerate = true;

-    }

-  }

-  /** set generate additional */

-  void setGenerateAdditional( bool val ) { d_generate_additional = val; }

-};/* class InstStrategyAutoGenTriggers */

-

-class InstStrategyFreeVariable : public InstStrategy{

-private:

-  /** guessed instantiations */

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

-  /** process functions */

-  void processResetInstantiationRound( Theory::Effort effort );

-  int process( Node f, Theory::Effort effort, int e );

-public:

-  InstStrategyFreeVariable( QuantifiersEngine* qe ) :

-      InstStrategy( qe ){}

-  ~InstStrategyFreeVariable(){}

-  /** identify */

-  std::string identify() const { return std::string("FreeVariable"); }

-};/* class InstStrategyFreeVariable */

-

-}

-}/* CVC4::theory namespace */

-}/* CVC4 namespace */

-

-#endif

+/*********************                                                        */
+/*! \file inst_strategy_e_matching.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): bobot, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief E matching instantiation strategies
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
+#define __CVC4__INST_STRATEGY_E_MATCHING_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/trigger.h"
+
+#include "context/context.h"
+#include "context/context_mm.h"
+
+#include "util/statistics_registry.h"
+#include "theory/quantifiers/instantiation_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//instantiation strategies
+
+class InstStrategyUserPatterns : public InstStrategy{
+private:
+  /** explicitly provided patterns */
+  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
+  /** counter for quantifiers */
+  std::map< Node, int > d_counter;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategyUserPatterns( QuantifiersEngine* ie ) :
+      InstStrategy( ie ){}
+  ~InstStrategyUserPatterns(){}
+public:
+  /** add pattern */
+  void addUserPattern( Node f, Node pat );
+  /** get num patterns */
+  int getNumUserGenerators( Node f ) { return (int)d_user_gen[f].size(); }
+  /** get user pattern */
+  inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
+  /** identify */
+  std::string identify() const { return std::string("UserPatterns"); }
+};/* class InstStrategyUserPatterns */
+
+class InstStrategyAutoGenTriggers : public InstStrategy{
+public:
+  enum {
+    RELEVANCE_NONE,
+    RELEVANCE_DEFAULT,
+  };
+private:
+  /** trigger generation strategy */
+  int d_tr_strategy;
+  /** relevance strategy */
+  int d_rlv_strategy;
+  /** regeneration */
+  bool d_regenerate;
+  int d_regenerate_frequency;
+  /** generate additional triggers */
+  bool d_generate_additional;
+  /** triggers for each quantifier */
+  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
+  std::map< Node, int > d_counter;
+  /** single, multi triggers for each quantifier */
+  std::map< Node, std::vector< Node > > d_patTerms[2];
+  std::map< Node, bool > d_is_single_trigger;
+  std::map< Node, bool > d_single_trigger_gen;
+  std::map< Node, bool > d_made_multi_trigger;
+private:
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+  /** generate triggers */
+  void generateTriggers( Node f );
+public:
+  /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
+      rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
+      rgfr is the frequency at which triggers are generated */
+  InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :
+      InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){
+    setRegenerateFrequency( rgfr );
+  }
+  ~InstStrategyAutoGenTriggers(){}
+public:
+  /** get auto-generated trigger */
+  inst::Trigger* getAutoGenTrigger( Node f );
+  /** identify */
+  std::string identify() const { return std::string("AutoGenTriggers"); }
+  /** set regenerate frequency, if fr<0, turn off regenerate */
+  void setRegenerateFrequency( int fr ){
+    if( fr<0 ){
+      d_regenerate = false;
+    }else{
+      d_regenerate_frequency = fr;
+      d_regenerate = true;
+    }
+  }
+  /** set generate additional */
+  void setGenerateAdditional( bool val ) { d_generate_additional = val; }
+};/* class InstStrategyAutoGenTriggers */
+
+class InstStrategyFreeVariable : public InstStrategy{
+private:
+  /** guessed instantiations */
+  std::map< Node, bool > d_guessed;
+  /** process functions */
+  void processResetInstantiationRound( Theory::Effort effort );
+  int process( Node f, Theory::Effort effort, int e );
+public:
+  InstStrategyFreeVariable( QuantifiersEngine* qe ) :
+      InstStrategy( qe ){}
+  ~InstStrategyFreeVariable(){}
+  /** identify */
+  std::string identify() const { return std::string("FreeVariable"); }
+};/* class InstStrategyFreeVariable */
+
+}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index c116b73f5..5c7c9415e 100755
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -1,375 +1,375 @@
-/*********************                                                        */

-/*! \file macros.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-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Sort inference module

- **

- ** This class implements quantifiers macro definitions.

- **/

-

-#include <vector>

-

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

-#include "theory/rewriter.h"

-

-using namespace CVC4;

-using namespace std;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-

-bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){

-  //first, collect macro definitions

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

-    if( assertions[i].getKind()==FORALL ){

-      std::vector< Node > args;

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

-        args.push_back( assertions[i][0][j] );

-      }

-      //look at the body of the quantifier for macro definition

-      process( assertions[i][1], true, args, assertions[i] );

-    }

-  }

-  //create macro defs

-  for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin();

-       it != d_macro_def_cases.end(); ++it ){

-    //create ite based on case definitions

-    Node val;

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

-      if( it->second[i].first.isNull() ){

-        Assert( i==0 );

-        val = it->second[i].second;

-      }else{

-        //if value is null, must generate it

-        if( val.isNull() ){

-          std::stringstream ss;

-          ss << "mdo_" << it->first << "_$$";

-          Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );

-          //will be defined in terms of fresh operator

-          std::vector< Node > children;

-          children.push_back( op );

-          children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() );

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

-        }

-        val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val );

-      }

-    }

-    d_macro_defs[ it->first ] = val;

-    Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl;

-  }

-  //now simplify bodies

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

-    d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) );

-  }

-  bool retVal = false;

-  if( doRewrite && !d_macro_defs.empty() ){

-    //now, rewrite based on macro definitions

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

-      Node prev = assertions[i];

-      assertions[i] = simplify( assertions[i] );

-      if( prev!=assertions[i] ){

-        assertions[i] = Rewriter::rewrite( assertions[i] );

-        Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;

-        retVal = true;

-      }

-    }

-  }

-  return retVal;

-}

-

-bool QuantifierMacros::contains( Node n, Node n_s ){

-  if( n==n_s ){

-    return true;

-  }else{

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

-      if( contains( n[i], n_s ) ){

-        return true;

-      }

-    }

-    return false;

-  }

-}

-

-bool QuantifierMacros::containsBadOp( Node n, Node n_op ){

-  if( n!=n_op ){

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

-      Node op = n.getOperator();

-      if( op==n_op.getOperator() ){

-        return true;

-      }

-      if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){

-        return true;

-      }

-    }

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

-      if( containsBadOp( n[i], n_op ) ){

-        return true;

-      }

-    }

-  }

-  return false;

-}

-

-bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){

-  return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );

-}

-

-void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){

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

-    candidates.push_back( n );

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

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

-      getMacroCandidates( n[i], candidates );

-    }

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

-    //if the LHS is a constant

-    if( n.getNumChildren()==2 && n[0].isConst() ){

-      getMacroCandidates( n[1], candidates );

-    }

-  }

-}

-

-Node QuantifierMacros::solveInEquality( Node n, Node lit ){

-  if( lit.getKind()==IFF || lit.getKind()==EQUAL ){

-    //return the opposite side of the equality if defined that way

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

-      if( lit[i]==n ){

-        return lit[ i==0 ? 1 : 0];

-      }

-    }

-    //must solve for term n in the literal lit

-    if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){

-      Node coeff;

-      Node term;

-      //could be solved for on LHS

-      if( lit[0].getKind()==MULT && lit[0][1]==n ){

-        Assert( lit[0][0].isConst() );

-        term = lit[1];

-        coeff = lit[0][0];

-      }else{

-        Assert( lit[1].getKind()==PLUS );

-        std::vector< Node > plus_children;

-        //find monomial with n

-        for( size_t j=0; j<lit[1].getNumChildren(); j++ ){

-          if( lit[1][j]==n ){

-            Assert( coeff.isNull() );

-            coeff = NodeManager::currentNM()->mkConst( Rational(1) );

-          }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){

-            Assert( coeff.isNull() );

-            Assert( lit[1][j][0].isConst() );

-            coeff = lit[1][j][0];

-          }else{

-            plus_children.push_back( lit[1][j] );

-          }

-        }

-        if( !coeff.isNull() ){

-          term = NodeManager::currentNM()->mkNode( PLUS, plus_children );

-          term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );

-        }

-      }

-      if( !coeff.isNull() ){

-        coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );

-        term = NodeManager::currentNM()->mkNode( MULT, coeff, term );

-        term = Rewriter::rewrite( term );

-        return term;

-      }

-    }

-  }

-  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;

-  return Node::null();

-}

-

-bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){

-  if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){

-    return true;

-  }else{

-    return false;

-  }

-}

-

-bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){

-  if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){

-    if( std::find( vars.begin(), vars.end(), n )==vars.end() ){

-      if( retOnly ){

-        return true;

-      }else{

-        vars.push_back( n );

-      }

-    }

-  }

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

-    if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){

-      return true;

-    }

-  }

-  return false;

-}

-

-bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,

-                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){

-  bool success = true;

-  for( size_t a=0; a<v_quant.size(); a++ ){

-    if( !solved[ v_quant[a] ].isNull() ){

-      vars.push_back( v_quant[a] );

-      subs.push_back( solved[ v_quant[a] ] );

-    }else{

-      if( reqComplete ){

-        success = false;

-        break;

-      }

-    }

-  }

-  return success;

-}

-

-void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){

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

-    process( n[0], !pol, args, f );

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

-    //bool favorPol = (n.getKind()==AND)==pol;

-    //conditional?

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

-    //can not do anything

-  }else{

-    //literal case

-    if( isMacroLiteral( n, pol ) ){

-      std::vector< Node > candidates;

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

-        getMacroCandidates( n[i], candidates );

-      }

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

-        Node m = candidates[i];

-        Node op = m.getOperator();

-        if( !containsBadOp( n, m ) ){

-          std::vector< Node > fvs;

-          getFreeVariables( m, args, fvs, false );

-          //get definition and condition

-          Node n_def = solveInEquality( m, n ); //definition for the macro

-          //definition must exist and not contain any free variables apart from fvs

-          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){

-            Node n_cond;  //condition when this definition holds

-            //conditional must not contain any free variables apart from fvs

-            if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){

-              Trace("macros") << m << " is possible macro in " << f << std::endl;

-              //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where

-              // x1 ... xn are distinct variables

-              if( d_macro_basis[op].empty() ){

-                for( size_t a=0; a<m.getNumChildren(); a++ ){

-                  std::stringstream ss;

-                  ss << "mda_" << op << "_$$";

-                  Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );

-                  d_macro_basis[op].push_back( v );

-                }

-              }

-              std::vector< Node > eq;

-              for( size_t a=0; a<m.getNumChildren(); a++ ){

-                eq.push_back( m[a] );

-              }

-              //solve system of equations "d_macro_basis[op] = m" for variables in fvs

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

-              //solve obvious cases first

-              for( size_t a=0; a<eq.size(); a++ ){

-                if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){

-                  if( solved[ eq[a] ].isNull() ){

-                    solved[ eq[a] ] = d_macro_basis[op][a];

-                  }

-                }

-              }

-              //now, apply substitution for obvious cases

-              std::vector< Node > vars;

-              std::vector< Node > subs;

-              getSubstitution( fvs, solved, vars, subs, false );

-              for( size_t a=0; a<eq.size(); a++ ){

-                eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );

-              }

-

-              Trace("macros-eq") << "Solve system of equations : " << std::endl;

-              for( size_t a=0; a<m.getNumChildren(); a++ ){

-                if( d_macro_basis[op][a]!=eq[a] ){

-                  Trace("macros-eq") << "   " << d_macro_basis[op][a] << " = " << eq[a] << std::endl;

-                }

-              }

-              Trace("macros-eq") << " for ";

-              for( size_t a=0; a<fvs.size(); a++ ){

-                if( solved[ fvs[a] ].isNull() ){

-                  Trace("macros-eq") << fvs[a] << " ";

-                }

-              }

-              Trace("macros-eq") << std::endl;

-              //DO_THIS

-

-

-              vars.clear();

-              subs.clear();

-              if( getSubstitution( fvs, solved, vars, subs, true ) ){

-                //build condition

-                std::vector< Node > conds;

-                if( !n_cond.isNull() ){

-                  //must apply substitution obtained from solving system of equations to original condition

-                  n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );

-                  conds.push_back( n_cond );

-                }

-                for( size_t a=0; a<eq.size(); a++ ){

-                  //collect conditions based on solving argument's system of equations

-                  if( d_macro_basis[op][a]!=eq[a] ){

-                    conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) );

-                  }

-                }

-                //build the condition

-                if( !conds.empty() ){

-                  n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds );

-                }

-                //apply the substitution to the

-                n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );

-                //now see if definition is consistent with others

-                if( isConsistentDefinition( op, n_cond, n_def ) ){

-                  //must clear if it is a base definition

-                  if( n_cond.isNull() ){

-                    d_macro_def_cases[ op ].clear();

-                  }

-                  d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) );

-                }

-              }

-            }

-          }

-        }

-      }

-    }

-  }

-}

-

-Node QuantifierMacros::simplify( Node n ){

-  Trace("macros-debug") << "simplify " << n << std::endl;

-  std::vector< Node > children;

-  bool childChanged = false;

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

-    Node nn = simplify( n[i] );

-    children.push_back( nn );

-    childChanged = childChanged || nn!=n[i];

-  }

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

-    Node op = n.getOperator();

-    if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){

-      //do subsitutition

-      Node ret = d_macro_defs[op];

-      ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );

-      return ret;

-    }

-  }

-  if( childChanged ){

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

-      children.insert( children.begin(), n.getOperator() );

-    }

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

-  }else{

-    return n;

-  }

-}

+/*********************                                                        */
+/*! \file macros.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sort inference module
+ **
+ ** This class implements quantifiers macro definitions.
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/macros.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
+  //first, collect macro definitions
+  for( size_t i=0; i<assertions.size(); i++ ){
+    if( assertions[i].getKind()==FORALL ){
+      std::vector< Node > args;
+      for( size_t j=0; j<assertions[i][0].getNumChildren(); j++ ){
+        args.push_back( assertions[i][0][j] );
+      }
+      //look at the body of the quantifier for macro definition
+      process( assertions[i][1], true, args, assertions[i] );
+    }
+  }
+  //create macro defs
+  for( std::map< Node, std::vector< std::pair< Node, Node > > >::iterator it = d_macro_def_cases.begin();
+       it != d_macro_def_cases.end(); ++it ){
+    //create ite based on case definitions
+    Node val;
+    for( size_t i=0; i<it->second.size(); ++i ){
+      if( it->second[i].first.isNull() ){
+        Assert( i==0 );
+        val = it->second[i].second;
+      }else{
+        //if value is null, must generate it
+        if( val.isNull() ){
+          std::stringstream ss;
+          ss << "mdo_" << it->first << "_$$";
+          Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" );
+          //will be defined in terms of fresh operator
+          std::vector< Node > children;
+          children.push_back( op );
+          children.insert( children.end(), d_macro_basis[ it->first ].begin(), d_macro_basis[ it->first ].end() );
+          val = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        }
+        val = NodeManager::currentNM()->mkNode( ITE, it->second[i].first, it->second[i].second, val );
+      }
+    }
+    d_macro_defs[ it->first ] = val;
+    Trace("macros-def") << "* " << val << " is a macro for " << it->first << std::endl;
+  }
+  //now simplify bodies
+  for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){
+    d_macro_defs[ it->first ] = Rewriter::rewrite( simplify( it->second ) );
+  }
+  bool retVal = false;
+  if( doRewrite && !d_macro_defs.empty() ){
+    //now, rewrite based on macro definitions
+    for( size_t i=0; i<assertions.size(); i++ ){
+      Node prev = assertions[i];
+      assertions[i] = simplify( assertions[i] );
+      if( prev!=assertions[i] ){
+        assertions[i] = Rewriter::rewrite( assertions[i] );
+        Trace("macros-rewrite") << "Rewrite " << prev << " to " << assertions[i] << std::endl;
+        retVal = true;
+      }
+    }
+  }
+  return retVal;
+}
+
+bool QuantifierMacros::contains( Node n, Node n_s ){
+  if( n==n_s ){
+    return true;
+  }else{
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( contains( n[i], n_s ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
+bool QuantifierMacros::containsBadOp( Node n, Node n_op ){
+  if( n!=n_op ){
+    if( n.getKind()==APPLY_UF ){
+      Node op = n.getOperator();
+      if( op==n_op.getOperator() ){
+        return true;
+      }
+      if( d_macro_def_cases.find( op )!=d_macro_def_cases.end() && !d_macro_def_cases[op].empty() ){
+        return true;
+      }
+    }
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      if( containsBadOp( n[i], n_op ) ){
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
+  return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );
+}
+
+void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
+  if( n.getKind()==APPLY_UF ){
+    candidates.push_back( n );
+  }else if( n.getKind()==PLUS ){
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      getMacroCandidates( n[i], candidates );
+    }
+  }else if( n.getKind()==MULT ){
+    //if the LHS is a constant
+    if( n.getNumChildren()==2 && n[0].isConst() ){
+      getMacroCandidates( n[1], candidates );
+    }
+  }
+}
+
+Node QuantifierMacros::solveInEquality( Node n, Node lit ){
+  if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
+    //return the opposite side of the equality if defined that way
+    for( int i=0; i<2; i++ ){
+      if( lit[i]==n ){
+        return lit[ i==0 ? 1 : 0];
+      }
+    }
+    //must solve for term n in the literal lit
+    if( lit[0].getType().isInteger() || lit[0].getType().isReal() ){
+      Node coeff;
+      Node term;
+      //could be solved for on LHS
+      if( lit[0].getKind()==MULT && lit[0][1]==n ){
+        Assert( lit[0][0].isConst() );
+        term = lit[1];
+        coeff = lit[0][0];
+      }else{
+        Assert( lit[1].getKind()==PLUS );
+        std::vector< Node > plus_children;
+        //find monomial with n
+        for( size_t j=0; j<lit[1].getNumChildren(); j++ ){
+          if( lit[1][j]==n ){
+            Assert( coeff.isNull() );
+            coeff = NodeManager::currentNM()->mkConst( Rational(1) );
+          }else if( lit[1][j].getKind()==MULT && lit[1][j][1]==n ){
+            Assert( coeff.isNull() );
+            Assert( lit[1][j][0].isConst() );
+            coeff = lit[1][j][0];
+          }else{
+            plus_children.push_back( lit[1][j] );
+          }
+        }
+        if( !coeff.isNull() ){
+          term = NodeManager::currentNM()->mkNode( PLUS, plus_children );
+          term = NodeManager::currentNM()->mkNode( MINUS, lit[0], term );
+        }
+      }
+      if( !coeff.isNull() ){
+        coeff = NodeManager::currentNM()->mkConst( Rational(1) / coeff.getConst<Rational>() );
+        term = NodeManager::currentNM()->mkNode( MULT, coeff, term );
+        term = Rewriter::rewrite( term );
+        return term;
+      }
+    }
+  }
+  Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl;
+  return Node::null();
+}
+
+bool QuantifierMacros::isConsistentDefinition( Node op, Node cond, Node def ){
+  if( d_macro_def_cases[op].empty() || ( cond.isNull() && !d_macro_def_cases[op][0].first.isNull() ) ){
+    return true;
+  }else{
+    return false;
+  }
+}
+
+bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ){
+  if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){
+    if( std::find( vars.begin(), vars.end(), n )==vars.end() ){
+      if( retOnly ){
+        return true;
+      }else{
+        vars.push_back( n );
+      }
+    }
+  }
+  for( size_t i=0; i<n.getNumChildren(); i++ ){
+    if( getFreeVariables( n[i], v_quant, vars, retOnly ) ){
+      return true;
+    }
+  }
+  return false;
+}
+
+bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+                                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){
+  bool success = true;
+  for( size_t a=0; a<v_quant.size(); a++ ){
+    if( !solved[ v_quant[a] ].isNull() ){
+      vars.push_back( v_quant[a] );
+      subs.push_back( solved[ v_quant[a] ] );
+    }else{
+      if( reqComplete ){
+        success = false;
+        break;
+      }
+    }
+  }
+  return success;
+}
+
+void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){
+  if( n.getKind()==NOT ){
+    process( n[0], !pol, args, f );
+  }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){
+    //bool favorPol = (n.getKind()==AND)==pol;
+    //conditional?
+  }else if( n.getKind()==ITE ){
+    //can not do anything
+  }else{
+    //literal case
+    if( isMacroLiteral( n, pol ) ){
+      std::vector< Node > candidates;
+      for( size_t i=0; i<n.getNumChildren(); i++ ){
+        getMacroCandidates( n[i], candidates );
+      }
+      for( size_t i=0; i<candidates.size(); i++ ){
+        Node m = candidates[i];
+        Node op = m.getOperator();
+        if( !containsBadOp( n, m ) ){
+          std::vector< Node > fvs;
+          getFreeVariables( m, args, fvs, false );
+          //get definition and condition
+          Node n_def = solveInEquality( m, n ); //definition for the macro
+          //definition must exist and not contain any free variables apart from fvs
+          if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) ){
+            Node n_cond;  //condition when this definition holds
+            //conditional must not contain any free variables apart from fvs
+            if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){
+              Trace("macros") << m << " is possible macro in " << f << std::endl;
+              //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
+              // x1 ... xn are distinct variables
+              if( d_macro_basis[op].empty() ){
+                for( size_t a=0; a<m.getNumChildren(); a++ ){
+                  std::stringstream ss;
+                  ss << "mda_" << op << "_$$";
+                  Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" );
+                  d_macro_basis[op].push_back( v );
+                }
+              }
+              std::vector< Node > eq;
+              for( size_t a=0; a<m.getNumChildren(); a++ ){
+                eq.push_back( m[a] );
+              }
+              //solve system of equations "d_macro_basis[op] = m" for variables in fvs
+              std::map< Node, Node > solved;
+              //solve obvious cases first
+              for( size_t a=0; a<eq.size(); a++ ){
+                if( std::find( fvs.begin(), fvs.end(), eq[a] )!=fvs.end() ){
+                  if( solved[ eq[a] ].isNull() ){
+                    solved[ eq[a] ] = d_macro_basis[op][a];
+                  }
+                }
+              }
+              //now, apply substitution for obvious cases
+              std::vector< Node > vars;
+              std::vector< Node > subs;
+              getSubstitution( fvs, solved, vars, subs, false );
+              for( size_t a=0; a<eq.size(); a++ ){
+                eq[a] = eq[a].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+              }
+
+              Trace("macros-eq") << "Solve system of equations : " << std::endl;
+              for( size_t a=0; a<m.getNumChildren(); a++ ){
+                if( d_macro_basis[op][a]!=eq[a] ){
+                  Trace("macros-eq") << "   " << d_macro_basis[op][a] << " = " << eq[a] << std::endl;
+                }
+              }
+              Trace("macros-eq") << " for ";
+              for( size_t a=0; a<fvs.size(); a++ ){
+                if( solved[ fvs[a] ].isNull() ){
+                  Trace("macros-eq") << fvs[a] << " ";
+                }
+              }
+              Trace("macros-eq") << std::endl;
+              //DO_THIS
+
+
+              vars.clear();
+              subs.clear();
+              if( getSubstitution( fvs, solved, vars, subs, true ) ){
+                //build condition
+                std::vector< Node > conds;
+                if( !n_cond.isNull() ){
+                  //must apply substitution obtained from solving system of equations to original condition
+                  n_cond = n_cond.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                  conds.push_back( n_cond );
+                }
+                for( size_t a=0; a<eq.size(); a++ ){
+                  //collect conditions based on solving argument's system of equations
+                  if( d_macro_basis[op][a]!=eq[a] ){
+                    conds.push_back( NodeManager::currentNM()->mkNode( eq[a].getType().isBoolean() ? IFF : EQUAL, d_macro_basis[op][a], eq[a] ) );
+                  }
+                }
+                //build the condition
+                if( !conds.empty() ){
+                  n_cond = conds.size()==1 ? conds[0] : NodeManager::currentNM()->mkNode( AND, conds );
+                }
+                //apply the substitution to the
+                n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+                //now see if definition is consistent with others
+                if( isConsistentDefinition( op, n_cond, n_def ) ){
+                  //must clear if it is a base definition
+                  if( n_cond.isNull() ){
+                    d_macro_def_cases[ op ].clear();
+                  }
+                  d_macro_def_cases[ op ].push_back( std::pair< Node, Node >( n_cond, n_def ) );
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+Node QuantifierMacros::simplify( Node n ){
+  Trace("macros-debug") << "simplify " << n << std::endl;
+  std::vector< Node > children;
+  bool childChanged = false;
+  for( size_t i=0; i<n.getNumChildren(); i++ ){
+    Node nn = simplify( n[i] );
+    children.push_back( nn );
+    childChanged = childChanged || nn!=n[i];
+  }
+  if( n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
+      //do subsitutition
+      Node ret = d_macro_defs[op];
+      ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );
+      return ret;
+    }
+  }
+  if( childChanged ){
+    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+      children.insert( children.begin(), n.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), children );
+  }else{
+    return n;
+  }
+}
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index b1fbb3e68..f4e58665d 100755
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -1,62 +1,62 @@
-/*********************                                                        */

-/*! \file macros.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-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Pre-process step for detecting quantifier macro definitions

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__QUANTIFIERS_MACROS_H

-#define __CVC4__QUANTIFIERS_MACROS_H

-

-#include <iostream>

-#include <string>

-#include <vector>

-#include <map>

-#include "expr/node.h"

-#include "expr/type_node.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-class QuantifierMacros{

-private:

-  void process( Node n, bool pol, std::vector< Node >& args, Node f );

-  bool contains( Node n, Node n_s );

-  bool containsBadOp( Node n, Node n_op );

-  bool isMacroLiteral( Node n, bool pol );

-  void getMacroCandidates( Node n, std::vector< Node >& candidates );

-  Node solveInEquality( Node n, Node lit );

-  bool isConsistentDefinition( Node op, Node cond, Node def );

-  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );

-  bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,

-                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );

-  //map from operators to macro basis terms

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

-  //map from operators to map from conditions to definition cases

-  std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases;

-  //map from operators to macro definition

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

-private:

-  Node simplify( Node n );

-public:

-  QuantifierMacros(){}

-  ~QuantifierMacros(){}

-

-  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );

-};

-

-}

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file macros.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-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_MACROS_H
+#define __CVC4__QUANTIFIERS_MACROS_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifierMacros{
+private:
+  void process( Node n, bool pol, std::vector< Node >& args, Node f );
+  bool contains( Node n, Node n_s );
+  bool containsBadOp( Node n, Node n_op );
+  bool isMacroLiteral( Node n, bool pol );
+  void getMacroCandidates( Node n, std::vector< Node >& candidates );
+  Node solveInEquality( Node n, Node lit );
+  bool isConsistentDefinition( Node op, Node cond, Node def );
+  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly );
+  bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
+                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
+  //map from operators to macro basis terms
+  std::map< Node, std::vector< Node > > d_macro_basis;
+  //map from operators to map from conditions to definition cases
+  std::map< Node, std::vector< std::pair< Node, Node > > > d_macro_def_cases;
+  //map from operators to macro definition
+  std::map< Node, Node > d_macro_defs;
+private:
+  Node simplify( Node n );
+public:
+  QuantifierMacros(){}
+  ~QuantifierMacros(){}
+
+  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index d1b0e0fea..a78cd5612 100755
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -1,145 +1,145 @@
-/*********************                                                        */

-/*! \file quant_util.cpp

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: bobot, mdeters

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief Implementation of quantifier utilities

- **/

-

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

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

-

-void QuantRelevance::registerQuantifier( Node f ){

-  //compute symbols in f

-  std::vector< Node > syms;

-  computeSymbols( f[1], syms );

-  d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );

-  //set initial relevance

-  int minRelevance = -1;

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

-    d_syms_quants[ syms[i] ].push_back( f );

-    int r = getRelevance( syms[i] );

-    if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){

-      minRelevance = r;

-    }

-  }

-  if( minRelevance!=-1 ){

-    setRelevance( f, minRelevance+1 );

-  }

-}

-

-

-/** compute symbols */

-void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){

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

-    Node op = n.getOperator();

-    if( std::find( syms.begin(), syms.end(), op )==syms.end() ){

-      syms.push_back( op );

-    }

-  }

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

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

-      computeSymbols( n[i], syms );

-    }

-  }

-}

-

-/** set relevance */

-void QuantRelevance::setRelevance( Node s, int r ){

-  if( d_computeRel ){

-    int rOld = getRelevance( s );

-    if( rOld==-1 || r<rOld ){

-      d_relevance[s] = r;

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

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

-          setRelevance( d_syms[s][i], r );

-        }

-      }else{

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

-          setRelevance( d_syms_quants[s][i], r+1 );

-        }

-      }

-    }

-  }

-}

-

-

-QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){

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

-  computePhaseReqs( n, false, phaseReqs2 );

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

-    if( it->second==1 ){

-      d_phase_reqs[ it->first ] = true;

-    }else if( it->second==-1 ){

-      d_phase_reqs[ it->first ] = false;

-    }

-  }

-  Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;

-  //now, compute if any patterns are equality required

-  if( computeEq ){

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

-      Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;

-      if( it->first.getKind()==EQUAL ){

-        if( it->first[0].hasAttribute(InstConstantAttribute()) ){

-          if( !it->first[1].hasAttribute(InstConstantAttribute()) ){

-            d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];

-            d_phase_reqs_equality[ it->first[0] ] = it->second;

-            Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;

-          }

-        }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){

-          d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];

-          d_phase_reqs_equality[ it->first[1] ] = it->second;

-          Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;

-        }

-      }

-    }

-  }

-}

-

-void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){

-  bool newReqPol = false;

-  bool newPolarity;

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

-    newReqPol = true;

-    newPolarity = !polarity;

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

-    if( !polarity ){

-      newReqPol = true;

-      newPolarity = false;

-    }

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

-    if( polarity ){

-      newReqPol = true;

-      newPolarity = true;

-    }

-  }else{

-    int val = polarity ? 1 : -1;

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

-      phaseReqs[n] = val;

-    }else if( val!=phaseReqs[n] ){

-      phaseReqs[n] = 0;

-    }

-  }

-  if( newReqPol ){

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

-      if( n.getKind()==IMPLIES && i==0 ){

-        computePhaseReqs( n[i], !newPolarity, phaseReqs );

-      }else{

-        computePhaseReqs( n[i], newPolarity, phaseReqs );

-      }

-    }

-  }

-}

+/*********************                                                        */
+/*! \file quant_util.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: bobot, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of quantifier utilities
+ **/
+
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/inst_match.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;
+
+void QuantRelevance::registerQuantifier( Node f ){
+  //compute symbols in f
+  std::vector< Node > syms;
+  computeSymbols( f[1], syms );
+  d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );
+  //set initial relevance
+  int minRelevance = -1;
+  for( int i=0; i<(int)syms.size(); i++ ){
+    d_syms_quants[ syms[i] ].push_back( f );
+    int r = getRelevance( syms[i] );
+    if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){
+      minRelevance = r;
+    }
+  }
+  if( minRelevance!=-1 ){
+    setRelevance( f, minRelevance+1 );
+  }
+}
+
+
+/** compute symbols */
+void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){
+  if( n.getKind()==APPLY_UF ){
+    Node op = n.getOperator();
+    if( std::find( syms.begin(), syms.end(), op )==syms.end() ){
+      syms.push_back( op );
+    }
+  }
+  if( n.getKind()!=FORALL ){
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      computeSymbols( n[i], syms );
+    }
+  }
+}
+
+/** set relevance */
+void QuantRelevance::setRelevance( Node s, int r ){
+  if( d_computeRel ){
+    int rOld = getRelevance( s );
+    if( rOld==-1 || r<rOld ){
+      d_relevance[s] = r;
+      if( s.getKind()==FORALL ){
+        for( int i=0; i<(int)d_syms[s].size(); i++ ){
+          setRelevance( d_syms[s][i], r );
+        }
+      }else{
+        for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
+          setRelevance( d_syms_quants[s][i], r+1 );
+        }
+      }
+    }
+  }
+}
+
+
+QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
+  std::map< Node, int > phaseReqs2;
+  computePhaseReqs( n, false, phaseReqs2 );
+  for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){
+    if( it->second==1 ){
+      d_phase_reqs[ it->first ] = true;
+    }else if( it->second==-1 ){
+      d_phase_reqs[ it->first ] = false;
+    }
+  }
+  Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;
+  //now, compute if any patterns are equality required
+  if( computeEq ){
+    for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){
+      Debug("inst-engine-phase-req") << "   " << it->first << " -> " << it->second << std::endl;
+      if( it->first.getKind()==EQUAL ){
+        if( it->first[0].hasAttribute(InstConstantAttribute()) ){
+          if( !it->first[1].hasAttribute(InstConstantAttribute()) ){
+            d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];
+            d_phase_reqs_equality[ it->first[0] ] = it->second;
+            Debug("inst-engine-phase-req") << "      " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;
+          }
+        }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){
+          d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];
+          d_phase_reqs_equality[ it->first[1] ] = it->second;
+          Debug("inst-engine-phase-req") << "      " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;
+        }
+      }
+    }
+  }
+}
+
+void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){
+  bool newReqPol = false;
+  bool newPolarity;
+  if( n.getKind()==NOT ){
+    newReqPol = true;
+    newPolarity = !polarity;
+  }else if( n.getKind()==OR || n.getKind()==IMPLIES ){
+    if( !polarity ){
+      newReqPol = true;
+      newPolarity = false;
+    }
+  }else if( n.getKind()==AND ){
+    if( polarity ){
+      newReqPol = true;
+      newPolarity = true;
+    }
+  }else{
+    int val = polarity ? 1 : -1;
+    if( phaseReqs.find( n )==phaseReqs.end() ){
+      phaseReqs[n] = val;
+    }else if( val!=phaseReqs[n] ){
+      phaseReqs[n] = 0;
+    }
+  }
+  if( newReqPol ){
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( n.getKind()==IMPLIES && i==0 ){
+        computePhaseReqs( n[i], !newPolarity, phaseReqs );
+      }else{
+        computePhaseReqs( n[i], newPolarity, phaseReqs );
+      }
+    }
+  }
+}
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index bb6855c47..1daaf3ea1 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -1,99 +1,99 @@
-/*********************                                                        */

-/*! \file quant_util.h

- ** \verbatim

- ** Original author: ajreynol

- ** Major contributors: none

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

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

- ** Copyright (c) 2009-2012  New York University and The University of Iowa

- ** See the file COPYING in the top-level source directory for licensing

- ** information.\endverbatim

- **

- ** \brief quantifier util

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY__QUANT_UTIL_H

-#define __CVC4__THEORY__QUANT_UTIL_H

-

-#include "theory/theory.h"

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

-

-#include <ext/hash_set>

-#include <iostream>

-#include <map>

-

-namespace CVC4 {

-namespace theory {

-

-

-class QuantRelevance

-{

-private:

-  /** for computing relavance */

-  bool d_computeRel;

-  /** map from quantifiers to symbols they contain */

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

-  /** map from symbols to quantifiers */

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

-  /** relevance for quantifiers and symbols */

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

-  /** compute symbols */

-  void computeSymbols( Node n, std::vector< Node >& syms );

-public:

-  QuantRelevance( bool cr ) : d_computeRel( cr ){}

-  ~QuantRelevance(){}

-  /** register quantifier */

-  void registerQuantifier( Node f );

-  /** set relevance */

-  void setRelevance( Node s, int r );

-  /** get relevance */

-  int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }

-  /** get number of quantifiers for symbol s */

-  int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }

-};

-

-class QuantPhaseReq

-{

-private:

-  /** helper functions compute phase requirements */

-  void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );

-public:

-  QuantPhaseReq( Node n, bool computeEq = false );

-  ~QuantPhaseReq(){}

-  /** is phase required */

-  bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }

-  /** get phase requirement */

-  bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }

-  /** phase requirements for each quantifier for each instantiation literal */

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

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

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

-};

-

-

-class EqualityQuery {

-public:

-  EqualityQuery(){}

-  virtual ~EqualityQuery(){};

-  /** reset */

-  virtual void reset() = 0;

-  /** contains term */

-  virtual bool hasTerm( Node a ) = 0;

-  /** get the representative of the equivalence class of a */

-  virtual Node getRepresentative( Node a ) = 0;

-  /** returns true if a and b are equal in the current context */

-  virtual bool areEqual( Node a, Node b ) = 0;

-  /** returns true is a and b are disequal in the current context */

-  virtual bool areDisequal( Node a, Node b ) = 0;

-  /** get the equality engine associated with this query */

-  virtual eq::EqualityEngine* getEngine() = 0;

-  /** get the equivalence class of a */

-  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;

-};/* class EqualityQuery */

-

-}

-}

-

-#endif

+/*********************                                                        */
+/*! \file quant_util.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters, bobot
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief quantifier util
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANT_UTIL_H
+#define __CVC4__THEORY__QUANT_UTIL_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+
+
+class QuantRelevance
+{
+private:
+  /** for computing relavance */
+  bool d_computeRel;
+  /** map from quantifiers to symbols they contain */
+  std::map< Node, std::vector< Node > > d_syms;
+  /** map from symbols to quantifiers */
+  std::map< Node, std::vector< Node > > d_syms_quants;
+  /** relevance for quantifiers and symbols */
+  std::map< Node, int > d_relevance;
+  /** compute symbols */
+  void computeSymbols( Node n, std::vector< Node >& syms );
+public:
+  QuantRelevance( bool cr ) : d_computeRel( cr ){}
+  ~QuantRelevance(){}
+  /** register quantifier */
+  void registerQuantifier( Node f );
+  /** set relevance */
+  void setRelevance( Node s, int r );
+  /** get relevance */
+  int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }
+  /** get number of quantifiers for symbol s */
+  int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }
+};
+
+class QuantPhaseReq
+{
+private:
+  /** helper functions compute phase requirements */
+  void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
+public:
+  QuantPhaseReq( Node n, bool computeEq = false );
+  ~QuantPhaseReq(){}
+  /** is phase required */
+  bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
+  /** get phase requirement */
+  bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }
+  /** phase requirements for each quantifier for each instantiation literal */
+  std::map< Node, bool > d_phase_reqs;
+  std::map< Node, bool > d_phase_reqs_equality;
+  std::map< Node, Node > d_phase_reqs_equality_term;
+};
+
+
+class EqualityQuery {
+public:
+  EqualityQuery(){}
+  virtual ~EqualityQuery(){};
+  /** reset */
+  virtual void reset() = 0;
+  /** contains term */
+  virtual bool hasTerm( Node a ) = 0;
+  /** get the representative of the equivalence class of a */
+  virtual Node getRepresentative( Node a ) = 0;
+  /** returns true if a and b are equal in the current context */
+  virtual bool areEqual( Node a, Node b ) = 0;
+  /** returns true is a and b are disequal in the current context */
+  virtual bool areDisequal( Node a, Node b ) = 0;
+  /** get the equality engine associated with this query */
+  virtual eq::EqualityEngine* getEngine() = 0;
+  /** get the equivalence class of a */
+  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+};/* class EqualityQuery */
+
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 2f6dc47db..108c09c87 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -9,33 +9,33 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Implementation of QuantifiersAttributes class

- **/

-

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

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

-

-using namespace std;

-using namespace CVC4;

-using namespace CVC4::kind;

-using namespace CVC4::context;

-using namespace CVC4::theory;

-using namespace CVC4::theory::quantifiers;

-

-void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){

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

-    if( attr=="axiom" ){

-      Trace("quant-attr") << "Set axiom " << n << std::endl;

-      AxiomAttribute aa;

-      n.setAttribute( aa, true );

-    }else if( attr=="conjecture" ){

-      Trace("quant-attr") << "Set conjecture " << n << std::endl;

-      ConjectureAttribute ca;

-      n.setAttribute( ca, true );

-    }

-  }else{

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

-      setUserAttribute( attr, n[i] );

-    }

-  }

-}

+ ** \brief Implementation of QuantifiersAttributes class
+ **/
+
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
+  if( n.getKind()==FORALL ){
+    if( attr=="axiom" ){
+      Trace("quant-attr") << "Set axiom " << n << std::endl;
+      AxiomAttribute aa;
+      n.setAttribute( aa, true );
+    }else if( attr=="conjecture" ){
+      Trace("quant-attr") << "Set conjecture " << n << std::endl;
+      ConjectureAttribute ca;
+      n.setAttribute( ca, true );
+    }
+  }else{
+    for( size_t i=0; i<n.getNumChildren(); i++ ){
+      setUserAttribute( attr, n[i] );
+    }
+  }
+}
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 88bac8bc9..f5a8a749a 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -9,43 +9,43 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Attributes for the theory quantifiers

- **

- ** Attributes for the theory quantifiers.

- **/

-

-#include "cvc4_private.h"

-

-#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H

-#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H

-

-#include "theory/rewriter.h"

-#include "theory/quantifiers_engine.h"

-

-namespace CVC4 {

-namespace theory {

-namespace quantifiers {

-

-/** Attribute true for quantifiers that are axioms */

-struct AxiomAttributeId {};

-typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;

-

-/** Attribute true for quantifiers that are conjecture */

-struct ConjectureAttributeId {};

-typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;

-

-struct QuantifiersAttributes

-{

-  /** set user attribute

-    *   This function will apply a custom set of attributes to all top-level universal

-    *   quantifiers contained in n

-    */

-  static void setUserAttribute( const std::string& attr, Node n );

-};

-

-

-}

-}

-}

-

-#endif

+ ** \brief Attributes for the theory quantifiers
+ **
+ ** Attributes for the theory quantifiers.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+
+#include "theory/rewriter.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Attribute true for quantifiers that are axioms */
+struct AxiomAttributeId {};
+typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
+
+/** Attribute true for quantifiers that are conjecture */
+struct ConjectureAttributeId {};
+typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
+
+struct QuantifiersAttributes
+{
+  /** set user attribute
+    *   This function will apply a custom set of attributes to all top-level universal
+    *   quantifiers contained in n
+    */
+  static void setUserAttribute( const std::string& attr, Node n );
+};
+
+
+}
+}
+}
+
+#endif