Module to infer alpha equivalence of quantified formulas. Minor clean up of options.

10 files changed, 378 insertions, 320 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
new file mode 100755
index 000000000..e4dcccdff
--- /dev/null
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file alpha_equivalence.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Alpha equivalence checking
+ **
+ **/
+
+#include "theory/quantifiers/alpha_equivalence.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+struct sortTypeOrder {
+  TermDb* d_tdb;
+  bool operator() (TypeNode i, TypeNode j) {
+    return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
+  }
+};
+
+bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+  if( tt.size()==arg_index.size()+1 ){
+    Node t = tt.back();
+    Node op = t.hasOperator() ? t.getOperator() : t;
+    arg_index.push_back( 0 );
+    Trace("aeq-debug") << op << " ";
+    return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index );
+  }else if( tt.empty() ){
+    //we are finished
+    Trace("aeq-debug") << std::endl;
+    if( d_quant.isNull() ){
+      d_quant = q;
+      return true;
+    }else{
+      //lemma ( q <=> d_quant )
+      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+      Trace("alpha-eq") << "  " << q << std::endl;
+      Trace("alpha-eq") << "  " << d_quant << std::endl;
+      qe->getOutputChannel().lemma( q.iffNode( d_quant ) );
+      return false;
+    }
+  }else{
+    Node t = tt.back();
+    int i = arg_index.back();
+    if( i==(int)t.getNumChildren() ){
+      tt.pop_back();
+      arg_index.pop_back();
+    }else{
+      tt.push_back( t[i] );
+      arg_index[arg_index.size()-1]++;
+    }
+    return registerNode( qe, q, tt, arg_index );
+  }
+}
+
+bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
+  if( index==(int)typs.size() ){
+    std::vector< Node > tt;
+    std::vector< int > arg_index;
+    tt.push_back( t );
+    Trace("aeq-debug") << " : ";
+    return d_data.registerNode( qe, q, tt, arg_index );
+  }else{
+    TypeNode curr = typs[index];
+    Assert( typ_count.find( curr )!=typ_count.end() );
+    Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
+    return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 );
+  }
+}
+
+bool AlphaEquivalence::registerQuantifier( Node q ) {
+  Assert( q.getKind()==FORALL );
+  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
+  //construct canonical quantified formula
+  Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true );
+  Trace("aeq") << "  canonical form: " << t << std::endl;
+  //compute variable type counts
+  std::map< TypeNode, int > typ_count;
+  std::vector< TypeNode > typs;
+  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+    TypeNode tn = q[0][i].getType();
+    typ_count[tn]++;
+    if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
+      typs.push_back( tn );
+    }
+  }
+  sortTypeOrder sto;
+  sto.d_tdb = d_qe->getTermDatabase();
+  std::sort( typs.begin(), typs.end(), sto );
+  Trace("aeq-debug") << "  ";
+  bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count );
+  Trace("aeq") << "  ...result : " << ret << std::endl;
+  return ret;
+}
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
new file mode 100755
index 000000000..fa2109ccc
--- /dev/null
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file alpha_equivalence.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Alpha equivalence checking
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__ALPHA_EQUIVALENCE_H
+#define __CVC4__ALPHA_EQUIVALENCE_H
+
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class AlphaEquivalenceNode {
+public:
+  std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
+  Node d_quant;
+  bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+};
+
+class AlphaEquivalenceTypeNode {
+public:
+  std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
+  AlphaEquivalenceNode d_data;
+  bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
+};
+
+class AlphaEquivalence {
+private:
+  QuantifiersEngine* d_qe;
+  //per # of variables per type
+  AlphaEquivalenceTypeNode d_ae_typ_trie;
+public:
+  AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
+  ~AlphaEquivalence(){}
+
+  bool registerQuantifier( Node q );
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 845e20795..0429abac9 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -309,7 +309,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
   }
   Node sol0 = Rewriter::rewrite( sol );
   Trace("csi-sol") << "now : " << sol0 << std::endl;
-  
+
   Node curr_sol = sol0;
   Node prev_sol;
   do{
@@ -359,7 +359,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){
       curr_sol = sol4;
     }
   }while( curr_sol!=prev_sol );
-  
+
   return curr_sol;
 }
 
@@ -726,7 +726,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
       if( karg!=-1 ){
         //collect the children of min_t
         std::vector< Node > tchildren;
-        if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
+        if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){
           tchildren.push_back( min_t[0] );
           std::vector< Node > rem_children;
           for( unsigned i=1; i<min_t.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 4167c3ad9..fdb64f6b0 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -281,61 +281,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
 }
 
 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
-  Assert( !tn.isNull() );
-  while( d_free_var[tn].size()<=i ){
-    std::stringstream oss;
-    oss << tn;
-    std::string typ_name = oss.str();
-    while( typ_name[0]=='(' ){
-      typ_name.erase( typ_name.begin() );
-    }
-    std::stringstream os;
-    os << typ_name[0] << i;
-    Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
-    d_free_var_num[x] = d_free_var[tn].size();
-    d_free_var[tn].push_back( x );
-  }
-  return d_free_var[tn][i];
-}
-
-
-
-Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) {
-  if( n.getKind()==BOUND_VARIABLE ){
-    std::map< TNode, TNode >::iterator it = subs.find( n );
-    if( it==subs.end() ){
-      TypeNode tn = n.getType();
-      //allocate variable
-      unsigned vn = var_count[tn];
-      var_count[tn]++;
-      subs[n] = getFreeVar( tn, vn );
-      return subs[n];
-    }else{
-      return it->second;
-    }
-  }else{
-    std::vector< Node > children;
-    if( n.getKind()!=EQUAL ){
-      if( n.hasOperator() ){
-        TNode op = n.getOperator();
-        if( !d_tge.isRelevantFunc( op ) ){
-          return Node::null();
-        }
-        children.push_back( op );
-      }else{
-        return Node::null();
-      }
-    }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node cn = getCanonicalTerm( n[i], var_count, subs );
-      if( cn.isNull() ){
-        return Node::null();
-      }else{
-        children.push_back( cn );
-      }
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }
+  return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i );
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
@@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
             TNode nr = q[1][r==0 ? 1 : 0];
             Node eq = nl.eqNode( nr );
             if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){
-              //must make it canonical
-              std::map< TypeNode, unsigned > var_count;
-              std::map< TNode, TNode > subs;
-              Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
-              eq = getCanonicalTerm( eq, var_count, subs );
+              //check if it contains only relevant functions
+              if( d_tge.isRelevantTerm( eq ) ){
+                //make it canonical
+                Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
+                eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq );
+              }else{
+                eq = Node::null();
+              }
             }
             if( !eq.isNull() ){
               if( r==0 ){
@@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
                 typ_to_subs_index[it->first] = sum;
                 sum += it->second;
                 for( unsigned i=0; i<it->second; i++ ){
-                  gsubs_vars.push_back( getFreeVar( it->first, i ) );
+                  gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) );
                 }
               }
             }
@@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map<
       }else{
         //check for max/min
         TypeNode tn = pat.getType();
-        unsigned vn = d_free_var_num[pat];
+        unsigned vn = pat.getAttribute(InstVarNumAttribute());
         std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn );
         if( it!=mnvn.end() ){
           if( vn<it->second ){
@@ -2012,6 +1961,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){
 bool TermGenEnv::isRelevantFunc( Node f ) {
   return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end();
 }
+
+bool TermGenEnv::isRelevantTerm( Node t ) {
+  if( t.getKind()!=BOUND_VARIABLE ){
+    if( t.getKind()!=EQUAL ){
+      if( t.hasOperator() ){
+        TNode op = t.getOperator();
+        if( !isRelevantFunc( op ) ){
+          return false;
+        }
+      }else{
+        return false;
+      }
+    }
+    for( unsigned i=0; i<t.getNumChildren(); i++ ){
+      if( !isRelevantTerm( t[i] ) ){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+
 TermDb * TermGenEnv::getTermDatabase() {
   return d_cg->getTermDatabase();
 }
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 6f99777f4..3aa932296 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -171,6 +171,7 @@ public:
   bool considerCurrentTermCanon( unsigned tg_id );
   void changeContext( bool add );
   bool isRelevantFunc( Node f );
+  bool isRelevantTerm( Node t );
   //carry
   TermDb * getTermDatabase();
   Node getGroundEqc( TNode r );
@@ -307,14 +308,8 @@ private:  //information regarding the conjectures
   /** conjecture index */
   TheoremIndex d_thm_index;
 private:  //free variable list
-  //free variables
-  std::map< TypeNode, std::vector< Node > > d_free_var;
-  //map from free variable to FV#
-  std::map< TNode, unsigned > d_free_var_num;
   // get canonical free variable #i of type tn
   Node getFreeVar( TypeNode tn, unsigned i );
-  // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );
 private:  //information regarding the terms
   //relevant patterns (the LHS's)
   std::map< TypeNode, std::vector< Node > > d_rel_patterns;
diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp
deleted file mode 100644
index 23e18bb02..000000000
--- a/src/theory/quantifiers/first_order_reasoning.cpp
+++ /dev/null
@@ -1,175 +0,0 @@
-/*********************                                                        */
-/*! \file first_order_reasoning.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief first order reasoning module
- **
- **/
-
-#include <vector>
-
-#include "theory/quantifiers/first_order_reasoning.h"
-#include "theory/rewriter.h"
-#include "proof/proof_manager.h"
-
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
-
-
-void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
-  if( n.getKind()==FORALL ){
-    collectLits( n[1], lits );
-  }else if( n.getKind()==OR ){
-    for(unsigned j=0; j<n.getNumChildren(); j++) {
-      collectLits(n[j], lits );
-    }
-  }else{
-    lits.push_back( n );
-  }
-}
-
-void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
-  for( unsigned i=0; i<assertions.size(); i++) {
-    Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
-  }
-
-  //process all assertions
-  int num_processed;
-  int num_true = 0;
-  int num_rounds = 0;
-  do {
-    num_processed = 0;
-    for( unsigned i=0; i<assertions.size(); i++ ){
-      if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
-        std::vector< Node > fo_lits;
-        collectLits( assertions[i], fo_lits );
-        Node unitLit = process( assertions[i], fo_lits );
-        if( !unitLit.isNull() ){
-          Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
-          bool pol = unitLit.getKind()!=NOT;
-          unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
-          if( unitLit.getKind()==EQUAL ){
-
-          }else if( unitLit.getKind()==APPLY_UF ){
-            //make sure all are unique vars;
-            bool success = true;
-            std::vector< Node > unique_vars;
-            for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
-              if( unitLit[j].getKind()==BOUND_VARIABLE ){
-                if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
-                  unique_vars.push_back( unitLit[j] );
-                }else{
-                  success = false;
-                  break;
-                }
-              }else{
-                success = false;
-                break;
-              }
-            }
-            if( success ){
-              d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
-              Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
-              Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
-              d_assertion_true[assertions[i]] = true;
-              num_processed++;
-            }
-          }else if( unitLit.getKind()==VARIABLE ){
-            d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
-            Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
-            Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
-            d_assertion_true[assertions[i]] = true;
-            num_processed++;
-          }
-        }
-        if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
-          num_true++;
-        }
-      }
-    }
-    num_rounds++;
-  }while( num_processed>0 );
-  Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
-  for( unsigned i=0; i<assertions.size(); i++ ){
-    Node curr = simplify( assertions[i] );
-    if( curr!=assertions[i] ){
-      curr = Rewriter::rewrite( curr );
-      PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
-      assertions[i] = curr;
-    }
-  }
-}
-
-Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
-  int index = -1;
-  for( unsigned i=0; i<lits.size(); i++) {
-    bool pol = lits[i].getKind()!=NOT;
-    Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
-    Node litDef;
-    if( n.getKind()==APPLY_UF ){
-      if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
-        litDef = d_const_def[n.getOperator()];
-      }
-    }else if( n.getKind()==VARIABLE ){
-      if( d_const_def.find(n)!=d_const_def.end() ){
-        litDef = d_const_def[n];
-      }
-    }
-    if( !litDef.isNull() ){
-      Node poln = NodeManager::currentNM()->mkConst( pol );
-      if( litDef==poln ){
-        Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
-        d_assertion_true[a] = true;
-        return Node::null();
-      }
-    }
-    if( litDef.isNull() ){
-      if( index==-1 ){
-        //store undefined index
-        index = i;
-      }else{
-        //two undefined, return null
-        return Node::null();
-      }
-    }
-  }
-  if( index!=-1 ){
-    return lits[index];
-  }else{
-    return Node::null();
-  }
-}
-
-Node FirstOrderPropagation::simplify( Node n ) {
-  if( n.getKind()==VARIABLE ){
-    if( d_const_def.find(n)!=d_const_def.end() ){
-      return d_const_def[n];
-    }
-  }else if( n.getKind()==APPLY_UF ){
-    if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
-      return d_const_def[n.getOperator()];
-    }
-  }
-  if( n.getNumChildren()==0 ){
-    return n;
-  }else{
-    std::vector< Node > children;
-    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-      children.push_back( n.getOperator() );
-    }
-    for(unsigned i=0; i<n.getNumChildren(); i++) {
-      children.push_back( simplify(n[i]) );
-    }
-    return NodeManager::currentNM()->mkNode( n.getKind(), children );
-  }
-}
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h
deleted file mode 100644
index 100cf34b6..000000000
--- a/src/theory/quantifiers/first_order_reasoning.h
+++ /dev/null
@@ -1,49 +0,0 @@
-/*********************                                                        */
-/*! \file first_order_reasoning.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  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 first-order reasoning
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__FIRST_ORDER_REASONING_H
-#define __CVC4__FIRST_ORDER_REASONING_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 FirstOrderPropagation {
-private:
-  std::map< Node, Node > d_const_def;
-  std::map< Node, bool > d_assertion_true;
-  Node process(Node a, std::vector< Node > & lits);
-  void collectLits( Node n, std::vector<Node> & lits );
-  Node simplify( Node n );
-public:
-  FirstOrderPropagation(){}
-  ~FirstOrderPropagation(){}
-
-  void simplify( std::vector< Node >& assertions );
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2af66e60a..e34465d9b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -54,10 +54,7 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
 # Whether to perform quantifier macro expansion
 option macrosQuant --macros-quant bool :default false
  perform quantifiers macro expansions
-# Whether to perform first-order propagation
-option foPropQuant --fo-prop-quant bool :default false
- perform first-order propagation on quantifiers
-
+ 
 #### E-matching options
  
 option eMatching --e-matching bool :read-write :default true
@@ -227,7 +224,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
 option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
   
-# older implementation
+# approach applied to general quantified formulas
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 option cbqi2 --cbqi2 bool :read-write :default false
@@ -246,4 +243,9 @@ option ltePartialInst --lte-partial-inst bool :default false
 option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
   treat arguments of inst closure as restricted terms for instantiation
  
+### reduction options
+
+option quantAlphaEquiv --quant-alpha-equiv bool :default false
+  infer alpha equivalence between quantified formulas
+ 
 endmodule
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 20d622122..84cb63617 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -77,7 +77,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
   }
 }
 
-TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) {
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   if( options::ceGuidedInst() ){
@@ -1154,6 +1154,133 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){
   nodes.insert( nodes.begin(), temp.begin(), temp.end() );
 }
 
+int TermDb::getIdForOperator( Node op ) {
+  std::map< Node, int >::iterator it = d_op_id.find( op );
+  if( it==d_op_id.end() ){
+    d_op_id[op] = d_op_id_count;
+    d_op_id_count++;
+    return d_op_id[op];
+  }else{
+    return it->second;
+  }
+}
+
+int TermDb::getIdForType( TypeNode t ) {
+  std::map< TypeNode, int >::iterator it = d_typ_id.find( t );
+  if( it==d_typ_id.end() ){
+    d_typ_id[t] = d_typ_id_count;
+    d_typ_id_count++;
+    return d_typ_id[t];
+  }else{
+    return it->second;
+  }
+}
+
+bool TermDb::getTermOrder( Node a, Node b ) {
+  if( a.getKind()==BOUND_VARIABLE ){
+    if( b.getKind()==BOUND_VARIABLE ){
+      return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute());
+    }else{
+      return true;
+    }
+  }else if( b.getKind()!=BOUND_VARIABLE ){
+    Node aop = a.hasOperator() ? a.getOperator() : a;
+    Node bop = b.hasOperator() ? b.getOperator() : b;
+    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
+    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
+    if( aop==bop ){
+      if( aop.getNumChildren()==bop.getNumChildren() ){
+        for( unsigned i=0; i<a.getNumChildren(); i++ ){
+          if( a[i]!=b[i] ){
+            //first distinct child determines the ordering
+            return getTermOrder( a[i], b[i] );
+          }
+        }
+      }else{
+        return aop.getNumChildren()<bop.getNumChildren();
+      }
+    }else{
+      return getIdForOperator( aop )<getIdForOperator( bop );
+    }
+  }
+  return false;
+}
+
+
+
+Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
+  Assert( !tn.isNull() );
+  while( d_cn_free_var[tn].size()<=i ){
+    std::stringstream oss;
+    oss << tn;
+    std::string typ_name = oss.str();
+    while( typ_name[0]=='(' ){
+      typ_name.erase( typ_name.begin() );
+    }
+    std::stringstream os;
+    os << typ_name[0] << i;
+    Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn );
+    InstVarNumAttribute ivna;
+    x.setAttribute(ivna,d_cn_free_var[tn].size());
+    d_cn_free_var[tn].push_back( x );
+  }
+  return d_cn_free_var[tn][i];
+}
+
+struct sortTermOrder {
+  TermDb* d_tdb;
+  bool operator() (Node i, Node j) {
+    return d_tdb->getTermOrder( i, j );
+  }
+};
+
+//this function makes a canonical representation of a term (
+//  - orders variables left to right
+//  - if apply_torder, then sort direct subterms of commutative operators
+Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) {
+  if( n.getKind()==BOUND_VARIABLE ){
+    std::map< TNode, TNode >::iterator it = subs.find( n );
+    if( it==subs.end() ){
+      TypeNode tn = n.getType();
+      //allocate variable
+      unsigned vn = var_count[tn];
+      var_count[tn]++;
+      subs[n] = getCanonicalFreeVar( tn, vn );
+      return subs[n];
+    }else{
+      return it->second;
+    }
+  }else if( n.getNumChildren()>0 ){
+    //collect children
+    std::vector< Node > cchildren;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      cchildren.push_back( n[i] );
+    }
+    //if applicable, first sort by term order
+    if( apply_torder && isComm( n.getKind() ) ){
+      sortTermOrder sto;
+      sto.d_tdb = this;
+      std::sort( cchildren.begin(), cchildren.end(), sto );
+    }
+    //now make canonical
+    for( unsigned i=0; i<cchildren.size(); i++ ){
+      cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder );
+    }
+    if( n.hasOperator() ){
+      cchildren.insert( cchildren.begin(), n.getOperator() );
+    }
+    return NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
+  }else{
+    return n;
+  }
+}
+
+Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){
+  std::map< TypeNode, unsigned > var_count;
+  std::map< TNode, TNode > subs;
+  return getCanonicalTerm( n, var_count, subs, apply_torder );
+}
+
 bool TermDb::containsTerm( Node n, Node t ) {
   if( n==t ){
     return true;
@@ -1179,6 +1306,15 @@ Node TermDb::simpleNegate( Node n ){
   }
 }
 
+bool TermDb::isAssoc( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
+}
+
+bool TermDb::isComm( Kind k ) {
+  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
+         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
+}
 
 void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){
@@ -1440,7 +1576,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect
     return p==n;
   }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){
     //try both ways?
-    unsigned rmax = isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
+    unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1;
     std::vector< int > new_tmp;
     for( unsigned r=0; r<rmax; r++ ){
       bool success = true;
@@ -1666,7 +1802,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) {
                 int end = d_const_list[tn1].size()-d_const_list_pos[tn1];
                 for( int i=start; i>=end; --i ){
                   Node c1 = d_const_list[tn1][i];
-                  //only consider if smaller than c, and 
+                  //only consider if smaller than c, and
                   if( doCompare( c1, c, ck ) ){
                     Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 );
                     c2 = Rewriter::rewrite( c2 );
@@ -1768,16 +1904,6 @@ int TermDbSygus::getSygusTermSize( Node n ){
   }
 }
 
-bool TermDbSygus::isAssoc( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT;
-}
-
-bool TermDbSygus::isComm( Kind k ) {
-  return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF ||
-         k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR;
-}
-
 bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) {
   if( k==GT ){
     dk = LT;
@@ -2257,7 +2383,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         std::stringstream body_out;
         printSygusTerm( body_out, let_body, new_lvs );
         std::string body = body_out.str();
-        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ 
+        for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
           std::stringstream old_str;
           old_str << new_lvs[i];
           std::stringstream new_str;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 1ede29c12..e61552713 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -149,13 +149,13 @@ public:
   unsigned getNumGroundTerms( Node f );
   /** count number of non-redundant ground terms per operator */
   std::map< Node, int > d_op_nonred_count;
-  /** map from APPLY_UF operators to ground terms for that operator */
+  /** map from operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
   std::map< Node, Node > d_term_elig_eqc;
-  /** map from APPLY_UF functions to trie */
+  /** map from operators to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   std::map< Node, TermArgTrie > d_func_map_eqc_trie;
   /**mapping from UF terms to representatives of their arguments */
@@ -326,12 +326,42 @@ public:
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
 
+//for term ordering
+private:
+  /** operator id count */
+  int d_op_id_count;
+  /** map from operators to id */
+  std::map< Node, int > d_op_id;
+  /** type id count */
+  int d_typ_id_count;
+  /** map from type to id */
+  std::map< TypeNode, int > d_typ_id;
+  //free variables
+  std::map< TypeNode, std::vector< Node > > d_cn_free_var;
+  // get canonical term, return null if it contains a term apart from handled signature
+  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder );
+public:
+  /** get id for operator */
+  int getIdForOperator( Node op );
+  /** get id for type */
+  int getIdForType( TypeNode t );
+  /** get term order */
+  bool getTermOrder( Node a, Node b );
+  /** get canonical free variable #i of type tn */
+  Node getCanonicalFreeVar( TypeNode tn, unsigned i );
+  /** get canonical term */
+  Node getCanonicalTerm( TNode n, bool apply_torder = false );
+
 //general utilities
 public:
   /** simple check for contains term */
   static bool containsTerm( Node n, Node t );
   /** simple negate */
   static Node simpleNegate( Node n );
+  /** is assoc */
+  static bool isAssoc( Kind k );
+  /** is comm */
+  static bool isComm( Kind k );
 
 //for sygus
 private:
@@ -441,10 +471,6 @@ public:
   void registerSygusType( TypeNode tn );
   /** get arg type */
   TypeNode getArgType( const DatatypeConstructor& c, int i );
-  /** is assoc */
-  bool isAssoc( Kind k );
-  /** is comm */
-  bool isComm( Kind k );
   /** isAntisymmetric */
   bool isAntisymmetric( Kind k, Kind& dk );
   /** is idempotent arg */