From: Tim King <taking@cs.nyu.edu>
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