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

C++ ast_manager类代码示例

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

本文整理汇总了C++中ast_manager的典型用法代码示例。如果您正苦于以下问题:C++ ast_manager类的具体用法?C++ ast_manager怎么用?C++ ast_manager使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。



在下文中一共展示了ast_manager类的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。

示例1: form

/**
   \brief Return true if n is of the form (= a b)
*/
static bool is_iff(ast_manager & m, expr * n, expr * & a, expr * & b) {
    if (m.is_iff(n, a, b))
        return true;
    if (m.is_eq(n, a, b) && m.is_bool(a))
        return true;
    return false;
}
开发者ID:therealoneisneo,项目名称:Z3,代码行数:10,代码来源:tseitin_cnf_tactic.cpp


示例2:

fpa_util::fpa_util(ast_manager & m):
    m_manager(m),
    m_fid(m.mk_family_id("fpa")),
    m_a_util(m),
    m_bv_util(m) {
    m_plugin = static_cast<fpa_decl_plugin*>(m.get_plugin(m_fid));
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:7,代码来源:fpa_decl_plugin.cpp


示例3: mk_new_rule_tail

 void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var, 
                       sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
     expr_ref_buffer new_args(m);
     unsigned n  = pred->get_num_args();
     for (unsigned i = 0; i < n; i++) {
         expr * arg = pred->get_arg(i);
         if (m.is_value(arg)) {
             new_args.push_back(arg);
         }
         else {
             SASSERT(is_var(arg));
             int vidx      = to_var(arg)->get_idx();
             var * new_var = 0;
             if (!varidx2var.find(vidx, new_var)) {
                 new_var = m.mk_var(next_idx, to_var(arg)->get_sort());
                 next_idx++;
                 varidx2var.insert(vidx, new_var);
                 if (non_local_vars.contains(vidx)) {
                     // other predicates used this variable... so it should be in the domain of the filter
                     new_rule_domain.push_back(to_var(arg)->get_sort());
                     new_rule_args.push_back(new_var);
                 }
             }
             SASSERT(new_var != 0);
             new_args.push_back(new_var);
         }
     }
     new_pred = m.mk_app(pred->get_decl(), new_args.size(), new_args.c_ptr());
 }
开发者ID:Moondee,项目名称:Artemis,代码行数:29,代码来源:dl_util.cpp


示例4: validate_quant_solution

static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::def_vector const& defs) {
    // verify:
    //    new_fml => fml[t/x]
    scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
    app_ref_vector xs(m);
    expr_substitution sub(m);
    for (unsigned i = 0; i < defs.size(); ++i) {
        xs.push_back(m.mk_const(defs.var(i)));
        sub.insert(xs.back(), defs.def(i));
    }
    rep->set_substitution(&sub);
    expr_ref fml1(fml, m);
    (*rep)(fml1);
    expr_ref tmp(m);
    tmp = m.mk_not(m.mk_implies(guard, fml1));
    front_end_params fp;
    smt::kernel solver(m, fp);
    solver.assert_expr(tmp);
    lbool res = solver.check();
    //SASSERT(res == l_false);
    if (res != l_false) {
        std::cout << "Validation failed: " << res << "\n";
        std::cout << mk_pp(tmp, m) << "\n";
        model_ref model;
        solver.get_model(model);
        model_smt2_pp(std::cout, m, *model, 0);
        fatal_error(0);
    }
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:29,代码来源:quant_solve.cpp


示例5: ctx_solver_simplify_tactic

 ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()):
     m(m), m_params(p), m_solver(m, m_front_p),  
     m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0), 
     m_cancel(false) {
     sort* i_sort = m_arith.mk_int();
     m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
 }
开发者ID:killbug2004,项目名称:Snippets,代码行数:7,代码来源:ctx_solver_simplify_tactic.cpp


示例6: deallocate

void func_entry::deallocate(ast_manager & m, unsigned arity) {
    for (unsigned i = 0; i < arity; i++) {
        m.dec_ref(m_args[i]);
    }
    m.dec_ref(m_result);
    small_object_allocator & allocator = m.get_allocator();
    unsigned sz = get_obj_size(arity);
    allocator.deallocate(sz, this);
}
开发者ID:sukwon0709,项目名称:byterun,代码行数:9,代码来源:func_interp.cpp


示例7: m

proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m), 
                                               m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
    symbol fam_name("proof_hypothesis");
    if (!m.has_plugin(fam_name)) {
        m.register_plugin(fam_name, alloc(hyp_decl_plugin));
    }
    m_hyp_fid = m.mk_family_id(fam_name);
    // m_spc_fid = m.get_family_id("spc");
    m_nil = m.mk_const(m_hyp_fid, OP_NIL);
}
开发者ID:chadbrewbaker,项目名称:z3,代码行数:10,代码来源:proof_checker.cpp


示例8: reset

static_features::static_features(ast_manager & m):
    m_manager(m),
    m_autil(m),
    m_bfid(m.get_basic_family_id()),
    m_afid(m.get_family_id("arith")),
    m_lfid(m.get_family_id("label")),
    m_label_sym("label"),
    m_pattern_sym("pattern"),
    m_expr_list_sym("expr-list") {
    reset();
}
开发者ID:sukwon0709,项目名称:byterun,代码行数:11,代码来源:static_features.cpp


示例9: pb_fuzzer

 pb_fuzzer(ast_manager& m): m(m), rand(0), ctx(m, params), vars(m) {
     params.m_model = true;
     params.m_pb_enable_simplex = true;
     unsigned N = 3;
     for (unsigned i = 0; i < N; ++i) {
         std::stringstream strm;
         strm << "b" << i;
         vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()));
         std::cout << "(declare-const " << strm.str() << " Bool)\n";
     }
 }
开发者ID:timfel,项目名称:z3,代码行数:11,代码来源:theory_pb.cpp


示例10: simplify_inj_axiom

/**
   \brief Little HACK for simplifying injectivity axioms
   
   \remark It is not covering all possible cases.
*/
bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
    expr * n = q->get_expr();
    if (q->is_forall() && m.is_or(n) && to_app(n)->get_num_args() == 2) {
        expr * arg1 = to_app(n)->get_arg(0);
        expr * arg2 = to_app(n)->get_arg(1);
        if (m.is_not(arg2)) 
            std::swap(arg1, arg2);
        if (m.is_not(arg1) && 
            m.is_eq(to_app(arg1)->get_arg(0)) && 
            m.is_eq(arg2)) {
            expr * app1 = to_app(to_app(arg1)->get_arg(0))->get_arg(0);
            expr * app2 = to_app(to_app(arg1)->get_arg(0))->get_arg(1);
            expr * var1 = to_app(arg2)->get_arg(0);
            expr * var2 = to_app(arg2)->get_arg(1);
            if (is_app(app1) &&
                is_app(app2) && 
                to_app(app1)->get_decl() == to_app(app2)->get_decl() &&
                to_app(app1)->get_num_args() == to_app(app2)->get_num_args() &&
                to_app(app1)->get_family_id() == null_family_id &&
                to_app(app1)->get_num_args() > 0 &&
                is_var(var1) && 
                is_var(var2) && 
                var1 != var2) {
                app * f1          = to_app(app1);
                app * f2          = to_app(app2);
                bool found_vars   = false;
                unsigned num      = f1->get_num_args();
                unsigned idx      = UINT_MAX;
                unsigned num_vars = 1;
                for (unsigned i = 0; i < num; i++) {
                    expr  * c1 = f1->get_arg(i);
                    expr  * c2 = f2->get_arg(i);
                    if (!is_var(c1) && !is_uninterp_const(c1))
                        return false;
                    if ((c1 == var1 && c2 == var2) || (c1 == var2 && c2 == var1)) {
                        if (found_vars)
                            return false;
                        found_vars = true;
                        idx = i;
                    }
                    else if (c1 == c2 && c1 != var1 && c1 != var2) {
                        if (is_var(c1)) {
                            ++num_vars;
                        }
                    }
                    else {
                        return false;
                    }
                }
                if (found_vars && !has_free_vars(q)) {
                    TRACE("inj_axiom", 
                          tout << "Cadidate for simplification:\n" << mk_ll_pp(q, m) << mk_pp(app1, m) << "\n" << mk_pp(app2, m) << "\n" <<
                          mk_pp(var1, m) << "\n" << mk_pp(var2, m) << "\nnum_vars: " << num_vars << "\n";);
开发者ID:Moondee,项目名称:Artemis,代码行数:58,代码来源:inj_axiom.cpp


示例11: mk_bits

void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) {
    sort_ref b(m);
    b = m.mk_bool_sort();
    for (unsigned i = 0; i < sz; ++i) {
        char buffer[128];
#ifdef _WINDOWS
        sprintf_s(buffer, ARRAYSIZE(buffer), "%s%d.smt", prefix, i);
#else
        sprintf(buffer, "%s%d.smt", prefix, i);
#endif
        r.push_back(m.mk_const(symbol(buffer), b));
    }
}
开发者ID:Moondee,项目名称:Artemis,代码行数:13,代码来源:bit_blaster.cpp


示例12: SASSERT

func_entry::func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result):
    m_args_are_values(true),
    m_result(result) {
    SASSERT(is_ground(result));
    m.inc_ref(result);
    for (unsigned i = 0; i < arity; i++) {
        expr * arg = args[i];
        SASSERT(is_ground(arg));
        if (!m.is_value(arg))
            m_args_are_values = false;
        m.inc_ref(arg);
        m_args[i] = arg;
    }
}
开发者ID:sukwon0709,项目名称:byterun,代码行数:14,代码来源:func_interp.cpp


示例13: tst_match

void tst_match(ast_manager & m, app * t, app * i) {
    substitution s(m);
    s.reserve(2, 10); // reserving a big number of variables to be safe.

    matcher      match;
    std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n";
    if (match(t, i, s)) {
        std::cout << "yes\n";
        s.display(std::cout);
    }
    else {
        std::cout << "no\n";
    }

    s.reset();
    
    if (t->get_decl() == i->get_decl()) {
        // trying to match the arguments of t and i
        std::cout << "Are the arguments of " << mk_pp(i, m) << " an instance of the arguments of " << mk_pp(t, m) << "\n";
        unsigned num_args = t->get_num_args();
        unsigned j;
        for (j = 0; j < num_args; j++) {
            if (!match(t->get_arg(j), i->get_arg(j), s))
                break;
        }
        if (j == num_args) {
            std::cout << "yes\n";
            s.display(std::cout);
            
            // create some dummy term to test for applying the substitution.
            sort_ref S(          m.mk_uninterpreted_sort(symbol("S")),    m);
            sort * domain[3]   = {S, S, S};
            func_decl_ref r(     m.mk_func_decl(symbol("r"), 3, domain, S), m);
            expr_ref x1(         m.mk_var(0, S), m);
            expr_ref x2(         m.mk_var(1, S), m);
            expr_ref x3(         m.mk_var(2, S), m);
            app_ref  rxyzw(      m.mk_app(r, x1.get(), x2.get(), x3.get()), m);
            expr_ref result(m);
            unsigned deltas[2] = {0,0};
            s.apply(2, deltas, expr_offset(rxyzw, 0), result);
            std::cout << "applying substitution to\n" << mk_pp(rxyzw,m) << "\nresult:\n" << mk_pp(result,m) << "\n";
        }
        else {
            std::cout << "no\n";
        }
    }
    
    std::cout << "\n";
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:49,代码来源:matcher.cpp


示例14: mk_quantifier

expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
    expr_ref result(m);
    expr_abstract(m, 0, num_bound, (expr* const*)bound, n, result);    
    if (num_bound > 0) {
        ptr_vector<sort> sorts;
        svector<symbol> names;
        for (unsigned i = 0; i < num_bound; ++i) {
            sorts.push_back(m.get_sort(bound[i]));
            names.push_back(bound[i]->get_decl()->get_name());
        }
        result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
    }
    return result;

}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:15,代码来源:expr_abstract.cpp


示例15: operator

 virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
     // Let m_clause be of the form (l_0 or ... or l_{num_source - 1})
     // Each source[i] proof is a proof for "false" using l_i as a hypothesis
     // So, I use lemma for producing a proof for (not l_i) that does not contain the hypothesis,
     // and unit_resolution for building a proof for the goal.
     SASSERT(num_source == m_clause->get_num_args());
     proof_ref_buffer prs(m);
     prs.push_back(m_clause_pr);
     for (unsigned i = 0; i < num_source; i++) {
         proof * pr_i  = source[i];
         expr * not_li = m.mk_not(m_clause->get_arg(i));
         prs.push_back(m.mk_lemma(pr_i, not_li));
     }
     result = m.mk_unit_resolution(prs.size(), prs.c_ptr());
 }
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:15,代码来源:split_clause_tactic.cpp


示例16: get_clause_num_literals

unsigned get_clause_num_literals(ast_manager & m, expr * cls) {
    SASSERT(is_clause(m, cls));
    if (is_literal(m, cls))
        return 1;
    SASSERT(m.is_or(cls));
    return to_app(cls)->get_num_args();
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:7,代码来源:ast_util.cpp


示例17: SASSERT

macro_substitution::macro_substitution(ast_manager & m, bool cores_enabled, bool proofs_enabled):
    m_manager(m),
    m_cores_enabled(cores_enabled),
    m_proofs_enabled(proofs_enabled) {
    SASSERT(!proofs_enabled || m.proofs_enabled());
    init();
}
开发者ID:chadbrewbaker,项目名称:z3,代码行数:7,代码来源:macro_substitution.cpp


示例18: inc_sat_solver

 inc_sat_solver(ast_manager& m, params_ref const& p):
     m(m), m_solver(p, m.limit(), 0),
     m_params(p), m_optimize_model(false),
     m_fmls(m),
     m_asmsf(m),
     m_fmls_head(0),
     m_core(m),
     m_map(m),
     m_bb_rewriter(m, p),
     m_num_scopes(0),
     m_dep_core(m),
     m_unknown("no reason given") {
     m_params.set_bool("elim_vars", false);
     m_solver.updt_params(m_params);
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
     simp2_p.set_bool("pull_cheap_ite", true);
     simp2_p.set_bool("push_ite_bv", false);
     simp2_p.set_bool("local_ctx", true);
     simp2_p.set_uint("local_ctx_limit", 10000000);
     simp2_p.set_bool("flat", true); // required by som
     simp2_p.set_bool("hoist_mul", false); // required by som
     simp2_p.set_bool("elim_and", true);
     m_preprocess =
         and_then(mk_card2bv_tactic(m, m_params),
                  using_params(mk_simplify_tactic(m), simp2_p),
                  mk_max_bv_sharing_tactic(m),
                  mk_bit_blaster_tactic(m, &m_bb_rewriter),
                  //mk_aig_tactic(),
                  using_params(mk_simplify_tactic(m), simp2_p));
 }
开发者ID:suezi,项目名称:z3,代码行数:31,代码来源:inc_sat_solver.cpp


示例19:

cost_parser::cost_parser(ast_manager & m):
    simple_parser(m),
    m_util(m),
    m_vars(m) {
    family_id fid;
    fid = m.get_basic_family_id();
    add_builtin_op("true",    fid, OP_TRUE);
    add_builtin_op("false",   fid, OP_FALSE);
    add_builtin_op("not",     fid, OP_NOT);
    add_builtin_op("and",     fid, OP_AND);
    add_builtin_op("implies", fid, OP_IMPLIES);
    add_builtin_op("or",      fid, OP_OR);
    add_builtin_op("ite",     fid, OP_ITE);
    add_builtin_op("=",       fid, OP_EQ);
    add_builtin_op("iff",     fid, OP_IFF);
    add_builtin_op("xor",     fid, OP_XOR);

    fid = m_util.get_family_id();
    add_builtin_op("+",  fid, OP_ADD);
    add_builtin_op("*",  fid, OP_MUL);
    add_builtin_op("-",  fid, OP_SUB);
    add_builtin_op("/",  fid, OP_DIV);
    add_builtin_op("<=", fid, OP_LE);
    add_builtin_op(">=", fid, OP_GE);
    add_builtin_op("<",  fid, OP_LT);
    add_builtin_op(">",  fid, OP_GT);
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:27,代码来源:cost_parser.cpp


示例20: operator

proof_ref replace_proof_converter::operator()(ast_manager & m, unsigned num_source, proof * const * source) {    
    SASSERT(num_source == 1);
    replace_map replace(m);
    proof_ref p(m);
    expr_ref tmp(source[0], m), e(m), f(m);
    
    // apply the substitution to the prefix before inserting it.
    for (unsigned i = 0; i < m_proofs.size(); ++i) {
        p = m_proofs[i].get();
        e = p;
        replace.apply(e);
        f = m.mk_asserted(m.get_fact(p));
        replace.insert(f, e);
        TRACE("proof_converter", tout << f->get_id() << " " << mk_pp(f, m) << 
              "\n|-> " << mk_pp(e, m) << "\n";);
    }    
开发者ID:NikolajBjorner,项目名称:z3,代码行数:16,代码来源:replace_proof_converter.cpp



注:本文中的ast_manager类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。


鲜花

握手

雷人

路过

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

请发表评论

全部评论

专题导读
上一篇:
C++ astring类代码示例发布时间:2022-05-31
下一篇:
C++ asset类代码示例发布时间: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