diff --git a/scripts/mk_project.py b/scripts/mk_project.py index bf026c4d5..301282870 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -71,7 +71,7 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') - add_lib('opt', ['smt', 'smtlogic_tactics'], 'opt') + add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure','interp','opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) diff --git a/src/opt/bvsls_opt_solver.cpp b/src/opt/bvsls_opt_solver.cpp new file mode 100644 index 000000000..9bb858856 --- /dev/null +++ b/src/opt/bvsls_opt_solver.cpp @@ -0,0 +1,123 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + bvsls_opt_solver.cpp + +Abstract: + + Uses the bvsls engine for optimization + +Author: + + Christoph (cwinter) 2014-3-28 + +Notes: + +--*/ + +#include "bvsls_opt_solver.h" + +namespace opt { + + bvsls_opt_solver::bvsls_opt_solver(ast_manager & m, params_ref const & p) : + opt_solver(m, p, symbol("QF_BV")), + m_manager(m), + m_params(p), + m_engine(m, p) + { + } + + bvsls_opt_solver::~bvsls_opt_solver() + { + } + + void bvsls_opt_solver::updt_params(params_ref & p) + { + opt_solver::updt_params(p); + m_engine.updt_params(p); + } + + void bvsls_opt_solver::collect_param_descrs(param_descrs & r) + { + opt_solver::collect_param_descrs(r); + } + + void bvsls_opt_solver::collect_statistics(statistics & st) const + { + opt_solver::collect_statistics(st); + } + + void bvsls_opt_solver::assert_expr(expr * t) { + m_engine.assert_expr(t); + } + + void bvsls_opt_solver::push_core() + { + opt_solver::push_core(); + } + + void bvsls_opt_solver::pop_core(unsigned n) + { + opt_solver::pop_core(n); + } + + lbool bvsls_opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) + { + SASSERT(num_assumptions == 0); + SASSERT(assumptions == 0); + return m_engine(); + } + + void bvsls_opt_solver::get_unsat_core(ptr_vector & r) + { + NOT_IMPLEMENTED_YET(); + } + + void bvsls_opt_solver::get_model(model_ref & m) + { + NOT_IMPLEMENTED_YET(); + } + + proof * bvsls_opt_solver::get_proof() + { + NOT_IMPLEMENTED_YET(); + } + + std::string bvsls_opt_solver::reason_unknown() const + { + NOT_IMPLEMENTED_YET(); + } + + void bvsls_opt_solver::get_labels(svector & r) + { + opt_solver::get_labels(r); + } + + void bvsls_opt_solver::set_cancel(bool f) + { + opt_solver::set_cancel(f); + m_engine.set_cancel(f); + } + + void bvsls_opt_solver::set_progress_callback(progress_callback * callback) + { + opt_solver::set_progress_callback(callback); + } + + unsigned bvsls_opt_solver::get_num_assertions() const + { + NOT_IMPLEMENTED_YET(); + } + + expr * bvsls_opt_solver::get_assertion(unsigned idx) const + { + NOT_IMPLEMENTED_YET(); + } + + void bvsls_opt_solver::display(std::ostream & out) const + { + NOT_IMPLEMENTED_YET(); + } +} \ No newline at end of file diff --git a/src/opt/bvsls_opt_solver.h b/src/opt/bvsls_opt_solver.h new file mode 100644 index 000000000..eac1d0403 --- /dev/null +++ b/src/opt/bvsls_opt_solver.h @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + bvsls_opt_solver.h + +Abstract: + + Uses the bvsls engine for optimization + +Author: + + Christoph (cwinter) 2014-3-28 + +Notes: + +--*/ +#ifndef _BVSLS_OPT_SOLVER_H_ +#define _BVSLS_OPT_SOLVER_H_ + +#include "bvsls_opt_engine.h" +#include "opt_solver.h" + +namespace opt { + + class bvsls_opt_solver : public opt_solver { + ast_manager & m_manager; + params_ref const & m_params; + bvsls_opt_engine m_engine; + + public: + bvsls_opt_solver(ast_manager & m, params_ref const & p); + virtual ~bvsls_opt_solver(); + + virtual void updt_params(params_ref & p); + virtual void collect_param_descrs(param_descrs & r); + virtual void collect_statistics(statistics & st) const; + virtual void assert_expr(expr * t); + virtual void push_core(); + virtual void pop_core(unsigned n); + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions); + virtual void get_unsat_core(ptr_vector & r); + virtual void get_model(model_ref & m); + virtual proof * get_proof(); + virtual std::string reason_unknown() const; + virtual void get_labels(svector & r); + virtual void set_cancel(bool f); + virtual void set_progress_callback(progress_callback * callback); + virtual unsigned get_num_assertions() const; + virtual expr * get_assertion(unsigned idx) const; + virtual void display(std::ostream & out) const; + }; + +} + +#endif \ No newline at end of file diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index a176fb3ee..61727fd1e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -33,6 +33,9 @@ Notes: #include "elim_uncnstr_tactic.h" #include "tactical.h" #include "model_smt2_pp.h" +#include "card2bv_tactic.h" +#include "bvsls_opt_solver.h" +#include "nnf_tactic.h" namespace opt { @@ -130,12 +133,13 @@ namespace opt { } lbool context::optimize() { - opt_solver& s = get_solver(); - m_optsmt.reset(); + m_optsmt.reset(); normalize(); internalize(); + opt_solver& s = get_solver(); solver::scoped_push _sp(s); for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { + TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;); s.assert_expr(m_hard_constraints[i].get()); } @@ -359,7 +363,19 @@ namespace opt { mk_simplify_tactic(m)); opt_params optp(m_params); tactic_ref tac2, tac3; - if (optp.elim_01()) { + if (optp.engine() == "bvsls") { + tac2 = mk_elim01_tactic(m); + tac3 = mk_lia2card_tactic(m); + params_ref lia_p; + lia_p.set_bool("compile_equality", optp.pb_compile_equality()); + tac3->updt_params(lia_p); + m_simplify = and_then(tac0.get(), tac2.get(), tac3.get(), + mk_card2bv_tactic(m), + mk_simplify_tactic(m), + mk_nnf_tactic(m)); + m_solver = alloc(bvsls_opt_solver, m, m_params); + } + else if (optp.elim_01()) { tac2 = mk_elim01_tactic(m); tac3 = mk_lia2card_tactic(m); params_ref lia_p; diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 117e2133d..929213472 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -27,6 +27,7 @@ Notes: class card2bv_rewriter { ast_manager& m; + arith_util au; pb_util pb; bv_util bv; @@ -43,51 +44,102 @@ class card2bv_rewriter { public: card2bv_rewriter(ast_manager& m): m(m), + au(m), pb(m), bv(m) {} br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - if (f->get_family_id() != pb.get_family_id()) { + if (f->get_family_id() == null_family_id) { + if (sz == 1) { + // Expecting minimize/maximize. + func_decl_ref fd(m); + fd = m.mk_func_decl(f->get_name(), m.get_sort(args[0]), f->get_range()); + result = m.mk_app(fd.get(), args[0]); + return BR_DONE; + } + else + return BR_FAILED; + } + else if (f->get_family_id() == m.get_basic_family_id()) { + result = m.mk_app(f, sz, args); + return BR_DONE; + } + else if (f->get_family_id() == pb.get_family_id()) { + expr_ref zero(m), a(m), b(m); + expr_ref_vector es(m); + unsigned bw = get_num_bits(f); + zero = bv.mk_numeral(rational(0), bw); + for (unsigned i = 0; i < sz; ++i) { + es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); + } + switch (es.size()) { + case 0: a = zero; break; + case 1: a = es[0].get(); break; + default: + a = es[0].get(); + for (unsigned i = 1; i < es.size(); ++i) { + a = bv.mk_bv_add(a, es[i].get()); + } + break; + } + b = bv.mk_numeral(pb.get_k(f), bw); + + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + UNREACHABLE(); + result = bv.mk_ule(a, b); + return BR_DONE; + case OP_AT_LEAST_K: + UNREACHABLE(); + case OP_PB_GE: + result = bv.mk_ule(b, a); + return BR_DONE; + case OP_PB_EQ: + result = m.mk_eq(a, b); + return BR_DONE; + default: + UNREACHABLE(); + } return BR_FAILED; } - expr_ref zero(m), a(m), b(m); - expr_ref_vector es(m); - unsigned bw = get_num_bits(f); - zero = bv.mk_numeral(rational(0), bw); - for (unsigned i = 0; i < sz; ++i) { - es.push_back(m.mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); - } - switch (es.size()) { - case 0: a = zero; break; - case 1: a = es[0].get(); break; - default: - a = es[0].get(); - for (unsigned i = 1; i < es.size(); ++i) { - a = bv.mk_bv_add(a, es[i].get()); - } - break; - } - b = bv.mk_numeral(pb.get_k(f), bw); + else if (f->get_family_id() == au.get_family_id()) + { + if (f->get_decl_kind() == OP_ADD) { + bool all_ite_01 = true; + unsigned bits = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { + bits += val1.get_num_bits(); + } + else if (m.is_ite(args[i]) && + au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && + au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { + bits++; + } + else + return BR_FAILED; + } - switch(f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - UNREACHABLE(); - result = bv.mk_ule(a, b); - return BR_DONE; - case OP_AT_LEAST_K: - UNREACHABLE(); - case OP_PB_GE: - result = bv.mk_ule(b, a); - return BR_DONE; - case OP_PB_EQ: - result = m.mk_eq(a, b); - return BR_DONE; - default: - UNREACHABLE(); + result = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + expr * q; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) + q = bv.mk_numeral(val1, bits); + else + q = m.mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); + result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); + } + return BR_DONE; + } + else + return BR_FAILED; } - return BR_FAILED; + else + return BR_FAILED; } }; @@ -151,7 +203,7 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - TRACE("pb2bv", g->display(tout);); + TRACE("card2bv-before", g->display(tout);); SASSERT(g->is_well_sorted()); fail_if_proof_generation("card2bv", g); mc = 0; pc = 0; core = 0; result.reset(); @@ -168,6 +220,7 @@ public: expr_ref new_f1(m), new_f2(m); for (unsigned idx = 0; idx < size; idx++) { m_rw1(g->form(idx), new_f1); + TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); m_rw2(new_f1, new_f2); g->update(idx, new_f2); } diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp new file mode 100644 index 000000000..2afdce295 --- /dev/null +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -0,0 +1,69 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + bvsls_opt_engine.cpp + +Abstract: + + Optimization extensions to bvsls + +Author: + + Christoph (cwinter) 2014-03-28 + +Notes: + +--*/ +#include "bvsls_opt_engine.h" + +bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) : + sls_engine(m, p) +{ +} + +bvsls_opt_engine::~bvsls_opt_engine() +{ +} + +bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(expr_ref const & objective) +{ + SASSERT(m_bv_util.is_bv(objective)); + m_tracker.initialize(m_assertions); + m_restart_limit = _RESTART_LIMIT_; + + optimization_result res(m_manager); + + do { + checkpoint(); + + IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl; ); + res.is_sat = search(); + + if (res.is_sat == l_undef) + { +#if _RESTART_INIT_ + m_tracker.randomize(); +#else + m_tracker.reset(m_assertions); +#endif + } + } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && + res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts); + + if (res.is_sat) + res.optimum = maximize(objective); + + return res; +} + +expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) +{ + expr_ref res(m_manager); + res = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(objective)); + + // TODO. + + return res; +} \ No newline at end of file diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h new file mode 100644 index 000000000..326e51df4 --- /dev/null +++ b/src/tactic/sls/bvsls_opt_engine.h @@ -0,0 +1,42 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + bvsls_opt_engine.h + +Abstract: + + Optimization extensions to bvsls + +Author: + + Christoph (cwinter) 2014-03-28 + +Notes: + +--*/ +#ifndef _BVSLS_OPT_ENGINE_H_ +#define _BVSLS_OPT_ENGINE_H_ + +#include "sls_engine.h" + +class bvsls_opt_engine : public sls_engine { +public: + bvsls_opt_engine(ast_manager & m, params_ref const & p); + ~bvsls_opt_engine(); + + class optimization_result { + public: + lbool is_sat; + expr_ref optimum; + optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {} + }; + + optimization_result optimize(expr_ref const & objective); + +protected: + expr_ref maximize(expr_ref const & objective); +}; + +#endif \ No newline at end of file