From ca6647503475fb36827e960d9e01c3f8a04c4ed3 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 9 Nov 2012 19:18:58 +0000 Subject: [PATCH] Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic) --- src/cvc4.i | 1 + src/smt/Makefile.am | 2 ++ src/smt/logic_exception.h | 47 ++++++++++++++++++++++++++++++++++++ src/smt/logic_exception.i | 7 ++++++ src/smt/smt_engine.cpp | 26 ++++++++++---------- src/smt/smt_engine.h | 15 ++++++------ src/theory/theory_engine.cpp | 10 +++++--- 7 files changed, 84 insertions(+), 24 deletions(-) create mode 100644 src/smt/logic_exception.h create mode 100644 src/smt/logic_exception.i 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& 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& cache) - throw(TypeCheckingException) { + throw(TypeCheckingException, LogicException) { Kind k = n.getKind(); @@ -1729,7 +1729,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector& 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 SmtEngine::getAssertions() throw(ModalException) { return vector(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) { -- 2.30.2