mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix scc omitting blocked clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2a8a28bb59
commit
ba53fc1230
|
@ -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";
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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 << ")";
|
||||
}
|
||||
|
|
|
@ -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<symbol, symbol, symbol_hash_proc, symbol_eq_proc> symbol2symbol;
|
||||
symbol2symbol m_translate;
|
||||
typedef map<symbol, sym_b, symbol_hash_proc, symbol_eq_proc> 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 {
|
||||
|
|
|
@ -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(),
|
||||
|
|
|
@ -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; }
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue