Node conjn = Node::fromExpr(conj).negate();
d_abdConj = conjn.toExpr();
asserts.push_back(conjn);
- d_sssfVarlist.clear();
- d_sssfSyms.clear();
std::string name("A");
Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture(
- name,
- asserts,
- axioms,
- TypeNode::fromType(grammarType),
- d_sssfVarlist,
- d_sssfSyms);
+ name, asserts, axioms, TypeNode::fromType(grammarType));
// should be a quantified conjecture with one function-to-synthesize
Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
// remember the abduct-to-synthesize
{
abdn = abdn[1];
}
- Assert(d_sssfVarlist.size() == d_sssfSyms.size());
+ // get the grammar type for the abduct
+ Node af = Node::fromExpr(d_sssf);
+ Node agdtbv = af.getAttribute(theory::SygusSynthFunVarListAttribute());
+ Assert(!agdtbv.isNull());
+ Assert(agdtbv.getKind() == kind::BOUND_VAR_LIST);
// convert back to original
// must replace formal arguments of abd with the free variables in the
// input problem that they correspond to.
- abdn = abdn.substitute(d_sssfVarlist.begin(),
- d_sssfVarlist.end(),
- d_sssfSyms.begin(),
- d_sssfSyms.end());
+ std::vector<Node> vars;
+ std::vector<Node> syms;
+ SygusVarToTermAttribute sta;
+ for (const Node& bv : agdtbv)
+ {
+ vars.push_back(bv);
+ syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
+ }
+ abdn =
+ abdn.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
// convert to expression
abd = abdn.toExpr();
* for. This is used for the get-abduct command.
*/
Expr d_sssf;
- /**
- * The substitution to apply to the solutions from the subsolver, used for
- * the get-abduct command.
- */
- std::vector<Node> d_sssfVarlist;
- std::vector<Node> d_sssfSyms;
/**
* The conjecture of the current abduction problem. This expression is only
* valid while we are in mode SMT_MODE_ABDUCT.
typedef expr::Attribute<SygusSideConditionAttributeId, Node>
SygusSideConditionAttribute;
+/** Attribute for indicating that a sygus variable encodes a term
+ *
+ * This is used, e.g., for abduction where the formal argument list of the
+ * abduct-to-synthesize corresponds to the free variables of the sygus
+ * problem.
+ */
+struct SygusVarToTermAttributeId
+{
+};
+typedef expr::Attribute<SygusVarToTermAttributeId, Node>
+ SygusVarToTermAttribute;
+
namespace quantifiers {
/** Attribute priority for rewrite rules */
Node SygusAbduct::mkAbductionConjecture(const std::string& name,
const std::vector<Node>& asserts,
const std::vector<Node>& axioms,
- TypeNode abdGType,
- std::vector<Node>& varlist,
- std::vector<Node>& syms)
+ TypeNode abdGType)
{
NodeManager* nm = NodeManager::currentNM();
std::unordered_set<Node, NodeHashFunction> symset;
<< "...finish, got " << symset.size() << " symbols." << std::endl;
Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
+ std::vector<Node> syms;
std::vector<Node> vars;
+ std::vector<Node> varlist;
std::vector<TypeNode> varlistTypes;
for (const Node& s : symset)
{
Node vlv = nm->mkBoundVar(ss.str(), tn);
varlist.push_back(vlv);
varlistTypes.push_back(tn);
+ // set that this variable encodes the term s
+ SygusVarToTermAttribute sta;
+ vlv.setAttribute(sta, s);
}
}
// make the sygus variable list
* The type abdGType (if non-null) is a sygus datatype type that encodes the
* grammar that should be used for solutions of the abduction conjecture.
*
- * The arguments varlist and syms specify the relationship between the free
- * variables of asserts and the formal argument list of the
- * abduct-to-synthesize. In particular, solutions to the synthesis conjecture
- * will be in the form of a closed term (lambda varlist. t). The intended
- * solution, which is a term whose free variables are a subset of asserts,
- * is the term t { varlist -> syms }.
+ * The relationship between the free variables of asserts and the formal
+ * rgument list of the abduct-to-synthesize are tracked by the attribute
+ * SygusVarToTermAttribute.
+ *
+ * In particular, solutions to the synthesis conjecture will be in the form
+ * of a closed term (lambda varlist. t). The intended solution, which is a
+ * term whose free variables are a subset of asserts, is the term
+ * t * { varlist -> SygusVarToTermAttribute(varlist) }.
*/
static Node mkAbductionConjecture(const std::string& name,
const std::vector<Node>& asserts,
const std::vector<Node>& axioms,
- TypeNode abdGType,
- std::vector<Node>& varlist,
- std::vector<Node>& syms);
+ TypeNode abdGType);
};
} // namespace quantifiers
{
return;
}
+ NodeManager* nm = NodeManager::currentNM();
for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
{
Node sol = sols[i];
if (is_unique_term)
{
out << "(define-fun " << f << " ";
- if (dt.getSygusVarList().isNull())
+ // Only include variables that are truly bound variables of the
+ // function-to-synthesize. This means we exclude variables that encode
+ // external terms. This ensures that --sygus-stream prints
+ // solutions with no arguments on the predicate for responses to
+ // the get-abduct command.
+ // pvs stores the variables that will be printed in the argument list
+ // below.
+ std::vector<Node> pvs;
+ Node vl = Node::fromExpr(dt.getSygusVarList());
+ if (!vl.isNull())
+ {
+ Assert(vl.getKind() == BOUND_VAR_LIST);
+ SygusVarToTermAttribute sta;
+ for (const Node& v : vl)
+ {
+ if (!v.hasAttribute(sta))
+ {
+ pvs.push_back(v);
+ }
+ }
+ }
+ if (pvs.empty())
{
out << "() ";
}
else
{
- out << dt.getSygusVarList() << " ";
+ vl = nm->mkNode(BOUND_VAR_LIST, pvs);
+ out << vl << " ";
}
out << dt.getSygusType() << " ";
if (status == 0)
projects / cvc5.git / commitdiff