*
* Returns false if the formula simplifies to "false"
*/
- bool simplifyAssertions() throw(TypeCheckingException, LogicException,
- UnsafeInterruptException);
+ bool simplifyAssertions();
-public:
+ public:
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
new SetToDefaultSourceListener(&d_managedReplayLog), true));
}
- ~SmtEnginePrivate() throw() {
+ ~SmtEnginePrivate()
+ {
delete d_listenerRegistrations;
if(d_propagatorNeedsFinish) {
}
ResourceManager* getResourceManager() { return d_resourceManager; }
- void spendResource(unsigned amount) throw(UnsafeInterruptException) {
+ void spendResource(unsigned amount)
+ {
d_resourceManager->spendResource(amount);
}
* even be simplified.
* the 2nd and 3rd arguments added for bookkeeping for proofs
*/
- void addFormula(TNode n, bool inUnsatCore, bool inInput = true)
- throw(TypeCheckingException, LogicException);
+ void addFormula(TNode n, bool inUnsatCore, bool inInput = true);
/** Expand definitions in n. */
- Node expandDefinitions(TNode n, NodeToNodeHashMap& cache,
- bool expandOnly = false)
- throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+ Node expandDefinitions(TNode n,
+ NodeToNodeHashMap& cache,
+ bool expandOnly = false);
/**
* Simplify node "in" by expanding definitions and applying any
}/* namespace CVC4::smt */
-SmtEngine::SmtEngine(ExprManager* em) throw()
+SmtEngine::SmtEngine(ExprManager* em)
: d_context(new Context()),
d_userLevels(),
d_userContext(new UserContext()),
}
}
-SmtEngine::~SmtEngine() throw() {
+SmtEngine::~SmtEngine()
+{
SmtScope smts(this);
try {
}
}
-void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
+void SmtEngine::setLogic(const LogicInfo& logic)
+{
SmtScope smts(this);
if(d_fullyInited) {
throw ModalException("Cannot set logic in SmtEngine after the engine has "
}
void SmtEngine::setLogic(const std::string& s)
- throw(ModalException, LogicException) {
+{
SmtScope smts(this);
try {
setLogic(LogicInfo(s));
}
}
-void SmtEngine::setLogic(const char* logic)
- throw(ModalException, LogicException) {
- setLogic(string(logic));
-}
-
+void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
LogicInfo SmtEngine::getLogicInfo() const {
return d_logic;
}
-
-void SmtEngine::setLogicInternal() throw() {
+void SmtEngine::setLogicInternal()
+{
Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already"
" finished initializing for this run");
d_logic.lock();
}
void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
- throw(OptionException, ModalException) {
-
+{
SmtScope smts(this);
Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
}
Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
- throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
-
+{
stack< triple<Node, Node, bool> > worklist;
stack<Node> result;
worklist.push(make_triple(Node(n), Node(n), false));
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
- throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+{
spendResource(options::preprocessStep());
Assert(d_smt.d_pendingPops == 0);
try {
}
void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
- throw(TypeCheckingException, LogicException) {
-
+{
if (n == d_true) {
// nothing to do
return;
//d_assertions.push_back(Rewriter::rewrite(n));
}
-void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
+void SmtEngine::ensureBoolean(const Expr& e)
+{
Type type = e.getType(options::typeChecking());
Type boolType = d_exprManager->booleanType();
if(type != boolType) {
}
}
-Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(Exception) {
+Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore)
+{
return checkSatisfiability(ex, inUnsatCore, false);
} /* SmtEngine::checkSat() */
-Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(Exception) {
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore)
+{
Assert(!ex.isNull());
return checkSatisfiability(ex, inUnsatCore, true);
} /* SmtEngine::query() */
}
}
-Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
+Result SmtEngine::checkSynth(const Expr& e)
+{
SmtScope smts(this);
Trace("smt") << "Check synth: " << e << std::endl;
Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
return checkSatisfiability( e_check, true, false );
}
-Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
+{
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
return node;
}
-Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+Expr SmtEngine::simplify(const Expr& ex)
+{
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
finalOptionsAreSet();
return n.toExpr();
}
-Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+Expr SmtEngine::expandDefinitions(const Expr& ex)
+{
d_private->spendResource(options::preprocessStep());
Assert(ex.getExprManager() == d_exprManager);
}
// TODO(#1108): Simplify the error reporting of this method.
-Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) {
+Expr SmtEngine::getValue(const Expr& ex) const
+{
Assert(ex.getExprManager() == d_exprManager);
SmtScope smts(this);
}
}
-Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull,
- bool strict) throw(Exception) {
+Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
+{
SmtScope smts(this);
if(!d_logic.isPure(THEORY_ARITH) && strict){
Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
}
-void SmtEngine::push() throw(ModalException, LogicException, UnsafeInterruptException) {
+void SmtEngine::push()
+{
SmtScope smts(this);
finalOptionsAreSet();
doPendingPops();
}
}
-void SmtEngine::reset() throw() {
+void SmtEngine::reset()
+{
SmtScope smts(this);
ExprManager *em = d_exprManager;
Trace("smt") << "SMT reset()" << endl;
new(this) SmtEngine(em);
}
-void SmtEngine::resetAssertions() throw() {
+void SmtEngine::resetAssertions()
+{
SmtScope smts(this);
doPendingPops();
d_context->push();
}
-void SmtEngine::interrupt() throw(ModalException) {
+void SmtEngine::interrupt()
+{
if(!d_fullyInited) {
return;
}
return d_private->getResourceManager()->getTimeUsage();
}
-unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
+unsigned long SmtEngine::getResourceRemaining() const
+{
return d_private->getResourceManager()->getResourceRemaining();
}
-unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
+unsigned long SmtEngine::getTimeRemaining() const
+{
return d_private->getResourceManager()->getTimeRemaining();
}
-Statistics SmtEngine::getStatistics() const throw() {
+Statistics SmtEngine::getStatistics() const
+{
return Statistics(*d_statisticsRegistry);
}
-SExpr SmtEngine::getStatistic(std::string name) const throw() {
+SExpr SmtEngine::getStatistic(std::string name) const
+{
return d_statisticsRegistry->getStatistic(name);
}
}
}
-
-
-void SmtEngine::beforeSearch() throw(ModalException) {
+void SmtEngine::beforeSearch()
+{
if(d_fullyInited) {
throw ModalException(
"SmtEngine::beforeSearch called after initialization.");
void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
- throw(OptionException, ModalException) {
-
+{
NodeManagerScope nms(d_nodeManager);
Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
}
CVC4::SExpr SmtEngine::getOption(const std::string& key) const
- throw(OptionException) {
-
+{
NodeManagerScope nms(d_nodeManager);
Trace("smt") << "SMT getOption(" << key << ")" << endl;
* Fully type-check the argument, and also type-check that it's
* actually Boolean.
*/
- void ensureBoolean(const Expr& e) throw(TypeCheckingException);
+ void ensureBoolean(const Expr& e) /* throw(TypeCheckingException) */;
void internalPush();
* Internally handle the setting of a logic. This function should always
* be called when d_logic is updated.
*/
- void setLogicInternal() throw();
+ void setLogicInternal() /* throw() */;
// TODO (Issue #1096): Remove this friend relationship.
friend class ::CVC4::preprocessing::PreprocessingPassContext;
/**
* Construct an SmtEngine with the given expression manager.
*/
- SmtEngine(ExprManager* em) throw();
+ SmtEngine(ExprManager* em) /* throw() */;
/**
* Destruct the SMT engine.
*/
- ~SmtEngine() throw();
+ ~SmtEngine();
/**
* Set the logic of the script.
*/
- void setLogic(const std::string& logic) throw(ModalException, LogicException);
+ void setLogic(
+ const std::string& logic) /* throw(ModalException, LogicException) */;
/**
* Set the logic of the script.
*/
- void setLogic(const char* logic) throw(ModalException, LogicException);
+ void setLogic(const char* logic) /* throw(ModalException, LogicException) */;
/**
* Set the logic of the script.
*/
- void setLogic(const LogicInfo& logic) throw(ModalException);
+ void setLogic(const LogicInfo& logic) /* throw(ModalException) */;
/**
* Get the logic information currently set
* Set information about the script executing.
*/
void setInfo(const std::string& key, const CVC4::SExpr& value)
- throw(OptionException, ModalException);
+ /* throw(OptionException, ModalException) */;
/**
* Query information about the SMT environment.
* Set an aspect of the current SMT execution environment.
*/
void setOption(const std::string& key, const CVC4::SExpr& value)
- throw(OptionException, ModalException);
+ /* throw(OptionException, ModalException) */;
/**
* Get an aspect of the current SMT execution environment.
*/
CVC4::SExpr getOption(const std::string& key) const
- throw(OptionException);
+ /* throw(OptionException) */;
/**
* Define function func in the current context to be:
* takes a Boolean flag to determine whether to include this asserted
* formula in an unsat core (if one is later requested).
*/
- Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+ Result assertFormula(const Expr& e, bool inUnsatCore = true)
+ /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
+ ;
/**
* 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, bool inUnsatCore = true) throw(Exception);
+ 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(Exception);
+ 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(Exception);
+ Result checkSynth(const Expr& e) /* throw(Exception) */;
/**
* Simplify a formula without doing "much" work. Does not involve
* @todo (design) is this meant to give an equivalent or an
* equisatisfiable formula?
*/
- Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+ Expr simplify(
+ const Expr&
+ e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
+ ;
/**
* Expand the definitions in a term or formula. No other
* simplification or normalization is done.
*/
- Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+ Expr expandDefinitions(
+ const Expr&
+ e) /* throw(TypeCheckingException, LogicException, UnsafeInterruptException) */
+ ;
/**
* 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) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException);
+ Expr getValue(const Expr& e) const
+ /* throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) */
+ ;
/**
* Add a function to the set of expressions whose value is to be
* The argument strict is whether to output
* warnings, such as when an unexpected logic is used.
*/
- Expr doQuantifierElimination(const Expr& e, bool doFull,
- bool strict = true) throw(Exception);
+ Expr doQuantifierElimination(const Expr& e,
+ bool doFull,
+ bool strict = true) /* throw(Exception) */;
/**
* Get list of quantified formulas that were instantiated
/**
* Push a user-level context.
*/
- void push() throw(ModalException, LogicException, UnsafeInterruptException);
+ void
+ push() /* throw(ModalException, LogicException, UnsafeInterruptException) */;
/**
* Pop a user-level context. Throws an exception if nothing to pop.
* recreated. The result is as if newly constructed (so it still
* retains the same options structure and ExprManager).
*/
- void reset() throw();
+ void reset() /* throw() */;
/**
* Reset all assertions, global declarations, etc.
*/
- void resetAssertions() throw();
+ void resetAssertions() /* throw() */;
/**
* Interrupt a running query. This can be called from another thread
* or from a signal handler. Throws a ModalException if the SmtEngine
* isn't currently in a query.
*/
- void interrupt() throw(ModalException);
+ void interrupt() /* throw(ModalException) */;
/**
* Set a resource limit for SmtEngine operations. This is like a time
* is not a cumulative resource limit set, this function throws a
* ModalException.
*/
- unsigned long getResourceRemaining() const throw(ModalException);
+ unsigned long getResourceRemaining() const /* throw(ModalException) */;
/**
* Get the remaining number of milliseconds that can be consumed by
* If there is not a cumulative resource limit set, this function
* throws a ModalException.
*/
- unsigned long getTimeRemaining() const throw(ModalException);
+ unsigned long getTimeRemaining() const /* throw(ModalException) */;
/**
* Permit access to the underlying ExprManager.
/**
* Export statistics from this SmtEngine.
*/
- Statistics getStatistics() const throw();
+ Statistics getStatistics() const /* throw() */;
/**
* Get the value of one named statistic from this SmtEngine.
*/
- SExpr getStatistic(std::string name) const throw();
+ SExpr getStatistic(std::string name) const /* throw() */;
/**
* Flush statistic from this SmtEngine. Safe to use in a signal handler.
/**
* Returns the most recent result of checkSat/query or (set-info :status).
*/
- Result getStatusOfLastCommand() const throw() {
- return d_status;
- }
-
+ Result getStatusOfLastCommand() const /* throw() */ { return d_status; }
/**
* Set user attribute.
* This function is called when an attribute is set by a user.
/** Throws a ModalException if the SmtEngine has been fully initialized. */
- void beforeSearch() throw(ModalException);
+ void beforeSearch() /* throw(ModalException) */;
LemmaChannels* channels() { return d_channels; }
projects / cvc5.git / commitdiff