From ba53fc12304fe936c338591bcb143286903cfc2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 Oct 2017 17:29:26 -0700 Subject: [PATCH] fix scc omitting blocked clauses Signed-off-by: Nikolaj Bjorner --- src/ast/ast_pp_util.cpp | 8 ++++---- src/ast/ast_smt_pp.cpp | 37 ++++++++++++++++++++----------------- src/ast/ast_smt_pp.h | 8 +++++--- src/ast/ast_translation.cpp | 2 +- src/sat/sat_clause.h | 4 ++-- src/sat/sat_scc.cpp | 4 ++-- 6 files changed, 34 insertions(+), 29 deletions(-) diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 677422b8a..455addf73 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -55,17 +55,17 @@ void ast_pp_util::display_decls(std::ostream& out) { void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) { if (neat) { smt2_pp_environment_dbg env(m); - for (unsigned i = 0; i < fmls.size(); ++i) { + for (expr* f : fmls) { out << "(assert "; - ast_smt2_pp(out, fmls[i], env); + ast_smt2_pp(out, f, env); out << ")\n"; } } else { ast_smt_pp ll_smt2_pp(m); - for (unsigned i = 0; i < fmls.size(); ++i) { + for (expr* f : fmls) { out << "(assert "; - ll_smt2_pp.display_expr_smt2(out, fmls[i]); + ll_smt2_pp.display_expr_smt2(out, f); out << ")\n"; } } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 906fd054b..189d305fc 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -124,16 +124,19 @@ bool smt_renaming::all_is_legal(char const* s) { smt_renaming::smt_renaming() { for (unsigned i = 0; i < ARRAYSIZE(m_predef_names); ++i) { symbol s(m_predef_names[i]); - m_translate.insert(s, s); + m_translate.insert(s, sym_b(s, false)); m_rev_translate.insert(s, s); } } -symbol smt_renaming::get_symbol(symbol s0) { +symbol smt_renaming::get_symbol(symbol s0, bool is_skolem) { + sym_b sb; symbol s; - if (m_translate.find(s0, s)) { - return s; + if (m_translate.find(s0, sb)) { + if (is_skolem == sb.is_skolem) + return sb.name; + NOT_IMPLEMENTED_YET(); } int k = 0; @@ -141,7 +144,7 @@ symbol smt_renaming::get_symbol(symbol s0) { s = fix_symbol(s0, k++); } while (m_rev_translate.contains(s)); - m_translate.insert(s0, s); + m_translate.insert(s0, sym_b(s, is_skolem)); m_rev_translate.insert(s, s0); return s; } @@ -202,7 +205,7 @@ class smt_printer { } void pp_decl(func_decl* d) { - symbol sym = m_renaming.get_symbol(d->get_name()); + symbol sym = m_renaming.get_symbol(d->get_name(), d->is_skolem()); if (d->get_family_id() == m_dt_fid) { datatype_util util(m_manager); if (util.is_recognizer(d)) { @@ -313,7 +316,7 @@ class smt_printer { if (num_sorts > 0) { m_out << "("; } - m_out << m_renaming.get_symbol(s->get_name()); + m_out << m_renaming.get_symbol(s->get_name(), false); if (num_sorts > 0) { for (unsigned i = 0; i < num_sorts; ++i) { m_out << " "; @@ -324,7 +327,7 @@ class smt_printer { return; } else { - sym = m_renaming.get_symbol(s->get_name()); + sym = m_renaming.get_symbol(s->get_name(), false); } visit_params(true, sym, s->get_num_parameters(), s->get_parameters()); } @@ -396,17 +399,17 @@ class smt_printer { else if (m_manager.is_label(n, pos, names) && names.size() >= 1) { m_out << "(! "; pp_marked_expr(n->get_arg(0)); - m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0]) << ")"; + m_out << (pos?":lblpos":":lblneg") << " " << m_renaming.get_symbol(names[0], false) << ")"; } else if (m_manager.is_label_lit(n, names) && names.size() >= 1) { - m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0]) << ")"; + m_out << "(! true :lblpos " << m_renaming.get_symbol(names[0], false) << ")"; } else if (num_args == 0) { if (decl->private_parameters()) { - m_out << m_renaming.get_symbol(decl->get_name()); + m_out << m_renaming.get_symbol(decl->get_name(), decl->is_skolem()); } else { - symbol sym = m_renaming.get_symbol(decl->get_name()); + symbol sym = m_renaming.get_symbol(decl->get_name(), decl->is_skolem()); visit_params(false, sym, decl->get_num_parameters(), decl->get_parameters()); } } @@ -500,7 +503,7 @@ class smt_printer { for (unsigned i = 0; i < q->get_num_decls(); ++i) { sort* s = q->get_decl_sort(i); m_out << "("; - print_bound(m_renaming.get_symbol(q->get_decl_name(i))); + print_bound(m_renaming.get_symbol(q->get_decl_name(i), false)); m_out << " "; visit_sort(s, true); m_out << ") "; @@ -565,7 +568,7 @@ class smt_printer { unsigned num_decls = q->get_num_decls(); if (idx < num_decls) { unsigned offs = num_decls-idx-1; - symbol name = m_renaming.get_symbol(q->get_decl_name(offs)); + symbol name = m_renaming.get_symbol(q->get_decl_name(offs), false); print_bound(name); return; } @@ -807,15 +810,15 @@ public: m_out << ")"; } m_out << "("; - m_out << m_renaming.get_symbol(d->name()); + m_out << m_renaming.get_symbol(d->name(), false); m_out << " "; bool first_constr = true; for (datatype::constructor* f : *d) { if (!first_constr) m_out << " "; else first_constr = false; m_out << "("; - m_out << m_renaming.get_symbol(f->name()); + m_out << m_renaming.get_symbol(f->name(), false); for (datatype::accessor* a : *f) { - m_out << " (" << m_renaming.get_symbol(a->name()) << " "; + m_out << " (" << m_renaming.get_symbol(a->name(), false) << " "; visit_sort(a->range()); m_out << ")"; } diff --git a/src/ast/ast_smt_pp.h b/src/ast/ast_smt_pp.h index dd2a6d753..766c8530c 100644 --- a/src/ast/ast_smt_pp.h +++ b/src/ast/ast_smt_pp.h @@ -24,8 +24,10 @@ Revision History: #include "util/map.h" class smt_renaming { + struct sym_b { symbol name; bool is_skolem; sym_b(symbol n, bool s): name(n), is_skolem(s) {} sym_b():name(),is_skolem(false) {}}; typedef map symbol2symbol; - symbol2symbol m_translate; + typedef map symbol2sym_b; + symbol2sym_b m_translate; symbol2symbol m_rev_translate; symbol fix_symbol(symbol s, int k); @@ -35,8 +37,8 @@ class smt_renaming { bool all_is_legal(char const* s); public: smt_renaming(); - symbol get_symbol(symbol s0); - symbol operator()(symbol const & s) { return get_symbol(s); } + symbol get_symbol(symbol s0, bool is_skolem = false); + symbol operator()(symbol const & s, bool is_skolem = false) { return get_symbol(s, is_skolem); } }; class ast_smt_pp { diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp index 1bce4bcbe..0599ec91d 100644 --- a/src/ast/ast_translation.cpp +++ b/src/ast/ast_translation.cpp @@ -160,7 +160,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) { new_fi.set_chainable(fi->is_chainable()); new_fi.set_pairwise(fi->is_pairwise()); new_fi.set_injective(fi->is_injective()); - new_fi.set_skolem(fi->is_skolem()); +/// TBD new_fi.set_skolem(fi->is_skolem()); new_fi.set_idempotent(fi->is_idempotent()); new_f = m_to_manager.mk_func_decl(f->get_name(), diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h index dd8028ec2..dd7af64eb 100644 --- a/src/sat/sat_clause.h +++ b/src/sat/sat_clause.h @@ -65,8 +65,8 @@ namespace sat { literal & operator[](unsigned idx) { SASSERT(idx < m_size); return m_lits[idx]; } literal const & operator[](unsigned idx) const { SASSERT(idx < m_size); return m_lits[idx]; } bool is_learned() const { return m_learned; } - void unset_learned() { if (id() == 642277) std::cout << "unlearn " << *this << "\n"; SASSERT(is_learned()); m_learned = false; } - void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); if (id() == 642277) std::cout << "shrink " << *this << "\n"; } } + void unset_learned() { SASSERT(is_learned()); m_learned = false; } + void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; mark_strengthened(); } } bool strengthened() const { return m_strengthened; } void mark_strengthened() { m_strengthened = true; update_approx(); } void unmark_strengthened() { m_strengthened = false; } diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 089c5c55f..544ef1f66 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -107,7 +107,7 @@ namespace sat { frame & fr = frames.back(); unsigned l_idx = fr.m_lidx; if (!fr.m_first) { - SASSERT(fr.m_it->is_binary_unblocked_clause()); + SASSERT(fr.m_it->is_binary_clause()); // after visiting child literal l2 = fr.m_it->get_literal(); unsigned l2_idx = l2.index(); @@ -118,7 +118,7 @@ namespace sat { } fr.m_first = false; while (fr.m_it != fr.m_end) { - if (!fr.m_it->is_binary_unblocked_clause()) { + if (!fr.m_it->is_binary_clause()) { fr.m_it++; continue; }