Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException...

diff --git a/src/cvc4.i b/src/cvc4.i
index 2eedbf64cfe288965ecde988bade57d5fe4a0bc3..ee760c5694eeaec4e227173bfa96846a2048ef4c 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -166,6 +166,7 @@ using namespace CVC4;
 
 %include "smt/smt_engine.i"
 %include "smt/modal_exception.i"
+%include "smt/logic_exception.i"
 
 %include "options/options.i"
 %include "options/option_exception.i"

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 6f5b8fe76c28c3e7e3febfcf96db958318fc369f..5555a6190a2e99f75fd3102612dabf4580890e1c 100644 (file)
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -13,6 +13,7 @@ libsmt_la_SOURCES = \
        command_list.cpp \
        command_list.h \
        modal_exception.h \
+       logic_exception.h \
        simplification_mode.h \
        simplification_mode.cpp
 
@@ -23,4 +24,5 @@ EXTRA_DIST = \
        options_handlers.h \
        smt_options_template.cpp \
        modal_exception.i \
+       logic_exception.i \
        smt_engine.i

diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
new file mode 100644 (file)
index 0000000..c282724
--- /dev/null
+++ b/src/smt/logic_exception.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file logic_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when a feature is used outside
+ ** the logic that CVC4 is currently using
+ **
+ ** \brief An exception that is thrown when a feature is used outside
+ ** the logic that CVC4 is currently using (for example, a quantifier
+ ** is used while running in a quantifier-free logic).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__LOGIC_EXCEPTION_H
+#define __CVC4__SMT__LOGIC_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC LogicException : public CVC4::Exception {
+public:
+  LogicException() :
+    Exception("Feature used while operating in "
+              "incorrect state") {
+  }
+
+  LogicException(const std::string& msg) :
+    Exception(msg) {
+  }
+
+  LogicException(const char* msg) :
+    Exception(msg) {
+  }
+};/* class LogicException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__LOGIC_EXCEPTION_H */

diff --git a/src/smt/logic_exception.i b/src/smt/logic_exception.i
new file mode 100644 (file)
index 0000000..9fb8594
--- /dev/null
+++ b/src/smt/logic_exception.i
@@ -0,0 +1,7 @@
+%{
+#include "smt/logic_exception.h"
+%}
+
+%ignore CVC4::LogicException::LogicException(const char*);
+
+%include "smt/Logic_exception.h"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bb8e93667bae6a0db25e6a20ba5d8860a2d3885c..df95265713fb041b1479aeeeb365e099a12c6762 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -306,7 +306,7 @@ private:
    *
    * Returns false if the formula simplifies to "false"
    */
-  bool simplifyAssertions() throw(TypeCheckingException);
+  bool simplifyAssertions() throw(TypeCheckingException, LogicException);
 
 public:
 
@@ -404,13 +404,13 @@ public:
    * even be simplified.
    */
   void addFormula(TNode n)
-    throw(TypeCheckingException);
+    throw(TypeCheckingException, LogicException);
 
   /**
    * Expand definitions in n.
    */
   Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
-    throw(TypeCheckingException);
+    throw(TypeCheckingException, LogicException);
 
   /**
    * Simplify node "in" by expanding definitions and applying any
@@ -1082,7 +1082,7 @@ void SmtEngine::defineFunction(Expr func,
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
-  throw(TypeCheckingException) {
+  throw(TypeCheckingException, LogicException) {
 
   Kind k = n.getKind();
 
@@ -1729,7 +1729,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
 
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
-  throw(TypeCheckingException) {
+  throw(TypeCheckingException, LogicException) {
   Assert(d_smt.d_pendingPops == 0);
   try {
 
@@ -2057,7 +2057,7 @@ void SmtEnginePrivate::processAssertions() {
 }
 
 void SmtEnginePrivate::addFormula(TNode n)
-  throw(TypeCheckingException) {
+  throw(TypeCheckingException, LogicException) {
 
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
 
@@ -2082,7 +2082,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
   }
 }
 
-Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException) {
+Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2149,7 +2149,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   return r;
 }/* SmtEngine::checkSat() */
 
-Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException) {
+Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(!ex.isNull());
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
@@ -2213,7 +2213,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   return r;
 }/* SmtEngine::query() */
 
-Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException) {
+Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2231,7 +2231,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException) {
   return quickCheck().asValidityResult();
 }
 
-Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException) {
+Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2252,7 +2252,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException) {
   return d_private->simplify(Node::fromExpr(e)).toExpr();
 }
 
-Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException) {
+Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -2272,7 +2272,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException) {
   return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr();
 }
 
-Expr SmtEngine::getValue(const Expr& ex) throw(ModalException) {
+Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
 
@@ -2652,7 +2652,7 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
-void SmtEngine::push() throw(ModalException) {
+void SmtEngine::push() throw(ModalException, LogicException) {
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index db6084c867d328a7d85943f97f47899c6b587ef0..5c383071a3ae223800655afe67a18910a52077cc 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,6 +28,7 @@
 #include "expr/expr_manager.h"
 #include "util/proof.h"
 #include "smt/modal_exception.h"
+#include "smt/logic_exception.h"
 #include "util/hash.h"
 #include "options/options.h"
 #include "util/result.h"
@@ -370,20 +371,20 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(const Expr& e) throw(TypeCheckingException);
+  Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
 
   /**
    * 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) throw(TypeCheckingException, ModalException);
+  Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException);
+  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -394,20 +395,20 @@ public:
    * @todo (design) is this meant to give an equivalent or an
    * equisatisfiable formula?
    */
-  Expr simplify(const Expr& e) throw(TypeCheckingException);
+  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException);
 
   /**
    * Expand the definitions in a term or formula.  No other
    * simplification or normalization is done.
    */
-  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException);
+  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException);
 
   /**
    * 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) throw(ModalException);
+  Expr getValue(const Expr& e) throw(ModalException, LogicException);
 
   /**
    * Add a function to the set of expressions whose value is to be
@@ -443,7 +444,7 @@ public:
   /**
    * Push a user-level context.
    */
-  void push() throw(ModalException);
+  void push() throw(ModalException, LogicException);
 
   /**
    * Pop a user-level context.  Throws an exception if nothing to pop.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a952c9ee62c914dfe5391d0e4b716b5f07ccd367..a76ad41cc4f567460459aaa341bdeb3d34d6c8ff 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -30,6 +30,8 @@
 #include "theory/rewriter.h"
 #include "theory/theory_traits.h"
 
+#include "smt/logic_exception.h"
+
 #include "util/node_visitor.h"
 #include "util/ite_removal.h"
 
@@ -684,7 +686,7 @@ void TheoryEngine::shutdown() {
 
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
   // Reset the interrupt flag
-  d_interrupted = false; 
+  d_interrupted = false;
 
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
@@ -695,7 +697,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << Theory::theoryOf(atom)
        << ", but got an asserted fact to that theory";
-    throw Exception(ss.str());
+    throw LogicException(ss.str());
   }
 
   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
@@ -793,7 +795,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
          << ", which doesn't include " << Theory::theoryOf(current)
          << ", but got an asserted fact to that theory";
-      throw Exception(ss.str());
+      throw LogicException(ss.str());
     }
 
     // If this is an atom, we preprocess its terms with the theory ppRewriter
@@ -883,7 +885,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << toTheoryId
        << ", but got an asserted fact to that theory";
-    throw Exception(ss.str());
+    throw LogicException(ss.str());
   }
 
   if (d_inConflict) {