diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-01-09 18:12:32 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-09 18:12:32 -0800 |
commit | ff9d2c84dae5eb21a7ef77f5931673fb23129730 (patch) | |
tree | 567463672f28f8b8f626c0bfc3e6b20f3798a6f4 /src/theory/quantifiers | |
parent | fa378358488a5bc2525dde852fcc9cbdeee9283e (diff) |
Fix linearization for terms where the solve variable does not occur. (#1506)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 46 |
1 files changed, 29 insertions, 17 deletions
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 2c71de666..275d7238d 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -1456,7 +1456,8 @@ static Node getPvCoeff(TNode pv, TNode n) * pv * -(a * b * c) * * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. + * a null node otherwise. If pv does not occur in children it returns a + * multiplication over children. */ static Node normalizePvMult( TNode pv, @@ -1518,13 +1519,21 @@ static Node normalizePvMult( { return zero; } - else if (coeff == bv::utils::mkOne(size_coeff)) + Node result; + if (found_pv) { - return 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; } - Node result = nm->mkNode(BITVECTOR_MULT, pv, coeff); - contains_pv[result] = true; - result.setAttribute(is_linear, true); return result; } @@ -1564,7 +1573,8 @@ static bool isLinearPlus( * pv * (a - c) + b * * Returns the normalized node if the resulting term is linear w.r.t. pv and - * a null node otherwise. + * a null node otherwise. If pv does not occur in children it returns an + * addition over children. */ static Node normalizePvPlus( Node pv, @@ -1609,6 +1619,7 @@ static Node normalizePvPlus( { Assert(isLinearPlus(nc, pv, contains_pv)); Node coeff = getPvCoeff(pv, nc[0]); + Assert(!coeff.isNull()); Node leaf = nc[1]; if (neg) { @@ -1622,22 +1633,23 @@ static Node normalizePvPlus( /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ return Node::null(); } - Assert(nb_c.getNumChildren() > 0); - - Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); - coeffs = Rewriter::rewrite(coeffs); + Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); - std::vector<Node> mult_children = {pv, coeffs}; - Node pv_mult_coeffs = normalizePvMult(pv, mult_children, contains_pv); + 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)); - Node result; /* pv * 0 + t --> t */ - if (pv_mult_coeffs == zero) + if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) { result = leafs; } @@ -1647,9 +1659,9 @@ static Node normalizePvPlus( contains_pv[result] = true; result.setAttribute(is_linear, true); } - return result; } - return pv_mult_coeffs; + Assert(!result.isNull()); + return result; } /** |