mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-05 15:16:54 +00:00
parent c11b6d90ce
commit 3d37c25bcc
1 changed files with 18 additions and 18 deletions

36
src/ast/arith_decl_plugin.h
View file

@ -115,7 +115,7 @@ protected:
func_decl * m_i_div_decl;
func_decl * m_i_mod_decl;
func_decl * m_i_rem_decl;
func_decl * m_to_real_decl;
func_decl * m_to_int_decl;
func_decl * m_is_int_decl;
@ -140,7 +140,7 @@ protected:
app * m_pi;
app * m_e;
app * m_0_pw_0_int;
app * m_0_pw_0_real;
func_decl * m_neg_root_decl;
@ -149,7 +149,7 @@ protected:
func_decl * m_mod_0_decl;
func_decl * m_u_asin_decl;
func_decl * m_u_acos_decl;
ptr_vector<app> m_small_ints;
ptr_vector<app> m_small_reals;
@ -175,11 +175,11 @@ public:
}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range);
virtual bool is_value(app * e) const;
@ -202,11 +202,11 @@ public:
app * mk_numeral(sexpr const * p, unsigned i);
app * mk_pi() const { return m_pi; }
app * mk_e() const { return m_e; }
app * mk_0_pw_0_int() const { return m_0_pw_0_int; }
app * mk_0_pw_0_real() const { return m_0_pw_0_real; }
virtual expr * get_some_value(sort * s);
@ -258,7 +258,7 @@ public:
bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
bool is_int(expr const * n) const { return is_int(get_sort(n)); }
bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
@ -275,7 +275,7 @@ public:
MATCH_BINARY(is_le);
MATCH_BINARY(is_ge);
MATCH_BINARY(is_lt);
MATCH_BINARY(is_gt);
MATCH_BINARY(is_gt);
MATCH_BINARY(is_mod);
MATCH_BINARY(is_rem);
MATCH_BINARY(is_div);
@ -297,25 +297,25 @@ class arith_util : public arith_recognizers {
SASSERT(m_plugin != 0);
return *m_plugin;
}
public:
arith_util(ast_manager & m);
ast_manager & get_manager() const { return m_manager; }
algebraic_numbers::manager & am() {
return plugin().am();
algebraic_numbers::manager & am() {
return plugin().am();
}
bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); }
bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val);
algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n);
sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); }
sort * mk_real() { return m_manager.mk_sort(m_afid, REAL_SORT); }
app * mk_numeral(rational const & val, bool is_int) const {
return plugin().mk_numeral(val, is_int);
app * mk_numeral(rational const & val, bool is_int) const {
return plugin().mk_numeral(val, is_int);
}
app * mk_numeral(rational const & val, sort const * s) const {
SASSERT(is_int(s) || is_real(s));
@ -379,9 +379,9 @@ public:
app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); }
app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); }
app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); }
/**
\brief Return the equality (= lhs rhs), but it makes sure that
\brief Return the equality (= lhs rhs), but it makes sure that
if one of the arguments is a numeral, then it will be in the right-hand-side;
if none of them are numerals, then the left-hand-side has a smaller id than the right hand side.
*/