From f2e636c598d298ef72a0f21d172bfbbd856ab354 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Jan 2019 16:37:21 -0800 Subject: [PATCH] record simplified input clauses as lemmas Signed-off-by: Nikolaj Bjorner --- src/sat/sat_cleaner.cpp | 12 ++++-------- src/sat/sat_solver.cpp | 9 ++++++++- src/smt/mam.cpp | 2 +- src/smt/smt_clause.cpp | 20 ++++++++++++++++---- src/smt/smt_clause.h | 6 ++++-- src/smt/smt_context_pp.cpp | 9 ++++++++- src/smt/smt_quantifier.cpp | 19 +++++++++++++------ 7 files changed, 54 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index afdccc4c2..728931f15 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -78,7 +78,6 @@ 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(); @@ -134,10 +133,6 @@ namespace sat { 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 < sz) { - tmp.set(c.size(), c.begin(), c.is_learned()); - } c.shrink(new_sz); *it2 = *it; it2++; @@ -145,11 +140,12 @@ namespace sat { s.attach_clause(c); } if (s.m_config.m_drat && new_sz < sz) { - // for optimization, could also report deletion - // of previous version of clause. s.m_drat.add(c, true); - s.m_drat.del(*tmp.get()); + c.restore(sz); + s.m_drat.del(c); + c.shrink(new_sz); } + break; } } } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3c97a985f..fa1d9352d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -320,11 +320,18 @@ namespace sat { clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) { TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << (learned?" learned":" aux") << "\n";); if (!learned) { + unsigned old_sz = num_lits; bool keep = simplify_clause(num_lits, lits); TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";); if (!keep) { return nullptr; // clause is equivalent to true. } + // if an input clause is simplified, then log the simplified version as learned + if (!learned && old_sz > num_lits && m_config.m_drat) { + m_lemma.reset(); + m_lemma.append(num_lits, lits); + m_drat.add(m_lemma); + } ++m_stats.m_non_learned_generation; } @@ -706,7 +713,7 @@ namespace sat { if (curr != prev) { prev = curr; if (i != j) - lits[j] = lits[i]; + std::swap(lits[j], lits[i]); j++; } break; diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index a6b5e5515..836c1dfcc 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -3915,7 +3915,7 @@ namespace smt { SASSERT(bindings[i]->get_generation() <= max_generation); } #endif - unsigned min_gen, max_gen; + unsigned min_gen = 0, max_gen = 0; m_interpreter.get_min_max_top_generation(min_gen, max_gen); m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes); } diff --git a/src/smt/smt_clause.cpp b/src/smt/smt_clause.cpp index 2b9b8dd3e..a1f1f9f03 100644 --- a/src/smt/smt_clause.cpp +++ b/src/smt/smt_clause.cpp @@ -19,6 +19,7 @@ Revision History: #include "smt/smt_clause.h" #include "smt/smt_justification.h" #include "ast/ast_ll_pp.h" +#include "ast/ast_pp.h" namespace smt { /** @@ -96,22 +97,33 @@ namespace smt { } } - void clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { + std::ostream& clause::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; m_lits[i].display(out, m, bool_var2expr_map); } - out << ")"; + return out << ")"; } - void clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { + std::ostream& clause::display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { out << "(clause"; for (unsigned i = 0; i < m_num_literals; i++) { out << " "; m_lits[i].display_compact(out, bool_var2expr_map); } - out << ")"; + return out << ")"; + } + + std::ostream& clause::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const { + expr_ref_vector args(m); + for (unsigned i = 0; i < m_num_literals; i++) { + literal lit = m_lits[i]; + args.push_back(bool_var2expr_map[lit.var()]); + if (lit.sign()) args[args.size()-1] = m.mk_not(args.back()); + } + expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m); + return out << disj; } }; diff --git a/src/smt/smt_clause.h b/src/smt/smt_clause.h index f0b352e05..025e2389d 100644 --- a/src/smt/smt_clause.h +++ b/src/smt/smt_clause.h @@ -239,9 +239,11 @@ namespace smt { set_activity(get_activity() + 1); } - void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + std::ostream& display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + + std::ostream& display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; - void display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; + std::ostream& display_compact(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; unsigned hash() const { return get_ptr_hash(this); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 20a084c81..4eb997c2e 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -160,7 +160,7 @@ namespace smt { } void context::display_clause(std::ostream & out, clause const * cls) const { - cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr()); + cls->display_smt2(out, m_manager, m_bool_var2expr.c_ptr()); } void context::display_clauses(std::ostream & out, ptr_vector const & v) const { @@ -185,11 +185,18 @@ namespace smt { out << "binary clauses:\n"; first = false; } + expr_ref t1(m_manager), t2(m_manager); + literal2expr(neg_l1, t1); + literal2expr(l2, t2); + expr_ref disj(m_manager.mk_or(t1, t2), m_manager); + out << disj << "\n"; +#if 0 out << "(clause "; display_literal(out, neg_l1); out << " "; display_literal(out, l2); out << ")\n"; +#endif } } } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index ce621144e..68c58d330 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -17,7 +17,7 @@ Revision History: --*/ #include "ast/ast_pp.h" -#include "ast/ast_smt2_pp.h" +#include "ast/ast_ll_pp.h" #include "smt/smt_quantifier.h" #include "smt/smt_context.h" #include "smt/smt_quantifier_stat.h" @@ -260,13 +260,20 @@ namespace smt { m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; } - TRACE("quantifier", - tout << mk_pp(q, m()) << " "; + static unsigned count = 0; + CTRACE("quantifier", f != nullptr, + tout << (count++) << " " << q->get_id() << "\n"; + if (q->get_id() == 28 || true) { + tout << mk_ll_pp(q, m()) << "\n"; + } + ); + + CTRACE("quantifier_", f != nullptr, + tout << expr_ref(q, m()) << " "; for (unsigned i = 0; i < num_bindings; ++i) { - tout << mk_pp(bindings[i]->get_owner(), m()) << " "; + tout << expr_ref(bindings[i]->get_owner(), m()) << " "; } tout << "\n"; - tout << "inserted: " << (f != nullptr) << "\n"; ); return f != nullptr; @@ -646,7 +653,7 @@ namespace smt { m_lazy_mam->add_pattern(q, mp); } else { - TRACE("quantifier", tout << "adding:\n" << mk_ismt2_pp(mp, m) << "\n";); + TRACE("quantifier", tout << "adding:\n" << expr_ref(mp, m) << "\n";); m_mam->add_pattern(q, mp); } if (!unary)