mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
port to inherit from std::exception
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
407bad3693
commit
a38bf3e22f
|
@ -22,7 +22,7 @@ Revision History:
|
|||
#include "ast/simplifiers/bound_manager.h"
|
||||
|
||||
struct is_unbounded_proc {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
arith_util m_util;
|
||||
bound_manager & m_bm;
|
||||
|
||||
|
|
|
@ -35,7 +35,7 @@ Notes:
|
|||
|
||||
class pb2bv_tactic : public tactic {
|
||||
public:
|
||||
struct non_pb { expr* e; non_pb(expr* e) : e(e) {}};
|
||||
struct non_pb : public std::exception { expr* e; non_pb(expr* e) : e(e) {}};
|
||||
|
||||
struct only_01_visitor {
|
||||
typedef rational numeral;
|
||||
|
@ -167,7 +167,7 @@ private:
|
|||
|
||||
enum constraint_kind { EQ, GE, LE };
|
||||
|
||||
struct failed {};
|
||||
struct failed : public std::exception {};
|
||||
|
||||
struct visitor {
|
||||
imp & m_owner;
|
||||
|
|
|
@ -130,7 +130,7 @@ public:
|
|||
};
|
||||
|
||||
struct has_nlmul {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager& m;
|
||||
arith_util a;
|
||||
has_nlmul(ast_manager& m):m(m), a(m) {}
|
||||
|
@ -185,7 +185,7 @@ probe * mk_arith_max_bw_probe() {
|
|||
|
||||
namespace {
|
||||
struct is_non_qflira_functor {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
arith_util u;
|
||||
bool m_int;
|
||||
|
@ -240,7 +240,7 @@ struct is_non_qflira_functor {
|
|||
};
|
||||
|
||||
struct is_non_qfauflira_functor {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
arith_util m_arith_util;
|
||||
array_util m_array_util;
|
||||
|
@ -427,7 +427,7 @@ probe * mk_is_mip_probe() {
|
|||
namespace {
|
||||
|
||||
struct is_non_nira_functor {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
arith_util u;
|
||||
bool m_int;
|
||||
|
@ -572,7 +572,7 @@ static bool is_lira(goal const & g) {
|
|||
|
||||
|
||||
struct is_non_qfufnra_functor {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
arith_util u;
|
||||
bool m_has_nonlinear;
|
||||
|
|
|
@ -32,7 +32,7 @@ Notes:
|
|||
|
||||
|
||||
struct is_non_fp_qfnra_predicate {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
bv_util bu;
|
||||
fpa_util fu;
|
||||
|
|
|
@ -27,7 +27,7 @@ tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) {
|
|||
}
|
||||
|
||||
struct is_fpa_function {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
fpa_util fu;
|
||||
|
||||
|
|
|
@ -20,7 +20,7 @@ Revision History:
|
|||
#include "tactic/goal.h"
|
||||
|
||||
struct has_term_ite_functor {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
has_term_ite_functor(ast_manager & _m):m(_m) {}
|
||||
void operator()(var *) {}
|
||||
|
|
|
@ -248,7 +248,7 @@ probe * mk_div(probe * p1, probe * p2) {
|
|||
}
|
||||
|
||||
struct is_non_propositional_predicate {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
|
||||
is_non_propositional_predicate(ast_manager & _m):m(_m) {}
|
||||
|
@ -270,7 +270,7 @@ struct is_non_propositional_predicate {
|
|||
};
|
||||
|
||||
struct is_non_qfbv_predicate {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
bv_util u;
|
||||
|
||||
|
@ -325,7 +325,7 @@ probe * mk_is_qfbv_probe() {
|
|||
}
|
||||
|
||||
struct is_non_qfaufbv_predicate {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
bv_util m_bv_util;
|
||||
array_util m_array_util;
|
||||
|
@ -364,7 +364,7 @@ probe * mk_is_qfaufbv_probe() {
|
|||
|
||||
|
||||
struct is_non_qfufbv_predicate {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
ast_manager & m;
|
||||
bv_util m_bv_util;
|
||||
|
||||
|
@ -503,7 +503,7 @@ probe * mk_produce_unsat_cores_probe() {
|
|||
}
|
||||
|
||||
struct has_pattern_probe : public probe {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
|
||||
struct proc {
|
||||
void operator()(var * n) {}
|
||||
|
@ -536,7 +536,7 @@ probe * mk_has_pattern_probe() {
|
|||
|
||||
|
||||
struct has_quantifier_probe : public probe {
|
||||
struct found {};
|
||||
struct found : public std::exception {};
|
||||
|
||||
struct proc {
|
||||
void operator()(var * n) {}
|
||||
|
|
Loading…
Reference in a new issue