mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

to_mbp_benchmark(): prints an mbp problem in benchmark format

Browse source 
currently unused. See comment in spacer_util.c:qe_project for example
usage
This commit is contained in:
Arie Gurfinkel 2018-05-21 22:01:49 -07:00
parent bf4c35982f
commit 00f870b7ff
2 changed files with 56 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/muz/spacer/spacer_util.cpp
View file

@ -469,6 +469,24 @@ namespace spacer {
sub (fml);
}
void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) {
ast_manager &m = vars.m();
ast_pp_util pp(m);
pp.collect(fml);
pp.display_decls(out);
out << "(define-fun mbp_benchmark_fml () Bool\n ";
out << mk_pp(fml, m) << ")\n\n";
out << "(push)\n"
<< "(assert mbp_benchmark_fml)\n"
<< "(check-sat)\n"
<< "(mbp mbp_benchmark_fml (";
for (auto v : vars) {out << mk_pp(v, m) << " ";}
out << "))\n"
<< "(pop)\n"
<< "(exit)\n";
}
/*
* eliminate simple equalities using qe_lite
* then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays
@ -489,6 +507,10 @@ namespace spacer {
fml = mk_and(flat);
}
// uncomment for benchmarks
//to_mbp_benchmark(verbose_stream(), fml, vars);
app_ref_vector arith_vars (m);
app_ref_vector array_vars (m);
array_util arr_u (m);

3
src/muz/spacer/spacer_util.h
View file

@ -125,6 +125,9 @@ bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
void to_mbp_benchmark(std::ostream &out, const expr* fml,
const app_ref_vector &vars);
/**
* do the following in sequence
* 1. use qe_lite to cheaply eliminate vars