mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +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 17:56:22 -08:00
parent 0b711c5ef8
commit 61341b8879
7 changed files with 144 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_config.cpp
View file

@ -114,6 +114,8 @@ namespace sat {
m_core_minimize = p.core_minimize();
m_core_minimize_partial = p.core_minimize_partial();
m_drat = p.drat();
m_drat_check = p.drat_check();
m_drat_file = p.drat_file();
m_dyn_sub_res = p.dyn_sub_res();
}

2
src/sat/sat_config.h
View file

@ -74,6 +74,8 @@ namespace sat {
bool m_core_minimize;
bool m_core_minimize_partial;
bool m_drat;
symbol m_drat_file;
bool m_drat_check;
symbol m_always_true;
symbol m_always_false;

121
src/sat/sat_drat.cpp
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -9,6 +9,9 @@ Abstract:
Produce DRAT proofs.
Check them using a very simple forward checker
that interacts with external plugins.
Author:
Nikolaj Bjorner (nbjorner) 2017-2-3
@ -25,43 +28,109 @@ namespace sat {
s(s),
m_out(0)
{
if (s.m_config.m_drat) {
m_out = alloc(std::ofstream, "proof.drat");
if (s.m_config.m_drat && s.m_config.m_drat_file != symbol()) {
m_out = alloc(std::ofstream, s.m_config.m_drat_file.str().c_str());
}
}
drat::~drat() {
dealloc(m_out);
}
void drat::add_empty() {
(*m_out) << "0\n";
std::ostream& operator<<(std::ostream& out, drat::status st) {
switch (st) {
case drat::status::learned: return out << "l";
case drat::status::asserted: return out << "a";
case drat::status::deleted: return out << "d";
default: return out;
}
}
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();
void drat::dump(unsigned sz, literal const* c, status st) {
if (is_cleaned(sz, c)) return;
switch (st) {
case status::asserted: return;
case status::learned: break;
case status::deleted: (*m_out) << "d "; break;
}
literal last = null_literal;
for (unsigned i = 0; i < sz; ++i) {
(*m_out) << c[i] << " ";
if (c[i] != last) {
(*m_out) << c[i] << " ";
last = c[i];
}
}
(*m_out) << "0\n";
}
void drat::del_literal(literal l) {
(*m_out) << "d ";
add_literal(l);
bool drat::is_cleaned(unsigned n, literal const* c) const {
literal last = null_literal;
for (unsigned i = 0; i < n; ++i) {
if (c[i] == last) return true;
last = c[i];
}
return false;
}
void drat::del_binary(literal l1, literal l2) {
(*m_out) << "d ";
add_binary(l1, l2);
void drat::append(unsigned n, literal const* c, status st) {
if (is_cleaned(n, c)) return;
m_status.push_back(st);
m_proof.push_back(0); // TBD
std::cout << st << " ";
literal last = null_literal;
for (unsigned i = 0; i < n; ++i) {
if (c[i] != last) {
std::cout << c[i] << " ";
last = c[i];
}
}
std::cout << "\n";
}
void drat::del_clause(clause& c) {
(*m_out) << "d ";
add_clause(c);
drat::status drat::get_status(bool learned) const {
return learned || s.m_searching ? status::learned : status::asserted;
}
void drat::add() {
if (m_out) (*m_out) << "0\n";
if (s.m_config.m_drat_check) append(0, 0, status::learned);
}
void drat::add(literal l, bool learned) {
status st = get_status(learned);
if (m_out) dump(1, &l, st);
if (s.m_config.m_drat_check) append(1, &l, st);
}
void drat::add(literal l1, literal l2, bool learned) {
literal ls[2] = {l1, l2};
status st = get_status(learned);
if (m_out) dump(2, ls, st);
if (s.m_config.m_drat_check) append(2, ls, st);
}
void drat::add(literal l1, literal l2, literal l3, bool learned) {
literal ls[3] = {l1, l2, l3};
status st = get_status(learned);
if (m_out) dump(3, ls, st);
if (s.m_config.m_drat_check) append(3, ls, get_status(learned));
}
void drat::add(clause& c, bool learned) {
status st = get_status(learned);
if (m_out) dump(c.size(), c.begin(), st);
if (s.m_config.m_drat_check) append(c.size(), c.begin(), get_status(learned));
}
void drat::del(literal l) {
if (m_out) dump(1, &l, status::deleted);
if (s.m_config.m_drat_check) append(1, &l, status::deleted);
}
void drat::del(literal l1, literal l2) {
literal ls[2] = {l1, l2};
if (m_out) dump(2, ls, status::deleted);
if (s.m_config.m_drat_check) append(2, ls, status::deleted);
}
void drat::del(clause& c) {
if (m_out) dump(c.size(), c.begin(), status::deleted);
if (s.m_config.m_drat_check) append(c.size(), c.begin(), status::deleted);
}
}

34
src/sat/sat_drat.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -21,19 +21,33 @@ Notes:
namespace sat {
class drat {
enum status { asserted, learned, deleted };
solver& s;
std::ostream* m_out;
std::ostream* m_out;
ptr_vector<clause> m_proof;
svector<status> m_status;
literal_vector m_units;
vector<watch_list> m_watches;
char_vector m_assignment;
void dump(unsigned n, literal const* lits, status st);
void append(unsigned n, literal const* lits, status st);
friend std::ostream& operator<<(std::ostream & out, status st);
status get_status(bool learned) const;
bool is_cleaned(unsigned n, literal const* lits) const;
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);
void add();
void add(literal l, bool learned);
void add(literal l1, literal l2, bool learned);
void add(literal l1, literal l2, literal l3, bool learned);
void add(clause& c, bool learned);
void del(literal l);
void del(literal l1, literal l2);
void del(clause& c);
};
};

5
src/sat/sat_params.pyg
View file

@ -25,4 +25,7 @@ def_module_params('sat',
('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'),
('drat', BOOL, False, 'produce DRAT proofs'),))
('drat', BOOL, False, 'produce DRAT proofs'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'),
))

26
src/sat/sat_solver.cpp
View file

@ -44,6 +44,7 @@ namespace sat {
m_mus(*this),
m_drat(*this),
m_inconsistent(false),
m_searching(false),
m_num_frozen(0),
m_activity_inc(128),
m_case_split_queue(m_activity),
@ -202,8 +203,9 @@ namespace sat {
void solver::del_clause(clause& c) {
if (!c.is_learned()) {
m_stats.m_non_learned_generation++;
} else if (m_config.m_drat) {
m_drat.del_clause(c);
}
if (m_config.m_drat) {
m_drat.del(c);
}
m_cls_allocator.del_clause(&c);
m_stats.m_del_clause++;
@ -222,7 +224,7 @@ namespace sat {
switch (num_lits) {
case 0:
if (m_config.m_drat) m_drat.add_empty();
if (m_config.m_drat) m_drat.add();
set_conflict(justification());
return 0;
case 1:
@ -239,8 +241,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 (m_config.m_drat)
m_drat.add(l1, l2, learned);
if (propagate_bin_clause(l1, l2)) {
if (at_base_lvl())
return;
@ -274,8 +276,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]);
if (m_config.m_drat)
m_drat.add(lits[0], lits[1], lits[2], learned);
m_stats.m_mk_ter_clause++;
clause * r = m_cls_allocator.mk_clause(3, lits, learned);
bool reinit = attach_ter_clause(*r);
@ -321,10 +323,12 @@ namespace sat {
if (reinit && !learned) push_reinit_stack(*r);
if (learned) {
m_learned.push_back(r);
if (m_config.m_drat) m_drat.add_clause(*r);
}
else
else {
m_clauses.push_back(r);
}
if (m_config.m_drat)
m_drat.add(*r, learned);
return r;
}
@ -529,8 +533,9 @@ namespace sat {
SASSERT(value(l) == l_undef);
TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
if (at_base_lvl()) {
if (m_config.m_drat) m_drat.add(l, !j.is_none());
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;
@ -753,6 +758,7 @@ namespace sat {
if (m_config.m_num_parallel > 1 && !m_par) {
return check_par(num_lits, lits);
}
flet<bool> _searching(m_searching, true);
#ifdef CLONE_BEFORE_SOLVING
if (m_mc.empty()) {
m_clone = alloc(solver, m_params, 0 /* do not clone extension */);

1
src/sat/sat_solver.h
View file

@ -90,6 +90,7 @@ namespace sat {
mus m_mus; // MUS for minimal core extraction
drat m_drat; // DRAT for generating proofs
bool m_inconsistent;
bool m_searching;
// 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
// justification for l, and the conflict is union of m_no_l and m_conflict;