Optimize Class Reference

Inheritance diagram for Optimize:

Public Member Functions
def	__init__
def	__del__
def	set
def	help
def	param_descrs
def	assert_exprs
def	add
def	add_soft
def	maximize
def	minimize
def	push
def	pop
def	check
def	reason_unknown
def	model
def	lower
def	upper
def	__repr__
def	sexpr
def	statistics
Data Fields
	ctx
	optimize

---

Detailed Description

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

Definition at line 6420 of file z3py.py.

---

Constructor & Destructor Documentation

def __init__	(		self,
			ctx = None
	)

Definition at line 6423 of file z3py.py.

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

def __del__

(

self

)

Definition at line 6428 of file z3py.py.

    def __del__(self):
        if self.optimize != None:
            Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)

---

Member Function Documentation

def __repr__

(

self

)

Return a formatted string with all added rules and constraints.

Definition at line 6518 of file z3py.py.

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

def add	(		self,
			args
	)

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

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

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 6460 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
        if not isinstance(weight, str):
            raise Z3Exception("weight should be a string or an integer")
        if id == None:
            id = ""
        id = to_symbol(id, self.ctx)
        v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
        return OptimizeObjective(self, v, False)

def assert_exprs	(		self,
			args
	)

Assert constraints as background axioms for the optimize solver.

Definition at line 6446 of file z3py.py.

Referenced by Optimize.add().

    def assert_exprs(self, *args):
        """Assert constraints as background axioms for the optimize solver."""
        args = _get_args(args)
        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:
                Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())

def check

(

self

)

Check satisfiability while optimizing objective functions.

Definition at line 6493 of file z3py.py.

    def check(self):
        """Check satisfiability while optimizing objective functions."""
        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))

def help

(

self

)

Display a string describing all available options.

Definition at line 6438 of file z3py.py.

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

def lower	(		self,
			obj
	)

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

def maximize	(		self,
			arg
	)

Add objective function to maximize.

Definition at line 6477 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()), True)

def minimize	(		self,
			arg
	)

Add objective function to minimize.

Definition at line 6481 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()), False)

def model

(

self

)

Return a model for the last check().

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

def param_descrs

(

self

)

Return the parameter description set.

Definition at line 6442 of file z3py.py.

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

def pop

(

self

)

restore to previously created backtracking point

Definition at line 6489 of file z3py.py.

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

def push

(

self

)

create a backtracking point for added rules, facts and assertions

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

def reason_unknown

(

self

)

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

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

def set	(		self,
			args,
			keys
	)

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

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

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 6522 of file z3py.py.

Referenced by Optimize.__repr__().

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

def statistics

(

self

)

Return statistics for the last `query()`.

Definition at line 6527 of file z3py.py.

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


        

def upper	(		self,
			obj
	)

Definition at line 6513 of file z3py.py.

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

---

Field Documentation

ctx

Definition at line 6423 of file z3py.py.

Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), ArrayRef::__getitem__(), ApplyResult::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), Optimize::add_soft(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), ApplyResult::as_expr(), QuantifierRef::body(), BoolSortRef::cast(), DatatypeSortRef::constructor(), ApplyResult::convert_model(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), SortRef::kind(), ArrayRef::mk_default(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Optimize::param_descrs(), Tactic::param_descrs(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Optimize::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Optimize::statistics(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

optimize

Definition at line 6423 of file z3py.py.

Referenced by Optimize.__del__(), Optimize.add_soft(), Optimize.assert_exprs(), Optimize.check(), Optimize.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.param_descrs(), Optimize.pop(), Optimize.push(), Optimize.reason_unknown(), Optimize.set(), Optimize.sexpr(), and Optimize.statistics().