From c56c7fd649a41e5b99a1ae150d059d895cd3cf69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 01:31:00 -0700 Subject: [PATCH 1/2] add handlers for dense difference logic Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 27 ++++++++++++++++++++++++++- src/smt/theory_dense_diff_logic_def.h | 2 ++ 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 8ae4e467f..bc6462a18 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -358,6 +358,7 @@ namespace opt { } smt::theory_opt& opt = get_optimizer(); smt::theory_var v = m_objective_vars[var]; + TRACE("opt", tout << "v" << var << " " << val << "\n";); if (typeid(smt::theory_inf_arith) == typeid(opt)) { smt::theory_inf_arith& th = dynamic_cast(opt); @@ -387,8 +388,32 @@ namespace opt { smt::theory_rdl& th = dynamic_cast(opt); return th.mk_ge(m_fm, v, val); } + + if (typeid(smt::theory_dense_i) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_i& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } - // difference logic? + if (typeid(smt::theory_dense_mi) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_mi& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + if (typeid(smt::theory_dense_si) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_si& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + if (typeid(smt::theory_dense_smi) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_smi& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";); return expr_ref(m.mk_true(), m); } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 628eeea83..ed94ee62c 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -1019,6 +1019,7 @@ namespace smt { template theory_var theory_dense_diff_logic::add_objective(app* term) { + TRACE("opt", tout << mk_pp(term, get_manager()) << "\n";); objective_term objective; theory_var result = m_objectives.size(); rational q(1), r(0); @@ -1053,6 +1054,7 @@ namespace smt { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); + TRACE("opt", tout << "mk_ineq " << v << " " << val << "\n";); if (t.size() == 1 && t[0].second.is_one()) { f = get_enode(t[0].first)->get_owner(); } From ec4770622690fc29b2eb0557b7d644651a92b90c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 02:23:50 -0700 Subject: [PATCH 2/2] fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 7 ++++++- src/smt/theory_dense_diff_logic_def.h | 6 ++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index cd40944b2..d1b7a489e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -273,7 +273,8 @@ namespace opt { display_benchmark(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat(0,0); - TRACE("opt", tout << "initial search result: " << is_sat << "\n";); + TRACE("opt", tout << "initial search result: " << is_sat << "\n"; + s.display(tout);); if (is_sat != l_false) { s.get_model(m_model); s.get_labels(m_labels); @@ -1037,6 +1038,10 @@ namespace opt { TRACE("opt", tout << "Purifying " << term << "\n";); term = purify(fm, term); } + else if (m.is_ite(term)) { + TRACE("opt", tout << "Purifying " << term << "\n";); + term = purify(fm, term); + } if (fm) { m_model_converter = concat(m_model_converter.get(), fm.get()); } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index ed94ee62c..addb5d92b 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -868,7 +868,8 @@ namespace smt { e = ctx.get_enode(to_app(n)); } else { - e = ctx.mk_enode(to_app(n), false, false, true); + ctx.internalize(n, false); + e = ctx.get_enode(n); } v = e->get_th_var(get_id()); if (v == null_theory_var) { @@ -1008,7 +1009,8 @@ namespace smt { inf_eps result(rational(0), r); blocker = mk_gt(v, result); IF_VERBOSE(10, verbose_stream() << blocker << "\n";); - return result; + r += m_objective_consts[v]; + return inf_eps(rational(0), r); } default: TRACE("opt", tout << "unbounded\n"; );