From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Feb 2015 18:07:49 +0000 (+0100)
Subject: Better support for solving multiple functions with cegqi-si.  Minor cleanup.
X-Git-Tag: cvc5-1.0.0~6396
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6893a60697e86eebccda6cc8e2e92cea7ee654e3;p=cvc5.git

Better support for solving multiple functions with cegqi-si.  Minor cleanup.
---

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 30eac03fb..616c51f54 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -271,23 +271,6 @@ void CegConjectureSingleInv::initialize() {
               }
             }
           }
-
-          /*
-          //equality resolution
-          for( unsigned j=0; j<conjuncts.size(); j++ ){
-            Node conj = conjuncts[j];
-            std::map< Node, std::vector< Node > > case_vals;
-            bool exh = processSingleInvLiteral( conj, false, case_vals );
-            Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl;
-            for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){
-              Trace("cegqi-si-er") << "  " << it->first << " -> ";
-              for( unsigned k=0; k<it->second.size(); k++ ){
-                Trace("cegqi-si-er") << it->second[k] << " ";
-              }
-              Trace("cegqi-si-er") << std::endl;
-            }
-          }
-          */
         }
       }
     }
@@ -358,32 +341,6 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol,
   return false;
 }
 
-bool CegConjectureSingleInv::processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ) {
-  if( lit.getKind()==NOT ){
-    return processSingleInvLiteral( lit[0], !pol, case_vals );
-  }else if( ( lit.getKind()==OR && pol ) || ( lit.getKind()==AND && !pol ) ){
-    bool exh = true;
-    for( unsigned k=0; k<lit.getNumChildren(); k++ ){
-      bool curr = processSingleInvLiteral( lit[k], pol, case_vals );
-      exh = exh && curr;
-    }
-    return exh;
-  }else if( lit.getKind()==IFF || lit.getKind()==EQUAL ){
-    if( pol ){
-      for( unsigned r=0; r<2; r++ ){
-        std::map< Node, Node >::iterator it = d_single_inv_map_to_prog.find( lit[r] );
-        if( it!=d_single_inv_map_to_prog.end() ){
-          if( r==1 || d_single_inv_map_to_prog.find( lit[1] )==d_single_inv_map_to_prog.end() ){
-            case_vals[it->second].push_back( lit[ r==0 ? 1 : 0 ] );
-            return true;
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
 bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
                                                             std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
                                                             std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
@@ -521,72 +478,91 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
       Trace("cegqi-engine-debug") << subs[index] << std::endl;
     }
     //try to improve substitutions : look for terms that contain terms in question
-    if( !subs_from_model.empty() ){
-      eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-      while( !eqcs_i.isFinished() ){
-        Node r = *eqcs_i;
-        int res = -1;
-        Node slv_n;
-        Node const_n;
-        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
-        while( !eqc_i.isFinished() ){
-          Node n = *eqc_i;
-          if( slv_n.isNull() || const_n.isNull() ){
-            std::vector< Node > vars;
-            int curr_res = classifyTerm( n, subs_from_model );
-            Trace("cegqi-si-debug2") << "Term : " << n << " classify : " << curr_res << std::endl;
-            if( curr_res!=-2 ){
-              if( curr_res!=-1 && slv_n.isNull() ){
-                res = curr_res;
-                slv_n = n;
-              }else if( const_n.isNull() ){
-                const_n = n;
-              }
-              //TODO : fairness
-              if( !slv_n.isNull() && !const_n.isNull() ){
+    bool success;
+    do{
+      success = false;
+      if( !subs_from_model.empty() ){
+        std::map< int, std::vector< Node > > cls_terms;
+        std::map< Node, std::vector< int > > vars;
+        std::map< Node, std::map< int, std::vector< Node > > > node_eqc;
+        std::map< Node, Node > node_rep;
+        int vn_max = -1;
+        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+        while( !eqcs_i.isFinished() ){
+          Node r = *eqcs_i;
+          TypeNode rtn = r.getType();
+          if( rtn.isInteger() || rtn.isReal() ){
+            eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+            while( !eqc_i.isFinished() ){
+              Node n = *eqc_i;
+              if( classifyTerm( n, subs_from_model, vars[n] ) ){
+                Trace("cegqi-si-debug") << "Term " << n << " in eqc " << r << " with " << vars[n].size() << " unset variables." << std::endl;
+                int vs = (int)vars[n].size();
+                cls_terms[vs].push_back( n );
+                node_eqc[r][vs].push_back( n );
+                node_rep[n] = r;
+                vn_max = vs>vn_max ? vs : vn_max;
               }
+              ++eqc_i;
             }
           }
-          ++eqc_i;
+          ++eqcs_i;
         }
-        if( !slv_n.isNull() && !const_n.isNull() ){
-          if( slv_n.getType().isInteger() || slv_n.getType().isReal() ){
-            Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[res] << " based on " << slv_n << " = " << const_n << std::endl;
-            subs_from_model.erase( d_single_inv_sk[res] );
-            Node prev_subs_res = subs[res];
-            subs[res] = d_single_inv_sk[res];
-            Node eq = slv_n.eqNode( const_n );
-            bool success = false;
-            std::map< Node, Node > msum;
-            if( QuantArith::getMonomialSumLit( eq, msum ) ){
-              Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
-              QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
-              Node veq;
-              if( QuantArith::isolate( d_single_inv_sk[res], msum, veq, EQUAL ) ){
-                Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[res] << " : " << veq << std::endl;
-                Node sol;
-                for( unsigned r=0; r<2; r++ ){
-                  if( veq[r]==d_single_inv_sk[res] ){
-                    sol = veq[ r==0 ? 1 : 0 ];
+        // will try processed, then unprocessed
+        for( unsigned p=0; p<2; p++ ){
+          Trace("cegqi-si-debug") << "Try " << ( p==0 ? "un" : "" ) << "processed equalities..." << std::endl;
+          //prefer smallest # variables first on LHS
+          for( int vn = 1; vn<=vn_max; vn++ ){
+            Trace("cegqi-si-debug") << "  Having " << vn << " variables on LHS..." << std::endl;
+            for( unsigned i=0; i<cls_terms[vn].size(); i++ ){
+              Node lhs = cls_terms[vn][i];
+              Node r = node_rep[lhs];
+              //prefer smallest # variables on RHS
+              for( int vnc = 0; vnc<=vn_max; vnc++ ){
+                Trace("cegqi-si-debug") << "    Having " << vnc << " variables on RHS..." << std::endl;
+                for( unsigned j=0; j<node_eqc[r][vnc].size(); j++ ){
+                  Node rhs = node_eqc[r][vnc][j];
+                  if( lhs!=rhs ){
+                    Trace("cegqi-si-debug") << "      try " << lhs << " " << rhs << std::endl;
+                    //for each variable in LHS
+                    for( unsigned k=0; k<vars[lhs].size(); k++ ){
+                      int v = vars[lhs][k];
+                      Trace("cegqi-si-debug") << "        variable " << v << std::endl;
+                      Assert( vars[lhs].size()==vn );
+                      //check if already processed
+                      bool proc = d_eq_processed[lhs][rhs].find( v )!=d_eq_processed[lhs][rhs].end();
+                      if( proc==(p==1) ){
+                        if( solveEquality( lhs, rhs, v, subs_from_model, subs ) ){
+                          Trace("cegqi-si-debug") << "Success, set " << lhs << " " << rhs << " " << v << std::endl;
+                          d_eq_processed[lhs][rhs][v] = true;
+                          success = true;
+                          break;
+                        }
+                      }
+                    }
+                    if( success ){ break; }
                   }
                 }
-                if( !sol.isNull() ){
-                  sol = applyProgVarSubstitution( sol, subs_from_model, subs );
-                  Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
-                  subs[res] = sol;
-                  Trace("cegqi-engine") << "  ...by arithmetic, " << d_single_inv_sk[res] << " -> " << sol << std::endl;
-                  success = true;
-                }
+                if( success ){ break; }
               }
+              if( success ){ break; }
             }
-            if( !success ){
-              subs[res] = prev_subs_res;
-            }
+            if( success ){ break; }
           }
+          if( success ){ break; }
+        }
+      }
+    }while( !subs_from_model.empty() && success );
+    
+    if( Trace.isOn("cegqi-si-warn") ){
+      if( !subs_from_model.empty() ){
+        Trace("cegqi-si-warn") << "Warning : could not find values for : " << std::endl;
+        for( std::map< Node, int >::iterator it = subs_from_model.begin(); it != subs_from_model.end(); ++it ){
+          Trace("cegqi-si-warn") << "  " << it->first << std::endl;
         }
-        ++eqcs_i;
       }
     }
+    
     Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() );
     lem = Rewriter::rewrite( lem );
     Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl;
@@ -599,6 +575,38 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
+bool CegConjectureSingleInv::solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
+  Trace("cegqi-si-debug") << "Can possibly set " << d_single_inv_sk[v] << " based on " << lhs << " = " << rhs << std::endl;
+  subs_from_model.erase( d_single_inv_sk[v] );
+  Node prev_subs_v = subs[v];
+  subs[v] = d_single_inv_sk[v];
+  Node eq = lhs.eqNode( rhs );
+  std::map< Node, Node > msum;
+  if( QuantArith::getMonomialSumLit( eq, msum ) ){
+    Trace("cegqi-si-debug") << "As monomial sum : " << std::endl;
+    QuantArith::debugPrintMonomialSum( msum, "cegqi-si");
+    Node veq;
+    if( QuantArith::isolate( d_single_inv_sk[v], msum, veq, EQUAL ) ){
+      Trace("cegqi-si-debug") << "Isolated for " << d_single_inv_sk[v] << " : " << veq << std::endl;
+      Node sol;
+      for( unsigned r=0; r<2; r++ ){
+        if( veq[r]==d_single_inv_sk[v] ){
+          sol = veq[ r==0 ? 1 : 0 ];
+        }
+      }
+      if( !sol.isNull() ){
+        sol = applyProgVarSubstitution( sol, subs_from_model, subs );
+        Trace("cegqi-si-debug") << "Substituted solution is : " << sol << std::endl;
+        subs[v] = sol;
+        Trace("cegqi-engine") << "  ...by arithmetic, " << d_single_inv_sk[v] << " -> " << sol << std::endl;
+        return true;
+      }
+    }
+  }
+  subs[v] = prev_subs_v;
+  return false;
+}
+
 Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ) {
   std::vector< Node > vars;
   collectProgVars( n, vars );
@@ -622,35 +630,34 @@ Node CegConjectureSingleInv::applyProgVarSubstitution( Node n, std::map< Node, i
   }
 }
 
-int CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model ) {
+bool CegConjectureSingleInv::classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars ) {
   if( n.getKind()==SKOLEM ){
     std::map< Node, int >::iterator it = subs_from_model.find( n );
     if( it!=subs_from_model.end() ){
-      return it->second;
+      if( std::find( vars.begin(), vars.end(), it->second )==vars.end() ){
+        vars.push_back( it->second );
+      }
+      return true;
     }else{
       // if it is symbolic argument, we are also fine
       if( std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end() ){
-        return -1;
+        return true;
       }else{
         //if it is another program, we are also fine
         if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){
-          return -1;
+          return true;
         }else{
-          return -2;
+          return false;
         }
       }
     }
   }else{
-    int curr_res = -1;
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      int res = classifyTerm( n[i], subs_from_model );
-      if( res==-2 ){
-        return res;
-      }else if( res!=-1 ){
-        curr_res = res;
+      if( !classifyTerm( n[i], subs_from_model, vars ) ){
+        return false;
       }
     }
-    return curr_res;
+    return true;
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 4a9ed76fe..a1f9d5a1f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -43,9 +43,12 @@ private:
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
 
   Node constructSolution( unsigned i, unsigned index );
-  int classifyTerm( Node n, std::map< Node, int >& subs_from_model );
+  bool classifyTerm( Node n, std::map< Node, int >& subs_from_model, std::vector< int >& vars );
   void collectProgVars( Node n, std::vector< Node >& vars );
   Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
+  //equalities processed
+  std::map< Node, std::map< Node, std::map< int, bool > > > d_eq_processed;
+  bool solveEquality( Node lhs, Node rhs, int v, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
 public:
   CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p );
   // original conjecture
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 02c4c3a28..7cefb0aec 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -661,7 +661,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int
             // if it is not already reconstructed
             if( d_reconstruct.find( itt->second )==d_reconstruct.end() ){
               Trace("csi-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
-              bool do_check = getPathToRoot( itt->second );
+              bool do_check = true;//getPathToRoot( itt->second );
               setReconstructed( itt->second, ns );
               if( do_check ){
                 Trace("csi-rcons-debug") << "...path to root, try reconstruction." << std::endl;
@@ -756,100 +756,116 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
       }
     }
     if( status!=0 ){
-      Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
-      //try other options
-      //match against other constructors
-      bool success;
-      int c_index = 0;
-      do{
-        success = false;
-        int index_found;
-        std::vector< Node > args;
-        if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){
-          success = true;
+      if( min_t.isConst() ){
+        Node min_t_c = d_qe->getTermDatabaseSygus()->builtinToSygusConst( min_t, stn );
+        if( !min_t_c.isNull() ){
+          d_reconstruct[id] = min_t_c;
           status = 0;
-          Node cons = Node::fromExpr( dt[index_found].getConstructor() );
-          Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
-          for( unsigned i=0; i<args.size(); i++ ){
-            Trace("csi-rcons-debug") << "  " << args[i] << std::endl;
-          }
-          if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
-            d_reconstruct_op[id].erase( cons );
-            status = 1;
-          }else{
-            c_index = index_found+1;
-          }
         }
-      }while( success && status!=0 );
-
+      }
       if( status!=0 ){
-        // construct an equivalence class of terms that are equivalent to t
-        if( d_rep[id]==id ){
-          Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
-          //get equivalence class of term
-          std::vector< Node > equiv;
-          if( tn.isBoolean() ){
-            Node curr = min_t;
-            Node new_t;
-            do{
-              new_t = Node::null();
-              if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
-                new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
-                                                              NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
-              }else if( curr.getKind()==ITE ){
-                new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
-                                                              NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
-              }else if( curr.getKind()==IFF ){
-                new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
-                                                              NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
-              }else if( curr.getKind()==OR || curr.getKind()==AND ){
-                new_t = TermDb::simpleNegate( curr ).negate();
-              }else if( curr.getKind()==NOT ){
-                new_t = TermDb::simpleNegate( curr[0] );
-              }else{
-                new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
-              }
-              if( !new_t.isNull() ){
-                if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
-                  curr = new_t;
-                  equiv.push_back( new_t );
+        Trace("csi-rcons-debug") << "Try matching for " << id << "." << std::endl;
+        //try other options
+        //match against other constructors
+        bool success;
+        int c_index = 0;
+        do{
+          success = false;
+          int index_found;
+          std::vector< Node > args;
+          if( d_qe->getTermDatabaseSygus()->getMatch( min_t, stn, index_found, args, karg, c_index ) ){
+            success = true;
+            status = 0;
+            Node cons = Node::fromExpr( dt[index_found].getConstructor() );
+            Trace("csi-rcons-debug") << "Try alternative for " << id << ", matching " << dt[index_found].getName() << " with children : " << std::endl;
+            for( unsigned i=0; i<args.size(); i++ ){
+              Trace("csi-rcons-debug") << "  " << args[i] << std::endl;
+            }
+            if( !collectReconstructNodes( id, args, dt[index_found], d_reconstruct_op[id][cons], status ) ){
+              d_reconstruct_op[id].erase( cons );
+              status = 1;
+            }else{
+              c_index = index_found+1;
+            }
+          }
+        }while( success && status!=0 );
+
+        if( status!=0 ){
+          // construct an equivalence class of terms that are equivalent to t
+          if( d_rep[id]==id ){
+            Trace("csi-rcons-debug") << "Try rewriting for " << id << "." << std::endl;
+            //get equivalence class of term
+            std::vector< Node > equiv;
+            if( tn.isBoolean() ){
+              Node curr = min_t;
+              Node new_t;
+              do{
+                new_t = Node::null();
+                if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){
+                  new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ),
+                                                                NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) );
+                }else if( curr.getKind()==ITE ){
+                  new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+                                                                NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) );
+                }else if( curr.getKind()==IFF ){
+                  new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ),
+                                                                NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) );
+                }else if( curr.getKind()==OR || curr.getKind()==AND ){
+                  new_t = TermDb::simpleNegate( curr ).negate();
+                }else if( curr.getKind()==NOT ){
+                  new_t = TermDb::simpleNegate( curr[0] );
                 }else{
-                  new_t = Node::null();
+                  new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) );
                 }
+                if( !new_t.isNull() ){
+                  if( new_t!=min_t && std::find( equiv.begin(), equiv.end(), new_t )==equiv.end() ){
+                    curr = new_t;
+                    equiv.push_back( new_t );
+                  }else{
+                    new_t = Node::null();
+                  }
+                }
+              }while( !new_t.isNull() );
+            }
+            for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+              Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
+              if( k==AND || k==OR ){
+                equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
+                equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
               }
-            }while( !new_t.isNull()  );
-          }
-          //assign ids to terms
-          Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
-          std::vector< int > equiv_ids;
-          for( unsigned i=0; i<equiv.size(); i++ ){
-            Trace("csi-rcons-debug") << "  " << equiv[i] << std::endl;
-            if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
-              int eq_id = allocate( equiv[i], stn );
-              d_eqc.erase( eq_id );
-              d_rep[eq_id] = id;
-              d_eqc[id].push_back( eq_id );
-              equiv_ids.push_back( eq_id );
-            }else{
-              equiv_ids.push_back( -1 );
             }
-          }
-          // now, try each of them
-          for( unsigned i=0; i<equiv.size(); i++ ){
-            if( equiv_ids[i]!=-1 ){
-              collectReconstructNodes( equiv[i], stn, status );
-              //if one succeeds
-              if( status==0 ){
-                Node rsol = getReconstructedSolution( equiv_ids[i] );
-                Assert( !rsol.isNull() );
-                //set all members of the equivalence class that this is the reconstructed solution
-                setReconstructed( id, rsol );
-                break;
+            //assign ids to terms
+            Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
+            std::vector< int > equiv_ids;
+            for( unsigned i=0; i<equiv.size(); i++ ){
+              Trace("csi-rcons-debug") << "  " << equiv[i] << std::endl;
+              if( d_rcons_to_id[stn].find( equiv[i] )==d_rcons_to_id[stn].end() ){
+                int eq_id = allocate( equiv[i], stn );
+                d_eqc.erase( eq_id );
+                d_rep[eq_id] = id;
+                d_eqc[id].push_back( eq_id );
+                equiv_ids.push_back( eq_id );
+              }else{
+                equiv_ids.push_back( -1 );
               }
             }
+            // now, try each of them
+            for( unsigned i=0; i<equiv.size(); i++ ){
+              if( equiv_ids[i]!=-1 ){
+                collectReconstructNodes( equiv[i], stn, status );
+                //if one succeeds
+                if( status==0 ){
+                  Node rsol = getReconstructedSolution( equiv_ids[i] );
+                  Assert( !rsol.isNull() );
+                  //set all members of the equivalence class that this is the reconstructed solution
+                  setReconstructed( id, rsol );
+                  break;
+                }
+              }
+            }
+          }else{
+            Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
           }
-        }else{
-          Trace("csi-rcons-debug") << "Do not try rewriting for " << id << ", rep = " << d_rep[id] << std::endl;
         }
       }
     }
@@ -963,7 +979,10 @@ int CegConjectureSingleInvSol::allocate( Node n, TypeNode stn ) {
   std::map< Node, int >::iterator it = d_rcons_to_id[stn].find( n );
   if( it==d_rcons_to_id[stn].end() ){
     int ret = d_id_count;
-    Trace("csi-rcons-debug") << "id " << ret << " : " << n << std::endl;
+    if( Trace.isOn("csi-rcons-debug") ){
+      const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+      Trace("csi-rcons-debug") << "id " << ret << " : " << n << " " <<  dt.getName() << std::endl;
+    }
     d_id_node[d_id_count] = n;
     d_id_type[d_id_count] = stn;
     d_rep[d_id_count] = d_id_count;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e3f73699b..08c8a7e3e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1568,6 +1568,8 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) {
       sc = Node::fromExpr( dt[carg].getSygusOp() );
     }else{
       //TODO
+      
+      
     }
     d_builtin_const_to_sygus[tn][c] = sc;
     return sc;