mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

adding drat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-02-03 15:41:08 -08:00
parent 505133a4b3
commit 0b711c5ef8
14 changed files with 255 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/src/sat/CMakeLists.txt
View file

@ -8,6 +8,7 @@ z3_add_component(sat
sat_clause_use_list.cpp
sat_cleaner.cpp
sat_config.cpp
sat_drat.cpp
sat_elim_eqs.cpp
sat_iff3_finder.cpp
sat_integrity_checker.cpp

6
src/opt/maxres.cpp
View file

@ -352,9 +352,9 @@ public:
while (is_sat == l_false) {
core.reset();
s().get_unsat_core(core);
//expr_ref_vector core1(m);
//core1.append(core.size(), core.c_ptr());
//std::cout << core1 << "\n";
expr_ref_vector core1(m);
core1.append(core.size(), core.c_ptr());
std::cout << core1 << "\n";
// verify_core(core);
model_ref mdl;
get_mus_model(mdl);

126
src/sat/card_extension.cpp
View file

@ -94,7 +94,7 @@ namespace sat {
alit = c[j];
}
}
set_conflict(c, alit);
set_conflict(c);
}
else if (j == bound) {
for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
@ -136,32 +136,40 @@ namespace sat {
}
void card_extension::assign(card& c, literal lit) {
if (value(lit) == l_true) {
return;
switch (value(lit)) {
case l_true:
break;
case l_false:
set_conflict(c);
break;
default:
m_stats.m_num_propagations++;
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c));
s().assign(lit, justification::mk_ext_justification(c.index()));
break;
}
m_stats.m_num_propagations++;
//TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
SASSERT(validate_unit_propagation(c));
s().assign(lit, justification::mk_ext_justification(c.index()));
}
void card_extension::watch_literal(card& c, literal lit) {
TRACE("sat", tout << "watch: " << lit << "\n";);
TRACE("sat_verbose", tout << "watch: " << lit << "\n";);
init_watch(lit.var());
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
if (cards == 0) {
cards = alloc(ptr_vector<card>);
m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
}
TRACE("sat", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
cards->push_back(&c);
}
void card_extension::set_conflict(card& c, literal lit) {
void card_extension::set_conflict(card& c) {
TRACE("sat", display(tout, c, true); );
SASSERT(validate_conflict(c));
m_stats.m_num_conflicts++;
if (!resolve_conflict(c, lit)) {
literal lit = last_false_literal(c);
if (!resolve_conflict(c, lit)) {
TRACE("sat", tout << "bail out conflict resolution\n";);
m_conflict.reset();
m_conflict.push_back(~c.lit());
unsigned sz = c.size();
@ -169,11 +177,40 @@ namespace sat {
m_conflict.push_back(c[i]);
}
m_conflict.push_back(lit);
SASSERT(validate_conflict(m_conflict));
// SASSERT(validate_conflict(m_conflict));
s().assign(lit, justification::mk_ext_justification(0));
}
SASSERT(s().inconsistent());
}
literal card_extension::last_false_literal(card& c) {
while (!m_active_var_set.empty()) m_active_var_set.erase();
reset_coeffs();
for (unsigned i = 0; i < c.size(); ++i) {
bool_var v = c[i].var();
m_active_var_set.insert(v);
m_active_vars.push_back(v);
m_coeffs.setx(v, c[i].sign() ? -1 : 1, 0);
}
literal_vector const& lits = s().m_trail;
for (unsigned i = lits.size(); i > 0; ) {
--i;
literal lit = lits[i];
bool_var v = lit.var();
if (m_active_var_set.contains(v) &&
(m_coeffs[v] > 0 == lits[i].sign())) {
//std::cout << "last literal: " << lit << "\n";
for (unsigned j = 0; j < c.size(); ++j) {
if (~lit == c[j] && j != c.k()-1) {
// std::cout << "POSITION " << j << " bound " << c.k() << "\n";
}
}
return ~lit;
}
}
UNREACHABLE();
return null_literal;
}
void card_extension::normalize_active_coeffs() {
while (!m_active_var_set.empty()) m_active_var_set.erase();
@ -244,7 +281,7 @@ namespace sat {
if (m_conflict_lvl < lvl(c.lit()) || m_conflict_lvl == 0) {
return false;
}
std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n";
// std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n";
reset_coeffs();
m_num_marks = 0;
@ -263,6 +300,8 @@ namespace sat {
v = consequent.var();
int offset = get_abs_coeff(v);
// TRACE("sat", display(tout, m_A););
if (offset == 0) {
goto process_next_resolvent;
}
@ -365,12 +404,14 @@ namespace sat {
bool_var v = m_active_vars[i];
slack += get_abs_coeff(v);
}
TRACE("sat", display(tout, m_A););
++idx;
alit = null_literal;
#if 1
std::cout << c.size() << " >= " << c.k() << "\n";
std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n";
// std::cout << c.size() << " >= " << c.k() << "\n";
// std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n";
while (0 <= slack) {
literal lit = lits[idx];
bool_var v = lit.var();
@ -432,7 +473,9 @@ namespace sat {
return false;
}
SASSERT(slack < 0);
SASSERT(validate_conflict(m_conflict));
SASSERT(validate_conflict(m_conflict, m_A));
TRACE("sat", tout << m_conflict << "\n";);
s().assign(alit, justification::mk_ext_justification(0));
return true;
@ -520,7 +563,7 @@ namespace sat {
void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
if (idx == 0) {
std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n";
// std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n";
SASSERT(m_conflict.back() == l);
for (unsigned i = 0; i + 1 < m_conflict.size(); ++i) {
SASSERT(value(m_conflict[i]) == l_false);
@ -537,7 +580,7 @@ namespace sat {
}
SASSERT(found););
std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n";
// std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n";
r.push_back(c.lit());
SASSERT(value(c.lit()) == l_true);
for (unsigned i = c.k(); i < c.size(); ++i) {
@ -552,7 +595,7 @@ namespace sat {
// literal is assigned to false.
unsigned sz = c.size();
unsigned bound = c.k();
TRACE("sat", tout << "assign: " << c.lit() << " " << ~alit << " " << bound << "\n";);
TRACE("sat", tout << "assign: " << c.lit() << ": " << ~alit << "@" << lvl(~alit) << "\n";);
SASSERT(0 < bound && bound < sz);
SASSERT(value(alit) == l_false);
@ -583,11 +626,11 @@ namespace sat {
// conflict
if (bound != index && value(c[bound]) == l_false) {
TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
set_conflict(c, alit);
set_conflict(c);
return l_false;
}
TRACE("sat", tout << "no swap " << index << " " << alit << "\n";);
// TRACE("sat", tout << "no swap " << index << " " << alit << "\n";);
// there are no literals to swap with,
// prepare for unit propagation by swapping the false literal into
// position bound. Then literals in positions 0..bound-1 have to be
@ -609,8 +652,8 @@ namespace sat {
if (v >= m_var_infos.size()) return;
var_info& vinfo = m_var_infos[v];
ptr_vector<card>* cards = vinfo.m_lit_watch[!l.sign()];
TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";);
TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";);
//TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";);
//TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";);
if (cards != 0 && !cards->empty() && !s().inconsistent()) {
ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
for (; it != end; ++it) {
@ -652,7 +695,7 @@ namespace sat {
}
void card_extension::pop(unsigned n) {
TRACE("sat", tout << "pop:" << n << "\n";);
TRACE("sat_verbose", tout << "pop:" << n << "\n";);
unsigned new_lim = m_var_lim.size() - n;
unsigned sz = m_var_lim[new_lim];
while (m_var_trail.size() > sz) {
@ -690,9 +733,9 @@ namespace sat {
void card_extension::display_watch(std::ostream& out, bool_var v, bool sign) const {
watch const* w = m_var_infos[v].m_lit_watch[sign];
if (w) {
if (w && !w->empty()) {
watch const& wl = *w;
out << "watch: " << literal(v, sign) << " |-> ";
out << literal(v, sign) << " |-> ";
for (unsigned i = 0; i < wl.size(); ++i) {
out << wl[i]->lit() << " ";
}
@ -708,7 +751,7 @@ namespace sat {
}
void card_extension::display(std::ostream& out, card& c, bool values) const {
out << c.lit();
out << c.lit() << "[" << c.size() << "]";
if (c.lit() != null_literal && values) {
out << "@(" << value(c.lit());
if (value(c.lit()) != l_undef) {
@ -750,6 +793,21 @@ namespace sat {
return out;
}
std::ostream& card_extension::display_justification(std::ostream& out, ext_justification_idx idx) const {
if (idx == 0) {
out << "conflict: " << m_conflict;
}
else {
card& c = *m_constraints[idx];
out << "bound " << c.lit() << ": ";
for (unsigned i = c.k(); i < c.size(); ++i) {
out << c[i] << " ";
}
out << ">= " << c.k();
}
return out;
}
void card_extension::collect_statistics(statistics& st) const {
st.update("cardinality propagations", m_stats.m_num_propagations);
st.update("cardinality conflicts", m_stats.m_num_conflicts);
@ -842,7 +900,6 @@ namespace sat {
// validate that m_A & m_B implies m_C
bool card_extension::validate_resolvent() {
std::cout << "validate resolvent\n";
u_map<unsigned> coeffs;
unsigned k = m_A.m_k + m_B.m_k;
for (unsigned i = 0; i < m_A.m_lits.size(); ++i) {
@ -899,11 +956,18 @@ namespace sat {
return true;
}
bool card_extension::validate_conflict(literal_vector const& lits) {
bool card_extension::validate_conflict(literal_vector const& lits, ineq& p) {
for (unsigned i = 0; i < lits.size(); ++i) {
if (value(lits[i]) != l_false) return false;
}
return true;
unsigned value = 0;
for (unsigned i = 0; i < p.m_lits.size(); ++i) {
unsigned coeff = p.m_coeffs[i];
if (!lits.contains(p.m_lits[i])) {
value += coeff;
}
}
return value < p.m_k;
}

6
src/sat/card_extension.h
View file

@ -103,7 +103,8 @@ namespace sat {
void assign(card& c, literal lit);
lbool add_assign(card& c, literal lit);
void watch_literal(card& c, literal lit);
void set_conflict(card& c, literal lit);
void set_conflict(card& c);
literal last_false_literal(card& c);
void clear_watch(card& c);
void reset_coeffs();
@ -131,7 +132,7 @@ namespace sat {
bool validate_assign(literal_vector const& lits, literal lit);
bool validate_lemma();
bool validate_unit_propagation(card const& c);
bool validate_conflict(literal_vector const& lits);
bool validate_conflict(literal_vector const& lits, ineq& p);
ineq m_A, m_B, m_C;
void active2pb(ineq& p);
@ -156,6 +157,7 @@ namespace sat {
virtual void clauses_modifed();
virtual lbool get_phase(bool_var v);
virtual std::ostream& display(std::ostream& out) const;
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const;
virtual void collect_statistics(statistics& st) const;
virtual extension* copy(solver* s);
};

1
src/sat/sat_config.cpp
View file

@ -113,6 +113,7 @@ namespace sat {
m_minimize_lemmas = p.minimize_lemmas();
m_core_minimize = p.core_minimize();
m_core_minimize_partial = p.core_minimize_partial();
m_drat = p.drat();
m_dyn_sub_res = p.dyn_sub_res();
}

2
src/sat/sat_config.h
View file

@ -73,7 +73,7 @@ namespace sat {
bool m_dyn_sub_res;
bool m_core_minimize;
bool m_core_minimize_partial;
bool m_drat;
symbol m_always_true;
symbol m_always_false;

67
src/sat/sat_drat.cpp Normal file
View file

@ -0,0 +1,67 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_drat.cpp
Abstract:
Produce DRAT proofs.
Author:
Nikolaj Bjorner (nbjorner) 2017-2-3
Notes:
--*/
#include "sat_solver.h"
#include "sat_drat.h"
namespace sat {
drat::drat(solver& s):
s(s),
m_out(0)
{
if (s.m_config.m_drat) {
m_out = alloc(std::ofstream, "proof.drat");
}
}
drat::~drat() {
dealloc(m_out);
}
void drat::add_empty() {
(*m_out) << "0\n";
}
void drat::add_literal(literal l) {
(*m_out) << l << " 0\n";
}
void drat::add_binary(literal l1, literal l2) {
(*m_out) << l1 << " " << l2 << " 0\n";
}
void drat::add_ternary(literal l1, literal l2, literal l3) {
(*m_out) << l1 << " " << l2 << " " << l3 << " 0\n";
}
void drat::add_clause(clause& c) {
unsigned sz = c.size();
for (unsigned i = 0; i < sz; ++i) {
(*m_out) << c[i] << " ";
}
(*m_out) << "0\n";
}
void drat::del_literal(literal l) {
(*m_out) << "d ";
add_literal(l);
}
void drat::del_binary(literal l1, literal l2) {
(*m_out) << "d ";
add_binary(l1, l2);
}
void drat::del_clause(clause& c) {
(*m_out) << "d ";
add_clause(c);
}
}

41
src/sat/sat_drat.h Normal file
View file

@ -0,0 +1,41 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
sat_drat.h
Abstract:
Produce DRAT proofs.
Author:
Nikolaj Bjorner (nbjorner) 2017-2-3
Notes:
--*/
#ifndef SAT_DRAT_H_
#define SAT_DRAT_H_
namespace sat {
class drat {
solver& s;
std::ostream* m_out;
public:
drat(solver& s);
~drat();
void add_empty();
void add_literal(literal l);
void add_binary(literal l1, literal l2);
void add_ternary(literal l1, literal l2, literal l3);
void add_clause(clause& c);
void del_literal(literal l);
void del_binary(literal l1, literal l2);
void del_clause(clause& c);
};
};
#endif

1
src/sat/sat_extension.h
View file

@ -43,6 +43,7 @@ namespace sat {
virtual void clauses_modifed() = 0;
virtual lbool get_phase(bool_var v) = 0;
virtual std::ostream& display(std::ostream& out) const = 0;
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual extension* copy(solver* s) = 0;
};

3
src/sat/sat_params.pyg
View file

@ -24,4 +24,5 @@ def_module_params('sat',
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('parallel_threads', UINT, 1, 'number of parallel threads to use'),
('cardinality_solver', BOOL, False, 'enable cardinality based solver'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat', BOOL, False, 'produce DRAT proofs'),))

41
src/sat/sat_solver.cpp
View file

@ -42,6 +42,7 @@ namespace sat {
m_asymm_branch(*this, p),
m_probing(*this, p),
m_mus(*this),
m_drat(*this),
m_inconsistent(false),
m_num_frozen(0),
m_activity_inc(128),
@ -199,7 +200,11 @@ namespace sat {
}
void solver::del_clause(clause& c) {
if (!c.is_learned()) m_stats.m_non_learned_generation++;
if (!c.is_learned()) {
m_stats.m_non_learned_generation++;
} else if (m_config.m_drat) {
m_drat.del_clause(c);
}
m_cls_allocator.del_clause(&c);
m_stats.m_del_clause++;
}
@ -214,9 +219,10 @@ namespace sat {
}
++m_stats.m_non_learned_generation;
}
switch (num_lits) {
case 0:
if (m_config.m_drat) m_drat.add_empty();
set_conflict(justification());
return 0;
case 1:
@ -233,6 +239,8 @@ namespace sat {
}
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
if (learned && m_config.m_drat)
m_drat.add_binary(l1, l2);
if (propagate_bin_clause(l1, l2)) {
if (at_base_lvl())
return;
@ -266,6 +274,8 @@ namespace sat {
clause * solver::mk_ter_clause(literal * lits, bool learned) {
if (learned && m_config.m_drat)
m_drat.add_ternary(lits[0], lits[1], lits[2]);
m_stats.m_mk_ter_clause++;
clause * r = m_cls_allocator.mk_clause(3, lits, learned);
bool reinit = attach_ter_clause(*r);
@ -309,8 +319,10 @@ namespace sat {
SASSERT(!learned || r->is_learned());
bool reinit = attach_nary_clause(*r);
if (reinit && !learned) push_reinit_stack(*r);
if (learned)
if (learned) {
m_learned.push_back(r);
if (m_config.m_drat) m_drat.add_clause(*r);
}
else
m_clauses.push_back(r);
return r;
@ -516,8 +528,10 @@ namespace sat {
void solver::assign_core(literal l, justification j) {
SASSERT(value(l) == l_undef);
TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
if (at_base_lvl())
if (at_base_lvl()) {
j = justification(); // erase justification for level 0
if (m_config.m_drat) m_drat.add_literal(l);
}
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
bool_var v = l.var();
@ -2058,6 +2072,10 @@ namespace sat {
}
consequent = ~m_not_l;
}
std::cout << "CONFLICT: " << m_core << "\n";
display_status(std::cout);
++count;
exit(0);
justification js = m_conflict;
@ -2098,8 +2116,6 @@ namespace sat {
IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
}
++count;
SASSERT(count == 1);
}
@ -2124,7 +2140,7 @@ namespace sat {
for (; it != end; ++it)
r = std::max(r, lvl(*it));
if (true || r != scope_lvl() || r != lvl(not_l)) {
std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n";
// std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n";
}
return r;
}
@ -2862,12 +2878,14 @@ namespace sat {
}
void solver::display_units(std::ostream & out) const {
unsigned end = init_trail_size();
unsigned end = m_trail.size(); // init_trail_size();
for (unsigned i = 0; i < end; i++) {
out << m_trail[i] << " ";
}
if (end != 0)
display_justification(out, m_justification[m_trail[i].var()]);
out << "\n";
}
//if (end != 0)
// out << "\n";
}
void solver::display(std::ostream & out) const {
@ -2886,6 +2904,9 @@ namespace sat {
if (js.is_clause()) {
out << *(m_cls_allocator.get_clause(js.get_clause_offset()));
}
else if (js.is_ext_justification() && m_ext) {
m_ext->display_justification(out << " ", js.get_ext_justification_idx());
}
}
unsigned solver::num_clauses() const {

3
src/sat/sat_solver.h
View file

@ -33,6 +33,7 @@ Revision History:
#include"sat_iff3_finder.h"
#include"sat_probing.h"
#include"sat_mus.h"
#include"sat_drat.h"
#include"sat_par.h"
#include"params.h"
#include"statistics.h"
@ -87,6 +88,7 @@ namespace sat {
asymm_branch m_asymm_branch;
probing m_probing;
mus m_mus; // MUS for minimal core extraction
drat m_drat; // DRAT for generating proofs
bool m_inconsistent;
// A conflict is usually a single justification. That is, a justification
// for false. If m_not_l is not null_literal, then m_conflict is a
@ -146,6 +148,7 @@ namespace sat {
friend class probing;
friend class iff3_finder;
friend class mus;
friend class drat;
friend class card_extension;
friend struct mk_stat;
public:

6
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -208,7 +208,7 @@ public:
}
virtual ast_manager& get_manager() const { return m; }
virtual void assert_expr(expr * t) {
TRACE("sat", tout << mk_pp(t, m) << "\n";);
TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
m_fmls.push_back(t);
}
virtual void set_produce_models(bool f) {}
@ -376,7 +376,7 @@ private:
init_preprocess();
SASSERT(g->models_enabled());
SASSERT(!g->proofs_enabled());
TRACE("sat", g->display(tout););
TRACE("goal2sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
}
@ -393,7 +393,7 @@ private:
}
g = m_subgoals[0];
expr_ref_vector atoms(m);
TRACE("sat", g->display_with_dependencies(tout););
TRACE("goal2sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
m_goal2sat.get_interpreted_atoms(atoms);
if (!atoms.empty()) {

4
src/sat/tactic/goal2sat.cpp
View file

@ -400,7 +400,7 @@ struct goal2sat::imp {
sat::bool_var v = m_solver.mk_var(true);
sat::literal lit(v, sign);
m_ext->add_at_least(v, lits, k.get_unsigned());
TRACE("sat", tout << "root: " << root << " lit: " << lit << "\n";);
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
if (root) {
m_result_stack.reset();
mk_clause(lit);
@ -616,7 +616,7 @@ struct goal2sat::imp {
}
f = m.mk_or(fmls.size(), fmls.c_ptr());
}
TRACE("sat", tout << mk_pp(f, m) << "\n";);
TRACE("goal2sat", tout << mk_pp(f, m) << "\n";);
process(f);
skip_dep:
;