Decision strategy: incorporate datatypes sygus solver. (#2479)

5 files changed, 81 insertions, 133 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 18ccd483c..82aa570c2 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -50,9 +50,7 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td,
 }
 
 SygusSymBreakNew::~SygusSymBreakNew() {
-  for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
-    delete it->second;
-  }
+
 }
 
 /** add tester */
@@ -108,7 +106,8 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l
     Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
     registerMeasureTerm( m );
     if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
-      std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
+      std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
+          d_szinfo.find(m);
       Assert( its!=d_szinfo.end() );
       Node mt = its->second->getOrMkMeasureValue(lemmas);
       //it relates the measure term to arithmetic
@@ -238,7 +237,8 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std:
   Node a = d_term_to_anchor[n];
   Assert( d_anchor_to_measure_term.find( a )!=d_anchor_to_measure_term.end() );
   Node m = d_anchor_to_measure_term[a];
-  std::map< Node, SearchSizeInfo * >::iterator itsz = d_szinfo.find( m );
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
+      d_szinfo.find(m);
   Assert( itsz!=d_szinfo.end() );
   unsigned ssz = itsz->second->d_curr_search_size;
   
@@ -1073,6 +1073,19 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
           Node ag = d_tds->getActiveGuardForEnumerator(e);
           if( !ag.isNull() ){
             d_anchor_to_active_guard[e] = ag;
+            std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itaas =
+                d_anchor_to_ag_strategy.find(e);
+            if (itaas == d_anchor_to_ag_strategy.end())
+            {
+              d_anchor_to_ag_strategy[e].reset(
+                  new DecisionStrategySingleton("sygus_enum_active",
+                                                ag,
+                                                d_td->getSatContext(),
+                                                d_td->getValuation()));
+            }
+            d_td->getDecisionManager()->registerStrategy(
+                DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
+                d_anchor_to_ag_strategy[e].get());
           }
           Node m;
           if( !ag.isNull() ){
@@ -1119,15 +1132,21 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) {
 }
 
 void SygusSymBreakNew::registerMeasureTerm( Node m ) {
-  std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.find( m );
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator it =
+      d_szinfo.find(m);
   if( it==d_szinfo.end() ){
     Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
-    d_szinfo[m] = new SearchSizeInfo( m, d_td->getSatContext() );
+    d_szinfo[m].reset(new SygusSizeDecisionStrategy(
+        m, d_td->getSatContext(), d_td->getValuation()));
+    // register this as a decision strategy
+    d_td->getDecisionManager()->registerStrategy(
+        DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get());
   }
 }
 
 void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) {
-  std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
+      d_szinfo.find(m);
   Assert( its!=d_szinfo.end() );
   if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){
     its->second->d_search_size[s] = true;
@@ -1174,13 +1193,15 @@ unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) {
 unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m)
 {
   Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl;
-  std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m );
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
+      d_szinfo.find(m);
   Assert( its!=d_szinfo.end() );
   return its->second->d_curr_search_size;
 }
   
 void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) {
-  std::map< Node, SearchSizeInfo * >::iterator itsz = d_szinfo.find( m );
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
+      d_szinfo.find(m);
   Assert( itsz!=d_szinfo.end() );
   itsz->second->d_curr_search_size++;
   Trace("sygus-fair") << "  register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl;
@@ -1322,8 +1343,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) {
     if (lemmas.empty() && !d_szinfo.empty())
     {
       Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
-      for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
-        SearchSizeInfo * s = it->second;
+      for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
+               p : d_szinfo)
+      {
+        SygusSizeDecisionStrategy* s = p.second.get();
         Trace("cegqi-engine") << s->d_curr_search_size << " ";
       }
       Trace("cegqi-engine") << std::endl;
@@ -1403,7 +1426,7 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va
   }
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
+Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue(
     std::vector<Node>& lemmas)
 {
   if (d_measure_value.isNull())
@@ -1418,7 +1441,7 @@ Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
   return d_measure_value;
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
+Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
     std::vector<Node>& lemmas, bool mkNew)
 {
   if (mkNew)
@@ -1436,69 +1459,23 @@ Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
   return d_measure_value_active;
 }
 
-Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ) {
-  if( options::sygusFair()!=SYGUS_FAIR_NONE ){
-    std::map< unsigned, Node >::iterator it = d_lits.find( s );
-    if( it==d_lits.end() ){
-      if (options::sygusAbortSize() != -1
-          && static_cast<int>(s) > options::sygusAbortSize())
-      {
-        std::stringstream ss;
-        ss << "Maximum term size (" << options::sygusAbortSize()
-           << ") for enumerative SyGuS exceeded.";
-        throw LogicException(ss.str());
-      }
-      Assert( !d_this.isNull() );
-      Node c = NodeManager::currentNM()->mkConst( Rational( s ) );
-      Node lit = NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND, d_this, c );
-      lit = d->getValuation().ensureLiteral( lit );
-      
-      Trace("sygus-fair") << "******* Sygus : allocate size literal " << s << " for " << d_this << " : " << lit << std::endl;
-      Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s << " for " << d_this << std::endl;
-      Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
-      Trace("sygus-dec") << "Sygus : Fairness split : " << lem << std::endl;
-      lemmas.push_back( lem );
-      d->getOutputChannel().requirePhase( lit, true );
-    
-      d_lits[s] = lit;
-      return lit;
-    }else{
-      return it->second;
-    }
-  }else{
+Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
+{
+  if (options::sygusFair() == SYGUS_FAIR_NONE)
+  {
     return Node::null();
   }
-}
-
-Node SygusSymBreakNew::getNextDecisionRequest( unsigned& priority, std::vector< Node >& lemmas ) {
-  Trace("sygus-dec-debug") << "SygusSymBreakNew: Get next decision " << std::endl;
-  for( std::map< Node, Node >::iterator it = d_anchor_to_active_guard.begin(); it != d_anchor_to_active_guard.end(); ++it ){
-    if( getGuardStatus( it->second )==0 ){
-      Trace("sygus-dec") << "Sygus : Decide next on active guard : " << it->second << "..." << std::endl;
-      priority = 1;
-      return it->second;
-    }
-  }
-  for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
-    SearchSizeInfo * s = it->second;
-    std::vector< Node > new_lit;
-    Node c_lit = s->getCurrentFairnessLiteral( d_td, lemmas );
-    Assert( !c_lit.isNull() );
-    int gstatus = getGuardStatus( c_lit );
-    if( gstatus==-1 ){
-      s->incrementCurrentLiteral();
-      c_lit = s->getCurrentFairnessLiteral( d_td, lemmas );
-      Assert( !c_lit.isNull() );
-      Trace("sygus-dec") << "Sygus : Decide on next lit : " << c_lit << "..." << std::endl;
-      priority = 1;
-      return c_lit;
-    }else if( gstatus==0 ){
-      Trace("sygus-dec") << "Sygus : Decide on current lit : " << c_lit << "..." << std::endl;
-      priority = 1;
-      return c_lit;
-    }
+  if (options::sygusAbortSize() != -1
+      && static_cast<int>(s) > options::sygusAbortSize())
+  {
+    std::stringstream ss;
+    ss << "Maximum term size (" << options::sygusAbortSize()
+       << ") for enumerative SyGuS exceeded.";
+    throw LogicException(ss.str());
   }
-  return Node::null();
+  Assert(!d_this.isNull());
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
 }
 
 int SygusSymBreakNew::getGuardStatus( Node g ) {
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index c5f3fe560..e2ed4192a 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -51,6 +51,18 @@ class TheoryDatatypes;
  * Some of these techniques are described in these papers:
  * "Refutation-Based Synthesis in SMT", Reynolds et al 2017.
  * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017.
+ *
+ * This class enforces two decisions stragies via calls to registerStrategy
+ * of the owning theory's DecisionManager:
+ * (1) Positive decisions on the active guards G of enumerators e registered
+ * to this class. These assert "there are more values to enumerate for e".
+ * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below),
+ * where n is a non-negative integer. This asserts "the measure of terms
+ * we are enumerating for enumerators whose measure term m is at most n",
+ * where measure is commonly term size, but can also be height.
+ *
+ * We prioritize decisions of form (1) before (2). Both kinds of decision are
+ * critical for solution completeness, which is enforced by DecisionManager.
  */
 class SygusSymBreakNew
 {
@@ -95,24 +107,6 @@ class SygusSymBreakNew
    * all preregistered enumerators.
    */
   void check(std::vector<Node>& lemmas);
-  /** get next decision request
-   *
-   * This function has the same interface as Theory::getNextDecisionRequest.
-   *
-   * The decisions returned by this method are of one of two forms:
-   * (1) Positive decisions on the active guards G of enumerators e registered
-   * to this class. These assert "there are more values to enumerate for e".
-   * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below),
-   * where n is a non-negative integer. This asserts "the measure of terms
-   * we are enumerating for enumerators whose measure term m is at most n",
-   * where measure is commonly term size, but can also be height.
-   *
-   * We prioritize decisions of form (1) before (2). For both decisions,
-   * we set the priority argument to "1", indicating that the decision is
-   * critical for solution completeness.
-   */
-  Node getNextDecisionRequest(unsigned& priority, std::vector<Node>& lemmas);
-
  private:
   /** Pointer to the datatype theory that owns this class. */
   TheoryDatatypes* d_td;
@@ -453,14 +447,17 @@ private:
    * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n).
    *
    * After determining the measure term m for e, if applicable, we initialize
-   * SearchSizeInfo for m below. This may result in lemmas
+   * SygusSizeDecisionStrategy for m below. This may result in lemmas
    */
   void registerSizeTerm(Node e, std::vector<Node>& lemmas);
-  /** information for each measure term allocated by this class */
-  class SearchSizeInfo
+  /** A decision strategy for each measure term allocated by this class */
+  class SygusSizeDecisionStrategy : public DecisionStrategyFmf
   {
    public:
-    SearchSizeInfo( Node t, context::Context* c ) : d_this( t ), d_curr_search_size(0), d_curr_lit( c, 0 ) {}
+    SygusSizeDecisionStrategy(Node t, context::Context* c, Valuation valuation)
+        : DecisionStrategyFmf(c, valuation), d_this(t), d_curr_search_size(0)
+    {
+    }
     /** the measure term */
     Node d_this;
     /**
@@ -512,28 +509,13 @@ private:
      */
     Node getOrMkActiveMeasureValue(std::vector<Node>& lemmas,
                                    bool mkNew = false);
-    /**
-     * The current search size literal for this measure term. This corresponds
-     * to the minimial n such that (DT_SYGUS_BOUND d_this n) is asserted in
-     * this SAT context.
-     */
-    context::CDO< unsigned > d_curr_lit;
-    /**
-     * Map from integers n to the fairness literal, for each n such that this
-     * literal has been allocated (by getFairnessLiteral below).
-     */
-    std::map< unsigned, Node > d_lits;
-    /**
-     * Returns the s^th fairness literal for this measure term. This adds a
-     * split on this literal to lemmas.
-     */
-    Node getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas );
-    /** get the current fairness literal */
-    Node getCurrentFairnessLiteral( TheoryDatatypes * d, std::vector< Node >& lemmas ) { 
-      return getFairnessLiteral( d_curr_lit.get(), d, lemmas ); 
+    /** Returns the s^th fairness literal for this measure term. */
+    Node mkLiteral(unsigned s) override;
+    /** identify */
+    std::string identify() const override
+    {
+      return std::string("sygus_enum_size");
     }
-    /** increment current term size */
-    void incrementCurrentLiteral() { d_curr_lit.set( d_curr_lit.get() + 1 ); }
 
    private:
     /** the measure value */
@@ -542,11 +524,13 @@ private:
     Node d_measure_value_active;
   };
   /** the above information for each registered measure term */
-  std::map< Node, SearchSizeInfo * > d_szinfo;
+  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>> d_szinfo;
   /** map from enumerators (anchors) to their associated measure term */
   std::map< Node, Node > d_anchor_to_measure_term;
   /** map from enumerators (anchors) to their active guard*/
   std::map< Node, Node > d_anchor_to_active_guard;
+  /** map from enumerators (anchors) to a decision stratregy for that guard */
+  std::map<Node, std::unique_ptr<DecisionStrategy>> d_anchor_to_ag_strategy;
   /** generic measure term
    *
    * This is a global term that is used as the measure term for all sygus
@@ -571,7 +555,7 @@ private:
    * incrementSearchSize so far is at least s.
    */
   void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas );
-  /** Allocates a SearchSizeInfo object in d_szinfo. */
+  /** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */
   void registerMeasureTerm( Node m );
   /**
    * Return the current search size for arbitrary term n. This is the current
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 9c7365ac1..b83e9616a 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -7,7 +7,7 @@
 theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
 typechecker "theory/datatypes/theory_datatypes_type_rules.h"
 
-properties check presolve parametric propagate getNextDecisionRequest
+properties check presolve parametric propagate
 
 rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 283c70ada..10328c653 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2238,17 +2238,6 @@ std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const Entailme
   return make_pair(false, Node::null());
 }
 
-Node TheoryDatatypes::getNextDecisionRequest( unsigned& priority ) {
-  if( d_sygus_sym_break ){
-    std::vector< Node > lemmas;
-    Node ret = d_sygus_sym_break->getNextDecisionRequest( priority, lemmas );
-    doSendLemmas( lemmas );
-    return ret;
-  }else{
-    return Node::null();
-  }
-}
-
 } /* namepsace CVC4::theory::datatypes */
 } /* namepsace CVC4::theory */
 } /* namepsace CVC4 */
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 233ebd052..de2863718 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -346,8 +346,6 @@ private:
  /** sygus symmetry breaking utility */
  SygusSymBreakNew* d_sygus_sym_break;
 
-public:
- Node getNextDecisionRequest(unsigned& priority) override;
 };/* class TheoryDatatypes */
 
 }/* CVC4::theory::datatypes namespace */