From: Andrew Reynolds Date: Wed, 11 Dec 2019 16:07:25 +0000 (-0600) Subject: Support symbolic unfolding in UNIF+PI (#3553) X-Git-Tag: cvc5-1.0.0~3776 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b12f67c710d359cd57d09dbff67f13bf26e10834;p=cvc5.git Support symbolic unfolding in UNIF+PI (#3553) --- 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> extra_cons; - std::map> - exclude_cons; - std::map> - include_cons; - // do not include "-", which is included by default for integers - exclude_cons[intTn].insert(nm->operatorOf(MINUS)); - std::unordered_set 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 unresolvedTypes; + unresolvedTypes.insert(u.toType()); + std::vector cargsEmpty; + Node cr = nm->mkConst(Rational(1)); + sdt.addConstructor(cr, "1", cargsEmpty); + std::vector cargsPlus; + cargsPlus.push_back(u); + cargsPlus.push_back(u); + sdt.addConstructor(PLUS, cargsPlus); + sdt.initializeDatatype(nm->integerType(), bvl, false, false); + std::vector datatypes; + datatypes.push_back(sdt.getDatatype()); + std::vector 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>::iterator ith; + Node ceApp[2]; + SygusEvalUnfold* eunf = d_unif->d_tds->getEvalUnfold(); + std::map 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 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 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")