mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-24 20:21:22 -07:00
parent c714abbff2
commit 10ba731697
2 changed files with 55 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

91
src/smt/diff_logic.h
View file

@ -324,10 +324,11 @@ private:
// Store in gamma the normalized weight. The normalized weight is given // Store in gamma the normalized weight. The normalized weight is given
// by the formula // by the formula
// m_assignment[e.get_source()] - m_assignment[e.get_target()] + e.get_weight() // m_assignment[e.get_source()] - m_assignment[e.get_target()] + e.get_weight()
void set_gamma(const edge & e, numeral & gamma) { numeral& set_gamma(const edge & e, numeral & gamma) {
gamma = m_assignment[e.get_source()]; gamma = m_assignment[e.get_source()];
gamma -= m_assignment[e.get_target()]; gamma -= m_assignment[e.get_target()];
gamma += e.get_weight(); gamma += e.get_weight();
return gamma;
} }
void reset_marks() { void reset_marks() {
@ -373,7 +374,7 @@ private:
TRACE("arith", tout << id << "\n";); TRACE("arith", tout << id << "\n";);
dl_var source = target; dl_var source = target;
for(;;) { while (true) {
++m_stats.m_propagation_cost; ++m_stats.m_propagation_cost;
if (m_mark[root] != DL_UNMARKED) { if (m_mark[root] != DL_UNMARKED) {
// negative cycle was found // negative cycle was found
@ -680,8 +681,14 @@ private:
int m_total_count = 0; int m_total_count = 0;
int m_run_counter = -1; int m_run_counter = -1;
svector<int> m_hybrid_visited, m_hybrid_parent; svector<int> m_hybrid_visited, m_hybrid_parent;
bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const {
return (gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp;
}
public: public:
template<typename Functor> template<typename Functor>
bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
auto zero_edge = true; auto zero_edge = true;
@ -713,13 +720,12 @@ public:
continue; continue;
} }
set_gamma(e, gamma); set_gamma(e, gamma);
if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) if (is_connected(gamma, zero_edge, e, timestamp)) {
&& e.get_timestamp() < timestamp) {
dl_var curr_target = e.get_target(); dl_var curr_target = e.get_target();
if (curr_target == target) { if (curr_target == target) {
f(e.get_explanation()); f(e.get_explanation());
m_freq_hybrid[e_id]++; m_freq_hybrid[e_id]++;
for (;;) { while (true) {
int p = m_hybrid_parent[v]; int p = m_hybrid_parent[v];
if (p == -1) if (p == -1)
return true; return true;
@ -981,12 +987,12 @@ public:
} }
} }
void display_edge(std::ostream & out, edge_id id) const { std::ostream& display_edge(std::ostream & out, edge_id id) const {
display_edge(out, m_edges[id]); return display_edge(out, m_edges[id]);
} }
void display_edge(std::ostream & out, const edge & e) const { std::ostream& display_edge(std::ostream & out, const edge & e) const {
out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n"; return out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n";
} }
template<typename FilterAssignmentProc> template<typename FilterAssignmentProc>
@ -1233,17 +1239,11 @@ public:
m_dfs_time[v] = 0; m_dfs_time[v] = 0;
succ.push_back(v); succ.push_back(v);
numeral gamma; numeral gamma;
for (unsigned i = 0; i < succ.size(); ++i) { for (dl_var w : succ) {
v = succ[i]; for (edge_id e_id : m_out_edges[w]) {
edge_id_vector & edges = m_out_edges[v]; edge & e = m_edges[e_id];
for (edge_id e_id : edges) { if (e.is_enabled() && set_gamma(e, gamma).is_zero()) {
edge & e = m_edges[e_id]; SASSERT(e.get_source() == w);
if (!e.is_enabled()) {
continue;
}
SASSERT(e.get_source() == v);
set_gamma(e, gamma);
if (gamma.is_zero()) {
dl_var target = e.get_target(); dl_var target = e.get_target();
if (m_dfs_time[target] == -1) { if (m_dfs_time[target] == -1) {
succ.push_back(target); succ.push_back(target);
@ -1334,40 +1334,37 @@ private:
m_edge_id(e) { m_edge_id(e) {
} }
}; };
public: public:
// Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp. // Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp.
// The functor f is applied on every explanation attached to the edges in the shortest path. // The functor f is applied on every explanation attached to the edges in the shortest path.
// Return true if the path exists, false otherwise. // Return true if the path exists, false otherwise.
// Return true if the path exists, false otherwise. // Return true if the path exists, false otherwise.
template<typename Functor> template<typename Functor>
bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
return find_shortest_path_aux(source, target, timestamp, f, true); return find_shortest_path_aux(source, target, timestamp, f, true);
} }
template<typename Functor> template<typename Functor>
bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) {
return find_shortest_path_aux(source, target, timestamp, f, false); return find_shortest_path_aux(source, target, timestamp, f, false);
} }
template<typename Functor> template<typename Functor>
bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) { bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) {
svector<bfs_elem> bfs_todo; svector<bfs_elem> bfs_todo;
svector<char> bfs_mark; svector<bool> bfs_mark;
bfs_mark.resize(m_assignment.size(), false); bfs_mark.resize(m_assignment.size(), false);
bfs_todo.push_back(bfs_elem(source, -1, null_edge_id)); bfs_todo.push_back(bfs_elem(source, -1, null_edge_id));
bfs_mark[source] = true; bfs_mark[source] = true;
unsigned m_head = 0;
numeral gamma; numeral gamma;
while (m_head < bfs_todo.size()) { for (unsigned head = 0; head < bfs_todo.size(); ++head) {
bfs_elem & curr = bfs_todo[m_head]; bfs_elem & curr = bfs_todo[head];
int parent_idx = m_head; int parent_idx = head;
m_head++;
dl_var v = curr.m_var; dl_var v = curr.m_var;
TRACE("dl_bfs", tout << "processing: " << v << "\n";); TRACE("dl_bfs", tout << "processing: " << v << "\n";);
edge_id_vector & edges = m_out_edges[v]; edge_id_vector & edges = m_out_edges[v];
@ -1378,18 +1375,16 @@ public:
continue; continue;
} }
set_gamma(e, gamma); set_gamma(e, gamma);
TRACE("dl_bfs", tout << "processing edge: "; display_edge(tout, e); tout << "gamma: " << gamma << "\n";); TRACE("dl_bfs", display_edge(tout << "processing edge: ", e) << " gamma: " << gamma << "\n";);
if ((gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp) { if (is_connected(gamma, zero_edge, e, timestamp)) {
// if (gamma.is_zero() && e.get_timestamp() < timestamp)
dl_var curr_target = e.get_target(); dl_var curr_target = e.get_target();
TRACE("dl_bfs", tout << "curr_target: " << curr_target << TRACE("dl_bfs", tout << "curr_target: " << curr_target << ", mark: " << bfs_mark[curr_target] << "\n";);
", mark: " << static_cast<int>(bfs_mark[curr_target]) << "\n";);
if (curr_target == target) { if (curr_target == target) {
TRACE("dl_bfs", tout << "found path\n";); TRACE("dl_bfs", tout << "found path\n";);
TRACE("dl_eq_bug", tout << "path: " << source << " --> " << target << "\n"; TRACE("dl_eq_bug", tout << "path: " << source << " --> " << target << "\n";
display_edge(tout, e); display_edge(tout, e);
int tmp_parent_idx = parent_idx; int tmp_parent_idx = parent_idx;
for (;;) { while (true) {
bfs_elem & curr = bfs_todo[tmp_parent_idx]; bfs_elem & curr = bfs_todo[tmp_parent_idx];
if (curr.m_edge_id == null_edge_id) { if (curr.m_edge_id == null_edge_id) {
break; break;
@ -1399,11 +1394,10 @@ public:
display_edge(tout, e); display_edge(tout, e);
tmp_parent_idx = curr.m_parent_idx; tmp_parent_idx = curr.m_parent_idx;
} }
tout.flush();
}); });
TRACE("dl_eq_bug", display_edge(tout, e);); TRACE("dl_eq_bug", display_edge(tout, e););
f(e.get_explanation()); f(e.get_explanation());
for (;;) { while (true) {
SASSERT(parent_idx >= 0); SASSERT(parent_idx >= 0);
bfs_elem & curr = bfs_todo[parent_idx]; bfs_elem & curr = bfs_todo[parent_idx];
if (curr.m_edge_id == null_edge_id) { if (curr.m_edge_id == null_edge_id) {
@ -1417,11 +1411,9 @@ public:
} }
} }
} }
else { else if (!bfs_mark[curr_target]) {
if (!bfs_mark[curr_target]) { bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id));
bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id)); bfs_mark[curr_target] = true;
bfs_mark[curr_target] = true;
}
} }
} }
} }
@ -1507,8 +1499,7 @@ private:
numeral get_reduced_weight(dfs_state& state, dl_var n, edge const& e) { numeral get_reduced_weight(dfs_state& state, dl_var n, edge const& e) {
numeral gamma; numeral gamma;
set_gamma(e, gamma); return state.m_delta[n] + set_gamma(e, gamma);
return state.m_delta[n] + gamma;
} }
template<bool is_fw> template<bool is_fw>

28
src/smt/theory_special_relations.h
View file

@ -58,11 +58,11 @@ namespace smt {
} }
bool_var var() const { return m_bvar;} bool_var var() const { return m_bvar;}
relation& get_relation() const { return m_relation; } relation& get_relation() const { return m_relation; }
bool phase() { return m_phase; } bool phase() const { return m_phase; }
void set_phase(bool b) { m_phase = b; } void set_phase(bool b) { m_phase = b; }
theory_var v1() { return m_v1; } theory_var v1() const { return m_v1; }
theory_var v2() { return m_v2; } theory_var v2() const { return m_v2; }
literal explanation() { return literal(m_bvar, !m_phase); } literal explanation() const { return literal(m_bvar, !m_phase); }
bool enable() { bool enable() {
edge_id edge = m_phase?m_pos:m_neg; edge_id edge = m_phase?m_pos:m_neg;
return m_relation.m_graph.enable_edge(edge); return m_relation.m_graph.enable_edge(edge);
@ -112,16 +112,16 @@ namespace smt {
typedef u_map<atom*> bool_var2atom; typedef u_map<atom*> bool_var2atom;
special_relations_util m_util; special_relations_util m_util;
arith_util m_autil; arith_util m_autil;
atoms m_atoms; atoms m_atoms;
unsigned_vector m_atoms_lim; unsigned_vector m_atoms_lim;
obj_map<func_decl, relation*> m_relations; obj_map<func_decl, relation*> m_relations;
bool_var2atom m_bool_var2atom; bool_var2atom m_bool_var2atom;
scoped_ptr<solver> m_nested_solver; scoped_ptr<solver> m_nested_solver;
struct atom_hash { struct atom_hash {
size_t operator()(atom a) const { size_t operator()(atom const& a) const {
return std::hash<int>()(a.v1()) ^ std::hash<int>()(a.v2()) ^ std::hash<bool>()(a.phase()); return std::hash<int>()(a.v1()) ^ std::hash<int>()(a.v2()) ^ std::hash<bool>()(a.phase());
} }
}; };
@ -158,6 +158,13 @@ namespace smt {
bool is_strict_neighbour_edge(graph const& g, edge_id id) const; bool is_strict_neighbour_edge(graph const& g, edge_id id) const;
bool disconnected(graph const& g, dl_var u, dl_var v) const; bool disconnected(graph const& g, dl_var u, dl_var v) const;
literal mk_literal(expr* _e);
enode* ensure_enode(expr* e);
theory_var mk_var(enode* n);
void collect_asserted_po_atoms(vector< std::pair<bool_var,bool> >& atoms) const;
void display_atom(std::ostream & out, atom& a) const;
public: public:
theory_special_relations(ast_manager& m); theory_special_relations(ast_manager& m);
~theory_special_relations() override; ~theory_special_relations() override;
@ -182,13 +189,6 @@ namespace smt {
bool can_propagate() override { return false; } bool can_propagate() override { return false; }
void propagate() override {} void propagate() override {}
void display(std::ostream & out) const override; void display(std::ostream & out) const override;
literal mk_literal(expr* _e);
enode* ensure_enode(expr* e);
theory_var mk_var(enode* n);
void collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const;
void display_atom( std::ostream & out, atom& a) const;
}; };
} }