From cbfcc24f0da280e21de5118cc2c0c6a18a71a629 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 3 May 2018 22:50:41 -0700 Subject: [PATCH] Refactor bv-intro-pow2 preprocessing pass. (#1851) --- src/Makefile.am | 4 +- src/preprocessing/passes/bv_intro_pow2.cpp | 104 ++++++++++++++++++ src/preprocessing/passes/bv_intro_pow2.h | 45 ++++++++ src/smt/smt_engine.cpp | 11 +- src/theory/bv/bvintropow2.cpp | 85 -------------- src/theory/bv/bvintropow2.h | 51 --------- test/regress/Makefile.tests | 1 + .../regress0/bv/test-bv_intro_pow2.smt2 | 14 +++ 8 files changed, 174 insertions(+), 141 deletions(-) create mode 100644 src/preprocessing/passes/bv_intro_pow2.cpp create mode 100644 src/preprocessing/passes/bv_intro_pow2.h delete mode 100644 src/theory/bv/bvintropow2.cpp delete mode 100644 src/theory/bv/bvintropow2.h create mode 100644 test/regress/regress0/bv/test-bv_intro_pow2.smt2 diff --git a/src/Makefile.am b/src/Makefile.am index 168e1e3b8..0eefbc1de 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -64,6 +64,8 @@ libcvc4_la_SOURCES = \ 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 \ @@ -326,8 +328,6 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp new file mode 100644 index 000000000..17336b86c --- /dev/null +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -0,0 +1,104 @@ +/********************* */ +/*! \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 + +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map; +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 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::applies(node)) + { + res = theory::bv::RewriteRule::run(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 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 */ diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h new file mode 100644 index 000000000..a5fe8e7bb --- /dev/null +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -0,0 +1,45 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c1e8596cf..10d21a66c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,6 +70,7 @@ #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" @@ -95,7 +96,6 @@ #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" @@ -2603,6 +2603,10 @@ void SmtEnginePrivate::finishInit() { std::unique_ptr boolToBv( new BoolToBV(d_preprocessingPassContext.get())); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); + std::unique_ptr bvIntroPow2( + new BvIntroPow2(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("bv-intro-pow2", + std::move(bvIntroPow2)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -4070,8 +4074,9 @@ void SmtEnginePrivate::processAssertions() { 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; diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp deleted file mode 100644 index e7b6caaef..000000000 --- a/src/theory/bv/bvintropow2.cpp +++ /dev/null @@ -1,85 +0,0 @@ -/********************* */ -/*! \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& 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 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::applies(node)) { - res = RewriteRule::run(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 */ diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h deleted file mode 100644 index e335c1339..000000000 --- a/src/theory/bv/bvintropow2.h +++ /dev/null @@ -1,51 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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& assertionsToPreprocess); - -private: - typedef std::unordered_map 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 */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 70cb56b8f..0a0732753 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -308,6 +308,7 @@ REG0_TESTS = \ 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 \ diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 new file mode 100644 index 000000000..96779d3a6 --- /dev/null +++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2 @@ -0,0 +1,14 @@ +; 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) -- 2.30.2