1 files changed, 349 insertions, 0 deletions
diff --git a/tool_bin/lib/linux/z3/include/z3_optimization.h b/tool_bin/lib/linux/z3/include/z3_optimization.h
new file mode 100644
index 0000000..a8ffd45
--- /dev/null
+++ b/tool_bin/lib/linux/z3/include/z3_optimization.h
@@ -0,0 +1,349 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    z3_optimization.h
+
+Abstract:
+
+    Optimization facilities
+
+Author:
+
+    Christoph M. Wintersteiger (cwinter) 2015-12-03
+
+Notes:
+
+--*/
+#ifndef Z3_OPTIMIZATION_H_
+#define Z3_OPTIMIZATION_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /** \defgroup capi C API */
+    /*@{*/
+
+    /** @name Optimization facilities */
+    /*@{*/
+    /**
+       \brief Create a new optimize context.
+
+       \remark User must use #Z3_optimize_inc_ref and #Z3_optimize_dec_ref to manage optimize objects.
+       Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
+
+       def_API('Z3_mk_optimize', OPTIMIZE, (_in(CONTEXT), ))
+    */
+    Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
+
+    /**
+       \brief Increment the reference counter of the given optimize context
+
+       def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Decrement the reference counter of the given optimize context.
+
+       def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Assert hard constraint to the optimization context.
+
+       \sa Z3_optimize_assert_soft
+
+       def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
+
+    /**
+       \brief Assert soft constraint to the optimization context.
+       \param c - context
+       \param o - optimization context
+       \param a - formula
+       \param weight - a positive weight, penalty for violating soft constraint
+       \param id - optional identifier to group soft constraints
+
+       \sa Z3_optimize_assert
+
+       def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
+    */
+    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
+
+    /**
+       \brief Add a maximization constraint.
+       \param c - context
+       \param o - optimization context
+       \param t - arithmetical term
+
+       \sa Z3_optimize_minimize
+
+       def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
+
+    /**
+       \brief Add a minimization constraint.
+       \param c - context
+       \param o - optimization context
+       \param t - arithmetical term
+
+       \sa Z3_optimize_maximize
+
+       def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
+    */
+    unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
+
+    /**
+       \brief Create a backtracking point.
+
+       The optimize solver contains a set of rules, added facts and assertions.
+       The set of rules, facts and assertions are restored upon calling #Z3_optimize_pop.
+
+       \sa Z3_optimize_pop
+
+       def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Backtrack one level.
+
+       \sa Z3_optimize_push
+
+       \pre The number of calls to pop cannot exceed calls to push.
+
+       def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Check consistency and produce optimal values.
+       \param c - context
+       \param o - optimization context
+       \param num_assumptions - number of additional assumptions
+       \param assumptions - the additional assumptions
+
+       \sa Z3_optimize_get_reason_unknown
+       \sa Z3_optimize_get_model
+       \sa Z3_optimize_get_statistics
+       \sa Z3_optimize_get_unsat_core
+
+       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
+    */
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
+
+
+    /**
+       \brief Retrieve a string that describes the last status returned by #Z3_optimize_check.
+
+       Use this method when #Z3_optimize_check returns \c Z3_L_UNDEF.
+
+       def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) ))
+    */
+    Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Retrieve the model for the last #Z3_optimize_check
+
+       The error handler is invoked if a model is not available because
+       the commands above were not invoked for the given optimization
+       solver, or if the result was \c Z3_L_FALSE.
+
+       def_API('Z3_optimize_get_model', MODEL, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Retrieve the unsat core for the last #Z3_optimize_check
+       The unsat core is a subset of the assumptions \c a.
+
+       def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))       
+     */
+    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Set parameters on optimization context.
+
+       \param c - context
+       \param o - optimization context
+       \param p - parameters
+
+       \sa Z3_optimize_get_help
+       \sa Z3_optimize_get_param_descrs
+
+       def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS)))
+    */
+    void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p);
+
+    /**
+       \brief Return the parameter description set for the given optimize object.
+
+       \param c - context
+       \param o - optimization context
+
+       \sa Z3_optimize_get_help
+       \sa Z3_optimize_set_params
+
+       def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Retrieve lower bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       \sa Z3_optimize_get_upper
+       \sa Z3_optimize_get_lower_as_vector
+       \sa Z3_optimize_get_upper_as_vector
+
+       def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
+
+    /**
+       \brief Retrieve upper bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       \sa Z3_optimize_get_lower
+       \sa Z3_optimize_get_lower_as_vector
+       \sa Z3_optimize_get_upper_as_vector
+
+       def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
+
+
+    /**
+       \brief Retrieve lower bound value or approximation for the i'th optimization objective.
+              The returned vector is of length 3. It always contains numerals.
+              The three numerals are coefficients \c a, \c b, \c c and encode the result of
+              #Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.
+              
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       \sa Z3_optimize_get_lower
+       \sa Z3_optimize_get_upper
+       \sa Z3_optimize_get_upper_as_vector
+
+       def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
+
+    /**
+       \brief Retrieve upper bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       \sa Z3_optimize_get_lower
+       \sa Z3_optimize_get_upper
+       \sa Z3_optimize_get_lower_as_vector
+
+       def_API('Z3_optimize_get_upper_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
+
+
+    /**
+       \brief Print the current context as a string.
+       \param c - context.
+       \param o - optimization context.
+
+       \sa Z3_optimize_from_file
+       \sa Z3_optimize_from_string
+
+       def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Parse an SMT-LIB2 string with assertions,
+       soft constraints and optimization objectives.
+       Add the parsed constraints and objectives to the optimization context.
+
+       \param c - context.
+       \param o - optimize context.
+       \param s - string containing SMT2 specification.
+
+       \sa Z3_optimize_from_file
+       \sa Z3_optimize_to_string
+
+       def_API('Z3_optimize_from_string', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
+    */
+    void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
+
+    /**
+       \brief Parse an SMT-LIB2 file with assertions,
+       soft constraints and optimization objectives.
+       Add the parsed constraints and objectives to the optimization context.
+
+       \param c - context.
+       \param o - optimize context.
+       \param s - path to file containing SMT2 specification.
+
+       \sa Z3_optimize_from_string
+       \sa Z3_optimize_to_string
+
+       def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING)))
+    */
+    void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
+
+    /**
+       \brief Return a string containing a description of parameters accepted by optimize.
+
+       \sa Z3_optimize_get_param_descrs
+       \sa Z3_optimize_set_params
+
+       def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
+
+    /**
+       \brief Retrieve statistics information from the last call to #Z3_optimize_check
+
+       def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
+
+    /**
+       \brief Return the set of asserted formulas on the optimization context.
+
+       def_API('Z3_optimize_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
+
+    /**
+       \brief Return objectives on the optimization context.
+       If the objective function is a max-sat objective it is returned
+       as a Pseudo-Boolean (minimization) sum of the form \ccode{(+ (if f1 w1 0) (if f2 w2 0) ...)}
+       If the objective function is entered as a maximization objective, then return
+       the corresponding minimization objective. In this way the resulting objective
+       function is always returned as a minimization objective.
+
+       def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
+
+    /*@}*/
+    /*@}*/
+
+#ifdef __cplusplus
+}
+#endif // __cplusplus
+
+#endif