mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix static

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-18 10:44:40 -08:00
parent 7b8101c502
commit c7ee532173
7 changed files with 39 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/sat/ba_solver.cpp
View file

@ -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);

19
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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
}

22
src/sat/tactic/goal2sat.cpp
View file

@ -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);