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

C++ cmd_context类代码示例

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

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



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

示例1: assert_exprs_from

/**
   \brief Assert expressions from ctx into t.
*/
void assert_exprs_from(cmd_context const & ctx, assertion_set & t) {
    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
    for (; it != end; ++it) {
        t.assert_expr(*it);
    }
}
开发者ID:Moondee,项目名称:Artemis,代码行数:10,代码来源:assertion_set.cpp


示例2: install_dl_cmds

void install_dl_cmds(cmd_context & ctx) {
    dl_context * dl_ctx = alloc(dl_context, ctx);
    ctx.insert(alloc(dl_rule_cmd, dl_ctx));
    ctx.insert(alloc(dl_query_cmd, dl_ctx));
    ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
    ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
    PRIVATE_PARAMS(ctx.insert(alloc(dl_push_cmd, dl_ctx));); // not exposed to keep command-extensions simple.
开发者ID:sukwon0709,项目名称:byterun,代码行数:7,代码来源:dl_cmds.cpp


示例3: execute

 virtual void execute(cmd_context & ctx) {
     ctx.regular_stream() << "\"";
     if (m_cmds.empty()) {
         vector<named_cmd> cmds;
         cmd_context::cmd_iterator it  = ctx.begin_cmds();
         cmd_context::cmd_iterator end = ctx.end_cmds();
         for (; it != end; ++it) {
             cmds.push_back(named_cmd((*it).m_key, (*it).m_value));
         }
         // named_cmd_lt is not a total order for commands, but this is irrelevant for Linux x Windows behavior
         std::sort(cmds.begin(), cmds.end(), named_cmd_lt());
         vector<named_cmd>::const_iterator it2  = cmds.begin();
         vector<named_cmd>::const_iterator end2 = cmds.end();
         for (; it2 != end2; ++it2) {
             display_cmd(ctx, it2->first, it2->second);
         }
     }
     else {
         svector<symbol>::const_iterator it  = m_cmds.begin();
         svector<symbol>::const_iterator end = m_cmds.end();
         for (; it != end; ++it) {
             cmd * c = ctx.find_cmd(*it);
             SASSERT(c);
             display_cmd(ctx, *it, c);
         }
     }
     ctx.regular_stream() << "\"\n";
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:28,代码来源:basic_cmds.cpp


示例4: print_certificate

 void print_certificate(cmd_context& ctx) {
     if (m_params.get_bool(":print-certificate", false)) {
         datalog::context& dlctx = m_dl_ctx->get_dl_context();
         if (!dlctx.display_certificate(ctx.regular_stream())) {
             throw cmd_exception("certificates are not supported for selected DL_ENGINE");
         }
         ctx.regular_stream() << "\n";
     }
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:9,代码来源:dl_cmds.cpp


示例5: set_background

 void set_background(cmd_context& ctx) {
     datalog::context& dlctx = m_dl_ctx->get_dl_context();
     ast_manager& m = ctx.m();                
     ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
     ptr_vector<expr>::const_iterator end = ctx.end_assertions();
     for (; it != end; ++it) {
         dlctx.assert_expr(*it);
     }
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:9,代码来源:dl_cmds.cpp


示例6: display_cmd

 void display_cmd(cmd_context & ctx, symbol const & s, cmd * c) {
     char const * usage = c->get_usage();
     char const * descr = c->get_descr(ctx);
     ctx.regular_stream() << " (" << s;
     if (usage)
         ctx.regular_stream() << " " << escaped(usage, true) << ")\n";
     else 
         ctx.regular_stream() << ")\n";
     if (descr) {
         ctx.regular_stream() << "    " << escaped(descr, true, 4) << "\n";
     }
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:12,代码来源:basic_cmds.cpp


示例7: print_statistics

 void print_statistics(cmd_context& ctx) {
     if (m_params.get_bool(":print-statistics", false)) {
         statistics st;
         datalog::context& dlctx = m_dl_ctx->get_dl_context();
         unsigned long long max_mem = memory::get_max_used_memory();
         unsigned long long mem = memory::get_allocation_size();
         dlctx.collect_statistics(st);
         st.update("time", ctx.get_seconds());            
         st.update("memory", static_cast<double>(mem)/static_cast<double>(1024*1024));
         st.update("max-memory", static_cast<double>(max_mem)/static_cast<double>(1024*1024));
         st.display_smt2(ctx.regular_stream());            
     }
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:13,代码来源:dl_cmds.cpp


示例8: print_answer

 void print_answer(cmd_context& ctx) {
     if (m_params.get_bool(":print-answer", false)) {
         datalog::context& dlctx = m_dl_ctx->get_dl_context();
         ast_manager& m = ctx.m();
         expr_ref query_result(dlctx.get_answer_as_formula(), m);
         sbuffer<symbol> var_names;
         unsigned num_decls = 0;
         if (is_quantifier(m_target)) {
             num_decls = to_quantifier(m_target)->get_num_decls();
         }
         ctx.display(ctx.regular_stream(), query_result, 0, num_decls, "X", var_names);
         ctx.regular_stream() << std::endl;
     }
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:14,代码来源:dl_cmds.cpp


示例9: execute

    virtual void execute(cmd_context & ctx) {
        if(m_arg_idx<2) {
            throw cmd_exception("at least 2 arguments expected");
        }
        ensure_domain(ctx);
        ast_manager& m = ctx.m();

        func_decl_ref pred(
            m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
        ctx.insert(pred);
        datalog::context& dctx = m_dl_ctx->get_dl_context();
        dctx.register_predicate(pred, false);
        if(!m_kinds.empty()) {
            dctx.set_predicate_representation(pred, m_kinds.size(), m_kinds.c_ptr());
        }
        m_domain = 0;
    }
开发者ID:sukwon0709,项目名称:byterun,代码行数:17,代码来源:dl_cmds.cpp


示例10: set_next_arg

 virtual void set_next_arg(cmd_context & ctx, expr * t) {
     SASSERT(m_idx == 0);
     if (!ctx.m().is_bool(t)) {
         throw cmd_exception("Invalid type for expression. Expected Boolean type.");
     }
     m_formula = t;
     ++m_idx;
 }
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:8,代码来源:opt_cmds.cpp


示例11: display

void assertion_set::display(cmd_context & ctx, std::ostream & out) const {
    out << "(assertion-set";
    unsigned sz = size();
    for (unsigned i = 0; i < sz; i++) {
        out << "\n  ";
        ctx.display(out, form(i), 2);
    }
    out << ")" << std::endl;
}
开发者ID:Moondee,项目名称:Artemis,代码行数:9,代码来源:assertion_set.cpp


示例12: set_next_arg

 virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
     cmd * c = ctx.find_cmd(s);
     if (c == 0) {
         std::string err_msg("unknown command '");
         err_msg = err_msg + s.bare_str() + "'";
         throw cmd_exception(err_msg);
     }
     m_cmds.push_back(s);
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:9,代码来源:basic_cmds.cpp


示例13: set_next_arg

 void set_next_arg(cmd_context & ctx, symbol const & s) override {
     cmd * c = ctx.find_cmd(s);
     if (c == nullptr) {
         std::string err_msg("unknown command '");
         err_msg = err_msg + s.bare_str() + "'";
         throw cmd_exception(std::move(err_msg));
     }
     m_cmds.push_back(s);
 }
开发者ID:NikolajBjorner,项目名称:z3,代码行数:9,代码来源:basic_cmds.cpp


示例14: execute

 void execute(cmd_context & ctx) override {
     ctx.regular_stream() << "\"";
     if (m_cmds.empty()) {
         vector<named_cmd> cmds;
         cmd_context::cmd_iterator it  = ctx.begin_cmds();
         cmd_context::cmd_iterator end = ctx.end_cmds();
         for (; it != end; ++it) {
             cmds.push_back(named_cmd((*it).m_key, (*it).m_value));
         }
         // named_cmd_lt is not a total order for commands, but this is irrelevant for Linux x Windows behavior
         std::sort(cmds.begin(), cmds.end(), named_cmd_lt());
         for (named_cmd const& nc : cmds) {
             display_cmd(ctx, nc.first, nc.second);
         }
     }
     else {
         for (symbol const& s : m_cmds) {
             cmd * c = ctx.find_cmd(s);
             SASSERT(c);
             display_cmd(ctx, s, c);
         }
     }
     ctx.regular_stream() << "\"\n";
 }
开发者ID:NikolajBjorner,项目名称:z3,代码行数:24,代码来源:basic_cmds.cpp


示例15: compute_interpolant_and_maybe_check

static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
    
    // create a fresh solver suitable for interpolation
    bool proofs_enabled, models_enabled, unsat_core_enabled;
    params_ref p;
    ast_manager &_m = ctx.m();
    // TODO: the following is a HACK to enable proofs in the old smt solver
    // When we stop using that solver, this hack can be removed
    scoped_proof_mode spm(_m,PGM_FINE);
    ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
    p.set_bool("proof", true);
    scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());

    ptr_vector<ast> cnsts;
    ptr_vector<ast> interps;
    model_ref m;
  
    // compute an interpolant
  
    lbool res;
    try {
        res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, 0);
    }
    catch (iz3_incompleteness &) {
        throw cmd_exception("incompleteness in interpolator");
    }

    switch(res){
    case l_false:
        ctx.regular_stream() << "unsat\n";
        show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
        break;

    case l_true:
        ctx.regular_stream() << "sat\n";
        // TODO: how to return the model to the context, if it exists?
        break;

    case l_undef:
        ctx.regular_stream() << "unknown\n";
        // TODO: how to return the model to the context, if it exists?
        break;
    }    

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

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


示例16: execute

    void execute(cmd_context & ctx) override {
        proof_ref pr(ctx.m());
        qe::simplify_rewriter_star qe(ctx.m());
        expr_ref result(ctx.m());

        qe(m_target, result, pr);            

        if (m_params.get_bool("print", true)) {
            ctx.display(ctx.regular_stream(), result);
            ctx.regular_stream() << std::endl; 
        }
        if (m_params.get_bool("print_statistics", false)) {
            statistics st;
            qe.collect_statistics(st);
            st.display(ctx.regular_stream());
        }
    }
开发者ID:NikolajBjorner,项目名称:z3,代码行数:17,代码来源:qe_cmd.cpp


示例17: get_interpolant_and_maybe_check

static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check) {

    check_can_interpolate(ctx);

    // get the proof, if there is one

    if (!ctx.has_manager() ||
        ctx.cs_state() != cmd_context::css_unsat)
        throw cmd_exception("proof is not available");
    expr_ref pr(ctx.m());
    pr = ctx.get_check_sat_result()->get_proof();
    if (pr == 0)
        throw cmd_exception("proof is not available");

    // get the assertions from the context

    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
    ptr_vector<ast> cnsts((unsigned)(end - it));
    for (int i = 0; it != end; ++it, ++i)
        cnsts[i] = *it;
    
    // compute an interpolant
  
    ptr_vector<ast> interps;
 
    try {
        iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,0);
    }
    catch (iz3_bad_tree &) {
        throw cmd_exception("interpolation pattern contains non-asserted formula");
    }
    catch (iz3_incompleteness &) {
        throw cmd_exception("incompleteness in interpolator");
    }

    show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:38,代码来源:interpolant_cmds.cpp


示例18: to_subpaving

static void to_subpaving(cmd_context & ctx, expr * t) {
    ast_manager & m = ctx.m();
    unsynch_mpq_manager qm;
    scoped_ptr<subpaving::context> s;
    s = subpaving::mk_mpq_context(ctx.m().limit(), qm);
    expr2var e2v(m);
    expr2subpaving e2s(m, *s, &e2v);
    params_ref p;
    p.set_bool("mul_to_power", true);
    th_rewriter simp(m, p);
    expr_ref t_s(m);
    simp(t, t_s);
    scoped_mpz n(qm), d(qm);
    ctx.regular_stream() << mk_ismt2_pp(t_s, m) << "\n=======>" << std::endl;
    subpaving::var x = e2s.internalize_term(t_s, n, d);
    expr2var::iterator it  = e2v.begin();
    expr2var::iterator end = e2v.end();
    for (; it != end; ++it) {
        ctx.regular_stream() << "x" << it->m_value << " := " << mk_ismt2_pp(it->m_key, m) << "\n";
    }
    s->display_constraints(ctx.regular_stream());
    ctx.regular_stream() << n << "/" << d << " x" << x << "\n";
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:23,代码来源:subpaving_cmds.cpp


示例19: ensure_domain

 void ensure_domain(cmd_context& ctx) {
     if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
 }
开发者ID:sukwon0709,项目名称:byterun,代码行数:3,代码来源:dl_cmds.cpp


示例20: store_expr_ref

void store_expr_ref(cmd_context & ctx, symbol const & v, expr * t) {
    ctx.insert(v, alloc(ast_object_ref, ctx, t));
}
开发者ID:CHolmes3,项目名称:z3,代码行数:3,代码来源:cmd_util.cpp



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


鲜花

握手

雷人

路过

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

请发表评论

全部评论

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