summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp113
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.h23
2 files changed, 117 insertions, 19 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
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback