Optimize Class Reference

Inheritance diagram for Optimize:

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

Data Fields
	ctx
	optimize

Detailed Description

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

Definition at line 7740 of file z3py.py.

Constructor & Destructor Documentation

__init__()

def __init__	(		self,
			ctx = None
	)

Definition at line 7743 of file z3py.py.

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

__del__()

def __del__

(

self

)

Definition at line 7752 of file z3py.py.

    def __del__(self):
        if self.optimize is not None and self.ctx.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

__deepcopy__()

def __deepcopy__	(		self,
			memo = {}
	)

Definition at line 7749 of file z3py.py.

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

__iadd__()

def __iadd__	(		self,
			fml
	)

Definition at line 7789 of file z3py.py.

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

__repr__()

def __repr__

(

self

)

Return a formatted string with all added rules and constraints.

Definition at line 7929 of file z3py.py.

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

add()

def add	(		self,
		*	args
	)

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

Definition at line 7785 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)
 

Referenced by Optimize.__iadd__().

add_soft()

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.

Definition at line 7822 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()

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

Definition at line 7793 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()

def assert_exprs	(		self,
		*	args
	)

Assert constraints as background axioms for the optimize solver.

Definition at line 7773 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())
 

Referenced by Optimize.add().

assertions()

def assertions

(

self

)

Return an AST vector containing all added constraints.

Definition at line 7921 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()

def check	(		self,
		*	assumptions
	)

Check satisfiability while optimizing objective functions.

Definition at line 7870 of file z3py.py.

    def check(self, *assumptions):
        """Check satisfiability while optimizing objective functions."""
        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()

def from_file	(		self,
			filename
	)

Parse assertions and objectives from a file

Definition at line 7913 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()

def from_string	(		self,
			s
	)

Parse assertions and objectives from a string

Definition at line 7917 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()

def help

(

self

)

Display a string describing all available options.

Definition at line 7765 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()

def lower	(		self,
			obj
	)

Definition at line 7893 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()

def lower_values	(		self,
			obj
	)

Definition at line 7903 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()

def maximize	(		self,
			arg
	)

Add objective function to maximize.

Definition at line 7846 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()

def minimize	(		self,
			arg
	)

Add objective function to minimize.

Definition at line 7854 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()

def model

(

self

)

Return a model for the last check().

Definition at line 7883 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")
 

Referenced by FuncInterp.translate().

objectives()

def objectives

(

self

)

returns set of objective functions

Definition at line 7925 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()

def param_descrs

(

self

)

Return the parameter description set.

Definition at line 7769 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()

def pop

(

self

)

restore to previously created backtracking point

Definition at line 7866 of file z3py.py.

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

push()

def push

(

self

)

create a backtracking point for added rules, facts and assertions

Definition at line 7862 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()

def reason_unknown

(

self

)

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

Definition at line 7879 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()

def set	(		self,
		*	args,
		**	keys
	)

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

Definition at line 7758 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_on_model()

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

Definition at line 7944 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()

def 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 7933 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)
 

Referenced by Optimize.__repr__().

statistics()

def statistics

(

self

)

Return statistics for the last check`.

Definition at line 7939 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)
 

unsat_core()

def unsat_core

(

self

)

Definition at line 7890 of file z3py.py.

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

upper()

def upper	(		self,
			obj
	)

Definition at line 7898 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()

def upper_values	(		self,
			obj
	)

Definition at line 7908 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

ctx

ctx

Definition at line 7744 of file z3py.py.

Referenced by Probe.__call__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), UserPropagateBase.conflict(), UserPropagateBase.ctx_ref(), Optimize.from_file(), Optimize.from_string(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Tactic.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.set_on_model(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Optimize.statistics(), and Optimize.unsat_core().

optimize

optimize

Definition at line 7745 of file z3py.py.

Referenced by Optimize.__deepcopy__(), Optimize.__del__(), Optimize.add_soft(), Optimize.assert_and_track(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), Optimize.from_file(), Optimize.from_string(), Optimize.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Optimize.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.set_on_model(), Optimize.sexpr(), Optimize.statistics(), and Optimize.unsat_core().