decision/justification_heuristic.h \
preprocessing/passes/bv_gauss.cpp \
preprocessing/passes/bv_gauss.h \
+ preprocessing/passes/bv_intro_pow2.cpp \
+ preprocessing/passes/bv_intro_pow2.h \
preprocessing/passes/int_to_bv.cpp \
preprocessing/passes/int_to_bv.h \
preprocessing/passes/pseudo_boolean_processor.cpp \
theory/bv/bv_subtheory_core.h \
theory/bv/bv_subtheory_inequality.cpp \
theory/bv/bv_subtheory_inequality.h \
- theory/bv/bvintropow2.cpp \
- theory/bv/bvintropow2.h \
theory/bv/slicer.cpp \
theory/bv/slicer.h \
theory/bv/theory_bv.cpp \
--- /dev/null
+/********************* */
+/*! \file bv_intro_pow2.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner, Liana Hadarean, Morgan Deters
+ ** 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 The BvIntroPow2 preprocessing pass
+ **
+ ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
+ ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
+ ** can be enabled via option `--bv-intro-pow2`.
+ **/
+
+#include "preprocessing/passes/bv_intro_pow2.h"
+
+#include <unordered_map>
+
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+using namespace CVC4::theory;
+
+namespace {
+
+Node pow2Rewrite(Node node, NodeMap& cache)
+{
+ NodeMap::const_iterator ci = cache.find(node);
+ if (ci != cache.end())
+ {
+ Node incache = (*ci).second;
+ return incache.isNull() ? node : incache;
+ }
+
+ Node res = Node::null();
+ switch (node.getKind())
+ {
+ case kind::AND:
+ {
+ bool changed = false;
+ std::vector<Node> children;
+ for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
+ {
+ Node child = node[i];
+ Node found = pow2Rewrite(child, cache);
+ changed = changed || (child != found);
+ children.push_back(found);
+ }
+ if (changed)
+ {
+ res = NodeManager::currentNM()->mkNode(kind::AND, children);
+ }
+ }
+ break;
+
+ case kind::EQUAL:
+ if (node[0].getType().isBitVector()
+ && theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::applies(node))
+ {
+ res = theory::bv::RewriteRule<theory::bv::IsPowerOfTwo>::run<false>(node);
+ }
+ break;
+ default: break;
+ }
+
+ cache.insert(std::make_pair(node, res));
+ 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, NodeHashFunction> cache;
+ for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ Node cur = (*assertionsToPreprocess)[i];
+ Node res = pow2Rewrite(cur, cache);
+ if (res != cur)
+ {
+ res = Rewriter::rewrite(res);
+ assertionsToPreprocess->replace(i, res);
+ }
+ }
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}/* CVC4::theory::bv namespace */
+}/* CVC4::theory namespace */
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file bv_intro_pow2.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Mathias Preiner
+ ** 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 The BvIntroPow2 preprocessing pass
+ **
+ ** Traverses the formula and applies the IsPowerOfTwo rewrite rule. This
+ ** preprocessing pass is particularly useful on QF_BV/pspace benchmarks and
+ ** can be enabled via option `--bv-intro-pow2`.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+#define __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class BvIntroPow2 : public PreprocessingPass
+{
+ public:
+ BvIntroPow2(PreprocessingPassContext* preprocContext);
+
+ protected:
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
#include "options/uf_options.h"
#include "preprocessing/passes/bool_to_bv.h"
#include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/bv_intro_pow2.h"
#include "preprocessing/passes/bv_to_bool.h"
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "smt_util/nary_builder.h"
#include "smt_util/node_visitor.h"
#include "theory/booleans/circuit_propagator.h"
-#include "theory/bv/bvintropow2.h"
#include "theory/bv/theory_bv_rewriter.h"
#include "theory/logic_info.h"
#include "theory/quantifiers/fun_def_process.h"
std::unique_ptr<BoolToBV> boolToBv(
new BoolToBV(d_preprocessingPassContext.get()));
d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
+ std::unique_ptr<BvIntroPow2> bvIntroPow2(
+ new BvIntroPow2(d_preprocessingPassContext.get()));
+ d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
+ std::move(bvIntroPow2));
}
Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
dumpAssertions("post-unconstrained-simp", d_assertions);
}
- if(options::bvIntroducePow2()){
- theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
+ if(options::bvIntroducePow2())
+ {
+ d_preprocessingPassRegistry.getPass("bv-intro-pow2")->apply(&d_assertions);
}
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl;
+++ /dev/null
-/********************* */
-/*! \file bvintropow2.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Paul Meng
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "theory/bv/bvintropow2.h"
-#include "theory/rewriter.h"
-#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
-
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-void BVIntroducePow2::pow2Rewrite(std::vector<Node>& assertionsToPreprocess){
- NodeMap cache;
- for(size_t i = 0, N= assertionsToPreprocess.size(); i < N; ++i){
- Node curr = assertionsToPreprocess[i];
- Node next = pow2Rewrite(curr, cache);
- if(next != curr){
- Node tmp = Rewriter::rewrite(next);
- next = tmp;
- }
- assertionsToPreprocess[i] = next;
- }
-}
-
-Node BVIntroducePow2::pow2Rewrite(Node node, NodeMap& cache){
- NodeMap::const_iterator ci = cache.find(node);
- if(ci != cache.end()){
- Node incache = (*ci).second;
-
- return incache.isNull() ? node : incache;
- }
-
- Node res = Node::null();
- switch(node.getKind()){
- case kind::AND:
- {
- bool changed = false;
- std::vector<Node> children;
- for(unsigned i = 0, N = node.getNumChildren(); i < N; ++i){
- Node child = node[i];
- Node found = pow2Rewrite(child, cache);
- changed = changed || (child != found);
- children.push_back(found);
- }
- if(changed){
- res = NodeManager::currentNM()->mkNode(kind::AND, children);
- }
- }
- break;
-
- case kind::EQUAL:
- if(node[0].getType().isBitVector()){
- if (RewriteRule<IsPowerOfTwo>::applies(node)) {
- res = RewriteRule<IsPowerOfTwo>::run<false>(node);
- }
- }
- break;
- default:
- break;
- }
-
- cache.insert(std::make_pair(node, res));
- return res.isNull() ? node : res;
-}
-
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file bvintropow2.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Paul Meng
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-
-
-#include "cvc4_private.h"
-#include "expr/node.h"
-
-#include <vector>
-#include <unordered_map>
-
-#ifndef __CVC4__THEORY__BV__BV_INTRO_POW_H
-#define __CVC4__THEORY__BV__BV_INTRO_POW_H
-
-namespace CVC4 {
-namespace theory {
-namespace bv {
-
-
-class BVIntroducePow2 {
-public:
- static void pow2Rewrite(std::vector<Node>& assertionsToPreprocess);
-
-private:
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
- static Node pow2Rewrite(Node assertionsToPreprocess, NodeMap& cache);
-};
-
-
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
-
-
-#endif /* __CVC4__THEORY__BV__BV_INTRO_POW_H */
regress0/bv/mult-pow2-negative.smt2 \
regress0/bv/sizecheck.cvc \
regress0/bv/smtcompbug.smt \
+ regress0/bv/test-bv_intro_pow2.smt2 \
regress0/bv/unsound1-reduced.smt2 \
regress0/chained-equality.smt2 \
regress0/constant-rewrite.smt \
--- /dev/null
+; COMMAND-LINE: --bv-intro-pow2 --no-check-proofs --no-check-unsat-cores
+(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))
+(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))))
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff