From f8348d0bc43c44ba97d1cc927370fe2d7915063c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Mar 2014 14:45:12 -0700 Subject: [PATCH] trying to fix build problems Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb_rewriter_def.h | 28 ++++++++++++++-------------- src/smt/theory_pb.cpp | 8 ++++---- src/util/sorting_network.h | 4 ++-- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/ast/rewriter/pb_rewriter_def.h b/src/ast/rewriter/pb_rewriter_def.h index 61d146136..e57f80277 100644 --- a/src/ast/rewriter/pb_rewriter_def.h +++ b/src/ast/rewriter/pb_rewriter_def.h @@ -59,7 +59,7 @@ void pb_rewriter_util::unique(typename PBU::args_t& args, typename PBU::num } } // sort and coalesce arguments: - PBU::compare cmp; + typename PBU::compare cmp; std::sort(args.begin(), args.end(), cmp); // coallesce @@ -110,9 +110,9 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: // <=> // -c*~l + y >= k - c // - PBU::numeral sum(0); + typename PBU::numeral sum(0); for (unsigned i = 0; i < args.size(); ++i) { - PBU::numeral c = args[i].second; + typename PBU::numeral c = args[i].second; if (c.is_neg()) { args[i].second = -c; args[i].first = m_util.negate(args[i].first); @@ -152,7 +152,7 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: if (!all_int) { // normalize to integers. - PBU::numeral d(denominator(k)); + typename PBU::numeral d(denominator(k)); for (unsigned i = 0; i < args.size(); ++i) { d = lcm(d, denominator(args[i].second)); } @@ -171,7 +171,7 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: // Ensure the largest coefficient is not larger than k: sum = PBU::numeral::zero(); for (unsigned i = 0; i < args.size(); ++i) { - PBU::numeral c = args[i].second; + typename PBU::numeral c = args[i].second; if (c > k) { args[i].second = k; } @@ -188,9 +188,9 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: } // apply cutting plane reduction: - PBU::numeral g(0); + typename PBU::numeral g(0); for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) { - PBU::numeral c = args[i].second; + typename PBU::numeral c = args[i].second; if (c != k) { if (g.is_zero()) { g = c; @@ -214,13 +214,13 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: // Example 5x + 5y + 2z + 2u >= 5 // becomes 3x + 3y + z + u >= 3 // - PBU::numeral k_new = div(k, g); + typename PBU::numeral k_new = div(k, g); if (!(k % g).is_zero()) { // k_new is the ceiling of k / g. k_new++; } for (unsigned i = 0; i < args.size(); ++i) { SASSERT(args[i].second.is_pos()); - PBU::numeral c = args[i].second; + typename PBU::numeral c = args[i].second; if (c == k) { c = k_new; } @@ -245,15 +245,15 @@ lbool pb_rewriter_util::normalize(typename PBU::args_t& args, typename PBU: // replace all coefficients by 1, and k by 2. // if (!k.is_one()) { - PBU::numeral min = args[0].second, max = args[0].second; + typename PBU::numeral min = args[0].second, max = args[0].second; for (unsigned i = 1; i < args.size(); ++i) { if (args[i].second < min) min = args[i].second; if (args[i].second > max) max = args[i].second; } SASSERT(min.is_pos()); - PBU::numeral n0 = k/max; - PBU::numeral n1 = floor(n0); - PBU::numeral n2 = ceil(k/min) - PBU::numeral::one(); + typename PBU::numeral n0 = k/max; + typename PBU::numeral n1 = floor(n0); + typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one(); if (n1 == n2 && !n0.is_int()) { IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq);); @@ -272,7 +272,7 @@ void pb_rewriter_util::prune(typename PBU::args_t& args, typename PBU::nume if (is_eq) { return; } - PBU::numeral nlt(0); + typename PBU::numeral nlt(0); unsigned occ = 0; for (unsigned i = 0; nlt < k && i < args.size(); ++i) { if (args[i].second < k) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index c610fe929..7976e27b3 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -625,7 +625,7 @@ namespace smt { 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); + ctx.mark_as_relevant(tmp.get()); } return negate?~literal(bv):literal(bv); } @@ -1146,8 +1146,8 @@ namespace smt { struct theory_pb::psort_expr { context& ctx; ast_manager& m; - typedef literal literal; - typedef literal_vector literal_vector; + typedef smt::literal literal; + typedef smt::literal_vector literal_vector; psort_expr(context& c): ctx(c), @@ -1740,7 +1740,7 @@ namespace smt { default: { app_ref tmp = m_lemma.to_expr(false, ctx, get_manager()); internalize_atom(tmp, false); - ctx.mark_as_relevant(tmp); + ctx.mark_as_relevant(tmp.get()); literal l(ctx.get_bool_var(tmp)); add_assign(c, m_ineq_literals, l); break; diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 8ba260cae..a1f58a3a7 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -40,8 +40,8 @@ Notes: void exchange(unsigned i, unsigned j, vect& out) { SASSERT(i <= j); if (i < j) { - Ext::T ei = out.get(i); - Ext::T ej = out.get(j); + typename Ext::T ei = out.get(i); + typename Ext::T ej = out.get(j); out.set(i, m_ext.mk_ite(m_ext.mk_le(ei, ej), ei, ej)); out.set(j, m_ext.mk_ite(m_ext.mk_le(ej, ei), ei, ej)); }