diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b52934dfe..be95032b7 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -69,7 +69,7 @@ def init_project_def(): add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('opt', ['smt', 'smtlogic_tactics'], 'opt') API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] - add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'], + add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure','opt'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp new file mode 100644 index 000000000..4f9609840 --- /dev/null +++ b/src/api/api_opt.cpp @@ -0,0 +1,113 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + api_opt.cpp + +Abstract: + API for optimization + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-3. + +Revision History: + +--*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" +#include"api_util.h" +#include"opt_context.h" + +extern "C" { + + struct Z3_optimize_ref : public api::object { + opt::context* m_opt; + Z3_optimize_ref():m_opt(0) {} + virtual ~Z3_optimize_ref() { dealloc(m_opt); } + }; + inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast(o); } + inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast(o); } + + Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) { + return 0; + } + + void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize o) { + + } + + void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) { + + } + + void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a) { + + } + + void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) { + + } + + void Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t) { + + } + + void Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t) { + + } + + Z3_lbool Z3_API Z3_optimize_check(Z3_context c) { + return Z3_L_UNDEF; + } + + void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p) { + + } + + Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o) { + return 0; + } + + + // get lower value or current approximation + Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx) { + return 0; + } + + // get upper or current approximation + Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx) { + return 0; + } + +#if 0 + + /** + \brief version with assumptions. + + */ + + void check_assumptions; + + /** + \brief retrieve the next answer. There are three modes: + + - the optimization context has been configured to produce partial results. + It returns with L_UNDEF and an partial result and caller can retrieve + the results by querying get_lower and get_upper. + - The full result was produced and it returned L_TRUE. + Retrieve the next result that has the same objective optimal. + - The context was configured to compute a Pareto front. + Search proceeds incrementally identifying feasible boxes. + Every return value is a new sub-box or set of sub-boxes. + */ + void Z3_optimize_get_next(Z3_context c, Z3_optimize o) { + } + + // +#endif + +}; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 08e645684..d7fea33d7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -47,6 +47,7 @@ DEFINE_TYPE(Z3_func_interp); #define Z3_func_interp_opt Z3_func_interp DEFINE_TYPE(Z3_func_entry); DEFINE_TYPE(Z3_fixedpoint); +DEFINE_TYPE(Z3_optimize); DEFINE_TYPE(Z3_rcf_num); DEFINE_VOID(Z3_theory_data); #endif