diff options
| author | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-01-05 16:29:44 -0800 |
| commit | 5eabda0f55cee3be81aa7ae126269c32e818322f (patch) | |
| tree | b873e4cb8e5d37ff3bb70596494bc5964aaef135 /src | |
| parent | b717513e2a1d956c4456d13e0625957fc84c2449 (diff) | |
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
Diffstat (limited to 'src')
71 files changed, 818 insertions, 562 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 773acf67e..d5223773e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -102,6 +102,8 @@ libcvc4_la_SOURCES = \ smt/smt_engine.cpp \ smt/smt_engine_check_proof.cpp \ smt/smt_engine.h \ + smt/smt_globals.cpp \ + smt/smt_globals.h \ smt/model_postprocessor.cpp \ smt/model_postprocessor.h \ smt/smt_options_handler.cpp \ diff --git a/src/base/Makefile.am b/src/base/Makefile.am index b03b61aee..ed41db8ed 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -19,8 +19,6 @@ libbase_la_SOURCES = \ cvc4_assert.h \ exception.cpp \ exception.h \ - lemma_input_channel_forward.h \ - lemma_output_channel_forward.h \ modal_exception.h \ output.cpp \ output.h diff --git a/src/base/lemma_input_channel_forward.h b/src/base/lemma_input_channel_forward.h deleted file mode 100644 index f74e24b4a..000000000 --- a/src/base/lemma_input_channel_forward.h +++ /dev/null @@ -1,30 +0,0 @@ -/********************* */ -/*! \file lemma_input_channel_forward.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Forward declaration of LemmaInputChannel. - ** - ** This forward declaration of LemmaInputChannel is needed for the option - ** lemmaInputChannel (defined in smt_options) can be a LemmaInputChannel* - ** without including expr.h. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H -#define __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H - -namespace CVC4 { - -class CVC4_PUBLIC LemmaInputChannel; - -}/* CVC4 namespace */ - -#endif /* __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H */ diff --git a/src/base/lemma_output_channel_forward.h b/src/base/lemma_output_channel_forward.h deleted file mode 100644 index c53bcc36f..000000000 --- a/src/base/lemma_output_channel_forward.h +++ /dev/null @@ -1,35 +0,0 @@ -/********************* */ -/*! \file lemma_output_channel_forward.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Forward declaration of the LemmaOutputChannel - ** - ** This forward declaration of LemmaOutputChannel is needed for the option - ** lemmaOutputChannel (defined in smt_options) can be a LemmaInputChannel* - ** without including expr.h. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H -#define __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H - -namespace CVC4 { - -/** - * This interface describes a mechanism for the propositional and theory - * engines to communicate with the "outside world" about new lemmas being - * discovered. - */ -class CVC4_PUBLIC LemmaOutputChannel; - -}/* CVC4 namespace */ - -#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H */ diff --git a/src/cvc4.i b/src/cvc4.i index 6ee0c7572..e81276f23 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -322,6 +322,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "util/hash.i" %include "util/proof.i" %include "util/regexp.i" +%include "util/result.i" %include "util/subrange_bound.i" %include "util/tuple.i" //%include "util/floatingpoint.i" @@ -335,7 +336,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "expr/predicate.i" %include "expr/record.i" %include "expr/resource_manager.i" -%include "expr/result.i" %include "proof/unsat_core.i" // TIM: diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 63f31ed67..d4964f56a 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -70,8 +70,6 @@ libexpr_la_SOURCES = \ predicate.cpp \ record.cpp \ record.h \ - result.cpp \ - result.h \ uninterpreted_constant.cpp \ uninterpreted_constant.h @@ -113,7 +111,6 @@ EXTRA_DIST = \ resource_manager.i \ sexpr.i \ record.i \ - result.i \ predicate.i \ variable_type_map.i \ uninterpreted_constant.i diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 8ef1a6a5f..df9c9e19f 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -65,6 +65,8 @@ public: d_stats.flushInformation(out); } + SmtGlobals* globals() { return d_smtEngine->globals(); } + protected: /** Executes treating cmd as a singleton */ virtual bool doCommandSingleton(CVC4::Command* cmd); @@ -74,9 +76,7 @@ private: };/* class CommandExecutor */ -bool smtEngineInvoke(SmtEngine* smt, - Command* cmd, - std::ostream *out); +bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out); }/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index c471ae585..cdd20c05a 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -117,24 +117,24 @@ void CommandExecutorPortfolio::lemmaSharingInit() const unsigned int sharingChannelSize = 1000000; for(unsigned i = 0; i < d_numThreads; ++i){ - d_channelsOut.push_back - (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); - d_channelsIn.push_back - (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); + d_channelsOut.push_back( + new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); + d_channelsIn.push_back( + new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); } /* Lemma I/O channels */ for(unsigned i = 0; i < d_numThreads; ++i) { string tag = "thread #" + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]); - d_threadOptions[i].set - (options::lemmaOutputChannel, - new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to)); - d_threadOptions[i].set - (options::lemmaInputChannel, - new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], - d_vmaps[i]->d_from, d_vmaps[i]->d_to)); + LemmaOutputChannel* outputChannel = + new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i], + d_vmaps[i]->d_from, d_vmaps[i]->d_to); + LemmaInputChannel* inputChannel = + new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i], + d_vmaps[i]->d_from, d_vmaps[i]->d_to); + d_smts[i]->globals()->setLemmaInputChannel(inputChannel); + d_smts[i]->globals()->setLemmaOutputChannel(outputChannel); } /* Output to string stream */ @@ -163,8 +163,10 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() for(unsigned i = 0; i < d_numThreads; ++i) { delete d_channelsIn[i]; delete d_channelsOut[i]; - d_threadOptions[i].set(options::lemmaInputChannel, NULL); - d_threadOptions[i].set(options::lemmaOutputChannel, NULL); + delete d_smts[i]->globals()->getLemmaInputChannel(); + d_smts[i]->globals()->setLemmaInputChannel(NULL); + delete d_smts[i]->globals()->getLemmaOutputChannel(); + d_smts[i]->globals()->setLemmaOutputChannel(NULL); } d_channelsIn.clear(); d_channelsOut.clear(); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index fd5aec7d0..c110ffa4f 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -28,7 +28,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "main/command_executor.h" @@ -50,6 +49,7 @@ #include "smt/smt_options_handler.h" #include "smt_util/command.h" #include "util/configuration.h" +#include "util/result.h" using namespace std; using namespace CVC4; @@ -285,11 +285,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParserBuilder.withStreamInput(cin); } replayParser = replayParserBuilder.build(); - opts.set(options::replayStream, new Parser::ExprStream(replayParser)); + pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser)); } - if( opts[options::replayLog] != NULL ) { - *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) - << expr::ExprSetDepth(-1); + if( pExecutor->globals()->getReplayLog() != NULL ) { + *(pExecutor->globals()->getReplayLog()) << + language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1); } int returnValue = 0; @@ -569,10 +569,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete parser; } - if( opts[options::replayStream] != NULL ) { + if( pExecutor->globals()->getReplayStream() != NULL ) { + ExprStream* replayStream = pExecutor->globals()->getReplayStream(); + pExecutor->globals()->setReplayStream(NULL); // this deletes the expression parser too - delete opts[options::replayStream]; - opts.set(options::replayStream, NULL); + delete replayStream; } Result result; @@ -610,8 +611,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // make sure to flush replay output log before early-exit - if( opts[options::replayLog] != NULL ) { - *opts[options::replayLog] << flush; + if( pExecutor->globals()->getReplayLog() != NULL ) { + *(pExecutor->globals()->getReplayLog()) << flush; } // make sure out and err streams are flushed too diff --git a/src/main/main.cpp b/src/main/main.cpp index 3f0842cc5..f8cb0677c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -24,7 +24,6 @@ #include "base/output.h" #include "expr/expr_manager.h" -#include "expr/result.h" #include "expr/statistics.h" #include "main/command_executor.h" #include "main/interactive_shell.h" @@ -37,6 +36,7 @@ #include "smt/smt_engine.h" #include "smt_util/command.h" #include "util/configuration.h" +#include "util/result.h" using namespace std; using namespace CVC4; diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 884c3eda7..ea7e3d458 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -20,11 +20,10 @@ #include <boost/exception_ptr.hpp> #include "base/output.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" - +#include "util/result.h" namespace CVC4 { diff --git a/src/options/options.h b/src/options/options.h index a83de9acb..8e1ca2b65 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -34,9 +34,6 @@ namespace options { class OptionsHandler; }/* CVC4::options namespace */ -// Forward declaration for smt_options -class ExprStream; - class CVC4_PUBLIC Options { /** The struct that holds all option values. */ options::OptionsHolder* d_holder; diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp index bce3643aa..2cf19a611 100644 --- a/src/options/options_handler_interface.cpp +++ b/src/options/options_handler_interface.cpp @@ -323,10 +323,6 @@ std::string checkReplayFilename(std::string option, std::string optarg, OptionsH return handler->checkReplayFilename(option, optarg); } -std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) { - PrettyCheckArgument(handler != NULL, handler, s_third_argument_warning); - return handler->checkReplayLogFilename(option, optarg); -} // ensure we are a stats-enabled build of CVC4 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { diff --git a/src/options/options_handler_interface.h b/src/options/options_handler_interface.h index 98575a313..e9e91ef0b 100644 --- a/src/options/options_handler_interface.h +++ b/src/options/options_handler_interface.h @@ -131,7 +131,6 @@ public: virtual void setRegularOutputChannel(std::string option, std::string optarg) = 0; virtual void setDiagnosticOutputChannel(std::string option, std::string optarg) = 0; virtual std::string checkReplayFilename(std::string option, std::string optarg) = 0; - virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg) = 0; virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException) = 0; virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; @@ -255,8 +254,6 @@ void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsH std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler); -std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler); - // ensure we are a stats-enabled build of CVC4 void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index ecf42ac58..231e5de90 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -14,8 +14,6 @@ ** Contains code for handling command-line options **/ -#warning "TODO: Remove ExprStream forward declaration from options.h." - #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) // force use of optreset; mingw32 croaks on argv-switching otherwise # include "cvc4autoconfig.h" diff --git a/src/options/smt_options b/src/options/smt_options index d531eefbe..b99a8a83b 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -148,15 +148,7 @@ expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-cons # --replay is currently broken; don't document it for 1.0 undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h" replay decisions from file -undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::options::checkReplayLogFilename :handler-include "options/options_handler_interface.h" - log decisions and propagations to file -option replayStream ExprStream* - -# portfolio options -option lemmaInputChannel LemmaInputChannel* :default NULL :include "base/lemma_input_channel_forward.h" - The input channel to receive notfication events for new lemmas -option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma_output_channel_forward.h" - The output channel to receive notfication events for new lemmas + option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false Force no CPU limit when dumping models and proofs diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index ffbc67cc4..b3666875d 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -45,21 +45,26 @@ using namespace CVC4::kind; namespace CVC4 { namespace prop { -CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : - d_satSolver(satSolver), - d_booleanVariables(context), - d_nodeToLiteralMap(context), - d_literalToNodeMap(context), - d_fullLitToNodeMap(fullLitToNodeMap), - d_convertAndAssertCounter(0), - d_registrar(registrar), - d_assertionTable(context), - d_removable(false) { +CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar, + context::Context* context, SmtGlobals* globals, + bool fullLitToNodeMap) + : d_satSolver(satSolver), + d_booleanVariables(context), + d_nodeToLiteralMap(context), + d_literalToNodeMap(context), + d_fullLitToNodeMap(fullLitToNodeMap), + d_convertAndAssertCounter(0), + d_registrar(registrar), + d_assertionTable(context), + d_globals(globals), + d_removable(false) { } -TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) : - CnfStream(satSolver, registrar, context, fullLitToNodeMap) { -} +TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, + context::Context* context, + SmtGlobals* globals, bool fullLitToNodeMap) + : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap) +{} void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) { Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl; @@ -184,7 +189,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister // If it's a theory literal, need to store it for back queries if ( isTheoryAtom || d_fullLitToNodeMap || - ( CVC4_USE_REPLAY && options::replayLog() != NULL ) || + ( CVC4_USE_REPLAY && d_globals->getReplayLog() != NULL ) || (Dump.isOn("clauses")) ) { d_literalToNodeMap.insert_safe(lit, node); diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d5d01d126..cfab216fe 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -25,14 +25,15 @@ #ifndef __CVC4__PROP__CNF_STREAM_H #define __CVC4__PROP__CNF_STREAM_H +#include <ext/hash_map> + +#include "context/cdinsert_hashmap.h" +#include "context/cdlist.h" #include "expr/node.h" -#include "prop/theory_proxy.h" -#include "prop/registrar.h" #include "proof/proof_manager.h" -#include "context/cdlist.h" -#include "context/cdinsert_hashmap.h" - -#include <ext/hash_map> +#include "prop/registrar.h" +#include "prop/theory_proxy.h" +#include "smt/smt_globals.h" namespace CVC4 { namespace prop { @@ -86,6 +87,9 @@ protected: /** A table of assertions, used for regenerating proofs. */ context::CDList<Node> d_assertionTable; + /** Container for misc. globals. */ + SmtGlobals* d_globals; + /** * How many literals were already mapped at the top-level when we * tried to convertAndAssert() something. This @@ -191,7 +195,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -291,7 +295,7 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); private: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2a1b05619..96ca7480f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,7 +25,6 @@ #include "decision/decision_engine.h" #include "expr/expr.h" #include "expr/resource_manager.h" -#include "expr/result.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -40,7 +39,7 @@ #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" - +#include "util/result.h" using namespace std; using namespace CVC4::context; @@ -68,7 +67,7 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) : d_inCheckSat(false), d_theoryEngine(te), d_decisionEngine(de), @@ -78,7 +77,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar(NULL), d_cnfStream(NULL), d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) { + d_resourceManager(NodeManager::currentResourceManager()), + d_globals(globals) +{ Debug("prop") << "Constructing the PropEngine" << endl; @@ -86,14 +87,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, d_registrar, - userContext, + (d_satSolver, d_registrar, userContext, d_globals, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); - d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream); + d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 57ff3c5c0..dfa84ef14 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -25,10 +25,11 @@ #include "base/modal_exception.h" #include "expr/node.h" -#include "expr/result.h" #include "options/options.h" #include "proof/proof_manager.h" +#include "smt/smt_globals.h" #include "util/unsafe_interrupt_exception.h" +#include "util/result.h" namespace CVC4 { @@ -91,12 +92,15 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); + /** Container for misc. globals. */ + SmtGlobals* d_globals; + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext); + PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext, SmtGlobals* global); /** * Destructor. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 386b12391..d0830b9a5 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -31,6 +31,43 @@ namespace CVC4 { namespace prop { +TheoryProxy::TheoryProxy(PropEngine* propEngine, + TheoryEngine* theoryEngine, + DecisionEngine* decisionEngine, + context::Context* context, + CnfStream* cnfStream, + SmtGlobals* globals) + : d_propEngine(propEngine), + d_cnfStream(cnfStream), + d_decisionEngine(decisionEngine), + d_theoryEngine(theoryEngine), + d_globals(globals), + d_queue(context) +{} + +TheoryProxy::~TheoryProxy() { + /* nothing to do for now */ +} + +/** The lemma input channel we are using. */ +LemmaInputChannel* TheoryProxy::inputChannel() { + return d_globals->getLemmaInputChannel(); +} + +/** The lemma output channel we are using. */ +LemmaOutputChannel* TheoryProxy::outputChannel() { + return d_globals->getLemmaOutputChannel(); +} + +std::ostream* TheoryProxy::replayLog() { + return d_globals->getReplayLog(); +} + +ExprStream* TheoryProxy::replayStream() { + return d_globals->getReplayStream(); +} + + void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -108,10 +145,10 @@ void TheoryProxy::notifyRestart() { static uint32_t lemmaCount = 0; - if(options::lemmaInputChannel() != NULL) { - while(options::lemmaInputChannel()->hasNewLemma()) { + if(inputChannel() != NULL) { + while(inputChannel()->hasNewLemma()) { Debug("shared") << "shared" << std::endl; - Expr lemma = options::lemmaInputChannel()->getNewLemma(); + Expr lemma = inputChannel()->getNewLemma(); Node asNode = lemma.getNode(); asNode = theory::Rewriter::rewrite(asNode); @@ -135,7 +172,7 @@ void TheoryProxy::notifyRestart() { void TheoryProxy::notifyNewLemma(SatClause& lemma) { Assert(lemma.size() > 0); - if(options::lemmaOutputChannel() != NULL) { + if(outputChannel() != NULL) { if(lemma.size() == 1) { // cannot share units yet //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); @@ -148,7 +185,7 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { if(d_shared.find(n) == d_shared.end()) { d_shared.insert(n); - options::lemmaOutputChannel()->notifyNewLemma(n.toExpr()); + outputChannel()->notifyNewLemma(n.toExpr()); } else { Debug("shared") <<"drop new " << n << std::endl; } @@ -158,8 +195,8 @@ void TheoryProxy::notifyNewLemma(SatClause& lemma) { SatLiteral TheoryProxy::getNextReplayDecision() { #ifdef CVC4_REPLAY - if(options::replayStream() != NULL) { - Expr e = options::replayStream()->nextExpr(); + if(replayStream() != NULL) { + Expr e = replayStream()->nextExpr(); if(!e.isNull()) { // we get null node when out of decisions to replay // convert & return ++d_replayedDecisions; @@ -172,9 +209,9 @@ SatLiteral TheoryProxy::getNextReplayDecision() { void TheoryProxy::logDecision(SatLiteral lit) { #ifdef CVC4_REPLAY - if(options::replayLog() != NULL) { + if(replayLog() != NULL) { Assert(lit != undefSatLiteral, "logging an `undef' decision ?!"); - *options::replayLog() << d_cnfStream->getNode(lit) << std::endl; + (*replayLog()) << d_cnfStream->getNode(lit) << std::endl; } #endif /* CVC4_REPLAY */ } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 413b4941d..59bc859cb 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,9 +23,15 @@ // Optional blocks below will be unconditionally included #define __CVC4_USE_MINISAT +#include <iosfwd> + #include "context/cdqueue.h" +#include "expr/node.h" #include "expr/statistics_registry.h" #include "prop/sat_solver.h" +#include "smt/smt_globals.h" +#include "smt_util/lemma_output_channel.h" +#include "smt_util/lemma_input_channel.h" #include "theory/theory.h" namespace CVC4 { @@ -42,40 +48,13 @@ class CnfStream; * The proxy class that allows the SatSolver to communicate with the theories */ class TheoryProxy { - - /** The prop engine we are using */ - PropEngine* d_propEngine; - - /** The CNF engine we are using */ - CnfStream* d_cnfStream; - - /** The decision engine we are using */ - DecisionEngine* d_decisionEngine; - - /** The theory engine we are using */ - TheoryEngine* d_theoryEngine; - - /** Queue of asserted facts */ - context::CDQueue<TNode> d_queue; - - /** - * Set of all lemmas that have been "shared" in the portfolio---i.e., - * all imported and exported lemmas. - */ - std::hash_set<Node, NodeHashFunction> d_shared; - - /** - * Statistic: the number of replayed decisions (via --replay). - */ - KEEP_STATISTIC(IntStat, d_replayedDecisions, - "prop::theoryproxy::replayedDecisions", 0); - public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream); + CnfStream* cnfStream, + SmtGlobals* globals); ~TheoryProxy(); @@ -117,25 +96,50 @@ public: SatValue getDecisionPolarity(SatVariable var); -};/* class SatSolver */ + private: + /** The prop engine we are using. */ + PropEngine* d_propEngine; -/* Functions that delegate to the concrete SAT solver. */ - -inline TheoryProxy::TheoryProxy(PropEngine* propEngine, - TheoryEngine* theoryEngine, - DecisionEngine* decisionEngine, - context::Context* context, - CnfStream* cnfStream) : - d_propEngine(propEngine), - d_cnfStream(cnfStream), - d_decisionEngine(decisionEngine), - d_theoryEngine(theoryEngine), - d_queue(context) -{} - -inline TheoryProxy::~TheoryProxy() { - /* nothing to do for now */ -} + /** The CNF engine we are using. */ + CnfStream* d_cnfStream; + + /** The decision engine we are using. */ + DecisionEngine* d_decisionEngine; + + /** The theory engine we are using. */ + TheoryEngine* d_theoryEngine; + + + /** + * Container for inputChannel, outputChannel, replayLog, and + * replayStream. + */ + SmtGlobals* d_globals; + + /** The lemma input channel we are using. */ + LemmaInputChannel* inputChannel(); + + /** The lemma output channel we are using. */ + LemmaOutputChannel* outputChannel(); + + std::ostream* replayLog(); + ExprStream* replayStream(); + + /** Queue of asserted facts */ + context::CDQueue<TNode> d_queue; + + /** + * Set of all lemmas that have been "shared" in the portfolio---i.e., + * all imported and exported lemmas. + */ + std::hash_set<Node, NodeHashFunction> d_shared; + + /** + * Statistic: the number of replayed decisions (via --replay). + */ + KEEP_STATISTIC(IntStat, d_replayedDecisions, + "prop::theoryproxy::replayedDecisions", 0); +};/* class SatSolver */ }/* CVC4::prop namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c1d49d8c8..3571ae0cb 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -724,7 +724,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_private(NULL), d_smtAttributes(NULL), d_statisticsRegistry(NULL), - d_stats(NULL) { + d_stats(NULL), + d_globals(new SmtGlobals()) +{ SmtScope smts(this); d_smtAttributes = new expr::attr::SmtAttributes(d_context); @@ -734,7 +736,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); + d_theoryEngine = new TheoryEngine(d_context, d_userContext, + d_private->d_iteRemover, + const_cast<const LogicInfo&>(d_logic), + d_globals); // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { @@ -764,7 +769,8 @@ void SmtEngine::finishInit() { d_decisionEngine = new DecisionEngine(d_context, d_userContext); d_decisionEngine->init(); // enable appropriate strategies - d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext); + d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, + d_userContext, d_globals); d_theoryEngine->setPropEngine(d_propEngine); d_theoryEngine->setDecisionEngine(d_decisionEngine); @@ -907,6 +913,9 @@ SmtEngine::~SmtEngine() throw() { delete d_context; d_context = NULL; + delete d_globals; + d_globals = NULL; + } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index c94646c40..3f049e392 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,15 +28,16 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/result.h" #include "expr/sexpr.h" #include "expr/statistics.h" #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" +#include "smt/smt_globals.h" #include "theory/logic_info.h" #include "util/hash.h" #include "util/proof.h" +#include "util/result.h" #include "util/unsafe_interrupt_exception.h" // In terms of abstraction, this is below (and provides services to) @@ -385,6 +386,8 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEngineStatistics* d_stats; + SmtGlobals* d_globals; + /** * Add to Model command. This is used for recording a command * that should be reported during a get-model call. @@ -729,6 +732,8 @@ public: * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized. */ static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException); + + SmtGlobals* globals() { return d_globals; } };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/smt/smt_globals.cpp b/src/smt/smt_globals.cpp new file mode 100644 index 000000000..4c1b0dc72 --- /dev/null +++ b/src/smt/smt_globals.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file smt_globals.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This class is a light container for globals that used to live + ** in options. This is NOT a good long term solution, but is a reasonable + ** stop gap. + ** + ** This class is a light container for globals that used to live + ** in options. This is NOT a good long term solution, but is a reasonable + ** stop gap. + **/ + +#include "smt/smt_globals.h" + +#include <cerrno> +#include <iostream> +#include <string> +#include <utility> + +#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY +#include "expr/expr_stream.h" +#include "options/option_exception.h" +#include "options/parser_options.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" +#include "smt/smt_options_handler.h" + +namespace CVC4 { + +SmtGlobals::SmtGlobals() + : d_gcReplayLog(false) + , d_replayLog(NULL) + , d_replayStream(NULL) + , d_lemmaInputChannel(NULL) + , d_lemmaOutputChannel(NULL) +{} + +SmtGlobals::~SmtGlobals(){ + if(d_gcReplayLog){ + delete d_replayLog; + d_gcReplayLog = false; + d_replayLog = NULL; + } +} + +void SmtGlobals::setReplayLog(std::ostream* log){ + d_replayLog = log; +} + +void SmtGlobals::setReplayStream(ExprStream* stream) { + d_replayStream = stream; +} + +void SmtGlobals::setLemmaInputChannel(LemmaInputChannel* in) { + d_lemmaInputChannel = in; +} + +void SmtGlobals::setLemmaOutputChannel(LemmaOutputChannel* out) { + d_lemmaOutputChannel = out; +} + +void SmtGlobals::parseReplayLog(std::string optarg) throw (OptionException) { + if(d_gcReplayLog){ + delete d_replayLog; + d_gcReplayLog = false; + d_replayLog = NULL; + } + + std::pair<bool, std::ostream*> checkResult = checkReplayLogFilename(optarg); + d_gcReplayLog = checkResult.first; + d_replayLog = checkResult.second; +} + +#warning "TODO: Move checkReplayLogFilename back into options and has calling setReplayLog as a side effect." +std::pair<bool, std::ostream*> SmtGlobals::checkReplayLogFilename(std::string optarg) + throw (OptionException) +{ +#ifdef CVC4_REPLAY + if(optarg == "") { + throw OptionException(std::string("Bad file name for --replay-log")); + } else if(optarg == "-") { + return std::make_pair(false, &std::cout); + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + std::ios_base::openmode out_trunc = std::ofstream::out | std::ofstream::trunc; + std::ostream* replayLog = new std::ofstream(optarg.c_str(), out_trunc); + if(replayLog == NULL || !*replayLog) { + std::stringstream ss; + ss << "Cannot open replay-log file: `" << optarg << "': " + << smt::SmtOptionsHandler::__cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + return std::make_pair(true, replayLog); + } +#else /* CVC4_REPLAY */ + throw OptionException("The replay feature was disabled in this build of CVC4."); +#endif /* CVC4_REPLAY */ +} + + +} /* namespace CVC4 */ diff --git a/src/smt/smt_globals.h b/src/smt/smt_globals.h new file mode 100644 index 000000000..00b90a703 --- /dev/null +++ b/src/smt/smt_globals.h @@ -0,0 +1,106 @@ +/********************* */ +/*! \file smt_globals.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SmtGlobals is a light container for psuedo-global datastructures + ** that are set by the user. + ** + ** SmtGlobals is a light container for psuedo-global datastructures + ** that are set by the user. These contain paramaters for infrequently + ** used modes: Portfolio and Replay. There should be exactly one of these + ** per SmtEngine with the same lifetime as the SmtEngine. + ** A user directly passes these as pointers and is resonsible for cleaning up + ** the memory. + ** + ** Basically, the problem this class is solving is that previously these were + ** using smt_options.h and the Options class as globals for these same + ** datastructures. + ** + ** This class is NOT a good long term solution, but is a reasonable stop gap. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__SMT_GLOBALS_H +#define __CVC4__SMT__SMT_GLOBALS_H + +#include <iosfwd> +#include <string> +#include <utility> + +#include "expr/expr_stream.h" +#include "options/option_exception.h" +#include "smt_util/lemma_input_channel.h" +#include "smt_util/lemma_output_channel.h" + +namespace CVC4 { + +/** + * SmtGlobals is a wrapper around 4 pointers: + * - getReplayLog() + * - getReplayStream() + * - getLemmaInputChannel() + * - getLemmaOutputChannel() + * + * The user can directly set these and is responsible for handling the + * memory for these. These datastructures are used for the Replay and Portfolio + * modes. + */ +class CVC4_PUBLIC SmtGlobals { + public: + /** Creates an empty SmtGlobals with all 4 pointers initially NULL. */ + SmtGlobals(); + ~SmtGlobals(); + + /** This setsReplayLog based on --replay-log */ + void parseReplayLog(std::string optarg) throw (OptionException); + void setReplayLog(std::ostream*); + std::ostream* getReplayLog() { return d_replayLog; } + + void setReplayStream(ExprStream* stream); + ExprStream* getReplayStream() { return d_replayStream; } + + void setLemmaInputChannel(LemmaInputChannel* in); + LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; } + + void setLemmaOutputChannel(LemmaOutputChannel* out); + LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; } + + private: + // Disable copy constructor. + SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED; + + // Disable assignment operator. + SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED; + + static std::pair<bool, std::ostream*> + checkReplayLogFilename(std::string optarg) throw (OptionException); + + /** + * d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog. + */ + bool d_gcReplayLog; + + /** This captures the old options::replayLog .*/ + std::ostream* d_replayLog; + + /** This captures the old options::replayStream .*/ + ExprStream* d_replayStream; + + /** This captures the old options::lemmaInputChannel .*/ + LemmaInputChannel* d_lemmaInputChannel; + + /** This captures the old options::lemmaOutputChannel .*/ + LemmaOutputChannel* d_lemmaOutputChannel; +}; /* class SmtGlobals */ + +} /* namespace CVC4 */ + +#endif /* __CVC4__SMT__SMT_GLOBALS_H */ diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp index e1a19d48b..147a53368 100644 --- a/src/smt/smt_options_handler.cpp +++ b/src/smt/smt_options_handler.cpp @@ -1308,7 +1308,7 @@ void SmtOptionsHandler::setDiagnosticOutputChannel(std::string option, std::stri std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) { #ifdef CVC4_REPLAY if(optarg == "") { - throw OptionException(std::string("Bad file name for --replay")); + throw OptionException (std::string("Bad file name for --replay")); } else { return optarg; } @@ -1317,28 +1317,6 @@ std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::stri #endif /* CVC4_REPLAY */ } -std::ostream* SmtOptionsHandler::checkReplayLogFilename(std::string option, std::string optarg) { -#ifdef CVC4_REPLAY - if(optarg == "") { - throw OptionException(std::string("Bad file name for --replay-log")); - } else if(optarg == "-") { - return &std::cout; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(replayLog == NULL || !*replayLog) { - std::stringstream ss; - ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - return replayLog; - } -#else /* CVC4_REPLAY */ - throw OptionException("The replay feature was disabled in this build of CVC4."); -#endif /* CVC4_REPLAY */ -} void SmtOptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) { #ifndef CVC4_STATISTICS_ON diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h index c4d27a722..f8e2ac155 100644 --- a/src/smt/smt_options_handler.h +++ b/src/smt/smt_options_handler.h @@ -124,7 +124,6 @@ public: virtual void setRegularOutputChannel(std::string option, std::string optarg); virtual void setDiagnosticOutputChannel(std::string option, std::string optarg); virtual std::string checkReplayFilename(std::string option, std::string optarg); - virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg); virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException); virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException); virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException); @@ -152,13 +151,14 @@ public: virtual void addDebugTag(std::string option, std::string optarg); virtual void setPrintSuccess(std::string option, bool value); + static std::string __cvc4_errno_failreason(); + private: SmtEngine* d_smtEngine; /* Helper utilities */ static std::string suggestTags(char const* const* validTags, std::string inputTag, char const* const* additionalTags = NULL); - static std::string __cvc4_errno_failreason(); /* Help strings */ static const std::string s_bitblastingModeHelp; diff --git a/src/smt_util/command.h b/src/smt_util/command.h index 17d65beb2..c9b968722 100644 --- a/src/smt_util/command.h +++ b/src/smt_util/command.h @@ -30,12 +30,12 @@ #include "expr/datatype.h" #include "expr/expr.h" -#include "expr/result.h" #include "expr/sexpr.h" #include "expr/type.h" #include "expr/variable_type_map.h" #include "proof/unsat_core.h" #include "util/proof.h" +#include "util/result.h" namespace CVC4 { diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h index 66fe06424..44f0b87f5 100644 --- a/src/smt_util/lemma_input_channel.h +++ b/src/smt_util/lemma_input_channel.h @@ -20,7 +20,6 @@ #ifndef __CVC4__LEMMA_INPUT_CHANNEL_H #define __CVC4__LEMMA_INPUT_CHANNEL_H -#include "base/lemma_input_channel_forward.h" #include "expr/expr.h" namespace CVC4 { diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h index 0fabe5721..df7abd1e9 100644 --- a/src/smt_util/lemma_output_channel.h +++ b/src/smt_util/lemma_output_channel.h @@ -21,7 +21,6 @@ #ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_H #define __CVC4__LEMMA_OUTPUT_CHANNEL_H -#include "base/lemma_output_channel_forward.h" #include "expr/expr.h" namespace CVC4 { diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index f39006788..1cd617b64 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,7 +53,6 @@ #pragma once -#include "expr/result.h" #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" #include "theory/arith/error_set.h" @@ -61,6 +60,7 @@ #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" #include "util/dense_map.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1e3b21b17..3c5c1c414 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -28,9 +28,11 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) +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) + , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) {} TheoryArith::~TheoryArith(){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index a0a8e2c89..d26a120ae 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -46,7 +46,9 @@ private: KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); virtual ~TheoryArith(); /** diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ab800f10d..bf1810331 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -33,7 +33,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -70,6 +69,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 0c2a704e8..32c12eba7 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -31,7 +31,6 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/result.h" #include "expr/statistics_registry.h" #include "options/arith_options.h" #include "smt/logic_exception.h" @@ -67,6 +66,7 @@ #include "util/dense_map.h" #include "util/integer.h" #include "util/rational.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 2863fad8a..ab57eb260 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -51,50 +51,52 @@ const bool d_solveWrite2 = false; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo), - d_numRow("theory::arrays::number of Row lemmas", 0), - d_numExt("theory::arrays::number of Ext lemmas", 0), - d_numProp("theory::arrays::number of propagations", 0), - d_numExplain("theory::arrays::number of explanations", 0), - d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), - d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), - d_ppFacts(u), - // d_ppCache(u), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), - d_notify(*this), - d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), - d_conflict(c, false), - d_backtracker(c), - d_infoMap(c, &d_backtracker), - d_mergeQueue(c), - d_mergeInProgress(false), - d_RowQueue(c), - d_RowAlreadyAdded(u), - d_sharedArrays(c), - d_sharedOther(c), - d_sharedTerms(c, false), - d_reads(c), - d_constReadsList(c), - d_constReadsContext(new context::Context()), - d_contextPopper(c, d_constReadsContext), - d_skolemIndex(c, 0), - d_decisionRequests(c), - d_permRef(c), - d_modelConstraints(c), - d_lemmasSaved(c), - d_defValues(c), - d_readTableContext(new context::Context()), - d_arrayMerges(c), - d_inCheckModel(false) +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals), + d_numRow("theory::arrays::number of Row lemmas", 0), + d_numExt("theory::arrays::number of Ext lemmas", 0), + d_numProp("theory::arrays::number of propagations", 0), + d_numExplain("theory::arrays::number of explanations", 0), + d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0), + d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0), + d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0), + d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0), + d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0), + d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0), + d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true), + d_ppFacts(u), + // d_ppCache(u), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_isPreRegistered(c), + d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true), + d_notify(*this), + d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true), + d_conflict(c, false), + d_backtracker(c), + d_infoMap(c, &d_backtracker), + d_mergeQueue(c), + d_mergeInProgress(false), + d_RowQueue(c), + d_RowAlreadyAdded(u), + d_sharedArrays(c), + d_sharedOther(c), + d_sharedTerms(c, false), + d_reads(c), + d_constReadsList(c), + d_constReadsContext(new context::Context()), + d_contextPopper(c, d_constReadsContext), + d_skolemIndex(c, 0), + d_decisionRequests(c), + d_permRef(c), + d_modelConstraints(c), + d_lemmasSaved(c), + d_defValues(c), + d_readTableContext(new context::Context()), + d_arrayMerges(c), + d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); StatisticsRegistry::registerStat(&d_numExt); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 28d994835..98cba0420 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -126,7 +126,9 @@ class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index a4a3757cd..246f1e7e8 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -28,9 +28,11 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) { - } + 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) + {} PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index fa6e8ab5c..2fbc0e402 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -27,8 +27,10 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} + 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) {} 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 b93d0561e..7b071b9e9 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -19,17 +19,17 @@ #ifndef __CVC4__BITBLASTER_TEMPLATE_H #define __CVC4__BITBLASTER_TEMPLATE_H - -#include "expr/node.h" -#include <vector> #include <ext/hash_map> +#include <vector> -#include "context/cdhashmap.h" #include "bitblast_strategies_template.h" +#include "context/cdhashmap.h" +#include "expr/node.h" #include "expr/resource_manager.h" #include "prop/sat_solver.h" -#include "theory/valuation.h" +#include "smt/smt_globals.h" #include "theory/theory_registrar.h" +#include "theory/valuation.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -84,25 +84,25 @@ protected: // caches and mappings TermDefMap d_termCache; ModelCache d_modelCache; - + void initAtomBBStrategies(); void initTermBBStrategies(); protected: /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; - AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; - virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; public: - TBitblaster(); + TBitblaster(); virtual ~TBitblaster() {} - virtual void bbAtom(TNode node) = 0; + virtual void bbAtom(TNode node) = 0; virtual void bbTerm(TNode node, Bits& bits) = 0; virtual void makeVariable(TNode node, Bits& bits) = 0; virtual T getBBAtom(TNode atom) const = 0; virtual bool hasBBAtom(TNode atom) const = 0; virtual void storeBBAtom(TNode atom, T atom_bb) = 0; - - + + bool hasBBTerm(TNode node) const; void getBBTerm(TNode node, Bits& bits) const; void storeBBTerm(TNode term, const Bits& bits); @@ -114,10 +114,10 @@ public: */ Node getTermModel(TNode node, bool fullModel); void invalidateModelCache(); -}; +}; -class TheoryBV; +class TheoryBV; class TLazyBitblaster : public TBitblaster<Node> { typedef std::vector<Node> Bits; @@ -127,19 +127,20 @@ class TLazyBitblaster : public TBitblaster<Node> { class MinisatNotify : public prop::BVSatSolverInterface::Notify { prop::CnfStream* d_cnf; TheoryBV *d_bv; - TLazyBitblaster* d_lazyBB; + TLazyBitblaster* d_lazyBB; public: MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv, TLazyBitblaster* lbv) : d_cnf(cnf) , d_bv(bv) , d_lazyBB(lbv) {} + bool notify(prop::SatLiteral lit); void notify(prop::SatClause& clause); void spendResource(unsigned ammount); void safePoint(unsigned ammount); }; - + TheoryBV *d_bv; context::Context* d_ctx; @@ -155,24 +156,25 @@ class TLazyBitblaster : public TBitblaster<Node> { ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. Only used when bvEagerPropagate option enabled. */ TNodeSet d_variables; - TNodeSet d_bbAtoms; + TNodeSet d_bbAtoms; AbstractionModule* d_abstraction; bool d_emptyNotify; context::CDO<bool> d_satSolverFullModel; - + void addAtom(TNode atom); bool hasValue(TNode a); - Node getModelFromSatSolver(TNode a, bool fullModel); + Node getModelFromSatSolver(TNode a, bool fullModel); + public: void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); Node getBBAtom(TNode atom) const; void storeBBAtom(TNode atom, Node atom_bb); - bool hasBBAtom(TNode atom) const; + bool hasBBAtom(TNode atom) const; TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false); ~TLazyBitblaster() throw(); - /** + /** * Pushes the assumption literal associated with node to the SAT * solver assumption queue. * @@ -261,26 +263,27 @@ class EagerBitblaster : public TBitblaster<Node> { TNodeSet d_variables; Node getModelFromSatSolver(TNode a, bool fullModel); - bool isSharedTerm(TNode node); + bool isSharedTerm(TNode node); public: + EagerBitblaster(theory::bv::TheoryBV* theory_bv); + ~EagerBitblaster(); + void addAtom(TNode atom); void makeVariable(TNode node, Bits& bits); void bbTerm(TNode node, Bits& bits); void bbAtom(TNode node); Node getBBAtom(TNode node) const; - bool hasBBAtom(TNode atom) const; + bool hasBBAtom(TNode atom) const; void bbFormula(TNode formula); void storeBBAtom(TNode atom, Node atom_bb); - EagerBitblaster(theory::bv::TheoryBV* theory_bv); - ~EagerBitblaster(); bool assertToSat(TNode node, bool propagate = true); bool solve(); void collectModelInfo(TheoryModel* m, bool fullModel); }; class BitblastingRegistrar: public prop::Registrar { - EagerBitblaster* d_bitblaster; + EagerBitblaster* d_bitblaster; public: BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 37e1bd9ba..ff13867cc 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -33,15 +33,16 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AssertionSet; AssertionSet d_assertionSet; /** Bitblasters */ EagerBitblaster* d_bitblaster; AigBitblaster* d_aigBitblaster; bool d_useAig; - TheoryBV* d_bv; + TheoryBV* d_bv; + public: - EagerBitblastSolver(theory::bv::TheoryBV* bv); + EagerBitblastSolver(theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 261a0b1c4..8ef49f786 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -35,7 +35,7 @@ class TheoryModel; namespace bv { -class TLazyBitblaster; +class TLazyBitblaster; class TheoryBV; class BVQuickCheck { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 77461163c..0e066eefb 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -18,8 +18,8 @@ #pragma once -#include "theory/bv/bv_subtheory.h" #include "theory/bv/bitblaster_template.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { @@ -58,7 +58,7 @@ class BitblastSolver : public SubtheorySolver { BVQuickCheck* d_quickCheck; QuickXPlain* d_quickXplain; // Node getModelValueRec(TNode node); - void setConflict(TNode conflict); + void setConflict(TNode conflict); public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index ec2bfd9c0..39606ca7c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -46,7 +46,8 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) d_nullContext = new context::Context(); d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, + d_nullContext, d_bv->globals()); MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 3c2b4ed78..b8173cb8b 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -26,12 +26,13 @@ #include "theory/theory_model.h" #include "theory_bv_utils.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; +namespace CVC4 { +namespace theory { +namespace bv { -TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify) +TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, + const std::string name, bool emptyNotify) : TBitblaster<Node>() , d_bv(bv) , d_ctx(c) @@ -44,13 +45,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st , d_satSolverFullModel(c, false) , d_name(name) , d_statistics(name) { + d_satSolver = prop::SatSolverFactory::createMinisat(c, name); d_nullRegistrar = new prop::NullRegistrar(); d_nullContext = new context::Context(); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext); - + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, + d_nullContext, d_bv->globals()); + d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this); @@ -59,7 +60,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st } void TLazyBitblaster::setAbstraction(AbstractionModule* abs) { - d_abstraction = abs; + d_abstraction = abs; } TLazyBitblaster::~TLazyBitblaster() throw() { @@ -103,8 +104,8 @@ void TLazyBitblaster::bbAtom(TNode node) { if (expansion.getKind() == kind::CONST_BOOLEAN) { atom_bb = expansion; } else { - Assert (expansion.getKind() == kind::AND); - std::vector<Node> atoms; + Assert (expansion.getKind() == kind::AND); + std::vector<Node> atoms; for (unsigned i = 0; i < expansion.getNumChildren(); ++i) { Node normalized_i = Rewriter::rewrite(expansion[i]); Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ? @@ -481,7 +482,7 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { } void TLazyBitblaster::clearSolver() { - Assert (d_ctx->getLevel() == 0); + Assert (d_ctx->getLevel() == 0); delete d_satSolver; delete d_satSolverNotify; delete d_cnfStream; @@ -492,16 +493,19 @@ void TLazyBitblaster::clearSolver() { d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); - - invalidateModelCache(); + + invalidateModelCache(); // recreate sat solver d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); - d_cnfStream = new prop::TseitinCnfStream(d_satSolver, - d_nullRegistrar, - d_nullContext); + d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar, + d_nullContext, d_bv->globals()); d_satSolverNotify = d_emptyNotify ? (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() : (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); d_satSolver->setNotify(d_satSolverNotify); } + +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4039fceec..0505035c7 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -31,38 +31,40 @@ #include "theory/theory_model.h" #include "theory/valuation.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; using namespace CVC4::context; - -using namespace std; using namespace CVC4::theory::bv::utils; +using namespace std; -TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo), - d_context(c), - d_alreadyPropagatedSet(c), - d_sharedTermsSet(c), - d_subtheories(), - d_subtheoryMap(), - d_statistics(), - d_staticLearnCache(), - d_lemmasAdded(c, false), - d_conflict(c, false), - d_invalidateModelCache(c, true), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_propagatedBy(c), - d_eagerSolver(NULL), - d_abstractionModule(new AbstractionModule()), - d_isCoreTheory(false), - d_calledPreregister(false) +namespace CVC4 { +namespace theory { +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), + d_context(c), + d_alreadyPropagatedSet(c), + d_sharedTermsSet(c), + d_subtheories(), + d_subtheoryMap(), + d_statistics(), + d_staticLearnCache(), + d_lemmasAdded(c, false), + d_conflict(c, false), + d_invalidateModelCache(c, true), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_propagatedBy(c), + d_eagerSolver(NULL), + d_abstractionModule(new AbstractionModule()), + d_isCoreTheory(false), + d_calledPreregister(false) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { d_eagerSolver = new EagerBitblastSolver(this); - return; + return; } if (options::bitvectorEqualitySolver()) { @@ -70,7 +72,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories.push_back(core_solver); d_subtheoryMap[SUB_CORE] = core_solver; } - + if (options::bitvectorInequalitySolver()) { SubtheorySolver* ineq_solver = new InequalitySolver(c, this); d_subtheories.push_back(ineq_solver); @@ -101,7 +103,7 @@ TheoryBV::~TheoryBV() { void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - return; + return; } if (options::bitvectorEqualitySolver()) { dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq); @@ -179,31 +181,31 @@ void TheoryBV::collectNumerators(TNode term, TNodeSet& seen) { d_BVDivByZeroAckerman[size] = TNodeSet(); } d_BVDivByZeroAckerman[size].insert(term[0]); - seen.insert(term); + seen.insert(term); } else if (term.getKind() == kind::BITVECTOR_ACKERMANIZE_UREM) { unsigned size = utils::getSize(term[0]); if (d_BVRemByZeroAckerman.find(size) == d_BVRemByZeroAckerman.end()) { d_BVRemByZeroAckerman[size] = TNodeSet(); } d_BVRemByZeroAckerman[size].insert(term[0]); - seen.insert(term); + seen.insert(term); } for (unsigned i = 0; i < term.getNumChildren(); ++i) { - collectNumerators(term[i], seen); + collectNumerators(term[i], seen); } - seen.insert(term); + seen.insert(term); } void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n"; - + Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); - TNodeSet seen; + TNodeSet seen; for (unsigned i = 0; i < assertions.size(); ++i) { - collectNumerators(assertions[i], seen); + collectNumerators(assertions[i], seen); } - + // process division UF Debug("bv-ackermanize") << "Process division UF...\n"; for (WidthToNumerators::const_iterator it = d_BVDivByZeroAckerman.begin(); it != d_BVDivByZeroAckerman.end(); ++it) { @@ -215,13 +217,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { TNode arg1 = *i; TNode arg2 = *j; TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); + TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UDIV, arg2); Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); Debug("bv-ackermanize") << " " << lemma << "\n"; - assertions.push_back(lemma); + assertions.push_back(lemma); } } } @@ -236,13 +238,13 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) { TNode arg1 = *i; TNode arg2 = *j; TNode acker1 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg1); - TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); + TNode acker2 = utils::mkNode(kind::BITVECTOR_ACKERMANIZE_UREM, arg2); Node arg_eq = utils::mkNode(kind::EQUAL, arg1, arg2); Node acker_eq = utils::mkNode(kind::EQUAL, acker1, acker2); Node lemma = utils::mkNode(kind::IMPLIES, arg_eq, acker_eq); Debug("bv-ackermanize") << " " << lemma << "\n"; - assertions.push_back(lemma); + assertions.push_back(lemma); } } } @@ -265,7 +267,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { if (options::bitvectorDivByZeroConst()) { Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL; - return nm->mkNode(kind, node[0], node[1]); + return nm->mkNode(kind, node[0], node[1]); } TNode num = node[0], den = node[1]; @@ -275,9 +277,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // Ackermanize UF if using eager bit-blasting - Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); + Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen); - return node; + return node; } else { Node divByZero = getBVDivByZero(node.getKind(), width); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); @@ -300,7 +302,7 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) { void TheoryBV::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // the aig bit-blaster option is set heuristically // if bv abstraction is not used @@ -309,13 +311,13 @@ void TheoryBV::preRegisterTerm(TNode node) { } if (node.getKind() == kind::BITVECTOR_EAGER_ATOM) { - Node formula = node[0]; + Node formula = node[0]; d_eagerSolver->assertFormula(formula); } // nothing to do for the other terms - return; + return; } - + for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->preRegister(node); } @@ -370,7 +372,7 @@ void TheoryBV::check(Effort e) Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound - d_invalidateModelCache.set(true); + d_invalidateModelCache.set(true); // if we are using the eager solver if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { // this can only happen on an empty benchmark @@ -380,28 +382,28 @@ void TheoryBV::check(Effort e) if (!Theory::fullEffort(e)) return; - std::vector<TNode> assertions; + std::vector<TNode> assertions; while (!done()) { TNode fact = get().assertion; Assert (fact.getKind() == kind::BITVECTOR_EAGER_ATOM); - assertions.push_back(fact); + assertions.push_back(fact); } - Assert (d_eagerSolver->hasAssertions(assertions)); - + Assert (d_eagerSolver->hasAssertions(assertions)); + bool ok = d_eagerSolver->checkSat(); if (!ok) { if (assertions.size() == 1) { d_out->conflict(assertions[0]); - return; + return; } Node conflict = NodeManager::currentNM()->mkNode(kind::AND, assertions); d_out->conflict(conflict); - return; + return; } return; } - - + + if (Theory::fullEffort(e)) { ++(d_statistics.d_numCallsToCheckFullEffort); } else { @@ -446,7 +448,7 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver->collectModelInfo(m, fullModel); + d_eagerSolver->collectModelInfo(m, fullModel); } for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { @@ -469,7 +471,7 @@ Node TheoryBV::getModelValue(TNode var) { void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - return; + return; } if (inConflict()) { @@ -508,29 +510,29 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } - Node node = Rewriter::rewrite(in); + Node node = Rewriter::rewrite(in); if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst()) || (node[1].getKind() == kind::BITVECTOR_EXTRACT && node[0].isConst())) { Node extract = node[0].isConst() ? node[1] : node[0]; if (extract[0].getKind() == kind::VARIABLE) { Node c = node[0].isConst() ? node[0] : node[1]; - + unsigned high = utils::getExtractHigh(extract); unsigned low = utils::getExtractLow(extract); unsigned var_bitwidth = utils::getSize(extract[0]); std::vector<Node> children; - + if (low == 0) { Assert (high != var_bitwidth - 1); unsigned skolem_size = var_bitwidth - high - 1; Node skolem = utils::mkVar(skolem_size); - children.push_back(skolem); + children.push_back(skolem); children.push_back(c); } else if (high == var_bitwidth - 1) { unsigned skolem_size = low; Node skolem = utils::mkVar(skolem_size); children.push_back(c); - children.push_back(skolem); + children.push_back(skolem); } else { unsigned skolem1_size = low; unsigned skolem2_size = var_bitwidth - high - 1; @@ -541,7 +543,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu children.push_back(skolem1); } Node concat = utils::mkNode(kind::BITVECTOR_CONCAT, children); - Assert (utils::getSize(concat) == utils::getSize(extract[0])); + Assert (utils::getSize(concat) == utils::getSize(extract[0])); outSubstitutions.addSubstitution(extract[0], concat); return PP_ASSERT_STATUS_SOLVED; } @@ -552,7 +554,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu case kind::BITVECTOR_SLT: case kind::BITVECTOR_ULE: case kind::BITVECTOR_SLE: - + default: // TODO other predicates break; @@ -562,7 +564,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu Node TheoryBV::ppRewrite(TNode t) { - Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; + Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; if (RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); @@ -591,8 +593,8 @@ Node TheoryBV::ppRewrite(TNode t) } else { res = t; } - } - + } + // if(t.getKind() == kind::EQUAL && // ((t[0].getKind() == kind::BITVECTOR_MULT && t[1].getKind() == kind::BITVECTOR_PLUS) || @@ -618,18 +620,18 @@ Node TheoryBV::ppRewrite(TNode t) // return new_eq; // } // } - + // if (new_eq.getKind() == kind::CONST_BOOLEAN) { // ++(d_statistics.d_numMultSlice); // return new_eq; // } // } // } - + if (options::bvAbstraction() && t.getType().isBoolean()) { - d_abstractionModule->addInputAtom(res); + d_abstractionModule->addInputAtom(res); } - Debug("bv-pp-rewrite") << "to " << res << "\n"; + Debug("bv-pp-rewrite") << "to " << res << "\n"; return res; } @@ -637,13 +639,13 @@ void TheoryBV::presolve() { Debug("bitvector") << "TheoryBV::presolve" << endl; } -static int prop_count = 0; +static int prop_count = 0; bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { Debug("bitvector::propagate") << indent() << getSatContext()->getLevel() << " " << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl; - prop_count++; - + prop_count++; + // If already in conflict, no more propagation if (d_conflict) { Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl; @@ -720,7 +722,7 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); if (status != EQUALITY_UNKNOWN) { @@ -736,7 +738,7 @@ void TheoryBV::enableCoreTheorySlicer() { d_isCoreTheory = true; if (d_subtheoryMap.find(SUB_CORE) != d_subtheoryMap.end()) { CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - core->enableSlicer(); + core->enableSlicer(); } } @@ -746,7 +748,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { return; } d_staticLearnCache.insert(in); - + if (in.getKind() == kind::EQUAL) { if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) || (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) { @@ -754,7 +756,7 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0]; if(p.getNumChildren() == 2 - && p[0].getKind() == kind::BITVECTOR_SHL + && p[0].getKind() == kind::BITVECTOR_SHL && p[1].getKind() == kind::BITVECTOR_SHL ){ unsigned size = utils::getSize(s); Node one = utils::mkConst(size, 1u); @@ -796,14 +798,18 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector void TheoryBV::setConflict(Node conflict) { if (options::bvAbstraction()) { Node new_conflict = d_abstractionModule->simplifyConflict(conflict); - + std::vector<Node> lemmas; - lemmas.push_back(new_conflict); + lemmas.push_back(new_conflict); d_abstractionModule->generalizeConflict(new_conflict, lemmas); for (unsigned i = 0; i < lemmas.size(); ++i) { - lemma(utils::mkNode(kind::NOT, lemmas[i])); + lemma(utils::mkNode(kind::NOT, lemmas[i])); } } d_conflict = true; d_conflictNode = conflict; } + +} /* namespace CVC4::theory::bv */ +} /* namespace CVC4::theory */ +} /* namespace CVC4 */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 4b3649a86..8ded63c28 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,6 +23,7 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/statistics_registry.h" +#include "smt/smt_globals.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" @@ -35,10 +36,10 @@ namespace bv { class CoreSolver; class InequalitySolver; class AlgebraicSolver; -class BitblastSolver; +class BitblastSolver; class EagerBitblastSolver; - + class AbstractionModule; class TheoryBV : public Theory { @@ -49,14 +50,14 @@ class TheoryBV : public Theory { /** Context dependent set of atoms we already propagated */ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet; - - std::vector<SubtheorySolver*> d_subtheories; - __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; + std::vector<SubtheorySolver*> d_subtheories; + __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals); + ~TheoryBV(); void setMasterEqualityEngine(eq::EqualityEngine* eq); @@ -80,13 +81,14 @@ public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); void enableCoreTheorySlicer(); - + Node ppRewrite(TNode t); void ppStaticLearn(TNode in, NodeBuilder<>& learned); - + void presolve(); - bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + private: class Statistics { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3d70e9a9a..9ba20fcc9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -31,32 +31,34 @@ #include "theory/type_enumerator.h" #include "theory/valuation.h" - using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::datatypes; - - -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), - //d_cycle_check(c), - d_hasSeenCycle(c, false), - d_infer(c), - d_infer_exp(c), - d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true), - d_labels( c ), - d_selector_apps( c ), - //d_consEqc( c ), - d_conflict( c, false ), - d_collectTermsCache( c ), - d_consTerms( c ), - d_selTerms( c ), - d_singleton_eq( u ){ +namespace CVC4 { +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), + //d_cycle_check(c), + d_hasSeenCycle(c, false), + d_infer(c), + d_infer_exp(c), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true), + d_labels( c ), + d_selector_apps( c ), + //d_consEqc( c ), + d_conflict( c, false ), + d_collectTermsCache( c ), + d_consTerms( c ), + d_selTerms( c ), + d_singleton_eq( u ) +{ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); @@ -2044,3 +2046,7 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& } return false; } + +} /* namepsace CVC4::theory::datatypes */ +} /* namepsace CVC4::theory */ +} /* namepsace CVC4 */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index bbbf799bd..fc6e435cc 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -180,31 +180,40 @@ private: /** sygus utilities */ SygusSplit * d_sygus_split; SygusSymBreak * d_sygus_sym_break; + private: /** singleton lemmas (for degenerate co-datatype case) */ std::map< TypeNode, Node > d_singleton_lemma[2]; + /** Cache for singleton equalities processed */ BoolMap d_singleton_eq; -private: + /** assert fact */ void assertFact( Node fact, Node exp ); + /** flush pending facts */ void flushPendingFacts(); + /** do pending merged */ void doPendingMerges(); + /** get or make eqc info */ EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); + /** has eqc info */ bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); } + /** get eqc constructor */ TNode getEqcConstructor( TNode r ); + protected: /** compute care graph */ void computeCareGraph(); + public: TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo); + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryDatatypes(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 6400fec38..9a8d77844 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -51,13 +51,11 @@ 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) : - Theory(THEORY_FP, c, u, out, valuation, logicInfo) { -}/* TheoryFp::TheoryFp() */ +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) +{}/* TheoryFp::TheoryFp() */ Node TheoryFp::expandDefinition(LogicRequest &, Node node) { diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 6fb41685f..fe3c377af 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -14,10 +14,11 @@ public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo); + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + SmtGlobals* globals); Node expandDefinition(LogicRequest &, Node node); diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 427ac577c..8cba51c8f 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -26,15 +26,16 @@ using namespace std; -using namespace CVC4; -using namespace theory; -using namespace idl; - -TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo) -: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) -, d_model(c) -, d_assertionsDB(c) +namespace CVC4 { +namespace theory { +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) + , d_model(c) + , d_assertionsDB(c) {} Node TheoryIdl::ppRewrite(TNode atom) { @@ -148,3 +149,7 @@ bool TheoryIdl::processAssertion(const IDLAssertion& assertion) { // Everything fine, no conflict return true; } + +} /* namepsace CVC4::theory::idl */ +} /* namepsace CVC4::theory */ +} /* namepsace CVC4 */ diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 7c879e722..aa7267eb7 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -45,7 +45,8 @@ public: /** Theory constructor. */ TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom); diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 60d0e1d48..2113ea66e 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -86,8 +86,9 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) { - } + virtual void safePoint(uint64_t amount) + throw(Interrupted, UnsafeInterruptException, AssertionException) + {} /** * Indicate a theory conflict has arisen. diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e9ff60137..b808f4cd5 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) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), +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), d_masterEqualityEngine(0) { d_numInstantiations = 0; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 98f486145..f24c10fc0 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -46,10 +46,14 @@ private: int d_baseDecLevel; eq::EqualityEngine* d_masterEqualityEngine; + private: - void computeCareGraph(); + void computeCareGraph(); + public: - TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryQuantifiers(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index db93c597c..82ebb5bf8 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -25,10 +25,11 @@ TheorySets::TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) : - Theory(THEORY_SETS, c, u, out, valuation, logicInfo), - d_internal(new TheorySetsPrivate(*this, c, u)) { -} + const LogicInfo& logicInfo, + SmtGlobals* globals) + : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, globals), + d_internal(new TheorySetsPrivate(*this, c, u)) +{} TheorySets::~TheorySets() { delete d_internal; diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 6136fc8f8..7ff8abec6 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -40,11 +40,9 @@ public: * Constructs a new instance of TheorySets w.r.t. the provided * contexts. */ - TheorySets(context::Context* c, - context::UserContext* u, - OutputChannel& out, - Valuation valuation, - const LogicInfo& logicInfo); + TheorySets(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheorySets(); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f200397bc..0c3171065 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -19,12 +19,12 @@ #include <boost/foreach.hpp> #include "expr/emptyset.h" -#include "expr/result.h" #include "options/sets_options.h" #include "theory/sets/expr_patterns.h" // ONLY included here #include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" #include "theory/theory_model.h" +#include "util/result.h" using namespace std; using namespace CVC4::expr::pattern; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index dfd3c4803..b68687d54 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -55,42 +55,44 @@ 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) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), - RMAXINT(LONG_MAX), - d_notify( *this ), - d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true), - d_conflict(c, false), - d_infer(c), - d_infer_exp(c), - d_nf_pairs(c), - d_loop_antec(u), - d_length_intro_vars(u), - d_pregistered_terms_cache(u), - d_registered_terms_cache(u), - d_preproc(u), - d_preproc_cache(u), - d_extf_infer_cache(c), - d_congruent(c), - d_proxy_var(u), - d_proxy_var_to_length(u), - d_neg_ctn_eqlen(c), - d_neg_ctn_ulen(c), - d_neg_ctn_cached(u), - d_ext_func_terms(c), - d_regexp_memberships(c), - d_regexp_ucached(u), - d_regexp_ccached(c), - d_pos_memberships(c), - d_neg_memberships(c), - d_inter_cache(c), - d_inter_index(c), - d_processed_memberships(c), - d_regexp_ant(c), - d_input_vars(u), - d_input_var_lsum(u), - d_cardinality_lits(u), - d_curr_cardinality(c, 0) +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), + RMAXINT(LONG_MAX), + d_notify( *this ), + d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true), + d_conflict(c, false), + d_infer(c), + d_infer_exp(c), + d_nf_pairs(c), + d_loop_antec(u), + d_length_intro_vars(u), + d_pregistered_terms_cache(u), + d_registered_terms_cache(u), + d_preproc(u), + d_preproc_cache(u), + d_extf_infer_cache(c), + d_congruent(c), + d_proxy_var(u), + d_proxy_var_to_length(u), + d_neg_ctn_eqlen(c), + d_neg_ctn_ulen(c), + d_neg_ctn_cached(u), + d_ext_func_terms(c), + d_regexp_memberships(c), + d_regexp_ucached(u), + d_regexp_ccached(c), + d_pos_memberships(c), + d_neg_memberships(c), + d_inter_cache(c), + d_inter_index(c), + d_processed_memberships(c), + d_regexp_ant(c), + d_input_vars(u), + d_input_var_lsum(u), + d_cardinality_lits(u), + d_curr_cardinality(c, 0) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 40358649b..ddb800ee1 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -52,7 +52,9 @@ class TheoryStrings : public Theory { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); + TheoryStrings(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals); ~TheoryStrings(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/theory.h b/src/theory/theory.h index 5f4c80cf2..d17d97f97 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -34,6 +34,7 @@ #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" @@ -245,7 +246,8 @@ protected: * Construct a Theory. */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw() + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals) throw() : d_id(id) , d_satContext(satContext) , d_userContext(userContext) @@ -261,6 +263,7 @@ protected: , d_out(&out) , d_valuation(valuation) , d_proofEnabled(false) + , d_globals(globals) { StatisticsRegistry::registerStat(&d_checkTime); StatisticsRegistry::registerStat(&d_computeCareGraphTime); @@ -313,6 +316,8 @@ protected: */ bool d_proofEnabled; + SmtGlobals* d_globals; + public: /** @@ -870,6 +875,10 @@ public: */ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + + /** Returns a pointer to the globals copy the theory is using. */ + SmtGlobals* globals() { return d_globals; } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 52922e2ca..a55b3a1c9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -104,7 +104,8 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, - const LogicInfo& logicInfo) + const LogicInfo& logicInfo, + SmtGlobals* globals) : d_propEngine(NULL), d_decisionEngine(NULL), d_context(context), @@ -133,6 +134,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_false(), d_interrupted(false), d_resourceManager(NodeManager::currentResourceManager()), + d_globals(globals), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -1390,8 +1392,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // Share with other portfolio threads - if(options::lemmaOutputChannel() != NULL) { - options::lemmaOutputChannel()->notifyNewLemma(node.toExpr()); + if(d_globals->getLemmaOutputChannel() != NULL) { + d_globals->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); } // Run theory preprocessing, maybe diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2185f22ff..adc4daeee 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,6 +30,7 @@ #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 "theory/atom_requests.h" #include "theory/bv/bv_to_bool.h" @@ -206,6 +207,7 @@ class TheoryEngine { */ context::CDHashSet<Node, NodeHashFunction> d_hasPropagated; + /** * Statistics for a particular theory. */ @@ -476,10 +478,14 @@ class TheoryEngine { bool d_interrupted; ResourceManager* d_resourceManager; + /** Container for misc. globals. */ + SmtGlobals* d_globals; + public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveITE& iteRemover, const LogicInfo& logic); + TheoryEngine(context::Context* context, context::UserContext* userContext, + RemoveITE& iteRemover, const LogicInfo& logic, SmtGlobals* globals); /** Destroys a theory engine */ ~TheoryEngine(); @@ -498,7 +504,9 @@ public: inline void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); 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_theoryTable[theoryId] = + new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], + theory::Valuation(this), d_logicInfo, d_globals); } inline void setPropEngine(prop::PropEngine* propEngine) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 31bee316a..e21b7ef7d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -30,18 +30,20 @@ using namespace CVC4::theory; using namespace CVC4::theory::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) : - Theory(THEORY_UF, c, u, out, valuation, logicInfo), - 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, "theory::uf::TheoryUF", true), - d_conflict(c, false), - d_literalsToPropagate(c), - d_literalsToPropagateIndex(c, 0), - d_functionsTerms(c), - d_symb(u) +TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo, SmtGlobals* globals) + : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals), + 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, "theory::uf::TheoryUF", true), + d_conflict(c, false), + d_literalsToPropagate(c), + d_literalsToPropagateIndex(c, 0), + d_functionsTerms(c), + d_symb(u) { // 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 82597e286..aff78f53d 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -161,7 +161,9 @@ private: 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); + TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, + Valuation valuation, const LogicInfo& logicInfo, + SmtGlobals* globals); ~TheoryUF(); diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 55f1a14da..b06666ae3 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,8 @@ libutil_la_SOURCES = \ proof.h \ regexp.cpp \ regexp.h \ + result.cpp \ + result.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ subrange_bound.cpp \ @@ -89,6 +91,7 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational_gmp_imp.h \ regexp.i \ + result.i \ subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/expr/result.cpp b/src/util/result.cpp index aeb62b0c3..b981164a4 100644 --- a/src/expr/result.cpp +++ b/src/util/result.cpp @@ -13,7 +13,7 @@ ** ** Encapsulation of the result of a query. **/ -#include "expr/result.h" +#include "util/result.h" #include <algorithm> #include <cctype> @@ -21,12 +21,10 @@ #include <string> #include "base/cvc4_assert.h" -#include "expr/node.h" +#include "options/set_language.h" using namespace std; -#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/." - namespace CVC4 { Result::Result() @@ -268,7 +266,7 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { } ostream& operator<<(ostream& out, const Result& r) { - r.toStream(out, Node::setlanguage::getLanguage(out)); + r.toStream(out, language::SetLanguage::getLanguage(out)); return out; }/* operator<<(ostream&, const Result&) */ diff --git a/src/expr/result.h b/src/util/result.h index 8069f7ef9..8069f7ef9 100644 --- a/src/expr/result.h +++ b/src/util/result.h diff --git a/src/expr/result.i b/src/util/result.i index becbe9aa9..b77bfd881 100644 --- a/src/expr/result.i +++ b/src/util/result.i @@ -1,5 +1,5 @@ %{ -#include "expr/result.h" +#include "util/result.h" %} %ignore CVC4::operator<<(std::ostream&, const Result& r); @@ -17,4 +17,4 @@ %ignore CVC4::operator==(enum Result::Validity, const Result&); %ignore CVC4::operator!=(enum Result::Validity, const Result&); -%include "expr/result.h" +%include "util/result.h" |