Option to force return values of Bool functions to be constant in CegisUnif (#1930)

6 files changed, 147 insertions, 44 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 691b2fef4..d784447c6 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -968,6 +968,14 @@ header = "options/quantifiers_options.h"
   help       = "Unification-based function synthesis"
 
 [[option]]
+  name       = "sygusBoolIteReturnConst"
+  category   = "regular"
+  long       = "sygus-bool-ite-return-const"
+  type       = "bool"
+  default    = "false"
+  help       = "Only use Boolean constants for return values in unification-based function synthesis"
+
+[[option]]
   name       = "sygusQePreproc"
   category   = "regular"
   long       = "sygus-qe-preproc"
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 9ae598f83..692055b87 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -37,7 +37,6 @@ bool CegisUnif::processInitialize(Node n,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& lemmas)
 {
-  Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
   // list of strategy points for unification candidates
   std::vector<Node> unif_candidate_pts;
   // map from strategy points to their conditions
@@ -453,24 +452,10 @@ void CegisUnifEnumManager::incrementNumEnumerators()
                                  << " to strategy point " << ci.second.d_pt
                                  << "\n";
         d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
-        // if the sygus datatype is interpreted as an infinite type
-        // (this should be the case for almost all examples)
-        TypeNode et = e.getType();
-        if (!et.isInterpretedFinite())
-        {
-          // it is disequal from all previous ones
-          for (const Node& ei : ci.second.d_enums[index])
-          {
-            if (ei == e)
-            {
-              continue;
-            }
-            Node deq = e.eqNode(ei).negate();
-            Trace("cegis-unif-enum-lemma")
-                << "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
-            d_qe->getOutputChannel().lemma(deq);
-          }
-        }
+        // TODO symmetry breaking for making
+        //   e distinct from ei : (ci.second.d_enums[index] \ {e})
+        // if its respective type has had at least
+        // ci.second.d_enums[index].size() distinct values enumerated
       }
     }
     // register the evaluation points at the new value
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index f331d8fc6..412d1b211 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -619,18 +619,18 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       cargs.push_back( std::vector< CVC4::Type >() );
     }
   }
-  //add constants if no variables and no connected types
-  if( ops.back().empty() && types.empty() ){
-    std::vector< Node > consts;
-    mkSygusConstantsForType( btype, consts );
-    for( unsigned j=0; j<consts.size(); j++ ){
-      std::stringstream ss;
-      ss << consts[j];
-      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
-      ops.back().push_back( consts[j].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
+  //add constants
+  std::vector<Node> consts;
+  mkSygusConstantsForType(btype, consts);
+  for (unsigned j = 0; j < consts.size(); j++)
+  {
+    std::stringstream ss;
+    ss << consts[j];
+    Trace("sygus-grammar-def") << "...add for constant " << ss.str()
+                               << std::endl;
+    ops.back().push_back(consts[j].toExpr());
+    cnames.push_back(ss.str());
+    cargs.push_back(std::vector<CVC4::Type>());
   }
   //add operators
   for (unsigned i = 0; i < 4; i++)
@@ -638,6 +638,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     CVC4::Kind k = i == 0
                        ? kind::NOT
                        : (i == 1 ? kind::AND : (i == 2 ? kind::OR : kind::ITE));
+    // TODO #1935 ITEs are added to Boolean grammars so that we can infer
+    // unification strategies. We can do away with this if we can infer
+    // unification strategies from and/or/not
+    if (k == ITE && !options::sygusUnif())
+    {
+      continue;
+    }
     Trace("sygus-grammar-def") << "...add for " << k << std::endl;
     ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
     cnames.push_back(kind::kindToString(k));
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 3fbb4b2b7..be8d6c5ca 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
 #include "options/base_options.h"
+#include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -38,7 +39,12 @@ void SygusUnifRl::initializeCandidate(
   SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas);
   // based on the strategy inferred for each function, determine if we are
   // using a unification strategy that is compatible our approach.
-  d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+  StrategyRestrictions restrictions;
+  if (options::sygusBoolIteReturnConst())
+  {
+    restrictions.d_iteReturnBoolConst = true;
+  }
+  d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions);
   registerStrategy(f, enums);
   // Copy candidates and check whether CegisUnif for any of them
   if (d_unif_candidates.find(f) != d_unif_candidates.end())
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 855922fc5..0ecf01b74 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -683,6 +683,14 @@ bool SygusUnifStrategy::inferTemplate(
 void SygusUnifStrategy::staticLearnRedundantOps(
     std::map<Node, std::vector<Node>>& strategy_lemmas)
 {
+  StrategyRestrictions restrictions;
+  staticLearnRedundantOps(strategy_lemmas, restrictions);
+}
+
+void SygusUnifStrategy::staticLearnRedundantOps(
+    std::map<Node, std::vector<Node>>& strategy_lemmas,
+    StrategyRestrictions& restrictions)
+{
   for (unsigned i = 0; i < d_esym_list.size(); i++)
   {
     Node e = d_esym_list[i];
@@ -710,7 +718,8 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   debugPrint("sygus-unif");
   std::map<Node, std::map<NodeRole, bool> > visited;
   std::map<Node, std::map<unsigned, bool> > needs_cons;
-  staticLearnRedundantOps(getRootEnumerator(), role_equal, visited, needs_cons);
+  staticLearnRedundantOps(
+      getRootEnumerator(), role_equal, visited, needs_cons, restrictions);
   // now, check the needs_cons map
   for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
   {
@@ -753,8 +762,9 @@ void SygusUnifStrategy::debugPrint(const char* c)
 void SygusUnifStrategy::staticLearnRedundantOps(
     Node e,
     NodeRole nrole,
-    std::map<Node, std::map<NodeRole, bool> >& visited,
-    std::map<Node, std::map<unsigned, bool> >& needs_cons)
+    std::map<Node, std::map<NodeRole, bool>>& visited,
+    std::map<Node, std::map<unsigned, bool>>& needs_cons,
+    StrategyRestrictions& restrictions)
 {
   if (visited[e].find(nrole) != visited[e].end())
   {
@@ -778,26 +788,81 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
   {
     EnumTypeInfoStrat* etis = snode.d_strats[j];
-    int cindex = Datatype::indexOf(etis->d_cons.toExpr());
-    Assert(cindex != -1);
-    Trace("sygus-strat-slearn")
-        << "...by strategy, can exclude operator " << etis->d_cons << std::endl;
-    needs_cons_curr[static_cast<unsigned>(cindex)] = false;
+    unsigned cindex =
+        static_cast<unsigned>(Datatype::indexOf(etis->d_cons.toExpr()));
+    Trace("sygus-strat-slearn") << "...by strategy, can exclude operator "
+                                << etis->d_cons << std::endl;
+    needs_cons_curr[cindex] = false;
+    // try to eliminate from etn's datatype all operators except TRUE/FALSE if
+    // arguments of ITE are the same BOOL type
+    if (restrictions.d_iteReturnBoolConst)
+    {
+      const Datatype& dt =
+          static_cast<DatatypeType>(etn.toType()).getDatatype();
+      Node op = Node::fromExpr(dt[cindex].getSygusOp());
+      TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
+      if (op.getKind() == kind::BUILTIN
+          && NodeManager::operatorToKind(op) == ITE
+          && sygus_tn.isBoolean()
+          && (TypeNode::fromType(dt[cindex].getArgType(1))
+              == TypeNode::fromType(dt[cindex].getArgType(2))))
+      {
+        unsigned ncons = dt.getNumConstructors(), indexT = ncons,
+                 indexF = ncons;
+        for (unsigned k = 0; k < ncons; ++k)
+        {
+          Node op_arg = Node::fromExpr(dt[k].getSygusOp());
+          if (dt[k].getNumArgs() > 0 || !op_arg.isConst())
+          {
+            continue;
+          }
+          if (op_arg.getConst<bool>())
+          {
+            indexT = k;
+          }
+          else
+          {
+            indexF = k;
+          }
+        }
+        if (indexT < ncons && indexF < ncons)
+        {
+          Trace("sygus-strat-slearn")
+              << "...for ite boolean arg, can exclude all operators but T/F\n";
+          for (unsigned k = 0; k < ncons; ++k)
+          {
+            needs_cons_curr[k] = false;
+          }
+          needs_cons_curr[indexT] = true;
+          needs_cons_curr[indexF] = true;
+        }
+      }
+    }
     for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
-      staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons);
+      staticLearnRedundantOps(
+          cec.first, cec.second, visited, needs_cons, restrictions);
     }
   }
   // get the current datatype
   const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
   // do not use recursive Boolean connectives for conditions of ITEs
-  if (nrole == role_ite_condition)
+  if (nrole == role_ite_condition && restrictions.d_iteCondOnlyAtoms)
   {
+    TypeNode sygus_tn = TypeNode::fromType(dt.getSygusType());
     for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
     {
       Node op = Node::fromExpr(dt[j].getSygusOp());
       Trace("sygus-strat-slearn")
           << "...for ite condition, look at operator : " << op << std::endl;
+      if (op.isConst() && dt[j].getNumArgs() == 0)
+      {
+        Trace("sygus-strat-slearn")
+            << "...for ite condition, can exclude Boolean constant " << op
+            << std::endl;
+        needs_cons_curr[j] = false;
+        continue;
+      }
       if (op.getKind() == kind::BUILTIN)
       {
         Kind k = NodeManager::operatorToKind(op);
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index a24e323e8..43919d68e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -238,6 +238,27 @@ class EnumTypeInfoStrat
 };
 
 /**
+ * flags for extra restrictions to be inferred during redundant operators
+ * learning
+ */
+struct StrategyRestrictions
+{
+  StrategyRestrictions() : d_iteReturnBoolConst(false), d_iteCondOnlyAtoms(true)
+  {
+  }
+  /**
+   * if this flag is true then staticLearnRedundantOps will also try to make
+   * the return value of boolean ITEs to be restricted to constants
+   */
+  bool d_iteReturnBoolConst;
+  /**
+   * if this flag is true then staticLearnRedundantOps will also try to make
+   * the condition values of ITEs to be restricted to atoms
+   */
+  bool d_iteCondOnlyAtoms;
+};
+
+/**
  * Stores strategy and enumeration information for a function-to-synthesize.
  *
  * When this class is initialized, we construct a "strategy tree" based on
@@ -279,6 +300,16 @@ class SygusUnifStrategy
    * These may correspond to static symmetry breaking predicates (for example,
    * those that exclude ITE from enumerators whose role is enum_io when the
    * strategy is ITE_strat).
+   *
+   * then the module may also try to apply the given pruning restrictions (see
+   * StrategyRestrictions for more details)
+   */
+  void staticLearnRedundantOps(
+      std::map<Node, std::vector<Node>>& strategy_lemmas,
+      StrategyRestrictions& restrictions);
+  /**
+   * creates the default restrictions when they are not given and calls the
+   * above function
    */
   void staticLearnRedundantOps(
       std::map<Node, std::vector<Node>>& strategy_lemmas);
@@ -353,8 +384,9 @@ class SygusUnifStrategy
   void staticLearnRedundantOps(
       Node e,
       NodeRole nrole,
-      std::map<Node, std::map<NodeRole, bool> >& visited,
-      std::map<Node, std::map<unsigned, bool> >& needs_cons);
+      std::map<Node, std::map<NodeRole, bool>>& visited,
+      std::map<Node, std::map<unsigned, bool>>& needs_cons,
+      StrategyRestrictions& restrictions);
   /** finish initialization of the strategy tree
    *
    * (e, nrole) specify the strategy node in the graph we are currently