diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index d24d6f91b..ce9ce385a 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -118,12 +118,16 @@ namespace smt { /** \brief find node that points to 'n' in m_thread */ - node find_rev_thread(node n, node ancestor) const; + node find_rev_thread(node n) const; void fix_depth(node start, node end); + void swap_order(node q, node v); + bool check_well_formed(); + bool is_preorder_traversal(node start, node end); + public: network_flow(graph & g, vector const & balances); diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index f2829e6a2..079a5ae70 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -21,6 +21,7 @@ Notes: #define _NETWORK_FLOW_DEF_H_ #include"network_flow.h" +#include"uint_set.h" namespace smt { @@ -269,7 +270,9 @@ namespace smt { } template - dl_var network_flow::find_rev_thread(node n, node ancestor) const { + dl_var network_flow::find_rev_thread(node n) const { + node ancestor = m_pred[n]; + SASSERT(ancestor != -1); while (m_thread[ancestor] != n) { ancestor = m_thread[ancestor]; } @@ -279,21 +282,19 @@ namespace smt { template void network_flow::fix_depth(node start, node end) { SASSERT(m_pred[start] != -1); - // Increase depths of all children in T_q by the same amount - int d = 1 + m_depth[m_pred[start]] - m_depth[start]; - do { - m_depth[start] += d; - start = m_thread[start]; + m_depth[start] = m_depth[m_pred[start]]+1; + while (start != end) { + start = m_thread[start]; + m_depth[start] = m_depth[m_pred[start]]+1; } - while (start != end); } /** \brief add entering_edge, remove leaving_edge from spanning tree. - Old tree: - root - / \ + Old tree: New tree: + root root + / \ / \ x y / \ / \ u w' @@ -304,9 +305,6 @@ namespace smt { \ q - New tree: - root - / \ x y / \ / \ u w' @@ -350,6 +348,7 @@ namespace smt { // Initialize m_upwards[q] = q_upwards bool prev_upwards = q_upwards; +#if 0 for (node n = q, prev = p; n != u; ) { SASSERT(m_pred[n] != u || n == v); // the last processed node is v node next = m_pred[n]; @@ -360,96 +359,79 @@ namespace smt { n = next; SASSERT(n != -1); } +#else + node old_pred = m_pred[q]; + 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; + } - // At this point m_pred and m_upwards have been updated. - - TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards);); +#endif - - // - node x = m_final[p]; - node y = m_thread[x]; - node z = m_final[q]; - - // ---- - // update m_final. - - // Do this before updating data structures - node gamma_p = m_pred[m_thread[m_final[p]]]; - node gamma_v = m_pred[m_thread[m_final[v]]]; - node theta = m_thread[m_final[v]]; - - // Check that f(u) is not in T_v - bool found_final_u = false; - for (node n = v; n != theta; n = m_thread[n]) { - if (n == m_final[u]) { - found_final_u = true; - break; - } - } - node phi = find_rev_thread(v, u); - node delta = found_final_u ? phi : m_final[u]; - - TRACE("network_flow", tout << "Graft T_q and T_r'\n";); - - for (node n = p; n != gamma_p && n != -1; n = m_pred[n]) { - TRACE("network_flow", tout << "1: m_final[" << n << "] |-> " << z << "\n";); - m_final[n] = z; - } - - // - - m_thread[x] = q; - m_thread[z] = y; + // m_thread and m_final were updated. + // update the depth. fix_depth(q, m_final[q]); - TRACE("network_flow", tout << "Update T_r'\n";); - - m_thread[phi] = theta; - - for (node n = u; n != gamma_v && n != -1; n = m_pred[n]) { - TRACE("network_flow", tout << "2: m_final[" << n << "] |-> " << delta << "\n";); - m_final[n] = delta; - } - - TRACE("network_flow", tout << pp_vector("Last Successors", m_final, true) << pp_vector("Depths", m_depth);); - - if (v != q) { - TRACE("network_flow", tout << "Reroot T_v at q\n";); - - node alpha1, alpha2; - node prev = q; - for (node n = v; n != q && n != -1; n = m_pred[n]) { - // Find all immediate successors of n - node t1 = m_thread[n]; - node t2 = m_thread[m_final[t1]]; - node t3 = m_thread[m_final[t2]]; - if (t1 == m_pred[n]) { - alpha1 = t2; - alpha2 = t3; - } - else if (t2 == m_pred[n]) { - alpha1 = t1; - alpha2 = t3; - } - else { - alpha1 = t1; - alpha2 = t2; - } - m_thread[n] = alpha1; - m_thread[m_final[alpha1]] = alpha2; - m_thread[m_final[alpha2]] = prev; - prev = n; - } - m_thread[m_final[q]] = prev; - } - TRACE("network_flow", { tout << pp_vector("Threads", m_thread, true); }); } + /** + swap v and q in tree. + - fixup m_final + - fixup m_thread + - fixup m_pred + + Case 1: final(q) == final(v) + ------- + Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next + New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next + + Case 2: final(q) != final(v) + ------- + Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next + New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next + + */ + + template + 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])); + node prev = find_rev_thread(v); + node final_q = m_final[q]; + node final_v = m_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]; + 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])); + } + + template std::string network_flow::display_spanning_tree() { ++m_step;; @@ -595,7 +577,8 @@ namespace smt { Furthermore, the nodes linked in m_thread follows a depth-first traversal order. - m_final[n] is deepest most node in a sub-tree rooted at n. + 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 @@ -670,6 +653,118 @@ namespace smt { return true; } + template + bool network_flow::is_preorder_traversal(node start, node end) { + + // get children of start: + uint_set children; + children.insert(start); + node root = m_pred.size()-1; + for (int i = 0; i < root; ++i) { + for (int j = 0; j < root; ++j) { + if (children.contains(m_pred[j])) { + children.insert(j); + } + } + } + // visit children using m_thread + children.remove(start); + do { + start = m_thread[start]; + SASSERT(children.contains(start)); + children.remove(start); + } + while (start != end); + SASSERT(children.empty()); + return true; + } + } #endif + +#if 0 + + // At this point m_pred and m_upwards have been updated. + + TRACE("network_flow", tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Upwards", m_upwards);); + + + // + node x = m_final[p]; + node y = m_thread[x]; + node z = m_final[q]; + + // ---- + // update m_final. + + // Do this before updating data structures + node gamma_p = m_pred[m_thread[m_final[p]]]; + node gamma_v = m_pred[m_thread[m_final[v]]]; + node theta = m_thread[m_final[v]]; + + // Check that f(u) is not in T_v + bool found_final_u = false; + for (node n = v; n != theta; n = m_thread[n]) { + if (n == m_final[u]) { + found_final_u = true; + break; + } + } + node phi = find_rev_thread(v); + node delta = found_final_u ? phi : m_final[u]; + + TRACE("network_flow", tout << "Graft T_q and T_r'\n";); + + for (node n = p; n != gamma_p && n != -1; n = m_pred[n]) { + TRACE("network_flow", tout << "1: m_final[" << n << "] |-> " << z << "\n";); + m_final[n] = z; + } + + // + + m_thread[x] = q; + m_thread[z] = y; + + + TRACE("network_flow", tout << "Update T_r'\n";); + + m_thread[phi] = theta; + + for (node n = u; n != gamma_v && n != -1; n = m_pred[n]) { + TRACE("network_flow", tout << "2: m_final[" << n << "] |-> " << delta << "\n";); + m_final[n] = delta; + } + + TRACE("network_flow", tout << pp_vector("Last Successors", m_final, true) << pp_vector("Depths", m_depth);); + + if (v != q) { + TRACE("network_flow", tout << "Reroot T_v at q\n";); + + node alpha1, alpha2; + node prev = q; + for (node n = v; n != q && n != -1; n = m_pred[n]) { + // Find all immediate successors of n + node t1 = m_thread[n]; + node t2 = m_thread[m_final[t1]]; + node t3 = m_thread[m_final[t2]]; + if (t1 == m_pred[n]) { + alpha1 = t2; + alpha2 = t3; + } + else if (t2 == m_pred[n]) { + alpha1 = t1; + alpha2 = t3; + } + else { + alpha1 = t1; + alpha2 = t2; + } + m_thread[n] = alpha1; + m_thread[m_final[alpha1]] = alpha2; + m_thread[m_final[alpha2]] = prev; + prev = n; + } + m_thread[m_final[q]] = prev; + } +#endif diff --git a/src/smt/theory_card.cpp b/src/smt/theory_card.cpp index 13b9e93c3..ecba59f1c 100644 --- a/src/smt/theory_card.cpp +++ b/src/smt/theory_card.cpp @@ -24,6 +24,7 @@ Notes: #include "theory_card.h" #include "smt_context.h" +#include "ast_pp.h" namespace smt { @@ -46,33 +47,59 @@ namespace smt { unsigned num_args = atom->get_num_args(); SASSERT(m_util.is_at_most_k(atom)); unsigned k = m_util.get_k(atom); - bool_var bv; + if (ctx.b_internalized(atom)) { return false; } + + TRACE("card", tout << "internalize: " << mk_pp(atom, m) << "\n";); + + if (k >= atom->get_num_args()) { + + NOT_IMPLEMENTED_YET(); + } + if (k == 0) { + NOT_IMPLEMENTED_YET(); + } + SASSERT(0 < k && k < atom->get_num_args()); SASSERT(!ctx.b_internalized(atom)); - bv = ctx.mk_bool_var(atom); - card* c = alloc(card, atom, bv, k); + bool_var bv = ctx.mk_bool_var(atom); + card* c = alloc(card, bv, k); add_card(c); - // - // TBD take repeated bv into account. - // base case: throw exception. - // refinement: adjust argument list and k for non-repeated values. - // for (unsigned i = 0; i < num_args; ++i) { expr* arg = atom->get_arg(i); if (!ctx.b_internalized(arg)) { - bv = ctx.mk_bool_var(arg); + ctx.internalize(arg, false); } - else { + + bool has_bv = false; + if (!m.is_not(arg) && ctx.b_internalized(arg)) { bv = ctx.get_bool_var(arg); + + if (null_theory_var == ctx.get_var_theory(bv)) { + ctx.set_var_theory(bv, get_id()); + has_bv = true; + } + else if (get_id() == ctx.get_var_theory(bv)) { + has_bv = true; + } } - if (null_theory_var == ctx.get_var_theory(bv)) { + // pre-processing should better remove negations under cardinality. + // assumes relevancy level = 2 or 0. + if (!has_bv) { + expr_ref tmp(m), fml(m); + tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort()); + fml = m.mk_iff(tmp, arg); + ctx.internalize(fml, false); + SASSERT(ctx.b_internalized(tmp)); + bv = ctx.get_bool_var(tmp); + SASSERT(null_theory_var == ctx.get_var_theory(bv)); ctx.set_var_theory(bv, get_id()); + literal lit(ctx.get_bool_var(fml)); + ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.mark_as_relevant(tmp); } - else { - SASSERT(ctx.get_var_theory(bv) == get_id()); // TBD, fishy - } + c->m_args.push_back(bv); add_watch(bv, c); } return true; @@ -110,12 +137,15 @@ namespace smt { void theory_card::assign_eh(bool_var v, bool is_true) { context& ctx = get_context(); + ast_manager& m = get_manager(); ptr_vector* cards = 0; card* c = 0; + TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";); + if (m_watch.find(v, cards)) { for (unsigned i = 0; i < cards->size(); ++i) { c = (*cards)[i]; - app* atm = c->m_atom; + svector const& args = c->m_args; // // is_true && m_t + 1 > k -> force false // !is_true && m_f + 1 >= arity - k -> force true @@ -128,10 +158,9 @@ namespace smt { case l_undef: { literal_vector& lits = get_lits(); lits.push_back(~literal(c->m_bv)); - for (unsigned i = 0; i < atm->get_num_args() && lits.size() < k + 1; ++i) { - expr* arg = atm->get_arg(i); - if (ctx.get_assignment(arg) == l_true) { - lits.push_back(~literal(ctx.get_bool_var(arg))); + for (unsigned i = 0; i < args.size() && lits.size() < k + 1; ++i) { + if (ctx.get_assignment(args[i]) == l_true) { + lits.push_back(~literal(args[i])); } } SASSERT(lits.size() == k + 1); @@ -142,17 +171,17 @@ namespace smt { break; } } - else if (!is_true && c->m_k >= atm->get_num_args() - c->m_f) { + else if (!is_true && c->m_k >= args.size() - c->m_f - 1) { // forced true switch (ctx.get_assignment(c->m_bv)) { case l_false: case l_undef: { + unsigned deficit = args.size() - c->m_k; literal_vector& lits = get_lits(); - lits.push_back(~literal(c->m_bv)); - for (unsigned i = 0; i < atm->get_num_args(); ++i) { - expr* arg = atm->get_arg(i); - if (ctx.get_assignment(arg) == l_false) { - lits.push_back(~literal(ctx.get_bool_var(arg))); + lits.push_back(literal(c->m_bv)); + for (unsigned i = 0; i < args.size() && lits.size() <= deficit; ++i) { + if (ctx.get_assignment(args[i]) == l_false) { + lits.push_back(literal(args[i])); } } add_clause(lits); @@ -173,10 +202,12 @@ namespace smt { } } if (m_cards.find(v, c)) { - app* atm = to_app(ctx.bool_var2expr(v)); - SASSERT(atm->get_num_args() >= c->m_f + c->m_t); + svector const& args = c->m_args; + SASSERT(args.size() >= c->m_f + c->m_t); bool_var bv; + TRACE("card", tout << " t:" << is_true << " k:" << c->m_k << " t:" << c->m_t << " f:" << c->m_f << "\n";); + // at most k // propagate false to children that are not yet assigned. // v & t1 & ... & tk => ~l_j @@ -185,8 +216,8 @@ namespace smt { literal_vector& lits = get_lits(); lits.push_back(literal(v)); bool done = false; - for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) { - bv = ctx.get_bool_var(atm->get_arg(i)); + for (unsigned i = 0; !done && i < args.size(); ++i) { + bv = args[i]; if (ctx.get_assignment(bv) == l_true) { lits.push_back(literal(bv)); } @@ -196,8 +227,8 @@ namespace smt { } } SASSERT(done || lits.size() == c->m_k + 1); - for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) { - bv = ctx.get_bool_var(atm->get_arg(i)); + for (unsigned i = 0; !done && i < args.size(); ++i) { + bv = args[i]; if (ctx.get_assignment(bv) == l_undef) { lits.push_back(literal(bv)); add_clause(lits); @@ -208,23 +239,22 @@ namespace smt { // at least k+1: // !v & !f1 & .. & !f_m => l_j // for m + k + 1 = arity() - if (!is_true && atm->get_num_args() == 1 + c->m_f + c->m_k) { + if (!is_true && args.size() <= 1 + c->m_f + c->m_k) { literal_vector& lits = get_lits(); - lits.push_back(~literal(v)); + lits.push_back(literal(v)); bool done = false; - for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) { - bv = ctx.get_bool_var(atm->get_arg(i)); + for (unsigned i = 0; !done && i < args.size(); ++i) { + bv = args[i]; if (ctx.get_assignment(bv) == l_false) { - lits.push_back(~literal(bv)); + lits.push_back(literal(bv)); } if (lits.size() > c->m_k + 1) { add_clause(lits); done = true; } } - SASSERT(done || lits.size() == c->m_k + 1); - for (unsigned i = 0; !done && i < atm->get_num_args(); ++i) { - bv = ctx.get_bool_var(atm->get_arg(i)); + for (unsigned i = 0; !done && i < args.size(); ++i) { + bv = args[i]; if (ctx.get_assignment(bv) != l_false) { lits.push_back(~literal(bv)); add_clause(lits); @@ -276,3 +306,315 @@ namespace smt { } } + +#if 0 + +class sorting { + void exchange(unsigned i, unsigned j, expr_ref_vector& es) { + SASSERT(i <= j); + if (i == j) { + return; + } + expr* ei = es[i].get(); + expr* ej = es[j].get(); + es[i] = m.mk_ite(mk_le(ei,ej), ei, ej); + es[j] = m.mk_ite(mk_le(ej,ei), ei, ej); + } + + void sort(unsigned k) { + if (k == 2) { + for (unsigned i = 0; i < m_es.size()/2; ++i) { + exchange(current(2*i), current(2*i+1), m_es); + next(2*i) = current(2*i); + next(2*i+1) = current(2*i+1); + } + std::swap(m_current, m_next); + } + else { + + for (unsigned i = 0; i < m_es.size()/k; ++i) { + for (unsigned j = 0; j < k / 2; ++j) { + next((k * i) + j) = current((k * i) + (2 * j)); + next((k * i) + (k / 2) + j) = current((k * i) + (2 * j) + 1); + } + } + + std::swap(m_current, m_next); + sort(k / 2); + for (unsigned i = 0; i < m_es.size() / k; ++i) { + for (unsigned j = 0; j < k / 2; ++j) { + next((k * i) + (2 * j)) = current((k * i) + j); + next((k * i) + (2 * j) + 1) = current((k * i) + (k / 2) + j); + } + + for (unsigned j = 0; j < (k / 2) - 1; ++j) { + exchange(next((k * i) + (2 * j) + 1), next((k * i) + (2 * (j + 1)))); + } + } + std::swap(m_current, m_next); + } + } + + private Term[] Merge(Term[] l1, Term[] l2) + { + if (l1.Length == 0) + { + return l2; + } + else if (l2.Length == 0) + { + return l1; + } + else if (l1.Length == 1 && l2.Length == 1) + { + var merged = new Term[2]; + merged[0] = l1[0]; + merged[1] = l2[0]; + Exchange(0, 1, merged); + return merged; + } + + var l1o = l1.Length / 2; + var l2o = l2.Length / 2; + var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o; + var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o; + + Term[] evenl1 = new Term[l1e]; + Term[] oddl1 = new Term[l1o]; + for (int i = 0; i < l1.Length; ++i) + { + if (i % 2 == 0) + { + evenl1[i / 2] = l1[i]; + } + else + { + oddl1[i / 2] = l1[i]; + } + } + + Term[] evenl2 = new Term[l2e]; + Term[] oddl2 = new Term[l2o]; + for (int i = 0; i < l2.Length; ++i) + { + if (i % 2 == 0) + { + evenl2[i / 2] = l2[i]; + } + else + { + oddl2[i / 2] = l2[i]; + } + } + + var even = Merge(evenl1, evenl2); + var odd = Merge(oddl1, oddl2); + + Term[] merge = new Term[l1.Length + l2.Length]; + + for (int i = 0; i < merge.Length; ++i) + { + if (i % 2 == 0) + { + merge[i] = even[i / 2]; + if (i > 0) + { + Exchange(i - 1, i, merge); + } + } + else + { + if (i / 2 < odd.Length) + { + merge[i] = odd[i / 2]; + } + else + { + merge[i] = even[(i / 2) + 1]; + } + } + } + + return merge; + } + +}; + +Sorting networks used in Formula: + +namespace Microsoft.Formula.Execution +{ + using System; + using System.Diagnostics.Contracts; + using Microsoft.Z3; + + internal class SortingNetwork + { + private Term[] elements; + private int[] current; + private int[] next; + + public SortingNetwork(SymbolicState owner, Term[] inputs, Sort sortingDomain) + { + Contract.Requires(owner != null && inputs != null && sortingDomain != null); + Contract.Requires(inputs.Length > 0); + + Owner = owner; + Size = (int)Math.Pow(2, (int)Math.Ceiling(Math.Log(inputs.Length, 2))); + + if (Size == 1) + { + elements = new Term[1]; + elements[0] = inputs[0]; + } + else if (Size > 1) + { + var defaultElement = owner.Context.MkNumeral(0, sortingDomain); + + current = new int[Size]; + next = new int[Size]; + elements = new Term[Size]; + for (int i = 0; i < Size; ++i) + { + current[i] = i; + elements[i] = (i < Size - inputs.Length) ? defaultElement : inputs[i - (Size - inputs.Length)]; + } + + int k = 2; + Term xi; + while (k <= Size) + { + Sort(k); + + for (int i = 0; i < Size; ++i) + { + xi = owner.Context.MkFreshConst("x", sortingDomain); + owner.Context.AssertCnstr(owner.Context.MkEq(xi, elements[i])); + elements[i] = xi; + } + + for (int i = 0; i < elements.Length / k; ++i) + { + for (int j = 0; j < k - 1; ++j) + { + owner.Context.AssertCnstr(owner.Context.MkBvUle(elements[(k * i) + j], elements[(k * i) + j + 1])); + } + } + + k *= 2; + } + } + } + + public Term[] Outputs + { + get { return elements; } + } + + public int Size + { + get; + private set; + } + + public SymbolicState Owner + { + get; + private set; + } + + + private void Swap() + { + var tmp = current; + current = next; + next = tmp; + } + + private Term[] Merge(Term[] l1, Term[] l2) + { + if (l1.Length == 0) + { + return l2; + } + else if (l2.Length == 0) + { + return l1; + } + else if (l1.Length == 1 && l2.Length == 1) + { + var merged = new Term[2]; + merged[0] = l1[0]; + merged[1] = l2[0]; + Exchange(0, 1, merged); + return merged; + } + + var l1o = l1.Length / 2; + var l2o = l2.Length / 2; + var l1e = (l1.Length % 2 == 1) ? l1o + 1 : l1o; + var l2e = (l2.Length % 2 == 1) ? l2o + 1 : l2o; + + Term[] evenl1 = new Term[l1e]; + Term[] oddl1 = new Term[l1o]; + for (int i = 0; i < l1.Length; ++i) + { + if (i % 2 == 0) + { + evenl1[i / 2] = l1[i]; + } + else + { + oddl1[i / 2] = l1[i]; + } + } + + Term[] evenl2 = new Term[l2e]; + Term[] oddl2 = new Term[l2o]; + for (int i = 0; i < l2.Length; ++i) + { + if (i % 2 == 0) + { + evenl2[i / 2] = l2[i]; + } + else + { + oddl2[i / 2] = l2[i]; + } + } + + var even = Merge(evenl1, evenl2); + var odd = Merge(oddl1, oddl2); + + Term[] merge = new Term[l1.Length + l2.Length]; + + for (int i = 0; i < merge.Length; ++i) + { + if (i % 2 == 0) + { + merge[i] = even[i / 2]; + if (i > 0) + { + Exchange(i - 1, i, merge); + } + } + else + { + if (i / 2 < odd.Length) + { + merge[i] = odd[i / 2]; + } + else + { + merge[i] = even[(i / 2) + 1]; + } + } + } + + return merge; + } + } +} + + +#endif diff --git a/src/smt/theory_card.h b/src/smt/theory_card.h index f38084292..ca1d5a061 100644 --- a/src/smt/theory_card.h +++ b/src/smt/theory_card.h @@ -30,9 +30,9 @@ namespace smt { bool_var m_bv; unsigned m_t; unsigned m_f; - app* m_atom; - card(app* a, bool_var bv, unsigned k): - m_k(k), m_bv(bv), m_atom(a), m_t(0), m_f(0) + svector m_args; + card(bool_var bv, unsigned k): + m_k(k), m_bv(bv), m_t(0), m_f(0) {} };