mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fix #2418, change types in sat_solver to avoid cast

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-24 11:52:28 -07:00
parent 809b0ebca7
commit 604e6b2705
4 changed files with 18 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/array_rewriter.cpp
View file

@ -315,6 +315,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c
sort_ref s = get_map_array_sort(f, num_args, args); sort_ref s = get_map_array_sort(f, num_args, args);
result = m_util.mk_const_array(s, value); result = m_util.mk_const_array(s, value);
} }
TRACE("array", tout << result << "\n";);
return BR_REWRITE2; return BR_REWRITE2;
} }

3
src/ast/rewriter/poly_rewriter_def.h
View file

@ -1041,8 +1041,9 @@ bool poly_rewriter<Config>::hoist_ite(expr* a, obj_hashtable<expr>& shared, nume
} }
rational k, g1; rational k, g1;
if (is_int_numeral(a, k)) { if (is_int_numeral(a, k)) {
normalize(k);
g = gcd(g, k); g = gcd(g, k);
return shared.empty(); return !is_minus_one(a) && shared.empty();
} }
ptr_buffer<expr> adds; ptr_buffer<expr> adds;
TO_BUFFER(is_add, adds, a); TO_BUFFER(is_add, adds, a);

6
src/sat/sat_solver.cpp
View file

@ -140,8 +140,8 @@ namespace sat {
// create new vars // create new vars
for (bool_var v = num_vars(); v < src.num_vars(); v++) { for (bool_var v = num_vars(); v < src.num_vars(); v++) {
bool ext = src.m_external[v] != 0; bool ext = src.m_external[v];
bool dvar = src.m_decision[v] != 0; bool dvar = src.m_decision[v];
VERIFY(v == mk_var(ext, dvar)); VERIFY(v == mk_var(ext, dvar));
if (src.was_eliminated(v)) { if (src.was_eliminated(v)) {
set_eliminated(v, true); set_eliminated(v, true);
@ -273,7 +273,7 @@ namespace sat {
} }
void solver::set_external(bool_var v) { void solver::set_external(bool_var v) {
if (m_external[v] != 0) return; if (m_external[v]) return;
m_external[v] = true; m_external[v] = true;
if (!m_ext) return; if (!m_ext) return;

24
src/sat/sat_solver.h
View file

@ -113,13 +113,13 @@ namespace sat {
clause_vector m_learned; clause_vector m_learned;
unsigned m_num_frozen; unsigned m_num_frozen;
vector<watch_list> m_watches; vector<watch_list> m_watches;
char_vector m_assignment; svector<lbool> m_assignment;
svector<justification> m_justification; svector<justification> m_justification;
svector<char> m_decision; svector<bool> m_decision;
svector<char> m_mark; svector<bool> m_mark;
svector<char> m_lit_mark; svector<bool> m_lit_mark;
svector<char> m_eliminated; svector<bool> m_eliminated;
svector<char> m_external; svector<bool> m_external;
unsigned_vector m_touched; unsigned_vector m_touched;
unsigned m_touch_index; unsigned m_touch_index;
literal_vector m_replay_assign; literal_vector m_replay_assign;
@ -311,18 +311,18 @@ namespace sat {
unsigned num_clauses() const override; unsigned num_clauses() const override;
void num_binary(unsigned& given, unsigned& learned) const; void num_binary(unsigned& given, unsigned& learned) const;
unsigned num_restarts() const { return m_restarts; } unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const override { return m_external[v] != 0; } bool is_external(bool_var v) const override { return m_external[v]; }
void set_external(bool_var v) override; void set_external(bool_var v) override;
void set_non_external(bool_var v) override; void set_non_external(bool_var v) override;
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
void set_eliminated(bool_var v, bool f) override; void set_eliminated(bool_var v, bool f) override;
bool was_eliminated(literal l) const { return was_eliminated(l.var()); } bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
unsigned scope_lvl() const { return m_scope_lvl; } unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; } unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
bool at_base_lvl() const override { return m_scope_lvl == 0; } bool at_base_lvl() const override { return m_scope_lvl == 0; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); } lbool value(literal l) const { return m_assignment[l.index()]; }
lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); } lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
unsigned lvl(bool_var v) const { return m_justification[v].level(); } unsigned lvl(bool_var v) const { return m_justification[v].level(); }
unsigned lvl(literal l) const { return m_justification[l.var()].level(); } unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
@ -386,10 +386,10 @@ namespace sat {
watch_list & get_wlist(literal l) { return m_watches[l.index()]; } watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; } watch_list const & get_wlist(literal l) const { return m_watches[l.index()]; }
watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; } watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; }
bool is_marked(bool_var v) const { return m_mark[v] != 0; } bool is_marked(bool_var v) const { return m_mark[v]; }
void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; } void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; }
void reset_mark(bool_var v) { SASSERT(is_marked(v)); m_mark[v] = false; } void reset_mark(bool_var v) { SASSERT(is_marked(v)); m_mark[v] = false; }
bool is_marked_lit(literal l) const { return m_lit_mark[l.index()] != 0; } bool is_marked_lit(literal l) const { return m_lit_mark[l.index()]; }
void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; } void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; }
void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; } void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; }
bool check_inconsistent(); bool check_inconsistent();