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

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-07 19:02:06 +01:00
parent 133f376172
commit 6b88446ee8
4 changed files with 349 additions and 122 deletions
Download patch file Download diff file Expand all files Collapse all files

448
src/sat/ba_solver.cpp
View file

File diff suppressed because it is too large Load diff

14
src/sat/ba_solver.h
View file

@ -79,7 +79,7 @@ namespace sat {
void set_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; } void set_size(unsigned sz) { SASSERT(sz <= m_size); m_size = sz; }
void update_literal(literal l) { m_lit = l; } void update_literal(literal l) { m_lit = l; }
bool was_removed() const { return m_removed; } bool was_removed() const { return m_removed; }
void remove() { m_removed = true; } void set_removed() { m_removed = true; }
void nullify_literal() { m_lit = null_literal; } void nullify_literal() { m_lit = null_literal; }
unsigned glue() const { return m_glue; } unsigned glue() const { return m_glue; }
void set_glue(unsigned g) { m_glue = g; } void set_glue(unsigned g) { m_glue = g; }
@ -199,7 +199,7 @@ namespace sat {
svector<uint64> m_coeffs; svector<uint64> m_coeffs;
uint64 m_k; uint64 m_k;
void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; } void reset(uint64 k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, unsigned c) { m_lits.push_back(l); m_coeffs.push_back(c); } void push(literal l, uint64 c) { m_lits.push_back(l); m_coeffs.push_back(c); }
}; };
solver* m_solver; solver* m_solver;
@ -286,7 +286,7 @@ namespace sat {
void cleanup_constraints(); void cleanup_constraints();
void cleanup_constraints(ptr_vector<constraint>& cs, bool learned); void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
void ensure_external(constraint const& c); void ensure_external(constraint const& c);
void remove_constraint(constraint& c); void remove_constraint(constraint& c, char const* reason);
// constraints // constraints
constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); } constraint& index2constraint(size_t idx) const { return *reinterpret_cast<constraint*>(idx); }
@ -304,6 +304,7 @@ namespace sat {
void nullify_tracking_literal(constraint& c); void nullify_tracking_literal(constraint& c);
void set_conflict(constraint& c, literal lit); void set_conflict(constraint& c, literal lit);
void assign(constraint& c, literal lit); void assign(constraint& c, literal lit);
bool assigned_above(literal above, literal below);
void get_antecedents(literal l, constraint const& c, literal_vector & r); void get_antecedents(literal l, constraint const& c, literal_vector & r);
bool validate_conflict(constraint const& c) const; bool validate_conflict(constraint const& c) const;
bool validate_unit_propagation(constraint const& c, literal alit) const; bool validate_unit_propagation(constraint const& c, literal alit) const;
@ -402,8 +403,13 @@ namespace sat {
bool validate_watch_literals() const; bool validate_watch_literals() const;
bool validate_watch_literal(literal lit) const; bool validate_watch_literal(literal lit) const;
bool validate_watched_constraint(constraint const& c) const; bool validate_watched_constraint(constraint const& c) const;
bool validate_watch(pb const& p) const; bool validate_watch(pb const& p, literal alit) const;
bool is_watching(literal lit, constraint const& c) const; bool is_watching(literal lit, constraint const& c) const;
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq const& pb);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, ineq& a, ineq& b);
literal translate_to_sat(solver& s, u_map<bool_var>& translation, literal lit);
ineq negate(ineq const& a) const;
void push_lit(literal_vector& lits, literal lit);
ineq m_A, m_B, m_C; ineq m_A, m_B, m_C;
void active2pb(ineq& p); void active2pb(ineq& p);

3
src/sat/sat_drat.cpp
View file

@ -272,7 +272,8 @@ namespace sat {
void drat::verify(unsigned n, literal const* c) { void drat::verify(unsigned n, literal const* c) {
if (!is_drup(n, c) && !is_drat(n, c)) { if (!is_drup(n, c) && !is_drat(n, c)) {
std::cout << "Verification failed\n"; std::cout << "Verification failed\n";
display(std::cout); UNREACHABLE();
//display(std::cout);
TRACE("sat", TRACE("sat",
tout << literal_vector(n, c) << "\n"; tout << literal_vector(n, c) << "\n";
display(tout); display(tout);

6
src/util/sorting_network.h
View file

@ -469,7 +469,9 @@ Notes:
} }
literal mk_ordered_1(bool full, bool is_eq, unsigned n, literal const* xs) { literal mk_ordered_1(bool full, bool is_eq, unsigned n, literal const* xs) {
if (n <= 1 && !is_eq) return ctx.mk_true(); if (n <= 1 && !is_eq) {
return ctx.mk_true();
}
if (n == 0) { if (n == 0) {
return ctx.mk_false(); return ctx.mk_false();
} }
@ -477,6 +479,8 @@ Notes:
return xs[0]; return xs[0];
} }
SASSERT(n > 1);
// y0 -> y1 // y0 -> y1
// x0 -> y0 // x0 -> y0
// x1 -> y1 // x1 -> y1