Support symbolic unfolding in UNIF+PI (#3553)

3 files changed, 94 insertions, 22 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 8da328eb6..2bc412361 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -458,28 +458,31 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     if (d_virtual_enum.isNull())
     {
       // we construct the default integer grammar with no variables, e.g.:
-      //   A -> 0 | 1 | A+A
+      //   A -> 1 | A+A
       TypeNode intTn = nm->integerType();
       // use a null variable list
       Node bvl;
-      std::stringstream ss;
-      ss << "_virtual_enum_grammar";
-      std::string virtualEnumName(ss.str());
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
-          exclude_cons;
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
-          include_cons;
-      // do not include "-", which is included by default for integers
-      exclude_cons[intTn].insert(nm->operatorOf(MINUS));
-      std::unordered_set<Node, NodeHashFunction> term_irrelevant;
-      TypeNode vtn = CegGrammarConstructor::mkSygusDefaultType(intTn,
-                                                               bvl,
-                                                               virtualEnumName,
-                                                               extra_cons,
-                                                               exclude_cons,
-                                                               include_cons,
-                                                               term_irrelevant);
+      std::string veName("_virtual_enum_grammar");
+      SygusDatatype sdt(veName);
+      TypeNode u = nm->mkSort(veName, ExprManager::SORT_FLAG_PLACEHOLDER);
+      std::set<Type> unresolvedTypes;
+      unresolvedTypes.insert(u.toType());
+      std::vector<TypeNode> cargsEmpty;
+      Node cr = nm->mkConst(Rational(1));
+      sdt.addConstructor(cr, "1", cargsEmpty);
+      std::vector<TypeNode> cargsPlus;
+      cargsPlus.push_back(u);
+      cargsPlus.push_back(u);
+      sdt.addConstructor(PLUS, cargsPlus);
+      sdt.initializeDatatype(nm->integerType(), bvl, false, false);
+      std::vector<Datatype> datatypes;
+      datatypes.push_back(sdt.getDatatype());
+      std::vector<DatatypeType> dtypes =
+          nm->toExprManager()->mkMutualDatatypeTypes(
+              datatypes,
+              unresolvedTypes,
+              ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+      TypeNode vtn = TypeNode::fromType(dtypes[0]);
       d_virtual_enum = nm->mkSkolem("_ve", vtn);
       d_tds->registerEnumerator(
           d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
@@ -636,7 +639,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
-  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false);
+  bool useSymCons = options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE;
+  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, useSymCons);
 }
 
 void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 84b160bb3..4727ab0b0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -1045,7 +1045,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         // add it as a constructor
         std::stringstream ssop;
         ssop << "monomial_" << sdc.d_name;
-        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc);
+        // we use 0 as the weight, since this constructor should be seen as
+        // a generalization of a non-Boolean variable (which has weight 0).
+        // This ensures that e.g. ( c1*x >= 0 ) has the same weight as
+        // ( x >= 0 ).
+        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, spc, 0);
       }
     }
     if (polynomialGrammar)
@@ -1053,6 +1057,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // add the constant
       Node coeff = nm->mkBoundVar(types[i]);
       lambdaVars.push_back(coeff);
+      sumChildren.push_back(coeff);
       cargsAnyTerm.push_back(unresAnyConst);
       // make the sygus operator lambda X. c1*t1 + ... + cn*tn + c
       Assert(sumChildren.size() > 1);
@@ -1069,7 +1074,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
       // make the any term datatype, add to back
       // do not consider the exclusion criteria of the generator
-      sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, spc);
+      // we use 0 as the weight, since this constructor should be seen as
+      // a simultaneous generalization of set of non-Boolean variables.
+      // 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);
     }
     else
     {
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 1a491394f..1ad33d5e7 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -804,6 +804,65 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
       // this violates the invariant that the i^th conditional enumerator
       // resolves the i^th separation conflict
       exp_conflict = true;
+      SygusTypeInfo& ti = d_unif->d_tds->getTypeInfo(ce.getType());
+      // The reasoning below is only necessary if we use symbolic constructors.
+      if (!ti.hasSubtermSymbolicCons())
+      {
+        break;
+      }
+      // Since the explanation of the condition (c_exp above) does not account
+      // for builtin subterms, we additionally require that the valuation of
+      // the condition is indeed different on the two points.
+      // For example, say ce has model value equal to the SyGuS datatype term:
+      //   C_leq_xy( 0, 1 )
+      // where C_leq_xy is a SyGuS datatype constructor taking two integer
+      // constants c_x and c_y, and whose builtin version is:
+      //   (0*x + 1*y >= 0)
+      // Then, c_exp above is:
+      //   is-C_leq_xy( ce )
+      // which is added to our explanation of the conflict, which does not
+      // account for the values of the arguments of C_leq_xy.
+      // Now, say that we are in a separation conflict due to f(1,2) and f(2,3)
+      // being assigned different values; the value of ce does not separate
+      // these two terms since:
+      //   (y>=0) { x -> 1, y -> 2 } = (y>=0) { x -> 2, y -> 3 } = true
+      // The code below adds a constraint that states that the above values are
+      // the same, which is part of the reason for the conflict. In the above
+      // example, we generate:
+      //   (DT_SYGUS_EVAL ce 1 2) == (DT_SYGUS_EVAL ce 2 3) { ce -> M(ce) }
+      // which unfolds via the SygusEvalUnfold utility to:
+      //   ( (c_x ce)*1 + (c_y ce)*2 >= 0 ) == ( (c_x ce)*2 + (c_y ce)*3 >= 0 )
+      // where c_x and c_y are the selectors of the subfields of C_leq_xy.
+      Trace("sygus-unif-sol-sym")
+          << "Explain symbolic separation conflict" << std::endl;
+      std::map<Node, std::vector<Node>>::iterator ith;
+      Node ceApp[2];
+      SygusEvalUnfold* eunf = d_unif->d_tds->getEvalUnfold();
+      std::map<Node, Node> vtm;
+      vtm[ce] = cv;
+      Trace("sygus-unif-sol-sym")
+          << "Model value for " << ce << " is " << cv << std::endl;
+      for (unsigned r = 0; r < 2; r++)
+      {
+        std::vector<Node> cechildren;
+        cechildren.push_back(ce);
+        Node ecurr = r == 0 ? e : er;
+        ith = d_unif->d_hd_to_pt.find(e);
+        AlwaysAssert(ith != d_unif->d_hd_to_pt.end());
+        cechildren.insert(
+            cechildren.end(), ith->second.begin(), ith->second.end());
+        Node cea = nm->mkNode(DT_SYGUS_EVAL, cechildren);
+        Trace("sygus-unif-sol-sym")
+            << "Sep conflict app #" << r << " : " << cea << std::endl;
+        std::vector<Node> tmpExp;
+        cea = eunf->unfold(cea, vtm, tmpExp, true, true);
+        Trace("sygus-unif-sol-sym") << "Unfolded to : " << cea << std::endl;
+        ceApp[r] = cea;
+      }
+      Node ceAppEq = ceApp[0].eqNode(ceApp[1]);
+      Trace("sygus-unif-sol-sym")
+          << "Sep conflict app explanation is : " << ceAppEq << std::endl;
+      exp.push_back(ceAppEq);
       break;
     }
     Trace("sygus-unif-sol")