From ec565ae7a0710837b53dd5fcf3841f727fbf7bb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 May 2016 01:00:42 -0700 Subject: [PATCH] fixes to #596 and #592: use exponential step increments on integer problems, align int.to.str with canonizer and disequality checker Signed-off-by: Nikolaj Bjorner --- src/opt/optsmt.cpp | 241 ++++++++++++++++++++++++++++++------ src/opt/optsmt.h | 9 ++ src/smt/theory_arith_aux.h | 2 +- src/smt/theory_seq.cpp | 77 ++++++++++-- src/smt/theory_seq.h | 1 + src/solver/solver_na2as.cpp | 14 ++- 6 files changed, 289 insertions(+), 55 deletions(-) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index e92ab4f97..d2363b36e 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -34,6 +34,7 @@ Notes: #include "arith_decl_plugin.h" #include "theory_arith.h" #include "ast_pp.h" +#include "ast_util.h" #include "model_pp.h" #include "th_rewriter.h" #include "opt_params.hpp" @@ -93,6 +94,158 @@ namespace opt { return l_true; } + /* + Enumerate locally optimal assignments until fixedpoint. + */ + lbool optsmt::geometric_opt() { + lbool is_sat = l_true; + + expr_ref bound(m); + + vector lower(m_lower); + unsigned steps = 0; + unsigned step_incs = 0; + rational delta_per_step(1); + unsigned num_scopes = 0; + unsigned delta_index = 0; // index of objective to speed up. + + while (!m.canceled()) { + SASSERT(delta_per_step.is_int()); + SASSERT(delta_per_step.is_pos()); + is_sat = m_s->check_sat(0, 0); + if (is_sat == l_true) { + bound = update_lower(); + if (!get_max_delta(lower, delta_index)) { + delta_per_step = rational::one(); + } + else if (steps > step_incs) { + delta_per_step *= rational(2); + ++step_incs; + steps = 0; + } + else { + ++steps; + } + if (delta_per_step > rational::one()) { + m_s->push(); + ++num_scopes; + // only try to improve delta_index. + bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step)); + } + TRACE("opt", tout << delta_per_step << " " << bound << "\n";); + m_s->assert_expr(bound); + } + else if (is_sat == l_false && delta_per_step > rational::one()) { + steps = 0; + step_incs = 0; + delta_per_step = rational::one(); + SASSERT(num_scopes > 0); + --num_scopes; + m_s->pop(1); + } + else { + break; + } + } + m_s->pop(num_scopes); + + if (m.canceled() || is_sat == l_undef) { + return l_undef; + } + + // set the solution tight. + for (unsigned i = 0; i < m_lower.size(); ++i) { + m_upper[i] = m_lower[i]; + } + + return l_true; + } + + + lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) { + arith_util arith(m); + bool is_int = arith.is_int(m_objs[obj_index].get()); + lbool is_sat = l_true; + expr_ref bound(m); + + for (unsigned i = 0; i < obj_index; ++i) { + commit_assignment(i); + } + + unsigned steps = 0; + unsigned step_incs = 0; + rational delta_per_step(1); + unsigned num_scopes = 0; + + while (!m.canceled()) { + SASSERT(delta_per_step.is_int()); + SASSERT(delta_per_step.is_pos()); + is_sat = m_s->check_sat(0, 0); + if (is_sat == l_true) { + m_s->maximize_objective(obj_index, bound); + m_s->get_model(m_model); + m_s->get_labels(m_labels); + inf_eps obj = m_s->saved_objective_value(obj_index); + update_lower_lex(obj_index, obj, is_maximize); + if (!is_int || !m_lower[obj_index].is_finite()) { + delta_per_step = rational(1); + } + else if (steps > step_incs) { + delta_per_step *= rational(2); + ++step_incs; + steps = 0; + } + else { + ++steps; + } + if (delta_per_step > rational::one()) { + m_s->push(); + ++num_scopes; + bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step)); + } + TRACE("opt", tout << delta_per_step << " " << bound << "\n";); + m_s->assert_expr(bound); + } + else if (is_sat == l_false && delta_per_step > rational::one()) { + steps = 0; + step_incs = 0; + delta_per_step = rational::one(); + SASSERT(num_scopes > 0); + --num_scopes; + m_s->pop(1); + } + else { + break; + } + } + m_s->pop(num_scopes); + + if (m.canceled() || is_sat == l_undef) { + return l_undef; + } + + // set the solution tight. + m_upper[obj_index] = m_lower[obj_index]; + for (unsigned i = obj_index+1; i < m_lower.size(); ++i) { + m_lower[i] = inf_eps(rational(-1), inf_rational(0)); + } + return l_true; + } + + bool optsmt::get_max_delta(vector const& lower, unsigned& idx) { + arith_util arith(m); + inf_eps max_delta; + for (unsigned i = 0; i < m_lower.size(); ++i) { + if (arith.is_int(m_objs[i].get())) { + inf_eps delta = m_lower[i] - lower[i]; + if (m_lower[i].is_finite() && delta > max_delta) { + max_delta = delta; + } + } + } + return max_delta.is_pos(); + } + /* Enumerate locally optimal assignments until fixedpoint. */ @@ -122,6 +275,7 @@ namespace opt { } lbool optsmt::symba_opt() { + smt::theory_opt& opt = m_s->get_optimizer(); if (typeid(smt::theory_inf_arith) != typeid(opt)) { @@ -138,7 +292,7 @@ namespace opt { } - fml = m.mk_or(ors.size(), ors.c_ptr()); + fml = mk_or(ors); tmp = m.mk_fresh_const("b", m.mk_bool_sort()); fml = m.mk_implies(tmp, fml); vars[0] = tmp; @@ -163,7 +317,7 @@ namespace opt { } } set_max(m_lower, m_s->get_objective_values(), disj); - fml = m.mk_or(ors.size(), ors.c_ptr()); + fml = mk_or(ors); tmp = m.mk_fresh_const("b", m.mk_bool_sort()); fml = m.mk_implies(tmp, fml); vars[0] = tmp; @@ -176,13 +330,30 @@ namespace opt { } } } - bound = m.mk_or(m_lower_fmls.size(), m_lower_fmls.c_ptr()); + bound = mk_or(m_lower_fmls); m_s->assert_expr(bound); if (m.canceled()) { return l_undef; } - return basic_opt(); + return geometric_opt(); + } + + void optsmt::update_lower_lex(unsigned idx, inf_eps const& v, bool is_maximize) { + if (v > m_lower[idx]) { + m_lower[idx] = v; + IF_VERBOSE(1, + if (is_maximize) + verbose_stream() << "(optsmt lower bound: " << v << ")\n"; + else + verbose_stream() << "(optsmt upper bound: " << (-v) << ")\n"; + ); + expr_ref tmp(m); + for (unsigned i = idx+1; i < m_vars.size(); ++i) { + m_s->maximize_objective(i, tmp); + m_lower[i] = m_s->saved_objective_value(i); + } + } } void optsmt::update_lower(unsigned idx, inf_eps const& v) { @@ -196,28 +367,22 @@ namespace opt { m_upper[idx] = v; } + std::ostream& operator<<(std::ostream& out, vector const& vs) { + for (unsigned i = 0; i < vs.size(); ++i) { + out << vs[i] << " "; + } + return out; + } + expr_ref optsmt::update_lower() { expr_ref_vector disj(m); m_s->get_model(m_model); m_s->get_labels(m_labels); m_s->maximize_objectives(disj); set_max(m_lower, m_s->get_objective_values(), disj); - TRACE("opt", - for (unsigned i = 0; i < m_lower.size(); ++i) { - tout << m_lower[i] << " "; - } - tout << "\n"; - model_pp(tout, *m_model); - ); - IF_VERBOSE(2, verbose_stream() << "(optsmt.lower "; - for (unsigned i = 0; i < m_lower.size(); ++i) { - verbose_stream() << m_lower[i] << " "; - } - verbose_stream() << ")\n";); - IF_VERBOSE(3, verbose_stream() << disj << "\n";); - IF_VERBOSE(3, model_pp(verbose_stream(), *m_model);); - - return expr_ref(m.mk_or(disj.size(), disj.c_ptr()), m); + TRACE("opt", model_pp(tout << m_lower << "\n", *m_model);); + IF_VERBOSE(2, verbose_stream() << "(optsmt.lower " << m_lower << ")\n";); + return mk_or(disj); } lbool optsmt::update_upper() { @@ -312,12 +477,21 @@ namespace opt { TRACE("opt", tout << "optsmt:lex\n";); solver::scoped_push _push(*m_s); SASSERT(obj_index < m_vars.size()); - return basic_lex(obj_index, is_maximize); + if (is_maximize && m_optsmt_engine == symbol("farkas")) { + return farkas_opt(); + } + else if (is_maximize && m_optsmt_engine == symbol("symba")) { + return symba_opt(); + } + else { + return geometric_lex(obj_index, is_maximize); + } } + // deprecated lbool optsmt::basic_lex(unsigned obj_index, bool is_maximize) { lbool is_sat = l_true; - expr_ref block(m), tmp(m); + expr_ref bound(m); for (unsigned i = 0; i < obj_index; ++i) { commit_assignment(i); @@ -326,25 +500,13 @@ namespace opt { is_sat = m_s->check_sat(0, 0); if (is_sat != l_true) break; - m_s->maximize_objective(obj_index, block); + m_s->maximize_objective(obj_index, bound); m_s->get_model(m_model); m_s->get_labels(m_labels); inf_eps obj = m_s->saved_objective_value(obj_index); - if (obj > m_lower[obj_index]) { - m_lower[obj_index] = obj; - IF_VERBOSE(1, - if (is_maximize) - verbose_stream() << "(optsmt lower bound: " << obj << ")\n"; - else - verbose_stream() << "(optsmt upper bound: " << (-obj) << ")\n"; - ); - for (unsigned i = obj_index+1; i < m_vars.size(); ++i) { - m_s->maximize_objective(i, tmp); - m_lower[i] = m_s->saved_objective_value(i); - } - } - TRACE("opt", tout << "strengthen bound: " << block << "\n";); - m_s->assert_expr(block); + update_lower_lex(obj_index, obj, is_maximize); + TRACE("opt", tout << "strengthen bound: " << bound << "\n";); + m_s->assert_expr(bound); // TBD: only works for simplex // blocking formula should be extracted based @@ -365,6 +527,7 @@ namespace opt { } + /** Takes solver with hard constraints added. Returns an optimal assignment to objective functions. @@ -383,7 +546,7 @@ namespace opt { is_sat = symba_opt(); } else { - is_sat = basic_opt(); + is_sat = geometric_opt(); } return is_sat; } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index e01c58681..f90bd1c81 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -69,19 +69,28 @@ namespace opt { void reset(); private: + + bool get_max_delta(vector const& lower, unsigned& idx); lbool basic_opt(); + lbool geometric_opt(); + lbool symba_opt(); lbool basic_lex(unsigned idx, bool is_maximize); + lbool geometric_lex(unsigned idx, bool is_maximize); + lbool farkas_opt(); void set_max(vector& dst, vector const& src, expr_ref_vector& fmls); expr_ref update_lower(); + void update_lower_lex(unsigned idx, inf_eps const& r, bool is_maximize); + + lbool update_upper(); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 72004f8b0..b4f887245 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -813,7 +813,7 @@ namespace smt { continue; if (proofs_enabled()) { new_bound.push_lit(l, ante.lit_coeffs()[i]); - } + } else { new_bound.push_lit(l, numeral::zero()); lits.insert(l.index()); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 239ba7420..72d8929b8 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1820,16 +1820,23 @@ bool theory_seq::solve_ne(unsigned idx) { TRACE("seq", display_disequation(tout << "reduces to false: ", n);); return true; } - else if (!change) { - TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";); - if (updated) { - new_ls.push_back(n.ls(i)); - new_rs.push_back(n.rs(i)); - } - continue; - } else { + // eliminate ite expressions. + reduce_ite(lhs, new_lits, num_undef_lits, change); + reduce_ite(rhs, new_lits, num_undef_lits, change); + reduce_ite(ls, new_lits, num_undef_lits, change); + reduce_ite(rs, new_lits, num_undef_lits, change); + + if (!change) { + TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";); + if (updated) { + new_ls.push_back(n.ls(i)); + new_rs.push_back(n.rs(i)); + } + continue; + } + if (!updated) { for (unsigned j = 0; j < i; ++j) { new_ls.push_back(n.ls(j)); @@ -1933,6 +1940,33 @@ bool theory_seq::solve_ne(unsigned idx) { return updated; } +void theory_seq::reduce_ite(expr_ref_vector & ls, literal_vector& new_lits, unsigned& num_undef_lits, bool& change) { + expr* cond, *th, *el; + context& ctx = get_context(); + for (unsigned i = 0; i < ls.size(); ++i) { + expr* e = ls[i].get(); + if (m.is_ite(e, cond, th, el)) { + literal lit(mk_literal(cond)); + switch (ctx.get_assignment(lit)) { + case l_true: + change = true; + new_lits.push_back(lit); + ls[i] = th; + break; + case l_false: + change = true; + new_lits.push_back(~lit); + ls[i] = el; + break; + case l_undef: + ++num_undef_lits; + break; + } + } + } +} + + bool theory_seq::solve_nc(unsigned idx) { nc const& n = m_ncs[idx]; @@ -2212,7 +2246,6 @@ bool theory_seq::add_itos_axiom(expr* e) { if (get_value(n, val)) { if (!m_itos_axioms.contains(val)) { m_itos_axioms.insert(val); - app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); expr_ref n1(arith_util(m).mk_numeral(val, true), m); add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false)); @@ -2604,6 +2637,32 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) { else if (m_util.str.is_index(e, e1, e2, e3)) { result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3); } + else if (m_util.str.is_itos(e, e1)) { + rational val; + if (get_value(e1, val)) { + expr_ref num(m), res(m); + context& ctx = get_context(); + num = m_autil.mk_numeral(val, true); + if (!ctx.e_internalized(num)) { + ctx.internalize(num, false); + } + enode* n1 = ctx.get_enode(num); + enode* n2 = ctx.get_enode(e1); + res = m_util.str.mk_string(symbol(val.to_string().c_str())); + if (n1->get_root() == n2->get_root()) { + result = res; + deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2))); + } + else { + add_axiom(~mk_eq(num, e1, false), mk_eq(e, res, false)); + add_axiom(mk_eq(num, e1, false), ~mk_eq(e, res, false)); + result = e; + } + } + else { + result = e; + } + } else { result = e; } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 4107f3d05..8c4de2111 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -410,6 +410,7 @@ namespace smt { bool solve_nqs(unsigned i); bool solve_ne(unsigned i); bool solve_nc(unsigned i); + void reduce_ite(expr_ref_vector& ls, literal_vector& new_lits, unsigned& num_undef_lits, bool& change); struct cell { cell* m_parent; diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 704038ffd..2ca6e187c 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -71,12 +71,14 @@ void solver_na2as::push() { } void solver_na2as::pop(unsigned n) { - pop_core(n); - unsigned lvl = m_scopes.size(); - SASSERT(n <= lvl); - unsigned new_lvl = lvl - n; - restore_assumptions(m_scopes[new_lvl]); - m_scopes.shrink(new_lvl); + if (n > 0) { + pop_core(n); + unsigned lvl = m_scopes.size(); + SASSERT(n <= lvl); + unsigned new_lvl = lvl - n; + restore_assumptions(m_scopes[new_lvl]); + m_scopes.shrink(new_lvl); + } } void solver_na2as::restore_assumptions(unsigned old_sz) {