diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-14 17:55:23 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-14 17:55:23 -0600 |
commit | bf385ca69a958e0939524d8fbcf988c1fb45d131 (patch) | |
tree | 469f60484b68df6ccd00cbc68320b1b18f2e0865 /src/theory/quantifiers/sygus/sygus_explain.cpp | |
parent | 3c730da7c39dc5cba11bdea99191e361e505bbc8 (diff) |
Quantifiers subdirectories (#1608)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_explain.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_explain.cpp | 301 |
1 files changed, 301 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp new file mode 100644 index 000000000..aafaa07e1 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -0,0 +1,301 @@ +/********************* */ +/*! \file sygus_explain.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of techniques for sygus explanations + **/ + +#include "theory/quantifiers/sygus/sygus_explain.h" + +#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" + +using namespace CVC4::kind; +using namespace std; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void TermRecBuild::addTerm(Node n) +{ + d_term.push_back(n); + std::vector<Node> currc; + d_kind.push_back(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + currc.push_back(n.getOperator()); + d_has_op.push_back(true); + } + else + { + d_has_op.push_back(false); + } + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + currc.push_back(n[i]); + } + d_children.push_back(currc); +} + +void TermRecBuild::init(Node n) +{ + Assert(d_term.empty()); + addTerm(n); +} + +void TermRecBuild::push(unsigned p) +{ + Assert(!d_term.empty()); + unsigned curr = d_term.size() - 1; + Assert(d_pos.size() == curr); + Assert(d_pos.size() + 1 == d_children.size()); + Assert(p < d_term[curr].getNumChildren()); + addTerm(d_term[curr][p]); + d_pos.push_back(p); +} + +void TermRecBuild::pop() +{ + Assert(!d_pos.empty()); + d_pos.pop_back(); + d_kind.pop_back(); + d_has_op.pop_back(); + d_children.pop_back(); + d_term.pop_back(); +} + +void TermRecBuild::replaceChild(unsigned i, Node r) +{ + Assert(!d_term.empty()); + unsigned curr = d_term.size() - 1; + unsigned o = d_has_op[curr] ? 1 : 0; + d_children[curr][i + o] = r; +} + +Node TermRecBuild::getChild(unsigned i) +{ + unsigned curr = d_term.size() - 1; + unsigned o = d_has_op[curr] ? 1 : 0; + return d_children[curr][i + o]; +} + +Node TermRecBuild::build(unsigned d) +{ + Assert(d_pos.size() + 1 == d_term.size()); + Assert(d < d_term.size()); + int p = d < d_pos.size() ? d_pos[d] : -2; + std::vector<Node> children; + unsigned o = d_has_op[d] ? 1 : 0; + for (unsigned i = 0; i < d_children[d].size(); i++) + { + Node nc; + if (p + o == i) + { + nc = build(d + 1); + } + else + { + nc = d_children[d][i]; + } + children.push_back(nc); + } + return NodeManager::currentNM()->mkNode(d_kind[d], children); +} + +void SygusExplain::getExplanationForConstantEquality(Node n, + Node vn, + std::vector<Node>& exp) +{ + std::map<unsigned, bool> cexc; + getExplanationForConstantEquality(n, vn, exp, cexc); +} + +void SygusExplain::getExplanationForConstantEquality( + Node n, Node vn, std::vector<Node>& exp, std::map<unsigned, bool>& cexc) +{ + Assert(vn.getKind() == kind::APPLY_CONSTRUCTOR); + Assert(n.getType() == vn.getType()); + TypeNode tn = n.getType(); + Assert(tn.isDatatype()); + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + int i = Datatype::indexOf(vn.getOperator().toExpr()); + Node tst = datatypes::DatatypesRewriter::mkTester(n, i, dt); + exp.push_back(tst); + for (unsigned j = 0; j < vn.getNumChildren(); j++) + { + if (cexc.find(j) == cexc.end()) + { + Node sel = NodeManager::currentNM()->mkNode( + kind::APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[i].getSelectorInternal(tn.toType(), j)), + n); + getExplanationForConstantEquality(sel, vn[j], exp); + } + } +} + +Node SygusExplain::getExplanationForConstantEquality(Node n, Node vn) +{ + std::map<unsigned, bool> cexc; + return getExplanationForConstantEquality(n, vn, cexc); +} + +Node SygusExplain::getExplanationForConstantEquality( + Node n, Node vn, std::map<unsigned, bool>& cexc) +{ + std::vector<Node> exp; + getExplanationForConstantEquality(n, vn, exp, cexc); + Assert(!exp.empty()); + return exp.size() == 1 ? exp[0] + : NodeManager::currentNM()->mkNode(kind::AND, exp); +} + +// we have ( n = vn => eval( n ) = bvr ) ^ vn != vnr , returns exp such that exp +// => ( eval( n ) = bvr ^ vn != vnr ) +void SygusExplain::getExplanationFor(TermRecBuild& trb, + Node n, + Node vn, + std::vector<Node>& exp, + std::map<TypeNode, int>& var_count, + SygusInvarianceTest& et, + Node vnr, + Node& vnr_exp, + int& sz) +{ + Assert(vnr.isNull() || vn != vnr); + Assert(vn.getKind() == APPLY_CONSTRUCTOR); + Assert(vnr.isNull() || vnr.getKind() == APPLY_CONSTRUCTOR); + Assert(n.getType() == vn.getType()); + TypeNode ntn = n.getType(); + std::map<unsigned, bool> cexc; + // for each child, + // check whether replacing that child by a fresh variable + // also satisfies the invariance test. + for (unsigned i = 0; i < vn.getNumChildren(); i++) + { + TypeNode xtn = vn[i].getType(); + Node x = d_tdb->getFreeVarInc(xtn, var_count); + trb.replaceChild(i, x); + Node nvn = trb.build(); + Assert(nvn.getKind() == kind::APPLY_CONSTRUCTOR); + if (et.is_invariant(d_tdb, nvn, x)) + { + cexc[i] = true; + // we are tracking term size if positive + if (sz >= 0) + { + int s = d_tdb->getSygusTermSize(vn[i]); + sz = sz - s; + } + } + else + { + trb.replaceChild(i, vn[i]); + } + } + const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); + int cindex = Datatype::indexOf(vn.getOperator().toExpr()); + Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors()); + Node tst = datatypes::DatatypesRewriter::mkTester(n, cindex, dt); + exp.push_back(tst); + // if the operator of vn is different than vnr, then disunification obligation + // is met + if (!vnr.isNull()) + { + if (vnr.getOperator() != vn.getOperator()) + { + vnr = Node::null(); + vnr_exp = NodeManager::currentNM()->mkConst(true); + } + } + for (unsigned i = 0; i < vn.getNumChildren(); i++) + { + Node sel = NodeManager::currentNM()->mkNode( + kind::APPLY_SELECTOR_TOTAL, + Node::fromExpr(dt[cindex].getSelectorInternal(ntn.toType(), i)), + n); + Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]); + if (cexc.find(i) == cexc.end()) + { + trb.push(i); + Node vnr_exp_c; + getExplanationFor( + trb, sel, vn[i], exp, var_count, et, vnr_c, vnr_exp_c, sz); + trb.pop(); + if (!vnr_c.isNull()) + { + Assert(!vnr_exp_c.isNull()); + if (vnr_exp_c.isConst() || vnr_exp.isNull()) + { + // recursively satisfied the disunification obligation + if (vnr_exp_c.isConst()) + { + // was successful, don't consider further + vnr = Node::null(); + } + vnr_exp = vnr_exp_c; + } + } + } + else + { + // if excluded, we may need to add the explanation for this + if (vnr_exp.isNull() && !vnr_c.isNull()) + { + vnr_exp = getExplanationForConstantEquality(sel, vnr[i]); + } + } + } +} + +void SygusExplain::getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et, + Node vnr, + unsigned& sz) +{ + // naive : + // return getExplanationForConstantEquality( n, vn, exp ); + + // set up the recursion object + std::map<TypeNode, int> var_count; + TermRecBuild trb; + trb.init(vn); + Node vnr_exp; + int sz_use = sz; + getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz_use); + Assert(sz_use >= 0); + sz = sz_use; + Assert(vnr.isNull() || !vnr_exp.isNull()); + if (!vnr_exp.isNull() && !vnr_exp.isConst()) + { + exp.push_back(vnr_exp.negate()); + } +} + +void SygusExplain::getExplanationFor(Node n, + Node vn, + std::vector<Node>& exp, + SygusInvarianceTest& et) +{ + int sz = -1; + std::map<TypeNode, int> var_count; + TermRecBuild trb; + trb.init(vn); + Node vnr; + Node vnr_exp; + getExplanationFor(trb, n, vn, exp, var_count, et, vnr, vnr_exp, sz); +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |