mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix validation code, disable PB compilation code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-08 14:08:51 -08:00
parent 72a7164e2d
commit 908dfd392e
3 changed files with 20 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/sat/ba_solver.cpp
View file

@ -2086,7 +2086,7 @@ namespace sat {
} }
lbool ba_solver::eval(model const& m, constraint const& c) const { lbool ba_solver::eval(model const& m, constraint const& c) const {
lbool v1 = c.lit() == null_literal ? l_true : value(c.lit()); lbool v1 = c.lit() == null_literal ? l_true : value(m, c.lit());
switch (c.tag()) { switch (c.tag()) {
case card_t: return eval(v1, eval(m, c.to_card())); case card_t: return eval(v1, eval(m, c.to_card()));
case pb_t: return eval(v1, eval(m, c.to_pb())); case pb_t: return eval(v1, eval(m, c.to_pb()));
@ -2118,7 +2118,7 @@ namespace sat {
lbool ba_solver::eval(model const& m, card const& c) const { lbool ba_solver::eval(model const& m, card const& c) const {
unsigned trues = 0, undefs = 0; unsigned trues = 0, undefs = 0;
for (literal l : c) { for (literal l : c) {
switch (l.sign() ? ~m[l.var()] : m[l.var()]) { switch (value(m, l)) {
case l_true: trues++; break; case l_true: trues++; break;
case l_undef: undefs++; break; case l_undef: undefs++; break;
default: break; default: break;
@ -2132,7 +2132,7 @@ namespace sat {
lbool ba_solver::eval(model const& m, pb const& p) const { lbool ba_solver::eval(model const& m, pb const& p) const {
unsigned trues = 0, undefs = 0; unsigned trues = 0, undefs = 0;
for (wliteral wl : p) { for (wliteral wl : p) {
switch (wl.second.sign() ? ~m[wl.second.var()] : m[wl.second.var()]) { switch (value(m, wl.second)) {
case l_true: trues += wl.first; break; case l_true: trues += wl.first; break;
case l_undef: undefs += wl.first; break; case l_undef: undefs += wl.first; break;
default: break; default: break;
@ -2174,7 +2174,7 @@ namespace sat {
bool odd = false; bool odd = false;
for (auto l : x) { for (auto l : x) {
switch (l.sign() ? ~m[l.var()] : m[l.var()]) { switch (value(m, l)) {
case l_true: odd = !odd; break; case l_true: odd = !odd; break;
case l_false: break; case l_false: break;
default: return l_undef; default: return l_undef;
@ -2736,9 +2736,10 @@ namespace sat {
} }
bool ba_solver::clausify(pb& p) { bool ba_solver::clausify(pb& p) {
return false;
if (get_config().m_card_solver) if (get_config().m_card_solver)
return false; return false;
bool ok = !p.learned(); bool ok = !p.learned();
bool is_def = p.lit() != null_literal; bool is_def = p.lit() != null_literal;
for (wliteral wl : p) { for (wliteral wl : p) {
@ -4094,21 +4095,21 @@ namespace sat {
bool ba_solver::check_model(model const& m) const { bool ba_solver::check_model(model const& m) const {
bool ok = true; bool ok = true;
for (constraint const* c : m_constraints) { for (constraint const* c : m_constraints) {
if (!check_model(m, *c)) ok = false; switch (eval(m, *c)) {
case l_false:
IF_VERBOSE(0, verbose_stream() << "failed checking " << c->id() << ": " << *c << "\n";);
ok = false;
break;
case l_true:
break;
case l_undef:
IF_VERBOSE(0, verbose_stream() << "undef " << c->id() << ": " << *c << "\n";);
break;
}
} }
return ok; return ok;
} }
bool ba_solver::check_model(model const& m, constraint const& c) const {
if (eval(m, c) != l_true) {
IF_VERBOSE(0, verbose_stream() << "failed checking " << c.id() << ": " << c << "\n";);
return false;
}
else {
return true;
}
}
}; };

3
src/sat/ba_solver.h
View file

@ -387,6 +387,8 @@ namespace sat {
// access solver // access solver
inline lbool value(bool_var v) const { return value(literal(v, false)); } inline lbool value(bool_var v) const { return value(literal(v, false)); }
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; }
inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); } inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); }
inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); } inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); }
inline bool inconsistent() const { inline bool inconsistent() const {
@ -467,7 +469,6 @@ namespace sat {
void copy_core(ba_solver* result, bool learned); void copy_core(ba_solver* result, bool learned);
void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints); void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
bool check_model(model const& m, constraint const& c) const;
public: public:
ba_solver(); ba_solver();
virtual ~ba_solver(); virtual ~ba_solver();

2
src/sat/sat_big.cpp
View file

@ -42,7 +42,7 @@ namespace sat {
m_roots[v.index()] = false; m_roots[v.index()] = false;
edges.push_back(v); edges.push_back(v);
} }
#if 1 #if 0
if (w.is_ext_constraint() && if (w.is_ext_constraint() &&
s.m_ext && s.m_ext &&
learned && learned &&