From 63d480fd92989381db5e6e3c827de19d6a630d1c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Jan 2019 21:17:39 -0800 Subject: [PATCH] fix cnf check Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 2 +- src/sat/sat_drat.cpp | 85 ++++++++++++++++++++++++++- src/sat/sat_drat.h | 12 +++- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- 4 files changed, 96 insertions(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 66c175ac8..d23fd5043 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -361,7 +361,7 @@ namespace opt { mdl = m_model; fix_model(mdl); if (mdl) mdl->set_model_completion(true); - TRACE("opt", tout << *mdl;); + CTRACE("opt", mdl, tout << *mdl;); } void context::get_box_model(model_ref& mdl, unsigned index) { diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 529a6bc57..4707fa0ac 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -143,7 +143,7 @@ namespace sat { IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st);); if (st == status::learned) { - verify(n, c.begin()); + verify(c); } m_status.push_back(st); @@ -225,6 +225,55 @@ namespace sat { m_units.resize(num_units); bool ok = m_inconsistent; m_inconsistent = false; + + if (!ok) { + literal_vector lits(n, c); + IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n"); + for (unsigned v = 0; v < m_assignment.size(); ++v) { + lbool val = m_assignment[v]; + if (val != l_undef) { + IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n"); + } + } + for (clause* cp : s.m_clauses) { + clause& cl = *cp; + bool found = false; + for (literal l : cl) { + if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) { + found = true; + break; + } + } + if (!found) { + IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n"); + } + } + for (clause* cp : s.m_learned) { + clause& cl = *cp; + bool found = false; + for (literal l : cl) { + if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) { + found = true; + break; + } + } + if (!found) { + IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n"); + } + } + svector bin; + s.collect_bin_clauses(bin, true); + for (auto & b : bin) { + bool found = false; + if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true; + if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true; + if (!found) { + IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n"); + } + } + IF_VERBOSE(0, s.display(verbose_stream())); + exit(0); + } return ok; } @@ -280,7 +329,10 @@ namespace sat { void drat::verify(unsigned n, literal const* c) { if (m_check_unsat && !is_drup(n, c) && !is_drat(n, c)) { - std::cout << "Verification failed\n"; + literal_vector lits(n, c); + std::cout << "Verification of " << lits << " failed\n"; + s.display(std::cout); + exit(0); UNREACHABLE(); //display(std::cout); TRACE("sat", @@ -291,6 +343,35 @@ namespace sat { } } + bool drat::contains(unsigned n, literal const* lits) { + for (unsigned i = m_proof.size(); i-- > 0; ) { + clause& c = *m_proof[i]; + status st = m_status[i]; + if (match(n, lits, c)) { + return st != status::deleted; + } + } + return false; + } + + bool drat::match(unsigned n, literal const* lits, clause const& c) const { + if (n == c.size()) { + for (unsigned i = 0; i < n; ++i) { + literal lit1 = lits[i]; + bool found = false; + for (literal lit2 : c) { + if (lit1 == lit2) { + found = true; + break; + } + } + if (!found) return false; + } + return true; + } + return false; + } + void drat::display(std::ostream& out) const { out << "units: " << m_units << "\n"; for (unsigned i = 0; i < m_assignment.size(); ++i) { diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 64d796839..35da0c31a 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -67,7 +67,6 @@ namespace sat { void propagate(literal l); void assign_propagate(literal l); void del_watch(clause& c, literal l); - void verify(unsigned n, literal const* c); bool is_drup(unsigned n, literal const* c); bool is_drat(unsigned n, literal const* c); bool is_drat(unsigned n, literal const* c, unsigned pos); @@ -75,6 +74,7 @@ namespace sat { void trace(std::ostream& out, unsigned n, literal const* c, status st); void display(std::ostream& out) const; void validate_propagation() const; + bool match(unsigned n, literal const* lits, clause const& c) const; public: drat(solver& s); @@ -93,6 +93,16 @@ namespace sat { void del(literal l1, literal l2); void del(clause& c); + void verify(clause const& c) { verify(c.size(), c.begin()); } + void verify(unsigned n, literal const* c); + void verify(literal l1, literal l2) { literal lits[2] = {l1, l2}; verify(2, lits); } + void verify(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; verify(3, lits); } + + bool contains(clause const& c) { return contains(c.size(), c.begin()); } + bool contains(unsigned n, literal const* c); + bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); } + bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); } + void check_model(model const& m); }; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5eb613ac2..8823c40c5 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -279,7 +279,6 @@ public: } } else { - m_is_cnf &= is_clause(t); assert_expr_core(t); } } @@ -287,6 +286,7 @@ public: ast_manager& get_manager() const override { return m; } void assert_expr_core(expr * t) override { TRACE("goal2sat", tout << mk_pp(t, m) << "\n";); + m_is_cnf &= is_clause(t); m_fmls.push_back(t); } void set_produce_models(bool f) override {}