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 | |
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')
34 files changed, 181 insertions, 146 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 877546da8..2c8fa9bcd 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -75,25 +75,22 @@ #ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H #define __CVC4__THEORY__ARITH__CONSTRAINT_H -#include "expr/node.h" -#include "proof/proof.h" +#include <ext/hash_map> +#include <list> +#include <set> +#include <vector> -#include "context/context.h" +#include "base/configuration_private.h" #include "context/cdlist.h" #include "context/cdqueue.h" - +#include "context/context.h" +#include "expr/node.h" +#include "proof/proof.h" #include "theory/arith/arithvar.h" -#include "theory/arith/delta_rational.h" +#include "theory/arith/callbacks.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint_forward.h" -#include "theory/arith/callbacks.h" - -#include "util/configuration_private.h" - -#include <vector> -#include <list> -#include <set> -#include <ext/hash_map> +#include "theory/arith/delta_rational.h" namespace CVC4 { namespace theory { @@ -107,7 +104,7 @@ namespace theory { namespace arith { /** - * Logs the types of different proofs. + * Logs the types of different proofs. * Current, proof types: * - NoAP : This constraint is not known to be true. * - AssumeAP : This is an input assertion. There is no proof. diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 054ab01e7..82d45871f 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -234,7 +234,7 @@ std::ostream& operator<<(std::ostream& os, const NodeLog& nl); class ApproximateSimplex; class TreeLog { private: - ApproximateSimplex* d_generator CVC4_UNUSED; + ApproximateSimplex* d_generator; int next_exec_ord; typedef std::map<int, NodeLog> ToNodeMap; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 843feed01..3c7a767c6 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -31,8 +31,8 @@ namespace arith { TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) + const LogicInfo& logicInfo) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) , d_ppRewriteTimer("theory::arith::ppRewriteTimer") { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c54414109..b69d51966 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -47,8 +47,7 @@ private: public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + Valuation valuation, const LogicInfo& logicInfo); virtual ~TheoryArith(); /** diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index cbcccd734..f9e036aa3 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -55,9 +55,8 @@ const bool d_solveWrite2 = false; TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals, - std::string name) - : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals, name), + const LogicInfo& logicInfo, std::string name) + : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, name), d_numRow(name + "theory::arrays::number of Row lemmas", 0), d_numExt(name + "theory::arrays::number of Ext lemmas", 0), d_numProp(name + "theory::arrays::number of propagations", 0), diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 88d83bfb9..eba6c000e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -93,7 +93,7 @@ class TheoryArrays : public Theory { // MISC ///////////////////////////////////////////////////////////////////////////// - private: + private: /** True node for predicates = true */ Node d_true; @@ -124,11 +124,11 @@ class TheoryArrays : public Theory { /** conflicts in setModelVal */ IntStat d_numSetModelValConflicts; - public: + public: TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals, std::string name = ""); + std::string instanceName = ""); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -139,7 +139,7 @@ class TheoryArrays : public Theory { // PREPROCESSING ///////////////////////////////////////////////////////////////////////////// - private: + private: // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used class PPNotifyClass { diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 246f1e7e8..dc42fc281 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -29,9 +29,8 @@ namespace booleans { class TheoryBool : public Theory { public: TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals) - : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, globals) + Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {} PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 2fbc0e402..facc10c67 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -29,8 +29,8 @@ class TheoryBuiltin : public Theory { public: TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, globals) {} + const LogicInfo& logicInfo) + : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ 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(); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index d49974df2..e33b4d05c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -40,10 +40,8 @@ namespace theory { namespace datatypes { TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo, - SmtGlobals* globals) - : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, globals), + Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), //d_cycle_check(c), d_hasSeenCycle(c, false), d_infer(c), diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 212b9d7cf..82306b863 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -215,7 +215,7 @@ protected: public: TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals); + const LogicInfo& logicInfo); ~TheoryDatatypes(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 9a8d77844..18bf993ad 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -7,44 +7,52 @@ namespace theory { namespace fp { namespace removeToFPGeneric { - + Node removeToFPGeneric (TNode node) { Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); - - FloatingPointToFPGeneric info = node.getOperator().getConst<FloatingPointToFPGeneric>(); - + + FloatingPointToFPGeneric info = + node.getOperator().getConst<FloatingPointToFPGeneric>(); + size_t children = node.getNumChildren(); - + Node op; - + if (children == 1) { - op = NodeManager::currentNM()->mkConst(FloatingPointToFPIEEEBitVector(info.t.exponent(), - info.t.significand())); + op = NodeManager::currentNM()->mkConst( + FloatingPointToFPIEEEBitVector(info.t.exponent(), + info.t.significand())); return NodeManager::currentNM()->mkNode(op, node[0]); - + } else { Assert(children == 2); Assert(node[0].getType().isRoundingMode()); - + TypeNode t = node[1].getType(); - + if (t.isFloatingPoint()) { - op = NodeManager::currentNM()->mkConst(FloatingPointToFPFloatingPoint(info.t.exponent(), - info.t.significand())); + op = NodeManager::currentNM()->mkConst( + FloatingPointToFPFloatingPoint(info.t.exponent(), + info.t.significand())); } else if (t.isReal()) { - op = NodeManager::currentNM()->mkConst(FloatingPointToFPReal(info.t.exponent(), - info.t.significand())); + op = NodeManager::currentNM()->mkConst( + FloatingPointToFPReal(info.t.exponent(), + info.t.significand())); } else if (t.isBitVector()) { - op = NodeManager::currentNM()->mkConst(FloatingPointToFPSignedBitVector(info.t.exponent(), - info.t.significand())); - + op = NodeManager::currentNM()->mkConst( + FloatingPointToFPSignedBitVector(info.t.exponent(), + info.t.significand())); + } else { - throw TypeCheckingExceptionPrivate(node, "cannot rewrite to_fp generic due to incorrect type of second argument"); + throw TypeCheckingExceptionPrivate( + node, + "cannot rewrite to_fp generic due to incorrect type of second " + "argument"); } - + return NodeManager::currentNM()->mkNode(op, node[0], node[1]); } - + Unreachable("to_fp generic not rewritten"); } } @@ -53,8 +61,8 @@ namespace removeToFPGeneric { /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp::TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_FP, c, u, out, valuation, logicInfo, globals) + const LogicInfo& logicInfo) + : Theory(THEORY_FP, c, u, out, valuation, logicInfo) {}/* TheoryFp::TheoryFp() */ diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index fe3c377af..ac2c68ac4 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -17,8 +17,7 @@ public: context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - SmtGlobals* globals); + const LogicInfo& logicInfo); Node expandDefinition(LogicRequest &, Node node); diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 8cba51c8f..815f5e76a 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -32,8 +32,8 @@ namespace idl { TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, globals) + const LogicInfo& logicInfo) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) , d_model(c) , d_assertionsDB(c) {} diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index aa7267eb7..7c879e722 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -45,8 +45,7 @@ public: /** Theory constructor. */ TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + Valuation valuation, const LogicInfo& logicInfo); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 02eeefcaf..fb689609d 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -24,8 +24,6 @@ #include "base/cvc4_assert.h" #include "expr/kind.h" -#warning "TODO: Remove logic_info_forward.h" - using namespace std; using namespace CVC4::theory; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 54b735114..6d7297c63 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -24,7 +24,6 @@ #include <string> #include <vector> #include "expr/kind.h" -#include "options/logic_info_forward.h" namespace CVC4 { diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index b6162ec38..9107eb72d 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -128,7 +128,7 @@ function alternate { " eval "alternate_for_$1=\"\${alternate_for_$1} - if(options::theoryAlternates()[\\\"$2\\\"]) { + if(engine->useTheoryAlternative(\\\"$2\\\")) { engine->addTheory< $3 >($1); return; }\"" diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index b808f4cd5..86fc057ea 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -34,8 +34,8 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals), +TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), d_masterEqualityEngine(0) { d_numInstantiations = 0; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 63f3379b8..6335349b1 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -53,7 +53,7 @@ private: public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals); + const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 82ebb5bf8..1280ad58d 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -25,9 +25,8 @@ TheorySets::TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - SmtGlobals* globals) - : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo) + : Theory(THEORY_SETS, c, u, out, valuation, logicInfo), d_internal(new TheorySetsPrivate(*this, c, u)) {} diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 7ff8abec6..bc39fcbbd 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -41,8 +41,7 @@ public: * contexts. */ TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals); + Valuation valuation, const LogicInfo& logicInfo); ~TheorySets(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 07a170a08..c0a892926 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -58,8 +58,8 @@ Node TheoryStrings::TermIndex::add( Node n, unsigned index, TheoryStrings* t, No TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, globals), + const LogicInfo& logicInfo) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), RMAXINT(LONG_MAX), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ddb800ee1..fef2983fd 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -54,7 +54,7 @@ class TheoryStrings : public Theory { public: TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals); + const LogicInfo& logicInfo); ~TheoryStrings(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 45c9b1936..ee5efc8db 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -17,6 +17,9 @@ #include "theory/theory.h" #include <vector> +#include <sstream> +#include <iostream> +#include <string> #include "base/cvc4_assert.h" #include "smt/smt_statistics_registry.h" @@ -48,9 +51,11 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){ return os; }/* ostream& operator<<(ostream&, Theory::Effort) */ -Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals, std::string name) throw() + +Theory::Theory(TheoryId id, context::Context* satContext, + context::UserContext* userContext, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + std::string name) throw() : d_id(id) , d_instanceName(name) , d_satContext(satContext) @@ -67,7 +72,6 @@ Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* , d_out(&out) , d_valuation(valuation) , d_proofsEnabled(false) - , d_globals(globals) { smtStatisticsRegistry()->registerStat(&d_checkTime); smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime); @@ -204,7 +208,8 @@ void Theory::debugPrintFacts() const{ std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{ std::hash_set<TNode, TNodeHashFunction> currentlyShared; - for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){ + for (shared_terms_iterator i = shared_terms_begin(), + i_end = shared_terms_end(); i != i_end; ++i) { currentlyShared.insert (*i); } return currentlyShared; @@ -242,18 +247,21 @@ void Theory::computeRelevantTerms(set<Node>& termSet) const } -Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions) +Theory::PPAssertStatus Theory::ppAssert(TNode in, + SubstitutionMap& outSubstitutions) { if (in.getKind() == kind::EQUAL) { // (and (= x t) phi) can be replaced by phi[x/t] if // 1) x is a variable // 2) x is not in the term t // 3) x : T and t : S, then S <: T - if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){ + if (in[0].isVar() && !in[1].hasSubterm(in[0]) && + (in[1].getType()).isSubtypeOf(in[0].getType()) ){ outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){ + if (in[1].isVar() && !in[0].hasSubterm(in[1]) && + (in[0].getType()).isSubtypeOf(in[1].getType())){ outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } @@ -267,9 +275,10 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti return PP_ASSERT_STATUS_UNSOLVED; } -std::pair<bool, Node> Theory::entailmentCheck(TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out){ +std::pair<bool, Node> Theory::entailmentCheck( + TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out) { return make_pair(false, Node::null()); } @@ -277,6 +286,12 @@ EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) : d_tid(tid) { } +std::string Theory::getFullInstanceName() const { + std::stringstream ss; + ss << "theory<" << d_id << ">" << d_instanceName; + return ss.str(); +} + EntailmentCheckParameters::~EntailmentCheckParameters(){} TheoryId EntailmentCheckParameters::getTheoryId() const { diff --git a/src/theory/theory.h b/src/theory/theory.h index 2c3c66d8b..9849dd0b9 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -20,9 +20,8 @@ #define __CVC4__THEORY__THEORY_H #include <ext/hash_set> -#include <iostream> +#include <iosfwd> #include <string> -#include <strings.h> #include "context/cdlist.h" #include "context/cdo.h" @@ -33,7 +32,6 @@ #include "options/theory_options.h" #include "options/theoryof_mode.h" #include "smt/logic_request.h" -#include "smt/smt_globals.h" #include "smt_util/command.h" #include "smt_util/dump.h" #include "theory/logic_info.h" @@ -140,9 +138,9 @@ private: friend class ::CVC4::TheoryEngine; // Disallow default construction, copy, assignment. - Theory() CVC4_UNUSED; - Theory(const Theory&) CVC4_UNUSED; - Theory& operator=(const Theory&) CVC4_UNUSED; + Theory() CVC4_UNDEFINED; + Theory(const Theory&) CVC4_UNDEFINED; + Theory& operator=(const Theory&) CVC4_UNDEFINED; /** * An integer identifying the type of the theory @@ -153,7 +151,7 @@ private: * an unique string identifier for each instance of a Theory class. We need * this to ensure unique statistics names over multiple theory instances. */ std::string d_instanceName; - + /** * The SAT search context for the Theory. */ @@ -243,10 +241,14 @@ protected: /** * Construct a Theory. + * + * The pair <id, instance> is assumed to uniquely identify this Theory + * w.r.t. the SmtEngine. */ - Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals, std::string name = "") throw(); // taking : No default. + Theory(TheoryId id, context::Context* satContext, + context::UserContext* userContext, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + std::string instance = "") throw(); // taking : No default. /** * This is called at shutdown time by the TheoryEngine, just before @@ -295,7 +297,11 @@ protected: void printFacts(std::ostream& os) const; void debugPrintFacts() const; - SmtGlobals* d_globals; + /** + * Whether proofs are enabled + * + */ + bool d_proofEnabled; public: @@ -415,13 +421,13 @@ public: return d_id; } - std::string getFullInstanceName() const { - std::stringstream ss; - ss << "theory<" << d_id << ">" << d_instanceName; - return ss.str(); - } + /** + * Returns a string that uniquely identifies this theory solver w.r.t. the + * SmtEngine. + */ + std::string getFullInstanceName() const; + - /** * Get the SAT context associated to this Theory. */ @@ -865,9 +871,6 @@ public: * Turn on proof-production mode. */ void produceProofs() { d_proofsEnabled = true; } - - /** Returns a pointer to the globals copy the theory is using. */ - SmtGlobals* globals() { return d_globals; } };/* class Theory */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index be2a89dbc..60716146e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -104,7 +104,7 @@ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logicInfo, - SmtGlobals* globals) + LemmaChannels* channels) : d_propEngine(NULL), d_decisionEngine(NULL), d_context(context), @@ -133,16 +133,20 @@ TheoryEngine::TheoryEngine(context::Context* context, d_false(), d_interrupted(false), d_resourceManager(NodeManager::currentResourceManager()), - d_globals(globals), + d_channels(channels), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)), d_bvToBoolPreprocessor(), + d_theoryAlternatives(), + d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) { - for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; + ++ theoryId) + { d_theoryTable[theoryId] = NULL; d_theoryOut[theoryId] = NULL; } @@ -155,7 +159,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - PROOF (ProofManager::currentPM()->initTheoryProofEngine(d_globals); ); + PROOF (ProofManager::currentPM()->initTheoryProofEngine(); ); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); @@ -1398,8 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // Share with other portfolio threads - if(d_globals->getLemmaOutputChannel() != NULL) { - d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); + if(d_channels->getLemmaOutputChannel() != NULL) { + d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); } // Run theory preprocessing, maybe @@ -1769,6 +1773,18 @@ void TheoryEngine::spendResource(unsigned ammount) { d_resourceManager->spendResource(ammount); } +void TheoryEngine::enableTheoryAlternative(const std::string& name){ + Debug("TheoryEngine::enableTheoryAlternative") + << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl; + + d_theoryAlternatives.insert(name); +} + +bool TheoryEngine::useTheoryAlternative(const std::string& name) { + return d_theoryAlternatives.find(name) != d_theoryAlternatives.end(); +} + + TheoryEngine::Statistics::Statistics(theory::TheoryId theory): conflicts(mkName("theory<", theory, ">::conflicts"), 0), propagations(mkName("theory<", theory, ">::propagations"), 0), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0bf00c079..cdd05c096 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY_ENGINE_H #include <deque> +#include <set> #include <vector> #include <utility> @@ -29,8 +30,8 @@ #include "options/options.h" #include "options/smt_options.h" #include "prop/prop_engine.h" -#include "smt/smt_globals.h" #include "smt_util/command.h" +#include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" #include "theory/bv/bv_to_bool.h" #include "theory/interrupted.h" @@ -467,14 +468,15 @@ class TheoryEngine { bool d_interrupted; ResourceManager* d_resourceManager; - /** Container for misc. globals. */ - SmtGlobals* d_globals; + /** Container for lemma input and output channels. */ + LemmaChannels* d_channels; public: /** Constructs a theory engine */ TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals); + RemoveITE& iteRemover, const LogicInfo& logic, + LemmaChannels* channels); /** Destroys a theory engine */ ~TheoryEngine(); @@ -495,7 +497,7 @@ public: d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], - theory::Valuation(this), d_logicInfo, d_globals); + theory::Valuation(this), d_logicInfo); } inline void setPropEngine(prop::PropEngine* propEngine) { @@ -832,7 +834,15 @@ public: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); + /** Theory alternative is in use. */ + bool useTheoryAlternative(const std::string& name); + + /** Enables using a theory alternative by name. */ + void enableTheoryAlternative(const std::string& name); + private: + std::set< std::string > d_theoryAlternatives; + std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; public: diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 93a920f82..e58c11aca 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -36,18 +36,19 @@ namespace uf { /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, SmtGlobals* globals, std::string name) - : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name), + const LogicInfo& logicInfo, std::string instanceName) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, instanceName), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ d_thss(NULL), - d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true), + d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF", + true), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_functionsTerms(c), - d_symb(u, name) + d_symb(u, instanceName) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index bd0016be7..e29b923f9 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -169,7 +169,7 @@ public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - SmtGlobals* globals, std::string name = ""); + std::string instanceName = ""); ~TheoryUF(); |