From 97dfb6d521ddd2c8fedd39cab27278aebe24041e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Nov 2013 15:55:08 -0800 Subject: [PATCH] moving to rational coefficients Signed-off-by: Nikolaj Bjorner --- src/api/api_pb.cpp | 10 ++- src/ast/pb_decl_plugin.cpp | 102 +++++++++++++++++--------- src/ast/pb_decl_plugin.h | 24 +++--- src/opt/objective_ast.h | 96 ++++++++++++++++++++++++ src/smt/theory_pb.cpp | 138 ++++++++++++++++++----------------- src/smt/theory_pb.h | 8 +- src/solver/tactic2solver.cpp | 2 +- 7 files changed, 261 insertions(+), 119 deletions(-) create mode 100644 src/opt/objective_ast.h diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index 17fe2f93e..6d5a56d2c 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -40,13 +40,17 @@ extern "C" { Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, - Z3_ast const args[], int coeffs[], + Z3_ast const args[], int _coeffs[], int k) { Z3_TRY; - LOG_Z3_mk_pble(c, num_args, args, coeffs, k); + LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); RESET_ERROR_CODE(); pb_util util(mk_c(c)->m()); - ast* a = util.mk_le(num_args, coeffs, to_exprs(args), k); + vector coeffs; + for (unsigned i = 0; i < num_args; ++i) { + coeffs.push_back(rational(_coeffs[i])); + } + ast* a = util.mk_le(num_args, coeffs.c_ptr(), to_exprs(args), rational(k)); mk_c(c)->save_ast_trail(a); check_sorts(c, a); RETURN_Z3(of_ast(a)); diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index 4cc317df3..07153e1ac 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -21,12 +21,13 @@ Revision History: pb_decl_plugin::pb_decl_plugin(): m_at_most_sym("at-most"), + m_at_least_sym("at-least"), m_pble_sym("pble"), m_pbge_sym("pbge") {} func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { SASSERT(m_manager); ast_manager& m = *m_manager; for (unsigned i = 0; i < arity; ++i) { @@ -34,37 +35,42 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p m.raise_exception("invalid non-Boolean sort applied to 'at-most'"); } } + symbol sym; switch(k) { + case OP_AT_LEAST_K: sym = m_at_least_sym; break; + case OP_AT_MOST_K: sym = m_at_most_sym; break; + case OP_PB_LE: sym = m_pble_sym; break; + case OP_PB_GE: sym = m_pbge_sym; break; + default: break; + } + switch(k) { + case OP_AT_LEAST_K: case OP_AT_MOST_K: { if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) { - m.raise_exception("function 'at-most' expects one non-negative integer parameter"); + m.raise_exception("function expects one non-negative integer parameter"); } - func_decl_info info(m_family_id, OP_AT_MOST_K, 1, parameters); - return m.mk_func_decl(m_at_most_sym, arity, domain, m.mk_bool_sort(), info); + func_decl_info info(m_family_id, k, 1, parameters); + return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info); } + case OP_PB_GE: case OP_PB_LE: { - if (num_parameters != 1 + arity || !parameters[0].is_int()) { - m.raise_exception("function 'pble' expects arity+1 integer parameters"); + if (num_parameters != 1 + arity) { + m.raise_exception("function expects arity+1 rational parameters"); } - for (unsigned i = 1; i < num_parameters; ++i) { - if (!parameters[i].is_int()) { + vector params; + for (unsigned i = 0; i < num_parameters; ++i) { + if (parameters[i].is_int()) { + params.push_back(parameter(rational(parameters[i].get_int()))); + } + else if (parameters[i].is_rational()) { + params.push_back(parameter(parameters[i].get_rational())); + } + else { m.raise_exception("function 'pble' expects arity+1 integer parameters"); } } - func_decl_info info(m_family_id, OP_PB_LE, num_parameters, parameters); - return m.mk_func_decl(m_pble_sym, arity, domain, m.mk_bool_sort(), info); - } - case OP_PB_GE: { - if (num_parameters != 1 + arity || !parameters[0].is_int()) { - m.raise_exception("function 'pbge' expects arity+1 integer parameters"); - } - for (unsigned i = 1; i < num_parameters; ++i) { - if (!parameters[i].is_int()) { - m.raise_exception("function 'pbge' expects arity+1 integer parameters"); - } - } - func_decl_info info(m_family_id, OP_PB_GE, num_parameters, parameters); - return m.mk_func_decl(m_pbge_sym, arity, domain, m.mk_bool_sort(), info); + func_decl_info info(m_family_id, k, num_parameters, params.c_ptr()); + return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info); } default: UNREACHABLE(); @@ -80,7 +86,7 @@ void pb_decl_plugin::get_op_names(svector & op_names, symbol const } } -app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k) { +app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) { vector params; params.push_back(parameter(k)); for (unsigned i = 0; i < num_args; ++i) { @@ -89,7 +95,7 @@ app * pb_util::mk_le(unsigned num_args, int const * coeffs, expr * const * args, return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort()); } -app * pb_util::mk_ge(unsigned num_args, int const * coeffs, expr * const * args, int k) { +app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) { vector params; params.push_back(parameter(k)); for (unsigned i = 0; i < num_args; ++i) { @@ -105,13 +111,11 @@ app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) return m.mk_app(m_fid, OP_AT_MOST_K, 1, ¶m, num_args, args, m.mk_bool_sort()); } - - bool pb_util::is_at_most_k(app *a) const { return is_app_of(a, m_fid, OP_AT_MOST_K); } -bool pb_util::is_at_most_k(app *a, unsigned& k) const { +bool pb_util::is_at_most_k(app *a, rational& k) const { if (is_at_most_k(a)) { k = get_k(a); return true; @@ -121,9 +125,35 @@ bool pb_util::is_at_most_k(app *a, unsigned& k) const { } } -int pb_util::get_k(app *a) const { - SASSERT(is_at_most_k(a) || is_le(a) || is_ge(a)); - return a->get_decl()->get_parameter(0).get_int(); + +app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k) { + parameter param(k); + return m.mk_app(m_fid, OP_AT_LEAST_K, 1, ¶m, num_args, args, m.mk_bool_sort()); +} + +bool pb_util::is_at_least_k(app *a) const { + return is_app_of(a, m_fid, OP_AT_LEAST_K); +} + +bool pb_util::is_at_least_k(app *a, rational& k) const { + if (is_at_least_k(a)) { + k = get_k(a); + return true; + } + else { + return false; + } +} + +rational pb_util::get_k(app *a) const { + parameter const& p = a->get_decl()->get_parameter(0); + if (is_at_most_k(a) || is_at_least_k(a)) { + return rational(p.get_int()); + } + else { + SASSERT(is_le(a) || is_ge(a)); + return p.get_rational(); + } } @@ -131,7 +161,7 @@ bool pb_util::is_le(app *a) const { return is_app_of(a, m_fid, OP_PB_LE); } -bool pb_util::is_le(app* a, int& k) const { +bool pb_util::is_le(app* a, rational& k) const { if (is_le(a)) { k = get_k(a); return true; @@ -145,7 +175,7 @@ bool pb_util::is_ge(app *a) const { return is_app_of(a, m_fid, OP_PB_GE); } -bool pb_util::is_ge(app* a, int& k) const { +bool pb_util::is_ge(app* a, rational& k) const { if (is_ge(a)) { k = get_k(a); return true; @@ -155,13 +185,13 @@ bool pb_util::is_ge(app* a, int& k) const { } } -int pb_util::get_coeff(app* a, unsigned index) { - if (is_at_most_k(a)) { - return 1; +rational pb_util::get_coeff(app* a, unsigned index) { + if (is_at_most_k(a) || is_at_least_k(a)) { + return rational::one(); } SASSERT(is_le(a) || is_ge(a)); SASSERT(1 + index < a->get_decl()->get_num_parameters()); - return a->get_decl()->get_parameter(index + 1).get_int(); + return a->get_decl()->get_parameter(index + 1).get_rational(); } diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index e7ab3ec25..4b768ff11 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -31,6 +31,7 @@ hence: enum pb_op_kind { OP_AT_MOST_K, // at most K Booleans are true. + OP_AT_LEAST_K, // at least K Booleans are true. OP_PB_LE, // pseudo-Boolean <= (generalizes at_most_k) OP_PB_GE, // pseudo-Boolean >= LAST_PB_OP @@ -39,11 +40,13 @@ enum pb_op_kind { class pb_decl_plugin : public decl_plugin { symbol m_at_most_sym; + symbol m_at_least_sym; symbol m_pble_sym; symbol m_pbge_sym; func_decl * mk_at_most(unsigned arity, unsigned k); - func_decl * mk_le(unsigned arity, int const* coeffs, int k); - func_decl * mk_ge(unsigned arity, int const* coeffs, int k); + func_decl * mk_at_least(unsigned arity, unsigned k); + func_decl * mk_le(unsigned arity, rational const* coeffs, int k); + func_decl * mk_ge(unsigned arity, rational const* coeffs, int k); public: pb_decl_plugin(); virtual ~pb_decl_plugin() {} @@ -76,16 +79,19 @@ public: ast_manager & get_manager() const { return m; } family_id get_family_id() const { return m_fid; } app * mk_at_most_k(unsigned num_args, expr * const * args, unsigned k); - app * mk_le(unsigned num_args, int const * coeffs, expr * const * args, int k); - app * mk_ge(unsigned num_args, int const * coeffs, expr * const * args, int k); + app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k); + app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); + app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k); bool is_at_most_k(app *a) const; - bool is_at_most_k(app *a, unsigned& k) const; - int get_k(app *a) const; + bool is_at_most_k(app *a, rational& k) const; + bool is_at_least_k(app *a) const; + bool is_at_least_k(app *a, rational& k) const; + rational get_k(app *a) const; bool is_le(app *a) const; - bool is_le(app* a, int& k) const; + bool is_le(app* a, rational& k) const; bool is_ge(app* a) const; - bool is_ge(app* a, int& k) const; - int get_coeff(app* a, unsigned index); + bool is_ge(app* a, rational& k) const; + rational get_coeff(app* a, unsigned index); }; diff --git a/src/opt/objective_ast.h b/src/opt/objective_ast.h new file mode 100644 index 000000000..b1005b40d --- /dev/null +++ b/src/opt/objective_ast.h @@ -0,0 +1,96 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + objective_ast.h + +Abstract: + Abstract data-type for compound objectives. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-21 + +Notes: + +--*/ +#ifndef __OBJECTIVE_AST_H_ +#define __OBJECTIVE_AST_H_ + +namespace opt { + + enum objective_t { + MINIMIZE, + MAXIMIZE, + MAXSAT, + LEX, + BOX, + PARETO + }; + + class compound_objective; + class min_max_objective; + class maxsat_objective; + + class objective { + objective_t m_type; + public: + objective(objective_t ty): + m_type(ty) + {} + virtual ~objective() {} + + objective_t type() const { return m_type; } + + // constructors; + static objective* mk_max(expr_ref& e); + static objective* mk_min(expr_ref& e); + static objective* mk_lex(unsigned sz, objective * const* children); + static objective* mk_box(unsigned sz, objective * const* children); + static objective* mk_pareto(unsigned sz, objective * const* children); + static objective* mk_maxsat(symbol id); + + // accessors (implicit cast operations) + compound_objective& get_compound(); // eg. SASSERT(m_type == LEX/BOX/PARETO); return dynamic_cast(*this); + min_max_objective& get_min_max(); + maxsat_objective& get_maxsat(); + }; + + class compound_objective : public objective { + ptr_vector m_children; + public: + compound_objective(objective_t t): objective(t) {} + virtual ~compound_objective() { + // dealloc vector m_children; + } + + objective *const* children() const { return m_children.c_ptr(); } + + unsigned num_children() const { return m_children.size(); } + } + + class min_max_objective : public objective { + bool m_is_max; + expr_ref m_expr; + public: + min_max_objective(bool is_max, expr_ref& e): m_is_max(is_max), m_expr(e) {} + + virtual ~min_max_objective() {} + + expr* term() { return m_expr; } + bool is_max() const { return m_is_max; } + }; + + class maxsat_objective : public objective { + symbol m_id; + public: + maxsat_objective(symbol const& id): m_id(id) {} + virtual ~maxsat_objective() {} + + symbol const& get_id() const { return m_id; } + }; + +}; + +#endif diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 8cc56926f..b46ad7e0d 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -30,44 +30,26 @@ namespace smt { void theory_pb::ineq::negate() { m_lit.neg(); - numeral sum = 0; + numeral sum(0); for (unsigned i = 0; i < size(); ++i) { m_args[i].first.neg(); sum += coeff(i); } - m_k = sum - m_k + 1; + m_k = sum - m_k + numeral::one(); SASSERT(well_formed()); } void theory_pb::ineq::reset() { - m_max_coeff = 0; + m_max_coeff.reset(); m_watch_sz = 0; - m_max_sum = 0; + m_max_sum.reset(); m_num_propagations = 0; m_compilation_threshold = UINT_MAX; m_compiled = l_false; m_args.reset(); - m_k = 0; + m_k.reset(); } - theory_pb::numeral theory_pb::ineq::gcd(numeral a, numeral b) { - while (a != b) { - if (a == 0) return b; - if (b == 0) return a; - SASSERT(a != 0 && b != 0); - if (a < b) { - b %= a; - } - else { - a %= b; - } - } - return a; - } - - theory_pb::numeral theory_pb::ineq::lcm(numeral a, numeral b) { - return (a*b)/gcd(a,b); - } void theory_pb::ineq::unique() { numeral& k = m_k; @@ -103,7 +85,7 @@ namespace smt { } args.pop_back(); } - if (coeff(i) == 0) { + if (coeff(i).is_zero()) { for (unsigned j = i; j + 1 < size(); ++j) { args[j] = args[j+1]; } @@ -127,10 +109,10 @@ namespace smt { // <=> // -c*~l + y >= k - c // - numeral sum = 0; + numeral sum(0); for (unsigned i = 0; i < size(); ++i) { numeral c = coeff(i); - if (c < 0) { + if (c.is_neg()) { args[i].second = -c; args[i].first = ~lit(i); k -= c; @@ -138,7 +120,7 @@ namespace smt { sum += coeff(i); } // detect tautologies: - if (k <= 0) { + if (k <= numeral::zero()) { args.reset(); return l_true; } @@ -147,8 +129,21 @@ namespace smt { args.reset(); return l_false; } + + // normalize to integers. + numeral d(denominator(k)); + for (unsigned i = 0; i < size(); ++i) { + d = lcm(d, denominator(coeff(i))); + } + if (!d.is_one()) { + k *= d; + for (unsigned i = 0; i < size(); ++i) { + args[i].second *= d; + } + } + // Ensure the largest coefficient is not larger than k: - sum = 0; + sum = numeral::zero(); for (unsigned i = 0; i < size(); ++i) { numeral c = coeff(i); if (c > k) { @@ -161,45 +156,52 @@ namespace smt { // normalize tight inequalities to unit coefficients. if (sum == k) { for (unsigned i = 0; i < size(); ++i) { - args[i].second = 1; + args[i].second = numeral::one(); } - k = size(); + k = numeral(size()); } // apply cutting plane reduction: - numeral g = 0; - for (unsigned i = 0; g != 1 && i < size(); ++i) { + numeral g(0); + for (unsigned i = 0; !g.is_one() && i < size(); ++i) { numeral c = coeff(i); if (c != k) { - g = gcd(g, c); + if (g.is_zero()) { + g = c; + } + else { + g = gcd(g, c); + } } } - if (g == 0) { + if (g.is_zero()) { // all coefficients are equal to k. for (unsigned i = 0; i < size(); ++i) { SASSERT(coeff(i) == k); - args[i].second = 1; + args[i].second = numeral::one(); } - k = 1; + k = numeral::one(); } - else if (g > 1) { + else if (g > numeral::one()) { // // Example 5x + 5y + 2z + 2u >= 5 // becomes 3x + 3y + z + u >= 3 // - numeral k_new = k / g; - if ((k % g) != 0) { // k_new is the ceiling of k / g. + 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 < size(); ++i) { + SASSERT(coeff(i).is_pos()); numeral c = coeff(i); if (c == k) { c = k_new; } else { - c = c / g; + c = div(c, g); } args[i].second = c; + SASSERT(coeff(i).is_pos()); } k = k_new; } @@ -208,12 +210,12 @@ namespace smt { } bool theory_pb::ineq::well_formed() const { - SASSERT(k() > 0); + SASSERT(k().is_pos()); uint_set vars; - numeral sum = 0; + numeral sum = numeral::zero(); for (unsigned i = 0; i < size(); ++i) { SASSERT(coeff(i) <= k()); - SASSERT(1 <= coeff(i)); + SASSERT(numeral::one() <= coeff(i)); SASSERT(lit(i) != true_literal); SASSERT(lit(i) != false_literal); SASSERT(lit(i) != null_literal); @@ -274,6 +276,9 @@ namespace smt { } k = -k; } + else { + SASSERT(m_util.is_at_least_k(atom) || m_util.is_ge(atom)); + } c->unique(); lbool is_true = c->normalize(); @@ -295,7 +300,7 @@ namespace smt { // maximal coefficient: numeral& max_coeff = c->m_max_coeff; - max_coeff = 0; + max_coeff = numeral::zero(); for (unsigned i = 0; i < args.size(); ++i) { max_coeff = std::max(max_coeff, args[i].second); } @@ -304,7 +309,7 @@ namespace smt { // pre-compile threshold for cardinality bool is_cardinality = true; for (unsigned i = 0; is_cardinality && i < args.size(); ++i) { - is_cardinality = (args[i].second == 1); + is_cardinality = (args[i].second.is_one()); } if (is_cardinality) { unsigned log = 1, n = 1; @@ -472,7 +477,7 @@ namespace smt { if (ctx.get_assignment(c.lit()) == l_undef) { return; } - numeral sum = 0, maxsum = 0; + numeral sum = numeral::zero(), maxsum = numeral::zero(); for (unsigned i = 0; i < c.size(); ++i) { switch(ctx.get_assignment(c.lit(i))) { case l_true: @@ -511,7 +516,7 @@ namespace smt { } literal_vector& theory_pb::get_helpful_literals(ineq& c, bool negate) { - numeral sum = 0; + numeral sum = numeral::zero(); context& ctx = get_context(); literal_vector& lits = get_lits(); for (unsigned i = 0; sum < c.k() && i < c.size(); ++i) { @@ -553,7 +558,7 @@ namespace smt { SASSERT(c.well_formed()); context& ctx = get_context(); - numeral maxsum = 0; + numeral maxsum = numeral::zero(); for (unsigned i = 0; i < c.size(); ++i) { if (ctx.get_assignment(c.lit(i)) != l_false) { maxsum += c.coeff(i); @@ -570,7 +575,7 @@ namespace smt { add_clause(c, ~lits[0], lits); } else { - c.m_max_sum = 0; + c.m_max_sum = numeral::zero(); c.m_watch_sz = 0; for (unsigned i = 0; c.max_sum() < c.k() + c.max_coeff() && i < c.size(); ++i) { if (ctx.get_assignment(c.lit(i)) != l_false) { @@ -822,10 +827,9 @@ namespace smt { context& ctx = get_context(); // only cardinality constraints are compiled. SASSERT(c.m_compilation_threshold < UINT_MAX); - DEBUG_CODE(for (unsigned i = 0; i < c.size(); ++i) SASSERT(c.coeff(i) == 1); ); - unsigned k = static_cast(c.k()); + DEBUG_CODE(for (unsigned i = 0; i < c.size(); ++i) SASSERT(c.coeff(i).is_one()); ); + unsigned k = c.k().get_unsigned(); unsigned num_args = c.size(); - SASSERT(0 <= k && k <= num_args); sort_expr se(*this); sorting_network sn(se); @@ -925,7 +929,7 @@ namespace smt { } for (unsigned i = 0; i < c.size(); ++i) { literal l(c.lit(i)); - if (c.coeff(i) != 1) { + if (!c.coeff(i).is_one()) { out << c.coeff(i) << "*"; } out << l; @@ -941,11 +945,11 @@ namespace smt { } } out << " >= " << c.m_k << "\n"; - if (c.m_num_propagations) out << "propagations: " << c.m_num_propagations << " "; - if (c.max_coeff()) out << "max_coeff: " << c.max_coeff() << " "; - if (c.watch_size()) out << "watch size: " << c.watch_size() << " "; - if (c.max_sum()) out << "max-sum: " << c.max_sum() << " "; - if (c.m_num_propagations || c.max_coeff() || c.watch_size() || c.max_sum()) out << "\n"; + if (c.m_num_propagations) out << "propagations: " << c.m_num_propagations << " "; + if (c.max_coeff().is_pos()) out << "max_coeff: " << c.max_coeff() << " "; + if (c.watch_size()) out << "watch size: " << c.watch_size() << " "; + if (c.max_sum().is_pos()) out << "max-sum: " << c.max_sum() << " "; + if (c.m_num_propagations || c.max_coeff().is_pos() || c.watch_size() || c.max_sum().is_pos()) out << "\n"; return out; } @@ -1077,23 +1081,25 @@ namespace smt { // context& ctx = get_context(); - numeral coeff2 = (conseq==null_literal)?1:0; + numeral coeff2 = (conseq==null_literal)?numeral::one():numeral::zero(); for (unsigned i = 0; i < c.size(); ++i) { if (c.lit(i) == conseq) { coeff2 = c.coeff(i); break; } } - SASSERT(coeff2 > 0); - numeral lc = ineq::lcm(coeff1, coeff2); + SASSERT(coeff2.is_pos()); + numeral lc = lcm(coeff1, coeff2); numeral g = lc/coeff1; - if (g > 1) { + SASSERT(g.is_int()); + if (g > numeral::one()) { for (unsigned i = 0; i < m_lemma.size(); ++i) { m_lemma.m_args[i].second *= g; } m_lemma.m_k *= g; } g = lc/coeff2; + SASSERT(g.is_int()); m_lemma.m_k += g*c.k(); for (unsigned i = 0; i < c.size(); ++i) { @@ -1132,7 +1138,7 @@ namespace smt { m_num_marks = 0; m_lemma.reset(); m_ineq_literals.reset(); - process_ineq(c, null_literal, 1); // add consequent to lemma. + process_ineq(c, null_literal, numeral::one()); // add consequent to lemma. // point into stack of assigned literals literal_vector const& lits = ctx.assigned_literals(); @@ -1241,15 +1247,15 @@ namespace smt { IF_VERBOSE(1, display(verbose_stream() << "lemma: ", m_lemma);); ast_manager& m = get_manager(); - svector coeffs; + svector coeffs; expr_ref_vector args(m); expr_ref tmp(m); for (unsigned i = 0; i < m_lemma.size(); ++i) { ctx.literal2expr(m_lemma.lit(i), tmp); args.push_back(tmp); - coeffs.push_back(static_cast(m_lemma.coeff(i))); + coeffs.push_back(m_lemma.coeff(i)); } - int k = static_cast(m_lemma.k()); + numeral k = m_lemma.k(); tmp = m_util.mk_ge(coeffs.size(), coeffs.c_ptr(), args.c_ptr(), k); internalize_atom(to_app(tmp), false); //m_ineq_literals.push_back(literal(ctx.get_bool_var(tmp))); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index e205f3f59..dd0fd41dc 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -29,8 +29,8 @@ namespace smt { struct sort_expr; class pb_justification; - typedef int64 numeral; - typedef svector > arg_t; + typedef rational numeral; + typedef vector > arg_t; struct stats { unsigned m_num_conflicts; @@ -91,8 +91,8 @@ namespace smt { bool well_formed() const; - static numeral gcd(numeral a, numeral b); - static numeral lcm(numeral a, numeral b); + //static numeral gcd(numeral a, numeral b); + //static numeral lcm(numeral a, numeral b); }; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index dde03f962..5b8e8e107 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -181,7 +181,7 @@ void tactic2solver::set_cancel(bool f) { void tactic2solver::collect_statistics(statistics & st) const { st.copy(m_stats); - SASSERT(m_stats.size() > 0); + //SASSERT(m_stats.size() > 0); } void tactic2solver::get_unsat_core(ptr_vector & r) {