Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)

6 files changed, 102 insertions, 25 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index bcd3a0784..d697a6aaf 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1141,6 +1141,12 @@ Expr DatatypeConstructor::getSelector(std::string name) const {
   return (*this)[name].getSelector();
 }
 
+Type DatatypeConstructor::getArgType(unsigned index) const
+{
+  PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+  return static_cast<SelectorType>((*this)[index].getType()).getRangeType();
+}
+
 bool DatatypeConstructor::involvesExternalType() const{
   for(const_iterator i = begin(); i != end(); ++i) {
     if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index fffabac77..826711897 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -390,6 +390,11 @@ class CVC4_PUBLIC DatatypeConstructor {
    * is returned.
    */
   Expr getSelector(std::string name) const;
+  /**
+   * Get argument type. Returns the return type of the i^th selector of this
+   * constructor.
+   */
+  Type getArgType(unsigned i) const;
 
   /** get selector internal
    *
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 7faeb0252..401ab03ee 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -179,21 +179,57 @@ bool CegConjecturePbe::initialize(Node n,
     std::map<Node, std::vector<Node>> strategy_lemmas;
     d_sygus_unif[c].initialize(
         d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas);
-    // collect lemmas from all strategies
-    for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
-    {
-      lemmas.insert(lemmas.end(), p.second.begin(), p.second.end());
-    }
     Assert(!d_candidate_to_enum[c].empty());
     Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
                        << " enumerators for " << c << "..." << std::endl;
+    // collect list per type of strategy points with strategy lemmas
+    std::map<TypeNode, std::vector<Node>> tn_to_strategy_pt;
+    for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
+    {
+      TypeNode tnsp = p.first.getType();
+      tn_to_strategy_pt[tnsp].push_back(p.first);
+    }
     // initialize the enumerators
+    NodeManager* nm = NodeManager::currentNM();
     for (const Node& e : d_candidate_to_enum[c])
     {
+      TypeNode etn = e.getType();
       d_tds->registerEnumerator(e, c, d_parent, true);
       Node g = d_tds->getActiveGuardForEnumerator(e);
       d_enum_to_active_guard[e] = g;
       d_enum_to_candidate[e] = c;
+      TNode te = e;
+      // initialize static symmetry breaking lemmas for it
+      // we register only one "master" enumerator per type
+      // thus, the strategy lemmas (which are for individual strategy points)
+      // are applicable (disjunctively) to the master enumerator
+      std::map<TypeNode, std::vector<Node>>::iterator itt =
+          tn_to_strategy_pt.find(etn);
+      if (itt != tn_to_strategy_pt.end())
+      {
+        std::vector<Node> disj;
+        for (const Node& sp : itt->second)
+        {
+          std::map<Node, std::vector<Node>>::iterator itsl =
+              strategy_lemmas.find(sp);
+          Assert(itsl != strategy_lemmas.end());
+          if (!itsl->second.empty())
+          {
+            TNode tsp = sp;
+            Node lem = itsl->second.size() == 1 ? itsl->second[0]
+                                                : nm->mkNode(AND, itsl->second);
+            if (tsp != te)
+            {
+              lem = lem.substitute(tsp, te);
+            }
+            disj.push_back(lem);
+          }
+        }
+        Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj);
+        Trace("sygus-pbe") << "  static redundant op lemma : " << lem
+                           << std::endl;
+        lemmas.push_back(lem);
+      }
     }
     Trace("sygus-pbe") << "Initialize " << d_examples[c].size()
                        << " example points for " << c << "..." << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index a3158fbe8..32af47c81 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -760,6 +760,8 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   {
     return;
   }
+  Trace("sygus-strat-slearn") << "Learn redundant operators " << e << " "
+                              << nrole << "..." << std::endl;
   visited[e][nrole] = true;
   EnumInfo& ei = getEnumInfo(e);
   if (ei.isTemplated())
@@ -769,34 +771,61 @@ void SygusUnifStrategy::staticLearnRedundantOps(
   TypeNode etn = e.getType();
   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
   StrategyNode& snode = tinfo.getStrategyNode(nrole);
-  if (snode.d_strats.empty())
-  {
-    return;
-  }
   std::map<unsigned, bool> needs_cons_curr;
-  // various strategies
+  // constructors that correspond to strategies are not needed
+  // the intuition is that the strategy itself is responsible for constructing
+  // all terms that use the given constructor
   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;
     for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
     {
       staticLearnRedundantOps(cec.first, cec.second, visited, needs_cons);
     }
   }
-  // get the master enumerator for the type of this enumerator
-  std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
-  if (itse == d_master_enum.end())
-  {
-    return;
-  }
-  Node em = itse->second;
-  Assert(!em.isNull());
   // get the current datatype
   const Datatype& dt = static_cast<DatatypeType>(etn.toType()).getDatatype();
-  // all constructors that are not a part of a strategy are needed
+  // do not use recursive Boolean connectives for conditions of ITEs
+  if (nrole == role_ite_condition)
+  {
+    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.getKind() == kind::BUILTIN)
+      {
+        Kind k = NodeManager::operatorToKind(op);
+        if (k == NOT || k == OR || k == AND)
+        {
+          // can eliminate if their argument types are simple loops to this type
+          bool type_ok = true;
+          for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+          {
+            TypeNode tn = TypeNode::fromType(dt[j].getArgType(k));
+            if (tn != etn)
+            {
+              type_ok = false;
+              break;
+            }
+          }
+          if (type_ok)
+          {
+            Trace("sygus-strat-slearn")
+                << "...for ite condition, can exclude Boolean connective : "
+                << op << std::endl;
+            needs_cons_curr[j] = false;
+          }
+        }
+      }
+    }
+  }
+  // all other constructors are needed
   for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
   {
     if (needs_cons_curr.find(j) == needs_cons_curr.end())
@@ -805,15 +834,15 @@ void SygusUnifStrategy::staticLearnRedundantOps(
     }
   }
   // update the constructors that the master enumerator needs
-  if (needs_cons.find(em) == needs_cons.end())
+  if (needs_cons.find(e) == needs_cons.end())
   {
-    needs_cons[em] = needs_cons_curr;
+    needs_cons[e] = needs_cons_curr;
   }
   else
   {
     for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
     {
-      needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
+      needs_cons[e][j] = needs_cons[e][j] || needs_cons_curr[j];
     }
   }
 }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 3121a4253..c45d4971e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1028,10 +1028,11 @@ bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
   }
 }
 
-TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i)
+TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
 {
   Assert(i < c.getNumArgs());
-  return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
+  return TypeNode::fromType(
+      static_cast<SelectorType>(c[i].getType()).getRangeType());
 }
 
 /** get first occurrence */
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index f108dfb8e..4a3dcb8d6 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -292,7 +292,7 @@ private:
   bool isKindArg( TypeNode tn, int i );
   bool isConstArg( TypeNode tn, int i );
   /** get arg type */
-  TypeNode getArgType(const DatatypeConstructor& c, unsigned i);
+  TypeNode getArgType(const DatatypeConstructor& c, unsigned i) const;
   /** get first occurrence */
   int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
   /** is type match */