Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.

6 files changed, 458 insertions, 25 deletions

diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 80011868b..be24d6c67 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -52,7 +52,10 @@ libquantifiers_la_SOURCES = \
 	rewrite_engine.h \
 	rewrite_engine.cpp \
 	relevant_domain.h \
-	relevant_domain.cpp
+	relevant_domain.cpp \
+	symmetry_breaking.h \
+	symmetry_breaking.cpp
+
 
 EXTRA_DIST = \
 	kinds \
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e1e2f96c2..30ff5242b 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -321,7 +321,7 @@ Node BoundedIntegers::getNextDecisionRequest() {
   return Node::null();
 }
 
-void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
+void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
   l = d_bounds[0][f][v];
   u = d_bounds[1][f][v];
   if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){
@@ -356,6 +356,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node
       l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
     }
   }
+}
+
+void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) {
+  getBounds( f, v, rsi, l, u );
   Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
   l = d_quantEngine->getModel()->getCurrentModelValue( l );
   u = d_quantEngine->getModel()->getCurrentModelValue( u );
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index 27d5b7569..3da938d31 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -115,6 +115,7 @@ public:
   int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; }
   Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
   Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+  void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u );
   bool isGroundRange(Node f, Node v);
 };
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index cdf697675..bf10369e6 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -840,14 +840,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Node i = fm->getUsedRepresentative( r[1] );
       Node e = fm->getUsedRepresentative( r[2] );
       d.addEntry(fm, mkArrayCond(i), e );
-      r = r[0];
+      r = fm->getRepresentative( r[0] );
     }
     Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
     bool success = false;
+    Node odefaultValue;
     if( r.getKind() == kind::STORE_ALL ){
       ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
-      Node defaultValue = Node::fromExpr(storeAll.getExpr());
-      defaultValue = fm->getUsedRepresentative( defaultValue, true );
+      odefaultValue = Node::fromExpr(storeAll.getExpr());
+      Node defaultValue = fm->getUsedRepresentative( odefaultValue, true );
       if( !defaultValue.isNull() ){
         d.addEntry(fm, defC, defaultValue);
         success = true;
@@ -855,6 +856,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     }
     if( !success ){
       Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
+      Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
       Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();
@@ -1191,29 +1193,35 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co
 }
 
 Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) {
-  if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
-    std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
-    exit( 0 );
-  }
-  Node b[2];
-  for( unsigned j=0; j<2; j++ ){
-    Node b1 = i1[j];
-    Node b2 = i2[j];
-    if( fm->isStar( b1 ) ){
-      b[j] = b2;
-    }else if( fm->isStar( b2 ) ){
-      b[j] = b1;
-    }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
-      b[j] = j==0 ? b2 : b1;
+  if( fm->isStar( i1 ) ){
+    return i2;
+  }else if( fm->isStar( i2 ) ){
+    return i1;
+  }else{
+    if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){
+      std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl;
+      exit( 0 );
+    }
+    Node b[2];
+    for( unsigned j=0; j<2; j++ ){
+      Node b1 = i1[j];
+      Node b2 = i2[j];
+      if( fm->isStar( b1 ) ){
+        b[j] = b2;
+      }else if( fm->isStar( b2 ) ){
+        b[j] = b1;
+      }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){
+        b[j] = j==0 ? b2 : b1;
+      }else{
+        b[j] = j==0 ? b1 : b2;
+      }
+    }
+    if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
+      return mk ? fm->getInterval( b[0], b[1] ) : i1;
     }else{
-      b[j] = j==0 ? b1 : b2;
+      return Node::null();
     }
   }
-  if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){
-    return mk ? fm->getInterval( b[0], b[1] ) : i1;
-  }else{
-    return Node::null();
-  }
 }
 
 Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
new file mode 100755
index 000000000..6a7baebb1
--- /dev/null
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -0,0 +1,296 @@
+/*********************                                                        */
+/*! \file symmetry_breaking.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 symmetry breaking module
+ **
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/symmetry_breaking.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "util/sort_inference.h"
+#include "theory/uf/theory_uf_strong_solver.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace std;
+
+namespace CVC4 {
+
+eq::EqualityEngine * SubsortSymmetryBreaker::getEqualityEngine() {
+  return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
+}
+
+bool SubsortSymmetryBreaker::areEqual( Node n1, Node n2 ) {
+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
+}
+
+bool SubsortSymmetryBreaker::areDisequal( Node n1, Node n2 ) {
+  return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
+}
+
+
+Node SubsortSymmetryBreaker::getRepresentative( Node n ) {
+  return getEqualityEngine()->getRepresentative( n );
+}
+
+uf::StrongSolverTheoryUF * SubsortSymmetryBreaker::getStrongSolver() {
+  return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getStrongSolver();
+}
+
+SubsortSymmetryBreaker::SubsortSymmetryBreaker(QuantifiersEngine* qe, context::Context* c) :
+d_qe(qe), d_conflict(c,false), d_max_dom_const_sort(c,0), d_has_dom_const_sort(c,false),
+d_fact_index(c,0), d_fact_list(c) {
+  d_true =  NodeManager::currentNM()->mkConst( true );
+}
+
+SubsortSymmetryBreaker::TypeInfo::TypeInfo( SubsortSymmetryBreaker * ssb, context::Context * c ) :
+d_ssb( ssb ), d_dom_constants( c ), d_first_active( c, 0 ){
+  d_dc_nodes = 0;
+}
+
+unsigned SubsortSymmetryBreaker::TypeInfo::getNumDomainConstants() {
+  if( d_nodes.empty() ){
+    return 0;
+  }else{
+    return 1 + d_dom_constants.size();
+  }
+}
+
+Node SubsortSymmetryBreaker::TypeInfo::getDomainConstant( int i ) {
+  if( i==0 ){
+    return d_nodes[0];
+  }else{
+    Assert( i<=(int)d_dom_constants.size() );
+    return d_dom_constants[i-1];
+  }
+}
+
+Node SubsortSymmetryBreaker::TypeInfo::getFirstActive() {
+  if( d_first_active.get()<(int)d_nodes.size() ){
+    Node fa = d_nodes[d_first_active.get()];
+    return d_ssb->getEqualityEngine()->hasTerm( fa ) ? fa : Node::null();
+  }else{
+    return Node::null();
+  }
+}
+
+SubsortSymmetryBreaker::TypeInfo * SubsortSymmetryBreaker::getTypeInfo( TypeNode tn, int sid ) {
+  if( d_type_info.find( sid )==d_type_info.end() ){
+    d_type_info[sid] = new TypeInfo( this, d_qe->getSatContext() );
+    d_sub_sorts[tn].push_back( sid );
+    d_sid_to_type[sid] = tn;
+  }
+  return d_type_info[sid];
+}
+
+void SubsortSymmetryBreaker::newEqClass( Node n ) {
+  Trace("sym-break-temp") << "New eq class " << n << std::endl;
+  if( !d_conflict ){
+    TypeNode tn = n.getType();
+    SortInference * si = d_qe->getTheoryEngine()->getSortInference();
+    if( si->isWellSorted( n ) ){
+      int sid = si->getSortId( n );
+      Trace("sym-break-debug") << "SSB: New eq class " << n << " : " << n.getType() << " : " << sid << std::endl;
+      TypeInfo * ti = getTypeInfo( tn, sid );
+      if( std::find( ti->d_nodes.begin(), ti->d_nodes.end(), n )==ti->d_nodes.end() ){
+        if( ti->d_nodes.empty() ){
+          //for first subsort, we add unit equality
+          if( d_sub_sorts[tn][0]!=sid ){
+            Trace("sym-break-temp") << "Do sym break unit with " << d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() << std::endl;
+            //add unit symmetry breaking lemma
+            Node eq = n.eqNode( d_type_info[d_sub_sorts[tn][0]]->getBaseConstant() );
+            eq = Rewriter::rewrite( eq );
+            d_unit_lemmas.push_back( eq );
+            Trace("sym-break-lemma") << "*** SymBreak : Unit lemma (" << sid << "==" << d_sub_sorts[tn][0] << ") : " << eq << std::endl;
+            d_pending_lemmas.push_back( eq );
+          }
+          Trace("sym-break-dc") << "* Set first domain constant : " << n << " for " << tn << " : " << sid << std::endl;
+          ti->d_dc_nodes++;
+        }
+        ti->d_node_to_id[n] = ti->d_nodes.size();
+        ti->d_nodes.push_back( n );
+      }
+      if( !d_has_dom_const_sort.get() ){
+        d_has_dom_const_sort.set( true );
+        d_max_dom_const_sort.set( sid );
+      }
+    }
+  }
+  Trace("sym-break-temp") << "Done new eq class" << std::endl;
+}
+
+
+
+void SubsortSymmetryBreaker::merge( Node a, Node b ) {
+
+}
+
+void SubsortSymmetryBreaker::assertDisequal( Node a, Node b ) {
+
+}
+
+void SubsortSymmetryBreaker::processFirstActive( TypeNode tn, int sid, int curr_card ){
+  TypeInfo * ti = getTypeInfo( tn, sid );
+  if( (int)ti->getNumDomainConstants()<curr_card ){
+    Trace("sym-break-dc-debug") << "Check for domain constants " << tn << " : " << sid << ", curr_card = " << curr_card << ", ";
+    Trace("sym-break-dc-debug") << "#domain constants = " << ti->getNumDomainConstants() << std::endl;
+    Node fa = ti->getFirstActive();
+    bool invalid = true;
+    while( invalid && !fa.isNull() && (int)ti->getNumDomainConstants()<curr_card ){
+      invalid = false;
+      unsigned deq = 0;
+      for( unsigned i=0; i<ti->getNumDomainConstants(); i++ ){
+        Node dc = ti->getDomainConstant( i );
+        if( areEqual( fa, dc ) ){
+          invalid = true;
+          break;
+        }else if( areDisequal( fa, dc ) ){
+          deq++;
+        }
+      }
+      if( deq==ti->getNumDomainConstants() ){
+        Trace("sym-break-dc") << "* Can infer domain constant #" << ti->getNumDomainConstants()+1;
+        Trace("sym-break-dc") << " : " << fa << " for " << tn << " : " << sid << std::endl;
+        //add to domain constants
+        ti->d_dom_constants.push_back( fa );
+        if( ti->d_node_to_id[fa]>ti->d_dc_nodes ){
+          Trace("sym-break-dc-debug") << "Swap nodes... " << ti->d_dc_nodes << " " << ti->d_node_to_id[fa] << " " << ti->d_nodes.size() << std::endl;
+          //swap
+          Node on = ti->d_nodes[ti->d_dc_nodes];
+          int id = ti->d_node_to_id[fa];
+
+          ti->d_nodes[ti->d_dc_nodes] = fa;
+          ti->d_nodes[id] = on;
+          ti->d_node_to_id[fa] = ti->d_dc_nodes;
+          ti->d_node_to_id[on] = id;
+        }
+        ti->d_dc_nodes++;
+        Trace("sym-break-dc-debug") << "Get max type info..." << std::endl;
+        Assert( d_has_dom_const_sort.get() );
+        int msid = d_max_dom_const_sort.get();
+        TypeInfo * max_ti = getTypeInfo( d_sid_to_type[msid], msid );
+        Trace("sym-break-dc-debug") << "Swap nodes..." << std::endl;
+        //now, check if we can apply symmetry breaking to another sort
+        if( ti->getNumDomainConstants()>max_ti->getNumDomainConstants() ){
+          Trace("sym-break-dc") << "Max domain constant subsort for " << tn << " becomes " << sid << std::endl;
+          d_max_dom_const_sort.set( sid );
+        }else if( ti!=max_ti ){
+          //construct symmetry breaking lemma
+          //current domain constant must be disequal from all current ones
+          Trace("sym-break-dc") << "Get domain constant " << ti->getNumDomainConstants()-1;
+          Trace("sym-break-dc") << " from max_ti, " << max_ti->getNumDomainConstants() << std::endl;
+          //apply a symmetry breaking lemma
+          Node m = max_ti->getDomainConstant(ti->getNumDomainConstants()-1);
+          //if fa and m are disequal from all previous domain constants in the other sort
+          std::vector< Node > cc;
+          for( unsigned r=0; r<2; r++ ){
+            Node n = ((r==0)==(msid>sid)) ? fa : m;
+            Node on = ((r==0)==(msid>sid)) ? m : fa;
+            TypeInfo * t = ((r==0)==(msid>sid)) ? max_ti : ti;
+            for( unsigned i=0; i<t->d_node_to_id[on]; i++ ){
+              cc.push_back( n.eqNode( t->d_nodes[i] ) );
+            }
+          }
+          //then, we can assume fa = m
+          cc.push_back( fa.eqNode( m ) );
+          Node lem = NodeManager::currentNM()->mkNode( kind::OR, cc );
+          lem = Rewriter::rewrite( lem );
+          if( std::find( d_lemmas.begin(), d_lemmas.end(), lem )==d_lemmas.end() ){
+            d_lemmas.push_back( lem );
+            Trace("sym-break-lemma") << "*** Symmetry break lemma for " << tn << " (" << sid << "==" << d_max_dom_const_sort.get() << ") : ";
+            Trace("sym-break-lemma") << lem << std::endl;
+            d_pending_lemmas.push_back( lem );
+          }
+        }
+        invalid = true;
+      }
+      if( invalid ){
+        ti->d_first_active.set( ti->d_first_active + 1 );
+        fa = ti->getFirstActive();
+      }
+    }
+  }
+}
+
+void SubsortSymmetryBreaker::printDebugTypeInfo( const char * c, TypeNode tn, int sid ) {
+  Trace(c) << "TypeInfo( " << tn << ", " << sid << " ) = " << std::endl;
+  Trace(c) << "  Domain constants : ";
+  TypeInfo * ti = getTypeInfo( tn, sid );
+  for( NodeList::const_iterator it = ti->d_dom_constants.begin(); it != ti->d_dom_constants.end(); ++it ){
+    Node dc = *it;
+    Trace(c) << dc << " ";
+  }
+  Trace(c) << std::endl;
+  Trace(c) << "  First active node : " << ti->getFirstActive() << std::endl;
+}
+
+
+void SubsortSymmetryBreaker::queueFact( Node n ) {
+  d_fact_list.push_back( n );
+  /*
+  if( n.getKind()==EQUAL ){
+    merge( n[0], n[1] );
+  }else if( n.getKind()==NOT && n[0].getKind()==EQUAL ){
+    assertDisequal( n[0][0], n[0][1] );
+  }else{
+    newEqClass( n );
+  }
+  */
+}
+
+bool SubsortSymmetryBreaker::check( Theory::Effort level ) {
+  d_pending_lemmas.clear();
+
+  Trace("sym-break-debug") << "SymBreak : check " << level << std::endl;
+  while( d_fact_index.get()<d_fact_list.size() ){
+    Node f = d_fact_list[d_fact_index.get()];
+    d_fact_index.set( d_fact_index.get() + 1 );
+    if( f.getKind()==EQUAL ){
+      merge( f[0], f[1] );
+    }else if( f.getKind()==NOT && f[0].getKind()==EQUAL ){
+      assertDisequal( f[0][0], f[0][1] );
+    }else{
+      newEqClass( f );
+    }
+  }
+  Trace("sym-break-debug") << "SymBreak : update first actives" << std::endl;
+  for( std::map< TypeNode, std::vector< int > >::iterator it = d_sub_sorts.begin(); it != d_sub_sorts.end(); ++it ){
+    int card = getStrongSolver()->getCardinality( it->first );
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      //check if the first active is disequal from all domain constants
+      processFirstActive( it->first, it->second[i], card );
+    }
+  }
+
+
+  Trace("sym-break-debug") << "SymBreak : finished check, now flush lemmas... (#lemmas = " << d_pending_lemmas.size() << ")" << std::endl;
+  //flush pending lemmas
+  if( !d_pending_lemmas.empty() ){
+    for( unsigned i=0; i<d_pending_lemmas.size(); i++ ){
+      getStrongSolver()->getOutputChannel().lemma( d_pending_lemmas[i] );
+      ++( getStrongSolver()->d_statistics.d_sym_break_lemmas );
+    }
+    d_pending_lemmas.clear();
+    return true;
+  }else{
+    return false;
+  }
+}
+
+
+
+}
+
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
new file mode 100755
index 000000000..3db9097f5
--- /dev/null
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -0,0 +1,121 @@
+/*********************                                                        */
+/*! \file symmetry_breaking.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 first-order reasoning
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H
+#define __CVC4__QUANT_SYMMETRY_BREAKING_H
+
+#include "theory/theory.h"
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+#include "util/sort_inference.h"
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace uf {
+  class StrongSolverTheoryUF;
+}
+
+class SubsortSymmetryBreaker {
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  //typedef context::CDChunkList<int> IntList;
+  typedef context::CDList<Node> NodeList;
+  typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap;
+private:
+  /** quantifiers engine */
+  QuantifiersEngine* d_qe;
+  eq::EqualityEngine * getEqualityEngine();
+  bool areDisequal( Node n1, Node n2 );
+  bool areEqual( Node n1, Node n2 );
+  Node getRepresentative( Node n );
+  uf::StrongSolverTheoryUF * getStrongSolver();
+  std::vector< Node > d_unit_lemmas;
+  Node d_true;
+  context::CDO< bool > d_conflict;
+public:
+  SubsortSymmetryBreaker( QuantifiersEngine* qe, context::Context* c );
+  ~SubsortSymmetryBreaker(){}
+
+private:
+  class TypeInfo {
+  private:
+    SubsortSymmetryBreaker * d_ssb;
+    //bool isActive( Node n, unsigned & deq );
+  public:
+    TypeInfo( SubsortSymmetryBreaker * ssb, context::Context* c );
+    //list of all nodes from this (sub)type
+    std::vector< Node > d_nodes;
+    //the current domain constants for this (sub)type
+    NodeList d_dom_constants;
+    //# nodes in d_nodes that have been domain constants, size of this distinct # of domain constants seen
+    unsigned d_dc_nodes;
+    //the node we are currently watching to become a domain constant
+    context::CDO< int > d_first_active;
+    //node to id
+    std::map< Node, unsigned > d_node_to_id;
+    Node getBaseConstant() { return d_nodes.empty() ? Node::null() : d_nodes[0]; }
+    bool hasDomainConstant( Node n );
+    unsigned getNumDomainConstants();
+    Node getDomainConstant( int i );
+    Node getFirstActive();
+  };
+  std::map< TypeNode, std::vector< int > > d_sub_sorts;
+  std::map< int, TypeNode > d_sid_to_type;
+  std::map< int, TypeInfo * > d_type_info;
+
+  //maximum domain constants sort
+  context::CDO< int > d_max_dom_const_sort;
+  context::CDO< bool > d_has_dom_const_sort;
+
+  TypeInfo * getTypeInfo( TypeNode tn, int sid );
+
+  void processFirstActive( TypeNode tn, int sid, int curr_card );
+private:
+  //void printDebugNodeInfo( const char * c, Node n );
+  void printDebugTypeInfo( const char * c, TypeNode tn, int sid );
+  /** new node */
+  void newEqClass( Node n );
+  /** merge */
+  void merge( Node a, Node b );
+  /** assert disequal */
+  void assertDisequal( Node a, Node b );
+  /** fact list */
+  context::CDO< unsigned > d_fact_index;
+  NodeList d_fact_list;
+  std::vector< Node > d_pending_lemmas;
+  std::vector< Node > d_lemmas;
+public:
+  /** queue fact */
+  void queueFact( Node n );
+  /** check */
+  bool check( Theory::Effort level );
+};
+
+}
+}
+
+#endif