diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/bv_abstraction.cpp | 65 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_abstraction.h | 50 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 3 |
4 files changed, 124 insertions, 0 deletions
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp new file mode 100644 index 000000000..27069de2f --- /dev/null +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -0,0 +1,65 @@ +/********************* */ +/*! \file bv_abstraction.cpp + ** \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 BvAbstraction preprocessing pass + ** + ** Abstract common structures over small domains to UF. This preprocessing + ** is particularly useful on QF_BV/mcm benchmarks and can be enabled via + ** option `--bv-abstraction`. + ** For more information see 3.4 Refactoring Isomorphic Circuits in [1]. + ** + ** [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for + ** Bit-vectors in Satisfiability Modulo Theories + ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf + **/ + +#include "preprocessing/passes/bv_abstraction.h" + +#include <vector> + +#include "options/bv_options.h" +#include "theory/bv/theory_bv.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +BvAbstraction::BvAbstraction(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "bv-abstraction"){}; + +PreprocessingPassResult BvAbstraction::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + std::vector<Node> new_assertions; + std::vector<Node> assertions(assertionsToPreprocess->begin(), + assertionsToPreprocess->end()); + TheoryEngine* te = d_preprocContext->getTheoryEngine(); + bv::TheoryBV* bv_theory = static_cast<bv::TheoryBV*>(te->theoryOf(THEORY_BV)); + bool changed = bv_theory->applyAbstraction(assertions, new_assertions); + for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + { + assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + } + // If we are using the lazy solver and the abstraction applies, then UF + // symbols were introduced. + if (options::bitblastMode() == bv::BITBLAST_MODE_LAZY && changed) + { + d_preprocContext->widenLogic(theory::THEORY_UF); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h new file mode 100644 index 000000000..67e2ef296 --- /dev/null +++ b/src/preprocessing/passes/bv_abstraction.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file bv_abstraction.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 BvAbstraction preprocessing pass + ** + ** Abstract common structures over small domains to UF. This preprocessing + ** is particularly useful on QF_BV/mcm benchmarks and can be enabled via + ** option `--bv-abstraction`. + ** For more information see 3.4 Refactoring Isomorphic Circuits in [1]. + ** + ** [1] Liana Hadarean, An Efficient and Trustworthy Theory Solver for + ** Bit-vectors in Satisfiability Modulo Theories + ** https://cs.nyu.edu/media/publications/hadarean_liana.pdf + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H +#define __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class BvAbstraction : public PreprocessingPass +{ + public: + BvAbstraction(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */ diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index a738f9484..7d2ceab2e 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -22,5 +22,11 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt) : d_smt(smt) {} +void PreprocessingPassContext::widenLogic(theory::TheoryId id) +{ + LogicRequest req(*d_smt); + req.widenLogic(id); +} + } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 66f4d9297..28f51d154 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -38,6 +38,9 @@ class PreprocessingPassContext { prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + /* Widen the logic to include the given theory. */ + void widenLogic(theory::TheoryId id); + private: /* Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; |