C++ RESET_ERROR_CODE函数代码示例

OStack程序员社区-中国程序员成长平台 › 门户 › 编程› C++›C++教程

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

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

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

示例1: Z3_algebraic_div

 Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b) {
     Z3_TRY;
     LOG_Z3_algebraic_div(c, a, b);
     RESET_ERROR_CODE();
     CHECK_IS_ALGEBRAIC_X(a, 0);
     CHECK_IS_ALGEBRAIC_X(b, 0);
     if ((is_rational(c, b) && get_rational(c, b).is_zero()) ||
         (!is_rational(c, b) && am(c).is_zero(get_irrational(c, b)))) {
         SET_ERROR_CODE(Z3_INVALID_ARG);
         RETURN_Z3(0);
     }
     BIN_OP(/,div);
     Z3_CATCH_RETURN(0);
 }

开发者ID:CHolmes3，项目名称:z3，代码行数:14，代码来源:api_algebraic.cpp

示例2: Z3_mk_fpa_to_sbv

 Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz) {
     Z3_TRY;
     LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
     RESET_ERROR_CODE();
     if (!is_rm(c, rm) || !is_fp(c, t)) {
         SET_ERROR_CODE(Z3_INVALID_ARG, "rm and float sorts expected");
         RETURN_Z3(nullptr);
     }
     api::context * ctx = mk_c(c);
     expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz);
     ctx->save_ast_trail(a);
     RETURN_Z3(of_expr(a));
     Z3_CATCH_RETURN(nullptr);
 }

开发者ID:angr，项目名称:angr-z3，代码行数:14，代码来源:api_fpa.cpp

示例3: Z3_mk_fpa_to_real

 Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t) {
     Z3_TRY;
     LOG_Z3_mk_fpa_to_real(c, t);
     RESET_ERROR_CODE();
     if (!is_fp(c, t)) {
         SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");
         RETURN_Z3(nullptr);
     }
     api::context * ctx = mk_c(c);
     expr * a = ctx->fpautil().mk_to_real(to_expr(t));
     ctx->save_ast_trail(a);
     RETURN_Z3(of_expr(a));
     Z3_CATCH_RETURN(nullptr);
 }

开发者ID:angr，项目名称:angr-z3，代码行数:14，代码来源:api_fpa.cpp

示例4: Z3_mk_fpa_fp

 Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) {
     Z3_TRY;
     LOG_Z3_mk_fpa_fp(c, sgn, exp, sig);
     RESET_ERROR_CODE();
     if (!is_bv(c, sgn) || !is_bv(c, exp) || !is_bv(c, sig)) {
         SET_ERROR_CODE(Z3_INVALID_ARG);
         RETURN_Z3(nullptr);
     }
     api::context * ctx = mk_c(c);
     expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(exp), to_expr(sig));
     ctx->save_ast_trail(a);
     RETURN_Z3(of_expr(a));
     Z3_CATCH_RETURN(nullptr);
 }

开发者ID:chadbrewbaker，项目名称:z3，代码行数:14，代码来源:api_fpa.cpp

示例5: Z3_mk_fpa_min

 Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) {
     Z3_TRY;
     LOG_Z3_mk_fpa_min(c, t1, t2);
     RESET_ERROR_CODE();
     if (!is_fp(c, t1) || !is_fp(c, t2)) {
         SET_ERROR_CODE(Z3_INVALID_ARG);
         RETURN_Z3(nullptr);
     }
     api::context * ctx = mk_c(c);
     expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2));
     ctx->save_ast_trail(a);
     RETURN_Z3(of_expr(a));
     Z3_CATCH_RETURN(nullptr);
 }

开发者ID:chadbrewbaker，项目名称:z3，代码行数:14，代码来源:api_fpa.cpp

示例6: Z3_get_pattern_num_terms

 unsigned Z3_API Z3_get_pattern_num_terms(Z3_context c, Z3_pattern p) {
     Z3_TRY;
     LOG_Z3_get_pattern_num_terms(c, p);
     RESET_ERROR_CODE();
     app* _p = to_pattern(p);
     if (mk_c(c)->m().is_pattern(_p)) {
         return _p->get_num_args();
     }
     else {
         SET_ERROR_CODE(Z3_SORT_ERROR);
         return 0;            
     }
     Z3_CATCH_RETURN(0);
 }

开发者ID:AleksandarZeljic，项目名称:z3，代码行数:14，代码来源:api_quant.cpp

示例7: Z3_get_guessed_literals

 Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c) {
     Z3_TRY;
     LOG_Z3_get_guessed_literals(c);
     RESET_ERROR_CODE();
     ast_manager& m = mk_c(c)->m();
     expr_ref_vector lits(m);
     mk_c(c)->get_smt_kernel().get_guessed_literals(lits);        
     labels* lbls = alloc(labels);
     for (unsigned i = 0; i < lits.size(); ++i) {
         lbls->push_back(labeled_literal(m,lits[i].get()));
     }
     RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));        
     Z3_CATCH_RETURN(0);
 }

开发者ID:CharudattaSChitale，项目名称:sygus-comp14，代码行数:14，代码来源:api_solver_old.cpp

示例8: Z3_apply_result_to_string

 Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r) {
     Z3_TRY;
     LOG_Z3_apply_result_to_string(c, r);
     RESET_ERROR_CODE();
     std::ostringstream buffer;
     buffer << "(goals\n";
     unsigned sz = to_apply_result(r)->m_subgoals.size();
     for (unsigned i = 0; i < sz; i++) {
         to_apply_result(r)->m_subgoals[i]->display(buffer);
     }
     buffer << ")";
     return mk_c(c)->mk_external_string(buffer.str());
     Z3_CATCH_RETURN("");
 }

开发者ID:EinNarr，项目名称:z3，代码行数:14，代码来源:api_tactic.cpp

示例9: Z3_add_const_interp

 void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) {
     Z3_TRY;
     LOG_Z3_add_const_interp(c, m, f, a);
     RESET_ERROR_CODE();
     func_decl* d = to_func_decl(f);
     if (!d || d->get_arity() != 0) {
         SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
     }
     else {
         model* mdl = to_model_ref(m);
         mdl->register_decl(d, to_expr(a));
     }
     Z3_CATCH;
 }

开发者ID:NikolajBjorner，项目名称:z3，代码行数:14，代码来源:api_model.cpp

示例10: Z3_get_array_sort_range

 Z3_sort Z3_API Z3_get_array_sort_range(Z3_context c, Z3_sort t) {
     Z3_TRY;
     LOG_Z3_get_array_sort_range(c, t);
     RESET_ERROR_CODE();
     CHECK_VALID_AST(t, 0);
     if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
             to_sort(t)->get_decl_kind() == ARRAY_SORT) {
         Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());
         RETURN_Z3(r);
     }
     SET_ERROR_CODE(Z3_INVALID_ARG);
     RETURN_Z3(0);
     Z3_CATCH_RETURN(0);
 }

开发者ID:0Chuzz，项目名称:z3，代码行数:14，代码来源:api_array.cpp

示例11: Z3_model_eval

 Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v) {
     Z3_TRY;
     LOG_Z3_model_eval(c, m, t, model_completion, v);
     if (v) *v = 0;
     RESET_ERROR_CODE();
     CHECK_NON_NULL(m, Z3_FALSE);
     model * _m = to_model_ref(m);
     expr_ref result(mk_c(c)->m());
     _m->eval(to_expr(t), result, model_completion == Z3_TRUE);
     mk_c(c)->save_ast_trail(result.get());
     *v = of_ast(result.get());
     RETURN_Z3_model_eval Z3_TRUE;
     Z3_CATCH_RETURN(0);
 }

开发者ID:kayceesrk，项目名称:Z3，代码行数:14，代码来源:api_model.cpp

示例12: Z3_mk_array_default

    Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) {
        Z3_TRY;
        LOG_Z3_mk_array_default(c, array);
        RESET_ERROR_CODE();
        ast_manager & m = mk_c(c)->m();
        expr * _a        = to_expr(array);

        func_decl * f   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_ARRAY_DEFAULT, 0, 0, 1, &_a);
        app * r        = m.mk_app(f, 1, &_a);
        mk_c(c)->save_ast_trail(r);
        check_sorts(c, r);
        RETURN_Z3(of_ast(r));
        Z3_CATCH_RETURN(0);
    }

开发者ID:0Chuzz，项目名称:z3，代码行数:14，代码来源:api_array.cpp

示例13: Z3_add_func_interp

 Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) {
     Z3_TRY;
     LOG_Z3_add_func_interp(c, m, f, else_val);
     RESET_ERROR_CODE();
     func_decl* d = to_func_decl(f);
     model* mdl = to_model_ref(m);
     Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); 
     f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity());
     mk_c(c)->save_object(f_ref);
     mdl->register_decl(d, f_ref->m_func_interp);
     f_ref->m_func_interp->set_else(to_expr(else_val));
     RETURN_Z3(of_func_interp(f_ref));
     Z3_CATCH_RETURN(nullptr);
 }

开发者ID:chadbrewbaker，项目名称:z3，代码行数:14，代码来源:api_model.cpp

示例14: Z3_is_numeral_ast

 Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) {
     Z3_TRY;
     LOG_Z3_is_numeral_ast(c, a);
     RESET_ERROR_CODE();        
     CHECK_IS_EXPR(a, Z3_FALSE);
     expr* e = to_expr(a);
     return
         mk_c(c)->autil().is_numeral(e) ||
         mk_c(c)->bvutil().is_numeral(e) ||
         mk_c(c)->fpautil().is_numeral(e) ||
         mk_c(c)->fpautil().is_rm_numeral(e) ||
         mk_c(c)->datalog_util().is_numeral_ext(e);
     Z3_CATCH_RETURN(Z3_FALSE);
 }

开发者ID:angr，项目名称:angr-z3，代码行数:14，代码来源:api_numeral.cpp

示例15: Z3_get_quantifier_num_no_patterns

 unsigned Z3_API Z3_get_quantifier_num_no_patterns(Z3_context c, Z3_ast a) {
     Z3_TRY;
     LOG_Z3_get_quantifier_num_no_patterns(c, a);
     RESET_ERROR_CODE();
     ast * _a = to_ast(a);
     if (_a->get_kind() == AST_QUANTIFIER) {
         return to_quantifier(_a)->get_num_no_patterns();
     }
     else {
         SET_ERROR_CODE(Z3_SORT_ERROR);
         return 0;
     }
     Z3_CATCH_RETURN(0);
 }

开发者ID:AleksandarZeljic，项目名称:z3，代码行数:14，代码来源:api_quant.cpp

示例16: Z3_solver_get_assertions

 Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s) {
     Z3_TRY;
     LOG_Z3_solver_get_assertions(c, s);
     RESET_ERROR_CODE();
     init_solver(c, s);
     Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
     mk_c(c)->save_object(v);
     unsigned sz = to_solver_ref(s)->get_num_assertions();
     for (unsigned i = 0; i < sz; i++) {
         v->m_ast_vector.push_back(to_solver_ref(s)->get_assertion(i));
     }
     RETURN_Z3(of_ast_vector(v));
     Z3_CATCH_RETURN(0);
 }

开发者ID:ai-se，项目名称:z3，代码行数:14，代码来源:api_solver.cpp

示例17: Z3_get_quantifier_bound_name

 Z3_symbol Z3_API Z3_get_quantifier_bound_name(Z3_context c, Z3_ast a, unsigned i) {
     Z3_TRY;
     LOG_Z3_get_quantifier_bound_name(c, a, i);
     RESET_ERROR_CODE();
     ast * _a = to_ast(a);
     if (_a->get_kind() == AST_QUANTIFIER) {
         return of_symbol(to_quantifier(_a)->get_decl_names()[i]);
     }
     else {
         SET_ERROR_CODE(Z3_SORT_ERROR);
         return 0;
     }
     Z3_CATCH_RETURN(0);
 }

开发者ID:AleksandarZeljic，项目名称:z3，代码行数:14，代码来源:api_quant.cpp

示例18: Z3_solver_get_proof

 Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s) {
     Z3_TRY;
     LOG_Z3_solver_get_proof(c, s);
     RESET_ERROR_CODE();
     init_solver(c, s);
     proof * p = to_solver_ref(s)->get_proof();
     if (!p) {
         SET_ERROR_CODE(Z3_INVALID_USAGE);
         RETURN_Z3(0);
     }
     mk_c(c)->save_ast_trail(p);
     RETURN_Z3(of_ast(p));
     Z3_CATCH_RETURN(0);
 }

开发者ID:ai-se，项目名称:z3，代码行数:14，代码来源:api_solver.cpp

示例19: Z3_check_assumptions

 Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, 
                                      unsigned num_assumptions, Z3_ast const assumptions[], 
                                      Z3_model * m, Z3_ast* proof, 
                                      unsigned* core_size, Z3_ast core[]) {
     Z3_TRY;
     LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core);
     RESET_ERROR_CODE();
     CHECK_SEARCHING(c);
     expr * const* _assumptions = to_exprs(assumptions);
     flet<bool> _model(mk_c(c)->fparams().m_model, true);
     cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
     api::context::set_interruptable(*(mk_c(c)), eh);
     lbool result;
     result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
     if (result != l_false && m) {
         model_ref _m;
         mk_c(c)->get_smt_kernel().get_model(_m);
         if (_m) {
             Z3_model_ref * m_ref = alloc(Z3_model_ref); 
             m_ref->m_model = _m;
             // Must bump reference counter for backward compatibility reasons.
             // Don't need to invoke save_object, since the counter was bumped
             m_ref->inc_ref(); 
             *m = of_model(m_ref);
         }
         else {
             *m = 0;
         }
     }
     if (result == l_false && core_size) {
         *core_size = mk_c(c)->get_smt_kernel().get_unsat_core_size();
         if (*core_size > num_assumptions) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
         }
         for (unsigned i = 0; i < *core_size; ++i) {
             core[i] = of_ast(mk_c(c)->get_smt_kernel().get_unsat_core_expr(i));
         }
     }
     else if (core_size) {
         *core_size = 0;
     }
     if (result == l_false && proof) {
         *proof = of_ast(mk_c(c)->get_smt_kernel().get_proof());
     }
     else if (proof) {
         *proof = 0; // breaks abstraction.
     }
     RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);         
     Z3_CATCH_RETURN(Z3_L_UNDEF);
 }

开发者ID:CharudattaSChitale，项目名称:sygus-comp14，代码行数:50，代码来源:api_solver_old.cpp

示例20: Z3_solver_get_statistics

 Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s) {
     Z3_TRY;
     LOG_Z3_solver_get_statistics(c, s);
     RESET_ERROR_CODE();
     init_solver(c, s);
     Z3_stats_ref * st = alloc(Z3_stats_ref);
     to_solver_ref(s)->collect_statistics(st->m_stats);
     get_memory_statistics(st->m_stats);
     get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);
     mk_c(c)->save_object(st);
     Z3_stats r = of_stats(st);
     RETURN_Z3(r);
     Z3_CATCH_RETURN(0);
 }

开发者ID:ai-se，项目名称:z3，代码行数:14，代码来源:api_solver.cpp

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