z3_optimization.h

Go to the documentation of this file.

/*++
Copyright (c) 2015 Microsoft Corporation
 
Module Name:
 
    z3_optimization.h
 
Abstract:
 
    Optimization facilities
 
Author:
 
    Christoph M. Wintersteiger (cwinter) 2015-12-03
 
Notes:
 
--*/
#pragma once
 
typedef void Z3_model_eh(void* ctx);
 
#ifdef __cplusplus
extern "C" {
#endif // __cplusplus
 
    Z3_optimize Z3_API Z3_mk_optimize(Z3_context c);
 
    void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d);
 
    void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d);
 
    void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
 
 
    void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t);
 
    unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
 
    unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
 
    unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);
 
    void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d);
 
    void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d);
 
    void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val);
    
    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
 
 
    Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d);
 
    Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
 
    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
 
    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);
 
    Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx);
 
    Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
 
 
    Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
 
    Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
 
 
    Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o);
 
    void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s);
 
    void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s);
 
    Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);
 
    Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d);
 
    Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o);
 
    Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o);
 
 
    void Z3_API Z3_optimize_register_model_eh(
        Z3_context   c, 
        Z3_optimize  o,
        Z3_model     m,
        void*        ctx,
        Z3_model_eh  model_eh);
 
 
#ifdef __cplusplus
}
#endif // __cplusplus