mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
6558999cef
commit
21759e5eb2
|
@ -46,20 +46,20 @@ static void show_interpolant_and_maybe_check(cmd_context & ctx,
|
|||
m_params.set_bool("flat", true);
|
||||
th_rewriter s(ctx.m(), m_params);
|
||||
|
||||
expr_ref_vector exprs(ctx.m());
|
||||
sort_ref_vector domain(ctx.m());
|
||||
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
|
||||
exprs.push_back(r);
|
||||
domain.push_back(ctx.m().mk_bool_sort());
|
||||
}
|
||||
func_decl_ref fn(ctx.m());
|
||||
fn = ctx.m().mk_func_decl(symbol("interpolants"), domain.size(), domain.c_ptr(), ctx.m().mk_bool_sort());
|
||||
expr_ref tmp(ctx.m());
|
||||
tmp = ctx.m().mk_app(fn, exprs.size(), exprs.c_ptr());
|
||||
ctx.regular_stream() << tmp << "\n";
|
||||
|
||||
s.cleanup();
|
||||
|
||||
|
|
Loading…
Reference in a new issue