diff options
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 34 |
1 files changed, 23 insertions, 11 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index be31d768b..c94646c40 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -22,22 +22,22 @@ #include <string> #include <vector> -#include "context/cdlist_forward.h" +#include "base/modal_exception.h" #include "context/cdhashmap_forward.h" #include "context/cdhashset_forward.h" +#include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "util/proof.h" -#include "util/unsat_core.h" -#include "smt/modal_exception.h" -#include "smt/logic_exception.h" +#include "expr/result.h" +#include "expr/sexpr.h" +#include "expr/statistics.h" #include "options/options.h" -#include "util/result.h" -#include "util/sexpr.h" +#include "proof/unsat_core.h" +#include "smt/logic_exception.h" +#include "theory/logic_info.h" #include "util/hash.h" +#include "util/proof.h" #include "util/unsafe_interrupt_exception.h" -#include "util/statistics.h" -#include "theory/logic_info.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -72,6 +72,10 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ +namespace options { + class OptionsHandler; +}/* CVC4::prop namespace */ + namespace expr { namespace attr { class AttributeManager; @@ -93,7 +97,6 @@ namespace smt { class SmtScope; class BooleanTermConverter; - void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); ProofManager* currentProofManager(); struct CommandCleanup; @@ -264,6 +267,11 @@ class CVC4_PUBLIC SmtEngine { std::map<std::string, Integer> d_commandVerbosity; /** + * This responds to requests to set options. + */ + options::OptionsHandler* d_optionsHandler; + + /** * A private utility class to SmtEngine. */ smt::SmtEnginePrivate* d_private; @@ -354,7 +362,6 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); - friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; // to access d_modelCommands @@ -717,6 +724,11 @@ public: */ void setPrintFuncInModel(Expr f, bool p); + + /** + * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized. + */ + static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException); };/* class SmtEngine */ }/* CVC4 namespace */ |