diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 15:08:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 15:08:00 -0500 |
commit | 72281a35622ae4656d3a2e4cd29e42cb96eba205 (patch) | |
tree | 1182a067911c1d7c2314fce70b76f0171c57ee3c /src/smt/smt_engine.cpp | |
parent | 9e654bc0105b04d08e8c0fb555a212228cab2c9d (diff) |
Track sygus variable to term relationship via attribute (#3182)
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 29 |
1 files changed, 16 insertions, 13 deletions
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<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(); |