mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-03 20:34:56 +01:00
parent eec153bb57
commit 2f6a9ba39b
3 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -307,7 +307,7 @@ namespace smt {
void context::assign_core(literal l, b_justification j, bool decision) {
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal_verbose(tout, l); tout << " level: " << m_scope_lvl << "\n";
display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););
m_assigned_literals.push_back(l);
m_assignment[l.index()] = l_true;

4
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 {
if (l.sign())
out << " (not " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << ") ";
out << " (not " << mk_pp(bool_var2expr(l.var()), m) << ") ";
else
out << " " << mk_bounded_pp(bool_var2expr(l.var()), m, 10) << " ";
out << " " << mk_pp(bool_var2expr(l.var()), m) << " ";
return out;
}

4
src/smt/smt_literal.cpp
View file

@ -30,9 +30,9 @@ namespace smt {
else if (*this == null_literal)
out << "null";
else if (sign())
out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m) << ")";
out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m, 3) << ")";
else
out << mk_bounded_pp(bool_var2expr_map[var()], m);
out << mk_bounded_pp(bool_var2expr_map[var()], m, 3);
}
void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const {