diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/options/options_handler.cpp | 23 | ||||
-rw-r--r-- | src/prop/cryptominisat.cpp | 12 | ||||
-rw-r--r-- | src/prop/cryptominisat.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 29 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 50 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 19 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 15 |
10 files changed, 103 insertions, 72 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b48647116..a72eb2c30 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1088,12 +1088,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, return theory::bv::SAT_SOLVER_MINISAT; } else if(optarg == "cryptominisat") { - if (options::incrementalSolving() && - options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("CryptoMinSat does not support incremental mode. \n\ - Try --bv-sat-solver=minisat")); - } - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY && options::bitblastMode.wasSetByUser()) { throw OptionException( @@ -1103,12 +1097,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); } - - // if (!options::bvAbstraction.wasSetByUser() && - // !options::skolemizeArguments.wasSetByUser()) { - // options::bvAbstraction.set(true); - // options::skolemizeArguments.set(true); - // } return theory::bv::SAT_SOLVER_CRYPTOMINISAT; } else if (optarg == "cadical") @@ -1118,7 +1106,8 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, { throw OptionException( std::string("CaDiCaL does not support incremental mode. \n\ - Try --bv-sat-solver=minisat")); + Try --bv-sat-solver=cryptominisat or " + "--bv-sat-solver=minisat")); } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY @@ -1126,7 +1115,7 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option, { throw OptionException( std::string("CaDiCaL does not support lazy bit-blasting. \n\ - Try --bv-sat-solver=minisat")); + Try --bv-sat-solver=minisat")); } if (!options::bitvectorToBool.wasSetByUser()) { @@ -1180,12 +1169,6 @@ theory::bv::BitblastMode OptionsHandler::stringToBitblastMode( } return theory::bv::BITBLAST_MODE_LAZY; } else if(optarg == "eager") { - - if (options::incrementalSolving() && - options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ - Try --bitblast=lazy")); - } if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); } diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 4f239343e..df5a20791 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -164,6 +164,18 @@ SatValue CryptoMinisatSolver::solve(long unsigned int& resource) { return solve(); } +SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions) +{ + TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime); + std::vector<CMSat::Lit> assumpts; + for (const SatLiteral& lit : assumptions) + { + assumpts.push_back(toInternalLit(lit)); + } + ++d_statistics.d_statCallsToSolve; + return toSatLiteralValue(d_solver->solve(&assumpts)); +} + SatValue CryptoMinisatSolver::value(SatLiteral l){ const std::vector<CMSat::lbool> model = d_solver->get_model(); CMSatVar var = l.getSatVariable(); diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index c265b2f35..c5345cb86 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -64,6 +64,8 @@ public: SatValue solve() override; SatValue solve(long unsigned int&) override; + SatValue solve(const std::vector<SatLiteral>& assumptions) override; + bool ok() const override; SatValue value(SatLiteral l) override; SatValue modelValue(SatLiteral l) override; diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 055efa413..add73eebe 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -76,6 +76,12 @@ public: /** Check the satisfiability of the added clauses */ virtual SatValue solve(long unsigned int&) = 0; + /** Check satisfiability under assumptions */ + virtual SatValue solve(const std::vector<SatLiteral>& assumptions) + { + Unimplemented("Solving under assumptions not implemented"); + }; + /** Interrupt the solver */ virtual void interrupt() = 0; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5296a3bca..de4537807 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1318,18 +1318,6 @@ void SmtEngine::setDefaults() { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - if (options::incrementalSolving()) - { - if (options::incrementalSolving.wasSetByUser()) - { - throw OptionException(std::string( - "Eager bit-blasting does not currently support incremental mode. " - "Try --bitblast=lazy")); - } - Notice() << "SmtEngine: turning off incremental to support eager " - << "bit-blasting" << endl; - setOption("incremental", SExpr("false")); - } if (options::produceModels() && (d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_UF))) @@ -4160,7 +4148,8 @@ void SmtEnginePrivate::processAssertions() { "Try --bv-div-zero-const to interpret division by zero as a constant."); } - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && !options::incrementalSolving()) { d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions); } diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 7b12c3465..01437cb64 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -30,8 +30,9 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) : TBitblaster<Node>(), + d_context(c), d_nullContext(new context::Context()), d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), @@ -75,9 +76,18 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) EagerBitblaster::~EagerBitblaster() {} -void EagerBitblaster::bbFormula(TNode node) { - d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, - TNode::null()); +void EagerBitblaster::bbFormula(TNode node) +{ + /* For incremental eager solving we assume formulas at context levels > 1. */ + if (options::incrementalSolving() && d_context->getLevel() > 1) + { + d_cnfStream->ensureLiteral(node); + } + else + { + d_cnfStream->convertAndAssert( + node, false, false, RULE_INVALID, TNode::null()); + } } /** @@ -185,6 +195,17 @@ bool EagerBitblaster::solve() { return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } +bool EagerBitblaster::solve(const std::vector<Node>& assumptions) +{ + std::vector<prop::SatLiteral> assumpts; + for (const Node& assumption : assumptions) + { + Assert(d_cnfStream->hasLiteral(assumption)); + assumpts.push_back(d_cnfStream->getLiteral(assumption)); + } + return prop::SAT_VALUE_TRUE == d_satSolver->solve(assumpts); +} + /** * Returns the value a is currently assigned to in the SAT solver * or null if the value is completely unassigned. diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index fbf1a4ddb..3e6190d76 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -36,7 +36,7 @@ class TheoryBV; class EagerBitblaster : public TBitblaster<Node> { public: - EagerBitblaster(TheoryBV* theory_bv); + EagerBitblaster(TheoryBV* theory_bv, context::Context* context); ~EagerBitblaster(); void addAtom(TNode atom); @@ -51,10 +51,12 @@ class EagerBitblaster : public TBitblaster<Node> bool assertToSat(TNode node, bool propagate = true); bool solve(); + bool solve(const std::vector<Node>& assumptions); bool collectModelInfo(TheoryModel* m, bool fullModel); void setProofLog(BitVectorProof* bvp); private: + context::Context* d_context; std::unique_ptr<context::Context> d_nullContext; typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 27dccfde0..7dd3fd3e7 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -2,7 +2,7 @@ /*! \file bv_eager_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Mathias Preiner + ** Liana Hadarean, Mathias Preiner, Tim King ** 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. @@ -27,24 +27,20 @@ namespace CVC4 { namespace theory { namespace bv { -EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv) - : d_assertionSet(), - d_bitblaster(nullptr), - d_aigBitblaster(nullptr), +EagerBitblastSolver::EagerBitblastSolver(context::Context* c, TheoryBV* bv) + : d_assertionSet(c), + d_assumptionSet(c), + d_context(c), + d_bitblaster(), + d_aigBitblaster(), d_useAig(options::bitvectorAig()), d_bv(bv), - d_bvp(nullptr) {} - -EagerBitblastSolver::~EagerBitblastSolver() { - if (d_useAig) { - Assert(d_bitblaster == nullptr); - delete d_aigBitblaster; - } else { - Assert(d_aigBitblaster == nullptr); - delete d_bitblaster; - } + d_bvp(nullptr) +{ } +EagerBitblastSolver::~EagerBitblastSolver() {} + void EagerBitblastSolver::turnOffAig() { Assert(d_aigBitblaster == nullptr && d_bitblaster == nullptr); d_useAig = false; @@ -54,15 +50,15 @@ void EagerBitblastSolver::initialize() { Assert(!isInitialized()); if (d_useAig) { #ifdef CVC4_USE_ABC - d_aigBitblaster = new AigBitblaster(); + d_aigBitblaster.reset(new AigBitblaster()); #else Unreachable(); #endif } else { - d_bitblaster = new EagerBitblaster(d_bv); + d_bitblaster.reset(new EagerBitblaster(d_bv, d_context)); THEORY_PROOF(if (d_bvp) { d_bitblaster->setProofLog(d_bvp); - d_bvp->setBitblaster(d_bitblaster); + d_bvp->setBitblaster(d_bitblaster.get()); }); } } @@ -79,6 +75,10 @@ void EagerBitblastSolver::assertFormula(TNode formula) { Assert(isInitialized()); Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula " << formula << "\n"; + if (options::incrementalSolving() && d_context->getLevel() > 1) + { + d_assumptionSet.insert(formula); + } d_assertionSet.insert(formula); // ensures all atoms are bit-blasted and converted to AIG if (d_useAig) { @@ -87,7 +87,9 @@ void EagerBitblastSolver::assertFormula(TNode formula) { #else Unreachable(); #endif - } else { + } + else + { d_bitblaster->bbFormula(formula); } } @@ -100,8 +102,8 @@ bool EagerBitblastSolver::checkSat() { if (d_useAig) { #ifdef CVC4_USE_ABC - const std::vector<TNode> assertions = {d_assertionSet.begin(), - d_assertionSet.end()}; + const std::vector<Node> assertions = {d_assertionSet.key_begin(), + d_assertionSet.key_end()}; Assert(!assertions.empty()); Node query = utils::mkAnd(assertions); @@ -111,6 +113,12 @@ bool EagerBitblastSolver::checkSat() { #endif } + if (options::incrementalSolving()) + { + const std::vector<Node> assumptions = {d_assumptionSet.key_begin(), + d_assumptionSet.key_end()}; + return d_bitblaster->solve(assumptions); + } return d_bitblaster->solve(); } diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 2754bdd3b..6a89a0f7c 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -2,7 +2,7 @@ /*! \file bv_eager_solver.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Andrew Reynolds + ** Liana Hadarean, Tim King, 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. @@ -16,7 +16,8 @@ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__THEORY__BV__BV_EAGER_SOLVER_H +#define __CVC4__THEORY__BV__BV_EAGER_SOLVER_H #include <unordered_set> #include <vector> @@ -37,7 +38,7 @@ class AigBitblaster; */ class EagerBitblastSolver { public: - EagerBitblastSolver(theory::bv::TheoryBV* bv); + EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -51,11 +52,13 @@ class EagerBitblastSolver { void setProofLog(BitVectorProof* bvp); private: - typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; - AssertionSet d_assertionSet; + context::CDHashSet<Node, NodeHashFunction> d_assertionSet; + context::CDHashSet<Node, NodeHashFunction> d_assumptionSet; + context::Context* d_context; + /** Bitblasters */ - EagerBitblaster* d_bitblaster; - AigBitblaster* d_aigBitblaster; + std::unique_ptr<EagerBitblaster> d_bitblaster; + std::unique_ptr<AigBitblaster> d_aigBitblaster; bool d_useAig; TheoryBV* d_bv; @@ -65,3 +68,5 @@ class EagerBitblastSolver { } // namespace bv } // namespace theory } // namespace CVC4 + +#endif // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 7dc6d3710..c4d419d83 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -74,7 +74,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver = new EagerBitblastSolver(this); + d_eagerSolver = new EagerBitblastSolver(c, this); return; } @@ -243,18 +243,20 @@ void TheoryBV::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == BITBLAST_MODE_EAGER) + { // the aig bit-blaster option is set heuristically - // if bv abstraction is not used - if (!d_eagerSolver->isInitialized()) { + // if bv abstraction is used + if (!d_eagerSolver->isInitialized()) + { d_eagerSolver->initialize(); } - if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) { + if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) + { Node formula = node[0]; d_eagerSolver->assertFormula(formula); } - // nothing to do for the other terms return; } @@ -342,6 +344,7 @@ void TheoryBV::check(Effort e) TNode fact = get().assertion; Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM); assertions.push_back(fact); + d_eagerSolver->assertFormula(fact[0]); } Assert (d_eagerSolver->hasAssertions(assertions)); |