summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/abstraction.cpp32
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.cpp2
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.cpp9
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp35
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h15
5 files changed, 27 insertions, 66 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a9ec7aa53..d7899f010 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -15,12 +15,14 @@
#include "theory/bv/abstraction.h"
#include "options/bv_options.h"
+#include "printer/printer.h"
#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
-
using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;
@@ -691,15 +693,6 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
}
Node AbstractionModule::simplifyConflict(TNode conflict) {
- if (Dump.isOn("bv-abstraction")) {
- NodeNodeMap seen;
- Node c = reverseAbstraction(conflict, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(c.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
-
Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
if (conflict.getKind() != kind::AND)
return conflict;
@@ -742,16 +735,6 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
Debug("bv-abstraction") << " => " << new_conflict <<"\n";
- if (Dump.isOn("bv-abstraction")) {
-
- NodeNodeMap seen;
- Node nc = reverseAbstraction(new_conflict, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(nc.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
-
return new_conflict;
}
@@ -836,15 +819,6 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
lemmas.push_back(lemma);
Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
storeLemma(lemma);
-
- if (Dump.isOn("bv-abstraction")) {
- NodeNodeMap seen;
- Node l = reverseAbstraction(lemma, seen);
- Dump("bv-abstraction") << PushCommand();
- Dump("bv-abstraction") << AssertCommand(l.toExpr());
- Dump("bv-abstraction") << CheckSatCommand();
- Dump("bv-abstraction") << PopCommand();
- }
}
}
}
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 6417740fd..48aa0fbd6 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -20,6 +20,7 @@
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/bv_solver_lazy.h"
#include "theory/bv/theory_bv.h"
@@ -71,6 +72,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_bitblastingRegistrar.get(),
d_nullContext.get(),
+ nullptr,
rm,
false,
"EagerBitblaster"));
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 1813784d7..93c91719b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -21,6 +21,7 @@
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
+#include "smt/smt_engine.h"
#include "smt/smt_statistics_registry.h"
#include "theory/bv/abstraction.h"
#include "theory/bv/bv_solver_lazy.h"
@@ -82,6 +83,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
d_nullRegistrar.get(),
d_nullContext.get(),
+ nullptr,
rm,
false,
"LazyBitblaster"));
@@ -573,8 +575,11 @@ void TLazyBitblaster::clearSolver() {
d_satSolver.reset(
prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
ResourceManager* rm = smt::currentResourceManager();
- d_cnfStream.reset(new prop::TseitinCnfStream(
- d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
+ d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
+ d_nullRegistrar.get(),
+ d_nullContext.get(),
+ nullptr,
+ rm));
d_satSolverNotify.reset(
d_emptyNotify
? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e900566f9..52f68c6ef 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -19,6 +19,10 @@
#include "expr/node_algorithm.h"
#include "options/bv_options.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "smt_util/boolean_simplification.h"
#include "theory/bv/bv_quick_check.h"
@@ -321,16 +325,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
TNode fact = worklist[r].node;
unsigned id = worklist[r].id;
- if (Dump.isOn("bv-algebraic")) {
- Node expl = d_explanations[id];
- Node query = utils::mkNot(nm->mkNode(kind::IMPLIES, expl, fact));
- Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(query.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
if (fact.isConst() &&
fact.getConst<bool>() == true) {
continue;
@@ -344,16 +338,6 @@ bool AlgebraicSolver::check(Theory::Effort e)
d_isComplete.set(true);
Debug("bv-subtheory-algebraic") << " UNSAT: assertion simplfies to false with conflict: "<< conflict << "\n";
- if (Dump.isOn("bv-algebraic")) {
- Dump("bv-algebraic")
- << EchoCommand("BVSolverLazy::AlgebraicSolver::conflict");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(conflict.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
-
++(d_statistics.d_numSimplifiesToFalse);
++(d_numSolved);
return false;
@@ -536,17 +520,6 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
Node new_right = nm->mkNode(kind::BITVECTOR_XOR, right, inverse);
bool changed = subst.addSubstitution(var, new_right, reason);
- if (Dump.isOn("bv-algebraic")) {
- Node query = utils::mkNot(nm->mkNode(
- kind::EQUAL, fact, nm->mkNode(kind::EQUAL, var, new_right)));
- Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation");
- Dump("bv-algebraic") << PushCommand();
- Dump("bv-algebraic") << AssertCommand(query.toExpr());
- Dump("bv-algebraic") << CheckSatCommand();
- Dump("bv-algebraic") << PopCommand();
- }
-
-
return changed;
}
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 0dbb51753..549843421 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -22,7 +22,10 @@
#include <sstream>
#include "context/context.h"
-#include "smt/command.h"
+#include "printer/printer.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
#include "util/statistics_registry.h"
@@ -449,9 +452,13 @@ public:
Node condition = node.eqNode(result).notNode();
- Dump("bv-rewrites")
- << CommentCommand(os.str())
- << CheckSatCommand(condition.toExpr());
+ const Printer& printer =
+ smt::currentSmtEngine()->getOutputManager().getPrinter();
+ std::ostream& out =
+ smt::currentSmtEngine()->getOutputManager().getDumpOut();
+
+ printer.toStreamCmdComment(out, os.str());
+ printer.toStreamCmdCheckSat(out, condition);
}
}
Debug("theory::bv::rewrite") << "RewriteRule<" << rule << ">(" << node << ") => " << result << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback