Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas.

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 8bf3d4d64bb32cdc79db0cab9595286a2695a3b4..62621f3899825f8c3d59aff0f68b0b212ebfe113 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -20,6 +20,7 @@
 #include "expr/node_manager.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
+#include "smt/smt_engine_scope.h"
 
 #include "theory/quantifiers/options.h"
 
@@ -739,31 +740,55 @@ bool SygusSplit::isGenericRedundant( TypeNode tn, Node g ) {
 
 
 SygusSymBreak::SygusSymBreak( SygusUtil * util, context::Context* c ) :
-d_util( util ), d_testers( c ), d_watched_terms( c ), d_watched_count( c ), d_anchor( c ), d_prog_depth( c, 0 ), d_conflict( c ) {
-
+d_util( util ), d_context( c ) {
 
 }
 
 void SygusSymBreak::addTester( Node tst ) {
+  if( options::sygusNormalFormGlobal() ){
+    Node a = getAnchor( tst[0] );
+    Trace("sygus-sym-break-debug") << "Add tester " << tst << " for " << a << std::endl;
+    std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a );
+    ProgSearch * ps;
+    if( it==d_prog_search.end() ){
+      ps = new ProgSearch( this, a, d_context );
+      d_prog_search[a] = ps;
+    }else{
+      ps = it->second;
+    }
+    ps->addTester( tst );
+  }
+}
+
+Node SygusSymBreak::getAnchor( Node n ) {
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    return getAnchor( n[0] );
+  }else{
+    return n;
+  }
+}
+
+void SygusSymBreak::ProgSearch::addTester( Node tst ) {
   NodeMap::const_iterator it = d_testers.find( tst[0] );
   if( it==d_testers.end() ){
     d_testers[tst[0]] = tst;
-    if( d_anchor.get().isNull() ){
-      if( tst[0].getKind()!=APPLY_SELECTOR_TOTAL ){
-        d_anchor = tst[0];
-        assignTester( tst, 0 );
-      }
+    if( tst[0]==d_anchor ){
+      assignTester( tst, 0 );
     }else{
       IntMap::const_iterator it = d_watched_terms.find( tst[0] );
       if( it!=d_watched_terms.end() ){
         assignTester( tst, (*it).second );
+      }else{
+        Trace("sygus-sym-break-debug2") << "...add to wait list " << tst << " for " << d_anchor << std::endl;
       }
     }
+  }else{
+    Trace("sygus-sym-break-debug2") << "...already seen " << tst << " for " << d_anchor << std::endl;
   }
 }
 
-void SygusSymBreak::assignTester( Node tst, int depth ) {
-  Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tst << ", depth = " << depth << std::endl;
+void 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();
   Assert( DatatypesRewriter::isTypeDatatype( tn ) );
@@ -786,7 +811,7 @@ void SygusSymBreak::assignTester( Node tst, int depth ) {
   }else{
     d_watched_count[depth+1] = d_watched_count[depth+1] + dt[tindex].getNumArgs();
   }
-  Trace("sygus-sym-break-debug") << "...watched count now " << d_watched_count[depth+1].get() << " for " << (depth+1) << std::endl;
+  Trace("sygus-sym-break-debug") << "...watched count now " << d_watched_count[depth+1].get() << " for " << (depth+1) << " of " << d_anchor << std::endl;
   //now decrement watch count and process
   if( depth>0 ){
     Assert( d_watched_count[depth]>0 );
@@ -799,7 +824,7 @@ void SygusSymBreak::assignTester( Node tst, int depth ) {
   }
 }
 
-Node SygusSymBreak::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers ) {
+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 );
@@ -818,10 +843,10 @@ Node SygusSymBreak::getCandidateProgramAtDepth( int depth, Node prog, int curr_d
       pre[i] = getCandidateProgramAtDepth( depth, sel, curr_depth+1, var_count, testers );
     }
   }
-  return d_util->mkGeneric( dt, tindex, var_count, pre );
+  return d_parent->d_util->mkGeneric( dt, tindex, var_count, pre );
 }
 
-void SygusSymBreak::processProgramDepth( int depth ){
+void 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 ){
@@ -829,32 +854,38 @@ void SygusSymBreak::processProgramDepth( int depth ){
       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.get(), 0, var_count, testers );
-      if( d_normalized.find( prog )==d_normalized.end() ){
-        Trace("sygus-sym-break") << "Currently considering program : " << prog << " at depth " << depth << std::endl;
-        Node progr = Rewriter::rewrite( prog );
-        std::map< TypeNode, int > var_count;
-        std::map< Node, Node > subs;
-        progr = d_util->getSygusNormalized( progr, var_count, subs );
-        Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
-        d_normalized[prog] = progr;
-        std::map< Node, Node >::iterator it = d_normalized_to_orig.find( progr );
-        if( it==d_normalized_to_orig.end() ){
-          d_normalized_to_orig[progr] = prog;
-        }else{
-          Assert( !testers.empty() );
-          Trace("sygus-nf") << "* Sygus sym break : " << prog << " and " << it->second << " both rewrite to " << progr << std::endl;
-          Node conflict = testers.size()==1 ? testers[0] : NodeManager::currentNM()->mkNode( AND, testers );
-          Trace("sygus-sym-break2") << "Conflict : " << conflict << std::endl;
-        }
-      }
+      Node prog = getCandidateProgramAtDepth( depth, d_anchor, 0, var_count, testers );
+      d_parent->processCurrentProgram( d_anchor, d_anchor_type, depth, prog, testers );
     }
     processProgramDepth( depth+1 );
   }
 }
 
+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() ){
+    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;
+    std::map< Node, Node > subs;
+    progr = d_util->getSygusNormalized( progr, var_count, subs );
+    Trace("sygus-sym-break2") << "...rewrites to " << progr << std::endl;
+    d_normalized[at][prog] = progr;
+    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;
+    }else{
+      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;
 
-SygusUtil::SygusUtil( Context* c ) {
+      // TODO : generalize conflict
+    }
+  }
+}
+
+SygusUtil::SygusUtil( Context* c ) : d_conflict( c, false ) {
   d_split = new SygusSplit( this );
   d_sym_break = new SygusSymBreak( this, c );
 }
@@ -913,19 +944,17 @@ Node SygusUtil::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >&
     Assert( !a.isNull() );
     children.push_back( a );
   }
-  if( Trace.isOn("sygus-split-debug3") ){
-    Trace("sygus-split-debug3") << "mkGeneric " << dt[c].getName() << ", op = " << op << " with arguments : " << std::endl;
-    for( unsigned i=0; i<children.size(); i++ ){
-      Trace("sygus-split-debug3") << "  " << children[i] << std::endl;
-    }
-  }
   if( op.getKind()==BUILTIN ){
     return NodeManager::currentNM()->mkNode( op, children );
   }else{
     if( children.size()==1 ){
       return children[0];
     }else{
-      return NodeManager::currentNM()->mkNode( APPLY, children );
+      Node n = NodeManager::currentNM()->mkNode( APPLY, children );
+      //must expand definitions
+      Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
+      Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+      return ne;
     }
   }
 }

diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 69806e07677df6d1d5c3ac3ca3e49365424a82e7..fd006566758cb0111dc011c9bdfd7c45ef42eb34 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -110,22 +110,36 @@ public:
 
 class SygusSymBreak
 {
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-  typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
-  typedef context::CDHashMap< int, int > IntIntMap;
 private:
   SygusUtil * d_util;
-  NodeMap d_testers;
-  IntMap d_watched_terms;
-  IntIntMap d_watched_count;
-  context::CDO<Node> d_anchor;
-  context::CDO<int> d_prog_depth;
-  std::map< Node, Node > d_normalized;
-  std::map< Node, Node > d_normalized_to_orig;
-  void assignTester( Node tst, int depth );
-  Node getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, std::map< TypeNode, int >& var_count, std::vector< Node >& testers );
-  void processProgramDepth( int depth );
-  context::CDO<Node> d_conflict;
+  context::Context* d_context;
+  class ProgSearch {
+    typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+    typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
+    typedef context::CDHashMap< int, int > IntIntMap;
+  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 );
+  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 ) {
+      d_anchor_type = d_anchor.getType();
+    }
+    Node d_anchor;
+    NodeMap d_testers;
+    IntMap d_watched_terms;
+    IntIntMap d_watched_count;
+    TypeNode d_anchor_type;
+    context::CDO<int> d_prog_depth;
+    void addTester( Node tst );
+  };
+  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;
+  Node getAnchor( Node n );
+  void processCurrentProgram( Node a, TypeNode at, int depth, Node prog, std::vector< Node >& testers );
 public:
   SygusSymBreak( SygusUtil * util, context::Context* c );
   /** add tester */
@@ -150,6 +164,8 @@ public:
   SygusUtil( context::Context* c );
   SygusSplit * getSplit() { return d_split; }
   SygusSymBreak * getSymBreak() { return d_sym_break; }
+  context::CDO<bool> d_conflict;
+  Node d_conflictNode;
 };
 
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f38545817baf0917030041e44106ed8d9849edd3..264158ed4635c65b0028cf2afcc42eb89192da16 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -338,12 +338,14 @@ void TheoryDatatypes::flushPendingFacts(){
 }
 
 void TheoryDatatypes::doPendingMerges(){
-  //do all pending merges
-  int i=0;
-  while( i<(int)d_pending_merge.size() ){
-    Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
-    merge( d_pending_merge[i][0], d_pending_merge[i][1] );
-    i++;
+  if( !d_conflict ){
+    //do all pending merges
+    int i=0;
+    while( i<(int)d_pending_merge.size() ){
+      Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
+      merge( d_pending_merge[i][0], d_pending_merge[i][1] );
+      i++;
+    }
   }
   d_pending_merge.clear();
 }
@@ -360,15 +362,22 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
   doPendingMerges();
   //add to tester if applicable
   if( atom.getKind()==kind::APPLY_TESTER ){
-    if( polarity ){
+    Node rep = getRepresentative( atom[0] );
+    EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
+    addTester( fact, eqc, rep );
+    if( !d_conflict && polarity ){
       Trace("dt-tester") << "Assert tester : " << atom << std::endl;
       if( d_sygus_util ){
         d_sygus_util->getSymBreak()->addTester( atom );
+        if( d_sygus_util->d_conflict ){
+          d_conflict = true;
+          d_conflictNode = d_sygus_util->d_conflictNode;
+          Trace("dt-conflict") << "CONFLICT: sygus symmetry breaking conflict : " << d_conflictNode << std::endl;
+          d_out->conflict( d_conflictNode );
+          return;
+        }
       }
     }
-    Node rep = getRepresentative( atom[0] );
-    EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
-    addTester( fact, eqc, rep );
   }
   doPendingMerges();
 }

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 6fc13498c33a625b545e177e5d2719e186e3f39e..9d4281186c9ac817cf82d434f5c55a42d1e8ab41 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -196,12 +196,14 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
-option sygusDecompose --sygus-decompose bool :default false
-  decompose single invocation synthesis conjectures
+option sygusSingleInv --sygus-single-inv bool :default false
+  process single invocation synthesis conjectures
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
 option sygusNormalFormArg --sygus-nf-arg bool :default true
   account for relationship between arguments of operations in sygus normal form
+option sygusNormalFormGlobal --sygus-nf-global bool :default true
+  narrow sygus search space based on global state of current candidate program
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions