Functions
Optimization facilities
Z3_optimize Z3_API	Z3_mk_optimize (Z3_context c)
	Create a new optimize context. More...

void Z3_API	Z3_optimize_inc_ref (Z3_context c, Z3_optimize d)
	Increment the reference counter of the given optimize context. More...

void Z3_API	Z3_optimize_dec_ref (Z3_context c, Z3_optimize d)
	Decrement the reference counter of the given optimize context. More...

void Z3_API	Z3_optimize_assert (Z3_context c, Z3_optimize o, Z3_ast a)
	Assert hard constraint to the optimization context. More...

void Z3_API	Z3_optimize_assert_and_track (Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
	Assert tracked hard constraint to the optimization context. More...

unsigned Z3_API	Z3_optimize_assert_soft (Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
	Assert soft constraint to the optimization context. More...

unsigned Z3_API	Z3_optimize_maximize (Z3_context c, Z3_optimize o, Z3_ast t)
	Add a maximization constraint. More...

unsigned Z3_API	Z3_optimize_minimize (Z3_context c, Z3_optimize o, Z3_ast t)
	Add a minimization constraint. More...

void Z3_API	Z3_optimize_push (Z3_context c, Z3_optimize d)
	Create a backtracking point. More...

void Z3_API	Z3_optimize_pop (Z3_context c, Z3_optimize d)
	Backtrack one level. More...

Z3_lbool Z3_API	Z3_optimize_check (Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
	Check consistency and produce optimal values. More...

Z3_string Z3_API	Z3_optimize_get_reason_unknown (Z3_context c, Z3_optimize d)
	Retrieve a string that describes the last status returned by Z3_optimize_check. More...

Z3_model Z3_API	Z3_optimize_get_model (Z3_context c, Z3_optimize o)
	Retrieve the model for the last Z3_optimize_check. More...

Z3_ast_vector Z3_API	Z3_optimize_get_unsat_core (Z3_context c, Z3_optimize o)
	Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions `a`. More...

void Z3_API	Z3_optimize_set_params (Z3_context c, Z3_optimize o, Z3_params p)
	Set parameters on optimization context. More...

Z3_param_descrs Z3_API	Z3_optimize_get_param_descrs (Z3_context c, Z3_optimize o)
	Return the parameter description set for the given optimize object. More...

Z3_ast Z3_API	Z3_optimize_get_lower (Z3_context c, Z3_optimize o, unsigned idx)
	Retrieve lower bound value or approximation for the i'th optimization objective. More...

Z3_ast Z3_API	Z3_optimize_get_upper (Z3_context c, Z3_optimize o, unsigned idx)
	Retrieve upper bound value or approximation for the i'th optimization objective. More...

Z3_ast_vector Z3_API	Z3_optimize_get_lower_as_vector (Z3_context c, Z3_optimize o, unsigned idx)
	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 `a`, `b`, `c` and encode the result of Z3_optimize_get_lower `a * infinity + b + c * epsilon`. More...

Z3_ast_vector Z3_API	Z3_optimize_get_upper_as_vector (Z3_context c, Z3_optimize o, unsigned idx)
	Retrieve upper bound value or approximation for the i'th optimization objective. More...

Z3_string Z3_API	Z3_optimize_to_string (Z3_context c, Z3_optimize o)
	Print the current context as a string. More...

void Z3_API	Z3_optimize_from_string (Z3_context c, Z3_optimize o, Z3_string s)
	Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context. More...

void Z3_API	Z3_optimize_from_file (Z3_context c, Z3_optimize o, Z3_string s)
	Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context. More...

Z3_string Z3_API	Z3_optimize_get_help (Z3_context c, Z3_optimize t)
	Return a string containing a description of parameters accepted by optimize. More...

Z3_stats Z3_API	Z3_optimize_get_statistics (Z3_context c, Z3_optimize d)
	Retrieve statistics information from the last call to Z3_optimize_check. More...

Z3_ast_vector Z3_API	Z3_optimize_get_assertions (Z3_context c, Z3_optimize o)
	Return the set of asserted formulas on the optimization context. More...

Z3_ast_vector Z3_API	Z3_optimize_get_objectives (Z3_context c, Z3_optimize o)
	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 `(+ (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. More...

Function Documentation

◆ Z3_mk_optimize()

Z3_optimize Z3_API Z3_mk_optimize ( Z3_context c )

Create a new optimize context.

Remarks: 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.

Referenced by optimize::optimize().

◆ Z3_optimize_assert()

void Z3_API Z3_optimize_assert	(	Z3_context	c,
		Z3_optimize	o,
		Z3_ast	a
	)

Assert hard constraint to the optimization context.

See also: Z3_optimize_assert_soft; Z3_optimize_assert_and_track

Referenced by optimize::add(), and Optimize::assert_exprs().

◆ Z3_optimize_assert_and_track()

void Z3_API Z3_optimize_assert_and_track	(	Z3_context	c,
		Z3_optimize	o,
		Z3_ast	a,
		Z3_ast	t
	)

Assert tracked hard constraint to the optimization context.

See also: Z3_optimize_assert; Z3_optimize_assert_soft

Referenced by optimize::add(), and Optimize::assert_and_track().

◆ Z3_optimize_assert_soft()

unsigned Z3_API Z3_optimize_assert_soft	(	Z3_context	c,
		Z3_optimize	o,
		Z3_ast	a,
		Z3_string	weight,
		Z3_symbol	id
	)

Assert soft constraint to the optimization context.

Parameters

c	- context
o	- optimization context
a	- formula
weight	- a positive weight, penalty for violating soft constraint
id	- optional identifier to group soft constraints

See also: Z3_optimize_assert; Z3_optimize_assert_and_track

Referenced by optimize::add_soft(), and Optimize::add_soft().

◆ Z3_optimize_check()

Z3_lbool Z3_API Z3_optimize_check	(	Z3_context	c,
		Z3_optimize	o,
		unsigned	num_assumptions,
		Z3_ast const	assumptions[]
	)

Check consistency and produce optimal values.

Parameters

c	- context
o	- optimization context
num_assumptions	- number of additional assumptions
assumptions	- the additional assumptions

See also: Z3_optimize_get_reason_unknown; Z3_optimize_get_model; Z3_optimize_get_statistics; Z3_optimize_get_unsat_core

Referenced by optimize::check(), and Optimize::check().

◆ Z3_optimize_dec_ref()

void Z3_API Z3_optimize_dec_ref	(	Z3_context	c,
		Z3_optimize	d
	)

Decrement the reference counter of the given optimize context.

Referenced by Optimize::__del__(), optimize::operator=(), and optimize::~optimize().

◆ Z3_optimize_from_file()

void Z3_API Z3_optimize_from_file	(	Z3_context	c,
		Z3_optimize	o,
		Z3_string	s
	)

Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Parameters

c	- context.
o	- optimize context.
s	- path to file containing SMT2 specification.

See also: Z3_optimize_from_string; Z3_optimize_to_string

Referenced by optimize::from_file(), and Optimize::from_file().

◆ Z3_optimize_from_string()

void Z3_API Z3_optimize_from_string	(	Z3_context	c,
		Z3_optimize	o,
		Z3_string	s
	)

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

Parameters

c	- context.
o	- optimize context.
s	- string containing SMT2 specification.

See also: Z3_optimize_from_file; Z3_optimize_to_string

Referenced by optimize::from_string(), and Optimize::from_string().

◆ Z3_optimize_get_assertions()

Z3_ast_vector Z3_API Z3_optimize_get_assertions	(	Z3_context	c,
		Z3_optimize	o
	)

Return the set of asserted formulas on the optimization context.

Referenced by optimize::assertions(), and Optimize::assertions().

◆ Z3_optimize_get_help()

Z3_string Z3_API Z3_optimize_get_help	(	Z3_context	c,
		Z3_optimize	t
	)

Return a string containing a description of parameters accepted by optimize.

See also: Z3_optimize_get_param_descrs; Z3_optimize_set_params

Referenced by optimize::help(), and Optimize::help().

◆ Z3_optimize_get_lower()

Z3_ast Z3_API Z3_optimize_get_lower	(	Z3_context	c,
		Z3_optimize	o,
		unsigned	idx
	)

Retrieve lower bound value or approximation for the i'th optimization objective.

Parameters

c	- context
o	- optimization context
idx	- index of optimization objective

See also: Z3_optimize_get_upper; Z3_optimize_get_lower_as_vector; Z3_optimize_get_upper_as_vector

Referenced by optimize::lower(), and OptimizeObjective::lower().

◆ Z3_optimize_get_lower_as_vector()

Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector	(	Z3_context	c,
		Z3_optimize	o,
		unsigned	idx
	)

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 a, b, c and encode the result of Z3_optimize_get_lower a * infinity + b + c * epsilon.

Parameters

c	- context
o	- optimization context
idx	- index of optimization objective

See also: Z3_optimize_get_lower; Z3_optimize_get_upper; Z3_optimize_get_upper_as_vector

Referenced by OptimizeObjective::lower_values().

◆ Z3_optimize_get_model()

Z3_model Z3_API Z3_optimize_get_model	(	Z3_context	c,
		Z3_optimize	o
	)

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 Z3_L_FALSE.

Referenced by optimize::get_model(), and Optimize::model().

◆ Z3_optimize_get_objectives()

Z3_ast_vector Z3_API Z3_optimize_get_objectives	(	Z3_context	c,
		Z3_optimize	o
	)

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 (+ (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.

Referenced by optimize::objectives(), and Optimize::objectives().

◆ Z3_optimize_get_param_descrs()

Z3_param_descrs Z3_API Z3_optimize_get_param_descrs	(	Z3_context	c,
		Z3_optimize	o
	)

Return the parameter description set for the given optimize object.

Parameters

c	- context
o	- optimization context

See also: Z3_optimize_get_help; Z3_optimize_set_params

Referenced by Optimize::param_descrs().

◆ Z3_optimize_get_reason_unknown()

Z3_string Z3_API Z3_optimize_get_reason_unknown	(	Z3_context	c,
		Z3_optimize	d
	)

Retrieve a string that describes the last status returned by Z3_optimize_check.

Use this method when Z3_optimize_check returns Z3_L_UNDEF.

Referenced by Optimize::reason_unknown().

◆ Z3_optimize_get_statistics()

Z3_stats Z3_API Z3_optimize_get_statistics	(	Z3_context	c,
		Z3_optimize	d
	)

Retrieve statistics information from the last call to Z3_optimize_check.

Referenced by optimize::statistics(), and Optimize::statistics().

◆ Z3_optimize_get_unsat_core()

Z3_ast_vector Z3_API Z3_optimize_get_unsat_core	(	Z3_context	c,
		Z3_optimize	o
	)

Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions a.

Referenced by optimize::unsat_core(), and Optimize::unsat_core().

◆ Z3_optimize_get_upper()

Z3_ast Z3_API Z3_optimize_get_upper	(	Z3_context	c,
		Z3_optimize	o,
		unsigned	idx
	)

Retrieve upper bound value or approximation for the i'th optimization objective.

Parameters

c	- context
o	- optimization context
idx	- index of optimization objective

See also: Z3_optimize_get_lower; Z3_optimize_get_lower_as_vector; Z3_optimize_get_upper_as_vector

Referenced by optimize::upper(), and OptimizeObjective::upper().

◆ Z3_optimize_get_upper_as_vector()

Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector	(	Z3_context	c,
		Z3_optimize	o,
		unsigned	idx
	)

Retrieve upper bound value or approximation for the i'th optimization objective.

Parameters

c	- context
o	- optimization context
idx	- index of optimization objective

See also: Z3_optimize_get_lower; Z3_optimize_get_upper; Z3_optimize_get_lower_as_vector

Referenced by OptimizeObjective::upper_values().

◆ Z3_optimize_inc_ref()

void Z3_API Z3_optimize_inc_ref	(	Z3_context	c,
		Z3_optimize	d
	)

Increment the reference counter of the given optimize context.

Referenced by optimize::operator=(), and optimize::optimize().

◆ Z3_optimize_maximize()

unsigned Z3_API Z3_optimize_maximize	(	Z3_context	c,
		Z3_optimize	o,
		Z3_ast	t
	)

Add a maximization constraint.

Parameters

c	- context
o	- optimization context
t	- arithmetical term

See also: Z3_optimize_minimize

Referenced by optimize::maximize(), and Optimize::maximize().

◆ Z3_optimize_minimize()

unsigned Z3_API Z3_optimize_minimize	(	Z3_context	c,
		Z3_optimize	o,
		Z3_ast	t
	)

Add a minimization constraint.

Parameters

c	- context
o	- optimization context
t	- arithmetical term

See also: Z3_optimize_maximize

Referenced by optimize::minimize(), and Optimize::minimize().

◆ Z3_optimize_pop()

void Z3_API Z3_optimize_pop	(	Z3_context	c,
		Z3_optimize	d
	)

Backtrack one level.

See also: Z3_optimize_push

Precondition: The number of calls to pop cannot exceed calls to push.

Referenced by optimize::pop(), and Optimize::pop().

◆ Z3_optimize_push()

void Z3_API Z3_optimize_push	(	Z3_context	c,
		Z3_optimize	d
	)

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.

See also: Z3_optimize_pop

Referenced by optimize::push(), and Optimize::push().

◆ Z3_optimize_set_params()

void Z3_API Z3_optimize_set_params	(	Z3_context	c,
		Z3_optimize	o,
		Z3_params	p
	)

Set parameters on optimization context.

Parameters

c	- context
o	- optimization context
p	- parameters

See also: Z3_optimize_get_help; Z3_optimize_get_param_descrs

Referenced by optimize::set(), and Optimize::set().

◆ Z3_optimize_to_string()

Z3_string Z3_API Z3_optimize_to_string	(	Z3_context	c,
		Z3_optimize	o
	)

Print the current context as a string.

Parameters

c	- context.
o	- optimization context.

See also: Z3_optimize_from_file; Z3_optimize_from_string

Referenced by Optimize::sexpr().

Functions

Function Documentation

◆ Z3_mk_optimize()

◆ Z3_optimize_assert()

◆ Z3_optimize_assert_and_track()

◆ Z3_optimize_assert_soft()

◆ Z3_optimize_check()

◆ Z3_optimize_dec_ref()

◆ Z3_optimize_from_file()

◆ Z3_optimize_from_string()

◆ Z3_optimize_get_assertions()

◆ Z3_optimize_get_help()

◆ Z3_optimize_get_lower()

◆ Z3_optimize_get_lower_as_vector()

◆ Z3_optimize_get_model()

◆ Z3_optimize_get_objectives()

◆ Z3_optimize_get_param_descrs()

◆ Z3_optimize_get_reason_unknown()

◆ Z3_optimize_get_statistics()

◆ Z3_optimize_get_unsat_core()

◆ Z3_optimize_get_upper()

◆ Z3_optimize_get_upper_as_vector()

◆ Z3_optimize_inc_ref()

◆ Z3_optimize_maximize()

◆ Z3_optimize_minimize()

◆ Z3_optimize_pop()

◆ Z3_optimize_push()

◆ Z3_optimize_set_params()

◆ Z3_optimize_to_string()