summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.cpp29
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.h4
-rw-r--r--src/theory/bv/bv_eager_solver.cpp50
-rw-r--r--src/theory/bv/bv_eager_solver.h19
-rw-r--r--src/theory/bv/theory_bv.cpp15
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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback