From 61341b8879fa6f14c4cf1327e10745180fc75e8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Feb 2017 17:56:22 -0800 Subject: [PATCH] adding drat Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 2 + src/sat/sat_config.h | 2 + src/sat/sat_drat.cpp | 121 ++++++++++++++++++++++++++++++++--------- src/sat/sat_drat.h | 34 ++++++++---- src/sat/sat_params.pyg | 5 +- src/sat/sat_solver.cpp | 26 +++++---- src/sat/sat_solver.h | 1 + 7 files changed, 144 insertions(+), 47 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 3e132c738..77a93c1e9 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -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(); } diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 34983f451..03616b6d8 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -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; diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 7e30c18ff..26f0bc98e 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -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); } } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 9d34c57b4..0e2cfe262 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -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 m_proof; + svector m_status; + literal_vector m_units; + vector 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); }; }; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index feefe653f..69b2bcea1 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -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'), + )) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 54122c019..fb4caac43 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -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 _searching(m_searching, true); #ifdef CLONE_BEFORE_SOLVING if (m_mc.empty()) { m_clone = alloc(solver, m_params, 0 /* do not clone extension */); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 2ab9d5c50..5041feba2 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -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;