From c7ee532173b97b67e93f3d0b02f3d425bb1ff96f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jan 2018 10:44:40 -0800 Subject: [PATCH] fix static Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 6 ++++-- src/ast/format.cpp | 4 ++-- src/ast/pb_decl_plugin.cpp | 1 + src/ast/pb_decl_plugin.h | 1 - src/sat/ba_solver.cpp | 14 ++++++++------ src/sat/sat_solver/inc_sat_solver.cpp | 19 ++++++++++--------- src/sat/tactic/goal2sat.cpp | 22 ++++++++++++++-------- 7 files changed, 39 insertions(+), 28 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index f6169a851..e1db044da 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -122,8 +122,10 @@ format * smt2_pp_environment::pp_fdecl_params(format * fname, func_decl * f) { (f->get_parameter(i).is_ast() && is_func_decl(f->get_parameter(i).get_ast()))); if (f->get_parameter(i).is_int()) fs.push_back(mk_int(get_manager(), f->get_parameter(i).get_int())); - else if (f->get_parameter(i).is_rational()) - fs.push_back(mk_string(get_manager(), f->get_parameter(i).get_rational().to_string().c_str())); + else if (f->get_parameter(i).is_rational()) { + std::string str = f->get_parameter(i).get_rational().to_string(); + fs.push_back(mk_string(get_manager(), str.c_str())); + } else fs.push_back(pp_fdecl_ref(to_func_decl(f->get_parameter(i).get_ast()))); } diff --git a/src/ast/format.cpp b/src/ast/format.cpp index 835892121..6c2a02989 100644 --- a/src/ast/format.cpp +++ b/src/ast/format.cpp @@ -151,7 +151,7 @@ namespace format_ns { } format * mk_int(ast_manager & m, int i) { - static char buffer[128]; + char buffer[128]; #ifdef _WINDOWS sprintf_s(buffer, ARRAYSIZE(buffer), "%d", i); #else @@ -161,7 +161,7 @@ namespace format_ns { } format * mk_unsigned(ast_manager & m, unsigned u) { - static char buffer[128]; + char buffer[128]; #ifdef _WINDOWS sprintf_s(buffer, ARRAYSIZE(buffer), "%u", u); #else diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index 928680131..298733a94 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -19,6 +19,7 @@ Revision History: #include "ast/pb_decl_plugin.h" #include "ast/ast_util.h" +#include "ast/ast_pp.h" pb_decl_plugin::pb_decl_plugin(): m_at_most_sym("at-most"), diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index 7fdb592aa..94536dfd6 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -123,7 +123,6 @@ public: app* mk_fresh_bool(); - private: rational to_rational(parameter const& p) const; }; diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 5868c4289..d29f81fca 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -111,7 +111,7 @@ namespace sat { // card ba_solver::card::card(unsigned id, literal lit, literal_vector const& lits, unsigned k): - pb_base(card_t, id, lit, lits.size(), get_obj_size(lits.size()), k) { + pb_base(card_t, id, lit, lits.size(), get_obj_size(lits.size()), k) { for (unsigned i = 0; i < size(); ++i) { m_lits[i] = lits[i]; } @@ -420,17 +420,18 @@ namespace sat { sz = j; // _bad_id = p.id(); BADLOG(display(verbose_stream() << "simplify ", p, true)); - - p.set_size(sz); - p.set_k(p.k() - true_val); - if (p.k() == 1 && p.lit() == null_literal) { + unsigned k = p.k() - true_val; + + if (k == 1 && p.lit() == null_literal) { literal_vector lits(sz, p.literals().c_ptr()); s().mk_clause(sz, lits.c_ptr(), p.learned()); remove_constraint(p, "is clause"); return; } - else if (p.lit() == null_literal || value(p.lit()) == l_true) { + p.set_size(sz); + p.set_k(k); + if (p.lit() == null_literal || value(p.lit()) == l_true) { init_watch(p); } else { @@ -2621,6 +2622,7 @@ namespace sat { return; } + VERIFY(c.size() - c.k() >= sz - k); c.set_size(sz); c.set_k(k); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e0cc8e581..f0d945d59 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -32,6 +32,7 @@ Notes: #include "tactic/core/simplify_tactic.h" #include "model/model_smt2_pp.h" #include "model/model_v2_pp.h" +#include "model/model_evaluator.h" #include "tactic/bv/bit_blaster_model_converter.h" #include "tactic/core/propagate_values_tactic.h" #include "sat/sat_solver.h" @@ -831,18 +832,18 @@ private: #if 0 IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";); + model_evaluator eval(*m_model); for (expr * f : m_fmls) { expr_ref tmp(m); - if (m_model->eval(f, tmp, true)) { - CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n"; - model_smt2_pp(tout, m, *(m_model.get()), 0);); - if (!m.is_true(tmp)) { - IF_VERBOSE(0, verbose_stream() << "failed to verify: " << tmp << "\n";); - IF_VERBOSE(0, verbose_stream() << m_params << "\n";); - } - VERIFY(m.is_true(tmp)); + eval(f, tmp); + CTRACE("sat", !m.is_true(tmp), + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << mk_pp(f, m) << "\n"; + model_smt2_pp(tout, m, *(m_model.get()), 0);); + if (!m.is_true(tmp)) { + IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";); + IF_VERBOSE(0, verbose_stream() << m_params << "\n";); } + VERIFY(m.is_true(tmp)); } #endif } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 68d15c48f..0b9f9805a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -520,7 +520,7 @@ struct goal2sat::imp { } } - void convert_at_least_k(app* t, rational k, bool root, bool sign) { + void convert_at_least_k(app* t, rational const& k, bool root, bool sign) { SASSERT(k.is_unsigned()); sat::literal_vector lits; unsigned sz = m_result_stack.size(); @@ -539,7 +539,7 @@ struct goal2sat::imp { } } - void convert_at_most_k(app* t, rational k, bool root, bool sign) { + void convert_at_most_k(app* t, rational const& k, bool root, bool sign) { SASSERT(k.is_unsigned()); sat::literal_vector lits; unsigned sz = m_result_stack.size(); @@ -560,7 +560,7 @@ struct goal2sat::imp { } } - void convert_eq_k(app* t, rational k, bool root, bool sign) { + void convert_eq_k(app* t, rational const& k, bool root, bool sign) { SASSERT(k.is_unsigned()); sat::literal_vector lits; convert_pb_args(t->get_num_args(), lits); @@ -622,16 +622,20 @@ struct goal2sat::imp { } else if (t->get_family_id() == pb.get_family_id()) { ensure_extension(); + rational k; switch (t->get_decl_kind()) { case OP_AT_MOST_K: - convert_at_most_k(t, pb.get_k(t), root, sign); + k = pb.get_k(t); + convert_at_most_k(t, k, root, sign); break; case OP_AT_LEAST_K: - convert_at_least_k(t, pb.get_k(t), root, sign); + k = pb.get_k(t); + convert_at_least_k(t, k, root, sign); break; case OP_PB_LE: if (pb.has_unit_coefficients(t)) { - convert_at_most_k(t, pb.get_k(t), root, sign); + k = pb.get_k(t); + convert_at_most_k(t, k, root, sign); } else { convert_pb_le(t, root, sign); @@ -639,7 +643,8 @@ struct goal2sat::imp { break; case OP_PB_GE: if (pb.has_unit_coefficients(t)) { - convert_at_least_k(t, pb.get_k(t), root, sign); + k = pb.get_k(t); + convert_at_least_k(t, k, root, sign); } else { convert_pb_ge(t, root, sign); @@ -647,7 +652,8 @@ struct goal2sat::imp { break; case OP_PB_EQ: if (pb.has_unit_coefficients(t)) { - convert_eq_k(t, pb.get_k(t), root, sign); + k = pb.get_k(t); + convert_eq_k(t, k, root, sign); } else { convert_pb_eq(t, root, sign);