diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 114 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 74 |
2 files changed, 103 insertions, 85 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c8d5e04a..11c226ee4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -647,10 +647,9 @@ public: * * Returns false if the formula simplifies to "false" */ - bool simplifyAssertions() throw(TypeCheckingException, LogicException, - UnsafeInterruptException); + bool simplifyAssertions(); -public: + public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), @@ -732,7 +731,8 @@ public: new SetToDefaultSourceListener(&d_managedReplayLog), true)); } - ~SmtEnginePrivate() throw() { + ~SmtEnginePrivate() + { delete d_listenerRegistrations; if(d_propagatorNeedsFinish) { @@ -743,7 +743,8 @@ public: } ResourceManager* getResourceManager() { return d_resourceManager; } - void spendResource(unsigned amount) throw(UnsafeInterruptException) { + void spendResource(unsigned amount) + { d_resourceManager->spendResource(amount); } @@ -840,13 +841,12 @@ public: * even be simplified. * the 2nd and 3rd arguments added for bookkeeping for proofs */ - void addFormula(TNode n, bool inUnsatCore, bool inInput = true) - throw(TypeCheckingException, LogicException); + void addFormula(TNode n, bool inUnsatCore, bool inInput = true); /** Expand definitions in n. */ - Node expandDefinitions(TNode n, NodeToNodeHashMap& cache, - bool expandOnly = false) - throw(TypeCheckingException, LogicException, UnsafeInterruptException); + Node expandDefinitions(TNode n, + NodeToNodeHashMap& cache, + bool expandOnly = false); /** * Simplify node "in" by expanding definitions and applying any @@ -983,7 +983,7 @@ public: }/* namespace CVC4::smt */ -SmtEngine::SmtEngine(ExprManager* em) throw() +SmtEngine::SmtEngine(ExprManager* em) : d_context(new Context()), d_userLevels(), d_userContext(new UserContext()), @@ -1176,7 +1176,8 @@ void SmtEngine::shutdown() { } } -SmtEngine::~SmtEngine() throw() { +SmtEngine::~SmtEngine() +{ SmtScope smts(this); try { @@ -1248,7 +1249,8 @@ SmtEngine::~SmtEngine() throw() { } } -void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { +void SmtEngine::setLogic(const LogicInfo& logic) +{ SmtScope smts(this); if(d_fullyInited) { throw ModalException("Cannot set logic in SmtEngine after the engine has " @@ -1259,7 +1261,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { } void SmtEngine::setLogic(const std::string& s) - throw(ModalException, LogicException) { +{ SmtScope smts(this); try { setLogic(LogicInfo(s)); @@ -1268,16 +1270,12 @@ void SmtEngine::setLogic(const std::string& s) } } -void SmtEngine::setLogic(const char* logic) - throw(ModalException, LogicException) { - setLogic(string(logic)); -} - +void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { return d_logic; } - -void SmtEngine::setLogicInternal() throw() { +void SmtEngine::setLogicInternal() +{ Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already" " finished initializing for this run"); d_logic.lock(); @@ -2124,8 +2122,7 @@ void SmtEngine::setDefaults() { } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException) { - +{ SmtScope smts(this); Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; @@ -2494,8 +2491,7 @@ void SmtEnginePrivate::finishInit() { } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) - throw(TypeCheckingException, LogicException, UnsafeInterruptException) { - +{ stack< triple<Node, Node, bool> > worklist; stack<Node> result; worklist.push(make_triple(Node(n), Node(n), false)); @@ -3877,7 +3873,7 @@ void SmtEnginePrivate::doMiplibTrick() { // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() - throw(TypeCheckingException, LogicException, UnsafeInterruptException) { +{ spendResource(options::preprocessStep()); Assert(d_smt.d_pendingPops == 0); try { @@ -4618,8 +4614,7 @@ void SmtEnginePrivate::processAssertions() { } void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) - throw(TypeCheckingException, LogicException) { - +{ if (n == d_true) { // nothing to do return; @@ -4652,7 +4647,8 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) //d_assertions.push_back(Rewriter::rewrite(n)); } -void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { +void SmtEngine::ensureBoolean(const Expr& e) +{ Type type = e.getType(options::typeChecking()); Type boolType = d_exprManager->booleanType(); if(type != boolType) { @@ -4664,11 +4660,13 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(Exception) { +Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) +{ return checkSatisfiability(ex, inUnsatCore, false); } /* SmtEngine::checkSat() */ -Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(Exception) { +Result SmtEngine::query(const Expr& ex, bool inUnsatCore) +{ Assert(!ex.isNull()); return checkSatisfiability(ex, inUnsatCore, true); } /* SmtEngine::query() */ @@ -4808,7 +4806,8 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ } } -Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { +Result SmtEngine::checkSynth(const Expr& e) +{ SmtScope smts(this); Trace("smt") << "Check synth: " << e << std::endl; Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl; @@ -4933,7 +4932,8 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { return checkSatisfiability( e_check, true, false ); } -Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { +Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) +{ Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -4960,7 +4960,8 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { return node; } -Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { +Expr SmtEngine::simplify(const Expr& ex) +{ Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); finalOptionsAreSet(); @@ -4983,7 +4984,8 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep return n.toExpr(); } -Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { +Expr SmtEngine::expandDefinitions(const Expr& ex) +{ d_private->spendResource(options::preprocessStep()); Assert(ex.getExprManager() == d_exprManager); @@ -5009,7 +5011,8 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L } // TODO(#1108): Simplify the error reporting of this method. -Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) { +Expr SmtEngine::getValue(const Expr& ex) const +{ Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -5558,8 +5561,8 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } -Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, - bool strict) throw(Exception) { +Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) +{ SmtScope smts(this); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; @@ -5682,7 +5685,8 @@ vector<Expr> SmtEngine::getAssertions() { return vector<Expr>(d_assertionList->begin(), d_assertionList->end()); } -void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptException) { +void SmtEngine::push() +{ SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -5792,7 +5796,8 @@ void SmtEngine::doPendingPops() { } } -void SmtEngine::reset() throw() { +void SmtEngine::reset() +{ SmtScope smts(this); ExprManager *em = d_exprManager; Trace("smt") << "SMT reset()" << endl; @@ -5806,7 +5811,8 @@ void SmtEngine::reset() throw() { new(this) SmtEngine(em); } -void SmtEngine::resetAssertions() throw() { +void SmtEngine::resetAssertions() +{ SmtScope smts(this); doPendingPops(); @@ -5828,7 +5834,8 @@ void SmtEngine::resetAssertions() throw() { d_context->push(); } -void SmtEngine::interrupt() throw(ModalException) { +void SmtEngine::interrupt() +{ if(!d_fullyInited) { return; } @@ -5851,19 +5858,23 @@ unsigned long SmtEngine::getTimeUsage() const { return d_private->getResourceManager()->getTimeUsage(); } -unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) { +unsigned long SmtEngine::getResourceRemaining() const +{ return d_private->getResourceManager()->getResourceRemaining(); } -unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) { +unsigned long SmtEngine::getTimeRemaining() const +{ return d_private->getResourceManager()->getTimeRemaining(); } -Statistics SmtEngine::getStatistics() const throw() { +Statistics SmtEngine::getStatistics() const +{ return Statistics(*d_statisticsRegistry); } -SExpr SmtEngine::getStatistic(std::string name) const throw() { +SExpr SmtEngine::getStatistic(std::string name) const +{ return d_statisticsRegistry->getStatistic(name); } @@ -5906,9 +5917,8 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) { } } - - -void SmtEngine::beforeSearch() throw(ModalException) { +void SmtEngine::beforeSearch() +{ if(d_fullyInited) { throw ModalException( "SmtEngine::beforeSearch called after initialization."); @@ -5917,8 +5927,7 @@ void SmtEngine::beforeSearch() throw(ModalException) { void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException) { - +{ NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; @@ -5954,8 +5963,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) } CVC4::SExpr SmtEngine::getOption(const std::string& key) const - throw(OptionException) { - +{ NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT getOption(" << key << ")" << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 6d648ccda..0501a6e8f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -338,7 +338,7 @@ class CVC4_PUBLIC SmtEngine { * Fully type-check the argument, and also type-check that it's * actually Boolean. */ - void ensureBoolean(const Expr& e) throw(TypeCheckingException); + void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */; void internalPush(); @@ -350,7 +350,7 @@ class CVC4_PUBLIC SmtEngine { * Internally handle the setting of a logic. This function should always * be called when d_logic is updated. */ - void setLogicInternal() throw(); + void setLogicInternal() /* throw() */; // TODO (Issue #1096): Remove this friend relationship. friend class ::CVC4::preprocessing::PreprocessingPassContext; @@ -413,27 +413,28 @@ class CVC4_PUBLIC SmtEngine { /** * Construct an SmtEngine with the given expression manager. */ - SmtEngine(ExprManager* em) throw(); + SmtEngine(ExprManager* em) /* throw() */; /** * Destruct the SMT engine. */ - ~SmtEngine() throw(); + ~SmtEngine(); /** * Set the logic of the script. */ - void setLogic(const std::string& logic) throw(ModalException, LogicException); + void setLogic( + const std::string& logic) /* throw(ModalException, LogicException) */; /** * Set the logic of the script. */ - void setLogic(const char* logic) throw(ModalException, LogicException); + void setLogic(const char* logic) /* throw(ModalException, LogicException) */; /** * Set the logic of the script. */ - void setLogic(const LogicInfo& logic) throw(ModalException); + void setLogic(const LogicInfo& logic) /* throw(ModalException) */; /** * Get the logic information currently set @@ -444,7 +445,7 @@ class CVC4_PUBLIC SmtEngine { * Set information about the script executing. */ void setInfo(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException); + /* throw(OptionException, ModalException) */; /** * Query information about the SMT environment. @@ -455,13 +456,13 @@ class CVC4_PUBLIC SmtEngine { * Set an aspect of the current SMT execution environment. */ void setOption(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException); + /* throw(OptionException, ModalException) */; /** * Get an aspect of the current SMT execution environment. */ CVC4::SExpr getOption(const std::string& key) const - throw(OptionException); + /* throw(OptionException) */; /** * Define function func in the current context to be: @@ -515,27 +516,29 @@ class CVC4_PUBLIC SmtEngine { * takes a Boolean flag to determine whether to include this asserted * formula in an unsat core (if one is later requested). */ - Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + Result assertFormula(const Expr& e, bool inUnsatCore = true) + /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ + ; /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const Expr& e, bool inUnsatCore = true) throw(Exception); + Result query(const Expr& e, bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ Result checkSat(const Expr& e = Expr(), - bool inUnsatCore = true) throw(Exception); + bool inUnsatCore = true) /* throw(Exception) */; /** * Assert a synthesis conjecture to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSynth(const Expr& e) throw(Exception); + Result checkSynth(const Expr& e) /* throw(Exception) */; /** * Simplify a formula without doing "much" work. Does not involve @@ -546,20 +549,28 @@ class CVC4_PUBLIC SmtEngine { * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + Expr simplify( + const Expr& + e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ + ; /** * Expand the definitions in a term or formula. No other * simplification or normalization is done. */ - Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException); + Expr expandDefinitions( + const Expr& + e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */ + ; /** * Get the assigned value of an expr (only if immediately preceded * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException); + Expr getValue(const Expr& e) const + /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */ + ; /** * Add a function to the set of expressions whose value is to be @@ -645,8 +656,9 @@ class CVC4_PUBLIC SmtEngine { * The argument strict is whether to output * warnings, such as when an unexpected logic is used. */ - Expr doQuantifierElimination(const Expr& e, bool doFull, - bool strict = true) throw(Exception); + Expr doQuantifierElimination(const Expr& e, + bool doFull, + bool strict = true) /* throw(Exception) */; /** * Get list of quantified formulas that were instantiated @@ -675,7 +687,8 @@ class CVC4_PUBLIC SmtEngine { /** * Push a user-level context. */ - void push() throw(ModalException, LogicException, UnsafeInterruptException); + void + push() /* throw(ModalException, LogicException, UnsafeInterruptException) */; /** * Pop a user-level context. Throws an exception if nothing to pop. @@ -687,19 +700,19 @@ class CVC4_PUBLIC SmtEngine { * recreated. The result is as if newly constructed (so it still * retains the same options structure and ExprManager). */ - void reset() throw(); + void reset() /* throw() */; /** * Reset all assertions, global declarations, etc. */ - void resetAssertions() throw(); + void resetAssertions() /* throw() */; /** * Interrupt a running query. This can be called from another thread * or from a signal handler. Throws a ModalException if the SmtEngine * isn't currently in a query. */ - void interrupt() throw(ModalException); + void interrupt() /* throw(ModalException) */; /** * Set a resource limit for SmtEngine operations. This is like a time @@ -784,7 +797,7 @@ class CVC4_PUBLIC SmtEngine { * is not a cumulative resource limit set, this function throws a * ModalException. */ - unsigned long getResourceRemaining() const throw(ModalException); + unsigned long getResourceRemaining() const /* throw(ModalException) */; /** * Get the remaining number of milliseconds that can be consumed by @@ -792,7 +805,7 @@ class CVC4_PUBLIC SmtEngine { * If there is not a cumulative resource limit set, this function * throws a ModalException. */ - unsigned long getTimeRemaining() const throw(ModalException); + unsigned long getTimeRemaining() const /* throw(ModalException) */; /** * Permit access to the underlying ExprManager. @@ -804,12 +817,12 @@ class CVC4_PUBLIC SmtEngine { /** * Export statistics from this SmtEngine. */ - Statistics getStatistics() const throw(); + Statistics getStatistics() const /* throw() */; /** * Get the value of one named statistic from this SmtEngine. */ - SExpr getStatistic(std::string name) const throw(); + SExpr getStatistic(std::string name) const /* throw() */; /** * Flush statistic from this SmtEngine. Safe to use in a signal handler. @@ -819,10 +832,7 @@ class CVC4_PUBLIC SmtEngine { /** * Returns the most recent result of checkSat/query or (set-info :status). */ - Result getStatusOfLastCommand() const throw() { - return d_status; - } - + Result getStatusOfLastCommand() const /* throw() */ { return d_status; } /** * Set user attribute. * This function is called when an attribute is set by a user. @@ -840,7 +850,7 @@ class CVC4_PUBLIC SmtEngine { /** Throws a ModalException if the SmtEngine has been fully initialized. */ - void beforeSearch() throw(ModalException); + void beforeSearch() /* throw(ModalException) */; LemmaChannels* channels() { return d_channels; } |