C++ arith_util类代码示例

OStack程序员社区-中国程序员成长平台 › 门户 › 编程› C++›C++教程

原作者: [db:作者] 来自: [db:来源] 收藏邀请

本文整理汇总了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；未经允许，请勿转载。