本文整理汇总了C++中RETURN_Z3函数的典型用法代码示例。如果您正苦于以下问题:C++ RETURN_Z3函数的具体用法?C++ RETURN_Z3怎么用?C++ RETURN_Z3使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了RETURN_Z3函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的C++代码示例。
示例1: Z3_get_model_func_else
Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i) {
Z3_TRY;
LOG_Z3_get_model_func_else(c, m, i);
RESET_ERROR_CODE();
CHECK_NON_NULL(m, 0);
Z3_func_decl d = get_model_func_decl_core(c, m, i);
if (d) {
model * _m = to_model_ref(m);
func_interp * g = _m->get_func_interp(to_func_decl(d));
if (g) {
expr * e = g->get_else();
mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_ast(e));
}
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
开发者ID:kayceesrk,项目名称:Z3,代码行数:20,代码来源:api_model.cpp
示例2: Z3_tactic_apply_ex
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p) {
Z3_TRY;
LOG_Z3_tactic_apply_ex(c, t, g, p);
RESET_ERROR_CODE();
param_descrs pd;
to_tactic_ref(t)->collect_param_descrs(pd);
to_param_ref(p).validate(pd);
Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
开发者ID:EinNarr,项目名称:z3,代码行数:11,代码来源:api_tactic.cpp
示例3: Z3_mk_fixedpoint
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_fixedpoint(c);
RESET_ERROR_CODE();
Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref, *mk_c(c));
d->m_datalog = alloc(api::fixedpoint_context, mk_c(c)->m(), mk_c(c)->fparams());
mk_c(c)->save_object(d);
Z3_fixedpoint r = of_datalog(d);
RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr);
}
开发者ID:angr,项目名称:angr-z3,代码行数:11,代码来源:api_datalog.cpp
示例4: Z3_get_smtlib_assumption
Z3_ast Z3_API Z3_get_smtlib_assumption(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_assumption(c, i);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
if (i < mk_c(c)->m_smtlib_parser->get_benchmark()->get_num_axioms()) {
ast * a = mk_c(c)->m_smtlib_parser->get_benchmark()->begin_axioms()[i];
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:20,代码来源:api_parsers.cpp
示例5: Z3_model_translate
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context target) {
Z3_TRY;
LOG_Z3_model_translate(c, m, target);
RESET_ERROR_CODE();
Z3_model_ref* dst = alloc(Z3_model_ref, *mk_c(target));
ast_translation tr(mk_c(c)->m(), mk_c(target)->m());
dst->m_model = to_model_ref(m)->translate(tr);
mk_c(target)->save_object(dst);
RETURN_Z3(of_model(dst));
Z3_CATCH_RETURN(nullptr);
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:11,代码来源:api_model.cpp
示例6: Z3_tactic_get_param_descrs
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t) {
Z3_TRY;
LOG_Z3_tactic_get_param_descrs(c, t);
RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
mk_c(c)->save_object(d);
to_tactic_ref(t)->collect_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
开发者ID:EinNarr,项目名称:z3,代码行数:11,代码来源:api_tactic.cpp
示例7: Z3_mk_fpa_to_fp_bv
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) {
Z3_TRY;
LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);
RESET_ERROR_CODE();
if (!is_bv(c, bv) || !is_fp_sort(c, s)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "bv then fp sort expected");
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!ctx->bvutil().is_bv(to_expr(bv)) ||
!fu.is_float(to_sort(s))) {
SET_ERROR_CODE(Z3_INVALID_ARG, "bv sort the flaot sort expected");
return nullptr;
}
expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(nullptr);
}
开发者ID:angr,项目名称:angr-z3,代码行数:20,代码来源:api_fpa.cpp
示例8: Z3_solver_translate
Z3_solver Z3_API Z3_solver_translate(Z3_context c, Z3_solver s, Z3_context target) {
Z3_TRY;
LOG_Z3_solver_translate(c, s, target);
RESET_ERROR_CODE();
params_ref const& p = to_solver(s)->m_params;
Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
mk_c(target)->save_object(sr);
Z3_solver r = of_solver(sr);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
开发者ID:ai-se,项目名称:z3,代码行数:12,代码来源:api_solver.cpp
示例9: Z3_goal_translate
Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) {
Z3_TRY;
LOG_Z3_goal_translate(c, g, target);
RESET_ERROR_CODE();
ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
Z3_goal_ref * _r = alloc(Z3_goal_ref);
_r->m_goal = to_goal_ref(g)->translate(translator);
mk_c(target)->save_object(_r);
Z3_goal r = of_goal(_r);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
开发者ID:Moondee,项目名称:Artemis,代码行数:12,代码来源:api_goal.cpp
示例10: Z3_mk_bv_numeral
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) {
Z3_TRY;
LOG_Z3_mk_bv_numeral(c, sz, bits);
RESET_ERROR_CODE();
rational r(0);
for (unsigned i = 0; i < sz; ++i) {
if (bits[i]) r += rational::power_of_two(i);
}
ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz));
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(nullptr);
}
开发者ID:angr,项目名称:angr-z3,代码行数:12,代码来源:api_numeral.cpp
示例11: Z3_func_interp_get_else
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f) {
Z3_TRY;
LOG_Z3_func_interp_get_else(c, f);
RESET_ERROR_CODE();
CHECK_NON_NULL(f, nullptr);
expr * e = to_func_interp_ref(f)->get_else();
if (e) {
mk_c(c)->save_ast_trail(e);
}
RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(nullptr);
}
开发者ID:NikolajBjorner,项目名称:z3,代码行数:12,代码来源:api_model.cpp
示例12: Z3_param_descrs_get_name
Z3_symbol Z3_API Z3_param_descrs_get_name(Z3_context c, Z3_param_descrs p, unsigned i) {
Z3_TRY;
LOG_Z3_param_descrs_get_name(c, p, i);
RESET_ERROR_CODE();
if (i >= to_param_descrs_ptr(p)->size()) {
SET_ERROR_CODE(Z3_IOB);
RETURN_Z3(0);
}
Z3_symbol result = of_symbol(to_param_descrs_ptr(p)->get_param_name(i));
return result;
Z3_CATCH_RETURN(0);
}
开发者ID:CHolmes3,项目名称:z3,代码行数:12,代码来源:api_params.cpp
示例13: Z3_get_context_assignment
Z3_ast Z3_API Z3_get_context_assignment(Z3_context c) {
Z3_TRY;
LOG_Z3_get_context_assignment(c);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
expr_ref result(m);
expr_ref_vector assignment(m);
mk_c(c)->get_smt_kernel().get_assignments(assignment);
result = mk_c(c)->mk_and(assignment.size(), assignment.c_ptr());
RETURN_Z3(of_ast(result.get()));
Z3_CATCH_RETURN(0);
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:12,代码来源:api_solver_old.cpp
示例14: 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);
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
开发者ID:therealoneisneo,项目名称:Z3,代码行数:12,代码来源:api_solver.cpp
示例15: Z3_get_smtlib_sort
Z3_sort Z3_API Z3_get_smtlib_sort(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_sort(c, i);
RESET_ERROR_CODE();
if (mk_c(c)->m_smtlib_parser) {
mk_c(c)->extract_smtlib_parser_decls();
if (i < mk_c(c)->m_smtlib_parser_sorts.size()) {
sort* s = mk_c(c)->m_smtlib_parser_sorts[i];
mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:21,代码来源:api_parsers.cpp
示例16: Z3_get_smtlib_decl
Z3_func_decl Z3_API Z3_get_smtlib_decl(Z3_context c, unsigned i) {
Z3_TRY;
LOG_Z3_get_smtlib_decl(c, i);
RESET_ERROR_CODE();
mk_c(c)->extract_smtlib_parser_decls();
if (mk_c(c)->m_smtlib_parser) {
if (i < mk_c(c)->m_smtlib_parser_decls.size()) {
func_decl * d = mk_c(c)->m_smtlib_parser_decls[i];
mk_c(c)->save_ast_trail(d);
RETURN_Z3(of_func_decl(d));
}
else {
SET_ERROR_CODE(Z3_IOB);
}
}
else {
SET_ERROR_CODE(Z3_NO_PARSER);
}
RETURN_Z3(0);
Z3_CATCH_RETURN(0);
}
开发者ID:CharudattaSChitale,项目名称:sygus-comp14,代码行数:21,代码来源:api_parsers.cpp
示例17: Z3_rcf_mk_rational
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
Z3_TRY;
LOG_Z3_rcf_mk_rational(c, val);
RESET_ERROR_CODE();
reset_rcf_cancel(c);
scoped_mpq q(rcfm(c).qm());
rcfm(c).qm().set(q, val);
rcnumeral r;
rcfm(c).set(r, q);
RETURN_Z3(from_rcnumeral(r));
Z3_CATCH_RETURN(0);
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:12,代码来源:api_rcf.cpp
示例18: Z3_mk_probe
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name) {
Z3_TRY;
LOG_Z3_mk_probe(c, name);
RESET_ERROR_CODE();
probe_info * p = mk_c(c)->find_probe(symbol(name));
if (p == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
probe * new_p = p->get();
RETURN_PROBE(new_p);
Z3_CATCH_RETURN(0);
}
开发者ID:EinNarr,项目名称:z3,代码行数:13,代码来源:api_tactic.cpp
示例19: Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
Z3_ast const args[], unsigned k) {
Z3_TRY;
LOG_Z3_mk_atmost(c, num_args, args, k);
RESET_ERROR_CODE();
parameter param(k);
pb_util util(mk_c(c)->m());
ast* a = util.mk_at_most_k(num_args, to_exprs(args), k);
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
开发者ID:AleksandarZeljic,项目名称:z3,代码行数:13,代码来源:api_pb.cpp
示例20: Z3_mk_tactic
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name) {
Z3_TRY;
LOG_Z3_mk_tactic(c, name);
RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == 0) {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
tactic * new_t = t->mk(mk_c(c)->m());
RETURN_TACTIC(new_t);
Z3_CATCH_RETURN(0);
}
开发者ID:EinNarr,项目名称:z3,代码行数:13,代码来源:api_tactic.cpp
注:本文中的RETURN_Z3函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论