diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-27 21:07:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-27 21:07:13 -0500 |
commit | 453de9df0af984491f6ced883220fdbf113f078b (patch) | |
tree | 94e6bcd728add7e81844cb4a70b366de6fd72380 | |
parent | 9b9ecdf85954e937bd569cba018b6b09eee787a1 (diff) |
Fixes for get-abduct (#3229)
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 34 |
2 files changed, 23 insertions, 20 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1827d902c..3c10516e4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5127,7 +5127,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) } Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj << std::endl; - std::vector<Expr> easserts = getAssertions(); + std::vector<Expr> easserts = getExpandedAssertions(); std::vector<Node> axioms; for (unsigned i = 0, size = easserts.size(); i < size; i++) { @@ -5135,7 +5135,12 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) } std::vector<Node> asserts(axioms.begin(), axioms.end()); // negate the conjecture - Node conjn = Node::fromExpr(conj).negate(); + Node conjn = Node::fromExpr(conj); + // must expand definitions + std::unordered_map<Node, Node, NodeHashFunction> cache; + conjn = d_private->expandDefinitions(conjn, cache); + // now negate + conjn = conjn.negate(); d_abdConj = conjn.toExpr(); asserts.push_back(conjn); std::string name("A"); diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 4f6219343..7e72ecb41 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -278,24 +278,22 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); std::vector<Node> iplc; iplc.push_back(instAttr); - if (!axioms.empty()) - { - Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms); - aconj = - aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); - Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; - Node sc = nm->mkNode(AND, aconj, abdApp); - Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); - sc = nm->mkNode(EXISTS, vbvl, sc); - Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); - sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); - instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); - // build in the side condition - // exists x. A( x ) ^ input_axioms( x ) - // as an additional annotation on the sygus conjecture. In other words, - // the abducts A we procedure must be consistent with our axioms. - iplc.push_back(instAttr); - } + Node aconj = axioms.size() == 0 + ? nm->mkConst(true) + : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms)); + aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl; + Node sc = nm->mkNode(AND, aconj, abdApp); + Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars); + sc = nm->mkNode(EXISTS, vbvl, sc); + Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType()); + sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); + instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar); + // build in the side condition + // exists x. A( x ) ^ input_axioms( x ) + // as an additional annotation on the sygus conjecture. In other words, + // the abducts A we procedure must be consistent with our axioms. + iplc.push_back(instAttr); Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc); Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd); |