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

trying to fix build problems

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-21 14:45:12 -07:00
parent 8cbe257434
commit f8348d0bc4
3 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/ast/rewriter/pb_rewriter_def.h
View file

@ -59,7 +59,7 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
} }
} }
// sort and coalesce arguments: // sort and coalesce arguments:
PBU::compare cmp; typename PBU::compare cmp;
std::sort(args.begin(), args.end(), cmp); std::sort(args.begin(), args.end(), cmp);
// coallesce // coallesce
@ -110,9 +110,9 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
// <=> // <=>
// -c*~l + y >= k - c // -c*~l + y >= k - c
// //
PBU::numeral sum(0); typename PBU::numeral sum(0);
for (unsigned i = 0; i < args.size(); ++i) { 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()) { if (c.is_neg()) {
args[i].second = -c; args[i].second = -c;
args[i].first = m_util.negate(args[i].first); args[i].first = m_util.negate(args[i].first);
@ -152,7 +152,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
if (!all_int) { if (!all_int) {
// normalize to integers. // normalize to integers.
PBU::numeral d(denominator(k)); typename PBU::numeral d(denominator(k));
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
d = lcm(d, denominator(args[i].second)); d = lcm(d, denominator(args[i].second));
} }
@ -171,7 +171,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
// Ensure the largest coefficient is not larger than k: // Ensure the largest coefficient is not larger than k:
sum = PBU::numeral::zero(); sum = PBU::numeral::zero();
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
PBU::numeral c = args[i].second; typename PBU::numeral c = args[i].second;
if (c > k) { if (c > k) {
args[i].second = k; args[i].second = k;
} }
@ -188,9 +188,9 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
} }
// apply cutting plane reduction: // apply cutting plane reduction:
PBU::numeral g(0); typename PBU::numeral g(0);
for (unsigned i = 0; !g.is_one() && i < args.size(); ++i) { 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 (c != k) {
if (g.is_zero()) { if (g.is_zero()) {
g = c; g = c;
@ -214,13 +214,13 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
// Example 5x + 5y + 2z + 2u >= 5 // Example 5x + 5y + 2z + 2u >= 5
// becomes 3x + 3y + z + u >= 3 // 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. if (!(k % g).is_zero()) { // k_new is the ceiling of k / g.
k_new++; k_new++;
} }
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
SASSERT(args[i].second.is_pos()); SASSERT(args[i].second.is_pos());
PBU::numeral c = args[i].second; typename PBU::numeral c = args[i].second;
if (c == k) { if (c == k) {
c = k_new; c = k_new;
} }
@ -245,15 +245,15 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
// replace all coefficients by 1, and k by 2. // replace all coefficients by 1, and k by 2.
// //
if (!k.is_one()) { 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) { for (unsigned i = 1; i < args.size(); ++i) {
if (args[i].second < min) min = args[i].second; if (args[i].second < min) min = args[i].second;
if (args[i].second > max) max = args[i].second; if (args[i].second > max) max = args[i].second;
} }
SASSERT(min.is_pos()); SASSERT(min.is_pos());
PBU::numeral n0 = k/max; typename PBU::numeral n0 = k/max;
PBU::numeral n1 = floor(n0); typename PBU::numeral n1 = floor(n0);
PBU::numeral n2 = ceil(k/min) - PBU::numeral::one(); typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
if (n1 == n2 && !n0.is_int()) { if (n1 == n2 && !n0.is_int()) {
IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq);); IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq););
@ -272,7 +272,7 @@ void pb_rewriter_util<PBU>::prune(typename PBU::args_t& args, typename PBU::nume
if (is_eq) { if (is_eq) {
return; return;
} }
PBU::numeral nlt(0); typename PBU::numeral nlt(0);
unsigned occ = 0; unsigned occ = 0;
for (unsigned i = 0; nlt < k && i < args.size(); ++i) { for (unsigned i = 0; nlt < k && i < args.size(); ++i) {
if (args[i].second < k) { if (args[i].second < k) {

8
src/smt/theory_pb.cpp
View file

@ -625,7 +625,7 @@ namespace smt {
ctx.set_var_theory(bv, get_id()); ctx.set_var_theory(bv, get_id());
literal lit(ctx.get_bool_var(fml)); literal lit(ctx.get_bool_var(fml));
ctx.mk_th_axiom(get_id(), 1, &lit); 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); return negate?~literal(bv):literal(bv);
} }
@ -1146,8 +1146,8 @@ namespace smt {
struct theory_pb::psort_expr { struct theory_pb::psort_expr {
context& ctx; context& ctx;
ast_manager& m; ast_manager& m;
typedef literal literal; typedef smt::literal literal;
typedef literal_vector literal_vector; typedef smt::literal_vector literal_vector;
psort_expr(context& c): psort_expr(context& c):
ctx(c), ctx(c),
@ -1740,7 +1740,7 @@ namespace smt {
default: { default: {
app_ref tmp = m_lemma.to_expr(false, ctx, get_manager()); app_ref tmp = m_lemma.to_expr(false, ctx, get_manager());
internalize_atom(tmp, false); internalize_atom(tmp, false);
ctx.mark_as_relevant(tmp); ctx.mark_as_relevant(tmp.get());
literal l(ctx.get_bool_var(tmp)); literal l(ctx.get_bool_var(tmp));
add_assign(c, m_ineq_literals, l); add_assign(c, m_ineq_literals, l);
break; break;

4
src/util/sorting_network.h
View file

@ -40,8 +40,8 @@ Notes:
void exchange(unsigned i, unsigned j, vect& out) { void exchange(unsigned i, unsigned j, vect& out) {
SASSERT(i <= j); SASSERT(i <= j);
if (i < j) { if (i < j) {
Ext::T ei = out.get(i); typename Ext::T ei = out.get(i);
Ext::T ej = out.get(j); typename Ext::T ej = out.get(j);
out.set(i, m_ext.mk_ite(m_ext.mk_le(ei, ej), ei, ej)); 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)); out.set(j, m_ext.mk_ite(m_ext.mk_le(ej, ei), ei, ej));
} }