From: Andrew Reynolds Date: Tue, 13 Aug 2019 20:08:00 +0000 (-0500) Subject: Track sygus variable to term relationship via attribute (#3182) X-Git-Tag: cvc5-1.0.0~4022 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=72281a35622ae4656d3a2e4cd29e42cb96eba205;p=cvc5.git Track sygus variable to term relationship via attribute (#3182) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e9c3f06ae..762b21fd8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5147,16 +5147,9 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) 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 @@ -5207,14 +5200,24 @@ bool SmtEngine::getAbductInternal(Expr& abd) { 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 vars; + std::vector 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(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f783b0a33..f032d202a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -169,12 +169,6 @@ class CVC4_PUBLIC SmtEngine { * 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 d_sssfVarlist; - std::vector d_sssfSyms; /** * The conjecture of the current abduction problem. This expression is only * valid while we are in mode SMT_MODE_ABDUCT. diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 329f9d08a..827c5e7f4 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -84,6 +84,18 @@ struct SygusSideConditionAttributeId typedef expr::Attribute 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 + SygusVarToTermAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 52fb60c06..4f6219343 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -35,9 +35,7 @@ SygusAbduct::SygusAbduct() {} Node SygusAbduct::mkAbductionConjecture(const std::string& name, const std::vector& asserts, const std::vector& axioms, - TypeNode abdGType, - std::vector& varlist, - std::vector& syms) + TypeNode abdGType) { NodeManager* nm = NodeManager::currentNM(); std::unordered_set symset; @@ -49,7 +47,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, << "...finish, got " << symset.size() << " symbols." << std::endl; Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl; + std::vector syms; std::vector vars; + std::vector varlist; std::vector varlistTypes; for (const Node& s : symset) { @@ -64,6 +64,9 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, 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 diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index d6bbd0e3f..2fdce542a 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -68,19 +68,19 @@ class SygusAbduct * 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& asserts, const std::vector& axioms, - TypeNode abdGType, - std::vector& varlist, - std::vector& syms); + TypeNode abdGType); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 41caf8c6c..b302c4657 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1017,6 +1017,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { return; } + NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++) { Node sol = sols[i]; @@ -1081,13 +1082,35 @@ void SynthConjecture::printSynthSolution(std::ostream& out) 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 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)