Work on solution reconstruction for single inv. Fix compiler error found by Tim...

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 2044d612c19cc79174a4417e4a9140d1cb25e73d..3475e9e97afd437b57fd549272f976a4b34c6c7c 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -477,7 +477,7 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
   if( d_conj ){
-    if( !Trace.isOn("cegqi-stats") ){
+    if( !(Trace.isOn("cegqi-stats")) ){
       out << "Solution:" << std::endl;
     }
     for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){
@@ -491,19 +491,21 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Assert( dt.isSygus() );
       //get the solution
       Node sol;
+      int status;
       if( d_last_inst_si ){
         Assert( d_conj->d_ceg_si );
-        sol = d_conj->d_ceg_si->getSolution( d_quantEngine, tn, i, Node::fromExpr( dt.getSygusVarList() ) );
+        sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, tn, status );
       }else{
         if( !d_conj->d_candidate_inst[i].empty() ){
           sol = d_conj->d_candidate_inst[i].back();
+          status = 1;
         }
       }
-      if( !Trace.isOn("cegqi-stats") ){
+      if( !(Trace.isOn("cegqi-stats")) ){
         out << "(define-fun " << f << " ";
         out << dt.getSygusVarList() << " ";
         out << dt.getSygusType() << " ";
-        if( d_last_inst_si ){
+        if( status==0 ){
           out << sol;
         }else{
           if( sol.isNull() ){

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index be20dd7c0e798cbd06ce451793073f0d1ccb01ba..e22674414fa7424b01eb5a335553bb2c5528296f 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -679,9 +679,11 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
   }
 }
 
-Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList ){
+Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed ){
   Assert( !d_lemmas_produced.empty() );
   Node s = constructSolution( i, 0 );
+  const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
+  Node varList = Node::fromExpr( dt.getSygusVarList() );
   //TODO : not in grammar
   Node prog = d_quant[0][i];
   Node prog_app = d_single_inv_app_map[prog];
@@ -697,6 +699,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
   d_orig_solution = s;
   Trace("cegqi-si-debug-sol") << "Solution (pre-rewrite): " << d_orig_solution << std::endl;
   s = pullITEs( s );
+  //s = flattenITEs( s );
   //do standard rewriting
   s = Rewriter::rewrite( s );
 
@@ -709,7 +712,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
   s = Rewriter::rewrite( s );
   Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl;
   d_solution = s;
-  if( options::cegqiSingleInvReconstruct() ){
+  if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){
     collectReconstructNodes( qe->getTermDatabaseSygus(), d_solution, stn, Node::null(), TypeNode::null(), false );
     std::vector< TypeNode > rcons_tn;
     for( std::map< TypeNode, std::map< Node, bool > >::iterator it = d_rcons_to_process.begin(); it != d_rcons_to_process.end(); ++it ){
@@ -723,7 +726,6 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
       Assert( !it->second.empty() );
       rcons_tn.push_back( it->first );
     }
-    /*
     bool success;
     unsigned index = 0;
     do {
@@ -733,17 +735,32 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, TypeNode stn,
         if( it->second.empty() ){
           to_erase.push_back( it->first );
         }else{
-          Node n = qe->getTermDatabase()->getEnumerateType( it->first, index );
-          
+          Node ns = qe->getTermDatabase()->getEnumerateTerm( it->first, index );
+          Node nb = qe->getTermDatabaseSygus()->sygusToBuiltin( ns, it->first );
+          Node nr = Rewriter::rewrite( nb );//qe->getTermDatabaseSygus()->getNormalized( it->first, nb, false, false );
+          if( it->second.find( nr )!=it->second.end() ){
+            Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
+            d_reconstructed[nr][it->first] = ns;
+            d_reconstructed_op[nr][it->first] = false;
+            setReconstructed( nr, it->first );
+          }
           success = false;
         }
       }
       for( unsigned i=0; i<to_erase.size(); i++ ){
+        Trace("cegqi-si-rcons") << "......reconstructed all terms for type " << to_erase[i] << std::endl;
         d_rcons_to_process.erase( to_erase[i] );
       }
       index++;
+      if( index%100==0 ){
+        Trace("cegqi-si-rcons-debug") << "Tried " << index << " for each type."  << std::endl;
+      }
+      if( success ){
+        reconstructed = 1;
+      }
     }while( !success );
-    */
+  }else{
+    reconstructed = 0;
   }
   if( Trace.isOn("cegqi-si-debug-sol") ){
     //debug solution
@@ -900,6 +917,60 @@ bool CegConjectureSingleInv::pullITECondition( Node root, Node n_ite, std::vecto
   }
 }
 
+Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) {
+  if( n.getKind()==ITE ){
+    Trace("csi-simp-debug") << "Flatten ITE : " << n << std::endl;
+    Node ret;
+    Node n0 = rec ? flattenITEs( n[0] ) : n[0];
+    Node n1 = rec ? flattenITEs( n[1] ) : n[1];
+    Node n2 = rec ? flattenITEs( n[2] ) : n[2];
+    if( n0.getKind()==NOT ){
+      ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
+    }else if( n0.getKind()==AND || n0.getKind()==OR ){
+      std::vector< Node > children;
+      for( unsigned i=1; i<n0.getNumChildren(); i++ ){
+        children.push_back( n0[i] );
+      }
+      Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( n0.getKind(), children );
+      Node ret;
+      if( n0.getKind()==AND ){
+        ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( n0[0], n1, n2 ), n2 );
+      }else{
+        ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( n0[0], n1, n2 ) );
+      }
+    }else{
+      if( n0.getKind()==ITE ){
+        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
+      }else if( n0.getKind()==IFF ){
+        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
+                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
+      }else{
+        return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+      }
+      ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
+    }
+    return flattenITEs( ret, false );
+  }else{
+    if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = flattenITEs( n[i] );
+        children.push_back( nc );
+        childChanged = childChanged || nc!=n[i];
+      }
+      if( !childChanged ){
+        return n;
+      }else{
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }else{
+      return n;
+    }
+  }
+}
+
 // assign is from literals to booleans
 // union_find is from args to values
 
@@ -1114,7 +1185,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
 
 void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean ) {
   if( ignoreBoolean && t.getType().isBoolean() ){
-    if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE ){
+    if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE || t.getKind()==NOT ){ //FIXME
       for( unsigned i=0; i<t.getNumChildren(); i++ ){
         collectReconstructNodes( tds, t[i], stn, parent, pstn, ignoreBoolean );
       }
@@ -1140,6 +1211,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
           collectReconstructNodes( tds, t[i], stnc, t, stn, ignB );
         }
         d_reconstructed[t][stn] = Node::fromExpr( dt[arg].getSygusOp() );
+        d_reconstructed_op[t][stn] = true;
         processed = true;
       }else{
         Trace("cegqi-si-rcons-debug") << "  Type has kind " << t.getKind() << ", but argument mismatch, with parent " << parent << std::endl;
@@ -1150,6 +1222,7 @@ void CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
       Trace("cegqi-si-rcons") << "...Reconstruction needed for " << t << " sygus type " << dt.getName() << " with parent " << parent << std::endl;
     }else{
       d_reconstructed[t][stn] = Node::fromExpr( dt[carg].getSygusOp() );
+      d_reconstructed_op[t][stn] = false;
       processed = true;
       Trace("cegqi-si-rcons-debug") << "  Type has constant." << std::endl;
     }
@@ -1178,9 +1251,11 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
       TypeNode stnc;
       for( std::map< TypeNode, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
         stnc = it2->first;
-        d_rcons_graph[ro][it->first][stnc][t].erase( it2->first );
+        d_rcons_graph[ro][it->first][stnc][t].erase( stn );
         if( d_rcons_graph[ro][it->first][stnc][t].empty() ){
           d_rcons_graph[ro][it->first][stnc].erase( t );
+        }else{
+          Trace("cegqi-si-rcons-debug") << "  " << ( r==0 ? "child" : "parent" ) << " " << it->first << " now has " << d_rcons_graph[ro][it->first][stnc][t].size() << std::endl;
         }
       }
       if( d_rcons_graph[ro][it->first][stnc].empty() ){
@@ -1198,6 +1273,27 @@ void CegConjectureSingleInv::setReconstructed( Node t, TypeNode stn ) {
   }
 }
 
+Node CegConjectureSingleInv::getReconstructedSolution( TypeNode stn, Node t ) {
+  std::map< TypeNode, Node >::iterator it = d_reconstructed[t].find( stn );
+  if( it!=d_reconstructed[t].end() ){
+    if( d_reconstructed_op[t][stn] ){
+      std::vector< Node > children;
+      children.push_back( it->second );
+      for( unsigned i=0; i<t.getNumChildren(); i++ ){
+        Node nc = getReconstructedSolution( stn, t[i] );
+        children.push_back( nc );
+      }
+      return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+    }else{
+      return it->second;
+    }
+  }else{
+    Trace("cegqi-si-rcons-debug") << "*** error : missing reconstruction for " << t << std::endl;
+    Assert( false );
+    return Node::null();
+  }
+}
+
 
 
 }
\ No newline at end of file

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index afd7167f2a481fc3a7df164c85a538a7415ae438..7667ccf11b4ed2ab98e6b7cb25c537613b7f587b 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -76,7 +76,7 @@ public:
   //check
   void check( QuantifiersEngine * qe, std::vector< Node >& lems );
   //get solution
-  Node getSolution( QuantifiersEngine * qe, TypeNode stn, unsigned i, Node varList );
+  Node getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed );
   
   
 //solution simplification
@@ -85,6 +85,7 @@ private:
   void debugTermSize( Node sol, int& t_size, int& num_ite );
   Node pullITEs( Node n );
   bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
+  Node flattenITEs( Node n, bool rec = true );
   Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
                          std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
   bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
@@ -94,12 +95,15 @@ private:
 private:
   std::map< Node, std::vector< TypeNode > > d_rcons_processed;
   std::map< Node, std::map< TypeNode, Node > > d_reconstructed;
+  std::map< Node, std::map< TypeNode, bool > > d_reconstructed_op;
   std::map< Node, std::map< TypeNode, std::map< Node, std::map< TypeNode, bool > > > > d_rcons_graph[2];
   std::map< TypeNode, std::map< Node, bool > > d_rcons_to_process;
   // term t with sygus type st
   void collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, Node parent, TypeNode pstn, bool ignoreBoolean );
   // set reconstructed 
   void setReconstructed( Node t, TypeNode stn );
+  // get solution
+  Node getReconstructedSolution( TypeNode stn, Node t );
 };
 
 }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 24d7cbb5ca00a22a2a722f82af109a91b6c62716..c5a3cec4d8ff909e6ab556964de7cf4a3c91f20f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1400,6 +1400,26 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
   }
 }
 
+Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
+  std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n );
+  if( it==d_sygus_to_builtin[tn].end() ){
+    Assert( n.getKind()==APPLY_CONSTRUCTOR );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    unsigned i = Datatype::indexOf( n.getOperator().toExpr() );
+    Assert( n.getNumChildren()==dt[i].getNumArgs() );
+    std::map< TypeNode, int > var_count;
+    std::map< int, Node > pre;
+    for( unsigned j=0; j<n.getNumChildren(); j++ ){
+      pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) );
+    }
+    Node ret = mkGeneric( dt, i, var_count, pre );
+    d_sygus_to_builtin[tn][n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
 Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
   return n;
   if( n.getKind()==SKOLEM ){
@@ -1436,7 +1456,7 @@ Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_cou
   }
 }
 
-Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
+Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool do_post_norm ) {
   if( do_pre_norm ){
     std::map< TypeNode, int > var_count;
     std::map< Node, Node > subs;
@@ -1446,9 +1466,11 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm ) {
   if( itn==d_normalized[t].end() ){
     Node progr = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( prog.toExpr() ) );
     progr = Rewriter::rewrite( progr );
-    std::map< TypeNode, int > var_count;
-    std::map< Node, Node > subs;
-    progr = getSygusNormalized( progr, var_count, subs );
+    if( do_post_norm ){
+      std::map< TypeNode, int > var_count;
+      std::map< Node, Node > subs;
+      progr = getSygusNormalized( progr, var_count, subs );
+    }
     Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
     d_normalized[t][prog] = progr;
     return progr;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index ce3a52d1cca0001291f611effe08dbe3137e3721..0f730929c3135ffbc6c1768d71fcb3ffaa662c12 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -388,6 +388,7 @@ private:
   std::map< TypeNode, std::map< Node, std::map< int, int > > > d_type_value_offset_status;
   //normalized map
   std::map< TypeNode, std::map< Node, Node > > d_normalized;
+  std::map< TypeNode, std::map< Node, Node > > d_sygus_to_builtin;
 public:
   TermDbSygus(){}
   bool isRegistered( TypeNode tn );
@@ -425,8 +426,9 @@ public:
   Node getTypeMaxValue( TypeNode tn );
   TypeNode getSygusType( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
+  Node sygusToBuiltin( Node n, TypeNode tn );
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
-  Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false );
+  Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
   int getTermSize( Node n );
 };