本文整理汇总了C++中arith_util类的典型用法代码示例。如果您正苦于以下问题：C++ arith_util类的具体用法？C++ arith_util怎么用？C++ arith_util使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了arith_util类的18个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: compatible_sort
bool compatible_sort(app * n) const {
if (m.is_bool(n))
return true;
if (m_int && m_arith_util.is_int(n))
return true;
if (m_real && m_arith_util.is_real(n))
return true;
if (m_array_util.is_array(n))
return true;
return false;
}
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:11，代码来源:probe_arith.cpp
示例2: operator
void operator()(app * n) {
if (!compatible_sort(n))
throw found();
family_id fid = n->get_family_id();
if (fid == m.get_basic_family_id())
return;
if (fid == u.get_family_id()) {
switch (n->get_decl_kind()) {
case OP_LE: case OP_GE: case OP_LT: case OP_GT:
case OP_ADD: case OP_NUM:
return;
case OP_MUL:
if (n->get_num_args() != 2)
throw found();
if (!u.is_numeral(n->get_arg(0)))
throw found();
return;
case OP_TO_REAL:
if (!m_real)
throw found();
break;
default:
throw found();
}
return;
}
if (is_uninterp_const(n))
return;
throw found();
}
开发者ID:jackluo923，项目名称:juxta，代码行数:30，代码来源:probe_arith.cpp
示例3: compatible_sort
bool compatible_sort(app * n) const {
if (m.is_bool(n))
return true;
if (m_int && u.is_int(n))
return true;
if (m_real && u.is_real(n))
return true;
return false;
}
开发者ID:jackluo923，项目名称:juxta，代码行数:9，代码来源:probe_arith.cpp
示例4: process_mul
subpaving::var process_mul(app * t, unsigned depth, mpz & n, mpz & d) {
unsigned num_args = t->get_num_args();
if (num_args <= 1)
found_non_simplified();
rational k;
expr * m;
if (m_autil.is_numeral(t->get_arg(0), k)) {
if (num_args != 2)
found_non_simplified();
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
m = t->get_arg(1);
}
else {
qm().set(n, 1);
qm().set(d, 1);
m = t;
}
expr * const * margs;
unsigned sz;
if (m_autil.is_mul(m)) {
margs = to_app(m)->get_args();
sz = to_app(m)->get_num_args();
}
else {
margs = &m;
sz = 1;
}
scoped_mpz n_arg(qm());
scoped_mpz d_arg(qm());
sbuffer<subpaving::power> pws;
for (unsigned i = 0; i < sz; i++) {
expr * arg = margs[i];
unsigned k;
as_power(arg, arg, k);
subpaving::var x_arg = process(arg, depth+1, n_arg, d_arg);
qm().power(n_arg, k, n_arg);
qm().power(d_arg, k, d_arg);
qm().mul(n, n_arg, n);
qm().mul(d, d_arg, d);
if (x_arg != subpaving::null_var)
pws.push_back(subpaving::power(x_arg, k));
}
subpaving::var x;
if (pws.empty())
x = subpaving::null_var;
else if (pws.size() == 1 && pws[0].degree() == 1)
x = pws[0].get_var();
else
x = s().mk_monomial(pws.size(), pws.c_ptr());
cache_result(t, x, n, d);
return x;
}
开发者ID:CHolmes3，项目名称:z3，代码行数:53，代码来源:expr2subpaving.cpp
示例5: mk_var_for
subpaving::var mk_var_for(expr * t) {
SASSERT(!m_autil.is_numeral(t));
subpaving::var x = m_expr2var->to_var(t);
if (x == subpaving::null_var) {
bool is_int = m_autil.is_int(t);
x = s().mk_var(is_int);
m_expr2var->insert(t, x);
if (x >= m_var2expr.size())
m_var2expr.resize(x+1, 0);
m_var2expr.set(x, t);
}
return x;
}
开发者ID:CHolmes3，项目名称:z3，代码行数:13，代码来源:expr2subpaving.cpp
示例6: as_power
// Put t as a^k.
void as_power(expr * t, expr * & a, unsigned & k) {
if (!m_autil.is_power(t)) {
a = t;
k = 1;
return;
}
rational _k;
if (!m_autil.is_numeral(to_app(t)->get_arg(1), _k) || !_k.is_int() || !_k.is_unsigned()) {
a = t;
k = 1;
return;
}
a = to_app(t)->get_arg(0);
k = _k.get_unsigned();
}
开发者ID:CHolmes3，项目名称:z3，代码行数:16，代码来源:expr2subpaving.cpp
示例7: process_num
subpaving::var process_num(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
VERIFY(m_autil.is_numeral(t, k));
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
return subpaving::null_var;
}
开发者ID:CHolmes3，项目名称:z3，代码行数:7，代码来源:expr2subpaving.cpp
示例8: operator
void operator()(app * n) {
sort * s = get_sort(n);
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
throw found();
family_id fid = n->get_family_id();
if (fid == m.get_basic_family_id())
return;
if (fid == fu.get_family_id() || fid == bu.get_family_id())
return;
if (is_uninterp_const(n))
return;
if (au.is_real(s) && au.is_numeral(n))
return;
throw found();
}
开发者ID:ForwardFunk，项目名称:SynTree，代码行数:16，代码来源:qffp_tactic.cpp
示例9:
u2i_cfg(ast_manager & m, sort * u):
m_autil(m),
m_asts(m),
m_usort(u) {
m_asts.push_back(u);
m_int_sort = m_autil.mk_int();
m_asts.push_back(m_int_sort);
}
开发者ID:Moondee，项目名称:Artemis，代码行数:8，代码来源:elim_distinct.cpp
示例10: operator
void operator()(app* a) {
if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) {
return;
}
if (m_arith.is_int_real(a)) {
m_avars.push_back(a);
if (!m_seen.contains(a)) {
m_proxies.push_back(a);
m_seen.insert(a);
}
}
for (expr* arg : *a) {
if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
m_proxies.push_back(to_app(arg));
m_seen.insert(arg);
}
}
}
开发者ID:levnach，项目名称:z3，代码行数:19，代码来源:qe_mbi.cpp
示例11: operator
void operator()(app * t) {
if (is_uninterp_const(t) && (m_util.is_int(t) || m_util.is_real(t))) {
if (!m_bm.has_lower(t)) {
m_set.assert_expr(m_util.mk_le(t, m_util.mk_numeral(m_upper, m_util.is_int(t))));
m_num_bounds++;
}
if (!m_bm.has_upper(t)) {
m_set.assert_expr(m_util.mk_ge(t, m_util.mk_numeral(m_lower, m_util.is_int(t))));
m_num_bounds++;
}
}
}
开发者ID:sukwon0709，项目名称:byterun，代码行数:12，代码来源:add_bounds.cpp
示例12: operator
void operator()(app * n) {
family_id fid = n->get_family_id();
if (fid == m.get_basic_family_id())
return;
if (fid == u.get_family_id()) {
switch (n->get_decl_kind()) {
case OP_LE: case OP_GE: case OP_LT: case OP_GT:
case OP_ADD: case OP_UMINUS: case OP_SUB: case OP_ABS:
case OP_NUM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
return;
case OP_MUL:
if (n->get_num_args() == 2 &&
u.is_real(n->get_arg(0)) &&
!u.is_numeral(n->get_arg(0)) &&
!u.is_numeral(n->get_arg(1))) {
m_has_nonlinear = true;
}
return;
case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
if (!u.is_numeral(n->get_arg(1)))
throw_found();
return;
case OP_POWER:
if (!u.is_numeral(n->get_arg(1)))
throw_found();
m_has_nonlinear = true;
return;
case OP_IS_INT:
case OP_TO_INT:
case OP_TO_REAL:
throw_found();
return;
default:
throw_found();
}
}
}
开发者ID:AleksandarZeljic，项目名称:z3，代码行数:38，代码来源:probe_arith.cpp
示例13: process_arith_app
subpaving::var process_arith_app(app * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(m_autil.is_arith_expr(t));
switch (t->get_decl_kind()) {
case OP_NUM:
return process_num(t, depth, n, d);
case OP_ADD:
return process_add(t, depth, n, d);
case OP_MUL:
return process_mul(t, depth, n, d);
case OP_POWER:
return process_power(t, depth, n, d);
case OP_TO_REAL:
return process(t->get_arg(0), depth+1, n, d);
case OP_SUB:
case OP_UMINUS:
found_non_simplified();
break;
case OP_TO_INT:
case OP_DIV:
case OP_IDIV:
case OP_MOD:
case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");
case OP_SIN:
case OP_COS:
case OP_TAN:
case OP_ASIN:
case OP_ACOS:
case OP_ATAN:
case OP_SINH:
case OP_COSH:
case OP_TANH:
case OP_ASINH:
case OP_ACOSH:
case OP_ATANH:
// TODO
throw default_exception("transcendental and hyperbolic functions are not supported yet.");
default:
UNREACHABLE();
}
return subpaving::null_var;
}
开发者ID:CHolmes3，项目名称:z3，代码行数:44，代码来源:expr2subpaving.cpp
示例14: process_power
subpaving::var process_power(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
SASSERT(t->get_num_args() == 2);
if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
unsigned _k = k.get_unsigned();
subpaving::var x = process(t->get_arg(0), depth+1, n, d);
if (x != subpaving::null_var) {
subpaving::power p(x, _k);
x = s().mk_monomial(1, &p);
}
qm().power(n, _k, n);
qm().power(d, _k, d);
cache_result(t, x, n, d);
return x;
}
开发者ID:CHolmes3，项目名称:z3，代码行数:19，代码来源:expr2subpaving.cpp
示例15: process
subpaving::var process(expr * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(is_int_real(t));
checkpoint();
if (is_cached(t)) {
unsigned idx = m_cache.find(t);
qm().set(n, m_cached_numerators[idx]);
qm().set(d, m_cached_denominators[idx]);
return m_cached_vars[idx];
}
SASSERT(!is_quantifier(t));
if (::is_var(t) || !m_autil.is_arith_expr(t)) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
return process_arith_app(to_app(t), depth, n, d);
}
开发者ID:CHolmes3，项目名称:z3，代码行数:20，代码来源:expr2subpaving.cpp
示例16: is_arith_op
bool is_arith_op(app* a) {
return a->get_family_id() == m_arith.get_family_id();
}
开发者ID:levnach，项目名称:z3，代码行数:3，代码来源:qe_mbi.cpp
示例17: is_int_real
bool is_int_real(expr * t) {
return m_autil.is_int_real(t);
}
开发者ID:CHolmes3，项目名称:z3，代码行数:3，代码来源:expr2subpaving.cpp
示例18: operator
void operator()(app * t) {
if (is_uninterp_const(t) && (m_util.is_int(t) || m_util.is_real(t)) && (!m_bm.has_lower(t) || !m_bm.has_upper(t)))
throw found();
}
开发者ID:CHolmes3，项目名称:z3，代码行数:4，代码来源:add_bounds_tactic.cpp
注：本文中的arith_util类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。 |
客服电话
APP下载
官方微信
请发表评论