diff options
Diffstat (limited to 'src/theory')
-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 |
5 files changed, 78 insertions, 39 deletions
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)); |