mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Remove m_final from spanning tree representation

Browse source
This commit is contained in:
Anh-Dung Phan 2013-11-06 13:30:29 -08:00
parent cf75a7743e
commit 034b33b6da
5 changed files with 55 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/opt/opt_solver.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include"smt_context.h" #include"smt_context.h"
#include"theory_arith.h" #include"theory_arith.h"
#include"theory_diff_logic.h" #include"theory_diff_logic.h"
#include "ast_pp.h"
namespace opt { namespace opt {
@ -94,7 +95,13 @@ namespace opt {
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) { lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt_solver_na2as", tout << "opt_opt_solver::check_sat_core: " << num_assumptions << "\n";); TRACE("opt_solver_na2as", {
tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n";
for (unsigned i = 0; i < m_context.size(); ++i) {
tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n";
}
});
lbool r = m_context.check(num_assumptions, assumptions); lbool r = m_context.check(num_assumptions, assumptions);
if (r == l_true && m_objective_enabled) { if (r == l_true && m_objective_enabled) {
m_objective_values.reset(); m_objective_values.reset();

2
src/opt/optimize_objectives.cpp
View file

@ -115,7 +115,7 @@ namespace opt {
verbose_stream() << m_lower[i] << " "; verbose_stream() << m_lower[i] << " ";
} }
verbose_stream() << "\n"; verbose_stream() << "\n";
// model_pp(verbose_stream(), *md); model_pp(verbose_stream(), *md);
); );
expr_ref_vector disj(m); expr_ref_vector disj(m);
expr_ref constraint(m); expr_ref constraint(m);

1
src/smt/network_flow.h
View file

@ -127,6 +127,7 @@ namespace smt {
bool check_well_formed(); bool check_well_formed();
bool is_preorder_traversal(node start, node end); bool is_preorder_traversal(node start, node end);
node get_final(int start);
public: public:

87
src/smt/network_flow_def.h
View file

@ -69,7 +69,6 @@ namespace smt {
m_pred.resize(num_nodes); m_pred.resize(num_nodes);
m_depth.resize(num_nodes); m_depth.resize(num_nodes);
m_thread.resize(num_nodes); m_thread.resize(num_nodes);
m_final.resize(num_nodes);
m_step = 0; m_step = 0;
} }
@ -84,7 +83,6 @@ namespace smt {
m_pred[root] = -1; m_pred[root] = -1;
m_depth[root] = 0; m_depth[root] = 0;
m_thread[root] = 0; m_thread[root] = 0;
m_final[root] = root - 1;
m_potentials[root] = numeral::zero(); m_potentials[root] = numeral::zero();
m_graph.init_var(root); m_graph.init_var(root);
@ -106,7 +104,6 @@ namespace smt {
m_pred[i] = root; m_pred[i] = root;
m_depth[i] = 1; m_depth[i] = 1;
m_thread[i] = i + 1; m_thread[i] = i + 1;
m_final[i] = i;
m_states[num_edges + i] = BASIS; m_states[num_edges + i] = BASIS;
node src = m_upwards[i] ? i : root; node src = m_upwards[i] ? i : root;
node tgt = m_upwards[i] ? root : i; node tgt = m_upwards[i] ? root : i;
@ -125,7 +122,6 @@ namespace smt {
TRACE("network_flow", { TRACE("network_flow", {
tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread);
tout << pp_vector("Last Successors", m_final);
tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards); tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards);
tout << pp_vector("Potentials", m_potentials) << pp_vector("Flows", m_flows); tout << pp_vector("Potentials", m_potentials) << pp_vector("Flows", m_flows);
}); });
@ -148,7 +144,7 @@ namespace smt {
node tgt = m_graph.get_target(m_entering_edge); node tgt = m_graph.get_target(m_entering_edge);
numeral cost = m_graph.get_weight(m_entering_edge); numeral cost = m_graph.get_weight(m_entering_edge);
numeral change = m_upwards[src] ? (-cost - m_potentials[src] + m_potentials[tgt]) : (cost + m_potentials[src] - m_potentials[tgt]); numeral change = m_upwards[src] ? (-cost - m_potentials[src] + m_potentials[tgt]) : (cost + m_potentials[src] - m_potentials[tgt]);
node last = m_thread[m_final[src]]; node last = m_thread[get_final(src)];
for (node u = src; u != last; u = m_thread[u]) { for (node u = src; u != last; u = m_thread[u]) {
m_potentials[u] += change; m_potentials[u] += change;
} }
@ -261,7 +257,6 @@ namespace smt {
template<typename Ext> template<typename Ext>
bool network_flow<Ext>::is_ancestor_of(node ancestor, node child) const { bool network_flow<Ext>::is_ancestor_of(node ancestor, node child) const {
for (node n = child; n != -1; n = m_pred[n]) { for (node n = child; n != -1; n = m_pred[n]) {
// q should be in T_v so swap p and q
if (n == ancestor) { if (n == ancestor) {
return true; return true;
} }
@ -295,26 +290,15 @@ namespace smt {
Old tree: New tree: Old tree: New tree:
root root root root
/ \ / \ / \ / \
x y x y x y
/ \ / \ / \ / \ / \ / \
u w' u s u s
| / | / /
v w v w v w
/ \ \ / \ \ / \ \
z p z p z p
\ \ \ /
q q q
x y
/ \ / \
u w'
/
v w
/ \ \
z p
\ /
q
*/ */
template<typename Ext> template<typename Ext>
@ -361,9 +345,12 @@ namespace smt {
} }
#else #else
node old_pred = m_pred[q]; node old_pred = m_pred[q];
m_pred[q] = p; if (q != v) {
for (node n = q; n != u; ) { for (node n = q; n != u; ) {
SASSERT(old_pred != u || n == v); // the last processed node is v SASSERT(old_pred != u || n == v); // the last processed node is v
TRACE("network_flow", {
tout << pp_vector("Predecessors", m_pred, true);
});
SASSERT(-1 != m_pred[old_pred]); SASSERT(-1 != m_pred[old_pred]);
node next_old_pred = m_pred[old_pred]; node next_old_pred = m_pred[old_pred];
swap_order(n, old_pred); swap_order(n, old_pred);
@ -372,22 +359,23 @@ namespace smt {
n = old_pred; n = old_pred;
old_pred = next_old_pred; old_pred = next_old_pred;
} }
}
m_pred[q] = p;
#endif #endif
// m_thread and m_final were updated. // m_thread were updated.
// update the depth. // update the depth.
fix_depth(q, m_final[q]); fix_depth(q, get_final(q));
TRACE("network_flow", { TRACE("network_flow", {
tout << pp_vector("Threads", m_thread, true); tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread);
tout << pp_vector("Depths", m_depth) << pp_vector("Upwards", m_upwards);
}); });
} }
/** /**
swap v and q in tree. swap v and q in tree.
- fixup m_final
- fixup m_thread - fixup m_thread
- fixup m_pred - fixup m_pred
@ -407,31 +395,27 @@ namespace smt {
void network_flow<Ext>::swap_order(node q, node v) { void network_flow<Ext>::swap_order(node q, node v) {
SASSERT(q != v); SASSERT(q != v);
SASSERT(m_pred[q] == v); SASSERT(m_pred[q] == v);
SASSERT(is_preorder_traversal(v, m_final[v])); SASSERT(is_preorder_traversal(v, get_final(v)));
node prev = find_rev_thread(v); node prev = find_rev_thread(v);
node final_q = m_final[q]; node final_q = get_final(q);
node final_v = m_final[v]; node final_v = get_final(v);
node next = m_thread[final_v]; node next = m_thread[final_v];
node alpha = find_rev_thread(q); node alpha = find_rev_thread(q);
if (final_q == final_v) { if (final_q == final_v) {
m_thread[final_q] = v; m_thread[final_q] = v;
m_thread[alpha] = next; m_thread[alpha] = next;
m_final[q] = alpha;
m_final[v] = alpha;
} }
else { else {
node beta = m_thread[final_q]; node beta = m_thread[final_q];
m_thread[final_q] = v; m_thread[final_q] = v;
m_thread[alpha] = beta; m_thread[alpha] = beta;
m_final[q] = final_v;
} }
m_thread[prev] = q; m_thread[prev] = q;
m_pred[v] = q; m_pred[v] = q;
SASSERT(is_preorder_traversal(q, m_final[q])); SASSERT(is_preorder_traversal(q, get_final(q)));
} }
template<typename Ext> template<typename Ext>
std::string network_flow<Ext>::display_spanning_tree() { std::string network_flow<Ext>::display_spanning_tree() {
++m_step;; ++m_step;;
@ -537,11 +521,11 @@ namespace smt {
roots[y] = x; roots[y] = x;
} }
static int get_final(int start, svector<int> const & thread, svector<int> const & depth) { template<typename Ext>
// really final or should one take into account connected tree? dl_var network_flow<Ext>::get_final(int start) {
int n = start; int n = start;
while (depth[thread[n]] > depth[start]) { while (m_depth[m_thread[n]] > m_depth[start]) {
n = thread[n]; n = m_thread[n];
} }
return n; return n;
} }
@ -566,7 +550,6 @@ namespace smt {
svector<node> m_pred; node |-> node svector<node> m_pred; node |-> node
svector<int> m_depth; node |-> int svector<int> m_depth; node |-> int
svector<node> m_thread; node |-> node svector<node> m_thread; node |-> node
svector<node> m_final; node |-> node
Tree is determined by m_pred: Tree is determined by m_pred:
- m_pred[root] == -1 - m_pred[root] == -1
@ -577,9 +560,6 @@ namespace smt {
Furthermore, the nodes linked in m_thread follows a Furthermore, the nodes linked in m_thread follows a
depth-first traversal order. depth-first traversal order.
m_final[n] is the last node in depth-first traversal order,
starting from n, that is still a child of n.
m_upwards direction of edge from i to m_pred[i] m_graph m_upwards direction of edge from i to m_pred[i] m_graph
*/ */
@ -593,6 +573,7 @@ namespace smt {
svector<bool> found(m_thread.size(), false); svector<bool> found(m_thread.size(), false);
found[root] = true; found[root] = true;
for (node x = m_thread[root]; x != root; x = m_thread[x]) { for (node x = m_thread[root]; x != root; x = m_thread[x]) {
SASSERT(x != m_thread[x]);
found[x] = true; found[x] = true;
} }
for (unsigned i = 0; i < found.size(); ++i) { for (unsigned i = 0; i < found.size(); ++i) {
@ -619,11 +600,6 @@ namespace smt {
SASSERT(m_depth[x] == m_depth[m_pred[x]] + 1); SASSERT(m_depth[x] == m_depth[m_pred[x]] + 1);
} }
// m_final of a node denotes the last node with a bigger depth
for (unsigned i = 0; i < m_final.size(); ++i) {
SASSERT(m_final[i] == get_final(i, m_thread, m_depth));
}
// m_thread forms a spanning tree over [0..root] // m_thread forms a spanning tree over [0..root]
// Union-find structure // Union-find structure
svector<int> roots(m_pred.size(), -1); svector<int> roots(m_pred.size(), -1);
@ -635,11 +611,6 @@ namespace smt {
merge(roots, x, y); merge(roots, x, y);
} }
std::cout << "roots" << std::endl;
for (unsigned i = 0; i < roots.size(); ++i) {
std::cout << i << " |-> " << roots[i] << std::endl;
}
// All nodes belong to the same spanning tree // All nodes belong to the same spanning tree
for (unsigned i = 0; i < roots.size(); ++i) { for (unsigned i = 0; i < roots.size(); ++i) {
SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0); SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0);

6
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -50,8 +50,8 @@ class blast_term_ite_tactic : public tactic {
bool max_steps_exceeded(unsigned num_steps) const { bool max_steps_exceeded(unsigned num_steps) const {
cooperate("blast term ite"); cooperate("blast term ite");
if (memory::get_allocation_size() > m_max_memory) // if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG); // throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
return false; return false;
} }
@ -62,6 +62,8 @@ class blast_term_ite_tactic : public tactic {
for (unsigned i = 0; i < num_args; ++i) { for (unsigned i = 0; i < num_args; ++i) {
expr* c, *t, *e; expr* c, *t, *e;
if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
enable_trace("blast_term_ite");
TRACE("blast_term_ite", result = m.mk_app(f, num_args, args); tout << result << "\n";);
expr_ref e1(m), e2(m); expr_ref e1(m), e2(m);
ptr_vector<expr> args1(num_args, args); ptr_vector<expr> args1(num_args, args);
args1[i] = t; args1[i] = t;