Listener::Listener(){}
Listener::~Listener(){}
-ListenerCollection::ListenerCollection() : d_listeners() {}
-ListenerCollection::~ListenerCollection() { Assert(empty()); }
-
-ListenerCollection::iterator ListenerCollection::addListener(Listener* listener)
-{
- return d_listeners.insert(d_listeners.end(), listener);
-}
-
-void ListenerCollection::removeListener(iterator position) {
- d_listeners.erase(position);
-}
-
-void ListenerCollection::notify() {
- for(iterator i = d_listeners.begin(), iend = d_listeners.end(); i != iend;
- ++i)
- {
- Listener* listener = *i;
- listener->notify();
- }
-}
-
-bool ListenerCollection::empty() const { return d_listeners.empty(); }
-
-
-ListenerCollection::Registration::Registration(
- ListenerCollection* collection, Listener* listener)
- : d_listener(listener)
- , d_position()
- , d_collection(collection)
-{
- d_position = d_collection->addListener(d_listener);
-}
-
-ListenerCollection::Registration::~Registration() {
- d_collection->removeListener(d_position);
- delete d_listener;
-}
-
- ListenerCollection::Registration* ListenerCollection::registerListener(
- Listener* listener)
-{
- return new Registration(this, listener);
-}
-
-
-ListenerRegistrationList::ListenerRegistrationList()
- : d_registrations()
-{}
-
-ListenerRegistrationList::~ListenerRegistrationList() {
- clear();
-}
-
-void ListenerRegistrationList::add(
- ListenerCollection::Registration* registration)
-{
- d_registrations.push_back(registration);
-}
-
-void ListenerRegistrationList::clear(){
- typedef std::list<ListenerCollection::Registration*>::iterator iterator;
- for(iterator i = d_registrations.begin(), iend = d_registrations.end();
- i != iend; ++i)
- {
- ListenerCollection::Registration* current = *i;
- delete current;
- }
- d_registrations.clear();
-}
-
}/* CVC4 namespace */
** \brief Utility classes for listeners and collections of listeners.
**
** Utilities for the development of a Listener interface class. This class
- ** provides a single notification that must be overwritten. This file also
- ** provides a utility class for a collection of listeners and an RAII style
- ** Registration class for managing the relationship between Listeners
- ** and the collection.
+ ** provides a single notification that must be overwritten.
**/
#include "cvc4_public.h"
virtual void notify() = 0;
};
-/**
- * ListenerCollection is a list of Listener instances.
- * One can add and remove Listeners.
- *
- * ListenerCollection does not own the memory of the Listeners.
- * As a sanity check, it asserted that all of its listeners
- * have been removed.
- */
-class CVC4_PUBLIC ListenerCollection {
-public:
- typedef std::list<Listener*> ListenerList;
- typedef ListenerList::iterator iterator;
-
- /** Creates an empty listener collection. */
- ListenerCollection();
-
- /**
- * Destroys an iterator collection.
- * If assertions are on, this throws an AssertionException if the collection
- * is not empty().
- */
- ~ListenerCollection();
-
- /**
- * This adds a listener to the current collection and returns
- * an iterator to the listener in the collection.
- * The user of the collection must call removeListener() using
- * this iterator.
- * The collection does not take over the memory for the listener.
- */
- iterator addListener(Listener* listener);
-
- /**
- * Remove an listener using the iterator distributed when adding the
- * listener.
- */
- void removeListener(iterator position);
-
- /** Calls notify() on all listeners in the collection. */
- void notify();
-
- /** Returns true if the collection contains no listeners. */
- bool empty() const;
-
- /**
- * Registration is an RAII utility function for using Listener
- * with ListenerCollection.
- *
- * On construction, the Registration takes a ListenerCollection,
- * collection,
- * and a Listener*, listener. It takes over the memory for listener. It then
- * adds listener to collection. On destruction it removes listener and calls
- * delete on listener.
- *
- * Because of this usage, a Registration must be destroyed before the
- * ListenerCollection it is attached to.
- */
- class CVC4_PUBLIC Registration {
- public:
- Registration(ListenerCollection* collection, Listener* listener);
- ~Registration();
-
- private:
- Listener* d_listener;
- ListenerCollection::iterator d_position;
- ListenerCollection* d_collection;
- };/* class CVC4::ListenerCollection::Registration */
-
-
- /**
- * Returns a new Registration given a Listener that is attached to this
- * ListenerCollection. Management of the memory is handed to the user of
- * this function. To remove the listener, call the destructor for the
- * Registration.
- */
- Registration* registerListener(Listener* listener);
-
-private:
-
- /**
- * Disabling the copy-constructor.
- * The user of the class must be know to remove listeners on the collection.
- * Allowing copies will only cause confusion.
- */
- ListenerCollection(const ListenerCollection& copy) = delete;
-
- /**
- * Disabling the assignment operator.
- * The user of the class must be know to remove listeners on the collection.
- * Allowing copies will only cause confusion.
- */
- ListenerCollection& operator=(const ListenerCollection& copy) = delete;
-
- /** A list of the listeners in the collection.*/
- ListenerList d_listeners;
-};/* class CVC4::ListenerCollection */
-
-/**
- * A list of ListenerCollection::Registration* pointers.
- *
- * This list assumes it has control over all of the memory of the registrations.
- */
-class ListenerRegistrationList {
- public:
- ListenerRegistrationList();
- ~ListenerRegistrationList();
-
- void add(ListenerCollection::Registration* registration);
- void clear();
-
- private:
- /** Disallow copying.*/
- ListenerRegistrationList(const ListenerRegistrationList&) = delete;
- /** Disallow assignment.*/
- ListenerRegistrationList operator=(const ListenerRegistrationList&) = delete;
- std::list<ListenerCollection::Registration*> d_registrations;
-};/* class CVC4::ListenerRegistrationList */
-
}/* CVC4 namespace */
#endif /* CVC4__LISTENER_H */
category = "regular"
long = "print-success"
type = "bool"
- notifies = ["notifyPrintSuccess"]
read_only = true
help = "print the \"success\" output required of SMT-LIBv2"
type = "int"
default = "0"
predicates = ["setDefaultExprDepthPredicate"]
- notifies = ["notifySetDefaultExprDepth"]
read_only = true
help = "print exprs to depth N (0 == default, -1 == no limit)"
type = "int"
default = "1"
predicates = ["setDefaultDagThreshPredicate"]
- notifies = ["notifySetDefaultDagThresh"]
read_only = true
help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
long = "print-expr-types"
type = "bool"
default = "false"
- notifies = ["notifySetPrintExprTypes"]
read_only = true
help = "print types with variables when printing exprs"
/** The current Options in effect */
static thread_local Options* s_current;
- /** Listeners for notifyBeforeSearch. */
- ListenerCollection d_beforeSearchListeners;
-
- /** Listeners for options::defaultExprDepth. */
- ListenerCollection d_setDefaultExprDepthListeners;
-
- /** Listeners for options::defaultDagThresh. */
- ListenerCollection d_setDefaultDagThreshListeners;
-
- /** Listeners for options::printExprTypes. */
- ListenerCollection d_setPrintExprTypesListeners;
-
- /** Listeners for options::dumpModeString. */
- ListenerCollection d_setDumpModeListeners;
-
- /** Listeners for options::printSuccess. */
- ListenerCollection d_setPrintSuccessListeners;
-
- /** Listeners for options::dumpToFileName. */
- ListenerCollection d_dumpToFileListeners;
-
- /** Listeners for options::regularChannelName. */
- ListenerCollection d_setRegularChannelListeners;
-
- /** Listeners for options::diagnosticChannelName. */
- ListenerCollection d_setDiagnosticChannelListeners;
-
- static ListenerCollection::Registration* registerAndNotify(
- ListenerCollection& collection, Listener* listener, bool notify);
-
/** Low-level assignment function for options */
template <class T>
void assign(T, std::string option, std::string value);
/** Set the generic listener associated with this class to ol */
void setListener(OptionsListener* ol);
- /**
- * Registers a listener for the notification, notifyBeforeSearch.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- *
- * This has multiple usages so having a notifyIfSet flag does not add
- * clarity. Users should check the relevant flags before registering this.
- */
- ListenerCollection::Registration* registerBeforeSearchListener(
- Listener* listener);
-
- /**
- * Registers a listener for options::defaultExprDepth being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetDefaultExprDepthListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::defaultDagThresh being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetDefaultExprDagListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::printExprTypes being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetPrintExprTypesListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::dumpModeString being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetDumpModeListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::printSuccess being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetPrintSuccessListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::dumpToFileName being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerDumpToFileNameListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::regularChannelName being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetRegularOutputChannelListener(
- Listener* listener, bool notifyIfSet);
-
- /**
- * Registers a listener for options::diagnosticChannelName being set.
- *
- * If notifyIfSet is true, this calls notify on the listener
- * if the option was set by the user.
- *
- * The memory for the Registration is controlled by the user and must
- * be destroyed before the Options object is.
- */
- ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener(
- Listener* listener, bool notifyIfSet);
/** Sends a std::flush to getErr(). */
void flushErr();
OptionsHandler::OptionsHandler(Options* options) : d_options(options) { }
-void OptionsHandler::notifyBeforeSearch(const std::string& option)
-{
- try{
- d_options->d_beforeSearchListeners.notify();
- } catch (ModalException&){
- std::stringstream ss;
- ss << "cannot change option `" << option << "' after final initialization";
- throw ModalException(ss.str());
- }
-}
-
unsigned long OptionsHandler::limitHandler(std::string option,
std::string optarg)
{
}
return ms;
}
-
-/* options/base_options_handlers.h */
-void OptionsHandler::notifyPrintSuccess(std::string option) {
- d_options->d_setPrintSuccessListeners.notify();
-}
-
// theory/quantifiers/options_handlers.h
void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
#endif /* CVC4_USE_LFSC */
}
-void OptionsHandler::notifyDumpToFile(std::string option) {
- d_options->d_dumpToFileListeners.notify();
-}
-
-
-void OptionsHandler::notifySetRegularOutputChannel(std::string option) {
- d_options->d_setRegularChannelListeners.notify();
-}
-
-void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) {
- d_options->d_setDiagnosticChannelListeners.notify();
-}
-
void OptionsHandler::statsEnabledBuild(std::string option, bool value)
{
#ifndef CVC4_STATISTICS_ON
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\"");
}
-void OptionsHandler::notifyDumpMode(std::string option)
-{
- d_options->d_setDumpModeListeners.notify();
-}
-
-
// expr/options_handlers.h
void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
if(depth < -1) {
}
}
-void OptionsHandler::notifySetDefaultExprDepth(std::string option) {
- d_options->d_setDefaultExprDepthListeners.notify();
-}
-
-void OptionsHandler::notifySetDefaultDagThresh(std::string option) {
- d_options->d_setDefaultDagThreshListeners.notify();
-}
-
-void OptionsHandler::notifySetPrintExprTypes(std::string option) {
- d_options->d_setPrintExprTypesListeners.notify();
-}
-
-
// main/options_handlers.h
static void print_config (const char * str, std::string config) {
* Throws a ModalException if this option is being set after final
* initialization.
*/
- void notifyBeforeSearch(const std::string& option);
- void notifyDumpMode(std::string option);
void setProduceAssertions(std::string option, bool value);
void proofEnabledBuild(std::string option, bool value);
void LFSCEnabledBuild(std::string option, bool value);
- void notifyDumpToFile(std::string option);
- void notifySetRegularOutputChannel(std::string option);
- void notifySetDiagnosticOutputChannel(std::string option);
void statsEnabledBuild(std::string option, bool value);
/* expr/options_handlers.h */
void setDefaultExprDepthPredicate(std::string option, int depth);
void setDefaultDagThreshPredicate(std::string option, int dag);
- void notifySetDefaultExprDepth(std::string option);
- void notifySetDefaultDagThresh(std::string option);
- void notifySetPrintExprTypes(std::string option);
/* main/options_handlers.h */
void copyright(std::string option);
InputLanguage stringToInputLanguage(std::string option, std::string optarg);
void enableTraceTag(std::string option, std::string optarg);
void enableDebugTag(std::string option, std::string optarg);
- void notifyPrintSuccess(std::string option);
private:
// that can throw exceptions.
}
-
Options::Options(OptionsListener* ol)
- : d_holder(new options::OptionsHolder())
- , d_handler(new options::OptionsHandler(this))
- , d_beforeSearchListeners(),
- d_olisten(ol)
+ : d_holder(new options::OptionsHolder()),
+ d_handler(new options::OptionsHandler(this)),
+ d_olisten(ol)
{}
Options::~Options() {
void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
-ListenerCollection::Registration* Options::registerAndNotify(
- ListenerCollection& collection, Listener* listener, bool notify)
-{
- ListenerCollection::Registration* registration =
- collection.registerListener(listener);
- if(notify) {
- try
- {
- listener->notify();
- }
- catch (OptionException& e)
- {
- // It can happen that listener->notify() throws an OptionException. In
- // that case, we have to make sure that we delete the registration of our
- // listener before rethrowing the exception. Otherwise the
- // ListenerCollection deconstructor will complain that not all
- // registrations have been removed before invoking the deconstructor.
- delete registration;
- throw OptionException(e.getRawMessage());
- }
- }
- return registration;
-}
-
-ListenerCollection::Registration* Options::registerBeforeSearchListener(
- Listener* listener)
-{
- return d_beforeSearchListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::defaultExprDepth);
- return registerAndNotify(d_setDefaultExprDepthListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDefaultExprDagListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::defaultDagThresh);
- return registerAndNotify(d_setDefaultDagThreshListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintExprTypesListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::printExprTypes);
- return registerAndNotify(d_setPrintExprTypesListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetDumpModeListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::dumpModeString);
- return registerAndNotify(d_setDumpModeListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerSetPrintSuccessListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::printSuccess);
- return registerAndNotify(d_setPrintSuccessListeners, listener, notify);
-}
-
-ListenerCollection::Registration* Options::registerDumpToFileNameListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::dumpToFileName);
- return registerAndNotify(d_dumpToFileListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetRegularOutputChannelListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::regularChannelName);
- return registerAndNotify(d_setRegularChannelListeners, listener, notify);
-}
-
-ListenerCollection::Registration*
-Options::registerSetDiagnosticOutputChannelListener(
- Listener* listener, bool notifyIfSet)
-{
- bool notify = notifyIfSet && wasSetByUser(options::diagnosticChannelName);
- return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify);
-}
-
${custom_handlers}$
#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
}
options->d_holder->binary_name = std::string(progName);
-
std::vector<std::string> nonoptions;
parseOptionsRecursive(options, argc, argv, &nonoptions);
if(Debug.isOn("options")){
std::string Options::getOption(const std::string& key) const
{
- Trace("options") << "SMT getOption(" << key << ")" << std::endl;
-
+ Trace("options") << "Options::getOption(" << key << ")" << std::endl;
${getoption_handlers}$
-
throw UnrecognizedOptionException(key);
}
category = "common"
long = "dump=MODE"
type = "std::string"
- notifies = ["notifyDumpMode"]
read_only = true
help = "dump preprocessed assertions, etc., see --dump=help"
category = "common"
long = "dump-to=FILE"
type = "std::string"
- notifies = ["notifyDumpToFile"]
read_only = true
help = "all dumping goes to FILE (instead of stdout)"
long = "produce-models"
type = "bool"
default = "false"
- notifies = ["notifyBeforeSearch"]
help = "support the get-value and get-model commands"
[[option]]
category = "regular"
long = "check-models"
type = "bool"
- notifies = ["notifyBeforeSearch"]
help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
[[option]]
category = "regular"
long = "debug-check-models"
type = "bool"
- notifies = ["notifyBeforeSearch"]
help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
[[option]]
type = "bool"
default = "false"
predicates = ["proofEnabledBuild"]
- notifies = ["notifyBeforeSearch"]
help = "turn on proof generation"
[[option]]
long = "check-proofs"
type = "bool"
predicates = ["LFSCEnabledBuild"]
- notifies = ["notifyBeforeSearch"]
help = "after UNSAT/VALID, machine-check the generated proof"
[[option]]
long = "produce-unsat-cores"
type = "bool"
predicates = ["proofEnabledBuild"]
- notifies = ["notifyBeforeSearch"]
help = "turn on unsat core generation"
[[option]]
long = "dump-unsat-cores"
type = "bool"
default = "false"
- notifies = ["notifyBeforeSearch"]
help = "output unsat cores after every UNSAT/VALID response"
[[option]]
long = "dump-unsat-cores-full"
type = "bool"
default = "false"
- notifies = ["notifyBeforeSearch"]
read_only = true
help = "dump the full unsat core, including unlabeled assertions"
type = "bool"
default = "false"
predicates = ["proofEnabledBuild"]
- notifies = ["notifyBeforeSearch"]
read_only = true
help = "turn on unsat assumptions generation"
long = "produce-assignments"
type = "bool"
default = "false"
- notifies = ["notifyBeforeSearch"]
help = "support the get-assignment command"
[[option]]
category = "undocumented"
type = "bool"
predicates = ["setProduceAssertions"]
- notifies = ["notifyBeforeSearch"]
help = "deprecated name for produce-assertions"
[[option]]
long = "produce-assertions"
type = "bool"
predicates = ["setProduceAssertions"]
- notifies = ["notifyBeforeSearch"]
help = "keep an assertions list (enables get-assertions command)"
[[option]]
smt_name = "regular-output-channel"
category = "regular"
type = "std::string"
- notifies = ["notifySetRegularOutputChannel"]
read_only = true
help = "set the regular output channel of the solver"
smt_name = "diagnostic-output-channel"
category = "regular"
type = "std::string"
- notifies = ["notifySetDiagnosticOutputChannel"]
read_only = true
help = "set the diagnostic output channel of the solver"
std::ostream* d_managed;
}; /* class ManagedOstream */
-class SetToDefaultSourceListener : public Listener {
- public:
- SetToDefaultSourceListener(ManagedOstream* managedOstream)
- : d_managedOstream(managedOstream){}
-
- void notify() override
- {
- 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
{
notifySetOption(options::printSuccess.getName());
}
+ if (opts->wasSetByUser(options::diagnosticChannelName))
+ {
+ notifySetOption(options::diagnosticChannelName.getName());
+ }
+ if (opts->wasSetByUser(options::regularChannelName))
+ {
+ notifySetOption(options::regularChannelName.getName());
+ }
+ if (opts->wasSetByUser(options::dumpToFileName))
+ {
+ notifySetOption(options::dumpToFileName.getName());
+ }
// set this as a listener to be notified of options changes from now on
opts->setListener(this);
}
Warning.getStream() << Command::printsuccess(value);
*options::out() << Command::printsuccess(value);
}
+ else if (key == options::regularChannelName.getName())
+ {
+ d_managedRegularChannel.set(options::regularChannelName());
+ }
+ else if (key == options::diagnosticChannelName.getName())
+ {
+ d_managedDiagnosticChannel.set(options::diagnosticChannelName());
+ }
+ else if (key == options::dumpToFileName.getName())
+ {
+ d_managedDumpChannel.set(options::dumpToFileName());
+ }
// otherwise, no action is necessary
}
#include "options/options.h"
#include "options/options_listener.h"
+#include "smt/managed_ostreams.h"
namespace CVC4 {
Options* d_options;
/** Pointer to the resource manager */
ResourceManager* d_resourceManager;
+ /** 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;
};
} // namespace smt
* updated by this method based on the current options and the logic itself.
* @param isInternalSubsolver Whether we are setting the options for an
* internal subsolver (see SmtEngine::isInternalSubsolver).
- *
+ *
* NOTE: we currently modify the current options in scope. This method
* can be further refactored to modify an options object provided as an
* explicit argument.
#include "proof/theory_proof.h"
#include "proof/unsat_core.h"
#include "prop/prop_engine.h"
-#include "smt/abstract_values.h"
#include "smt/abduction_solver.h"
+#include "smt/abstract_values.h"
#include "smt/command.h"
#include "smt/command_list.h"
#include "smt/defined_function.h"
#include "smt/logic_request.h"
-#include "smt/managed_ostreams.h"
#include "smt/model_blocker.h"
#include "smt/model_core_builder.h"
+#include "smt/options_manager.h"
#include "smt/process_assertions.h"
-#include "smt/set_defaults.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_engine_stats.h"
#include "smt/term_formula_removal.h"
SmtEngine* d_smt;
}; /* class ResourceOutListener */
-class BeforeSearchListener : public Listener {
- public:
- BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
- void notify() override { d_smt->beforeSearch(); }
-
- private:
- SmtEngine* d_smt;
-}; /* class BeforeSearchListener */
-
-class SetDefaultExprDepthListener : public Listener {
- public:
- void notify() override
- {
- 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:
- void notify() override
- {
- 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:
- void notify() override
- {
- 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:
- void notify() override
- {
- const std::string& value = options::dumpModeString();
- Dump.setDumpFromString(value);
- }
-};
-
-class PrintSuccessListener : public Listener {
- public:
- void notify() override
- {
- 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.
* The point of this is to separate the public and private portions of
typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
- /** 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;
-
/**
- * This list contains:
- * softResourceOut
- * hardResourceOut
- * beforeSearchListener
- *
- * This needs to be deleted before both NodeManager's Options,
- * SmtEngine, d_resourceManager, and TheoryEngine.
+ * Manager for limiting time and abstract resource usage.
*/
- ListenerRegistrationList* d_listenerRegistrations;
+ ResourceManager* d_resourceManager;
+
+ /** Resource out listener */
+ std::unique_ptr<ResourceOutListener> d_routListener;
/** A circuit propagator for non-clausal propositional deduction */
booleans::CircuitPropagator d_propagator;
public:
SmtEnginePrivate(SmtEngine& smt)
: d_smt(smt),
- d_managedRegularChannel(),
- d_managedDiagnosticChannel(),
- d_managedDumpChannel(),
- d_listenerRegistrations(new ListenerRegistrationList()),
+ d_routListener(new ResourceOutListener(d_smt)),
d_propagator(true, true),
d_assertions(),
d_assertionsProcessed(smt.getUserContext(), false),
d_processor(smt, *smt.getResourceManager()),
- // d_needsExpandDefs(true), //TODO?
d_exprNames(smt.getUserContext()),
d_iteRemover(smt.getUserContext()),
d_sygusConjectureStale(smt.getUserContext(), true)
d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
ResourceManager* rm = d_smt.getResourceManager();
-
- d_listenerRegistrations->add(
- rm->registerListener(new ResourceOutListener(d_smt)));
-
- try
- {
- Options& opts = d_smt.getOptions();
- // 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(
- opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt)));
-
- // These do need registration calls.
- d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener(
- new SetDefaultExprDepthListener(), true));
- d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener(
- new SetDefaultExprDagListener(), true));
- d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener(
- new SetPrintExprTypesListener(), true));
- d_listenerRegistrations->add(
- opts.registerSetDumpModeListener(new DumpModeListener(), true));
- d_listenerRegistrations->add(opts.registerSetPrintSuccessListener(
- new PrintSuccessListener(), true));
- d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener(
- new SetToDefaultSourceListener(&d_managedRegularChannel), true));
- d_listenerRegistrations->add(
- opts.registerSetDiagnosticOutputChannelListener(
- new SetToDefaultSourceListener(&d_managedDiagnosticChannel),
- true));
- d_listenerRegistrations->add(opts.registerDumpToFileNameListener(
- new SetToDefaultSourceListener(&d_managedDumpChannel), true));
- }
- catch (OptionException& e)
- {
- // Registering the option listeners can lead to OptionExceptions, e.g.
- // when the user chooses a dump tag that does not exist. In that case, we
- // have to make sure that we delete existing listener registrations and
- // that we unsubscribe from NodeManager events. Otherwise we will have
- // errors in the deconstructors of the NodeManager (because the
- // NodeManager tries to notify an SmtEnginePrivate that does not exist)
- // and the ListenerCollection (because not all registrations have been
- // removed before calling the deconstructor).
- delete d_listenerRegistrations;
- d_smt.d_nodeManager->unsubscribeEvents(this);
- throw OptionException(e.getRawMessage());
- }
+ rm->registerListener(d_routListener.get());
}
~SmtEnginePrivate()
{
- delete d_listenerRegistrations;
-
if(d_propagator.getNeedsFinish()) {
d_propagator.finish();
d_propagator.setNeedsFinish(false);
d_statisticsRegistry.reset(new StatisticsRegistry());
d_resourceManager.reset(
new ResourceManager(*d_statisticsRegistry.get(), d_options));
+ d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
d_private.reset(new smt::SmtEnginePrivate(*this));
d_stats.reset(new SmtEngineStatistics());
// parsing smt2, this occurs at the moment we enter "Assert mode", page 52
// of SMT-LIB 2.6 standard.
- // Inialize the resource manager based on the options.
- if (options::perCallResourceLimit() != 0)
- {
- d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
- }
- if (options::cumulativeResourceLimit() != 0)
- {
- d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
- true);
- }
- if (options::perCallMillisecondLimit() != 0)
- {
- d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
- }
-
// set the random seed
Random::getRandom().setSeed(options::seed());
- // ensure that our heuristics are properly set up
- setDefaults(d_logic, d_isInternalSubsolver);
-
+ // Call finish init on the options manager. This inializes the resource
+ // manager based on the options, and sets up the best default options
+ // based on our heuristics.
+ d_optm->finishInit(d_logic, d_isInternalSubsolver);
+
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
d_stats.reset(nullptr);
d_private.reset(nullptr);
+ d_optm.reset(nullptr);
// d_resourceManager must be destroyed before d_statisticsRegistry
d_resourceManager.reset(nullptr);
d_statisticsRegistry.reset(nullptr);
}
}
-void SmtEngine::beforeSearch()
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
{
+ // Always check whether the SmtEngine has been initialized (which is done
+ // upon entering Assert mode the first time). No option can be set after
+ // initialized.
if(d_fullyInited) {
- throw ModalException(
- "SmtEngine::beforeSearch called after initialization.");
+ throw ModalException("SmtEngine::setOption called after initialization.");
}
-}
-
-
-void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
-{
NodeManagerScope nms(d_nodeManager);
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
namespace smt {
/** Utilities */
class AbstractValues;
+class OptionsManager;
/** Subsolvers */
class AbductionSolver;
/**
/** Set print function in model. */
void setPrintFuncInModel(Expr f, bool p);
- /**
- * Check and throw a ModalException if the SmtEngine has been fully
- * initialized.
- *
- * throw@ ModalException
- */
- void beforeSearch();
-
/**
* Get expression name.
*
* Manager for limiting time and abstract resource usage.
*/
std::unique_ptr<ResourceManager> d_resourceManager;
+ /**
+ * The options manager, which is responsible for implementing core options
+ * such as those related to time outs and printing. It is also responsible
+ * for set default options based on the logic.
+ */
+ std::unique_ptr<smt::OptionsManager> d_optm;
/**
* The global scope object. Upon creation of this SmtEngine, it becomes the
* SmtEngine in scope. It says the SmtEngine in scope until it is destructed,
d_thisCallResourceUsed(0),
d_thisCallResourceBudget(0),
d_on(false),
- d_listeners(),
d_statistics(new ResourceManager::Statistics(stats)),
d_options(options)
<< d_perCallTimer.elapsed() << std::endl;
}
- d_listeners.notify();
+ for (Listener* l : d_listeners)
+ {
+ l->notify();
+ }
}
}
d_on = on;
}
-ListenerCollection::Registration* ResourceManager::registerListener(
- Listener* listener)
+void ResourceManager::registerListener(Listener* listener)
{
- return d_listeners.registerListener(listener);
+ return d_listeners.push_back(listener);
}
} /* namespace CVC4 */
static uint64_t getFrequencyCount() { return s_resourceCount; }
/**
- * Registers a listener that is notified on a resource out.
- *
- * This Registration must be destroyed by the user before this
- * ResourceManager.
+ * Registers a listener that is notified on a resource out or (per-call)
+ * timeout.
*/
- ListenerCollection::Registration* registerListener(Listener* listener);
+ void registerListener(Listener* listener);
private:
/** The per-call wall clock timer. */
static const uint64_t s_resourceCount;
/** Receives a notification on reaching a limit. */
- ListenerCollection d_listeners;
+ std::vector<Listener*> d_listeners;
void spendResource(unsigned amount);
cvc4_add_unit_test_black(exception_black util)
cvc4_add_unit_test_black(integer_black util)
cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(listener_black util)
cvc4_add_unit_test_black(output_black util)
cvc4_add_unit_test_black(rational_black util)
cvc4_add_unit_test_white(rational_white util)
+++ /dev/null
-/********************* */
-/*! \file listener_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Andres Noetzli, Paul Meng
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4 output classes.
- **
- ** Black box testing of CVC4 output classes.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "base/listener.h"
-
-using namespace CVC4;
-using namespace std;
-
-class ListenerBlack : public CxxTest::TestSuite {
-
- std::multiset<std::string> d_events;
-
- class EventListener : public Listener {
- public:
- EventListener(std::multiset<std::string>& events, std::string name)
- : d_events(events), d_name(name) {}
- ~EventListener() override {}
-
- void notify() override { d_events.insert(d_name); }
-
- private:
- std::multiset<std::string>& d_events;
- std::string d_name;
- };
-
-public:
-
- static std::multiset<std::string> mkMultiset(std::string arr[], int len){
- return std::multiset<std::string>(arr, arr + len);
- }
-
- void setUp() override { d_events.clear(); }
-
- void tearDown() override { d_events.clear(); }
-
- void testEmptyCollection() {
- // Makes an new collection and tests that it is empty.
- ListenerCollection* collection = new ListenerCollection;
- TS_ASSERT(collection->empty());
- TS_ASSERT_THROWS_NOTHING( delete collection );
- }
-
- void testSingletonCollection() {
- ListenerCollection collection;
- std::string expected[1] = {"a"};
- {
- ListenerCollection::Registration a(&collection, new EventListener(d_events, "a"));
- collection.notify();
- TS_ASSERT(not collection.empty());
- }
- TS_ASSERT(collection.empty());
- TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 1));
- }
-
- void testSingleRegisterTearDown() {
- // Tests that collection succeeds at destruction after
- // registering a single event.
- ListenerCollection* collection = new ListenerCollection;
- {
- ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
- TS_ASSERT(not collection->empty());
- // The destructor for a now runs.
- }
- TS_ASSERT(collection->empty());
- TS_ASSERT_THROWS_NOTHING( delete collection );
- }
-
- void testMultipleCollection() {
- ListenerCollection* collection = new ListenerCollection;
- {
- ListenerCollection::Registration c(collection, new EventListener(d_events, "c"));
- collection->notify();
- // d_events == {"c"}
- ListenerCollection::Registration b(collection, new EventListener(d_events, "b"));
- ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
- collection->notify();
- // d_events == {"a", "b", "c", "c"}
- TS_ASSERT(not collection->empty());
- }
- TS_ASSERT(collection->empty());
- std::string expected[4] = {"a", "b", "c", "c"};
- TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 4));
- TS_ASSERT_THROWS_NOTHING( delete collection );
- }
-
- void testRegisterMiddleTearDown() {
- // Tests that collection succeeds at destruction after
- // registering several events.
- ListenerCollection* collection = new ListenerCollection;
- {
- ListenerCollection::Registration a(collection, new EventListener(d_events, "a"));
- ListenerCollection::Registration* b =
- new ListenerCollection::Registration(collection, new EventListener(d_events, "b"));
- ListenerCollection::Registration c(collection, new EventListener(d_events, "c"));
-
- collection->notify();
- delete b;
- collection->notify();
- // The destructor for a and c now run.
- TS_ASSERT(not collection->empty());
- }
- TS_ASSERT(collection->empty());
- TS_ASSERT_THROWS_NOTHING( delete collection );
- }
-
-
-
- void testRegisterMultiple() {
- // This tests adds and notify multiple times.
- ListenerCollection collection;
-
- std::vector<ListenerCollection::Registration*> listeners;
- for(int i = 0; i < 4 ; ++i){
- stringstream ss; ss << i;
- Listener* listener = new EventListener(d_events, ss.str());
- listeners.push_back(new ListenerCollection::Registration(&collection, listener));
- collection.notify();
- }
-
- TS_ASSERT(not collection.empty());
- for(unsigned i=0; i < listeners.size(); ++i){
- ListenerCollection::Registration* at_i = listeners[i];
- delete at_i;
- }
- listeners.clear();
- TS_ASSERT(collection.empty());
-
- std::string expected[10] =
- {"0", "0", "0", "0", "1", "1", "1", "2", "2", "3"};
- TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10));
-
- // No more events occur.
- collection.notify();
- TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10));
- }
-
-};
projects / cvc5.git / commitdiff