diff options
author | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-28 12:35:45 -0800 |
commit | 2ba8bb701ce289ba60afec01b653b0930cc59298 (patch) | |
tree | 46df365b7b41ce662a0f94de5b11c3ed20829851 /src/theory/bv | |
parent | 42b665f2a00643c81b42932fab1441987628c5a5 (diff) |
Adding listeners to Options.
- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.
- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.
- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.
- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.
- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.
- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.
- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 1 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 17 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 |
5 files changed, 16 insertions, 19 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 66eea0997..9c6c4af9b 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -26,7 +26,6 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt/smt_globals.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" #include "util/resource_manager.h" diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 2e4f06c38..dd561667c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -43,16 +43,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); - d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, - smtStatisticsRegistry(), - "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_bitblastingRegistrar, - d_nullContext, - d_bv->globals(), - options::proof(), - "EagerBitblaster"); - + d_satSolver = prop::SatSolverFactory::createMinisat( + d_nullContext, smtStatisticsRegistry(), "EagerBitblaster"); + + d_cnfStream = new prop::TseitinCnfStream( + d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(), + "EagerBitblaster"); + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); d_bvp = NULL; diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 9268e2152..ca21e98c4 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -56,13 +56,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, d_nullContext, - d_bv->globals(), options::proof(), "LazyBitblaster"); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, + this); d_satSolver->setNotify(d_satSolverNotify); } @@ -526,11 +526,12 @@ void TLazyBitblaster::clearSolver() { d_satSolver = prop::SatSolverFactory::createMinisat( d_ctx, smtStatisticsRegistry()); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, - d_nullContext, d_bv->globals()); + d_nullContext); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : - (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); + (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, + this); d_satSolver->setNotify(d_satSolverNotify); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 8f7e975cd..191f70638 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -44,8 +44,8 @@ namespace bv { TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 27138abfc..1da15abf8 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -22,7 +22,6 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/context.h" -#include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" @@ -56,7 +55,8 @@ class TheoryBV : public Theory { public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo); ~TheoryBV(); |