decision/decision_strategy.h \
decision/justification_heuristic.cpp \
decision/justification_heuristic.h \
+ preprocessing/passes/bv_abstraction.cpp \
+ preprocessing/passes/bv_abstraction.h \
preprocessing/passes/bv_gauss.cpp \
preprocessing/passes/bv_gauss.h \
preprocessing/passes/bv_intro_pow2.cpp \
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt)
: d_smt(smt) {}
+void PreprocessingPassContext::widenLogic(theory::TheoryId id)
+{
+ LogicRequest req(*d_smt);
+ req.widenLogic(id);
+}
+
} // namespace preprocessing
} // namespace CVC4
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;
#include "options/theory_options.h"
#include "options/uf_options.h"
#include "preprocessing/passes/bool_to_bv.h"
+#include "preprocessing/passes/bv_abstraction.h"
#include "preprocessing/passes/bv_gauss.h"
#include "preprocessing/passes/bv_intro_pow2.h"
#include "preprocessing/passes/bv_to_bool.h"
*/
bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
- // Abstract common structure over small domains to UF
- // return true if changes were made.
- void bvAbstraction();
-
// Simplify ITE structure
bool simpITE();
// actually assembling preprocessing pipelines).
std::unique_ptr<BoolToBV> boolToBv(
new BoolToBV(d_preprocessingPassContext.get()));
+ std::unique_ptr<BvAbstraction> bvAbstract(
+ new BvAbstraction(d_preprocessingPassContext.get()));
std::unique_ptr<BVGauss> bvGauss(
new BVGauss(d_preprocessingPassContext.get()));
std::unique_ptr<BvIntroPow2> bvIntroPow2(
std::unique_ptr<RealToInt> realToInt(
new RealToInt(d_preprocessingPassContext.get()));
d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
+ d_preprocessingPassRegistry.registerPass("bv-abstraction",
+ std::move(bvAbstract));
d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
std::move(bvIntroPow2));
return true;
}
-void SmtEnginePrivate::bvAbstraction() {
- Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
- std::vector<Node> new_assertions;
- bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- d_assertions.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() == theory::bv::BITBLAST_MODE_LAZY &&
- changed) {
- LogicRequest req(d_smt);
- req.widenLogic(THEORY_UF);
- }
-}
-
-
-
bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref());
}
- if ( options::bvAbstraction() &&
- !options::incrementalSolving()) {
- dumpAssertions("pre-bv-abstraction", d_assertions);
- bvAbstraction();
- dumpAssertions("post-bv-abstraction", d_assertions);
+ if (options::bvAbstraction() && !options::incrementalSolving())
+ {
+ d_preprocessingPassRegistry.getPass("bv-abstraction")->apply(&d_assertions);
}
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
}
}
-bool TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
- return bv_theory->applyAbstraction(assertions, new_assertions);
-}
-
void TheoryEngine::mkAckermanizationAssertions(std::vector<Node>& assertions) {
bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
bv_theory->mkAckermanizationAssertions(assertions);
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
public:
void staticInitializeBVOptions(const std::vector<Node>& assertions);
- bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
void mkAckermanizationAssertions(std::vector<Node>& assertions);
Node ppSimpITE(TNode assertion);
regress1/bv/divtest.smt2 \
regress1/bv/fuzz34.smt \
regress1/bv/fuzz38.smt \
+ regress1/bv/test-bv-abstraction.smt2 \
regress1/bv/unsound1.smt2 \
regress1/bvdiv2.smt2 \
regress1/constarr3.cvc \
--- /dev/null
+; COMMAND-LINE: --bv-abstraction
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 8))
+(declare-fun x1 () (_ BitVec 8))
+(declare-fun y0 () (_ BitVec 8))
+(declare-fun y1 () (_ BitVec 8))
+(declare-fun y2 () (_ BitVec 8))
+(assert
+ (or
+ (= x0 (bvadd (bvmul (_ bv2 8) y0) y1))
+ (= x0 (bvadd (bvmul (_ bv2 8) y1) y2))
+ (= x0 (bvadd (bvmul (_ bv2 8) y2) y0))
+ )
+)
+(assert
+ (or
+ (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y0) (bvmul (_ bv2 8) x0)) (_ bv5 8)))
+ (= x1 (bvadd (bvadd (bvmul (_ bv3 8) y1) (bvmul (_ bv2 8) x0)) (_ bv5 8)))
+ (= x1 (bvadd (bvadd (bvmul (_ bv3 8) x0) (bvmul (_ bv2 8) y2)) (_ bv5 8)))
+ )
+)
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff