summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/options_handler.cpp23
-rw-r--r--src/prop/cryptominisat.cpp12
-rw-r--r--src/prop/cryptominisat.h2
-rw-r--r--src/prop/sat_solver.h6
-rw-r--r--src/smt/smt_engine.cpp15
-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
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress0/bv/eager-inc-cryptominisat.smt227
-rw-r--r--test/unit/theory/theory_bv_white.h7
13 files changed, 136 insertions, 74 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));
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c43e083f3..c15e3d045 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -239,6 +239,7 @@ REG0_TESTS = \
regress0/bv/core/slice-18.smt \
regress0/bv/core/slice-19.smt \
regress0/bv/core/slice-20.smt \
+ regress0/bv/eager-inc-cryptominisat.smt2 \
regress0/bv/divtest_2_5.smt2 \
regress0/bv/divtest_2_6.smt2 \
regress0/bv/fuzz01.smt \
diff --git a/test/regress/regress0/bv/eager-inc-cryptominisat.smt2 b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2
new file mode 100644
index 000000000..1c96ca25d
--- /dev/null
+++ b/test/regress/regress0/bv/eager-inc-cryptominisat.smt2
@@ -0,0 +1,27 @@
+; REQUIRES: cryptominisat
+; COMMAND-LINE: --incremental --bv-sat-solver=cryptominisat --bitblast=eager
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+
+(assert (bvult a (bvadd b c)))
+(check-sat)
+; EXPECT: sat
+
+(push 1)
+(assert (bvult c b))
+(check-sat)
+; EXPECT: sat
+
+
+(push 1)
+(assert (bvugt c b))
+(check-sat)
+; EXPECT: unsat
+(pop 2)
+
+(check-sat)
+; EXPECT: sat
+(exit)
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index f95785f53..c830e7813 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -67,8 +67,11 @@ public:
void testBitblasterCore() {
d_smt->setOption("bitblast", SExpr("eager"));
- EagerBitblaster* bb = new EagerBitblaster(dynamic_cast<TheoryBV*>(
- d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]));
+ d_smt->setOption("incremental", SExpr("false"));
+ EagerBitblaster* bb = new EagerBitblaster(
+ dynamic_cast<TheoryBV*>(
+ d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
+ d_smt->d_context);
Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
Node x_plus_y = d_nm->mkNode(kind::BITVECTOR_PLUS, x, y);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback