diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp | 377 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp | 345 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h | 108 | ||||
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_instantiator_white.h | 4 |
6 files changed, 463 insertions, 375 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f6c66b743..0ea7a6837 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -434,6 +434,8 @@ libcvc4_add_sources( theory/quantifiers/cegqi/ceg_arith_instantiator.h theory/quantifiers/cegqi/ceg_bv_instantiator.cpp theory/quantifiers/cegqi/ceg_bv_instantiator.h + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h theory/quantifiers/cegqi/ceg_dt_instantiator.cpp theory/quantifiers/cegqi/ceg_dt_instantiator.h theory/quantifiers/cegqi/ceg_epr_instantiator.cpp diff --git a/src/Makefile.am b/src/Makefile.am index 7856d7f29..8c1c0871d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -448,6 +448,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/cegqi/ceg_arith_instantiator.h \ theory/quantifiers/cegqi/ceg_bv_instantiator.cpp \ theory/quantifiers/cegqi/ceg_bv_instantiator.h \ + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp \ + theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h \ theory/quantifiers/cegqi/ceg_dt_instantiator.cpp \ theory/quantifiers/cegqi/ceg_dt_instantiator.h \ theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 3cf605238..72e7d7e68 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -17,6 +17,7 @@ #include <stack> #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" #include "util/bitvector.h" #include "util/random.h" @@ -28,11 +29,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -struct BvLinearAttributeId -{ -}; -using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>; - // this class can be used to query the model value through the CegInstaniator // class class CegInstantiatorBvInverterQuery : public BvInverterQuery @@ -534,371 +530,6 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, return result; } -/** - * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, - * or -pv * t. Extracting the coefficient of multiplications only succeeds if - * the multiplication are normalized with normalizePvMult. - * - * If sucessful it returns - * 1 if n == pv, - * -1 if n == -pv, - * t if n == pv * t, - * -t if n == -pv * t. - * If n is not a linear term, a null node is returned. - */ -static Node getPvCoeff(TNode pv, TNode n) -{ - bool neg = false; - Node coeff; - - if (n.getKind() == BITVECTOR_NEG) - { - neg = true; - n = n[0]; - } - - if (n == pv) - { - coeff = bv::utils::mkOne(bv::utils::getSize(pv)); - } - /* All multiplications are normalized to pv * (t1 * t2). */ - else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) - { - Assert(n.getNumChildren() == 2); - Assert(n[0] == pv); - coeff = n[1]; - } - else /* n is in no form to extract the coefficient for pv */ - { - Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " - << n << std::endl; - return Node::null(); - } - Assert(!coeff.isNull()); - - if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); - return coeff; -} - -/** - * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * -pv * b * c - * - * is rewritten to - * - * pv * -(a * b * c) - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns a - * multiplication over children. - */ -static Node normalizePvMult( - TNode pv, - const std::vector<Node>& children, - std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) -{ - bool neg, neg_coeff = false; - bool found_pv = false; - NodeManager* nm; - NodeBuilder<> nb(BITVECTOR_MULT); - BvLinearAttribute is_linear; - - nm = NodeManager::currentNM(); - for (TNode nc : children) - { - if (!contains_pv[nc]) - { - nb << nc; - continue; - } - - neg = false; - if (nc.getKind() == BITVECTOR_NEG) - { - neg = true; - nc = nc[0]; - } - - if (!found_pv && nc == pv) - { - found_pv = true; - neg_coeff = neg; - continue; - } - else if (!found_pv && nc.getKind() == BITVECTOR_MULT - && nc.getAttribute(is_linear)) - { - Assert(nc.getNumChildren() == 2); - Assert(nc[0] == pv); - Assert(!contains_pv[nc[1]]); - found_pv = true; - neg_coeff = neg; - nb << nc[1]; - continue; - } - return Node::null(); /* non-linear */ - } - Assert(nb.getNumChildren() > 0); - - Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); - if (neg_coeff) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - } - coeff = Rewriter::rewrite(coeff); - unsigned size_coeff = bv::utils::getSize(coeff); - Node zero = bv::utils::mkZero(size_coeff); - if (coeff == zero) - { - return zero; - } - Node result; - if (found_pv) - { - if (coeff == bv::utils::mkOne(size_coeff)) - { - return pv; - } - result = nm->mkNode(BITVECTOR_MULT, pv, coeff); - contains_pv[result] = true; - result.setAttribute(is_linear, true); - } - else - { - result = coeff; - } - return result; -} - -#ifdef CVC4_ASSERTIONS -static bool isLinearPlus( - TNode n, - TNode pv, - std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) -{ - Node coeff; - Assert(n.getAttribute(BvLinearAttribute())); - Assert(n.getNumChildren() == 2); - if (n[0] != pv) - { - Assert(n[0].getKind() == BITVECTOR_MULT); - Assert(n[0].getNumChildren() == 2); - Assert(n[0][0] == pv); - Assert(!contains_pv[n[0][1]]); - } - Assert(!contains_pv[n[1]]); - coeff = getPvCoeff(pv, n[0]); - Assert(!coeff.isNull()); - Assert(!contains_pv[coeff]); - return true; -} -#endif - -/** - * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks - * terms in which pv occurs. - * For example, - * - * a * pv + b + c * -pv - * - * is rewritten to - * - * pv * (a - c) + b - * - * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. If pv does not occur in children it returns an - * addition over children. - */ -static Node normalizePvPlus( - Node pv, - const std::vector<Node>& children, - std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) -{ - NodeManager* nm; - NodeBuilder<> nb_c(BITVECTOR_PLUS); - NodeBuilder<> nb_l(BITVECTOR_PLUS); - BvLinearAttribute is_linear; - bool neg; - - nm = NodeManager::currentNM(); - for (TNode nc : children) - { - if (!contains_pv[nc]) - { - nb_l << nc; - continue; - } - - neg = false; - if (nc.getKind() == BITVECTOR_NEG) - { - neg = true; - nc = nc[0]; - } - - if (nc == pv - || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) - { - Node coeff = getPvCoeff(pv, nc); - Assert(!coeff.isNull()); - if (neg) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - } - nb_c << coeff; - continue; - } - else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) - { - Assert(isLinearPlus(nc, pv, contains_pv)); - Node coeff = getPvCoeff(pv, nc[0]); - Assert(!coeff.isNull()); - Node leaf = nc[1]; - if (neg) - { - coeff = nm->mkNode(BITVECTOR_NEG, coeff); - leaf = nm->mkNode(BITVECTOR_NEG, leaf); - } - nb_c << coeff; - nb_l << leaf; - continue; - } - /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ - return Node::null(); - } - Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); - - Node pv_mult_coeffs, result; - if (nb_c.getNumChildren() > 0) - { - Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); - coeffs = Rewriter::rewrite(coeffs); - result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv); - } - - if (nb_l.getNumChildren() > 0) - { - Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); - leafs = Rewriter::rewrite(leafs); - Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); - /* pv * 0 + t --> t */ - if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) - { - result = leafs; - } - else - { - result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); - contains_pv[result] = true; - result.setAttribute(is_linear, true); - } - } - Assert(!result.isNull()); - return result; -} - -/** - * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv - * marks terms in which pv occurs. - * For example, equality - * - * -pv * a + b = c + pv - * - * rewrites to - * - * pv * (-a - 1) = c - b. - */ -static Node normalizePvEqual( - Node pv, - const std::vector<Node>& children, - std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) -{ - Assert(children.size() == 2); - - NodeManager* nm = NodeManager::currentNM(); - BvLinearAttribute is_linear; - Node coeffs[2], leafs[2]; - bool neg; - TNode child; - - for (unsigned i = 0; i < 2; ++i) - { - child = children[i]; - neg = false; - if (child.getKind() == BITVECTOR_NEG) - { - neg = true; - child = child[0]; - } - if (child.getAttribute(is_linear) || child == pv) - { - if (child.getKind() == BITVECTOR_PLUS) - { - Assert(isLinearPlus(child, pv, contains_pv)); - coeffs[i] = getPvCoeff(pv, child[0]); - leafs[i] = child[1]; - } - else - { - Assert(child.getKind() == BITVECTOR_MULT || child == pv); - coeffs[i] = getPvCoeff(pv, child); - } - } - if (neg) - { - if (!coeffs[i].isNull()) - { - coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); - } - if (!leafs[i].isNull()) - { - leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); - } - } - } - - if (coeffs[0].isNull() || coeffs[1].isNull()) - { - return Node::null(); - } - - Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); - coeff = Rewriter::rewrite(coeff); - std::vector<Node> mult_children = {pv, coeff}; - Node lhs = normalizePvMult(pv, mult_children, contains_pv); - - Node rhs; - if (!leafs[0].isNull() && !leafs[1].isNull()) - { - rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); - } - else if (!leafs[0].isNull()) - { - rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); - } - else if (!leafs[1].isNull()) - { - rhs = leafs[1]; - } - else - { - rhs = bv::utils::mkZero(bv::utils::getSize(pv)); - } - rhs = Rewriter::rewrite(rhs); - - if (lhs == rhs) - { - return bv::utils::mkTrue(); - } - - Node result = lhs.eqNode(rhs); - contains_pv[result] = true; - return result; -} - Node BvInstantiator::rewriteTermForSolvePv( Node pv, Node n, @@ -928,7 +559,7 @@ Node BvInstantiator::rewriteTermForSolvePv( if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) { - Node result = normalizePvEqual(pv, children, contains_pv); + Node result = utils::normalizePvEqual(pv, children, contains_pv); if (!result.isNull()) { Trace("cegqi-bv-nl") @@ -949,11 +580,11 @@ Node BvInstantiator::rewriteTermForSolvePv( Node result; if (n.getKind() == BITVECTOR_MULT) { - result = normalizePvMult(pv, children, contains_pv); + result = utils::normalizePvMult(pv, children, contains_pv); } else { - result = normalizePvPlus(pv, children, contains_pv); + result = utils::normalizePvPlus(pv, children, contains_pv); } if (!result.isNull()) { diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp new file mode 100644 index 000000000..b74d358ac --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -0,0 +1,345 @@ +/********************* */ +/*! \file ceg_bv_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 ceg_bv_instantiator + **/ + +#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" + +#include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { +namespace utils { + +Node getPvCoeff(TNode pv, TNode n) +{ + bool neg = false; + Node coeff; + + if (n.getKind() == BITVECTOR_NEG) + { + neg = true; + n = n[0]; + } + + if (n == pv) + { + coeff = bv::utils::mkOne(bv::utils::getSize(pv)); + } + /* All multiplications are normalized to pv * (t1 * t2). */ + else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) + { + Assert(n.getNumChildren() == 2); + Assert(n[0] == pv); + coeff = n[1]; + } + else /* n is in no form to extract the coefficient for pv */ + { + Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " + << n << std::endl; + return Node::null(); + } + Assert(!coeff.isNull()); + + if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); + return coeff; +} + +Node normalizePvMult( + TNode pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + bool neg, neg_coeff = false; + bool found_pv = false; + NodeManager* nm; + NodeBuilder<> nb(BITVECTOR_MULT); + BvLinearAttribute is_linear; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (!found_pv && nc == pv) + { + found_pv = true; + neg_coeff = neg; + continue; + } + else if (!found_pv && nc.getKind() == BITVECTOR_MULT + && nc.getAttribute(is_linear)) + { + Assert(nc.getNumChildren() == 2); + Assert(nc[0] == pv); + Assert(!contains_pv[nc[1]]); + found_pv = true; + neg_coeff = neg; + nb << nc[1]; + continue; + } + return Node::null(); /* non-linear */ + } + Assert(nb.getNumChildren() > 0); + + Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); + if (neg_coeff) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + coeff = Rewriter::rewrite(coeff); + unsigned size_coeff = bv::utils::getSize(coeff); + Node zero = bv::utils::mkZero(size_coeff); + if (coeff == zero) + { + return zero; + } + Node result; + if (found_pv) + { + if (coeff == bv::utils::mkOne(size_coeff)) + { + return pv; + } + result = nm->mkNode(BITVECTOR_MULT, pv, coeff); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + else + { + result = coeff; + } + return result; +} + +#ifdef CVC4_ASSERTIONS +namespace { +bool isLinearPlus( + TNode n, + TNode pv, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + Node coeff; + Assert(n.getAttribute(BvLinearAttribute())); + Assert(n.getNumChildren() == 2); + if (n[0] != pv) + { + Assert(n[0].getKind() == BITVECTOR_MULT); + Assert(n[0].getNumChildren() == 2); + Assert(n[0][0] == pv); + Assert(!contains_pv[n[0][1]]); + } + Assert(!contains_pv[n[1]]); + coeff = utils::getPvCoeff(pv, n[0]); + Assert(!coeff.isNull()); + Assert(!contains_pv[coeff]); + return true; +} +} // namespace +#endif + +Node normalizePvPlus( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + NodeManager* nm; + NodeBuilder<> nb_c(BITVECTOR_PLUS); + NodeBuilder<> nb_l(BITVECTOR_PLUS); + BvLinearAttribute is_linear; + bool neg; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb_l << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (nc == pv + || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) + { + Node coeff = utils::getPvCoeff(pv, nc); + Assert(!coeff.isNull()); + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + nb_c << coeff; + continue; + } + else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) + { + Assert(isLinearPlus(nc, pv, contains_pv)); + Node coeff = utils::getPvCoeff(pv, nc[0]); + Assert(!coeff.isNull()); + Node leaf = nc[1]; + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + leaf = nm->mkNode(BITVECTOR_NEG, leaf); + } + nb_c << coeff; + nb_l << leaf; + continue; + } + /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ + return Node::null(); + } + Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); + + Node pv_mult_coeffs, result; + if (nb_c.getNumChildren() > 0) + { + Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); + coeffs = Rewriter::rewrite(coeffs); + result = pv_mult_coeffs = + utils::normalizePvMult(pv, {pv, coeffs}, contains_pv); + } + + if (nb_l.getNumChildren() > 0) + { + Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); + leafs = Rewriter::rewrite(leafs); + Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); + /* pv * 0 + t --> t */ + if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) + { + result = leafs; + } + else + { + result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + } + Assert(!result.isNull()); + return result; +} + +Node normalizePvEqual( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + Assert(children.size() == 2); + + NodeManager* nm = NodeManager::currentNM(); + BvLinearAttribute is_linear; + Node coeffs[2], leafs[2]; + bool neg; + TNode child; + + for (unsigned i = 0; i < 2; ++i) + { + child = children[i]; + neg = false; + if (child.getKind() == BITVECTOR_NEG) + { + neg = true; + child = child[0]; + } + if (child.getAttribute(is_linear) || child == pv) + { + if (child.getKind() == BITVECTOR_PLUS) + { + Assert(isLinearPlus(child, pv, contains_pv)); + coeffs[i] = utils::getPvCoeff(pv, child[0]); + leafs[i] = child[1]; + } + else + { + Assert(child.getKind() == BITVECTOR_MULT || child == pv); + coeffs[i] = utils::getPvCoeff(pv, child); + } + } + if (neg) + { + if (!coeffs[i].isNull()) + { + coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); + } + if (!leafs[i].isNull()) + { + leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); + } + } + } + + if (coeffs[0].isNull() || coeffs[1].isNull()) + { + return Node::null(); + } + + Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); + coeff = Rewriter::rewrite(coeff); + std::vector<Node> mult_children = {pv, coeff}; + Node lhs = utils::normalizePvMult(pv, mult_children, contains_pv); + + Node rhs; + if (!leafs[0].isNull() && !leafs[1].isNull()) + { + rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); + } + else if (!leafs[0].isNull()) + { + rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); + } + else if (!leafs[1].isNull()) + { + rhs = leafs[1]; + } + else + { + rhs = bv::utils::mkZero(bv::utils::getSize(pv)); + } + rhs = Rewriter::rewrite(rhs); + + if (lhs == rhs) + { + return bv::utils::mkTrue(); + } + + Node result = lhs.eqNode(rhs); + contains_pv[result] = true; + return result; +} + +} // namespace utils +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h new file mode 100644 index 000000000..551ce08e0 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -0,0 +1,108 @@ +/********************* */ +/*! \file ceg_bv_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 ceg_bv_instantiator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV_INSTANTIATOR_UTILS_H +#define __CVC4__BV_INSTANTIATOR_UTILS_H + +#include "expr/attribute.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +struct BvLinearAttributeId +{ +}; +using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>; + +namespace utils { + +/** + * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, + * or -pv * t. Extracting the coefficient of multiplications only succeeds if + * the multiplication are normalized with normalizePvMult. + * + * If sucessful it returns + * 1 if n == pv, + * -1 if n == -pv, + * t if n == pv * t, + * -t if n == -pv * t. + * If n is not a linear term, a null node is returned. + */ +Node getPvCoeff(TNode pv, TNode n); + +/** + * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * -pv * b * c + * + * is rewritten to + * + * pv * -(a * b * c) + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns a + * multiplication over children. + */ +Node normalizePvMult( + TNode pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv); + +/** + * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * pv + b + c * -pv + * + * is rewritten to + * + * pv * (a - c) + b + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns an + * addition over children. + */ +Node normalizePvPlus( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv); + +/** + * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv + * marks terms in which pv occurs. + * For example, equality + * + * -pv * a + b = c + pv + * + * rewrites to + * + * pv * (-a - 1) = c - b. + */ +Node normalizePvEqual( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv); + +} // namespace utils +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 +#endif diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 018744bd1..5d50490c0 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -19,11 +19,10 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" -#include "theory/quantifiers/cegqi/ceg_bv_instantiator.cpp" - #include <cxxtest/TestSuite.h> #include <iostream> #include <vector> @@ -33,6 +32,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::quantifiers::utils; using namespace CVC4::smt; class BvInstantiatorWhite : public CxxTest::TestSuite |