mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
improving drat output perf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1e90be62bc
commit
7fa9768c36
|
@ -48,6 +48,7 @@ Notes:
|
|||
namespace opt {
|
||||
|
||||
void context::scoped_state::push() {
|
||||
m_asms_lim.push_back(m_asms.size());
|
||||
m_hard_lim.push_back(m_hard.size());
|
||||
m_objectives_lim.push_back(m_objectives.size());
|
||||
m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size());
|
||||
|
@ -55,6 +56,7 @@ namespace opt {
|
|||
|
||||
void context::scoped_state::pop() {
|
||||
m_hard.resize(m_hard_lim.back());
|
||||
m_asms.resize(m_asms_lim.back());
|
||||
unsigned k = m_objectives_term_trail_lim.back();
|
||||
while (m_objectives_term_trail.size() > k) {
|
||||
unsigned idx = m_objectives_term_trail.back();
|
||||
|
@ -73,6 +75,7 @@ namespace opt {
|
|||
}
|
||||
m_objectives_lim.pop_back();
|
||||
m_hard_lim.pop_back();
|
||||
m_asms_lim.pop_back();
|
||||
}
|
||||
|
||||
void context::scoped_state::add(expr* hard) {
|
||||
|
@ -188,6 +191,12 @@ namespace opt {
|
|||
clear_state();
|
||||
}
|
||||
|
||||
void context::add_hard_constraint(expr* f, expr* t) {
|
||||
m_scoped_state.m_asms.push_back(t);
|
||||
m_scoped_state.add(m.mk_implies(t, f));
|
||||
clear_state();
|
||||
}
|
||||
|
||||
void context::get_hard_constraints(expr_ref_vector& hard) {
|
||||
hard.append(m_scoped_state.m_hard);
|
||||
}
|
||||
|
@ -253,7 +262,7 @@ namespace opt {
|
|||
m_hard_constraints.append(s.m_hard);
|
||||
}
|
||||
|
||||
lbool context::optimize(expr_ref_vector const& asms) {
|
||||
lbool context::optimize(expr_ref_vector const& _asms) {
|
||||
if (m_pareto) {
|
||||
return execute_pareto();
|
||||
}
|
||||
|
@ -263,6 +272,8 @@ namespace opt {
|
|||
clear_state();
|
||||
init_solver();
|
||||
import_scoped_state();
|
||||
expr_ref_vector asms(_asms);
|
||||
asms.append(m_scoped_state.m_asms);
|
||||
normalize(asms);
|
||||
if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) {
|
||||
return l_false;
|
||||
|
|
|
@ -115,20 +115,23 @@ namespace opt {
|
|||
arith_util m_arith;
|
||||
bv_util m_bv;
|
||||
unsigned_vector m_hard_lim;
|
||||
unsigned_vector m_asms_lim;
|
||||
unsigned_vector m_objectives_lim;
|
||||
unsigned_vector m_objectives_term_trail;
|
||||
unsigned_vector m_objectives_term_trail_lim;
|
||||
map_id m_indices;
|
||||
|
||||
public:
|
||||
expr_ref_vector m_hard;
|
||||
expr_ref_vector m_hard;
|
||||
expr_ref_vector m_asms;
|
||||
vector<objective> m_objectives;
|
||||
|
||||
scoped_state(ast_manager& m):
|
||||
m(m),
|
||||
m_arith(m),
|
||||
m_bv(m),
|
||||
m_hard(m)
|
||||
m_hard(m),
|
||||
m_asms(m)
|
||||
{}
|
||||
void push();
|
||||
void pop();
|
||||
|
@ -180,6 +183,7 @@ namespace opt {
|
|||
unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
|
||||
unsigned add_objective(app* t, bool is_max);
|
||||
void add_hard_constraint(expr* f);
|
||||
void add_hard_constraint(expr* f, expr* t);
|
||||
|
||||
void get_hard_constraints(expr_ref_vector& hard);
|
||||
expr_ref get_objective(unsigned i);
|
||||
|
|
|
@ -72,14 +72,36 @@ namespace sat {
|
|||
}
|
||||
|
||||
void drat::dump(unsigned n, literal const* c, status st) {
|
||||
switch (st) {
|
||||
case status::asserted: return;
|
||||
case status::external: return; // requires extension to drat format.
|
||||
case status::learned: break;
|
||||
case status::deleted: (*m_out) << "d "; break;
|
||||
if (st == status::asserted || st == status::external) {
|
||||
return;
|
||||
}
|
||||
for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
|
||||
(*m_out) << "0\n";
|
||||
|
||||
char buffer[10000];
|
||||
int len = 0;
|
||||
if (st == status::deleted) {
|
||||
buffer[0] = 'd';
|
||||
buffer[1] = ' ';
|
||||
len = 2;
|
||||
}
|
||||
for (unsigned i = 0; i < n && len >= 0; ++i) {
|
||||
literal lit = c[i];
|
||||
int _lit = lit.var();
|
||||
if (lit.sign()) _lit = -_lit;
|
||||
len += snprintf(buffer + len, sizeof(buffer) - len, "%d ", _lit);
|
||||
}
|
||||
|
||||
if (len >= 0) {
|
||||
len += snprintf(buffer + len, sizeof(buffer) - len, "0\n");
|
||||
}
|
||||
if (len >= 0) {
|
||||
m_out->write(buffer, len);
|
||||
}
|
||||
else {
|
||||
if (st == status::deleted) (*m_out) << "d ";
|
||||
for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
|
||||
(*m_out) << "0\n";
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
void drat::bdump(unsigned n, literal const* c, status st) {
|
||||
|
|
|
@ -1701,6 +1701,7 @@ namespace sat {
|
|||
if (is_fixed_at(lit, c_fixed_truth) || is_true_at(lit, level)) continue;
|
||||
bool unsat = false;
|
||||
if (is_false_at(lit, level)) {
|
||||
if (lit.sign() && lit.var() == 34523) std::cout << "false at " << lit << "\n";
|
||||
unsat = true;
|
||||
}
|
||||
else {
|
||||
|
@ -1708,7 +1709,9 @@ namespace sat {
|
|||
reset_lookahead_reward(lit);
|
||||
unsigned num_units = push_lookahead1(lit, level);
|
||||
update_lookahead_reward(lit, level);
|
||||
if (lit.sign() && lit.var() == 34523) std::cout << "num units.1 " << num_units << " " << inconsistent() << "\n";
|
||||
num_units += do_double(lit, dl_lvl);
|
||||
if (lit.sign() && lit.var() == 34523) std::cout << "num units.2 " << num_units << "\n";
|
||||
if (dl_lvl > level) {
|
||||
base = dl_lvl;
|
||||
//SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
|
||||
|
|
Loading…
Reference in a new issue