From 8c85ee6b7c83eded4b9f1f46975473d827dca9ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Dec 2013 23:36:42 +0100 Subject: [PATCH] fixing lex optimization Signed-off-by: Nikolaj Bjorner --- src/opt/opt_cmds.cpp | 2 +- src/opt/opt_context.cpp | 107 ++++++++++++++++++++--------- src/opt/opt_context.h | 8 ++- src/opt/opt_solver.cpp | 50 +++++++------- src/opt/opt_solver.h | 15 ++--- src/opt/optsmt.cpp | 130 +++++++++++++++++++++--------------- src/opt/optsmt.h | 8 ++- src/smt/smt_context.cpp | 5 ++ src/smt/smt_context.h | 2 + src/smt/theory_arith.h | 2 +- src/smt/theory_arith_aux.h | 8 ++- src/smt/theory_opt.h | 3 +- src/util/inf_eps_rational.h | 4 ++ 13 files changed, 219 insertions(+), 125 deletions(-) diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 5347fa1b2..88cfd20dd 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -314,7 +314,7 @@ public: break; case l_undef: ctx.regular_stream() << "unknown\n"; - opt.display_range_assignment(ctx.regular_stream()); + opt.display_assignment(ctx.regular_stream()); break; } if (p.get_bool("print_statistics", false)) { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6df46e783..8a70683fb 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -28,6 +28,7 @@ Notes: #include "lia2card_tactic.h" #include "elim01_tactic.h" #include "tactical.h" +#include "model_smt2_pp.h" namespace opt { @@ -85,12 +86,13 @@ namespace opt { return is_sat; } s.get_model(m_model); + m_optsmt.setup(s); update_lower(); switch (m_objectives.size()) { case 0: return is_sat; case 1: - return execute(m_objectives[0], false); + return execute(m_objectives[0], true); default: { opt_params optp(m_params); symbol pri = optp.priority(); @@ -111,19 +113,17 @@ namespace opt { mdl = m_model; if (m_model_converter) { (*m_model_converter)(mdl, 0); + get_solver().mc()(mdl, 0); } } - lbool context::execute_min_max(unsigned index, bool committed, bool is_max) { - // HACK: reuse m_optsmt without regard for box reuse and not considering - // use-case of lex. - lbool result = m_optsmt(get_solver()); + lbool context::execute_min_max(unsigned index, bool committed) { + lbool result = m_optsmt.lex(index); if (result == l_true) m_optsmt.get_model(m_model); if (committed) m_optsmt.commit_assignment(index); return result; } - lbool context::execute_maxsat(symbol const& id, bool committed) { maxsmt& ms = *m_maxsmts.find(id); lbool result = ms(get_solver()); @@ -134,8 +134,8 @@ namespace opt { lbool context::execute(objective const& obj, bool committed) { switch(obj.m_type) { - case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, true); - case O_MINIMIZE: return execute_min_max(obj.m_index, committed, false); + case O_MAXIMIZE: return execute_min_max(obj.m_index, committed); + case O_MINIMIZE: return execute_min_max(obj.m_index, committed); case O_MAXSMT: return execute_maxsat(obj.m_id, committed); default: UNREACHABLE(); return l_undef; } @@ -145,16 +145,23 @@ namespace opt { lbool r = l_true; for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { r = execute(m_objectives[i], i + 1 < m_objectives.size()); + if (r == l_true && !get_lower_as_num(i).is_finite()) { + return r; + } } + DEBUG_CODE(if (r == l_true) validate_lex();); return r; } lbool context::execute_box() { - lbool r = l_true; + lbool r = m_optsmt.box(); for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { - get_solver().push(); - r = execute(m_objectives[i], false); - get_solver().pop(1); + objective const& obj = m_objectives[i]; + if (obj.m_type == O_MAXSMT) { + get_solver().push(); + r = execute(obj, false); + get_solver().pop(1); + } } return r; } @@ -244,7 +251,9 @@ namespace opt { terms[i] = m.mk_not(terms[i].get()); } } - id = symbol(index); + std::ostringstream out; + out << term; + id = symbol(out.str().c_str()); return true; } if (is_maximize(fml, term, index) && @@ -266,7 +275,9 @@ namespace opt { offset += weights[i]; } neg = true; - id = symbol(index); + std::ostringstream out; + out << term; + id = symbol(out.str().c_str()); return true; } return false; @@ -426,17 +437,15 @@ namespace opt { for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; display_objective(out, obj); - out << "|-> " << get_upper(i) << "\n"; + if (get_lower_as_num(i) != get_upper_as_num(i)) { + out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n"; + } + else { + out << "|-> " << get_lower(i) << "\n"; + } } } - void context::display_range_assignment(std::ostream& out) { - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; - display_objective(out, obj); - out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n"; - } - } void context::display_objective(std::ostream& out, objective const& obj) const { switch(obj.m_type) { @@ -453,8 +462,7 @@ namespace opt { } } - - expr_ref context::get_lower(unsigned idx) { + inf_eps context::get_lower_as_num(unsigned idx) { if (idx > m_objectives.size()) { throw default_exception("index out of bounds"); } @@ -464,18 +472,19 @@ namespace opt { rational r = m_maxsmts.find(obj.m_id)->get_lower(); if (obj.m_neg) r.neg(); r += obj.m_offset; - return to_expr(inf_eps(r)); + return inf_eps(r); } case O_MINIMIZE: case O_MAXIMIZE: - return to_expr(m_optsmt.get_lower(obj.m_index)); + return m_optsmt.get_lower(obj.m_index); default: UNREACHABLE(); - return expr_ref(m); - } + return inf_eps(); + } } - expr_ref context::get_upper(unsigned idx) { + + inf_eps context::get_upper_as_num(unsigned idx) { if (idx > m_objectives.size()) { throw default_exception("index out of bounds"); } @@ -485,17 +494,25 @@ namespace opt { rational r = m_maxsmts.find(obj.m_id)->get_upper(); if (obj.m_neg) r.neg(); r += obj.m_offset; - return to_expr(inf_eps(r)); + return inf_eps(r); } case O_MINIMIZE: case O_MAXIMIZE: - return to_expr(m_optsmt.get_upper(obj.m_index)); + return m_optsmt.get_upper(obj.m_index); default: UNREACHABLE(); - return expr_ref(m); + return inf_eps(); } } + expr_ref context::get_lower(unsigned idx) { + return to_expr(get_lower_as_num(idx)); + } + + expr_ref context::get_upper(unsigned idx) { + return to_expr(get_upper_as_num(idx)); + } + expr_ref context::to_expr(inf_eps const& n) { rational inf = n.get_infinity(); rational r = n.get_rational(); @@ -676,4 +693,30 @@ namespace opt { return out.str(); } + void context::validate_lex() { + arith_util a(m); + rational r1; + expr_ref val(m); + for (unsigned i = 0; i < m_objectives.size(); ++i) { + objective const& obj = m_objectives[i]; + switch(obj.m_type) { + case O_MINIMIZE: + case O_MAXIMIZE: { + inf_eps n = m_optsmt.get_lower(obj.m_index); + if (n.get_infinity().is_zero() && + n.get_infinitesimal().is_zero() && + m_model->eval(obj.m_term, val) && + a.is_numeral(val, r1)) { + rational r2 = n.get_rational(); + CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";); + CTRACE("opt", r1 != r2, model_smt2_pp(tout, m, *m_model, 0);); + SASSERT(r1 == r2); + } + break; + } + case O_MAXSMT: + break; + } + } + } } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index bc13795eb..50f69d59e 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -115,7 +115,7 @@ namespace opt { void validate_feasibility(maxsmt& ms); lbool execute(objective const& obj, bool committed); - lbool execute_min_max(unsigned index, bool committed, bool is_max); + lbool execute_min_max(unsigned index, bool committed); lbool execute_maxsat(symbol const& s, bool committed); lbool execute_lex(); lbool execute_box(); @@ -139,10 +139,16 @@ namespace opt { void update_lower(); + inf_eps get_lower_as_num(unsigned idx); + inf_eps get_upper_as_num(unsigned idx); + + opt_solver& get_solver(); void display_objective(std::ostream& out, objective const& obj) const; + void validate_lex(); + }; } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 01d64b6cc..8ed4c863d 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -34,9 +34,9 @@ namespace opt { m_params(p), m_context(mgr, m_params), m(mgr), - m_objective_enabled(false), m_dump_benchmarks(false), - m_dump_count(0) { + m_dump_count(0), + m_fm(m) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); @@ -71,7 +71,6 @@ namespace opt { m_context.pop(n); } - smt::theory_opt& opt_solver::get_optimizer() { smt::context& ctx = m_context.get_context(); smt::theory_id arith_id = m_context.m().get_family_id("arith"); @@ -118,21 +117,26 @@ namespace opt { to_smt2_benchmark(buffer, "opt_solver", "QF_BV"); buffer.close(); } - if (r == l_true && m_objective_enabled) { - m_objective_values.reset(); - smt::theory_opt& opt = get_optimizer(); - for (unsigned i = 0; i < m_objective_vars.size(); ++i) { - smt::theory_var v = m_objective_vars[i]; - m_objective_values.push_back(opt.maximize(v)); - } - } return r; } + + void opt_solver::maximize_objectives() { + for (unsigned i = 0; i < m_objective_vars.size(); ++i) { + maximize_objective(i); + } + } + + void opt_solver::maximize_objective(unsigned i) { + smt::theory_var v = m_objective_vars[i]; + m_objective_values[i] = get_optimizer().maximize(v); + m_context.get_context().update_model(); + } void opt_solver::get_unsat_core(ptr_vector & r) { unsigned sz = m_context.get_unsat_core_size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) { r.push_back(m_context.get_unsat_core_expr(i)); + } } void opt_solver::get_model(model_ref & m) { @@ -177,6 +181,7 @@ namespace opt { smt::theory_var opt_solver::add_objective(app* term) { m_objective_vars.push_back(get_optimizer().add_objective(term)); + m_objective_values.push_back(inf_eps(rational(-1), inf_rational())); return m_objective_vars.back(); } @@ -184,26 +189,30 @@ namespace opt { return m_objective_values; } + inf_eps const& opt_solver::get_objective_value(unsigned i) { + return m_objective_values[i]; + } + expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) { smt::theory_opt& opt = get_optimizer(); smt::theory_var v = m_objective_vars[var]; if (typeid(smt::theory_inf_arith) == typeid(opt)) { smt::theory_inf_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(v, val), m); + return expr_ref(th.mk_ge(m_fm, v, val), m); } if (typeid(smt::theory_mi_arith) == typeid(opt)) { smt::theory_mi_arith& th = dynamic_cast(opt); - SASSERT(val.get_infinity().is_zero()); - return expr_ref(th.mk_ge(v, val.get_numeral()), m); + SASSERT(val.is_finite()); + return expr_ref(th.mk_ge(m_fm, v, val.get_numeral()), m); } if (typeid(smt::theory_i_arith) == typeid(opt)) { - SASSERT(val.get_infinity().is_zero()); + SASSERT(val.is_finite()); SASSERT(val.get_infinitesimal().is_zero()); smt::theory_i_arith& th = dynamic_cast(opt); - return expr_ref(th.mk_ge(v, val.get_rational()), m); + return expr_ref(th.mk_ge(m_fm, v, val.get_rational()), m); } // difference logic? @@ -251,12 +260,5 @@ namespace opt { pp.display_smt2(buffer, to_expr(m.mk_true())); } - opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) { - s.m_objective_enabled = new_value; - } - - opt_solver::toggle_objective::~toggle_objective() { - s.m_objective_enabled = m_old_value; - } } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index d5fb58afe..844e276ba 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -30,6 +30,7 @@ Notes: #include"smt_params.h" #include"smt_types.h" #include"theory_opt.h" +#include"filter_model_converter.h" namespace opt { @@ -49,6 +50,7 @@ namespace opt { bool m_dump_benchmarks; unsigned m_dump_count; statistics m_stats; + filter_model_converter m_fm; public: opt_solver(ast_manager & m, params_ref const & p, symbol const & l); virtual ~opt_solver(); @@ -73,22 +75,19 @@ namespace opt { smt::theory_var add_objective(app* term); void reset_objectives(); + void maximize_objective(unsigned i); + void maximize_objectives(); vector const& get_objective_values(); + inf_eps const & get_objective_value(unsigned obj_index); expr_ref mk_gt(unsigned obj_index, inf_eps const& val); expr_ref mk_ge(unsigned obj_index, inf_eps const& val); + model_converter& mc() { return m_fm; } + static opt_solver& to_opt(solver& s); bool dump_benchmarks(); - class toggle_objective { - opt_solver& s; - bool m_old_value; - public: - toggle_objective(opt_solver& s, bool new_value); - ~toggle_objective(); - }; - smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat. smt::theory_opt& get_optimizer(); diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index d870d5675..3f8f1c939 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -66,7 +66,6 @@ namespace opt { Enumerate locally optimal assignments until fixedpoint. */ lbool optsmt::basic_opt() { - opt_solver::toggle_objective _t(*m_s, true); lbool is_sat = l_true; while (is_sat == l_true && !m_cancel) { @@ -98,8 +97,7 @@ namespace opt { return l_undef; } - opt_solver::toggle_objective _t(*m_s, true); - lbool is_sat= l_true; + lbool is_sat = l_true; while (is_sat == l_true && !m_cancel) { is_sat = update_upper(); @@ -126,6 +124,7 @@ namespace opt { } void optsmt::update_lower() { + m_s->maximize_objectives(); m_s->get_model(m_model); set_max(m_lower, m_s->get_objective_values()); IF_VERBOSE(1, @@ -150,7 +149,6 @@ namespace opt { smt::theory_opt& opt = m_s->get_optimizer(); SASSERT(typeid(smt::theory_inf_arith) == typeid(opt)); smt::theory_inf_arith& th = dynamic_cast(opt); - expr_ref bound(m); expr_ref_vector bounds(m); @@ -165,10 +163,9 @@ namespace opt { for (unsigned i = 0; i < m_lower.size() && !m_cancel; ++i) { if (m_lower[i] < m_upper[i]) { - smt::theory_var v = m_vars[i]; mid.push_back((m_upper[i]+m_lower[i])/rational(2)); //mid.push_back(m_upper[i]); - bound = th.mk_ge(v, mid[i]); + bound = m_s->mk_ge(i, mid[i]); bounds.push_back(bound); } else { @@ -190,7 +187,7 @@ namespace opt { break; case l_false: IF_VERBOSE(2, verbose_stream() << "conflict: " << th.conflict_minimize() << "\n";); - if (!th.conflict_minimize().get_infinity().is_zero()) { + if (!th.conflict_minimize().is_finite()) { // bounds is not in the core. The context is unsat. m_upper[i] = m_lower[i]; return l_false; @@ -216,28 +213,76 @@ namespace opt { return l_true; } - /** - Takes solver with hard constraints added. - Returns an optimal assignment to objective functions. - */ - lbool optsmt::operator()(opt_solver& solver) { - if (m_objs.empty()) { - return l_true; - } - lbool is_sat = l_true; + void optsmt::setup(opt_solver& solver) { m_s = &solver; solver.reset_objectives(); m_vars.reset(); + // force base level { - // force base level solver::scoped_push _push(solver); } for (unsigned i = 0; i < m_objs.size(); ++i) { m_vars.push_back(solver.add_objective(m_objs[i].get())); } + } + lbool optsmt::lex(unsigned obj_index) { + solver::scoped_push _push(*m_s); + SASSERT(obj_index < m_vars.size()); + return basic_lex(obj_index); + } + + lbool optsmt::basic_lex(unsigned obj_index) { + lbool is_sat = l_true; + expr_ref block(m); + + while (is_sat == l_true && !m_cancel) { + is_sat = m_s->check_sat(0, 0); + if (is_sat != l_true) break; + + m_s->maximize_objective(obj_index); + m_s->get_model(m_model); + inf_eps obj = m_s->get_objective_value(obj_index); + if (obj > m_lower[obj_index]) { + m_lower[obj_index] = obj; + for (unsigned i = obj_index+1; i < m_vars.size(); ++i) { + m_s->maximize_objective(i); + m_lower[i] = m_s->get_objective_value(i); + } + } + block = m_s->mk_gt(obj_index, obj); + m_s->assert_expr(block); + + // TBD: only works for simplex + // blocking formula should be extracted based + // on current state. + } + + if (m_cancel || 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; + } + + /** + Takes solver with hard constraints added. + Returns an optimal assignment to objective functions. + */ + lbool optsmt::box() { + lbool is_sat = l_true; + if (m_vars.empty()) { + return is_sat; + } + // assertions added during search are temporary. + solver::scoped_push _push(*m_s); if (m_engine == symbol("farkas")) { is_sat = farkas_opt(); } @@ -252,15 +297,15 @@ namespace opt { } inf_eps optsmt::get_value(unsigned i) const { - return m_is_max[i]?m_lower[i]:-m_lower[i]; + return get_lower(i); } inf_eps optsmt::get_lower(unsigned i) const { - return m_is_max[i]?m_lower[i]:-m_upper[i]; + return m_is_max[i]?m_lower[i]:-m_lower[i]; } inf_eps optsmt::get_upper(unsigned i) const { - return m_is_max[i]?m_upper[i]:-m_lower[i]; + return m_is_max[i]?m_upper[i]:-m_upper[i]; } void optsmt::get_model(model_ref& mdl) { @@ -269,33 +314,13 @@ namespace opt { // force lower_bound(i) <= objective_value(i) void optsmt::commit_assignment(unsigned i) { - inf_eps mid(0); - - // TBD: case analysis should be revisited - rational hi = get_upper(i).get_infinity(); - rational lo = get_lower(i).get_infinity(); - if (hi.is_pos() && !lo.is_neg()) { - mid = get_lower(i); - } - else if (hi.is_pos() && lo.is_neg()) { - mid = inf_eps(0); - } - else if (hi.is_pos() && lo.is_pos()) { - mid = inf_eps(0); // TBD: get a value from a model? - } - else if (hi.is_neg() && lo.is_neg()) { - mid = inf_eps(0); // TBD: get a value from a model? - } - else { - mid = hi; - } - m_lower[i] = mid; - m_upper[i] = mid; - TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << mid << "\n"; + inf_eps lo = m_lower[i]; + TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << lo << "\n"; tout << get_lower(i) << ":" << get_upper(i) << "\n";); // Only assert bounds for bounded objectives - if (mid.get_infinity().is_zero()) - m_s->assert_expr(m_s->mk_ge(i, mid)); + if (lo.is_finite()) { + m_s->assert_expr(m_s->mk_ge(i, lo)); + } } std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const { @@ -314,14 +339,13 @@ namespace opt { void optsmt::display_assignment(std::ostream& out) const { unsigned sz = m_objs.size(); for (unsigned i = 0; i < sz; ++i) { - display_objective(out, i) << " |-> " << get_value(i) << std::endl; - } - } - - void optsmt::display_range_assignment(std::ostream& out) const { - unsigned sz = m_objs.size(); - for (unsigned i = 0; i < sz; ++i) { - display_objective(out, i) << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]" << std::endl; + if (get_lower(i) != get_upper(i)) { + display_objective(out, i) << " |-> [" << get_lower(i) + << ":" << get_upper(i) << "]" << std::endl; + } + else { + display_objective(out, i) << " |-> " << get_value(i) << std::endl; + } } } diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h index 9571817f6..c61599bb2 100644 --- a/src/opt/optsmt.h +++ b/src/opt/optsmt.h @@ -41,7 +41,11 @@ namespace opt { public: optsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_objs(m) {} - lbool operator()(opt_solver& solver); + void setup(opt_solver& solver); + + lbool box(); + + lbool lex(unsigned obj_index); void add(app* t, bool is_max); @@ -67,6 +71,8 @@ namespace opt { lbool basic_opt(); + lbool basic_lex(unsigned idx); + lbool farkas_opt(); void set_max(vector& dst, vector const& src); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 02ee06985..9599eaacb 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3937,6 +3937,11 @@ namespace smt { return th->get_value(n, value); } + void context::update_model() { + mk_proto_model(l_true); + m_model = m_proto_model->mk_model(); + } + void context::mk_proto_model(lbool r) { TRACE("get_model", display(tout); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index aed164570..42af9738b 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1390,6 +1390,8 @@ namespace smt { void get_model(model_ref & m) const; + void update_model(); + void get_proto_model(proto_model_ref & m) const; unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index f0211ca9d..8bc841ca0 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -1000,7 +1000,7 @@ namespace smt { virtual inf_eps_rational maximize(theory_var v); virtual theory_var add_objective(app* term); virtual expr* mk_gt(theory_var v, inf_rational const& val); - virtual expr* mk_ge(theory_var v, inf_numeral const& val); + virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val); void enable_record_conflict(expr* bound); void record_conflict(unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs, diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 26fb655a9..f9f98b867 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -23,6 +23,7 @@ Revision History: #include"theory_arith.h" #include"smt_farkas_util.h" #include"th_rewriter.h" +#include"filter_model_converter.h" namespace smt { @@ -1085,14 +1086,15 @@ namespace smt { This allows to handle inequalities with non-standard numbers. */ template - expr* theory_arith::mk_ge(theory_var v, inf_numeral const& val) { + expr* theory_arith::mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val) { SASSERT(m_objective_theory_vars.contains(v)); ast_manager& m = get_manager(); context& ctx = get_context(); std::ostringstream strm; - strm << val << " <= v" << v; - expr* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); + strm << val << " <= " << mk_pp(get_enode(v)->get_owner(), get_manager()); + app* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); if (!ctx.b_internalized(b)) { + fm.insert(b->get_decl()); bool_var bv = ctx.mk_bool_var(b); ctx.set_var_theory(bv, get_id()); // ctx.set_enode_flag(bv, true); diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index 208330bfb..2d4d33e20 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -24,6 +24,7 @@ Notes: #ifndef _THEORY_OPT_H_ #define _THEORY_OPT_H_ +class filter_model_converter; namespace smt { class theory_opt { public: @@ -31,7 +32,7 @@ namespace smt { virtual inf_eps maximize(theory_var v) { UNREACHABLE(); return inf_eps::infinity(); } virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } virtual expr* mk_gt(theory_var v, inf_rational const& val) { UNREACHABLE(); return 0; } - virtual expr* mk_ge(theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; } + virtual expr* mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return 0; } }; } diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h index 9f40404ba..698075e01 100644 --- a/src/util/inf_eps_rational.h +++ b/src/util/inf_eps_rational.h @@ -143,6 +143,10 @@ class inf_eps_rational { return m_infty; } + bool is_finite() const { + return m_infty.is_zero(); + } + static inf_eps_rational zero() { return inf_eps_rational(Numeral::zero()); }