diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 1c4a5bc4c..998214464 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -23,6 +23,7 @@ Notes: #include"smt_context.h" #include"theory_arith.h" #include"theory_diff_logic.h" +#include "ast_pp.h" namespace opt { @@ -94,7 +95,13 @@ namespace opt { 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); if (r == l_true && m_objective_enabled) { m_objective_values.reset(); diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index bcda00381..9705652fb 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -115,7 +115,7 @@ namespace opt { verbose_stream() << m_lower[i] << " "; } verbose_stream() << "\n"; - // model_pp(verbose_stream(), *md); + model_pp(verbose_stream(), *md); ); expr_ref_vector disj(m); expr_ref constraint(m); diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index ce9ce385a..a90e901e8 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -127,6 +127,7 @@ namespace smt { bool check_well_formed(); bool is_preorder_traversal(node start, node end); + node get_final(int start); public: diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 079a5ae70..96557301f 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -69,7 +69,6 @@ namespace smt { m_pred.resize(num_nodes); m_depth.resize(num_nodes); m_thread.resize(num_nodes); - m_final.resize(num_nodes); m_step = 0; } @@ -84,7 +83,6 @@ namespace smt { m_pred[root] = -1; m_depth[root] = 0; m_thread[root] = 0; - m_final[root] = root - 1; m_potentials[root] = numeral::zero(); m_graph.init_var(root); @@ -106,7 +104,6 @@ namespace smt { m_pred[i] = root; m_depth[i] = 1; m_thread[i] = i + 1; - m_final[i] = i; m_states[num_edges + i] = BASIS; node src = m_upwards[i] ? i : root; node tgt = m_upwards[i] ? root : i; @@ -125,7 +122,6 @@ namespace smt { TRACE("network_flow", { 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("Potentials", m_potentials) << pp_vector("Flows", m_flows); }); @@ -148,7 +144,7 @@ namespace smt { node tgt = m_graph.get_target(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]); - node last = m_thread[m_final[src]]; + node last = m_thread[get_final(src)]; for (node u = src; u != last; u = m_thread[u]) { m_potentials[u] += change; } @@ -261,7 +257,6 @@ namespace smt { template bool network_flow::is_ancestor_of(node ancestor, node child) const { for (node n = child; n != -1; n = m_pred[n]) { - // q should be in T_v so swap p and q if (n == ancestor) { return true; } @@ -295,26 +290,15 @@ namespace smt { Old tree: New tree: root root / \ / \ - x y - / \ / \ - u w' - | / - v w - / \ \ - z p - \ - q - - x y - / \ / \ - u w' - / - v w - / \ \ - z p - \ / - q - + x y x y + / \ / \ / \ / \ + u s u s + | / / + v w v w + / \ \ / \ \ + z p z p + \ \ / + q q */ template @@ -359,35 +343,39 @@ namespace smt { n = next; SASSERT(n != -1); } -#else - node old_pred = m_pred[q]; +#else + node old_pred = m_pred[q]; + if (q != v) { + for (node n = q; n != u; ) { + 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]); + node next_old_pred = m_pred[old_pred]; + swap_order(n, old_pred); + std::swap(m_upwards[n], prev_upwards); + prev_upwards = !prev_upwards; // flip previous version of upwards. + n = old_pred; + old_pred = next_old_pred; + } + } m_pred[q] = p; - for (node n = q; n != u; ) { - SASSERT(old_pred != u || n == v); // the last processed node is v - SASSERT(-1 != m_pred[old_pred]); - node next_old_pred = m_pred[old_pred]; - swap_order(n, old_pred); - std::swap(m_upwards[n], prev_upwards); - prev_upwards = !prev_upwards; // flip previous version of upwards. - n = old_pred; - old_pred = next_old_pred; - } - #endif - // m_thread and m_final were updated. + // m_thread were updated. // update the depth. - fix_depth(q, m_final[q]); + fix_depth(q, get_final(q)); 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. - - fixup m_final - fixup m_thread - fixup m_pred @@ -407,31 +395,27 @@ namespace smt { void network_flow::swap_order(node q, node v) { SASSERT(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 final_q = m_final[q]; - node final_v = m_final[v]; + node final_q = get_final(q); + node final_v = get_final(v); node next = m_thread[final_v]; node alpha = find_rev_thread(q); if (final_q == final_v) { m_thread[final_q] = v; m_thread[alpha] = next; - m_final[q] = alpha; - m_final[v] = alpha; } else { - node beta = m_thread[final_q]; + node beta = m_thread[final_q]; m_thread[final_q] = v; m_thread[alpha] = beta; - m_final[q] = final_v; } m_thread[prev] = q; m_pred[v] = q; - SASSERT(is_preorder_traversal(q, m_final[q])); + SASSERT(is_preorder_traversal(q, get_final(q))); } - template std::string network_flow::display_spanning_tree() { ++m_step;; @@ -537,11 +521,11 @@ namespace smt { roots[y] = x; } - static int get_final(int start, svector const & thread, svector const & depth) { - // really final or should one take into account connected tree? + template + dl_var network_flow::get_final(int start) { int n = start; - while (depth[thread[n]] > depth[start]) { - n = thread[n]; + while (m_depth[m_thread[n]] > m_depth[start]) { + n = m_thread[n]; } return n; } @@ -566,7 +550,6 @@ namespace smt { svector m_pred; node |-> node svector m_depth; node |-> int svector m_thread; node |-> node - svector m_final; node |-> node Tree is determined by m_pred: - m_pred[root] == -1 @@ -577,9 +560,6 @@ namespace smt { Furthermore, the nodes linked in m_thread follows a 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 */ @@ -593,6 +573,7 @@ namespace smt { svector found(m_thread.size(), false); found[root] = true; for (node x = m_thread[root]; x != root; x = m_thread[x]) { + SASSERT(x != m_thread[x]); found[x] = true; } for (unsigned i = 0; i < found.size(); ++i) { @@ -619,11 +600,6 @@ namespace smt { 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] // Union-find structure svector roots(m_pred.size(), -1); @@ -635,11 +611,6 @@ namespace smt { 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 for (unsigned i = 0; i < roots.size(); ++i) { SASSERT(roots[i] + roots.size() == 0 || roots[i] >= 0); diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index c69849253..fbc66c418 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -50,8 +50,8 @@ class blast_term_ite_tactic : public tactic { bool max_steps_exceeded(unsigned num_steps) const { cooperate("blast term ite"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + // if (memory::get_allocation_size() > m_max_memory) + // throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return false; } @@ -62,6 +62,8 @@ class blast_term_ite_tactic : public tactic { for (unsigned i = 0; i < num_args; ++i) { expr* 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); ptr_vector args1(num_args, args); args1[i] = t;