diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/managed_ostreams.cpp | 192 | ||||
| -rw-r--r-- | src/smt/managed_ostreams.h | 181 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 409 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 29 | ||||
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine_scope.h | 2 | ||||
| -rw-r--r-- | src/smt/smt_globals.cpp | 111 | ||||
| -rw-r--r-- | src/smt/smt_globals.h | 106 | ||||
| -rw-r--r-- | src/smt/smt_options_handler.cpp | 1710 | ||||
| -rw-r--r-- | src/smt/smt_options_handler.h | 198 | ||||
| -rw-r--r-- | src/smt/update_ostream.h | 122 |
11 files changed, 832 insertions, 2230 deletions
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp new file mode 100644 index 000000000..1901f731d --- /dev/null +++ b/src/smt/managed_ostreams.cpp @@ -0,0 +1,192 @@ +/********************* */ +/*! \file managed_ostreams.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-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Wrappers to handle memory management of ostreams. + ** + ** This file contains wrappers to handle special cases of managing memory + ** related to ostreams. + **/ + +#include "smt/managed_ostreams.h" + +#include <ostream> + +#include "options/open_ostream.h" +#include "options/smt_options.h" +#include "smt/update_ostream.h" + +namespace CVC4 { + +ManagedOstream::ManagedOstream() : d_managed(NULL) {} + +ManagedOstream::~ManagedOstream() { + manage(NULL); + Assert(d_managed == NULL); +} + +void ManagedOstream::set(const std::string& filename) { + std::pair<bool, std::ostream*> pair = open(filename); + initialize(pair.second); + manage(pair.first ? pair.second : NULL); +} + +std::pair<bool, std::ostream*> ManagedOstream::open(const std::string& filename) + const { + OstreamOpener opener(getName()); + addSpecialCases(&opener); + return opener.open(filename); +} + +void ManagedOstream::manage(std::ostream* new_managed_value) { + if(d_managed == new_managed_value){ + // This is a no-op. + } else { + Assert(d_managed != new_managed_value); + std::ostream* old_managed_value = d_managed; + d_managed = new_managed_value; + if(old_managed_value != NULL){ + delete old_managed_value; + } + } +} + +ManagedDumpOStream::~ManagedDumpOStream() { + if(Dump.getStreamPointer() == getManagedOstream()) { + Dump.setStream(&null_os); + } +} + +std::string ManagedDumpOStream::defaultSource() const{ + return options::dumpToFileName(); +} + + +void ManagedDumpOStream::initialize(std::ostream* outStream) { +#ifdef CVC4_DUMPING + DumpOstreamUpdate dumpGetStream; + dumpGetStream.apply(outStream); +#else /* CVC4_DUMPING */ + throw OptionException( + "The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ +} + +void ManagedDumpOStream::addSpecialCases(OstreamOpener* opener) const { + opener->addSpecialCase("-", &DumpOutC::dump_cout); +} + +ManagedRegularOutputChannel::~ManagedRegularOutputChannel() { + // Set all ostream that may still be using the old value of this channel + // to null_os. Consult RegularOutputChannelListener for the list of + // channels. + if(options::err() == getManagedOstream()){ + options::err.set(&null_os); + } +} + +std::string ManagedRegularOutputChannel::defaultSource() const { + return options::regularChannelName(); +} + +void ManagedRegularOutputChannel::initialize(std::ostream* outStream) { + OptionsErrOstreamUpdate optionsErrOstreamUpdate; + optionsErrOstreamUpdate.apply(outStream); +} + +void ManagedRegularOutputChannel::addSpecialCases(OstreamOpener* opener) + const { + opener->addSpecialCase("stdout", &std::cout); + opener->addSpecialCase("stderr", &std::cerr); +} + +ManagedDiagnosticOutputChannel::~ManagedDiagnosticOutputChannel() { + // Set all ostreams that may still be using the old value of this channel + // to null_os. Consult DiagnosticOutputChannelListener for the list of + // channels. + if(options::err() == getManagedOstream()){ + options::err.set(&null_os); + } + + if(Debug.getStreamPointer() == getManagedOstream()) { + Debug.setStream(&null_os); + } + if(Warning.getStreamPointer() == getManagedOstream()){ + Warning.setStream(&null_os); + } + if(Message.getStreamPointer() == getManagedOstream()){ + Message.setStream(&null_os); + } + if(Notice.getStreamPointer() == getManagedOstream()){ + Notice.setStream(&null_os); + } + if(Chat.getStreamPointer() == getManagedOstream()){ + Chat.setStream(&null_os); + } + if(Trace.getStreamPointer() == getManagedOstream()){ + Trace.setStream(&null_os); + } +} + + +std::string ManagedDiagnosticOutputChannel::defaultSource() const { + return options::diagnosticChannelName(); +} +void ManagedDiagnosticOutputChannel::initialize(std::ostream* outStream) { + DebugOstreamUpdate debugOstreamUpdate; + debugOstreamUpdate.apply(outStream); + WarningOstreamUpdate warningOstreamUpdate; + warningOstreamUpdate.apply(outStream); + MessageOstreamUpdate messageOstreamUpdate; + messageOstreamUpdate.apply(outStream); + NoticeOstreamUpdate noticeOstreamUpdate; + noticeOstreamUpdate.apply(outStream); + ChatOstreamUpdate chatOstreamUpdate; + chatOstreamUpdate.apply(outStream); + TraceOstreamUpdate traceOstreamUpdate; + traceOstreamUpdate.apply(outStream); + OptionsErrOstreamUpdate optionsErrOstreamUpdate; + optionsErrOstreamUpdate.apply(outStream); +} + +void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) + const { + opener->addSpecialCase("stdout", &std::cout); + opener->addSpecialCase("stderr", &std::cerr); +} + + +ManagedReplayLogOstream::ManagedReplayLogOstream() : d_replayLog(NULL) {} +ManagedReplayLogOstream::~ManagedReplayLogOstream(){ + if(d_replayLog != NULL) { + (*d_replayLog) << std::flush; + } +} + +std::string ManagedReplayLogOstream::defaultSource() const { + return options::replayLogFilename(); +} + +void ManagedReplayLogOstream::initialize(std::ostream* outStream) { + if(outStream != NULL){ + *outStream << language::SetLanguage(options::outputLanguage()) + << expr::ExprSetDepth(-1); + } + /* Do this regardless of managing the memory. */ + d_replayLog = outStream; +} + +/** Adds special cases to an ostreamopener. */ +void ManagedReplayLogOstream::addSpecialCases(OstreamOpener* opener) const { + opener->addSpecialCase("-", &std::cout); +} + + +}/* CVC4 namespace */ diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h new file mode 100644 index 000000000..05d026b24 --- /dev/null +++ b/src/smt/managed_ostreams.h @@ -0,0 +1,181 @@ +/********************* */ +/*! \file managed_ostreams.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-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Wrappers to handle memory management of ostreams. + ** + ** This file contains wrappers to handle special cases of managing memory + ** related to ostreams. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MANAGED_OSTREAMS_H +#define __CVC4__MANAGED_OSTREAMS_H + +#include <ostream> + +#include "options/open_ostream.h" +#include "smt/update_ostream.h" + +namespace CVC4 { + +/** This abstracts the management of ostream memory and initialization. */ +class ManagedOstream { + public: + /** Initially getManagedOstream() == NULL. */ + ManagedOstream(); + virtual ~ManagedOstream(); + + /** Returns the pointer to the managed ostream. */ + std::ostream* getManagedOstream() const { return d_managed; } + + /** Returns the name of the ostream geing managed. */ + virtual const char* getName() const = 0; + + /** + * Set opens a file with filename, initializes the stream. + * If the opened ostream is marked as managed, this calls manage(stream). + * If the opened ostream is not marked as managed, this calls manage(NULL). + */ + void set(const std::string& filename); + + /** If this is associated with an option, return the string value. */ + virtual std::string defaultSource() { return ""; } + + protected: + + /** + * Opens an ostream using OstreamOpener with the name getName() with the + * special cases added by addSpecialCases(). + */ + std::pair<bool, std::ostream*> open(const std::string& filename) const; + + /** + * Updates the value of managed pointer. Whenever this changes, + * beforeRelease() is called on the old value. + */ + void manage(std::ostream* new_managed_value); + + /** Initializes an output stream. Not necessarily managed. */ + virtual void initialize(std::ostream* outStream) {} + + /** Adds special cases to an ostreamopener. */ + virtual void addSpecialCases(OstreamOpener* opener) const {} + + private: + std::ostream* d_managed; +}; /* class ManagedOstream */ + +class SetToDefaultSourceListener : public Listener { + public: + SetToDefaultSourceListener(ManagedOstream* managedOstream) + : d_managedOstream(managedOstream){} + + virtual void notify() { + d_managedOstream->set(d_managedOstream->defaultSource()); + } + + private: + ManagedOstream* d_managedOstream; +}; + +/** + * This controls the memory associated with --dump-to. + * This is is assumed to recieve a set whenever diagnosticChannelName + * is updated. + */ +class ManagedDumpOStream : public ManagedOstream { + public: + ManagedDumpOStream(){} + ~ManagedDumpOStream(); + + virtual const char* getName() const { return "dump-to"; } + virtual std::string defaultSource() const; + + protected: + /** Initializes an output stream. Not necessarily managed. */ + virtual void initialize(std::ostream* outStream); + + /** Adds special cases to an ostreamopener. */ + virtual void addSpecialCases(OstreamOpener* opener) const; +};/* class ManagedDumpOStream */ + +/** + * When d_managedRegularChannel is non-null, it owns the memory allocated + * with the regular-output-channel. This is set when + * options::regularChannelName is set. + */ +class ManagedRegularOutputChannel : public ManagedOstream { + public: + ManagedRegularOutputChannel(){} + + /** Assumes Options are in scope. */ + ~ManagedRegularOutputChannel(); + + virtual const char* getName() const { return "regular-output-channel"; } + virtual std::string defaultSource() const; + + protected: + /** Initializes an output stream. Not necessarily managed. */ + virtual void initialize(std::ostream* outStream); + + /** Adds special cases to an ostreamopener. */ + virtual void addSpecialCases(OstreamOpener* opener) const; +};/* class ManagedRegularOutputChannel */ + + +/** + * This controls the memory associated with diagnostic-output-channel. + * This is is assumed to recieve a set whenever options::diagnosticChannelName + * is updated. + */ +class ManagedDiagnosticOutputChannel : public ManagedOstream { + public: + ManagedDiagnosticOutputChannel(){} + + /** Assumes Options are in scope. */ + ~ManagedDiagnosticOutputChannel(); + + virtual const char* getName() const { return "diagnostic-output-channel"; } + virtual std::string defaultSource() const; + + protected: + /** Initializes an output stream. Not necessarily managed. */ + virtual void initialize(std::ostream* outStream); + + /** Adds special cases to an ostreamopener. */ + virtual void addSpecialCases(OstreamOpener* opener) const; +};/* class ManagedRegularOutputChannel */ + +/** This controls the memory associated with replay-log. */ +class ManagedReplayLogOstream : public ManagedOstream { + public: + ManagedReplayLogOstream(); + ~ManagedReplayLogOstream(); + + std::ostream* getReplayLog() const { return d_replayLog; } + virtual const char* getName() const { return "replay-log"; } + virtual std::string defaultSource() const; + + protected: + /** Initializes an output stream. Not necessarily managed. */ + virtual void initialize(std::ostream* outStream); + + /** Adds special cases to an ostreamopener. */ + virtual void addSpecialCases(OstreamOpener* opener) const; + + private: + std::ostream* d_replayLog; +};/* class ManagedRegularOutputChannel */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__MANAGED_OSTREAMS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c66031265..df3466d92 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,6 +26,8 @@ #include <utility> #include <vector> +#include "base/configuration.h" +#include "base/configuration_private.h" #include "base/exception.h" #include "base/listener.h" #include "base/modal_exception.h" @@ -52,8 +54,8 @@ #include "options/decision_mode.h" #include "options/decision_options.h" #include "options/main_options.h" +#include "options/open_ostream.h" #include "options/option_exception.h" -#include "options/options_handler_interface.h" #include "options/printer_options.h" #include "options/prop_options.h" #include "options/quantifiers_options.h" @@ -72,9 +74,10 @@ #include "smt/boolean_terms.h" #include "smt/command_list.h" #include "smt/logic_request.h" +#include "smt/managed_ostreams.h" #include "smt/model_postprocessor.h" #include "smt/smt_engine_scope.h" -#include "smt/smt_options_handler.h" +#include "smt/update_ostream.h" #include "smt_util/boolean_simplification.h" #include "smt_util/command.h" #include "smt_util/ite_removal.h" @@ -95,8 +98,6 @@ #include "theory/theory_engine.h" #include "theory/theory_model.h" #include "theory/theory_traits.h" -#include "util/configuration.h" -#include "util/configuration_private.h" #include "util/hash.h" #include "util/proof.h" #include "util/resource_manager.h" @@ -322,6 +323,125 @@ class HardResourceOutListener : public Listener { SmtEngine* d_smt; }; /* class HardResourceOutListener */ +class SetLogicListener : public Listener { + public: + SetLogicListener(SmtEngine& smt) : d_smt(&smt) {} + virtual void notify() { + LogicInfo inOptions(options::forceLogicString()); + d_smt->setLogic(inOptions); + } + private: + SmtEngine* d_smt; +}; /* class SetLogicListener */ + +class BeforeSearchListener : public Listener { + public: + BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {} + virtual void notify() { + d_smt->beforeSearch(); + } + private: + SmtEngine* d_smt; +}; /* class BeforeSearchListener */ + +class UseTheoryListListener : public Listener { + public: + UseTheoryListListener(TheoryEngine* theoryEngine) + : d_theoryEngine(theoryEngine) + {} + + void notify() { + std::stringstream commaList(options::useTheoryList()); + std::string token; + + Debug("UseTheoryListListener") << "UseTheoryListListener::notify() " + << options::useTheoryList() << std::endl; + + while(std::getline(commaList, token, ',')){ + if(token == "help") { + puts(theory::useTheoryHelp); + exit(1); + } + if(theory::useTheoryValidate(token)) { + d_theoryEngine->enableTheoryAlternative(token); + } else { + throw OptionException( + std::string("unknown option for --use-theory : `") + token + + "'. Try --use-theory=help."); + } + } + } + + private: + TheoryEngine* d_theoryEngine; +}; /* class UseTheoryListListener */ + + +class SetDefaultExprDepthListener : public Listener { + public: + virtual void notify() { + int depth = options::defaultExprDepth(); + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); + // intentionally exclude Dump stream from this list + } +}; + +class SetDefaultExprDagListener : public Listener { + public: + virtual void notify() { + int dag = options::defaultDagThresh(); + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); + } +}; + +class SetPrintExprTypesListener : public Listener { + public: + virtual void notify() { + bool value = options::printExprTypes(); + Debug.getStream() << expr::ExprPrintTypes(value); + Trace.getStream() << expr::ExprPrintTypes(value); + Notice.getStream() << expr::ExprPrintTypes(value); + Chat.getStream() << expr::ExprPrintTypes(value); + Message.getStream() << expr::ExprPrintTypes(value); + Warning.getStream() << expr::ExprPrintTypes(value); + // intentionally exclude Dump stream from this list + } +}; + +class DumpModeListener : public Listener { + public: + virtual void notify() { + const std::string& value = options::dumpModeString(); + Dump.setDumpFromString(value); + } +}; + +class PrintSuccessListener : public Listener { + public: + virtual void notify() { + bool value = options::printSuccess(); + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + Message.getStream() << Command::printsuccess(value); + Warning.getStream() << Command::printsuccess(value); + *options::out() << Command::printsuccess(value); + } +}; + + /** * This is an inelegant solution, but for the present, it will work. @@ -340,20 +460,38 @@ class HardResourceOutListener : public Listener { class SmtEnginePrivate : public NodeManagerListener { SmtEngine& d_smt; + typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; + typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; + /** * Manager for limiting time and abstract resource usage. */ ResourceManager* d_resourceManager; - /** - * Listener for the when a soft resource out occurs. - */ - RegisterListener* d_softResourceOutListener; + /** Manager for the memory of regular-output-channel. */ + ManagedRegularOutputChannel d_managedRegularChannel; + + /** Manager for the memory of diagnostic-output-channel. */ + ManagedDiagnosticOutputChannel d_managedDiagnosticChannel; + + /** Manager for the memory of --dump-to. */ + ManagedDumpOStream d_managedDumpChannel; + + /** Manager for --replay-log. */ + ManagedReplayLogOstream d_managedReplayLog; /** - * Listener for the when a hard resource out occurs. + * This list contains: + * softResourceOut + * hardResourceOut + * setForceLogic + * beforeSearchListener + * UseTheoryListListener + * + * This needs to be deleted before both NodeManager's Options, + * SmtEngine, d_resourceManager, and TheoryEngine. */ - RegisterListener* d_hardResourceOutListener; + ListenerRegistrationList* d_listenerRegistrations; /** Learned literals */ vector<Node> d_nonClausalLearnedLiterals; @@ -399,7 +537,7 @@ class SmtEnginePrivate : public NodeManagerListener { * same AbstractValues for the same real constants. Only used if * options::abstractValues() is on. */ - hash_map<Node, Node, NodeHashFunction> d_abstractValues; + NodeToNodeHashMap d_abstractValues; /** Number of calls of simplify assertions active. */ @@ -442,18 +580,20 @@ private: */ void removeITEs(); - Node intToBV(TNode n, std::hash_map<Node, Node, NodeHashFunction>& cache); - Node intToBVMakeBinary(TNode n, std::hash_map<Node, Node, NodeHashFunction>& cache); + Node intToBV(TNode n, NodeToNodeHashMap& cache); + Node intToBVMakeBinary(TNode n, NodeToNodeHashMap& cache); /** - * Helper function to fix up assertion list to restore invariants needed after ite removal + * Helper function to fix up assertion list to restore invariants needed after + * ite removal. */ - void collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache); + void collectSkolems(TNode n, set<TNode>& skolemSet, NodeToBoolHashMap& cache); /** - * Helper function to fix up assertion list to restore invariants needed after ite removal + * Helper function to fix up assertion list to restore invariants needed after + * ite removal. */ - bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache); + bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache); // Lift bit-vectors of size 1 to booleans void bvToBool(); @@ -468,8 +608,10 @@ private: // Simplify based on unconstrained values void unconstrainedSimp(); - // Ensures the assertions asserted after before now - // effectively come before d_realAssertionsEnd + /** + * Ensures the assertions asserted after before now effectively come before + * d_realAssertionsEnd. + */ void compressBeforeRealAssertions(size_t before); /** @@ -480,12 +622,21 @@ private: void constrainSubtypes(TNode n, AssertionPipeline& assertions) throw(); - // trace nodes back to their assertions using CircuitPropagator's BackEdgesMap - void traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions); - // remove conjuncts in toRemove from conjunction n; return # of removed conjuncts - size_t removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove); + /** + * Trace nodes back to their assertions using CircuitPropagator's + * BackEdgesMap. + */ + void traceBackToAssertions(const std::vector<Node>& nodes, + std::vector<TNode>& assertions); - // scrub miplib encodings + /** + * Remove conjuncts in toRemove from conjunction n. Return # of removed + * conjuncts. + */ + size_t removeFromConjunction(Node& n, + const std::hash_set<unsigned long>& toRemove); + + /** Scrub miplib encodings. */ void doMiplibTrick(); /** @@ -495,15 +646,18 @@ private: * * Returns false if the formula simplifies to "false" */ - bool simplifyAssertions() throw(TypeCheckingException, LogicException, UnsafeInterruptException); + bool simplifyAssertions() throw(TypeCheckingException, LogicException, + UnsafeInterruptException); public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), - d_resourceManager(NULL), - d_softResourceOutListener(NULL), - d_hardResourceOutListener(NULL), + d_managedRegularChannel(), + d_managedDiagnosticChannel(), + d_managedDumpChannel(), + d_managedReplayLog(), + d_listenerRegistrations(new ListenerRegistrationList()), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), d_booleanTermConverter(NULL), @@ -525,21 +679,59 @@ public: d_true = NodeManager::currentNM()->mkConst(true); d_resourceManager = NodeManager::currentResourceManager(); - d_softResourceOutListener = new RegisterListener( - d_resourceManager->getSoftListeners(), - new SoftResourceOutListener(d_smt)); - - d_hardResourceOutListener = new RegisterListener( - d_resourceManager->getHardListeners(), - new HardResourceOutListener(d_smt)); - + d_listenerRegistrations->add(d_resourceManager->registerSoftListener( + new SoftResourceOutListener(d_smt))); + + d_listenerRegistrations->add(d_resourceManager->registerHardListener( + new HardResourceOutListener(d_smt))); + + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + d_listenerRegistrations->add( + nodeManagerOptions.registerForceLogicListener( + new SetLogicListener(d_smt), true)); + + // Multiple options reuse BeforeSearchListener so registration requires an + // extra bit of care. + // We can safely not call notify on this before search listener at + // registration time. This d_smt cannot be beforeSearch at construction + // time. Therefore the BeforeSearchListener is a no-op. Therefore it does + // not have to be called. + d_listenerRegistrations->add( + nodeManagerOptions.registerBeforeSearchListener( + new BeforeSearchListener(d_smt))); + + // These do need registration calls. + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDefaultExprDepthListener( + new SetDefaultExprDepthListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDefaultExprDagListener( + new SetDefaultExprDagListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetPrintExprTypesListener( + new SetPrintExprTypesListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDumpModeListener( + new DumpModeListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetPrintSuccessListener( + new PrintSuccessListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetRegularOutputChannelListener( + new SetToDefaultSourceListener(&d_managedRegularChannel), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDiagnosticOutputChannelListener( + new SetToDefaultSourceListener(&d_managedDiagnosticChannel), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerDumpToFileNameListener( + new SetToDefaultSourceListener(&d_managedDumpChannel), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetReplayLogFilename( + new SetToDefaultSourceListener(&d_managedReplayLog), true)); } ~SmtEnginePrivate() throw() { - delete d_hardResourceOutListener; - d_hardResourceOutListener = NULL; - delete d_softResourceOutListener; - d_softResourceOutListener = NULL; + delete d_listenerRegistrations; if(d_propagatorNeedsFinish) { d_propagator.finish(); @@ -642,11 +834,10 @@ public: void addFormula(TNode n, bool inUnsatCore, bool inInput = true) throw(TypeCheckingException, LogicException); - /** - * Expand definitions in n. - */ - Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false) - throw(TypeCheckingException, LogicException, UnsafeInterruptException); + /** Expand definitions in n. */ + Node expandDefinitions(TNode n, NodeToNodeHashMap& cache, + bool expandOnly = false) + throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** * Rewrite Boolean terms in a Node. @@ -660,7 +851,7 @@ public: Node simplify(TNode in) { // Substitute out any abstract values in ex. // Expand definitions. - hash_map<Node, Node, NodeHashFunction> cache; + NodeToNodeHashMap cache; Node n = expandDefinitions(in, cache).toExpr(); // Make sure we've done all preprocessing, etc. Assert(d_assertions.size() == 0); @@ -689,24 +880,33 @@ public: d_abstractValueMap.addSubstitution(val, n); } // We are supposed to ascribe types to all abstract values that go out. - Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val); + NodeManager* current = d_smt.d_nodeManager; + Node ascription = current->mkConst(AscriptionType(n.getType().toType())); + Node retval = current->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val); return retval; } - std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache; + NodeToNodeHashMap d_rewriteApplyToConstCache; Node rewriteApplyToConst(TNode n) { Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl; - if(n.getMetaKind() == kind::metakind::CONSTANT || n.getMetaKind() == kind::metakind::VARIABLE) { + if(n.getMetaKind() == kind::metakind::CONSTANT || + n.getMetaKind() == kind::metakind::VARIABLE) + { return n; } - if(rewriteApplyToConstCache.find(n) != rewriteApplyToConstCache.end()) { - Trace("rewriteApplyToConst") << "in cache :: " << rewriteApplyToConstCache[n] << std::endl; - return rewriteApplyToConstCache[n]; + if(d_rewriteApplyToConstCache.find(n) != d_rewriteApplyToConstCache.end()) { + Trace("rewriteApplyToConst") << "in cache :: " + << d_rewriteApplyToConstCache[n] + << std::endl; + return d_rewriteApplyToConstCache[n]; } + if(n.getKind() == kind::APPLY_UF) { - if(n.getNumChildren() == 1 && n[0].isConst() && n[0].getType().isInteger()) { + if(n.getNumChildren() == 1 && n[0].isConst() && + n[0].getType().isInteger()) + { stringstream ss; ss << n.getOperator() << "_"; if(n[0].getConst<Rational>() < 0) { @@ -714,15 +914,19 @@ public: } else { ss << n[0]; } - Node newvar = NodeManager::currentNM()->mkSkolem(ss.str(), n.getType(), "rewriteApplyToConst skolem", NodeManager::SKOLEM_EXACT_NAME); - rewriteApplyToConstCache[n] = newvar; + Node newvar = NodeManager::currentNM()->mkSkolem( + ss.str(), n.getType(), "rewriteApplyToConst skolem", + NodeManager::SKOLEM_EXACT_NAME); + d_rewriteApplyToConstCache[n] = newvar; Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl; return newvar; } else { stringstream ss; - ss << "The rewrite-apply-to-const preprocessor is currently limited;\n" - << "it only works if all function symbols are unary and with Integer\n" - << "domain, and all applications are to integer values.\n" + ss << "The rewrite-apply-to-const preprocessor is currently limited;" + << std::endl + << "it only works if all function symbols are unary and with Integer" + << std::endl + << "domain, and all applications are to integer values." << std::endl << "Found application: " << n; Unhandled(ss.str()); } @@ -736,11 +940,21 @@ public: builder << rewriteApplyToConst(n[i]); } Node rewr = builder; - rewriteApplyToConstCache[n] = rewr; + d_rewriteApplyToConstCache[n] = rewr; Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl; return rewr; } + void addUseTheoryListListener(TheoryEngine* theoryEngine){ + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + d_listenerRegistrations->add( + nodeManagerOptions.registerUseTheoryListListener( + new UseTheoryListListener(theoryEngine), true)); + } + + std::ostream* getReplayLog() const { + return d_managedReplayLog.getReplayLog(); + } };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -765,7 +979,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_dumpCommands(), d_defineCommands(), d_logic(), - d_originalOptions(em->getOptions()), + d_originalOptions(), d_pendingPops(0), d_fullyInited(false), d_problemExtended(false), @@ -773,15 +987,15 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_needPostsolve(false), d_earlyTheoryPP(true), d_status(), - d_optionsHandler(new SmtOptionsHandler(this)), + d_replayStream(NULL), d_private(NULL), d_smtAttributes(NULL), d_statisticsRegistry(NULL), d_stats(NULL), - d_globals(new SmtGlobals()) + d_channels(new LemmaChannels()) { - SmtScope smts(this); + d_originalOptions.copyValues(em->getOptions()); d_smtAttributes = new expr::attr::SmtAttributes(d_context); d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); @@ -800,7 +1014,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic), - d_globals); + d_channels); // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { @@ -809,6 +1023,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : THEORY_PROOF(ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); ); } + d_private->addUseTheoryListListener(d_theoryEngine); + // global push/pop around everything, to ensure proper destruction // of context-dependent data structures d_userContext->push(); @@ -830,7 +1046,8 @@ void SmtEngine::finishInit() { d_decisionEngine->init(); // enable appropriate strategies d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, - d_userContext, d_globals); + d_userContext, d_private->getReplayLog(), + d_replayStream, d_channels); d_theoryEngine->setPropEngine(d_propEngine); d_theoryEngine->setDecisionEngine(d_decisionEngine); @@ -959,9 +1176,6 @@ SmtEngine::~SmtEngine() throw() { delete d_statisticsRegistry; d_statisticsRegistry = NULL; - delete d_optionsHandler; - d_optionsHandler = NULL; - delete d_private; d_private = NULL; @@ -973,8 +1187,8 @@ SmtEngine::~SmtEngine() throw() { delete d_context; d_context = NULL; - delete d_globals; - d_globals = NULL; + delete d_channels; + d_channels = NULL; } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl @@ -985,13 +1199,15 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); if(d_fullyInited) { - throw ModalException("Cannot set logic in SmtEngine after the engine has finished initializing"); + throw ModalException("Cannot set logic in SmtEngine after the engine has " + "finished initializing."); } d_logic = logic; setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) { +void SmtEngine::setLogic(const std::string& s) + throw(ModalException, LogicException) { SmtScope smts(this); try { setLogic(LogicInfo(s)); @@ -1000,7 +1216,8 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicExcept } } -void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) { +void SmtEngine::setLogic(const char* logic) + throw(ModalException, LogicException) { setLogic(string(logic)); } @@ -1009,13 +1226,14 @@ LogicInfo SmtEngine::getLogicInfo() const { } void SmtEngine::setLogicInternal() throw() { - Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already finished initializing for this run"); + Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already" + " finished initializing for this run"); d_logic.lock(); } void SmtEngine::setDefaults() { - if(options::forceLogic.wasSetByUser()) { - d_logic = *(options::forceLogic()); + if(options::forceLogicString.wasSetByUser()) { + d_logic = LogicInfo(options::forceLogicString()); } else if (options::solveIntAsBV() > 0) { d_logic = LogicInfo("QF_BV"); @@ -1039,11 +1257,13 @@ void SmtEngine::setDefaults() { d_logic = d_logic.getUnlockedCopy(); d_logic.enableQuantifiers(); d_logic.lock(); - Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; + Trace("smt") << "turning on quantifier logic, for strings-exp" + << std::endl; } if(! options::finiteModelFind.wasSetByUser()) { options::finiteModelFind.set( true ); - Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; + Trace("smt") << "turning on finite-model-find, for strings-exp" + << std::endl; } if(! options::fmfBoundInt.wasSetByUser()) { if(! options::fmfBoundIntLazy.wasSetByUser()) { @@ -1067,7 +1287,8 @@ void SmtEngine::setDefaults() { if(options::checkModels()) { if(! options::produceAssertions()) { - Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl; + Notice() << "SmtEngine: turning on produce-assertions to support " + << "check-models." << endl; setOption("produce-assertions", SExpr("true")); } } @@ -1077,7 +1298,8 @@ void SmtEngine::setDefaults() { if(options::simplificationMode.wasSetByUser()) { throw OptionException("simplification not supported with unsat cores"); } - Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl; + Notice() << "SmtEngine: turning off simplification to support unsat-cores" + << endl; options::simplificationMode.set(SIMPLIFICATION_MODE_NONE); } @@ -4923,9 +5145,10 @@ void SmtEngine::reset() throw() { if(Dump.isOn("benchmark")) { Dump("benchmark") << ResetCommand(); } - Options opts = d_originalOptions; + Options opts; + opts.copyValues(d_originalOptions); this->~SmtEngine(); - NodeManager::fromExprManager(em)->getOptions() = opts; + NodeManager::fromExprManager(em)->getOptions().copyValues(opts); new(this) SmtEngine(em); } @@ -5022,11 +5245,10 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) { -void SmtEngine::beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException) { - if(smt != NULL && smt->d_fullyInited) { - std::stringstream ss; - ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; - throw ModalException(ss.str()); +void SmtEngine::beforeSearch() throw(ModalException) { + if(d_fullyInited) { + throw ModalException( + "SmtEngine::beforeSearch called after initialization."); } } @@ -5064,8 +5286,8 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) } string optionarg = value.getValue(); - - d_optionsHandler->setOption(key, optionarg); + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + nodeManagerOptions.setOption(key, optionarg); } CVC4::SExpr SmtEngine::getOption(const std::string& key) const @@ -5121,7 +5343,14 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr(result); } - return SExpr::parseAtom(d_optionsHandler->getOption(key)); + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + return SExpr::parseAtom(nodeManagerOptions.getOption(key)); +} + +void SmtEngine::setReplayStream(ExprStream* replayStream) { + AlwaysAssert(!d_fullyInited, + "Cannot set replay stream once fully initialized"); + d_replayStream = replayStream; } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2f222790c..3616762bc 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,10 +28,11 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "expr/expr_stream.h" #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" -#include "smt/smt_globals.h" +#include "smt_util/lemma_channels.h" #include "theory/logic_info.h" #include "util/hash.h" #include "util/proof.h" @@ -73,10 +74,6 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ -namespace options { - class OptionsHandler; -}/* CVC4::prop namespace */ - namespace expr { namespace attr { class AttributeManager; @@ -267,10 +264,8 @@ class CVC4_PUBLIC SmtEngine { */ std::map<std::string, Integer> d_commandVerbosity; - /** - * This responds to requests to set options. - */ - options::OptionsHandler* d_optionsHandler; + /** ReplayStream for the solver. */ + ExprStream* d_replayStream; /** * A private utility class to SmtEngine. @@ -386,7 +381,8 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEngineStatistics* d_stats; - SmtGlobals* d_globals; + /** Container for the lemma input and output channels for this SmtEngine.*/ + LemmaChannels* d_channels; /** * Add to Model command. This is used for recording a command @@ -728,12 +724,19 @@ public: void setPrintFuncInModel(Expr f, bool p); + /** Throws a ModalException if the SmtEngine has been fully initialized. */ + void beforeSearch() throw(ModalException); + + LemmaChannels* channels() { return d_channels; } + + /** - * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized. + * Expermintal feature: Sets the sequence of decisions. + * This currently requires very fine grained knowledge about literal + * translation. */ - static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException); + void setReplayStream(ExprStream* exprStream); - SmtGlobals* globals() { return d_globals; } };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 14adcc536..354a43cc8 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -25,10 +25,10 @@ #warning "TODO: Why is lfsc's check.h being included like this?" #include "check.h" +#include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" #include "smt/smt_engine.h" -#include "util/configuration_private.h" #include "util/statistics_registry.h" using namespace CVC4; diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index c4ec15371..5a7e39849 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -19,6 +19,7 @@ #pragma once +#include "base/configuration_private.h" #include "base/cvc4_assert.h" #include "base/output.h" #include "base/tls.h" @@ -27,7 +28,6 @@ #include "proof/proof_manager.h" #include "options/smt_options.h" #include "smt/smt_engine.h" -#include "util/configuration_private.h" namespace CVC4 { diff --git a/src/smt/smt_globals.cpp b/src/smt/smt_globals.cpp deleted file mode 100644 index 4c1b0dc72..000000000 --- a/src/smt/smt_globals.cpp +++ /dev/null @@ -1,111 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index 00b90a703..000000000 --- a/src/smt/smt_globals.h +++ /dev/null @@ -1,106 +0,0 @@ -/********************* */ -/*! \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 deleted file mode 100644 index 758ffaec8..000000000 --- a/src/smt/smt_options_handler.cpp +++ /dev/null @@ -1,1710 +0,0 @@ -/********************* */ -/*! \file options_handler_interface.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-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Interface for custom handlers and predicates options. - ** - ** Interface for custom handlers and predicates options. - **/ - -#include "smt/smt_options_handler.h" - -#include <cerrno> -#include <cstring> -#include <ostream> -#include <sstream> -#include <string> - -#include "base/modal_exception.h" -#include "base/output.h" -#include "cvc4autoconfig.h" -#include "expr/expr_iomanip.h" -#include "expr/metakind.h" -#include "expr/node_manager.h" -#include "lib/strtok_r.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" -#include "options/base_options.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/bv_options.h" -#include "options/decision_mode.h" -#include "options/decision_options.h" -#include "options/didyoumean.h" -#include "options/language.h" -#include "options/main_options.h" -#include "options/option_exception.h" -#include "options/options_handler_interface.h" -#include "options/parser_options.h" -#include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/set_language.h" -#include "options/simplification_mode.h" -#include "options/smt_options.h" -#include "options/theory_options.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" -#include "smt/smt_engine.h" -#include "smt_util/command.h" -#include "smt_util/dump.h" -#include "theory/logic_info.h" -#include "util/configuration.h" -#include "util/configuration_private.h" -#include "util/resource_manager.h" - - -#warning "TODO: Make SmtOptionsHandler non-public and refactor driver unified." - -namespace CVC4 { -namespace smt { - -SmtOptionsHandler::SmtOptionsHandler(SmtEngine* smt) - : d_smtEngine(smt) -{} - -SmtOptionsHandler::~SmtOptionsHandler(){} - -// theory/arith/options_handlers.h -const std::string SmtOptionsHandler::s_arithUnateLemmasHelp = "\ -Unate lemmas are generated before SAT search begins using the relationship\n\ -of constant terms and polynomials.\n\ -Modes currently supported by the --unate-lemmas option:\n\ -+ none \n\ -+ ineqs \n\ - Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ -+ eqs \n\ - Outputs lemmas of the general forms\n\ - (= p c) implies (<= p d) for c < d, or\n\ - (= p c) implies (not (= p d)) for c != d.\n\ -+ all \n\ - A combination of inequalities and equalities.\n\ -"; - -const std::string SmtOptionsHandler::s_arithPropagationModeHelp = "\ -This decides on kind of propagation arithmetic attempts to do during the search.\n\ -+ none\n\ -+ unate\n\ - use constraints to do unate propagation\n\ -+ bi (Bounds Inference)\n\ - infers bounds on basic variables using the upper and lower bounds of the\n\ - non-basic variables in the tableau.\n\ -+both\n\ -"; - -const std::string SmtOptionsHandler::s_errorSelectionRulesHelp = "\ -This decides on the rule used by simplex during heuristic rounds\n\ -for deciding the next basic variable to select.\n\ -Heuristic pivot rules available:\n\ -+min\n\ - The minimum abs() value of the variable's violation of its bound. (default)\n\ -+max\n\ - The maximum violation the bound\n\ -+varord\n\ - The variable order\n\ -"; - -ArithUnateLemmaMode SmtOptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "all") { - return ALL_PRESOLVE_LEMMAS; - } else if(optarg == "none") { - return NO_PRESOLVE_LEMMAS; - } else if(optarg == "ineqs") { - return INEQUALITY_PRESOLVE_LEMMAS; - } else if(optarg == "eqs") { - return EQUALITY_PRESOLVE_LEMMAS; - } else if(optarg == "help") { - puts(s_arithUnateLemmasHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --unate-lemmas: `") + - optarg + "'. Try --unate-lemmas help."); - } -} - -ArithPropagationMode SmtOptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "none") { - return NO_PROP; - } else if(optarg == "unate") { - return UNATE_PROP; - } else if(optarg == "bi") { - return BOUND_INFERENCE_PROP; - } else if(optarg == "both") { - return BOTH_PROP; - } else if(optarg == "help") { - puts(s_arithPropagationModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --arith-prop: `") + - optarg + "'. Try --arith-prop help."); - } -} - -ErrorSelectionRule SmtOptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "min") { - return MINIMUM_AMOUNT; - } else if(optarg == "varord") { - return VAR_ORDER; - } else if(optarg == "max") { - return MAXIMUM_AMOUNT; - } else if(optarg == "help") { - puts(s_errorSelectionRulesHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") + - optarg + "'. Try --heuristic-pivot-rule help."); - } -} - -// theory/quantifiers/options_handlers.h - -const std::string SmtOptionsHandler::s_instWhenHelp = "\ -Modes currently supported by the --inst-when option:\n\ -\n\ -full-last-call (default)\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ -full\n\ -+ Run instantiation round at full effort, before theory combination.\n\ -\n\ -full-delay \n\ -+ Run instantiation round at full effort, before theory combination, after\n\ - all other theories have finished.\n\ -\n\ -full-delay-last-call \n\ -+ Alternate running instantiation rounds at full effort after all other\n\ - theories have finished, and last call. \n\ -\n\ -last-call\n\ -+ Run instantiation at last call effort, after theory combination and\n\ - and theories report sat.\n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_literalMatchHelp = "\ -Literal match modes currently supported by the --literal-match option:\n\ -\n\ -none (default)\n\ -+ Do not use literal matching.\n\ -\n\ -predicate\n\ -+ Consider the phase requirements of predicate literals when applying heuristic\n\ - quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ - formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ - terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ - Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_mbqiModeHelp = "\ -Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ -\n\ -default \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ -\n\ -none \n\ -+ Disable model-based quantifier instantiation.\n\ -\n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -fmc-interval \n\ -+ Same as default, but with intervals for models of integer functions.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_qcfWhenModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ -\n\ -default \n\ -+ Default, apply conflict finding at full effort.\n\ -\n\ -last-call \n\ -+ Apply conflict finding at last call, after theory combination and \n\ - and all theories report sat. \n\ -\n\ -std \n\ -+ Apply conflict finding at standard effort.\n\ -\n\ -std-h \n\ -+ Apply conflict finding at standard effort when heuristic says to. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_qcfModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf option:\n\ -\n\ -prop-eq \n\ -+ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\ -\n\ -conflict \n\ -+ Apply QCF algorithm to find conflicts only.\n\ -\n\ -partial \n\ -+ Apply QCF algorithm to instantiate heuristically as well. \n\ -\n\ -mc \n\ -+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_userPatModeHelp = "\ -User pattern modes currently supported by the --user-pat option:\n\ -\n\ -trust \n\ -+ When provided, use only user-provided patterns for a quantified formula.\n\ -\n\ -use \n\ -+ Use both user-provided and auto-generated patterns when patterns\n\ - are provided for a quantified formula.\n\ -\n\ -resort \n\ -+ Use user-provided patterns only after auto-generated patterns saturate.\n\ -\n\ -ignore \n\ -+ Ignore user-provided patterns. \n\ -\n\ -interleave \n\ -+ Alternate between use/resort. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_triggerSelModeHelp = "\ -Trigger selection modes currently supported by the --trigger-sel option:\n\ -\n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ -+ Consider only minimal subterms that meet criteria for triggers.\n\ -\n\ -max \n\ -+ Consider only maximal subterms that meet criteria for triggers. \n\ -\n\ -"; -const std::string SmtOptionsHandler::s_prenexQuantModeHelp = "\ -Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ -\n\ -default \n\ -+ Default, prenex all nested quantifiers except those with user patterns.\n\ -\n\ -all \n\ -+ Prenex all nested quantifiers.\n\ -\n\ -none \n\ -+ Do no prenex nested quantifiers. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_cegqiFairModeHelp = "\ -Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ -\n\ -uf-dt-size \n\ -+ Enforce fairness using an uninterpreted function for datatypes size.\n\ -\n\ -default | dt-size \n\ -+ Default, enforce fairness using size theory operator.\n\ -\n\ -dt-height-bound \n\ -+ Enforce fairness by height bound predicate.\n\ -\n\ -none \n\ -+ Do not enforce fairness. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_termDbModeHelp = "\ -Modes for term database, supported by --term-db-mode:\n\ -\n\ -all \n\ -+ Quantifiers module considers all ground terms.\n\ -\n\ -relevant \n\ -+ Quantifiers module considers only ground terms connected to current assertions. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_iteLiftQuantHelp = "\ -Modes for term database, supported by --ite-lift-quant:\n\ -\n\ -none \n\ -+ Do not lift if-then-else in quantified formulas.\n\ -\n\ -simple \n\ -+ Lift if-then-else in quantified formulas if results in smaller term size.\n\ -\n\ -all \n\ -+ Lift if-then-else in quantified formulas. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_sygusInvTemplHelp = "\ -Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ -\n\ -none \n\ -+ Synthesize invariant directly.\n\ -\n\ -pre \n\ -+ Synthesize invariant based on weakening of precondition .\n\ -\n\ -post \n\ -+ Synthesize invariant based on strengthening of postcondition. \n\ -\n\ -"; - -const std::string SmtOptionsHandler::s_macrosQuantHelp = "\ -Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ -\n\ -all \n\ -+ Infer definitions for functions, including those containing quantified formulas.\n\ -\n\ -ground (default) \n\ -+ Only infer ground definitions for functions.\n\ -\n\ -ground-uf \n\ -+ Only infer ground definitions for functions that result in triggers for all free variables.\n\ -\n\ -"; - -theory::quantifiers::InstWhenMode SmtOptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "pre-full") { - return theory::quantifiers::INST_WHEN_PRE_FULL; - } else if(optarg == "full") { - return theory::quantifiers::INST_WHEN_FULL; - } else if(optarg == "full-delay") { - return theory::quantifiers::INST_WHEN_FULL_DELAY; - } else if(optarg == "full-last-call") { - return theory::quantifiers::INST_WHEN_FULL_LAST_CALL; - } else if(optarg == "full-delay-last-call") { - return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL; - } else if(optarg == "last-call") { - return theory::quantifiers::INST_WHEN_LAST_CALL; - } else if(optarg == "help") { - puts(s_instWhenHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --inst-when: `") + - optarg + "'. Try --inst-when help."); - } -} - -void SmtOptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) { - if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) { - throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); - } -} - -theory::quantifiers::LiteralMatchMode SmtOptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "none") { - return theory::quantifiers::LITERAL_MATCH_NONE; - } else if(optarg == "predicate") { - return theory::quantifiers::LITERAL_MATCH_PREDICATE; - } else if(optarg == "equality") { - return theory::quantifiers::LITERAL_MATCH_EQUALITY; - } else if(optarg == "help") { - puts(s_literalMatchHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --literal-matching: `") + - optarg + "'. Try --literal-matching help."); - } -} - -void SmtOptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) { - if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) { - throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); - } -} - -theory::quantifiers::MbqiMode SmtOptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "gen-ev") { - return theory::quantifiers::MBQI_GEN_EVAL; - } else if(optarg == "none") { - return theory::quantifiers::MBQI_NONE; - } else if(optarg == "default" || optarg == "fmc") { - return theory::quantifiers::MBQI_FMC; - } else if(optarg == "fmc-interval") { - return theory::quantifiers::MBQI_FMC_INTERVAL; - } else if(optarg == "abs") { - return theory::quantifiers::MBQI_ABS; - } else if(optarg == "trust") { - return theory::quantifiers::MBQI_TRUST; - } else if(optarg == "help") { - puts(s_mbqiModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --mbqi: `") + - optarg + "'. Try --mbqi help."); - } -} - - -void SmtOptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {} - - -theory::quantifiers::QcfWhenMode SmtOptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default") { - return theory::quantifiers::QCF_WHEN_MODE_DEFAULT; - } else if(optarg == "last-call") { - return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL; - } else if(optarg == "std") { - return theory::quantifiers::QCF_WHEN_MODE_STD; - } else if(optarg == "std-h") { - return theory::quantifiers::QCF_WHEN_MODE_STD_H; - } else if(optarg == "help") { - puts(s_qcfWhenModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-when: `") + - optarg + "'. Try --quant-cf-when help."); - } -} - -theory::quantifiers::QcfMode SmtOptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "conflict") { - return theory::quantifiers::QCF_CONFLICT_ONLY; - } else if(optarg == "default" || optarg == "prop-eq") { - return theory::quantifiers::QCF_PROP_EQ; - } else if(optarg == "partial") { - return theory::quantifiers::QCF_PARTIAL; - } else if(optarg == "mc" ) { - return theory::quantifiers::QCF_MC; - } else if(optarg == "help") { - puts(s_qcfModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-mode: `") + - optarg + "'. Try --quant-cf-mode help."); - } -} - -theory::quantifiers::UserPatMode SmtOptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "use") { - return theory::quantifiers::USER_PAT_MODE_USE; - } else if(optarg == "default" || optarg == "trust") { - return theory::quantifiers::USER_PAT_MODE_TRUST; - } else if(optarg == "resort") { - return theory::quantifiers::USER_PAT_MODE_RESORT; - } else if(optarg == "ignore") { - return theory::quantifiers::USER_PAT_MODE_IGNORE; - } else if(optarg == "interleave") { - return theory::quantifiers::USER_PAT_MODE_INTERLEAVE; - } else if(optarg == "help") { - puts(s_userPatModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --user-pat: `") + - optarg + "'. Try --user-pat help."); - } -} - -theory::quantifiers::TriggerSelMode SmtOptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" || optarg == "all" ) { - return theory::quantifiers::TRIGGER_SEL_DEFAULT; - } else if(optarg == "min") { - return theory::quantifiers::TRIGGER_SEL_MIN; - } else if(optarg == "max") { - return theory::quantifiers::TRIGGER_SEL_MAX; - } else if(optarg == "help") { - puts(s_triggerSelModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --trigger-sel: `") + - optarg + "'. Try --trigger-sel help."); - } -} - - -theory::quantifiers::PrenexQuantMode SmtOptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" ) { - return theory::quantifiers::PRENEX_NO_USER_PAT; - } else if(optarg == "all") { - return theory::quantifiers::PRENEX_ALL; - } else if(optarg == "none") { - return theory::quantifiers::PRENEX_NONE; - } else if(optarg == "help") { - puts(s_prenexQuantModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --prenex-quant: `") + - optarg + "'. Try --prenex-quant help."); - } -} - -theory::quantifiers::CegqiFairMode SmtOptionsHandler::stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "uf-dt-size" ) { - return theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE; - } else if(optarg == "default" || optarg == "dt-size") { - return theory::quantifiers::CEGQI_FAIR_DT_SIZE; - } else if(optarg == "dt-height-bound" ){ - return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED; - } else if(optarg == "none") { - return theory::quantifiers::CEGQI_FAIR_NONE; - } else if(optarg == "help") { - puts(s_cegqiFairModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --cegqi-fair: `") + - optarg + "'. Try --cegqi-fair help."); - } -} - -theory::quantifiers::TermDbMode SmtOptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "all" ) { - return theory::quantifiers::TERM_DB_ALL; - } else if(optarg == "relevant") { - return theory::quantifiers::TERM_DB_RELEVANT; - } else if(optarg == "help") { - puts(s_termDbModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --term-db-mode: `") + - optarg + "'. Try --term-db-mode help."); - } -} - -theory::quantifiers::IteLiftQuantMode SmtOptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "all" ) { - return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL; - } else if(optarg == "simple") { - return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE; - } else if(optarg == "none") { - return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE; - } else if(optarg == "help") { - puts(s_iteLiftQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --ite-lift-quant: `") + - optarg + "'. Try --ite-lift-quant help."); - } -} - -theory::quantifiers::SygusInvTemplMode SmtOptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "none" ) { - return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE; - } else if(optarg == "pre") { - return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE; - } else if(optarg == "post") { - return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST; - } else if(optarg == "help") { - puts(s_sygusInvTemplHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + - optarg + "'. Try --sygus-inv-templ help."); - } -} - -theory::quantifiers::MacrosQuantMode SmtOptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "all" ) { - return theory::quantifiers::MACROS_QUANT_MODE_ALL; - } else if(optarg == "ground") { - return theory::quantifiers::MACROS_QUANT_MODE_GROUND; - } else if(optarg == "ground-uf") { - return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF; - } else if(optarg == "help") { - puts(s_macrosQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --macros-quant-mode: `") + - optarg + "'. Try --macros-quant-mode help."); - } -} - - - -// theory/bv/options_handlers.h -void SmtOptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) { -#ifndef CVC4_USE_ABC - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_USE_ABC */ -} - -void SmtOptionsHandler::abcEnabledBuild(std::string option, std::string value) throw(OptionException) { -#ifndef CVC4_USE_ABC - if(!value.empty()) { - std::stringstream ss; - ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_USE_ABC */ -} - -const std::string SmtOptionsHandler::s_bitblastingModeHelp = "\ -Bit-blasting modes currently supported by the --bitblast option:\n\ -\n\ -lazy (default)\n\ -+ Separate boolean structure and term reasoning betwen the core\n\ - SAT solver and the bv SAT solver\n\ -\n\ -eager\n\ -+ Bitblast eagerly to bv SAT solver\n\ -"; - -theory::bv::BitblastMode SmtOptionsHandler::stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "lazy") { - if (!options::bitvectorPropagate.wasSetByUser()) { - options::bitvectorPropagate.set(true); - } - if (!options::bitvectorEqualitySolver.wasSetByUser()) { - options::bitvectorEqualitySolver.set(true); - } - if (!options::bitvectorEqualitySlicer.wasSetByUser()) { - if (options::incrementalSolving() || - options::produceModels()) { - options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF); - } else { - options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO); - } - } - - if (!options::bitvectorInequalitySolver.wasSetByUser()) { - options::bitvectorInequalitySolver.set(true); - } - if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { - options::bitvectorAlgebraicSolver.set(true); - } - return theory::bv::BITBLAST_MODE_LAZY; - } else if(optarg == "eager") { - - if (options::incrementalSolving() && - options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ - Try --bitblast=lazy")); - } - if (!options::bitvectorToBool.wasSetByUser()) { - options::bitvectorToBool.set(true); - } - - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } - return theory::bv::BITBLAST_MODE_EAGER; - } else if(optarg == "help") { - puts(s_bitblastingModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --bitblast: `") + - optarg + "'. Try --bitblast=help."); - } -} - -const std::string SmtOptionsHandler::s_bvSlicerModeHelp = "\ -Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\ -\n\ -auto (default)\n\ -+ Turn slicer on if input has only equalities over core symbols\n\ -\n\ -on\n\ -+ Turn slicer on\n\ -\n\ -off\n\ -+ Turn slicer off\n\ -"; - -theory::bv::BvSlicerMode SmtOptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "auto") { - return theory::bv::BITVECTOR_SLICER_AUTO; - } else if(optarg == "on") { - return theory::bv::BITVECTOR_SLICER_ON; - } else if(optarg == "off") { - return theory::bv::BITVECTOR_SLICER_OFF; - } else if(optarg == "help") { - puts(s_bitblastingModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --bv-eq-slicer: `") + - optarg + "'. Try --bv-eq-slicer=help."); - } -} - -void SmtOptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) { - if(arg) { - if(options::bitblastMode.wasSetByUser()) { - if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) { - throw OptionException("bitblast-aig must be used with eager bitblaster"); - } - } else { - theory::bv::BitblastMode mode = stringToBitblastMode("", "eager"); - options::bitblastMode.set(mode); - } - if(!options::bitvectorAigSimplifications.wasSetByUser()) { - options::bitvectorAigSimplifications.set("balance;drw"); - } - } -} - - -// theory/booleans/options_handlers.h -const std::string SmtOptionsHandler::s_booleanTermConversionModeHelp = "\ -Boolean term conversion modes currently supported by the\n\ ---boolean-term-conversion-mode option:\n\ -\n\ -bitvectors [default]\n\ -+ Boolean terms are converted to bitvectors of size 1.\n\ -\n\ -datatypes\n\ -+ Boolean terms are converted to enumerations in the Datatype theory.\n\ -\n\ -native\n\ -+ Boolean terms are converted in a \"natural\" way depending on where they\n\ - are used. If in a datatype context, they are converted to an enumeration.\n\ - Elsewhere, they are converted to a bitvector of size 1.\n\ -"; - -theory::booleans::BooleanTermConversionMode SmtOptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){ - if(optarg == "bitvectors") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS; - } else if(optarg == "datatypes") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES; - } else if(optarg == "native") { - return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE; - } else if(optarg == "help") { - puts(s_booleanTermConversionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + - optarg + "'. Try --boolean-term-conversion-mode help."); - } -} - -// theory/uf/options_handlers.h -const std::string SmtOptionsHandler::s_ufssModeHelp = "\ -UF strong solver options currently supported by the --uf-ss option:\n\ -\n\ -full \n\ -+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ -\n\ -no-minimal \n\ -+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ -\n\ -none \n\ -+ Do not use uf strong solver to shrink model sizes. \n\ -\n\ -"; - -theory::uf::UfssMode SmtOptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" || optarg == "full" ) { - return theory::uf::UF_SS_FULL; - } else if(optarg == "no-minimal") { - return theory::uf::UF_SS_NO_MINIMAL; - } else if(optarg == "none") { - return theory::uf::UF_SS_NONE; - } else if(optarg == "help") { - puts(s_ufssModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --uf-ss: `") + - optarg + "'. Try --uf-ss help."); - } -} - - - -// theory/options_handlers.h -const std::string SmtOptionsHandler::s_theoryOfModeHelp = "\ -TheoryOf modes currently supported by the --theoryof-mode option:\n\ -\n\ -type (default) \n\ -+ type variables, constants and equalities by type\n\ -\n\ -term \n\ -+ type variables as uninterpreted, equalities by the parametric theory\n\ -"; - -theory::TheoryOfMode SmtOptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) { - if(optarg == "type") { - return theory::THEORY_OF_TYPE_BASED; - } else if(optarg == "term") { - return theory::THEORY_OF_TERM_BASED; - } else if(optarg == "help") { - puts(s_theoryOfModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --theoryof-mode: `") + - optarg + "'. Try --theoryof-mode help."); - } -} - -void SmtOptionsHandler::useTheory(std::string option, std::string optarg) { - if(optarg == "help") { - puts(theory::useTheoryHelp); - exit(1); - } - if(theory::useTheoryValidate(optarg)) { - std::map<std::string, bool> m = options::theoryAlternates(); - m[optarg] = true; - options::theoryAlternates.set(m); - } else { - throw OptionException(std::string("unknown option for ") + option + ": `" + - optarg + "'. Try --use-theory help."); - } -} - - - -// printer/options_handlers.h -const std::string SmtOptionsHandler::s_modelFormatHelp = "\ -Model format modes currently supported by the --model-format option:\n\ -\n\ -default \n\ -+ Print model as expressions in the output language format.\n\ -\n\ -table\n\ -+ Print functional expressions over finite domains in a table format.\n\ -"; - -const std::string SmtOptionsHandler::s_instFormatHelp = "\ -Inst format modes currently supported by the --model-format option:\n\ -\n\ -default \n\ -+ Print instantiations as a list in the output language format.\n\ -\n\ -szs\n\ -+ Print instantiations as SZS compliant proof.\n\ -"; - -ModelFormatMode SmtOptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default") { - return MODEL_FORMAT_MODE_DEFAULT; - } else if(optarg == "table") { - return MODEL_FORMAT_MODE_TABLE; - } else if(optarg == "help") { - puts(s_modelFormatHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --model-format: `") + - optarg + "'. Try --model-format help."); - } -} - -InstFormatMode SmtOptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default") { - return INST_FORMAT_MODE_DEFAULT; - } else if(optarg == "szs") { - return INST_FORMAT_MODE_SZS; - } else if(optarg == "help") { - puts(s_instFormatHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --inst-format: `") + - optarg + "'. Try --inst-format help."); - } -} - - - -// decision/options_handlers.h -const std::string SmtOptionsHandler::s_decisionModeHelp = "\ -Decision modes currently supported by the --decision option:\n\ -\n\ -internal (default)\n\ -+ Use the internal decision heuristics of the SAT solver\n\ -\n\ -justification\n\ -+ An ATGP-inspired justification heuristic\n\ -\n\ -justification-stoponly\n\ -+ Use the justification heuristic only to stop early, not for decisions\n\ -"; - -decision::DecisionMode SmtOptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) { - options::decisionStopOnly.set(false); - - if(optarg == "internal") { - return decision::DECISION_STRATEGY_INTERNAL; - } else if(optarg == "justification") { - return decision::DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "justification-stoponly") { - options::decisionStopOnly.set(true); - return decision::DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "help") { - puts(s_decisionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --decision: `") + - optarg + "'. Try --decision help."); - } -} - -decision::DecisionWeightInternal SmtOptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "off") - return decision::DECISION_WEIGHT_INTERNAL_OFF; - else if(optarg == "max") - return decision::DECISION_WEIGHT_INTERNAL_MAX; - else if(optarg == "sum") - return decision::DECISION_WEIGHT_INTERNAL_SUM; - else if(optarg == "usr1") - return decision::DECISION_WEIGHT_INTERNAL_USR1; - else - throw OptionException(std::string("--decision-weight-internal must be off, max or sum.")); -} - - - -// smt/options_handlers.h -const std::string SmtOptionsHandler::SmtOptionsHandler::s_dumpHelp = "\ -Dump modes currently supported by the --dump option:\n\ -\n\ -benchmark\n\ -+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ - does not include any declarations or assertions. Implied by all following\n\ - modes.\n\ -\n\ -declarations\n\ -+ Dump user declarations. Implied by all following modes.\n\ -\n\ -skolems\n\ -+ Dump internally-created skolem variable declarations. These can\n\ - arise from preprocessing simplifications, existential elimination,\n\ - and a number of other things. Implied by all following modes.\n\ -\n\ -assertions\n\ -+ Output the assertions after preprocessing and before clausification.\n\ - Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ - where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ - PASS can also be the special value \"everything\", in which case the\n\ - assertions are printed before any preprocessing (with\n\ - \"assertions:pre-everything\") or after all preprocessing completes\n\ - (with \"assertions:post-everything\").\n\ -\n\ -clauses\n\ -+ Do all the preprocessing outlined above, and dump the CNF-converted\n\ - output\n\ -\n\ -state\n\ -+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ - Implied by all \"stateful\" modes below and conflicts with all\n\ - non-stateful modes below.\n\ -\n\ -t-conflicts [non-stateful]\n\ -+ Output correctness queries for all theory conflicts\n\ -\n\ -missed-t-conflicts [stateful]\n\ -+ Output completeness queries for theory conflicts\n\ -\n\ -t-propagations [stateful]\n\ -+ Output correctness queries for all theory propagations\n\ -\n\ -missed-t-propagations [stateful]\n\ -+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ -\n\ -t-lemmas [non-stateful]\n\ -+ Output correctness queries for all theory lemmas\n\ -\n\ -t-explanations [non-stateful]\n\ -+ Output correctness queries for all theory explanations\n\ -\n\ -bv-rewrites [non-stateful]\n\ -+ Output correctness queries for all bitvector rewrites\n\ -\n\ -bv-abstraction [non-stateful]\n\ -+ Output correctness queries for all bv abstraction \n\ -\n\ -bv-algebraic [non-stateful]\n\ -+ Output correctness queries for bv algebraic solver. \n\ -\n\ -theory::fullcheck [non-stateful]\n \ -+ Output completeness queries for all full-check effort-level theory checks\n\ -\n\ -Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either assertions or clauses), and\n\ -perhaps one or more stateful or non-stateful modes for checking correctness\n\ -and completeness of decision procedure implementations. Stateful modes dump\n\ -the contextual assertions made by the core solver (all decisions and\n\ -propagations as assertions; that affects the validity of the resulting\n\ -correctness and completeness queries, so of course stateful and non-stateful\n\ -modes cannot be mixed in the same run.\n\ -\n\ -The --output-language option controls the language used for dumping, and\n\ -this allows you to connect CVC4 to another solver implementation via a UNIX\n\ -pipe to perform on-line checking. The --dump-to option can be used to dump\n\ -to a file.\n\ -"; - -const std::string SmtOptionsHandler::s_simplificationHelp = "\ -Simplification modes currently supported by the --simplification option:\n\ -\n\ -batch (default) \n\ -+ save up all ASSERTions; run nonclausal simplification and clausal\n\ - (MiniSat) propagation for all of them only after reaching a querying command\n\ - (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ -\n\ -none\n\ -+ do not perform nonclausal simplification\n\ -"; - -void SmtOptionsHandler::dumpMode(std::string option, std::string optarg) { -#ifdef CVC4_DUMPING - char* optargPtr = strdup(optarg.c_str()); - char* tokstr = optargPtr; - char* toksave; - while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { - tokstr = NULL; - if(!strcmp(optargPtr, "benchmark")) { - } else if(!strcmp(optargPtr, "declarations")) { - } else if(!strcmp(optargPtr, "assertions")) { - Dump.on("assertions:post-everything"); - } else if(!strncmp(optargPtr, "assertions:", 11)) { - const char* p = optargPtr + 11; - if(!strncmp(p, "pre-", 4)) { - p += 4; - } else if(!strncmp(p, "post-", 5)) { - p += 5; - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - if(!strcmp(p, "everything")) { - } else if(!strcmp(p, "definition-expansion")) { - } else if(!strcmp(p, "boolean-terms")) { - } else if(!strcmp(p, "constrain-subtypes")) { - } else if(!strcmp(p, "substitution")) { - } else if(!strcmp(p, "strings-pp")) { - } else if(!strcmp(p, "skolem-quant")) { - } else if(!strcmp(p, "simplify")) { - } else if(!strcmp(p, "static-learning")) { - } else if(!strcmp(p, "ite-removal")) { - } else if(!strcmp(p, "repeat-simplify")) { - } else if(!strcmp(p, "rewrite-apply-to-const")) { - } else if(!strcmp(p, "theory-preprocessing")) { - } else if(!strcmp(p, "nonclausal")) { - } else if(!strcmp(p, "theorypp")) { - } else if(!strcmp(p, "itesimp")) { - } else if(!strcmp(p, "unconstrained")) { - } else if(!strcmp(p, "repeatsimp")) { - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - Dump.on("assertions"); - } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "clauses")) { - } else if(!strcmp(optargPtr, "t-conflicts") || - !strcmp(optargPtr, "t-lemmas") || - !strcmp(optargPtr, "t-explanations") || - !strcmp(optargPtr, "bv-rewrites") || - !strcmp(optargPtr, "theory::fullcheck")) { - // These are "non-state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is dumped, it will interfere with the validity - // of these generated queries. - if(Dump.isOn("state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("no-permit-state"); - } - } else if(!strcmp(optargPtr, "state") || - !strcmp(optargPtr, "missed-t-conflicts") || - !strcmp(optargPtr, "t-propagations") || - !strcmp(optargPtr, "missed-t-propagations")) { - // These are "state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is not dumped, it will interfere with the - // validity of these generated queries. - if(Dump.isOn("no-permit-state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "non-state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("state"); - } - } else if(!strcmp(optargPtr, "help")) { - puts(s_dumpHelp.c_str()); - exit(1); - } else if(!strcmp(optargPtr, "bv-abstraction")) { - Dump.on("bv-abstraction"); - } else if(!strcmp(optargPtr, "bv-algebraic")) { - Dump.on("bv-algebraic"); - } else { - throw OptionException(std::string("unknown option for --dump: `") + - optargPtr + "'. Try --dump help."); - } - - Dump.on(optargPtr); - Dump.on("benchmark"); - if(strcmp(optargPtr, "benchmark")) { - Dump.on("declarations"); - if(strcmp(optargPtr, "declarations")) { - Dump.on("skolems"); - } - } - } - free(optargPtr); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - -LogicInfo* SmtOptionsHandler::stringToLogicInfo(std::string option, std::string optarg) throw(OptionException) { - try { -#warning "TODO: Fix the blatant memory leak here." - LogicInfo* logic = new LogicInfo(optarg); - if(d_smtEngine != NULL) { - d_smtEngine->setLogic(*logic); - } - return logic; - } catch(IllegalArgumentException& e) { - throw OptionException(std::string("invalid logic specification for --force-logic: `") + - optarg + "':\n" + e.what()); - } -} - -SimplificationMode SmtOptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "batch") { - return SIMPLIFICATION_MODE_BATCH; - } else if(optarg == "none") { - return SIMPLIFICATION_MODE_NONE; - } else if(optarg == "help") { - puts(s_simplificationHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --simplification: `") + - optarg + "'. Try --simplification help."); - } -} - - -void SmtOptionsHandler::beforeSearch(std::string option, bool value) throw(ModalException) { - SmtEngine::beforeSearch(d_smtEngine, option); -} - -void SmtOptionsHandler::setProduceAssertions(std::string option, bool value) throw() { - options::produceAssertions.set(value); - options::interactiveMode.set(value); -} - - -void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) { -#if !(IS_PROOFS_BUILD) - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; - throw OptionException(ss.str()); - } -#endif /* IS_PROOFS_BUILD */ -} - - -// This macro is used for setting :regular-output-channel and :diagnostic-output-channel -// to redirect a stream. It maintains all attributes set on the stream. -#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \ - { \ - int dagSetting = expr::ExprDag::getDag(__channel_get); \ - size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \ - bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ - OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \ - __channel_set; \ - __channel_get << expr::ExprDag(dagSetting); \ - __channel_get << expr::ExprSetDepth(exprDepthSetting); \ - __channel_get << expr::ExprPrintTypes(printtypesSetting); \ - __channel_get << language::SetLanguage(languageSetting); \ - } - -void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) { -#ifdef CVC4_DUMPING - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name for --dump-to")); - } else if(optarg == "-") { - outStream = &DumpOutC::dump_cout; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream)); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - -void SmtOptionsHandler::setRegularOutputChannel(std::string option, std::string optarg) { - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name setting for regular output channel")); - } else if(optarg == "stdout") { - outStream = &std::cout; - } else if(optarg == "stderr") { - outStream = &std::cerr; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); -} - -void SmtOptionsHandler::setDiagnosticOutputChannel(std::string option, std::string optarg) { - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name setting for diagnostic output channel")); - } else if(optarg == "stdout") { - outStream = &std::cout; - } else if(optarg == "stderr") { - outStream = &std::cerr; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); -} - -#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM - - - -std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) { -#ifdef CVC4_REPLAY - if(optarg == "") { - throw OptionException (std::string("Bad file name for --replay")); - } else { - return optarg; - } -#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 - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_STATISTICS_ON */ -} - -unsigned long SmtOptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException) { - unsigned long ms; - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - - // make sure the resource is set if the option is updated - // if the smt engine is null the resource will be set in the - if (d_smtEngine != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); - rm->setTimeLimit(ms, true); - } - return ms; -} - -unsigned long SmtOptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - - if (d_smtEngine != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); - rm->setTimeLimit(ms, false); - } - return ms; -} - -unsigned long SmtOptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - - if (d_smtEngine != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); - rm->setResourceLimit(ms, true); - } - return ms; -} - -unsigned long SmtOptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) { - throw OptionException("option `"+option+"` requires a number as an argument"); - } - - // TODO: Remove check? - if (d_smtEngine != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); - rm->setResourceLimit(ms, false); - } - return ms; -} - - - -// expr/options_handlers.h -void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) { - if(depth < -1) { - throw OptionException("--default-expr-depth requires a positive argument, or -1."); - } - - Debug.getStream() << expr::ExprSetDepth(depth); - Trace.getStream() << expr::ExprSetDepth(depth); - Notice.getStream() << expr::ExprSetDepth(depth); - Chat.getStream() << expr::ExprSetDepth(depth); - Message.getStream() << expr::ExprSetDepth(depth); - Warning.getStream() << expr::ExprSetDepth(depth); - // intentionally exclude Dump stream from this list -} - -void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) { - if(dag < 0) { - throw OptionException("--default-dag-thresh requires a nonnegative argument."); - } - - Debug.getStream() << expr::ExprDag(dag); - Trace.getStream() << expr::ExprDag(dag); - Notice.getStream() << expr::ExprDag(dag); - Chat.getStream() << expr::ExprDag(dag); - Message.getStream() << expr::ExprDag(dag); - Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); -} - -void SmtOptionsHandler::setPrintExprTypes(std::string option) { - Debug.getStream() << expr::ExprPrintTypes(true); - Trace.getStream() << expr::ExprPrintTypes(true); - Notice.getStream() << expr::ExprPrintTypes(true); - Chat.getStream() << expr::ExprPrintTypes(true); - Message.getStream() << expr::ExprPrintTypes(true); - Warning.getStream() << expr::ExprPrintTypes(true); - // intentionally exclude Dump stream from this list -} - - -// main/options_handlers.h -void SmtOptionsHandler::showConfiguration(std::string option) { - fputs(Configuration::about().c_str(), stdout); - printf("\n"); - printf("version : %s\n", Configuration::getVersionString().c_str()); - if(Configuration::isGitBuild()) { - const char* branchName = Configuration::getGitBranchName(); - if(*branchName == '\0') { - branchName = "-"; - } - printf("scm : git [%s %s%s]\n", - branchName, - std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), - Configuration::hasGitModifications() ? - " (with modifications)" : ""); - } else if(Configuration::isSubversionBuild()) { - printf("scm : svn [%s r%u%s]\n", - Configuration::getSubversionBranchName(), - Configuration::getSubversionRevision(), - Configuration::hasSubversionModifications() ? - " (with modifications)" : ""); - } else { - printf("scm : no\n"); - } - printf("\n"); - printf("library : %u.%u.%u\n", - Configuration::getVersionMajor(), - Configuration::getVersionMinor(), - Configuration::getVersionRelease()); - printf("\n"); - printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); - printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); - printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); - printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); - printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); - printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); - printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); - printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); - printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); - printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); - printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); - printf("\n"); - printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); - printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); - printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); - printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); - printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); - printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); - printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); - exit(0); -} - -void SmtOptionsHandler::showDebugTags(std::string option) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else if(! Configuration::isDebugBuild()) { - throw OptionException("debug tags not available in non-debug builds"); - } else { - throw OptionException("debug tags not available in non-tracing builds"); - } - exit(0); -} - -void SmtOptionsHandler::showTraceTags(std::string option) { - if(Configuration::isTracingBuild()) { - printf("available tags:"); - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for (unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - } else { - throw OptionException("trace tags not available in non-tracing build"); - } - exit(0); -} - -void SmtOptionsHandler::threadN(std::string option) { - throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); -} - - - -/* options/base_options_handlers.h */ -void SmtOptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) { - if(Configuration::isMuzzledBuild()) { - DebugChannel.setStream(CVC4::null_os); - TraceChannel.setStream(CVC4::null_os); - NoticeChannel.setStream(CVC4::null_os); - ChatChannel.setStream(CVC4::null_os); - MessageChannel.setStream(CVC4::null_os); - WarningChannel.setStream(CVC4::null_os); - } else { - if(value < 2) { - ChatChannel.setStream(CVC4::null_os); - } else { - ChatChannel.setStream(std::cout); - } - if(value < 1) { - NoticeChannel.setStream(CVC4::null_os); - } else { - NoticeChannel.setStream(std::cout); - } - if(value < 0) { - MessageChannel.setStream(CVC4::null_os); - WarningChannel.setStream(CVC4::null_os); - } else { - MessageChannel.setStream(std::cout); - WarningChannel.setStream(std::cerr); - } - } -} - -void SmtOptionsHandler::increaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() + 1); - setVerbosity(option, options::verbosity()); -} - -void SmtOptionsHandler::decreaseVerbosity(std::string option) { - options::verbosity.set(options::verbosity() - 1); - setVerbosity(option, options::verbosity()); -} - -OutputLanguage SmtOptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "help") { - options::languageHelp.set(true); - return language::output::LANG_AUTO; - } - - try { - return language::toOutputLanguage(optarg); - } catch(OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --output-language help"); - } - - Unreachable(); -} - -InputLanguage SmtOptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "help") { - options::languageHelp.set(true); - return language::input::LANG_AUTO; - } - - try { - return language::toInputLanguage(optarg); - } catch(OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help"); - } - - Unreachable(); -} - -void SmtOptionsHandler::addTraceTag(std::string option, std::string optarg) { - if(Configuration::isTracingBuild()) { - if(!Configuration::isTraceTag(optarg.c_str())) { - - if(optarg == "help") { - printf("available tags:"); - unsigned ntags = Configuration::getNumTraceTags(); - char const* const* tags = Configuration::getTraceTags(); - for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - exit(0); - } - - throw OptionException(std::string("trace tag ") + optarg + - std::string(" not available.") + - suggestTags(Configuration::getTraceTags(), optarg) ); - } - } else { - throw OptionException("trace tags not available in non-tracing builds"); - } - Trace.on(optarg); -} - -void SmtOptionsHandler::addDebugTag(std::string option, std::string optarg) { - if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { - if(!Configuration::isDebugTag(optarg.c_str()) && - !Configuration::isTraceTag(optarg.c_str())) { - - if(optarg == "help") { - printf("available tags:"); - unsigned ntags = Configuration::getNumDebugTags(); - char const* const* tags = Configuration::getDebugTags(); - for(unsigned i = 0; i < ntags; ++ i) { - printf(" %s", tags[i]); - } - printf("\n"); - exit(0); - } - - throw OptionException(std::string("debug tag ") + optarg + - std::string(" not available.") + - suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) ); - } - } else if(! Configuration::isDebugBuild()) { - throw OptionException("debug tags not available in non-debug builds"); - } else { - throw OptionException("debug tags not available in non-tracing builds"); - } - Debug.on(optarg); - Trace.on(optarg); -} - -void SmtOptionsHandler::setPrintSuccess(std::string option, bool value) { - Debug.getStream() << Command::printsuccess(value); - Trace.getStream() << Command::printsuccess(value); - Notice.getStream() << Command::printsuccess(value); - Chat.getStream() << Command::printsuccess(value); - Message.getStream() << Command::printsuccess(value); - Warning.getStream() << Command::printsuccess(value); - *options::out() << Command::printsuccess(value); -} - - -std::string SmtOptionsHandler::suggestTags(char const* const* validTags, std::string inputTag, - char const* const* additionalTags) -{ - DidYouMean didYouMean; - - const char* opt; - for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { - didYouMean.addWord(validTags[i]); - } - if(additionalTags != NULL) { - for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) { - didYouMean.addWord(additionalTags[i]); - } - } - - return didYouMean.getMatchAsString(inputTag); -} - -std::string SmtOptionsHandler::__cvc4_errno_failreason() { -#if HAVE_STRERROR_R -#if STRERROR_R_CHAR_P - if(errno != 0) { - // GNU version of strerror_r: *might* use the given buffer, - // or might not. It returns a pointer to buf, or not. - char buf[80]; - return std::string(strerror_r(errno, buf, sizeof buf)); - } else { - return "unknown reason"; - } -#else /* STRERROR_R_CHAR_P */ - if(errno != 0) { - // XSI version of strerror_r: always uses the given buffer. - // Returns an error code. - char buf[80]; - if(strerror_r(errno, buf, sizeof buf) == 0) { - return std::string(buf); - } else { - // some error occurred while getting the error string - return "unknown reason"; - } - } else { - return "unknown reason"; - } -#endif /* STRERROR_R_CHAR_P */ -#else /* HAVE_STRERROR_R */ - return "unknown reason"; -#endif /* HAVE_STRERROR_R */ -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h deleted file mode 100644 index f8e2ac155..000000000 --- a/src/smt/smt_options_handler.h +++ /dev/null @@ -1,198 +0,0 @@ -/********************* */ -/*! \file options_handler_interface.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 Interface for custom handlers and predicates options. - ** - ** Interface for custom handlers and predicates options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__SMT__SMT_OPTIONS_HANDLER_H -#define __CVC4__SMT__SMT_OPTIONS_HANDLER_H - -#include <ostream> -#include <string> - -#include "base/modal_exception.h" -#include "options/arith_heuristic_pivot_rule.h" -#include "options/arith_propagation_mode.h" -#include "options/arith_unate_lemma_mode.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/bv_bitblast_mode.h" -#include "options/decision_mode.h" -#include "options/language.h" -#include "options/option_exception.h" -#include "options/options_handler_interface.h" -#include "options/printer_modes.h" -#include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" -#include "options/theoryof_mode.h" -#include "options/ufss_mode.h" -#include "smt/smt_engine.h" -#include "theory/logic_info.h" - -namespace CVC4 { -namespace smt { - -class CVC4_PUBLIC SmtOptionsHandler : public options::OptionsHandler { -public: - SmtOptionsHandler(SmtEngine* smt); - ~SmtOptionsHandler(); - - // TODO - // theory/arith/options_handlers.h - // theory/quantifiers/options_handlers.h - // theory/bv/options_handlers.h - // theory/booleans/options_handlers.h - // theory/uf/options_handlers.h - // theory/options_handlers.h - // printer/options_handlers.h - // decision/options_handlers.h - // smt/options_handlers.h - // expr/options_handlers.h - // main/options_handlers.h - // options/base_options_handlers.h - - // theory/arith/options_handlers.h - virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException); - virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException); - virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException); - - // theory/quantifiers/options_handlers.h - virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException); - virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException); - virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException); - virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException); - virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException); - virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException); - virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); - - // theory/bv/options_handlers.h - virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException); - virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException); - virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException); - virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); - virtual void setBitblastAig(std::string option, bool arg) throw(OptionException); - - - // theory/booleans/options_handlers.h - virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); - - // theory/uf/options_handlers.h - virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException); - - // theory/options_handlers.h - virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); - virtual void useTheory(std::string option, std::string optarg); - - - // printer/options_handlers.h - virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException); - virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException); - - // decision/options_handlers.h - virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException); - virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException); - - - // smt/options_handlers.h - virtual void dumpMode(std::string option, std::string optarg); - virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException); - virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); - virtual void beforeSearch(std::string option, bool value) throw(ModalException); - virtual void setProduceAssertions(std::string option, bool value) throw(); - virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException); - virtual void dumpToFile(std::string option, std::string optarg); - 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 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); - virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException); - virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException); - - /* expr/options_handlers.h */ - virtual void setDefaultExprDepth(std::string option, int depth); - virtual void setDefaultDagThresh(std::string option, int dag); - virtual void setPrintExprTypes(std::string option); - - /* main/options_handlers.h */ - virtual void showConfiguration(std::string option); - virtual void showDebugTags(std::string option); - virtual void showTraceTags(std::string option); - virtual void threadN(std::string option); - - /* options/base_options_handlers.h */ - virtual void setVerbosity(std::string option, int value) throw(OptionException); - virtual void increaseVerbosity(std::string option); - virtual void decreaseVerbosity(std::string option); - virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException); - virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) ; - virtual void addTraceTag(std::string option, std::string optarg); - 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); - - /* Help strings */ - static const std::string s_bitblastingModeHelp; - static const std::string s_booleanTermConversionModeHelp; - static const std::string s_bvSlicerModeHelp; - static const std::string s_cegqiFairModeHelp; - static const std::string s_decisionModeHelp; - static const std::string s_dumpHelp; - static const std::string s_instFormatHelp ; - static const std::string s_instWhenHelp; - static const std::string s_iteLiftQuantHelp; - static const std::string s_literalMatchHelp; - static const std::string s_macrosQuantHelp; - static const std::string s_mbqiModeHelp; - static const std::string s_modelFormatHelp; - static const std::string s_prenexQuantModeHelp; - static const std::string s_qcfModeHelp; - static const std::string s_qcfWhenModeHelp; - static const std::string s_simplificationHelp; - static const std::string s_sygusInvTemplHelp; - static const std::string s_termDbModeHelp; - static const std::string s_theoryOfModeHelp; - static const std::string s_triggerSelModeHelp; - static const std::string s_ufssModeHelp; - static const std::string s_userPatModeHelp; - static const std::string s_errorSelectionRulesHelp; - static const std::string s_arithPropagationModeHelp; - static const std::string s_arithUnateLemmasHelp; - - -}; /* class SmtOptionsHandler */ - - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SMT_OPTIONS_HANDLER_H */ diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h new file mode 100644 index 000000000..9e0100786 --- /dev/null +++ b/src/smt/update_ostream.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file update_ostream.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-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__UPDATE_OSTREAM_H +#define __CVC4__UPDATE_OSTREAM_H + +#include <ostream> + +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "expr/expr_iomanip.h" +#include "options/language.h" +#include "options/set_language.h" +#include "options/base_options.h" +#include "smt_util/dump.h" + +namespace CVC4 { + +class ChannelSettings { + public: + ChannelSettings(std::ostream& out) + : d_dagSetting(expr::ExprDag::getDag(out)), + d_exprDepthSetting(expr::ExprSetDepth::getDepth(out)), + d_printtypesSetting(expr::ExprPrintTypes::getPrintTypes(out)), + d_languageSetting(language::SetLanguage::getLanguage(out)) + {} + + void apply(std::ostream& out) { + out << expr::ExprDag(d_dagSetting); + out << expr::ExprSetDepth(d_exprDepthSetting); + out << expr::ExprPrintTypes(d_printtypesSetting); + out << language::SetLanguage(d_languageSetting); + } + + private: + const int d_dagSetting; + const size_t d_exprDepthSetting; + const bool d_printtypesSetting; + const OutputLanguage d_languageSetting; +}; /* class ChannelSettings */ + +class OstreamUpdate { +public: + virtual std::ostream& get() = 0; + virtual void set(std::ostream* setTo) = 0; + + void apply(std::ostream* setTo) { + PrettyCheckArgument(setTo != NULL, setTo); + + ChannelSettings initialSettings(get()); + set(setTo); + initialSettings.apply(get()); + } +}; /* class OstreamUpdate */ + +class OptionsErrOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return *(options::err()); } + virtual void set(std::ostream* setTo) { return options::err.set(setTo); } +}; /* class OptionsErrOstreamUpdate */ + +class DumpOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Dump.getStream(); } + virtual void set(std::ostream* setTo) { Dump.setStream(setTo); } +}; /* class DumpOstreamUpdate */ + +class DebugOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Debug.getStream(); } + virtual void set(std::ostream* setTo) { Debug.setStream(setTo); } +}; /* class DebugOstreamUpdate */ + +class WarningOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Warning.getStream(); } + virtual void set(std::ostream* setTo) { Warning.setStream(setTo); } +}; /* class WarningOstreamUpdate */ + +class MessageOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Message.getStream(); } + virtual void set(std::ostream* setTo) { Message.setStream(setTo); } +}; /* class MessageOstreamUpdate */ + +class NoticeOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Notice.getStream(); } + virtual void set(std::ostream* setTo) { Notice.setStream(setTo); } +}; /* class NoticeOstreamUpdate */ + +class ChatOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Chat.getStream(); } + virtual void set(std::ostream* setTo) { Chat.setStream(setTo); } +}; /* class ChatOstreamUpdate */ + +class TraceOstreamUpdate : public OstreamUpdate { + public: + virtual std::ostream& get() { return Trace.getStream(); } + virtual void set(std::ostream* setTo) { Trace.setStream(setTo); } +}; /* class TraceOstreamUpdate */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__UPDATE_OSTREAM_H */ |