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

C++ params_ref类代码示例

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

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



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

示例1: _tactic_apply

    static Z3_apply_result _tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g, params_ref p) {
        goal_ref new_goal;
        new_goal = alloc(goal, *to_goal_ref(g));
        Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m());
        mk_c(c)->save_object(ref); 

        unsigned timeout     = p.get_uint("timeout", UINT_MAX);
        bool     use_ctrl_c  = p.get_bool("ctrl_c", false);
        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
        
        to_tactic_ref(t)->updt_params(p);

        api::context::set_interruptable si(*(mk_c(c)), eh);
        {
            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
            scoped_timer timer(timeout, &eh);
            try {
                exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_mc, ref->m_pc, ref->m_core);
                return of_apply_result(ref);
            }
            catch (z3_exception & ex) {
                mk_c(c)->handle_exception(ex);
                return 0;
            }
        }
    }
开发者ID:EinNarr,项目名称:z3,代码行数:26,代码来源:api_tactic.cpp


示例2: updt_params

 void updt_params(params_ref const & p) {
     m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     m_max_steps      = p.get_uint("max_steps", UINT_MAX);
     m_blast_add      = p.get_bool("blast_add", true);
     m_blast_mul      = p.get_bool("blast_mul", true);
     m_blast_full     = p.get_bool("blast_full", false);
     m_blast_quant    = p.get_bool("blast_quant", false);
     m_blaster.set_max_memory(m_max_memory);
 }
开发者ID:greatmazinger,项目名称:z3,代码行数:9,代码来源:bit_blaster_rewriter.cpp


示例3: show_interpolant_and_maybe_check

static void show_interpolant_and_maybe_check(cmd_context & ctx,
                                             ptr_vector<ast> &cnsts,
                                             expr *t, 
                                             ptr_vector<ast> &interps,
                                             params_ref &m_params,
                                             bool check)
{
  
    if (m_params.get_bool("som", false))
        m_params.set_bool("flat", true);
    th_rewriter s(ctx.m(), m_params);
  
    for(unsigned i = 0; i < interps.size(); i++){

        expr_ref r(ctx.m());
        proof_ref pr(ctx.m());
        s(to_expr(interps[i]),r,pr);

        ctx.regular_stream()  << mk_pp(r.get(), ctx.m()) << std::endl;
#if 0
        ast_smt_pp pp(ctx.m());
        pp.set_logic(ctx.get_logic().str().c_str());
        pp.display_smt2(ctx.regular_stream(), to_expr(interps[i]));
        ctx.regular_stream() << std::endl;
#endif
    }

    s.cleanup();

    // verify, for the paranoid...
    if(check || interp_params(m_params).check()){
        std::ostringstream err;
        ast_manager &_m = ctx.m();

        // need a solver -- make one here FIXME is this right?
        bool proofs_enabled, models_enabled, unsat_core_enabled;
        params_ref p;
        ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
        scoped_ptr<solver> sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());

        if(iz3check(_m,sp.get(),err,cnsts,t,interps))
            ctx.regular_stream() << "correct\n";
        else 
            ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
    }

    for(unsigned i = 0; i < interps.size(); i++){
        ctx.m().dec_ref(interps[i]);
    }

    interp_params itp_params(m_params);
    if(itp_params.profile())
        profiling::print(ctx.regular_stream());

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


示例4: updt_params

void sls_engine::updt_params(params_ref const & _p) {
    sls_params p(_p);
    m_produce_models = _p.get_bool("model", false);
    m_max_restarts = p.max_restarts();
    m_tracker.set_random_seed(p.random_seed());
    m_walksat = p.walksat();
    m_walksat_repick = p.walksat_repick();
    m_paws_sp = p.paws_sp();
    m_paws = m_paws_sp < 1024;
    m_wp = p.wp();
    m_vns_mc = p.vns_mc();
    m_vns_repick = p.vns_repick();

    m_restart_base = p.restart_base();
    m_restart_next = m_restart_base;
    m_restart_init = p.restart_init();

    m_early_prune = p.early_prune();
    m_random_offset = p.random_offset();
    m_rescore = p.rescore();

    // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
    if (m_walksat_repick && !m_walksat)
        NOT_IMPLEMENTED_YET();
    if (m_vns_repick && !m_walksat)
        NOT_IMPLEMENTED_YET();
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:27,代码来源:sls_engine.cpp


示例5: updt_params

 void updt_params(params_ref const & _p) {
     sls_params p(_p);
     m_produce_models = _p.get_bool("model", false);
     m_max_restarts = p.restarts();            
     m_tracker.set_random_seed(p.random_seed());
     m_plateau_limit = p.plateau_limit();
 }
开发者ID:Jornason,项目名称:z3,代码行数:7,代码来源:sls_tactic.cpp


示例6: dl_query_test_wpa

void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
    params.set_bool("magic_sets_for_queries", true);
    ast_manager m;
    random_gen ran(0);
    reg_decl_plugins(m);
    arith_util arith(m);
    const char * problem_dir = "C:\\tvm\\src\\z3_2\\debug\\test\\w0.datalog";
    dl_decl_util dl_util(m);

    std::cerr << "Testing queries on " << problem_dir <<"\n";
    register_engine re;
    context ctx(m, re, fparams);
    ctx.updt_params(params);
    {
        wpa_parser* p = wpa_parser::create(ctx, m);
        TRUSTME( p->parse_directory(problem_dir) );
        dealloc(p);
    }

    const unsigned attempts = 10;

    func_decl * v_pred = ctx.try_get_predicate_decl(symbol("V"));
    SASSERT(v_pred);
    sort * var_sort = v_pred->get_domain(0);

    uint64 var_sz;
    TRUSTME( ctx.try_get_sort_constant_count(var_sort, var_sz) );

    for(unsigned attempt=0; attempt<attempts; attempt++) {
        unsigned el1 = ran()%var_sz;
        unsigned el2 = ran()%var_sz;

        expr_ref_vector q_args(m);
        q_args.push_back(dl_util.mk_numeral(el1, var_sort));
        q_args.push_back(dl_util.mk_numeral(el2, var_sort));

        app_ref query_lit(m.mk_app(v_pred, q_args.c_ptr()), m);
        lbool is_sat = ctx.query(query_lit);
        SASSERT(is_sat != l_undef);
        bool found = is_sat == l_true;
        std::cerr<<"query finished: "<<found<<"\n";

        relation_fact ans_fact(m);
        ans_fact.push_back(to_app(q_args.back()));

        q_args.pop_back();
        q_args.push_back(m.mk_var(0, var_sort));

        query_lit = m.mk_app(v_pred, q_args.c_ptr());
        is_sat = ctx.query(query_lit.get());
        SASSERT(is_sat != l_false);
        std::cerr<<"non-ground query finished\n";
        if(ctx.result_contains_fact(ans_fact)!=found) {
            std::cerr<<"wrong wpa answer!\n";
            UNREACHABLE();
        }
    }

}
开发者ID:jackluo923,项目名称:juxta,代码行数:59,代码来源:dl_query.cpp


示例7: merge_default_params

params_ref context_params::merge_default_params(params_ref const & p) {
    if (!m_auto_config && !p.contains("auto_config")) {
        params_ref new_p = p;
        new_p.set_bool("auto_config", false);
        return new_p;
    }
    else {
        return p;
    }
}
开发者ID:Jornason,项目名称:z3,代码行数:10,代码来源:context_params.cpp


示例8: updt_local_params

void smt_params::updt_local_params(params_ref const & _p) {
    smt_params_helper p(_p);
    m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
    m_random_seed = p.random_seed();
    m_relevancy_lvl = p.relevancy();
    m_ematching   = p.ematching();
    m_phase_selection = static_cast<phase_selection>(p.phase_selection());
    m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
    m_restart_factor = p.restart_factor();
    m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
    m_delay_units = p.delay_units();
    m_delay_units_threshold = p.delay_units_threshold();
    m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
    m_soft_timeout = p.soft_timeout();
    model_params mp(_p);
    m_model_compact = mp.compact();
    if (_p.get_bool("arith.greatest_error_pivot", false))
        m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
    else if (_p.get_bool("arith.least_error_pivot", false))
        m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
    theory_array_params::updt_params(_p);
}
开发者ID:therealoneisneo,项目名称:Z3,代码行数:22,代码来源:smt_params.cpp


示例9: get_value

 std::string get_value(char const * name) {
     std::string r;
     bool error = false;
     std::string error_msg;
     #pragma omp critical (gparams)
     {
         try {
             symbol m, p;
             normalize(name, m, p);
             if (m == symbol::null) {
                 if (m_params.contains(p)) {
                     r = get_value(m_params, p);
                 }
                 else {
                     r = get_default(get_param_descrs(), p, m);
                 }
             }
             else {
                 params_ref * ps = nullptr;
                 if (m_module_params.find(m, ps) && ps->contains(p)) {
                     r = get_value(*ps, p);
                 }
                 else {
                     param_descrs * d;
                     if (get_module_param_descrs().find(m, d)) {
                         r = get_default(*d, p, m);
                     }
                     else {
                         std::stringstream strm;
                         strm << "unknown module '" << m << "'";
                         throw exception(strm.str());
                     }
                 }
             }
         }
         catch (z3_exception & ex) {
             // Exception cannot cross critical section boundaries.
             error = true;
             error_msg = ex.msg();
         }
     }
     if (error)
         throw exception(std::move(error_msg));
     return r;
 }
开发者ID:levnach,项目名称:z3,代码行数:45,代码来源:gparams.cpp


示例10: updt_params

 virtual void updt_params(params_ref const & p) {
     m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true);
     m_aig_per_assertion = p.get_bool("aig_per_assertion", true); 
 }
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:5,代码来源:aig_tactic.cpp


示例11: updt_params

void context_params::updt_params(params_ref const & p) {
    m_timeout           = p.get_uint("timeout", UINT_MAX);
    m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", true));
    m_auto_config       = p.get_bool("auto_config", true);
    m_proof             = p.get_bool("proof", false);
    m_model             = p.get_bool("model", true);
    m_model_validate    = p.get_bool("model_validate", false);
    m_trace             = p.get_bool("trace", false);
    m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
    m_unsat_core        = p.get_bool("unsat_core", false);
    m_debug_ref_count   = p.get_bool("debug_ref_count", false);
    m_smtlib2_compliant = p.get_bool("smtlib2_compliant", false);
}
开发者ID:Jornason,项目名称:z3,代码行数:13,代码来源:context_params.cpp


示例12: get_double

double params_ref::get_double(char const * k, params_ref const & fallback, double _default) const {
    return m_params ? m_params->get_double(k, fallback, _default) : fallback.get_double(k, _default);
}
开发者ID:greatmazinger,项目名称:z3,代码行数:3,代码来源:params.cpp


示例13: updt_params

 void updt_params(params_ref const & p) {
     m_fparams.m_nlquant_elim = p.get_bool(":qe-nonlinear", false);
     m_qe.updt_params(p);
 }
开发者ID:Moondee,项目名称:Artemis,代码行数:4,代码来源:qe_tactic.cpp


示例14: params2front_end_params

/**
   Update front_end_params using s.
   Only the most frequently used options are updated.

   This function is mainly used to allow smt::context to be used in
   the new strategy framework.
*/
void params2front_end_params(params_ref const & s, front_end_params & t) {
    t.m_quant_elim = s.get_bool(":elim-quant", t.m_quant_elim);
    t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl);
    TRACE("qi_cost", s.display(tout); tout << "\n";);
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:11,代码来源:params2front_end_params.cpp


示例15: get_solver_params

void context_params::get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled) {
    proofs_enabled     = m.proofs_enabled() && p.get_bool("proof", m_proof);
    models_enabled     = p.get_bool("model", m_model);
    unsat_core_enabled = p.get_bool("unsat_core", m_unsat_core);
    p = merge_default_params(p);
}
开发者ID:Jornason,项目名称:z3,代码行数:6,代码来源:context_params.cpp


示例16: updt_params_core

 void updt_params_core(params_ref const & p) {
     m_normalize_int_only = p.get_bool("norm_int_only", true);
 }
开发者ID:jawline,项目名称:z3,代码行数:3,代码来源:normalize_bounds_tactic.cpp


示例17: get_bool

bool params_ref::get_bool(char const * k, params_ref const & fallback, bool _default) const {
    return m_params ? m_params->get_bool(k, fallback, _default) : fallback.get_bool(k, _default);
}
开发者ID:greatmazinger,项目名称:z3,代码行数:3,代码来源:params.cpp


示例18:

void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) {
    m_max_memory        = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
    m_max_steps         = p.get_uint("max_steps", UINT_MAX);
    updt_local_params(p);
}
开发者ID:martin-neuhaeusser,项目名称:z3,代码行数:5,代码来源:fpa2bv_rewriter.cpp


示例19: get_sym

symbol params_ref::get_sym(char const * k, params_ref const & fallback, symbol const & _default) const {
    return m_params ? m_params->get_sym(k, fallback, _default) : fallback.get_sym(k, _default);
}
开发者ID:greatmazinger,项目名称:z3,代码行数:3,代码来源:params.cpp


示例20:

void bv2int_rewriter_ctx::update_params(params_ref const& p) {
    m_max_size = p.get_uint("max_bv_size", UINT_MAX);
}
开发者ID:kayceesrk,项目名称:Z3,代码行数:3,代码来源:bv2int_rewriter.cpp



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


鲜花

握手

雷人

路过

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

请发表评论

全部评论

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