From: Tim King Date: Thu, 14 Sep 2017 17:09:40 +0000 (-0700) Subject: Simplifying the throw specifier of SmtEngine::checkSat and related calls to CVC4... X-Git-Tag: cvc5-1.0.0~5638 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e4fc6c7b57668f18ce087c45e001c101375c20ea;p=cvc5.git Simplifying the throw specifier of SmtEngine::checkSat and related calls to CVC4::Exception. (#1085) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index af4510ff1..b1a0a1acd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4383,14 +4383,14 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { - return checkSatisfiability( ex, inUnsatCore, false ); -}/* SmtEngine::checkSat() */ +Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(Exception) { + return checkSatisfiability(ex, inUnsatCore, false); +} /* SmtEngine::checkSat() */ -Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) { +Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(Exception) { Assert(!ex.isNull()); - return checkSatisfiability( ex, inUnsatCore, true ); -}/* SmtEngine::query() */ + return checkSatisfiability(ex, inUnsatCore, true); +} /* SmtEngine::query() */ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQuery) { try { @@ -4497,8 +4497,7 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ } } - -Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException) { +Result SmtEngine::checkSynth(const Expr& e) throw(Exception) { SmtScope smts(this); Trace("smt") << "Check synth: " << e << std::endl; Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl; @@ -5207,7 +5206,8 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { } } -Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) throw(TypeCheckingException, ModalException, LogicException) { +Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, + bool strict) throw(Exception) { SmtScope smts(this); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ed265e2b8..735364db8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -462,19 +462,20 @@ public: * 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(TypeCheckingException, ModalException, LogicException); + 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(TypeCheckingException, ModalException, LogicException); + Result checkSat(const Expr& e = Expr(), + 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(TypeCheckingException, ModalException, LogicException); + Result checkSynth(const Expr& e) throw(Exception); /** * Simplify a formula without doing "much" work. Does not involve @@ -536,9 +537,11 @@ public: void printSynthSolution( std::ostream& out ); /** - * Do quantifier elimination, doFull false means just output one disjunct, strict is whether to output warnings. + * Do quantifier elimination, doFull false means just output one disjunct, + * strict is whether to output warnings. */ - Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException); + Expr doQuantifierElimination(const Expr& e, bool doFull, + bool strict = true) throw(Exception); /** * Get list of quantified formulas that were instantiated