Improve polynomial anyterm grammar (#3566)

This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation.

This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).

3 files changed, 118 insertions, 20 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 1adc3123e..8df43087f 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -487,6 +487,37 @@ bool CegGrammarConstructor::isHandledType(TypeNode t)
   return true;
 }
 
+Node CegGrammarConstructor::createLambdaWithZeroArg(
+    Kind k, TypeNode bArgType, std::shared_ptr<SygusPrintCallback> spc)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> opLArgs;
+  std::vector<Expr> opLArgsExpr;
+  // get the builtin type
+  opLArgs.push_back(nm->mkBoundVar(bArgType));
+  opLArgsExpr.push_back(opLArgs.back().toExpr());
+  // build zarg
+  Node zarg;
+  Assert(bArgType.isReal() || bArgType.isBitVector());
+  if (bArgType.isReal())
+  {
+    zarg = nm->mkConst(Rational(0));
+  }
+  else
+  {
+    unsigned size = bArgType.getBitVectorSize();
+    zarg = bv::utils::mkZero(size);
+  }
+  Node body = nm->mkNode(k, zarg, opLArgs.back());
+  // use a print callback since we do not want to print the lambda
+  spc = std::make_shared<printer::SygusExprPrintCallback>(body.toExpr(),
+                                                          opLArgsExpr);
+  // create operator
+  Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body);
+  Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n";
+  return op;
+}
+
 void CegGrammarConstructor::mkSygusDefaultGrammar(
     TypeNode range,
     Node bvl,
@@ -543,7 +574,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator
       itc;
   // maps types to the index of its "any term" grammar construction
-  std::map<TypeNode, unsigned> typeToGAnyTerm;
+  std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm;
   options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
@@ -589,7 +620,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   // we construct the grammar for the Boolean type last.
   for (int i = (types.size() - 2); i >= 0; --i)
   {
-    Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
+    Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " "
+                               << unres_types[i] << std::endl;
     TypeNode unres_t = unres_types[i];
     options::SygusGrammarConsMode tsgcm = sgcm;
     if (tsgcm == options::SygusGrammarConsMode::ANY_TERM
@@ -606,12 +638,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       {
         // Add a placeholder for the "any term" version of this datatype, to be
         // constructed later.
-        typeToGAnyTerm[types[i]] = sdts.size();
         std::stringstream ssat;
         ssat << sdts[i].d_sdt.getName() << "_any_term";
         sdts.push_back(SygusDatatypeGenerator(ssat.str()));
         TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres);
         unres_types.push_back(unresAnyTerm);
+        // set tracking information for later addition at boolean type.
+        std::pair<unsigned, bool> p(sdts.size() - 1, false);
+        typeToGAnyTerm[types[i]] = p;
       }
     }
     Trace("sygus-grammar-def")
@@ -916,7 +950,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     cargsIte.push_back(unres_t);
     sdts[i].addConstructor(k, cargsIte);
   }
-  std::map<TypeNode, unsigned>::iterator itgat;
+  std::map<TypeNode, std::pair<unsigned, bool>>::iterator itgat;
   // initialize the datatypes (except for the last one, reserved for Bool)
   for (unsigned i = 0, size = types.size() - 1; i < size; ++i)
   {
@@ -933,9 +967,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // no any term datatype, we are done
       continue;
     }
+    unsigned iat = itgat->second.first;
     Trace("sygus-grammar-def")
         << "Build any-term datatype for " << types[i] << "..." << std::endl;
-    unsigned iat = itgat->second;
+
     // for now, only real has any term construction
     Assert(types[i].isReal());
     // We have initialized the given type sdts[i], which should now contain
@@ -1132,6 +1167,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as
       // e.g. ( x >= 0 ) or ( y >= 0 ).
       sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc, 0);
+      // mark that predicates should be of the form (= pol 0) and (<= pol 0)
+      itgat->second.second = true;
     }
     else
     {
@@ -1193,34 +1230,76 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       continue;
     }
     unsigned iuse = i;
-    // use the any-term type if it exists
+    bool zarg = false;
+    // use the any-term type if it exists and a zero argument if it is a
+    // polynomial grammar
     itgat = typeToGAnyTerm.find(types[i]);
     if (itgat != typeToGAnyTerm.end())
     {
-      iuse = itgat->second;
+      iuse = itgat->second.first;
+      zarg = itgat->second.second;
+      Trace("sygus-grammar-def")
+          << "...unres type " << unres_types[i] << " became "
+          << (!zarg ? "polynomial " : "") << "unres anyterm type "
+          << unres_types[iuse] << "\n";
     }
     Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
     //add equality per type
     Kind k = EQUAL;
     Trace("sygus-grammar-def") << "...add for " << k << std::endl;
     std::stringstream ss;
-    ss << kindToString(k) << "_" << types[i];
-    std::vector<TypeNode> cargsBinary;
-    cargsBinary.push_back(unres_types[iuse]);
-    cargsBinary.push_back(unres_types[iuse]);
-    sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargsBinary);
+    std::vector<TypeNode> cargs;
+    cargs.push_back(unres_types[iuse]);
+    // if polynomial grammar, generate (= anyterm 0) and (<= anyterm 0) as the
+    // predicates
+    if (zarg)
+    {
+      std::shared_ptr<SygusPrintCallback> spc;
+      Node op = createLambdaWithZeroArg(k, types[i], spc);
+      ss << "eq_" << types[i];
+      sdtBool.addConstructor(op, ss.str(), cargs);
+    }
+    else
+    {
+      ss << kindToString(k) << "_" << types[i];
+      cargs.push_back(unres_types[iuse]);
+      sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargs);
+      cargs.pop_back();
+    }
     // type specific predicates
+    std::shared_ptr<SygusPrintCallback> spc;
+    std::stringstream ssop;
     if (types[i].isReal())
     {
       Kind kind = LEQ;
-      Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
-      sdtBool.addConstructor(kind, cargsBinary);
+      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+      if (zarg)
+      {
+        Node op = createLambdaWithZeroArg(kind, types[i], spc);
+        ssop << "leq_" << types[i];
+        sdtBool.addConstructor(op, ssop.str(), cargs);
+      }
+      else
+      {
+        cargs.push_back(unres_types[iuse]);
+        sdtBool.addConstructor(kind, cargs);
+      }
     }
     else if (types[i].isBitVector())
     {
       Kind kind = BITVECTOR_ULT;
-      Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
-      sdtBool.addConstructor(kind, cargsBinary);
+      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+      if (zarg)
+      {
+        Node op = createLambdaWithZeroArg(kind, types[i], spc);
+        ssop << "leq_" << types[i];
+        sdtBool.addConstructor(op, ssop.str(), cargs);
+      }
+      else
+      {
+        cargs.push_back(unres_types[iuse]);
+        sdtBool.addConstructor(kind, cargs);
+      }
     }
     else if (types[i].isDatatype())
     {
@@ -1254,6 +1333,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   }
   // add Boolean connectives, if not in a degenerate case of (recursively)
   // having only constant constructors
+  Trace("sygus-grammar-def")
+      << "...add Boolean connectives for unres type " << unres_bt << std::endl;
   if (sdtBool.d_sdt.getNumConstructors() > consts.size())
   {
     for (unsigned i = 0; i < 4; i++)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 1abe8bf5f..b0c575809 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -100,7 +100,7 @@ public:
   *   - term_irrelevant: a set of terms that should not be included in the
   *      grammar.
   *   - include_cons: a set of operators such that if this set is not empty,
-  *     its elements that are in the default grammar (and only them) 
+  *     its elements that are in the default grammar (and only them)
   *     will be included.
   */
  static TypeNode mkSygusDefaultType(
@@ -248,8 +248,25 @@ public:
       std::set<Type>& unres);
 
   // helper function for mkSygusTemplateType
-  static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, 
-                                          const std::string& fun, unsigned& tcount );
+  static TypeNode mkSygusTemplateTypeRec(Node templ,
+                                         Node templ_arg,
+                                         TypeNode templ_arg_sygus_type,
+                                         Node bvl,
+                                         const std::string& fun,
+                                         unsigned& tcount);
+
+  /**
+   * Given a kind k, create a lambda operator with the given builtin input type
+   * and an extra zero argument of that same type.  For example, for k = LEQ and
+   * bArgType = Int, the operator will be lambda x : Int. x + 0.  Currently the
+   * supported input types are Real (thus also Int) and BitVector.
+   *
+   * This method also creates a print callback for the operator, saved via the
+   * argument spc, if the caller wishes to not print the lambda.
+   */
+  static Node createLambdaWithZeroArg(Kind k,
+                                      TypeNode bArgType,
+                                      std::shared_ptr<SygusPrintCallback> spc);
   //---------------- end grammar construction
 };
 
diff --git a/test/regress/regress1/sygus/issue3507.smt2 b/test/regress/regress1/sygus/issue3507.smt2
index aca7a61b0..c8700f37b 100644
--- a/test/regress/regress1/sygus/issue3507.smt2
+++ b/test/regress/regress1/sygus/issue3507.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --uf-ho
+; COMMAND-LINE: --sygus-inference --uf-ho --quiet
 (set-logic ALL)
 (declare-fun f (Int) Bool)
 (declare-fun g (Int) Bool)