Inheritance diagram for Optimize:

Public Member Functions
	__init__ (self, optimize=None, ctx=None)
	__copy__ (self)
	__deepcopy__ (self, memo={})
	__del__ (self)
	__enter__ (self)
	__exit__ (self, *exc_info)
	set (self, args, *keys)
	help (self)
	param_descrs (self)
	assert_exprs (self, *args)
	add (self, *args)
	__iadd__ (self, fml)
	assert_and_track (self, a, p)
	add_soft (self, arg, weight="1", id=None)
	set_initial_value (self, var, value)
	maximize (self, arg)
	minimize (self, arg)
	push (self)
	pop (self)
	check (self, *assumptions)
	reason_unknown (self)
	model (self)
	unsat_core (self)
	lower (self, obj)
	upper (self, obj)
	lower_values (self, obj)
	upper_values (self, obj)
	from_file (self, filename)
	from_string (self, s)
	assertions (self)
	objectives (self)
	__repr__ (self)
	sexpr (self)
	statistics (self)
	translate (self, target)
	set_on_model (self, on_model)
Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx = _get_ctx(ctx)
	optimize = Z3_mk_optimize(self.ctx.ref())

Protected Attributes
	_on_models_id = None

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Optimize API provides methods for solving using objective functions and weighted soft constraints

Definition at line 8716 of file z3py.py.

Constructor & Destructor Documentation

◆ init()

__init__	(	self,
		optimize = None,
		ctx = None )

Definition at line 8719 of file z3py.py.

    def __init__(self, optimize=None, ctx=None):
        self.ctx = _get_ctx(ctx)
        if optimize is None:
            self.optimize = Z3_mk_optimize(self.ctx.ref())
        else:
            self.optimize = optimize
        self._on_models_id = None
        Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
 

◆ del()

__del__ ( self )

Definition at line 8734 of file z3py.py.

    def __del__(self):
        if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
            Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
        if self._on_models_id is not None:
            del _on_models[self._on_models_id]
 

Member Function Documentation

◆ copy()

__copy__ ( self )

Definition at line 8728 of file z3py.py.

    def __copy__(self):
        return self.translate(self.ctx)
 

◆ deepcopy()

__deepcopy__	(		self,
			memo = {} )

Definition at line 8731 of file z3py.py.

    def __deepcopy__(self, memo={}):
        return self.translate(self.ctx)
 

◆ enter()

__enter__ ( self )

Definition at line 8740 of file z3py.py.

    def __enter__(self):
        self.push()
        return self
 

◆ exit()

__exit__	(		self,
		*	exc_info )

Definition at line 8744 of file z3py.py.

    def __exit__(self, *exc_info):
        self.pop()
 

◆ iadd()

__iadd__	(		self,
			fml )

Definition at line 8778 of file z3py.py.

    def __iadd__(self, fml):
        self.add(fml)
        return self
 

◆ repr()

__repr__ ( self )

Return a formatted string with all added rules and constraints.

Definition at line 8925 of file z3py.py.

    def __repr__(self):
        """Return a formatted string with all added rules and constraints."""
        return self.sexpr()
 

◆ add()

add	(		self,
		*	args )

Assert constraints as background axioms for the optimize solver. Alias for assert_expr.

Definition at line 8774 of file z3py.py.

    def add(self, *args):
        """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
        self.assert_exprs(*args)
 

◆ add_soft()

add_soft	(	self,
		arg,
		weight = "1",
		id = None )

Add soft constraint with optional weight and optional identifier.
   If no weight is supplied, then the penalty for violating the soft constraint
   is 1.
   Soft constraints are grouped by identifiers. Soft constraints that are
   added without identifiers are grouped by default.

Definition at line 8811 of file z3py.py.

    def add_soft(self, arg, weight="1", id=None):
        """Add soft constraint with optional weight and optional identifier.
           If no weight is supplied, then the penalty for violating the soft constraint
           is 1.
           Soft constraints are grouped by identifiers. Soft constraints that are
           added without identifiers are grouped by default.
        """
        if _is_int(weight):
            weight = "%d" % weight
        elif isinstance(weight, float):
            weight = "%f" % weight
        if not isinstance(weight, str):
            raise Z3Exception("weight should be a string or an integer")
        if id is None:
            id = ""
        id = to_symbol(id, self.ctx)
 
        def asoft(a):
            v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
            return OptimizeObjective(self, v, False)
        if sys.version_info.major >= 3 and isinstance(arg, Iterable):
            return [asoft(a) for a in arg]
        return asoft(arg)
 

◆ assert_and_track()

assert_and_track	(	self,
		a,
		p )

Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.

If `p` is a string, it will be automatically converted into a Boolean constant.

>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Optimize()
>>> s.assert_and_track(x > 0,  'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0,  p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True

Definition at line 8782 of file z3py.py.

    def assert_and_track(self, a, p):
        """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
 
        If `p` is a string, it will be automatically converted into a Boolean constant.
 
        >>> x = Int('x')
        >>> p3 = Bool('p3')
        >>> s = Optimize()
        >>> s.assert_and_track(x > 0,  'p1')
        >>> s.assert_and_track(x != 1, 'p2')
        >>> s.assert_and_track(x < 0,  p3)
        >>> print(s.check())
        unsat
        >>> c = s.unsat_core()
        >>> len(c)
        2
        >>> Bool('p1') in c
        True
        >>> Bool('p2') in c
        False
        >>> p3 in c
        True
        """
        if isinstance(p, str):
            p = Bool(p, self.ctx)
        _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
        _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
        Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
 

◆ assert_exprs()

assert_exprs	(		self,
		*	args )

Assert constraints as background axioms for the optimize solver.

Definition at line 8762 of file z3py.py.

    def assert_exprs(self, *args):
        """Assert constraints as background axioms for the optimize solver."""
        args = _get_args(args)
        s = BoolSort(self.ctx)
        for arg in args:
            if isinstance(arg, Goal) or isinstance(arg, AstVector):
                for f in arg:
                    Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
            else:
                arg = s.cast(arg)
                Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
 

◆ assertions()

assertions ( self )

Return an AST vector containing all added constraints.

Definition at line 8917 of file z3py.py.

    def assertions(self):
        """Return an AST vector containing all added constraints."""
        return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx)
 

◆ check()

check	(		self,
		*	assumptions )

Check consistency and produce optimal values.

Definition at line 8866 of file z3py.py.

    def check(self, *assumptions):
        """Check consistency and produce optimal values."""
        assumptions = _get_args(assumptions)
        num = len(assumptions)
        _assumptions = (Ast * num)()
        for i in range(num):
            _assumptions[i] = assumptions[i].as_ast()
        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
 

◆ from_file()

from_file	(		self,
			filename )

Parse assertions and objectives from a file

Definition at line 8909 of file z3py.py.

    def from_file(self, filename):
        """Parse assertions and objectives from a file"""
        Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
 

◆ from_string()

from_string	(		self,
			s )

Parse assertions and objectives from a string

Definition at line 8913 of file z3py.py.

    def from_string(self, s):
        """Parse assertions and objectives from a string"""
        Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
 

◆ help()

help ( self )

Display a string describing all available options.

Definition at line 8754 of file z3py.py.

    def help(self):
        """Display a string describing all available options."""
        print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
 

◆ lower()

lower	(		self,
			obj )

Definition at line 8889 of file z3py.py.

    def lower(self, obj):
        if not isinstance(obj, OptimizeObjective):
            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
        return obj.lower()
 

◆ lower_values()

lower_values	(		self,
			obj )

Definition at line 8899 of file z3py.py.

    def lower_values(self, obj):
        if not isinstance(obj, OptimizeObjective):
            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
        return obj.lower_values()
 

◆ maximize()

maximize	(		self,
			arg )

Add objective function to maximize.

Definition at line 8842 of file z3py.py.

    def maximize(self, arg):
        """Add objective function to maximize."""
        return OptimizeObjective(
            self,
            Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
            is_max=True,
        )
 

◆ minimize()

minimize	(		self,
			arg )

Add objective function to minimize.

Definition at line 8850 of file z3py.py.

    def minimize(self, arg):
        """Add objective function to minimize."""
        return OptimizeObjective(
            self,
            Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
            is_max=False,
        )
 

◆ model()

model ( self )

Return a model for the last check().

Definition at line 8879 of file z3py.py.

    def model(self):
        """Return a model for the last check()."""
        try:
            return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
        except Z3Exception:
            raise Z3Exception("model is not available")
 

◆ objectives()

objectives ( self )

returns set of objective functions

Definition at line 8921 of file z3py.py.

    def objectives(self):
        """returns set of objective functions"""
        return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx)
 

◆ param_descrs()

param_descrs ( self )

Return the parameter description set.

Definition at line 8758 of file z3py.py.

    def param_descrs(self):
        """Return the parameter description set."""
        return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
 

◆ pop()

pop ( self )

restore to previously created backtracking point

Definition at line 8862 of file z3py.py.

    def pop(self):
        """restore to previously created backtracking point"""
        Z3_optimize_pop(self.ctx.ref(), self.optimize)
 

◆ push()

push ( self )

create a backtracking point for added rules, facts and assertions

Definition at line 8858 of file z3py.py.

    def push(self):
        """create a backtracking point for added rules, facts and assertions"""
        Z3_optimize_push(self.ctx.ref(), self.optimize)
 

◆ reason_unknown()

reason_unknown ( self )

Return a string that describes why the last `check()` returned `unknown`.

Definition at line 8875 of file z3py.py.

    def reason_unknown(self):
        """Return a string that describes why the last `check()` returned `unknown`."""
        return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
 

◆ set()

set	(		self,
		*	args,
		**	keys )

Set a configuration option.
The method `help()` return a string containing all available options.

Definition at line 8747 of file z3py.py.

    def set(self, *args, **keys):
        """Set a configuration option.
        The method `help()` return a string containing all available options.
        """
        p = args2params(args, keys, self.ctx)
        Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
 

◆ set_initial_value()

set_initial_value	(	self,
		var,
		value )

initialize the solver's state by setting the initial value of var to value

Definition at line 8835 of file z3py.py.

    def set_initial_value(self, var, value):
        """initialize the solver's state by setting the initial value of var to value
        """
        s = var.sort()
        value = s.cast(value)
        Z3_optimize_set_initial_value(self.ctx.ref(), self.optimize, var.ast, value.ast)
 

◆ set_on_model()

set_on_model	(		self,
			on_model )

Register a callback that is invoked with every incremental improvement to
objective values. The callback takes a model as argument.
The life-time of the model is limited to the callback so the
model has to be (deep) copied if it is to be used after the callback

Definition at line 8953 of file z3py.py.

    def set_on_model(self, on_model):
        """Register a callback that is invoked with every incremental improvement to
        objective values. The callback takes a model as argument.
        The life-time of the model is limited to the callback so the
        model has to be (deep) copied if it is to be used after the callback
        """
        id = len(_on_models) + 41
        mdl = Model(self.ctx)
        _on_models[id] = (on_model, mdl)
        self._on_models_id = id
        Z3_optimize_register_model_eh(
            self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
        )
 
 

◆ sexpr()

sexpr ( self )

Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.

Definition at line 8929 of file z3py.py.

    def sexpr(self):
        """Return a formatted string (in Lisp-like format) with all added constraints.
        We say the string is in s-expression format.
        """
        return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
 

◆ statistics()

statistics ( self )

Return statistics for the last check`.

Definition at line 8935 of file z3py.py.

    def statistics(self):
        """Return statistics for the last check`.
        """
        return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
 

◆ translate()

translate	(		self,
			target )

Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

>>> c1 = Context()
>>> c2 = Context()
>>> o1 = Optimize(ctx=c1)
>>> o2 = o1.translate(c2)

Definition at line 8940 of file z3py.py.

    def translate(self, target):
        """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
 
        >>> c1 = Context()
        >>> c2 = Context()
        >>> o1 = Optimize(ctx=c1)
        >>> o2 = o1.translate(c2)
        """
        if z3_debug():
            _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
        opt = Z3_optimize_translate(self.ctx.ref(), self.optimize, target.ref())
        return Optimize(opt, target)
 

◆ unsat_core()

unsat_core ( self )

Definition at line 8886 of file z3py.py.

    def unsat_core(self):
        return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
 

◆ upper()

upper	(		self,
			obj )

Definition at line 8894 of file z3py.py.

    def upper(self, obj):
        if not isinstance(obj, OptimizeObjective):
            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
        return obj.upper()
 

◆ upper_values()

upper_values	(		self,
			obj )

Definition at line 8904 of file z3py.py.

    def upper_values(self, obj):
        if not isinstance(obj, OptimizeObjective):
            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
        return obj.upper_values()
 

Field Documentation

◆ _on_models_id

_on_models_id = None

protected

Definition at line 8725 of file z3py.py.

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8720 of file z3py.py.

◆ optimize

optimize = Z3_mk_optimize(self.ctx.ref())

Definition at line 8722 of file z3py.py.

Public Member Functions

Data Fields

Protected Attributes

Additional Inherited Members