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);
}
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(
// 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)
// 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);
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
{
// 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")
projects / cvc5.git / commitdiff