From 2d0ff7d68a8fca6f0cdb60734f6d4232663aa654 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 May 2019 15:39:35 +0200 Subject: [PATCH] print literals more compactly Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 4 +--- src/smt/smt_literal.cpp | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index b6d58cd51..0ed69c03c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1424,9 +1424,7 @@ namespace smt { } void context::add_lit_occs(clause * cls) { - unsigned num_lits = cls->get_num_literals(); - for (unsigned i = 0; i < num_lits; i++) { - literal l = cls->get_literal(i); + for (literal l : *cls) { m_lit_occs[l.index()].insert(cls); } } diff --git a/src/smt/smt_literal.cpp b/src/smt/smt_literal.cpp index 86a9f0b0c..a52293aab 100644 --- a/src/smt/smt_literal.cpp +++ b/src/smt/smt_literal.cpp @@ -30,9 +30,9 @@ namespace smt { else if (*this == null_literal) out << "null"; else if (sign()) - out << "(not " << mk_pp(bool_var2expr_map[var()], m) << ")"; + out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m) << ")"; else - out << mk_pp(bool_var2expr_map[var()], m); + out << mk_bounded_pp(bool_var2expr_map[var()], m); } void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const {