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