mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

fixing Windows compile issue

Browse source
This commit is contained in:
nilsbecker 2019-02-22 14:09:35 +01:00
parent ec76efedbe
commit 6e508d4221
3 changed files with 40 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/bv_decl_plugin.cpp
View file

@ -18,7 +18,6 @@ Revision History:
--*/ --*/
#include<sstream> #include<sstream>
#include<iomanip> #include<iomanip>
#include<bitset>
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "util/warning.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); 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 { app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) }; parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); 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) { if (bv_size % 4 == 0) {
m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n";
} else { } else {
m_manager.trace_stream() << "#b" << std::bitset<sizeof(unsigned)*8>(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; 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) { for (unsigned i = 0; i < size; ++i) {
if (i == 0 && firstDigitLength != 0) { if (i == 0 && firstDigitLength != 0) {
m_manager.trace_stream() << std::bitset<digitBitSize>(digits[size-1]).to_string().substr(digitBitSize - firstDigitLength); log_binary_data(m_manager.trace_stream(), digits[size-1], firstDigitLength);
} else { } else {
m_manager.trace_stream() << std::bitset<digitBitSize>(digits[size-i-1]); log_binary_data(m_manager.trace_stream(), digits[size-i-1], digitBitSize);
} }
} }
m_manager.trace_stream() << "\n"; m_manager.trace_stream() << "\n";

18
src/smt/theory_jobscheduler.cpp
View file

@ -306,8 +306,10 @@ namespace smt {
literal end_ge_lo = mk_ge(ji.m_end, clb); literal end_ge_lo = mk_ge(ji.m_end, clb);
// Initialization ensures that satisfiable states have completion time below end. // Initialization ensures that satisfiable states have completion time below end.
ast_manager& m = get_manager(); 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()) {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 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(); region& r = ctx.get_region();
ctx.assign(end_ge_lo, ctx.assign(end_ge_lo,
ctx.mk_justification( ctx.mk_justification(
@ -383,8 +385,10 @@ namespace smt {
context& ctx = get_context(); context& ctx = get_context();
ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr);
ast_manager& m = get_manager(); 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()) {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 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; return true;
} }
@ -890,8 +894,10 @@ namespace smt {
if (ctx.is_diseq(e1, e2)) if (ctx.is_diseq(e1, e2))
continue; continue;
literal eq = mk_eq_lit(e1, e2); 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()) {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 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) { if (ctx.get_assignment(eq) != l_false) {
ctx.mark_as_relevant(eq); ctx.mark_as_relevant(eq);
if (assume_eq(e1, e2)) { if (assume_eq(e1, e2)) {

18
src/smt/theory_lra.cpp
View file

@ -1062,8 +1062,10 @@ public:
expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); 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); if (m.has_trace_stream()) th.log_axiom_instantiation(lo);
mk_axiom(mk_literal(lo)); mk_axiom(mk_literal(lo));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m.has_trace_stream()) {
if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_not(hi)); m.trace_stream() << "[end-of-instance]\n";
th.log_axiom_instantiation(m.mk_not(hi));
}
mk_axiom(~mk_literal(hi)); mk_axiom(~mk_literal(hi));
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
@ -1805,8 +1807,10 @@ public:
case lp::lia_move::branch: { case lp::lia_move::branch: {
TRACE("arith", tout << "branch\n";); TRACE("arith", tout << "branch\n";);
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); 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()) {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; 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";); IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";);
// branch on term >= k + 1 // branch on term >= k + 1
// branch on term <= k // branch on term <= k
@ -1820,8 +1824,10 @@ public:
++m_stats.m_gomory_cuts; ++m_stats.m_gomory_cuts;
// m_explanation implies term <= k // m_explanation implies term <= k
app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); 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()) {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; th.log_axiom_instantiation(b);
m.trace_stream() << "[end-of-instance]\n";
}
IF_VERBOSE(2, verbose_stream() << "cut " << b << "\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());); 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(); m_eqs.reset();