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

C++ goal_ref类代码示例

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

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



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

示例1: operator

    void operator()(goal_ref const & g, goal_ref_buffer & result) override {
        ast_manager& m(g->m());
        tactic_report report("qfufbv_ackr", *g);
        fail_if_unsat_core_generation("qfufbv_ackr", g);
        fail_if_proof_generation("qfufbv_ackr", g);

        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
开发者ID:bishoksan,项目名称:z3,代码行数:7,代码来源:qfufbv_tactic.cpp


示例2: operator

        void operator()(goal_ref const & g, 
                        goal_ref_buffer & result) {
            SASSERT(g->is_well_sorted());
            fail_if_proof_generation("occf", g);

            bool produce_models = g->models_enabled();
            tactic_report report("occf", *g);
            
            m_mc = nullptr;
            
            ptr_vector<expr> new_lits;
            
            cnstr2bvar c2b;
            
            unsigned sz = g->size();
            for (unsigned i = 0; i < sz; i++) {
                checkpoint();
                expr * f = g->form(i);
                expr_dependency * d = g->dep(i);
                if (!m.is_or(f))
                    continue;
                app * cls = to_app(f);
                if (!is_target(cls))
                    continue;
                if (produce_models && !m_mc) {
                    m_mc = alloc(generic_model_converter, m, "occf");
                    g->add(m_mc);
                }
                expr * keep = nullptr;
                new_lits.reset();
                unsigned num = cls->get_num_args();
                for (unsigned j = 0; j < num; j++) {
                    expr * l = cls->get_arg(j);
                    if (is_constraint(l)) {
                        expr * new_l = get_aux_lit(c2b, l, g);
                        if (new_l != nullptr) {
                            new_lits.push_back(new_l);
                        }
                        else if (keep == nullptr) {
                            keep = l;
                        }
                        else {
                            new_l = mk_aux_lit(c2b, l, produce_models, g);
                            new_lits.push_back(new_l);
                        }
                    }
                    else {
                        new_lits.push_back(l);
                    }
                }
                if (keep != nullptr)
                    new_lits.push_back(keep);
                g->update(i, m.mk_or(new_lits.size(), new_lits.c_ptr()), nullptr, d);
            }
            g->inc_depth();
            result.push_back(g.get());
            TRACE("occf", g->display(tout););
开发者ID:NikolajBjorner,项目名称:z3,代码行数:57,代码来源:occf_tactic.cpp


示例3: operator

 virtual void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     SASSERT(g->is_well_sorted());        
     mc = 0; pc = 0; core = 0; result.reset();
     
     TRACE("sls", g->display(tout););
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:9,代码来源:sls_tactic.cpp


示例4: operator

 virtual void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     fail_if_proof_generation("aig", g);
     mc = 0; pc = 0; core = 0;
     operator()(g);
     g->inc_depth();
     result.push_back(g.get());
 }
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:11,代码来源:aig_tactic.cpp


示例5: operator

 virtual void operator()(goal_ref const & in, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     
     mc = 0; pc = 0; core = 0;
     reduce(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:11,代码来源:ctx_solver_simplify_tactic.cpp


示例6: extract_clauses_and_dependencies

void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector<expr>& assumptions, expr2expr_map& bool2dep, ref<filter_model_converter>& fmc) {
    expr2expr_map dep2bool;
    ptr_vector<expr> deps;
    ast_manager& m = g->m();
    expr_ref_vector clause(m);
    unsigned sz = g->size();
    for (unsigned i = 0; i < sz; i++) {
        expr * f            = g->form(i);
        expr_dependency * d = g->dep(i);
        if (d == 0 || !g->unsat_core_enabled()) {
            clauses.push_back(f);
        }
        else {
            // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f.
            clause.reset();
            clause.push_back(f);
            deps.reset();
            m.linearize(d, deps);
            SASSERT(!deps.empty()); // d != 0, then deps must not be empty
            ptr_vector<expr>::iterator it  = deps.begin();
            ptr_vector<expr>::iterator end = deps.end();
            for (; it != end; ++it) {
                expr * d = *it;
                if (is_uninterp_const(d) && m.is_bool(d)) {
                    // no need to create a fresh boolean variable for d
                    if (!bool2dep.contains(d)) {
                        assumptions.push_back(d);
                        bool2dep.insert(d, d);
                    }
                    clause.push_back(m.mk_not(d));
                }
                else {
                    // must normalize assumption
                    expr * b = 0;
                    if (!dep2bool.find(d, b)) {
                        b = m.mk_fresh_const(0, m.mk_bool_sort());
                        dep2bool.insert(d, b);
                        bool2dep.insert(b, d);
                        assumptions.push_back(b);
                        if (!fmc) {
                            fmc = alloc(filter_model_converter, m);
                        }
                        fmc->insert(to_app(b)->get_decl());
                    }
                    clause.push_back(m.mk_not(b));
                }
            }
            SASSERT(clause.size() > 1);
            expr_ref cls(m);
            cls = mk_or(m, clause.size(), clause.c_ptr());
            clauses.push_back(cls);
        }
    }
}
开发者ID:ForwardFunk,项目名称:SynTree,代码行数:54,代码来源:smt_tactic.cpp


示例7: operator

    virtual void operator()(goal_ref const & g,
        goal_ref_buffer & result,
        model_converter_ref & mc,
        proof_converter_ref & pc,
        expr_dependency_ref & core) {
        mc = 0;
        ast_manager& m(g->m());
        tactic_report report("qfufbv_ackr", *g);
        fail_if_unsat_core_generation("qfufbv_ackr", g);
        fail_if_proof_generation("qfufbv_ackr", g);

        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
开发者ID:mseve,项目名称:z3,代码行数:12,代码来源:qfufbv_tactic.cpp


示例8: operator

        void operator()(goal_ref const & g, 
                        goal_ref_buffer & result, 
                        model_converter_ref & mc, 
                        proof_converter_ref & pc,
                        expr_dependency_ref & core) {
            mc = 0; pc = 0; core = 0;
            bool proofs_enabled = g->proofs_enabled();

            if (proofs_enabled && m_blast_quant)
                throw tactic_exception("quantified variable blasting does not support proof generation");
            
            tactic_report report("bit-blaster", *g);
            
            TRACE("before_bit_blaster", g->display(tout););
开发者ID:CHolmes3,项目名称:z3,代码行数:14,代码来源:bit_blaster_tactic.cpp


示例9: full_eval

        bool full_eval(goal_ref const & g, model & mdl) {
            bool res = true;

            unsigned sz = g->size();
            for (unsigned i = 0; i < sz && res; i++) {
                checkpoint();
                expr_ref o(m_manager);

                if (!mdl.eval(g->form(i), o, true))
                    exit(ERR_INTERNAL_FATAL);

                res = m_manager.is_true(o.get());
            }        

            TRACE("sls", tout << "Evaluation: " << res << std::endl;);
开发者ID:Jornason,项目名称:z3,代码行数:15,代码来源:sls_tactic.cpp


示例10: operator

        virtual void operator()(goal_ref const & g,
                                goal_ref_buffer & result,
                                model_converter_ref & mc,
                                proof_converter_ref & pc,
                                expr_dependency_ref & core) {
            SASSERT(g->is_well_sorted());
            m_proofs_enabled      = g->proofs_enabled();
            m_produce_models      = g->models_enabled();
            m_produce_unsat_cores = g->unsat_core_enabled();

            mc = 0; pc = 0; core = 0; result.reset();
            tactic_report report("fpa2bv", *g);
            m_rw.reset();

            TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout););
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:15,代码来源:fpa2bv_tactic.cpp


示例11: simplify

 bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
     reset();
     normalize(g);
     if (g->inconsistent()) {
         return false;
     }
     for (unsigned i = 0; i < g->size(); ++i) {
         process_vars(i, g);
     }
     
     if (m_ge.empty()) {
         return false;
     }
     
     for (unsigned i = 0; i < m_ge.size(); ++i) {
         classify_vars(i, to_app(g->form(m_ge[i])));
     }
     
     declassifier dcl(m_vars);
     expr_mark visited;        
     for (unsigned i = 0; !m_vars.empty() && i < m_other.size(); ++i) {
         for_each_expr(dcl, visited, g->form(m_other[i]));
     }
     
     if (m_vars.empty()) {
         return false;
     }
     
     // display_annotation(tout, g);
     m_progress = false;
     // first eliminate variables
     var_map::iterator it = next_resolvent(m_vars.begin()); 
     while (it != m_vars.end()) {            
         app * e = it->m_key;
         rec const& r = it->m_value;
         TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
         if (r.pos.empty()) {                
             replace(r.neg, e, m.mk_false(), g);
             mc.set_value(e, false);
         }
         else if (r.neg.empty()) {
             replace(r.pos, e, m.mk_true(), g);
             mc.set_value(e, true);
         }
         if (g->inconsistent()) return false;
         ++it;
         it = next_resolvent(it);
     }        
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:48,代码来源:pb_preprocess_tactic.cpp


示例12: operator

        void operator()(goal_ref const & g, 
                        goal_ref_buffer & result, 
                        model_converter_ref & mc, 
                        proof_converter_ref & pc,
                        expr_dependency_ref & core) {
            SASSERT(g->is_well_sorted());
            mc = 0; pc = 0; core = 0;
            tactic_report report("horn", *g);
            bool produce_proofs = g->proofs_enabled();

            if (produce_proofs) {                
                if (!m_ctx.get_params().generate_proof_trace()) {
                    params_ref params = m_ctx.get_params().p;
                    params.set_bool("generate_proof_trace", true);
                    updt_params(params);
                }
            }

            unsigned sz = g->size();
            expr_ref q(m), f(m);
            expr_ref_vector queries(m);
            std::stringstream msg;

            m_ctx.reset();
            m_ctx.ensure_opened();

            for (unsigned i = 0; i < sz; i++) {
                f = g->form(i);
                formula_kind k = get_formula_kind(f);
                switch(k) {
                case IS_RULE:
                    m_ctx.add_rule(f, symbol::null);
                    break;
                case IS_QUERY:
                    queries.push_back(f);
                    break;
                default: 
                    msg << "formula is not in Horn fragment: " << mk_pp(g->form(i), m) << "\n";
                    TRACE("horn", tout << msg.str(););
                    throw tactic_exception(msg.str().c_str());
                }
            }
开发者ID:CHolmes3,项目名称:z3,代码行数:42,代码来源:horn_tactic.cpp


示例13: reduce_core

 void reduce_core(goal_ref const& g, goal_ref_buffer& result) {
     init(g);
     m_context.push();
     assert_clauses(g);
     m_context.push();   // internalize assertions. 
     prune_clauses();
     goal_ref r(g);
     insert_result(r);
     r->elim_true();
     result.push_back(r.get());        
     m_context.pop(2);
     TRACE("unit_subsumption_tactic", g->display(tout); r->display(tout););
开发者ID:sukwon0709,项目名称:byterun,代码行数:12,代码来源:unit_subsumption_tactic.cpp


示例14: operator

    virtual void operator()(
        goal_ref const & g, 
        goal_ref_buffer & result, 
        model_converter_ref & mc, 
        proof_converter_ref & pc,
        expr_dependency_ref & core) {
        SASSERT(g->is_well_sorted());
        pc = 0; core = 0;

        if (g->proofs_enabled()) {
            throw tactic_exception("pb-preprocess does not support proofs");
        }

        pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
        mc = pp;

        g->inc_depth();        
        result.push_back(g.get());       
        while (simplify(g, *pp));
        // decompose(g);
    }
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:21,代码来源:pb_preprocess_tactic.cpp


示例15: operator

    void operator()(goal_ref const & g, goal_ref_buffer & result,
                    model_converter_ref & mc, proof_converter_ref & pc,
                    expr_dependency_ref & core) override {
        mc = nullptr;
        tactic_report report("collect-statistics", *g);

        collect_proc cp(m, m_stats);
        expr_mark visited;
        const unsigned sz = g->size();
        for (unsigned i = 0; i < sz; i++)
            for_each_expr(cp, visited, g->form(i));

        std::cout << "(" << std::endl;
        stats_type::iterator it = m_stats.begin();
        stats_type::iterator end = m_stats.end();
        for (; it != end; it++)
            std::cout << " :" << it->first << "    " << it->second << std::endl;
        std::cout << ")" << std::endl;

        g->inc_depth();
        result.push_back(g.get());
    }
开发者ID:chadbrewbaker,项目名称:z3,代码行数:22,代码来源:collect_statistics_tactic.cpp


示例16: operator

 void operator()(goal_ref const & g, 
                 goal_ref_buffer & result, 
                 model_converter_ref & mc, 
                 proof_converter_ref & pc,
                 expr_dependency_ref & core) {
     mc = 0; pc = 0; core = 0;
     
     if (!is_target(*g))
         throw tactic_exception("bv1 blaster cannot be applied to goal");
     
     tactic_report report("bv1-blaster", *g);
     m_num_steps = 0;
     
     bool proofs_enabled = g->proofs_enabled();
     expr_ref   new_curr(m());
     proof_ref  new_pr(m());
     unsigned   size = g->size();
     for (unsigned idx = 0; idx < size; idx++) {
         if (g->inconsistent())
             break;
         expr * curr = g->form(idx);
         m_rw(curr, new_curr, new_pr);
         m_num_steps += m_rw.get_num_steps();
         if (proofs_enabled) {
             proof * pr = g->pr(idx);
             new_pr     = m().mk_modus_ponens(pr, new_pr);
         }
         g->update(idx, new_curr, new_pr, g->dep(idx));
     }
     
     if (g->models_enabled())
         mc = mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits);
     g->inc_depth();
     result.push_back(g.get());
     m_rw.cfg().cleanup();
 }
开发者ID:CHolmes3,项目名称:z3,代码行数:36,代码来源:bv1_blaster_tactic.cpp


示例17: operator

 virtual void operator()(goal_ref const & in, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     double val = (*m_p)(*(in.get())).get_value();
     #pragma omp critical (probe_value_tactic)
     {
         if (m_msg)
             m_ctx.diagnostic_stream() << m_msg << " ";
         m_ctx.diagnostic_stream() << val;
         if (m_newline)
             m_ctx.diagnostic_stream() << std::endl;
     }
     skip_tactic::operator()(in, result, mc, pc, core);
 }
开发者ID:greatmazinger,项目名称:z3,代码行数:16,代码来源:echo_tactic.cpp


示例18: operator

 void operator()(goal_ref const & g, 
                 goal_ref_buffer & result) {
     tactic_report report("add-bounds", *g);
     bound_manager bm(m);
     expr_fast_mark1 visited;
     add_bound_proc proc(bm, *(g.get()), m_lower, m_upper);
     unsigned sz = g->size();
     for (unsigned i = 0; i < sz; i++)
         quick_for_each_expr(proc, visited, g->form(i));
     visited.reset();
     g->inc_depth();
     result.push_back(g.get());
     if (proc.m_num_bounds > 0) 
         g->updt_prec(goal::UNDER);
     report_tactic_progress(":added-bounds", proc.m_num_bounds);
     TRACE("add_bounds", g->display(tout););
开发者ID:NikolajBjorner,项目名称:z3,代码行数:16,代码来源:add_bounds_tactic.cpp


示例19: operator

 void operator()(goal_ref const & g,
                 goal_ref_buffer & result,
                 model_converter_ref & mc,
                 proof_converter_ref & pc,
                 expr_dependency_ref & core) override {
     mc = nullptr; pc = nullptr; core = nullptr;
     bool produce_proofs = g->proofs_enabled();
     tactic_report report("dt2bv", *g);
     unsigned   size = g->size();
     expr_fast_mark1 visited;
     check_fd proc(*this);
     for (unsigned i = 0; i < size; ++i) {
         quick_for_each_expr(proc, visited, g->form(i));
     }
     obj_hashtable<sort>::iterator it = m_non_fd_sorts.begin(), end = m_non_fd_sorts.end();
     for (; it != end; ++it) {
         m_fd_sorts.remove(*it);
     }
     if (!m_fd_sorts.empty()) {
         ref<extension_model_converter> ext = alloc(extension_model_converter, m);
         ref<filter_model_converter> filter = alloc(filter_model_converter, m);
         enum2bv_rewriter rw(m, m_params);
         rw.set_is_fd(&m_is_fd);            
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
         for (unsigned idx = 0; idx < size; idx++) {
             rw(g->form(idx), new_curr, new_pr);
             if (produce_proofs) {
                 proof * pr = g->pr(idx);
                 new_pr = m.mk_modus_ponens(pr, new_pr);
             }
             g->update(idx, new_curr, new_pr, g->dep(idx));
         }
         expr_ref_vector bounds(m);
         rw.flush_side_constraints(bounds);
         for (unsigned i = 0; i < bounds.size(); ++i) {
             g->assert_expr(bounds[i].get());
         }
         {
             obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
             for (; it != end; ++it) {
                 filter->insert(it->m_value);
             }
         }
         {
             obj_map<func_decl, expr*>::iterator it = rw.enum2def().begin(), end = rw.enum2def().end();
             for (; it != end; ++it) {
                 ext->insert(it->m_key, it->m_value);
             }
         }
         
         mc = concat(filter.get(), ext.get());
         report_tactic_progress(":fd-num-translated", rw.num_translated());
     }
     g->inc_depth();
     result.push_back(g.get());
     TRACE("dt2bv", g->display(tout););
开发者ID:chadbrewbaker,项目名称:z3,代码行数:57,代码来源:dt2bv_tactic.cpp


示例20: operator

 virtual void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
                         proof_converter_ref & pc,
                         expr_dependency_ref & core) {
     SASSERT(g->is_well_sorted());
     ast_manager & m = g->m();
     bool produce_proofs = g->proofs_enabled();
     rw r(m, produce_proofs);
     #pragma omp critical (tactic_cancel)
     {
         m_rw = &r;
     }
     mc = 0; pc = 0; core = 0; result.reset();
     tactic_report report("distribute-forall", *g);
     
     expr_ref   new_curr(m);
     proof_ref  new_pr(m);
     unsigned size = g->size();
     for (unsigned idx = 0; idx < size; idx++) {
         if (g->inconsistent())
             break;
         expr * curr = g->form(idx);
         r(curr, new_curr, new_pr);
         if (g->proofs_enabled()) {
             proof * pr = g->pr(idx);
             new_pr     = m.mk_modus_ponens(pr, new_pr);
         }
         g->update(idx, new_curr, new_pr, g->dep(idx));
     }
     
     g->inc_depth();
     result.push_back(g.get());
     TRACE("distribute-forall", g->display(tout););
开发者ID:killbug2004,项目名称:Snippets,代码行数:34,代码来源:distribute_forall_tactic.cpp



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


鲜花

握手

雷人

路过

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

请发表评论

全部评论

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