From 3b3498c4b5935b202f04214ecc7273e14952e927 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Mar 2014 15:39:11 -0700 Subject: [PATCH] initial sls experiment Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 2 + src/opt/fu_malik.cpp | 5 +- src/opt/pb_sls.cpp | 258 +++++++++++++++++++---------- src/opt/pb_sls.h | 3 +- src/opt/weighted_maxsat.cpp | 112 +++++++++++-- src/smt/theory_pb.h | 2 +- src/tactic/arith/elim01_tactic.cpp | 20 ++- 7 files changed, 295 insertions(+), 107 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 5245b9685..3e0278237 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -496,6 +496,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); if (arity == 0 && !is_const_op(k)) { + UNREACHABLE(); m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } @@ -513,6 +514,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); if (num_args == 0 && !is_const_op(k)) { + UNREACHABLE(); m_manager->raise_exception("no arguments supplied to arithmetical operator"); return 0; } diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp index a2d75514a..af6cd6b26 100644 --- a/src/opt/fu_malik.cpp +++ b/src/opt/fu_malik.cpp @@ -54,6 +54,7 @@ namespace opt { unsigned m_upper; unsigned m_lower; model_ref m_model; + unsigned m_num_steps; imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft): m(m), @@ -63,7 +64,8 @@ namespace opt { m_orig_soft(soft), m_aux(m), m_upper(0), - m_lower(0) + m_lower(0), + m_num_steps(0) { m_upper = m_soft.size() + 1; m_assignment.resize(m_soft.size(), false); @@ -100,6 +102,7 @@ namespace opt { if (m_s != &m_opt_solver) { m_s->collect_statistics(st); } + st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper); } void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const { diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index ad1c06b3e..002170924 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -20,6 +20,7 @@ Notes: #include "smt_literal.h" #include "ast_pp.h" #include "uint_set.h" +#include "th_rewriter.h" namespace smt { struct pb_sls::imp { @@ -56,8 +57,11 @@ namespace smt { ast_manager& m; pb_util pb; unsynch_mpz_manager mgr; + th_rewriter m_rewrite; volatile bool m_cancel; vector m_clauses; // clauses to be satisfied + expr_ref_vector m_orig_clauses; // for debugging + model_ref m_orig_model; // for debugging vector m_soft; // soft constraints vector m_weights; // weights of soft constraints rational m_penalty; // current penalty of soft constraints @@ -70,66 +74,88 @@ namespace smt { uint_set m_hard_false; // list of hard clauses that are false. uint_set m_soft_false; // list of soft clauses that are false. unsigned m_max_flips; // maximal number of flips - unsigned m_non_greedy_perc; // percent of moves to do non-greedy style + unsigned m_non_greedy_percent; // percent of moves to do non-greedy style random_gen m_rng; imp(ast_manager& m): m(m), pb(m), - m_cancel(false) + m_rewrite(m), + m_cancel(false), + m_orig_clauses(m) { - m_max_flips = 100; - m_non_greedy_perc = 30; + init_max_flips(); + m_non_greedy_percent = 30; + m_decl2var.insert(m.mk_true()->get_decl(), 0); + m_var2decl.push_back(m.mk_true()->get_decl()); + m_assignment.push_back(true); + m_hard_occ.push_back(unsigned_vector()); + m_soft_occ.push_back(unsigned_vector()); } ~imp() { } - unsigned max_flips() { - return m_max_flips; + void init_max_flips() { + m_max_flips = 200; } void add(expr* f) { clause cls(mgr); if (compile_clause(f, cls)) { m_clauses.push_back(cls); + m_orig_clauses.push_back(f); } } void add(expr* f, rational const& w) { clause cls(mgr); if (compile_clause(f, cls)) { - m_clauses.push_back(cls); + m_soft.push_back(cls); m_weights.push_back(w); } } - void set_model(model const& mdl) { - unsigned sz = mdl.get_num_constants(); + void set_model(model_ref & mdl) { + m_orig_model = mdl; + unsigned sz = mdl->get_num_constants(); for (unsigned i = 0; i < sz; ++i) { - func_decl* f = mdl.get_constant(i); + func_decl* f = mdl->get_constant(i); if (m.is_bool(f->get_range())) { literal lit = mk_literal(f); SASSERT(!lit.sign()); - m_assignment[lit.var()] = m.is_true(mdl.get_const_interp(f)); + m_assignment[lit.var()] = m.is_true(mdl->get_const_interp(f)); } } } lbool operator()() { init(); - for (unsigned i = 0; i < max_flips(); ++i) { - flip(); + IF_VERBOSE(1, verbose_stream() << "(pb.sls initial penalty: " << m_best_penalty << ")\n"; + verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems() + << " penalty: " << m_penalty << ")\n";); + init_max_flips(); + while (m_max_flips > 0) { + --m_max_flips; + literal lit = flip(); if (m_cancel) { return l_undef; } - IF_VERBOSE(3, verbose_stream() + IF_VERBOSE(1, verbose_stream() << "(pb.sls violated: " << m_hard_false.num_elems() - << " penalty: " << m_penalty << ")\n";); - if (m_best_penalty.is_zero()) { + << " penalty: " << m_penalty << " " << lit << ")\n";); + if (m_hard_false.num_elems() == 0 && m_best_penalty.is_zero()) { return l_true; } } - return m_best_assignment.empty()?l_false:l_true; + IF_VERBOSE(1, verbose_stream() << "(pb.sls best penalty " << m_best_penalty << ")\n";); + if (m_best_assignment.empty()) { + return l_false; + } + else { + m_assignment.reset(); + m_assignment.append(m_best_assignment); + return l_true; + } } bool get_value(literal l) { @@ -140,8 +166,8 @@ namespace smt { } void get_model(model_ref& mdl) { mdl = alloc(model, m); - for (unsigned i = 0; i < m_var2decl.size(); ++i) { - mdl->register_decl(m_var2decl[i], m_best_assignment[i]?m.mk_true():m.mk_false()); + for (unsigned i = 1; i < m_var2decl.size(); ++i) { + mdl->register_decl(m_var2decl[i], m_assignment[i]?m.mk_true():m.mk_false()); } } @@ -151,6 +177,40 @@ namespace smt { void updt_params(params_ref& p) { } + bool soft_holds(unsigned index) { + return eval(m_soft[index]); + } + + void display(std::ostream& out, clause const& cls) { + for (unsigned i = 0; i < cls.m_lits.size(); ++i) { + out << cls.m_weights[i] << "*" << cls.m_lits[i] << " "; + if (i + 1 < cls.m_lits.size()) { + out << "+ "; + } + } + out << "(" << cls.m_value << ") "; + if (cls.m_eq) { + out << "= "; + } + else { + out << ">= "; + } + out << cls.m_k << "\n"; + } + + void display(std::ostream& out) { + for (unsigned i = 0; i < m_clauses.size(); ++i) { + display(out, m_clauses[i]); + } + out << "soft:\n"; + for (unsigned i = 0; i < m_soft.size(); ++i) { + display(out << m_weights[i] << ": ", m_soft[i]); + } + for (unsigned i = 0; i < m_assignment.size(); ++i) { + out << literal(i) << ": " << m_var2decl[i]->get_name() << " |-> " << (m_assignment[i]?"true":"false") << "\n"; + } + } + bool eval(clause& cls) { unsigned sz = cls.m_lits.size(); cls.m_value.reset(); @@ -194,6 +254,9 @@ namespace smt { for (unsigned i = 0; i < m_clauses.size(); ++i) { if (!eval(m_clauses[i])) { m_hard_false.insert(i); + expr_ref tmp(m); + VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp)); + std::cout << "original evaluation: " << tmp << "\n"; } } for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -203,44 +266,62 @@ namespace smt { } } m_best_penalty = m_penalty; + TRACE("opt", display(tout);); } - void flip() { + literal flip() { + literal result; if (m_hard_false.empty()) { - flip_soft(); + result = flip_soft(); } else { - flip_hard(); + result = flip_hard(); } + if (m_hard_false.empty() && m_best_penalty > m_penalty) { + IF_VERBOSE(1, verbose_stream() << "(pb.sls improved bound " << m_penalty << ")\n";); + m_best_assignment.reset(); + m_best_assignment.append(m_assignment); + m_best_penalty = m_penalty; + init_max_flips(); + } + if (!m_assignment[result.var()]) { + result.neg(); + } + return result; } - void flip_hard() { + literal flip_hard() { SASSERT(!m_hard_false.empty()); + literal lit; clause const& cls = pick_hard_clause(); + // IF_VERBOSE(1, display(verbose_stream(), cls);); int break_count; int min_bc = INT_MAX; unsigned min_bc_index = 0; for (unsigned i = 0; i < cls.m_lits.size(); ++i) { - literal lit = cls.m_lits[i]; + lit = cls.m_lits[i]; break_count = flip(lit); - if (break_count <= 0) { - return; - } if (break_count < min_bc) { min_bc = break_count; min_bc_index = i; } + else if (break_count == min_bc && m_rng(5) == 1) { + min_bc_index = i; + } VERIFY(-break_count == flip(~lit)); } - if (m_rng(100) <= m_non_greedy_perc) { - flip(cls.m_lits[m_rng(cls.m_lits.size())]); + if (m_rng(100) <= m_non_greedy_percent) { + lit = cls.m_lits[m_rng(cls.m_lits.size())]; } else { - flip(cls.m_lits[min_bc_index]); + lit = cls.m_lits[min_bc_index]; } + flip(lit); + return lit; } - void flip_soft() { + literal flip_soft() { + literal lit; clause const& cls = pick_soft_clause(); int break_count; int min_bc = INT_MAX; @@ -248,18 +329,11 @@ namespace smt { rational penalty = m_penalty; rational min_penalty = penalty; for (unsigned i = 0; i < cls.m_lits.size(); ++i) { - literal lit = cls.m_lits[i]; + lit = cls.m_lits[i]; break_count = flip(lit); SASSERT(break_count >= 0); if (break_count == 0 && penalty > m_penalty) { - if (m_best_penalty > m_penalty) { - IF_VERBOSE(1, verbose_stream() << "(pb.sls improved bound " - << m_penalty << ")\n";); - m_best_assignment.reset(); - m_best_assignment.append(m_assignment); - m_best_penalty = m_penalty; - } - return; + return lit; } if ((break_count < min_bc) || (break_count == min_bc && m_penalty < min_penalty)) { @@ -269,13 +343,15 @@ namespace smt { } VERIFY(-break_count == flip(~lit)); } - if (m_rng(100) <= m_non_greedy_perc) { - flip(cls.m_lits[m_rng(cls.m_lits.size())]); + if (m_rng(100) <= m_non_greedy_percent) { + lit = cls.m_lits[m_rng(cls.m_lits.size())]; } else { // just do a greedy move: - flip(cls.m_lits[min_bc_index]); + lit = cls.m_lits[min_bc_index]; } + flip(lit); + return lit; } // @@ -313,44 +389,47 @@ namespace smt { SASSERT(get_value(l)); m_assignment[l.var()] = !m_assignment[l.var()]; int break_count = 0; - { - unsigned_vector const& occ = m_hard_occ[l.var()]; - for (unsigned i = 0; i < occ.size(); ++i) { - unsigned j = occ[i]; - if (eval(m_clauses[j])) { - if (m_hard_false.contains(j)) { - break_count--; - m_hard_false.remove(j); - } + unsigned_vector const& occh = m_hard_occ[l.var()]; + scoped_mpz value(mgr); + for (unsigned i = 0; i < occh.size(); ++i) { + unsigned j = occh[i]; + value = m_clauses[j].m_value; + if (eval(m_clauses[j])) { + if (m_hard_false.contains(j)) { + break_count--; + m_hard_false.remove(j); } - else { - if (!m_hard_false.contains(j)) { - break_count++; - m_hard_false.insert(j); - } + } + else { + if (!m_hard_false.contains(j)) { + break_count++; + m_hard_false.insert(j); + } + else if (value < m_clauses[j].m_value) { + break_count++; } } } - { - unsigned_vector const& occ = m_soft_occ[l.var()]; - for (unsigned i = 0; i < occ.size(); ++i) { - unsigned j = occ[i]; - if (eval(m_soft[j])) { - if (m_soft_false.contains(j)) { - m_penalty -= m_weights[j]; - m_soft_false.remove(j); - } + unsigned_vector const& occs = m_soft_occ[l.var()]; + for (unsigned i = 0; i < occs.size(); ++i) { + unsigned j = occs[i]; + if (eval(m_soft[j])) { + if (m_soft_false.contains(j)) { + m_penalty -= m_weights[j]; + m_soft_false.remove(j); } - else { - if (!m_soft_false.contains(j)) { - m_penalty += m_weights[j]; - m_soft_false.insert(j); - } + } + else { + if (!m_soft_false.contains(j)) { + m_penalty += m_weights[j]; + m_soft_false.insert(j); } - } - } + } + } SASSERT(get_value(~l)); + TRACE("opt", tout << "flip: " << l << " num false: " << m_hard_false.num_elems() + << " penalty: " << m_penalty << " break count: " << break_count << "\n";); return break_count; } @@ -396,19 +475,28 @@ namespace smt { } bool compile_clause(expr* _f, clause& cls) { - if (!is_app(_f)) return false; - app* f = to_app(_f); + expr_ref tmp(m); + m_rewrite(_f, tmp); + if (!is_app(tmp)) return false; + app* f = to_app(tmp); unsigned sz = f->get_num_args(); expr* const* args = f->get_args(); literal lit; - rational coeff; + rational coeff, k; if (pb.is_ge(f) || pb.is_eq(f)) { + k = pb.get_k(f); + SASSERT(k.is_int()); + cls.m_k = k.to_mpq().numerator(); for (unsigned i = 0; i < sz; ++i) { - coeff = pb.get_coeff(f, i); + coeff = pb.get_coeff(f, i); SASSERT(coeff.is_int()); lit = mk_literal(args[i]); if (lit == null_literal) return false; - SASSERT(lit != false_literal && lit != true_literal); + if (lit == false_literal) continue; + if (lit == true_literal) { + cls.m_k -= coeff.to_mpq().numerator(); + continue; + } cls.m_lits.push_back(lit); cls.m_weights.push_back(coeff.to_mpq().numerator()); if (get_value(lit)) { @@ -416,15 +504,13 @@ namespace smt { } } cls.m_eq = pb.is_eq(f); - coeff = pb.get_k(f); - SASSERT(coeff.is_int()); - cls.m_k = coeff.to_mpq().numerator(); } else if (m.is_or(f)) { for (unsigned i = 0; i < sz; ++i) { lit = mk_literal(args[i]); if (lit == null_literal) return false; - SASSERT(lit != false_literal && lit != true_literal); + if (lit == false_literal) continue; + if (lit == true_literal) return false; cls.m_lits.push_back(lit); cls.m_weights.push_back(mpz(1)); if (get_value(lit)) { @@ -434,6 +520,9 @@ namespace smt { cls.m_eq = false; cls.m_k = mpz(1); } + else if (m.is_true(f)) { + return false; + } else { lit = mk_literal(f); if (lit == null_literal) return false; @@ -460,7 +549,7 @@ namespace smt { void pb_sls::add(expr* f, rational const& w) { m_imp->add(f, w); } - void pb_sls::set_model(model const& mdl) { + void pb_sls::set_model(model_ref& mdl) { m_imp->set_model(mdl); } lbool pb_sls::operator()() { @@ -475,6 +564,9 @@ namespace smt { void pb_sls::get_model(model_ref& mdl) { m_imp->get_model(mdl); } + bool pb_sls::soft_holds(unsigned index) { + return m_imp->soft_holds(index); + } void pb_sls::updt_params(params_ref& p) { m_imp->updt_params(p); } diff --git a/src/opt/pb_sls.h b/src/opt/pb_sls.h index 2d01e9043..a65ed83bf 100644 --- a/src/opt/pb_sls.h +++ b/src/opt/pb_sls.h @@ -35,7 +35,8 @@ namespace smt { ~pb_sls(); void add(expr* f); void add(expr* f, rational const& w); - void set_model(model const& mdl); + bool soft_holds(unsigned index); + void set_model(model_ref& mdl); lbool operator()(); void set_cancel(bool f); void collect_statistics(statistics& st) const; diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 1fdb35256..8e38572c4 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -118,7 +118,7 @@ namespace smt { m_propagate = true; } - void assert_weighted(expr* fml, rational const& w) { + bool_var assert_weighted(expr* fml, rational const& w) { context & ctx = get_context(); ast_manager& m = get_manager(); app_ref var(m), wfml(m); @@ -132,7 +132,7 @@ namespace smt { m_assigned.push_back(false); m_rmin_cost += w; m_normalize = true; - register_var(var, true); + return register_var(var, true); } bool_var register_var(app* var, bool attach) { @@ -341,6 +341,25 @@ namespace smt { return result; } + expr_ref mk_optimal_block(svector const& ws, rational const& weight) { + ast_manager& m = get_manager(); + expr_ref_vector disj(m); + rational new_w = weight*m_den; + m_zmin_cost = new_w.to_mpq().numerator(); + m_cost_save.reset(); + for (unsigned i = 0; i < ws.size(); ++i) { + bool_var bv = ws[i]; + theory_var v = m_bool2var[bv]; + m_cost_save.push_back(v); + disj.push_back(m.mk_not(m_vars[v].get())); + } + if (m_min_cost_atom) { + disj.push_back(m.mk_not(m_min_cost_atom)); + } + expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m); + return result; + } + private: @@ -493,6 +512,9 @@ namespace opt { if (m_engine == symbol("wpm2b")) { return wpm2b_solve(); } + if (m_engine == symbol("sls")) { + return sls_solve(); + } return incremental_solve(); } @@ -522,10 +544,6 @@ namespace opt { lbool incremental_solve() { IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";); - smt::pb_sls sls(m); - for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - sls.add(s.get_assertion(i)); - } TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); solver::scoped_push _s(s); @@ -533,8 +551,9 @@ namespace opt { bool was_sat = false; for (unsigned i = 0; i < m_soft.size(); ++i) { wth().assert_weighted(m_soft[i].get(), m_weights[i]); - sls.add(m_soft[i].get(), m_weights[i]); } + s.display(std::cout); + solver::scoped_push __s(s); while (l_true == is_sat) { is_sat = s.check_sat_core(0,0); @@ -545,15 +564,6 @@ namespace opt { if (wth().is_optimal()) { m_upper = wth().get_min_cost(); updt_model(s); - s.display(std::cout); - model_ref mdl; - s.get_model(mdl); - model_smt2_pp(std::cout, m, *(mdl.get()), 0); - - sls.set_model(*(mdl.get())); - lbool found = sls(); - std::cout << found << "\n"; - } expr_ref fml = wth().mk_block(); s.assert_expr(fml); @@ -575,6 +585,76 @@ namespace opt { return is_sat; } + lbool sls_solve() { + IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";); + smt::pb_sls sls(m); + svector ws; + for (unsigned i = 0; i < s.get_num_assertions(); ++i) { + sls.add(s.get_assertion(i)); + } + TRACE("opt", tout << "weighted maxsat\n";); + scoped_ensure_theory wth(*this); + solver::scoped_push _s(s); + lbool is_sat = l_true; + bool was_sat = false; + for (unsigned i = 0; i < m_soft.size(); ++i) { + ws.push_back(wth().assert_weighted(m_soft[i].get(), m_weights[i])); + sls.add(m_soft[i].get(), m_weights[i]); + } + s.display(std::cout); + + expr_ref fml(m); + solver::scoped_push __s(s); + while (l_true == is_sat) { + is_sat = s.check_sat_core(0,0); + if (m_cancel) { + is_sat = l_undef; + } + if (is_sat == l_true) { + if (wth().is_optimal()) { + m_upper = wth().get_min_cost(); + updt_model(s); + sls.set_model(m_model); + if (l_true == sls()) { + sls.get_model(m_model); + svector wsf; + rational weight(0); + for (unsigned i = 0; i < ws.size(); ++i) { + if (!sls.soft_holds(i)) { + wsf.push_back(ws[i]); + weight += m_weights[i]; + } + } + fml = wth().mk_optimal_block(wsf, weight); + m_upper = weight; + s.assert_expr(fml); + } + else { + fml = wth().mk_block(); + } + } + else { + fml = wth().mk_block(); + } + s.assert_expr(fml); + was_sat = true; + } + IF_VERBOSE(3, verbose_stream() << "(incremental bound)\n";); + } + if (was_sat) { + wth().get_assignment(m_assignment); + } + if (is_sat == l_false && was_sat) { + is_sat = l_true; + } + m_upper = wth().get_min_cost(); + if (is_sat == l_true) { + m_lower = m_upper; + } + TRACE("opt", tout << "min cost: " << m_upper << "\n";); + return is_sat; + } + /** Iteratively increase cost until there is an assignment during final_check that satisfies min_cost. diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 5aea94999..46c68900a 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -121,7 +121,7 @@ namespace smt { unsigned m_num_propagations; unsigned m_compilation_threshold; lbool m_compiled; - + ineq(unsynch_mpz_manager& m, literal l, bool is_eq) : m_mpz(m), m_lit(l), m_is_eq(is_eq), m_max_watch(m), m_watch_sum(m), diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp index e6c345734..ad6e2c3b0 100644 --- a/src/tactic/arith/elim01_tactic.cpp +++ b/src/tactic/arith/elim01_tactic.cpp @@ -24,6 +24,7 @@ Notes: #include"arith_decl_plugin.h" #include"elim01_tactic.h" #include"model_smt2_pp.h" +#include"th_rewriter.h" class bool2int_model_converter : public model_converter { ast_manager& m; @@ -120,6 +121,7 @@ public: typedef obj_hashtable expr_set; ast_manager & m; arith_util a; + th_rewriter m_rewriter; params_ref m_params; unsigned m_max_hi_default; rational m_max_hi; @@ -127,6 +129,7 @@ public: elim01_tactic(ast_manager & _m, params_ref const & p): m(_m), a(m), + m_rewriter(m), m_max_hi_default(8), m_max_hi(rational(m_max_hi_default)) { } @@ -177,12 +180,13 @@ public: } } - expr_ref new_curr(m); + expr_ref new_curr(m), tmp_curr(m); proof_ref new_pr(m); for (unsigned i = 0; i < g->size(); i++) { expr * curr = g->form(i); - sub(curr, new_curr); + sub(curr, tmp_curr); + m_rewriter(tmp_curr, new_curr); g->update(i, new_curr, new_pr, g->dep(i)); } for (unsigned i = 0; i < axioms.size(); ++i) { @@ -219,12 +223,18 @@ public: ites.push_back(m.mk_ite(xs.back(), a.mk_numeral(rational(1 << sh), true), zero)); ++sh; } - if (ites.size() == 1) { + switch (ites.size()) { + case 0: + sum = zero; + break; + case 1: sum = ites[0].get(); - } - else { + break; + default: sum = a.mk_add(ites.size(), (expr*const*)ites.c_ptr()); + break; } + TRACE("pb", tout << mk_pp(x, m) << " " << sum << " max: " << max_value << "\n";); sub.insert(x, sum); b2i->insert(x->get_decl(), xfs.size(), xfs.c_ptr());