mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
adjust benchmark generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6aa0086969
commit
670f56e5e4
|
@ -38,12 +38,13 @@ namespace opt {
|
|||
m_context(mgr, m_params),
|
||||
m(mgr),
|
||||
m_dump_benchmarks(false),
|
||||
m_dump_count(0),
|
||||
m_fm(m) {
|
||||
m_logic = l;
|
||||
if (m_logic != symbol::null)
|
||||
m_context.set_logic(m_logic);
|
||||
}
|
||||
|
||||
unsigned opt_solver::m_dump_count = 0;
|
||||
|
||||
opt_solver::~opt_solver() {
|
||||
}
|
||||
|
@ -119,15 +120,14 @@ namespace opt {
|
|||
tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
|
||||
}
|
||||
});
|
||||
|
||||
lbool r = m_context.check(num_assumptions, assumptions);
|
||||
if (dump_benchmarks()) {
|
||||
std::stringstream file_name;
|
||||
file_name << "opt_solver" << ++m_dump_count << ".smt2";
|
||||
std::ofstream buffer(file_name.str().c_str());
|
||||
to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
|
||||
to_smt2_benchmark(buffer, "opt_solver", "");
|
||||
buffer.close();
|
||||
}
|
||||
lbool r = m_context.check(num_assumptions, assumptions);
|
||||
return r;
|
||||
}
|
||||
|
||||
|
|
|
@ -48,7 +48,7 @@ namespace opt {
|
|||
svector<smt::theory_var> m_objective_vars;
|
||||
vector<inf_eps> m_objective_values;
|
||||
bool m_dump_benchmarks;
|
||||
unsigned m_dump_count;
|
||||
static unsigned m_dump_count;
|
||||
statistics m_stats;
|
||||
filter_model_converter m_fm;
|
||||
public:
|
||||
|
|
|
@ -246,9 +246,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
m_propagate = false;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
bool is_optimal() const {
|
||||
return m_cost < m_min_cost;
|
||||
|
@ -755,7 +753,7 @@ namespace opt {
|
|||
pb_util u(m);
|
||||
lbool is_sat = bound(al, ws, bs, k);
|
||||
if (is_sat != l_true) return is_sat;
|
||||
#if 1
|
||||
#if 0
|
||||
rational mininc(0);
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
if (mininc.is_zero() || mininc > ws[i]) {
|
||||
|
@ -795,6 +793,7 @@ namespace opt {
|
|||
nbs.push_back(m.mk_not(bs[i]));
|
||||
}
|
||||
m_imp = alloc(imp, m, m_solver, nbs, ws); // race condition.
|
||||
m_imp->updt_params(m_params);
|
||||
lbool is_sat = m_imp->pb_solve();
|
||||
k = m_imp->m_lower;
|
||||
m_solver.pop_core(1);
|
||||
|
@ -804,6 +803,10 @@ namespace opt {
|
|||
void updt_params(params_ref& p) {
|
||||
opt_params _p(p);
|
||||
m_engine = _p.wmaxsat_engine();
|
||||
m_solver.updt_params(p);
|
||||
if (m_imp) {
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -388,8 +388,8 @@ namespace smt {
|
|||
c->prune();
|
||||
TRACE("pb", display(tout, *c););
|
||||
|
||||
|
||||
literal lit(abv);
|
||||
|
||||
switch(is_true) {
|
||||
case l_false:
|
||||
lit = ~lit;
|
||||
|
@ -405,6 +405,17 @@ namespace smt {
|
|||
|
||||
// TBD: special cases: k == 1, or args.size() == 1
|
||||
|
||||
if (c->k().is_one()) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~lit);
|
||||
for (unsigned i = 0; i < c->size(); ++i) {
|
||||
lits.push_back(c->lit(i));
|
||||
SASSERT(c->coeff(i).is_one());
|
||||
ctx.mk_th_axiom(get_id(), lit, ~c->lit(i));
|
||||
}
|
||||
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
// maximal coefficient:
|
||||
|
|
Loading…
Reference in a new issue