add sketch of C-based API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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)

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<iostream>
+#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<Z3_optimize_ref *>(o); }
+    inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast<Z3_optimize>(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
+
+};

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