From: Mathias Preiner Date: Tue, 8 May 2018 22:18:15 +0000 (-0700) Subject: Refactor bv-abstraction preprocessing pass. (#1860) X-Git-Tag: cvc5-1.0.0~5075 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08ddea9c91fc5c481642c4911d4af562ac2a88e1;p=cvc5.git Refactor bv-abstraction preprocessing pass. (#1860) --- diff --git a/src/Makefile.am b/src/Makefile.am index 0eefbc1de..411fd363e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -62,6 +62,8 @@ libcvc4_la_SOURCES = \ 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 \ 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 + +#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 new_assertions; + std::vector assertions(assertionsToPreprocess->begin(), + assertionsToPreprocess->end()); + TheoryEngine* te = d_preprocContext->getTheoryEngine(); + bv::TheoryBV* bv_theory = static_cast(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; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 565f99ec5..113d53507 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -69,6 +69,7 @@ #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" @@ -613,10 +614,6 @@ public: */ 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(); @@ -2588,6 +2585,8 @@ void SmtEnginePrivate::finishInit() { // actually assembling preprocessing pipelines). std::unique_ptr boolToBv( new BoolToBV(d_preprocessingPassContext.get())); + std::unique_ptr bvAbstract( + new BvAbstraction(d_preprocessingPassContext.get())); std::unique_ptr bvGauss( new BVGauss(d_preprocessingPassContext.get())); std::unique_ptr bvIntroPow2( @@ -2601,6 +2600,8 @@ void SmtEnginePrivate::finishInit() { std::unique_ptr 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)); @@ -3184,24 +3185,6 @@ bool SmtEnginePrivate::nonClausalSimplify() { return true; } -void SmtEnginePrivate::bvAbstraction() { - Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl; - std::vector 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); @@ -4042,11 +4025,9 @@ void SmtEnginePrivate::processAssertions() { 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; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 11da42e07..74b73d718 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1992,11 +1992,6 @@ void TheoryEngine::staticInitializeBVOptions( } } -bool TheoryEngine::ppBvAbstraction(const std::vector& assertions, std::vector& new_assertions) { - bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; - return bv_theory->applyAbstraction(assertions, new_assertions); -} - void TheoryEngine::mkAckermanizationAssertions(std::vector& assertions) { bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; bv_theory->mkAckermanizationAssertions(assertions); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 80853bb6f..3ae0a9ea9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -852,7 +852,6 @@ private: /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: void staticInitializeBVOptions(const std::vector& assertions); - bool ppBvAbstraction(const std::vector& assertions, std::vector& new_assertions); void mkAckermanizationAssertions(std::vector& assertions); Node ppSimpITE(TNode assertion); diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index cf702ed7c..b86ee911d 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1035,6 +1035,7 @@ REG1_TESTS = \ 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 \ diff --git a/test/regress/regress1/bv/test-bv-abstraction.smt2 b/test/regress/regress1/bv/test-bv-abstraction.smt2 new file mode 100644 index 000000000..7a926d4be --- /dev/null +++ b/test/regress/regress1/bv/test-bv-abstraction.smt2 @@ -0,0 +1,24 @@ +; 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)