summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/cvc4.i1
-rw-r--r--src/smt/Makefile.am2
-rw-r--r--src/smt/logic_exception.h47
-rw-r--r--src/smt/logic_exception.i7
-rw-r--r--src/smt/smt_engine.cpp26
-rw-r--r--src/smt/smt_engine.h15
-rw-r--r--src/theory/theory_engine.cpp10
7 files changed, 84 insertions, 24 deletions
diff --git a/src/cvc4.i b/src/cvc4.i
index 2eedbf64c..ee760c569 100644
--- 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 6f5b8fe76..5555a6190 100644
--- 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
index 000000000..c2827249d
--- /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
index 000000000..9fb859418
--- /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 bb8e93667..df9526571 100644
--- 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 db6084c86..5c383071a 100644
--- 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 a952c9ee6..a76ad41cc 100644
--- 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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback