diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 50f1fbfed..d95261402 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include #include -#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" @@ -876,6 +875,17 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { return mk_numeral(val, bv_size); } +void log_binary_data(std::ostream &out, unsigned val, unsigned numBits) { + SASSERT(numBits <= sizeof(unsigned)*8); + for (int shift = numBits-1; shift >= 0; --shift) { + if (val & (1 << shift)) { + out << "1"; + } else { + out << "0"; + } + } + } + app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { parameter p[2] = { parameter(val), parameter(static_cast(bv_size)) }; app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); @@ -888,7 +898,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { if (bv_size % 4 == 0) { m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; } else { - m_manager.trace_stream() << "#b" << std::bitset(val.get_unsigned()).to_string().substr(sizeof(unsigned)*8 - bv_size) << "\n"; + m_manager.trace_stream() << "#b"; + log_binary_data(m_manager.trace_stream(), val.get_unsigned(), bv_size); + m_manager.trace_stream() << "\n"; } return r; } @@ -923,9 +935,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { } for (unsigned i = 0; i < size; ++i) { if (i == 0 && firstDigitLength != 0) { - m_manager.trace_stream() << std::bitset(digits[size-1]).to_string().substr(digitBitSize - firstDigitLength); + log_binary_data(m_manager.trace_stream(), digits[size-1], firstDigitLength); } else { - m_manager.trace_stream() << std::bitset(digits[size-i-1]); + log_binary_data(m_manager.trace_stream(), digits[size-i-1], digitBitSize); } } m_manager.trace_stream() << "\n"; diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index e878594f3..6b1034ab6 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -306,8 +306,10 @@ namespace smt { literal end_ge_lo = mk_ge(ji.m_end, clb); // Initialization ensures that satisfiable states have completion time below end. ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); + m.trace_stream() << "[end-of-instance]\n"; + } region& r = ctx.get_region(); ctx.assign(end_ge_lo, ctx.mk_justification( @@ -383,8 +385,10 @@ namespace smt { context& ctx = get_context(); ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); + m.trace_stream() << "[end-of-instance]\n"; + } return true; } @@ -890,8 +894,10 @@ namespace smt { if (ctx.is_diseq(e1, e2)) continue; literal eq = mk_eq_lit(e1, e2); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); + m.trace_stream() << "[end-of-instance]\n"; + } if (ctx.get_assignment(eq) != l_false) { ctx.mark_as_relevant(eq); if (assume_eq(e1, e2)) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6961f8e0b..5703e34dd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1062,8 +1062,10 @@ public: expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); if (m.has_trace_stream()) th.log_axiom_instantiation(lo); mk_axiom(mk_literal(lo)); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_not(hi)); + if (m.has_trace_stream()) { + m.trace_stream() << "[end-of-instance]\n"; + th.log_axiom_instantiation(m.mk_not(hi)); + } mk_axiom(~mk_literal(hi)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1805,8 +1807,10 @@ public: case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); + m.trace_stream() << "[end-of-instance]\n"; + } IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1820,8 +1824,10 @@ public: ++m_stats.m_gomory_cuts; // m_explanation implies term <= k app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); - if (m.has_trace_stream()) th.log_axiom_instantiation(b); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + th.log_axiom_instantiation(b); + m.trace_stream() << "[end-of-instance]\n"; + } IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset();