• 设为首页
  • 点击收藏
  • 手机版
    手机扫一扫访问
    迪恩网络手机版
  • 关注官方公众号
    微信扫一扫关注
    迪恩网络公众号

C++ arith_util类代码示例

原作者: [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;未经允许,请勿转载。


鲜花

握手

雷人

路过

鸡蛋
该文章已有0人参与评论

请发表评论

全部评论

专题导读
上一篇:
C++ arr类代码示例发布时间:2022-05-31
下一篇:
C++ arguments类代码示例发布时间:2022-05-31
热门推荐
阅读排行榜

扫描微信二维码

查看手机版网站

随时了解更新最新资讯

139-2527-9053

在线客服(服务时间 9:00~18:00)

在线QQ客服
地址:深圳市南山区西丽大学城创智工业园
电邮:jeky_zhao#qq.com
移动电话:139-2527-9053

Powered by 互联科技 X3.4© 2001-2213 极客世界.|Sitemap