mirror of
https://github.com/Z3Prover/z3
synced 2025-08-21 10:41:35 +00:00
speed-up handling of cnf input to inc_sat_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
9bd4050e0c
commit
b8d18c6c6d
7 changed files with 133 additions and 57 deletions
|
|
@ -78,6 +78,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
void cleaner::cleanup_clauses(clause_vector & cs) {
|
||||
tmp_clause tmp;
|
||||
clause_vector::iterator it = cs.begin();
|
||||
clause_vector::iterator it2 = it;
|
||||
clause_vector::iterator end = cs.end();
|
||||
|
|
@ -88,12 +89,10 @@ namespace sat {
|
|||
CTRACE("sat_cleaner_frozen", c.frozen(), tout << c << "\n";);
|
||||
unsigned sz = c.size();
|
||||
unsigned i = 0, j = 0;
|
||||
bool sat = false;
|
||||
m_cleanup_counter += sz;
|
||||
for (; i < sz; i++) {
|
||||
switch (s.value(c[i])) {
|
||||
case l_true:
|
||||
sat = true;
|
||||
goto end_loop;
|
||||
case l_false:
|
||||
m_elim_literals++;
|
||||
|
|
@ -108,9 +107,9 @@ namespace sat {
|
|||
}
|
||||
end_loop:
|
||||
CTRACE("sat_cleaner_frozen", c.frozen(),
|
||||
tout << "sat: " << sat << ", new_size: " << j << "\n";
|
||||
tout << "sat: " << (i < sz) << ", new_size: " << j << "\n";
|
||||
tout << mk_lits_pp(j, c.begin()) << "\n";);
|
||||
if (sat) {
|
||||
if (i < sz) {
|
||||
m_elim_clauses++;
|
||||
s.del_clause(c);
|
||||
}
|
||||
|
|
@ -119,33 +118,37 @@ namespace sat {
|
|||
CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
|
||||
if (c.size() > 0) tout << "unit: " << c[0] << "\n";
|
||||
s.display_watches(tout););
|
||||
if (new_sz == 0) {
|
||||
switch (new_sz) {
|
||||
case 0:
|
||||
s.set_conflict(justification());
|
||||
s.del_clause(c);
|
||||
}
|
||||
else if (new_sz == 1) {
|
||||
break;
|
||||
case 1:
|
||||
s.assign(c[0], justification());
|
||||
s.del_clause(c);
|
||||
}
|
||||
else {
|
||||
break;
|
||||
case 2:
|
||||
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
if (new_sz == 2) {
|
||||
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
|
||||
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
s.del_clause(c);
|
||||
TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
|
||||
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
s.del_clause(c);
|
||||
break;
|
||||
default:
|
||||
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
if (s.m_config.m_drat && new_sz < i) {
|
||||
tmp.set(c.size(), c.begin(), c.is_learned());
|
||||
}
|
||||
else {
|
||||
c.shrink(new_sz);
|
||||
*it2 = *it;
|
||||
it2++;
|
||||
if (!c.frozen()) {
|
||||
s.attach_clause(c);
|
||||
}
|
||||
if (s.m_config.m_drat) {
|
||||
// for optimization, could also report deletion
|
||||
// of previous version of clause.
|
||||
s.m_drat.add(c, true);
|
||||
}
|
||||
c.shrink(new_sz);
|
||||
*it2 = *it;
|
||||
it2++;
|
||||
if (!c.frozen()) {
|
||||
s.attach_clause(c);
|
||||
}
|
||||
if (s.m_config.m_drat && new_sz < i) {
|
||||
// for optimization, could also report deletion
|
||||
// of previous version of clause.
|
||||
s.m_drat.add(c, true);
|
||||
s.m_drat.del(*tmp.get());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -349,7 +349,7 @@ namespace sat {
|
|||
}
|
||||
if (sz == 2) {
|
||||
s.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
s.del_clause(c);
|
||||
s.del_clause(c, false);
|
||||
continue;
|
||||
}
|
||||
*it2 = *it;
|
||||
|
|
@ -611,10 +611,15 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (j < sz) {
|
||||
if (s.m_config.m_drat) s.m_drat.del(c);
|
||||
if (j < sz && !r) {
|
||||
if (s.m_config.m_drat) {
|
||||
m_dummy.set(c.size(), c.begin(), c.is_learned());
|
||||
}
|
||||
c.shrink(j);
|
||||
if (s.m_config.m_drat) s.m_drat.add(c, true);
|
||||
if (s.m_config.m_drat) {
|
||||
s.m_drat.add(c, true);
|
||||
s.m_drat.del(*m_dummy.get());
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
|
@ -2020,8 +2025,7 @@ namespace sat {
|
|||
for (auto & c2 : m_neg_cls) {
|
||||
m_new_cls.reset();
|
||||
if (!resolve(c1, c2, pos_l, m_new_cls))
|
||||
continue;
|
||||
if (false && v == 767) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " + " << c2 << " -> " << m_new_cls << "\n");
|
||||
continue;
|
||||
TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
|
||||
if (cleanup_clause(m_new_cls))
|
||||
continue; // clause is already satisfied.
|
||||
|
|
|
|||
|
|
@ -60,6 +60,7 @@ class inc_sat_solver : public solver {
|
|||
atom2bool_var m_map;
|
||||
scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
|
||||
tactic_ref m_preprocess;
|
||||
bool m_is_cnf;
|
||||
unsigned m_num_scopes;
|
||||
sat::literal_vector m_asms;
|
||||
goal_ref_buffer m_subgoals;
|
||||
|
|
@ -88,6 +89,7 @@ public:
|
|||
m_fmls_head(0),
|
||||
m_core(m),
|
||||
m_map(m),
|
||||
m_is_cnf(true),
|
||||
m_num_scopes(0),
|
||||
m_unknown("no reason given"),
|
||||
m_internalized_converted(false),
|
||||
|
|
@ -262,9 +264,22 @@ public:
|
|||
void assert_expr_core2(expr * t, expr * a) override {
|
||||
if (a) {
|
||||
m_asmsf.push_back(a);
|
||||
assert_expr_core(m.mk_implies(a, t));
|
||||
if (m_is_cnf && is_literal(t) && is_literal(a)) {
|
||||
assert_expr_core(m.mk_or(::mk_not(m, a), t));
|
||||
}
|
||||
else if (m_is_cnf && m.is_or(t) && is_clause(t) && is_literal(a)) {
|
||||
expr_ref_vector args(m);
|
||||
args.push_back(::mk_not(m, a));
|
||||
args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
|
||||
assert_expr_core(m.mk_or(args.size(), args.c_ptr()));
|
||||
}
|
||||
else {
|
||||
m_is_cnf = false;
|
||||
assert_expr_core(m.mk_implies(a, t));
|
||||
}
|
||||
}
|
||||
else {
|
||||
m_is_cnf &= is_clause(t);
|
||||
assert_expr_core(t);
|
||||
}
|
||||
}
|
||||
|
|
@ -545,7 +560,12 @@ private:
|
|||
SASSERT(!g->proofs_enabled());
|
||||
TRACE("sat", m_solver.display(tout); g->display(tout););
|
||||
try {
|
||||
(*m_preprocess)(g, m_subgoals);
|
||||
if (m_is_cnf) {
|
||||
m_subgoals.push_back(g.get());
|
||||
}
|
||||
else {
|
||||
(*m_preprocess)(g, m_subgoals);
|
||||
}
|
||||
}
|
||||
catch (tactic_exception & ex) {
|
||||
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
|
||||
|
|
@ -705,6 +725,25 @@ private:
|
|||
}
|
||||
}
|
||||
|
||||
bool is_literal(expr* n) {
|
||||
return is_uninterp_const(n) || (m.is_not(n, n) && is_uninterp_const(n));
|
||||
}
|
||||
|
||||
bool is_clause(expr* fml) {
|
||||
if (is_literal(fml)) {
|
||||
return true;
|
||||
}
|
||||
if (!m.is_or(fml)) {
|
||||
return false;
|
||||
}
|
||||
for (expr* n : *to_app(fml)) {
|
||||
if (!is_literal(n)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
lbool internalize_formulas() {
|
||||
if (m_fmls_head == m_fmls.size()) {
|
||||
return l_true;
|
||||
|
|
@ -712,7 +751,8 @@ private:
|
|||
dep2asm_t dep2asm;
|
||||
goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
|
||||
for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
|
||||
g->assert_expr(m_fmls[i].get());
|
||||
expr* fml = m_fmls.get(i);
|
||||
g->assert_expr(fml);
|
||||
}
|
||||
lbool res = internalize_goal(g, dep2asm, false);
|
||||
if (res != l_undef) {
|
||||
|
|
|
|||
|
|
@ -38,9 +38,13 @@ void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const {
|
|||
}
|
||||
|
||||
sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
|
||||
sat::bool_var v = sat::null_bool_var;
|
||||
m_mapping.find(n, v);
|
||||
return v;
|
||||
unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
|
||||
if (idx == UINT_MAX) {
|
||||
return sat::null_bool_var;
|
||||
}
|
||||
else {
|
||||
return m_mapping[idx].m_value;
|
||||
}
|
||||
}
|
||||
|
||||
struct collect_boolean_interface_proc {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue