mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
Display Fu Malik statistics
This commit is contained in:
Anh-Dung Phan
parent
0acf331ed1
commit
074e851d49
7 changed files with 104 additions and 29 deletions
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
#include "tactic2solver.h"
|
||||
#include "goal.h"
|
||||
#include "probe.h"
|
||||
#include "tactic.h"
|
||||
#include "smt_context.h"
|
||||
|
||||
/**
|
||||
|
|
@ -41,16 +42,16 @@ Notes:
|
|||
namespace opt {
|
||||
|
||||
struct fu_malik::imp {
|
||||
ast_manager& m;
|
||||
ref<solver> m_s;
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_soft;
|
||||
expr_ref_vector m_orig_soft;
|
||||
expr_ref_vector m_aux;
|
||||
expr_ref_vector m_assignment;
|
||||
unsigned m_upper_size;
|
||||
|
||||
ref<solver> m_s;
|
||||
solver & m_original_solver;
|
||||
bool m_use_new_bv_solver;
|
||||
bool m_use_new_bv_solver;
|
||||
|
||||
imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
|
||||
m(m),
|
||||
|
|
@ -82,6 +83,63 @@ namespace opt {
|
|||
* add at-most-one constraint with blocking
|
||||
*/
|
||||
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
||||
void set2vector(expr_set const& set, expr_ref_vector & es) const {
|
||||
es.reset();
|
||||
expr_set::iterator it = set.begin(), end = set.end();
|
||||
for (; it != end; ++it) {
|
||||
es.push_back(*it);
|
||||
}
|
||||
}
|
||||
|
||||
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
|
||||
set.reset();
|
||||
expr_set::iterator it = set1.begin(), end = set1.end();
|
||||
for (; it != end; ++it) {
|
||||
set.insert(*it);
|
||||
}
|
||||
it = set2.begin();
|
||||
end = set2.end();
|
||||
for (; it != end; ++it) {
|
||||
set.insert(*it);
|
||||
}
|
||||
}
|
||||
|
||||
void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) {
|
||||
if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
|
||||
core.reset();
|
||||
return;
|
||||
}
|
||||
|
||||
SASSERT(!literals.empty());
|
||||
if (literals.size() == 1) {
|
||||
core.reset();
|
||||
core.insert(literals[0].get());
|
||||
return;
|
||||
}
|
||||
|
||||
unsigned mid = literals.size()/2;
|
||||
expr_ref_vector ls1(m), ls2(m);
|
||||
ls1.append(mid, literals.c_ptr());
|
||||
ls2.append(literals.size()-mid, literals.c_ptr() + mid);
|
||||
|
||||
expr_ref_vector as1(m);
|
||||
as1.append(assumptions);
|
||||
as1.append(ls1);
|
||||
expr_set core2;
|
||||
quick_explain(as1, ls2, !ls1.empty(), core2);
|
||||
|
||||
expr_ref_vector as2(m), cs2(m);
|
||||
as2.append(assumptions);
|
||||
set2vector(core2, cs2);
|
||||
as2.append(cs2);
|
||||
expr_set core1;
|
||||
quick_explain(as2, ls1, !core2.empty(), core1);
|
||||
|
||||
set_union(core1, core2, core);
|
||||
}
|
||||
|
||||
lbool step() {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
|
||||
expr_ref_vector assumptions(m), block_vars(m);
|
||||
|
|
@ -95,12 +153,14 @@ namespace opt {
|
|||
|
||||
ptr_vector<expr> core;
|
||||
if (m_use_new_bv_solver) {
|
||||
unsigned i = 0;
|
||||
while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
core.push_back(assumptions[i].get());
|
||||
++i;
|
||||
expr_set core_set;
|
||||
expr_ref_vector empty(m);
|
||||
quick_explain(empty, assumptions, true, core_set);
|
||||
expr_set::iterator it = core_set.begin(), end = core_set.end();
|
||||
for (; it != end; ++it) {
|
||||
core.push_back(*it);
|
||||
}
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
|
||||
}
|
||||
else {
|
||||
s().get_unsat_core(core);
|
||||
|
|
@ -164,11 +224,11 @@ namespace opt {
|
|||
probe *p = mk_is_qfbv_probe();
|
||||
bool all_bv = (*p)(g).is_true();
|
||||
if (all_bv) {
|
||||
opt_solver & os = opt_solver::to_opt(m_original_solver);
|
||||
smt::context & ctx = os.get_context();
|
||||
tactic* t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
|
||||
smt::context & ctx = opt_s.get_context();
|
||||
tactic_ref t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
// The new SAT solver hasn't supported unsat core yet
|
||||
m_s = mk_tactic2solver(m, t);
|
||||
m_s = mk_tactic2solver(m, t.get());
|
||||
SASSERT(m_s != &m_original_solver);
|
||||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
m_s->assert_expr(current_solver.get_assertion(i));
|
||||
|
|
@ -211,6 +271,11 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
}
|
||||
statistics st;
|
||||
s().collect_statistics(st);
|
||||
SASSERT(st.size() > 0);
|
||||
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
|
||||
opt_s.set_interim_stats(st);
|
||||
// We are done and soft_constraints has
|
||||
// been updated with the max-sat assignment.
|
||||
return is_sat;
|
||||
|
|
|
|||
|
|
@ -55,7 +55,13 @@ namespace opt {
|
|||
}
|
||||
|
||||
void opt_solver::collect_statistics(statistics & st) const {
|
||||
m_context.collect_statistics(st);
|
||||
// Hack to display fu_malik statistics
|
||||
if (m_stats.size() > 0) {
|
||||
st.copy(m_stats);
|
||||
}
|
||||
else {
|
||||
m_context.collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
void opt_solver::assert_expr(expr * t) {
|
||||
|
|
@ -213,6 +219,10 @@ namespace opt {
|
|||
}
|
||||
return dynamic_cast<opt_solver&>(s);
|
||||
}
|
||||
|
||||
void opt_solver::set_interim_stats(statistics & st) {
|
||||
m_stats.copy(st);
|
||||
}
|
||||
|
||||
void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic,
|
||||
char const * status, char const * attributes) {
|
||||
|
|
|
|||
|
|
@ -46,7 +46,8 @@ namespace opt {
|
|||
bool m_objective_enabled;
|
||||
svector<smt::theory_var> m_objective_vars;
|
||||
vector<inf_eps> m_objective_values;
|
||||
bool m_is_dump;
|
||||
bool m_is_dump;
|
||||
statistics m_stats;
|
||||
public:
|
||||
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
|
||||
virtual ~opt_solver();
|
||||
|
|
@ -77,7 +78,8 @@ namespace opt {
|
|||
expr_ref block_upper_bound(unsigned obj_index, inf_eps const& val);
|
||||
|
||||
static opt_solver& to_opt(solver& s);
|
||||
|
||||
void set_interim_stats(statistics & st);
|
||||
|
||||
class toggle_objective {
|
||||
opt_solver& s;
|
||||
bool m_old_value;
|
||||
|
|
|
|||
|
|
@ -671,6 +671,7 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
lbool solver::check() {
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
|
||||
SASSERT(scope_lvl() == 0);
|
||||
#ifdef CLONE_BEFORE_SOLVING
|
||||
if (m_mc.empty()) {
|
||||
|
|
@ -1970,7 +1971,7 @@ namespace sat {
|
|||
m_cancel = f;
|
||||
}
|
||||
|
||||
void solver::collect_statistics(statistics & st) {
|
||||
void solver::collect_statistics(statistics & st) {
|
||||
m_stats.collect_statistics(st);
|
||||
m_cleaner.collect_statistics(st);
|
||||
m_simplifier.collect_statistics(st);
|
||||
|
|
|
|||
|
|
@ -135,6 +135,7 @@ public:
|
|||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
try {
|
||||
IF_VERBOSE(0, verbose_stream() << "(smt.smt-tactic using the old SAT solver)\n";);
|
||||
SASSERT(in->is_well_sorted());
|
||||
ast_manager & m = in->m();
|
||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
|
|
|
|||
|
|
@ -40,6 +40,7 @@ class tactic2solver : public solver_na2as {
|
|||
bool m_produce_models;
|
||||
bool m_produce_proofs;
|
||||
bool m_produce_unsat_cores;
|
||||
statistics m_stats;
|
||||
public:
|
||||
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
|
||||
virtual ~tactic2solver();
|
||||
|
|
@ -161,6 +162,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
|
|||
m_result->m_unknown = ex.msg();
|
||||
}
|
||||
m_tactic->collect_statistics(m_result->m_stats);
|
||||
m_tactic->collect_statistics(m_stats);
|
||||
m_result->m_model = md;
|
||||
m_result->m_proof = pr;
|
||||
if (m_produce_unsat_cores) {
|
||||
|
|
@ -177,9 +179,9 @@ void tactic2solver::set_cancel(bool f) {
|
|||
m_tactic->set_cancel(f);
|
||||
}
|
||||
|
||||
void tactic2solver::collect_statistics(statistics & st) const {
|
||||
if (m_result.get())
|
||||
m_result->collect_statistics(st);
|
||||
void tactic2solver::collect_statistics(statistics & st) const {
|
||||
st.copy(m_stats);
|
||||
SASSERT(m_stats.size() > 0);
|
||||
}
|
||||
|
||||
void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
|
||||
|
|
|
|||
|
|
@ -31,15 +31,6 @@ Notes:
|
|||
|
||||
#define MEMLIMIT 300
|
||||
|
||||
tactic * mk_new_sat_tactic(ast_manager & m) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;);
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
return new_sat;
|
||||
}
|
||||
|
||||
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
|
|
@ -94,7 +85,10 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * new_sat = and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic());
|
||||
#else
|
||||
tactic * new_sat = mk_new_sat_tactic(m);
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
#endif
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue