Apply sygus search space narrowing for all subprograms of current global state.

2 files changed, 96 insertions, 40 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 62621f389..4e7aaad53 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -787,7 +787,7 @@ void SygusSymBreak::ProgSearch::addTester( Node tst ) {
   }
 }
 
-void SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) {
+bool SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) {
   Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tst << ", depth = " << depth << " of " << d_anchor << std::endl;
   int tindex = Datatype::indexOf( tst.getOperator().toExpr() );
   TypeNode tn = tst[0].getType();
@@ -817,52 +817,98 @@ void SygusSymBreak::ProgSearch::assignTester( Node tst, int depth ) {
     Assert( d_watched_count[depth]>0 );
     d_watched_count[depth] = d_watched_count[depth] - 1;
   }
-  processProgramDepth( depth );
-  //assign preexisting testers
-  for( unsigned i=0; i<tst_waiting.size(); i++ ){
-    assignTester( tst_waiting[i], depth+1 );
-  }
-}
-
-Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) {
-  Assert( depth>=curr_depth );
-  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
-  NodeMap::const_iterator it = d_testers.find( prog );
-  Assert( it!=d_testers.end() );
-  Node tst = (*it).second;
-  testers.push_back( tst );
-  Assert( tst[0]==prog );
-  int tindex = Datatype::indexOf( tst.getOperator().toExpr() );
-  TypeNode tn = prog.getType();
-  Assert( DatatypesRewriter::isTypeDatatype( tn ) );
-  const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-  std::map< int, Node > pre;
-  if( curr_depth<depth ){
-    for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
-      Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog );
-      pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers );
+  //determine if any subprograms on the current path are redundant
+  if( processSubprograms( tst[0], depth, depth ) ){
+    if( processProgramDepth( depth ) ){
+      //assign preexisting testers
+      for( unsigned i=0; i<tst_waiting.size(); i++ ){
+        if( !assignTester( tst_waiting[i], depth+1 ) ){
+          return false;
+        }
+      }
+      return true;
     }
   }
-  return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre );
+  return false;
 }
 
-void SygusSymBreak::ProgSearch::processProgramDepth( int depth ){
+bool SygusSymBreak::ProgSearch::processProgramDepth( int depth ){
   if( depth==d_prog_depth.get() && ( depth==0 || ( d_watched_count.find( depth )!=d_watched_count.end() && d_watched_count[depth]==0 ) ) ){
     d_prog_depth = d_prog_depth + 1;
     if( depth>0 ){
-      Trace("sygus-sym-break-debug") << "Program is set for depth=" << depth << std::endl;
+      Trace("sygus-sym-break-debug") << "Program is set for depth " << depth << std::endl;
       std::map< TypeNode, int > var_count;
       std::vector< Node > testers;
       //now have entire information about candidate program at given depth
       Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers );
-      d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers );
+      if( !prog.isNull() ){
+        if( !d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers ) ){
+          return false;
+        }
+      }else{
+        Assert( false );
+      }
     }
-    processProgramDepth( depth+1 );
+    return processProgramDepth( depth+1 );
+  }else{
+    return true;
   }
 }
 
-void SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ) {
-  if( d_normalized[at].find( prog )==d_normalized[at].end() ){
+bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odepth ) {
+  Trace("sygus-sym-break-debug") << "Processing subprograms on path " << n << ", which has depth " << depth << std::endl;
+  depth--;
+  if( depth>0 ){
+    Assert( n.getKind()==APPLY_SELECTOR_TOTAL );
+    std::map< TypeNode, int > var_count;
+    std::vector< Node > testers;
+    //now have entire information about candidate program at given depth
+    Node prog = getCandidateProgramAtDepth( odepth-depth, n[0], 0, var_count, testers );
+    if( !prog.isNull() ){
+      if( !d_parent->processCurrentProgram( n[0], n[0].getType(), odepth-depth, prog, testers ) ){
+        return false;
+      }
+      //also try higher levels
+      return processSubprograms( n[0], depth, odepth );
+    }else{
+      Trace("sygus-sym-break-debug") << "...program incomplete." << std::endl;
+    }
+  }
+  return true;
+}
+
+Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) {
+  Assert( depth>=curr_depth );
+  Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl;
+  NodeMap::const_iterator it = d_testers.find( prog );
+  if( it!=d_testers.end() ){
+    Node tst = (*it).second;
+    testers.push_back( tst );
+    Assert( tst[0]==prog );
+    int tindex = Datatype::indexOf( tst.getOperator().toExpr() );
+    TypeNode tn = prog.getType();
+    Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    std::map< int, Node > pre;
+    if( curr_depth<depth ){
+      for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
+        Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex][i].getSelector() ), prog );
+        pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers );
+        if( pre[i].isNull() ){
+          return Node::null();
+        }
+      }
+    }
+    return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre );
+  }else{
+    Trace("sygus-sym-break-debug") << "...failure." << std::endl;
+    return Node::null();
+  }
+}
+
+bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers ) {
+  std::map< Node, Node >::iterator it = d_normalized[at].find( prog );
+  if( it==d_normalized[at].end() ){
     Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << " for " << a << std::endl;
     Node progr = Rewriter::rewrite( prog );
     std::map< TypeNode, int > var_count;
@@ -873,16 +919,24 @@ void SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
     std::map< Node, Node >::iterator it = d_normalized_to_orig[at].find( progr );
     if( it==d_normalized_to_orig[at].end() ){
       d_normalized_to_orig[at][progr] = prog;
+      d_redundant[at][prog] = false;
     }else{
+      d_redundant[at][prog] = true;
       Assert( !testers.empty() );
       Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl;
-      d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers );
-      Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl;
-      d_util->d_conflict = true;
-
-      // TODO : generalize conflict
     }
   }
+  Assert( d_redundant[at].find( prog )!=d_redundant[at].end() );
+  if( d_redundant[at][prog] ){
+    d_util->d_conflictNode = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers );
+    Trace("sygus-sym-break2") << "Conflict : " << d_util->d_conflictNode << std::endl;
+    d_util->d_conflict = true;
+    d_redundant[at][prog] = true;
+    // TODO : generalize conflict
+    return false;
+  }else{
+    return true;
+  }
 }
 
 SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index fd0065667..cf43b0a31 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -120,8 +120,9 @@ private:
   private:
     SygusSymBreak * d_parent;
     Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers );
-    void processProgramDepth( int depth );
-    void assignTester( Node tst, int depth );
+    bool processProgramDepth( int depth );
+    bool processSubprograms( Node n, int depth, int odepth );
+    bool assignTester( Node tst, int depth );
   public:
     ProgSearch( SygusSymBreak * p, Node a, context::Context* c ) : 
       d_parent( p ), d_anchor( a ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_prog_depth( c, 0 ) {
@@ -138,8 +139,9 @@ private:
   std::map< Node, ProgSearch * > d_prog_search;
   std::map< TypeNode, std::map< Node, Node > > d_normalized;
   std::map< TypeNode, std::map< Node, Node > > d_normalized_to_orig;
+  std::map< TypeNode, std::map< Node, bool > > d_redundant;
   Node getAnchor( Node n );
-  void processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers );
+  bool processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers );
 public:
   SygusSymBreak( SygusUtil * util, context::Context* c );
   /** add tester */