mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

update to logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-04 23:08:41 +03:00
parent 20754bc72d
commit 7e415c1b69
9 changed files with 54 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/ast/rewriter/seq_rewriter.cpp
View file

@ -549,7 +549,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case _OP_STRING_STRIDOF: case _OP_STRING_STRIDOF:
UNREACHABLE(); UNREACHABLE();
} }
CTRACE("seq_verbose", st != BR_FAILED, tout << f->get_name() << " " << result << "\n";); CTRACE("seq_verbose", st != BR_FAILED, tout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";);
return st; return st;
} }
@ -616,32 +616,31 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
m_util.str.get_concat(a, m_es); m_util.str.get_concat(a, m_es);
unsigned len = 0; unsigned len = 0;
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < m_es.size(); ++i) { for (expr* e : m_es) {
if (m_util.str.is_string(m_es[i].get(), b)) { if (m_util.str.is_string(e, b)) {
len += b.length(); len += b.length();
} }
else if (m_util.str.is_unit(m_es[i].get())) { else if (m_util.str.is_unit(e)) {
len += 1; len += 1;
} }
else if (m_util.str.is_empty(m_es[i].get())) { else if (m_util.str.is_empty(e)) {
// skip // skip
} }
else { else {
m_es[j] = m_es[i].get(); m_es[j++] = e;
++j;
} }
} }
if (j == 0) { if (j == 0) {
result = m_autil.mk_numeral(rational(len, rational::ui64()), true); result = m_autil.mk_int(len);
return BR_DONE; return BR_DONE;
} }
if (j != m_es.size() || j != 1) { if (j != m_es.size() || j != 1) {
expr_ref_vector es(m()); expr_ref_vector es(m());
for (unsigned i = 0; i < j; ++i) { for (unsigned i = 0; i < j; ++i) {
es.push_back(m_util.str.mk_length(m_es[i].get())); es.push_back(m_util.str.mk_length(m_es.get(i)));
} }
if (len != 0) { if (len != 0) {
es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true)); es.push_back(m_autil.mk_int(len));
} }
result = m_autil.mk_add(es.size(), es.c_ptr()); result = m_autil.mk_add(es.size(), es.c_ptr());
return BR_REWRITE2; return BR_REWRITE2;

2
src/smt/smt_clause.cpp
View file

@ -123,7 +123,7 @@ namespace smt {
if (lit.sign()) args[args.size()-1] = m.mk_not(args.back()); if (lit.sign()) args[args.size()-1] = m.mk_not(args.back());
} }
expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m); expr_ref disj(m.mk_or(args.size(), args.c_ptr()), m);
return out << mk_bounded_pp(disj, m, 3); return out << mk_pp(disj, m, 3);
} }
}; };

26
src/smt/smt_conflict_resolution.cpp
View file

@ -101,7 +101,7 @@ namespace smt {
*/ */
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) { void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
SASSERT(m_antecedents); SASSERT(m_antecedents);
TRACE("conflict_detail", TRACE("conflict_",
ast_manager& m = get_manager(); ast_manager& m = get_manager();
tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m); tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
switch (js.get_kind()) { switch (js.get_kind()) {
@ -333,7 +333,6 @@ namespace smt {
} }
if (lvl == m_conflict_lvl) { if (lvl == m_conflict_lvl) {
TRACE("conflict", m_ctx.display_literal(tout << "marking:", antecedent) << "\n";);
num_marks++; num_marks++;
} }
else { else {
@ -343,12 +342,21 @@ namespace smt {
} }
} }
void conflict_resolution::process_justification(justification * js, unsigned & num_marks) { void conflict_resolution::process_justification(literal consequent, justification * js, unsigned & num_marks) {
literal_vector & antecedents = m_tmp_literal_vector; literal_vector & antecedents = m_tmp_literal_vector;
antecedents.reset(); antecedents.reset();
justification2literals_core(js, antecedents); justification2literals_core(js, antecedents);
for (literal l : antecedents) for (literal l : antecedents)
process_antecedent(l, num_marks); process_antecedent(l, num_marks);
(void)consequent;
TRACE("conflict_smt2",
for (literal& l : antecedents) {
l.neg();
SASSERT(m_ctx.get_assignment(l) == l_false);
}
antecedents.push_back(consequent);
m_ctx.display_literals_smt2(tout, antecedents););
} }
/** /**
@ -505,8 +513,7 @@ namespace smt {
switch (js.get_kind()) { switch (js.get_kind()) {
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = js.get_clause(); clause * cls = js.get_clause();
TRACE("conflict", m_ctx.display_clause_detail(tout, cls);); TRACE("conflict_smt2", m_ctx.display_clause_smt2(tout, *cls););
TRACE("conflict", tout << literal_vector(cls->get_num_literals(), cls->begin()) << "\n";);
if (cls->is_lemma()) if (cls->is_lemma())
cls->inc_clause_activity(); cls->inc_clause_activity();
unsigned num_lits = cls->get_num_literals(); unsigned num_lits = cls->get_num_literals();
@ -530,17 +537,18 @@ namespace smt {
} }
justification * js = cls->get_justification(); justification * js = cls->get_justification();
if (js) if (js)
process_justification(js, num_marks); process_justification(consequent, js, num_marks);
break; break;
} }
case b_justification::BIN_CLAUSE: case b_justification::BIN_CLAUSE:
TRACE("conflict_smt2", m_ctx.display_literals_smt2(tout, consequent, ~js.get_literal()) << "\n";);
SASSERT(consequent.var() != js.get_literal().var()); SASSERT(consequent.var() != js.get_literal().var());
process_antecedent(js.get_literal(), num_marks); process_antecedent(js.get_literal(), num_marks);
break; break;
case b_justification::AXIOM: case b_justification::AXIOM:
break; break;
case b_justification::JUSTIFICATION: case b_justification::JUSTIFICATION:
process_justification(js.get_justification(), num_marks); process_justification(consequent, js.get_justification(), num_marks);
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
@ -572,11 +580,13 @@ namespace smt {
} }
while (num_marks > 0); while (num_marks > 0);
TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent); tout << "\n";); TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent)<< "\n";);
m_lemma[0] = ~consequent; m_lemma[0] = ~consequent;
m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var())); m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var()));
TRACE("conflict_smt2", m_ctx.display_literals_smt2(tout << "lemma:", m_lemma) << "\n";);
// TODO: // TODO:
// //
// equality optimization should go here. // equality optimization should go here.

2
src/smt/smt_conflict_resolution.h
View file

@ -177,7 +177,7 @@ namespace smt {
unsigned get_max_lvl(literal consequent, b_justification js); unsigned get_max_lvl(literal consequent, b_justification js);
unsigned skip_literals_above_conflict_level(); unsigned skip_literals_above_conflict_level();
void process_antecedent(literal antecedent, unsigned & num_marks); void process_antecedent(literal antecedent, unsigned & num_marks);
void process_justification(justification * js, unsigned & num_marks); void process_justification(literal consequent, justification * js, unsigned & num_marks);
bool_var_vector m_unmark; bool_var_vector m_unmark;
bool_var_vector m_lemma_min_stack; bool_var_vector m_lemma_min_stack;

2
src/smt/smt_context.cpp
View file

@ -3935,7 +3935,7 @@ namespace smt {
for (unsigned i = 0; i < num_lits; i++) { for (unsigned i = 0; i < num_lits; i++) {
literal l = lits[i]; literal l = lits[i];
tout << l << " "; tout << l << " ";
display_literal(tout, l); display_literal_smt2(tout, l);
tout << ", ilvl: " << get_intern_level(l.var()) << "\n" tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
<< mk_pp(bool_var2expr(l.var()), m) << "\n"; << mk_pp(bool_var2expr(l.var()), m) << "\n";
}); });

4
src/smt/smt_context.h
View file

@ -1318,8 +1318,12 @@ namespace smt {
std::ostream& display_literal_smt2(std::ostream& out, literal lit) const; std::ostream& display_literal_smt2(std::ostream& out, literal lit) const;
std::ostream& display_literals_smt2(std::ostream& out, literal l1, literal l2) const { literal ls[2] = { l1, l2 }; return display_literals_smt2(out, 2, ls); }
std::ostream& display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const; std::ostream& display_literals_smt2(std::ostream& out, unsigned num_lits, literal const* lits) const;
std::ostream& display_literals_smt2(std::ostream& out, literal_vector const& ls) const { return display_literals_smt2(out, ls.size(), ls.c_ptr()); }
std::ostream& display_literal_verbose(std::ostream & out, literal lit) const; std::ostream& display_literal_verbose(std::ostream & out, literal lit) const;
std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const; std::ostream& display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const;

10
src/smt/smt_context_pp.cpp
View file

@ -103,9 +103,9 @@ namespace smt {
std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const { std::ostream& context::display_literal_smt2(std::ostream& out, literal l) const {
if (l.sign()) if (l.sign())
out << " (not " << mk_pp(bool_var2expr(l.var()), m) << ") "; out << "(not " << mk_pp(bool_var2expr(l.var()), m) << ") ";
else else
out << " " << mk_pp(bool_var2expr(l.var()), m) << " "; out << mk_pp(bool_var2expr(l.var()), m) << " ";
return out; return out;
} }
@ -173,8 +173,7 @@ namespace smt {
} }
std::ostream& context::display_clause_smt2(std::ostream & out, clause const& cls) const { std::ostream& context::display_clause_smt2(std::ostream & out, clause const& cls) const {
cls.display_smt2(out, m, m_bool_var2expr.c_ptr()); return display_literals_smt2(out, cls.get_num_literals(), cls.begin());
return out;
} }
std::ostream& context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const { std::ostream& context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
@ -604,7 +603,8 @@ namespace smt {
case b_justification::JUSTIFICATION: { case b_justification::JUSTIFICATION: {
literal_vector lits; literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits); const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
out << "justification " << j.get_justification()->get_from_theory() << ": " << lits; out << "justification " << j.get_justification()->get_from_theory() << ": ";
display_literals_smt2(out, lits);
break; break;
} }
default: default:

13
src/smt/smt_literal.cpp
View file

@ -35,6 +35,19 @@ namespace smt {
out << mk_bounded_pp(bool_var2expr_map[var()], m, 3); out << mk_bounded_pp(bool_var2expr_map[var()], m, 3);
} }
void literal::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
if (*this == true_literal)
out << "true";
else if (*this == false_literal)
out << "false";
else if (*this == null_literal)
out << "null";
else if (sign())
out << "(not " << mk_pp(bool_var2expr_map[var()], m, 3) << ")";
else
out << mk_pp(bool_var2expr_map[var()], m, 3);
}
void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const { void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const {
if (*this == true_literal) if (*this == true_literal)
out << "true"; out << "true";

2
src/smt/smt_literal.h
View file

@ -63,6 +63,8 @@ namespace smt {
void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const; void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
void display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const; void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const;
unsigned hash() const { return m_val; } unsigned hash() const { return m_val; }