IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule.
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-#include "theory/rewriter.h"
+#include "theory/bv/theory_bv_utils.h"
namespace cvc5 {
namespace preprocessing {
using NodeMap = std::unordered_map<Node, Node>;
using namespace cvc5::theory;
-namespace {
+BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "bv-intro-pow2"){};
+
+PreprocessingPassResult BvIntroPow2::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ std::unordered_map<Node, Node> cache;
+ for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ Node cur = (*assertionsToPreprocess)[i];
+ Node res = pow2Rewrite(cur, cache);
+ if (res != cur)
+ {
+ res = rewrite(res);
+ assertionsToPreprocess->replace(i, res);
+ }
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
-Node pow2Rewrite(Node node, NodeMap& cache)
+bool BvIntroPow2::isPowerOfTwo(TNode node)
{
- NodeMap::const_iterator ci = cache.find(node);
+ if (node.getKind() != kind::EQUAL)
+ {
+ return false;
+ }
+ if (node[0].getKind() != kind::BITVECTOR_AND
+ && node[1].getKind() != kind::BITVECTOR_AND)
+ {
+ return false;
+ }
+ if (!bv::utils::isZero(node[0]) && !bv::utils::isZero(node[1]))
+ {
+ return false;
+ }
+
+ TNode t = !bv::utils::isZero(node[0]) ? node[0] : node[1];
+ if (t.getNumChildren() != 2) return false;
+ TNode a = t[0];
+ TNode b = t[1];
+ unsigned size = bv::utils::getSize(t);
+ if (size < 2) return false;
+ Node diff =
+ rewrite(NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b));
+ return (diff.isConst()
+ && (diff == bv::utils::mkConst(size, 1u)
+ || diff == bv::utils::mkOnes(size)));
+}
+
+Node BvIntroPow2::rewritePowerOfTwo(TNode node)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ TNode term = bv::utils::isZero(node[0]) ? node[1] : node[0];
+ TNode a = term[0];
+ TNode b = term[1];
+ unsigned size = bv::utils::getSize(term);
+ Node diff = rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b));
+ Assert(diff.isConst());
+ TNode x = diff == bv::utils::mkConst(size, 1u) ? a : b;
+ Node one = bv::utils::mkConst(size, 1u);
+ Node sk = bv::utils::mkVar(size);
+ Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk);
+ Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh);
+ return x_eq_sh;
+}
+
+Node BvIntroPow2::pow2Rewrite(Node node, std::unordered_map<Node, Node>& cache)
+{
+ const auto& ci = cache.find(node);
if (ci != cache.end())
{
Node incache = (*ci).second;
break;
case kind::EQUAL:
- if (node[0].getType().isBitVector()
- && theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::applies(node))
+ if (node[0].getType().isBitVector() && isPowerOfTwo(node))
{
- res = theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::run<false>(node);
+ res = rewritePowerOfTwo(node);
}
break;
default: break;
return res.isNull() ? node : res;
}
-} // namespace
-
-BvIntroPow2::BvIntroPow2(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "bv-intro-pow2"){};
-
-PreprocessingPassResult BvIntroPow2::applyInternal(
- AssertionPipeline* assertionsToPreprocess)
-{
- std::unordered_map<Node, Node> cache;
- for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
- {
- Node cur = (*assertionsToPreprocess)[i];
- Node res = pow2Rewrite(cur, cache);
- if (res != cur)
- {
- res = rewrite(res);
- assertionsToPreprocess->replace(i, res);
- }
- }
- return PreprocessingPassResult::NO_CONFLICT;
-}
-
} // namespace passes
} // namespace preprocessing
protected:
PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+ /** Checks whether PowerOfTwo rewrite applies. */
+ bool isPowerOfTwo(TNode node);
+ /**
+ * Applies PowerOfTwo rewrite.
+ *
+ * x & (x-1) = 0 => x = 1 << sk
+ *
+ * where sk is a fresh Skolem.
+ *
+ * WARNING: this is an **EQUISATISFIABLE** transformation!
+ * Only to be called on top level assertions.
+ */
+ Node rewritePowerOfTwo(TNode node);
+ /** Does the traversal of assertions and applies rweritePowerOfTwo. */
+ Node pow2Rewrite(Node node, std::unordered_map<Node, Node>& cache);
};
} // namespace passes
BBAddNeg,
UltAddOne,
ConcatToMult,
- IsPowerOfTwo,
MultSltMult,
BitOfConst,
};
case MultDistrib: out << "MultDistrib"; return out;
case UltAddOne: out << "UltAddOne"; return out;
case ConcatToMult: out << "ConcatToMult"; return out;
- case IsPowerOfTwo: out << "IsPowerOfTwo"; return out;
case MultSltMult: out << "MultSltMult"; return out;
case NormalizeEqAddNeg: out << "NormalizeEqAddNeg"; return out;
case BitOfConst: out << "BitOfConst"; return out;
RewriteRule<MultDistrib> rule118;
RewriteRule<UltAddOne> rule119;
RewriteRule<ConcatToMult> rule120;
- RewriteRule<IsPowerOfTwo> rule121;
RewriteRule<RedorEliminate> rule122;
RewriteRule<RedandEliminate> rule123;
RewriteRule<SignExtendEqConst> rule124;
#include "options/bv_options.h"
#include "theory/bv/theory_bv_rewrite_rules.h"
#include "theory/bv/theory_bv_utils.h"
-#include "theory/rewriter.h"
#include "util/bitvector.h"
namespace cvc5 {
/* -------------------------------------------------------------------------- */
-/**
- * x ^(x-1) = 0 => 1 << sk
- * WARNING: this is an **EQUISATISFIABLE** transformation!
- * Only to be called on top level assertions.
- *
- * @param node
- *
- * @return
- */
-template<> inline
-bool RewriteRule<IsPowerOfTwo>::applies(TNode node) {
- if (node.getKind()!= kind::EQUAL) return false;
- if (node[0].getKind() != kind::BITVECTOR_AND &&
- node[1].getKind() != kind::BITVECTOR_AND)
- return false;
- if (!utils::isZero(node[0]) &&
- !utils::isZero(node[1]))
- return false;
-
- TNode t = !utils::isZero(node[0])? node[0]: node[1];
- if (t.getNumChildren() != 2) return false;
- TNode a = t[0];
- TNode b = t[1];
- unsigned size = utils::getSize(t);
- if(size < 2) return false;
- Node diff = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, a, b));
- return (diff.isConst() && (diff == utils::mkConst(size, 1u) || diff == utils::mkOnes(size)));
-}
-
-template <>
-inline Node RewriteRule<IsPowerOfTwo>::apply(TNode node)
-{
- Debug("bv-rewrite") << "RewriteRule<IsPowerOfTwo>(" << node << ")"
- << std::endl;
- NodeManager *nm = NodeManager::currentNM();
- TNode term = utils::isZero(node[0]) ? node[1] : node[0];
- TNode a = term[0];
- TNode b = term[1];
- unsigned size = utils::getSize(term);
- Node diff = Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, a, b));
- Assert(diff.isConst());
- TNode x = diff == utils::mkConst(size, 1u) ? a : b;
- Node one = utils::mkConst(size, 1u);
- Node sk = utils::mkVar(size);
- Node sh = nm->mkNode(kind::BITVECTOR_SHL, one, sk);
- Node x_eq_sh = nm->mkNode(kind::EQUAL, x, sh);
- return x_eq_sh;
-}
-
-/* -------------------------------------------------------------------------- */
-
/**
* Rewrite
* sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m)
-; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores
+; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores --bv-solver=layered
(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :status unsat)
-(declare-fun x () (_ BitVec 32))
-(declare-fun y () (_ BitVec 32))
-(declare-fun z () (_ BitVec 32))
+(declare-fun x () (_ BitVec 1024))
+(declare-fun y () (_ BitVec 1024))
+(declare-fun z () (_ BitVec 1024))
(assert (= z (bvadd x y)))
(assert (distinct x y))
-(assert (and (distinct x (_ bv0 32)) (= (bvand x (bvsub x (_ bv1 32))) (_ bv0 32))))
-(assert (and (distinct y (_ bv0 32)) (= (bvand y (bvsub y (_ bv1 32))) (_ bv0 32))))
-(assert (and (distinct z (_ bv0 32)) (= (bvand z (bvsub z (_ bv1 32))) (_ bv0 32))))
+(assert (and (distinct x (_ bv0 1024)) (= (bvand x (bvsub x (_ bv1 1024))) (_ bv0 1024))))
+(assert (and (distinct y (_ bv0 1024)) (= (bvand y (bvsub y (_ bv1 1024))) (_ bv0 1024))))
+(assert (and (distinct z (_ bv0 1024)) (= (bvand z (bvsub z (_ bv1 1024))) (_ bv0 1024))))
(check-sat)
(exit)
projects / cvc5.git / commitdiff