diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 32 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 35 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 15 |
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; |