Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
Goal Class Reference
+ Inheritance diagram for Goal:

Public Member Functions

def __init__
def __del__
def depth
def inconsistent
def prec
def precision
def size
def __len__
def get
def __getitem__
def assert_exprs
def append
def insert
def add
def __repr__
def sexpr
def translate
def simplify
def as_expr

Data Fields

 ctx
 goal

Detailed Description

Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).

Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals.
A goal has a solution if one of its subgoals has a solution.
A goal is unsatisfiable if all subgoals are unsatisfiable.

Definition at line 4536 of file z3py.py.


Constructor & Destructor Documentation

def __init__ (   self,
  models = True,
  unsat_cores = False,
  proofs = False,
  ctx = None,
  goal = None 
)

Definition at line 4544 of file z3py.py.

04544 
04545     def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
04546         if __debug__:
04547             _z3_assert(goal == None or ctx != None, "If goal is different from None, then ctx must be also different from None")
04548         self.ctx    = _get_ctx(ctx)
04549         self.goal   = goal
04550         if self.goal == None:
04551             self.goal   = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
04552         Z3_goal_inc_ref(self.ctx.ref(), self.goal)

def __del__ (   self)

Definition at line 4553 of file z3py.py.

04553 
04554     def __del__(self):
04555         if self.goal != None:
04556             Z3_goal_dec_ref(self.ctx.ref(), self.goal)


Member Function Documentation

def __getitem__ (   self,
  arg 
)
Return a constraint in the goal `self`.

>>> g = Goal()
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g[0]
x == 0
>>> g[1]
y > x

Definition at line 4661 of file z3py.py.

04661 
04662     def __getitem__(self, arg):
04663         """Return a constraint in the goal `self`.
04664         
04665         >>> g = Goal()
04666         >>> x, y = Ints('x y')
04667         >>> g.add(x == 0, y > x)
04668         >>> g[0]
04669         x == 0
04670         >>> g[1]
04671         y > x
04672         """
04673         if arg >= len(self):
04674             raise IndexError
04675         return self.get(arg)

def __len__ (   self)
Return the number of constraints in the goal `self`.

>>> g = Goal()
>>> len(g)
0
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> len(g)
2

Definition at line 4635 of file z3py.py.

04635 
04636     def __len__(self):
04637         """Return the number of constraints in the goal `self`.
04638 
04639         >>> g = Goal()
04640         >>> len(g)
04641         0
04642         >>> x, y = Ints('x y')
04643         >>> g.add(x == 0, y > x)
04644         >>> len(g)
04645         2
04646         """
04647         return self.size()

def __repr__ (   self)

Definition at line 4724 of file z3py.py.

04724 
04725     def __repr__(self):
04726         return obj_to_string(self)

def add (   self,
  args 
)
Add constraints.

>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 0, x < 2)
>>> g
[x > 0, x < 2]

Definition at line 4713 of file z3py.py.

04713 
04714     def add(self, *args):
04715         """Add constraints.
04716         
04717         >>> x = Int('x')
04718         >>> g = Goal()
04719         >>> g.add(x > 0, x < 2)
04720         >>> g
04721         [x > 0, x < 2]
04722         """
04723         self.assert_exprs(*args)

def append (   self,
  args 
)
Add constraints.

>>> x = Int('x')
>>> g = Goal()
>>> g.append(x > 0, x < 2)
>>> g
[x > 0, x < 2]

Definition at line 4691 of file z3py.py.

04691 
04692     def append(self, *args):
04693         """Add constraints.
04694         
04695         >>> x = Int('x')
04696         >>> g = Goal()
04697         >>> g.append(x > 0, x < 2)
04698         >>> g
04699         [x > 0, x < 2]
04700         """
04701         self.assert_exprs(*args)
        
def as_expr (   self)
Return goal `self` as a single Z3 expression.

>>> x = Int('x')
>>> g = Goal()
>>> g.as_expr()
True
>>> g.add(x > 1)
>>> g.as_expr()
x > 1
>>> g.add(x < 10)
>>> g.as_expr()
And(x > 1, x < 10)

Definition at line 4774 of file z3py.py.

04774 
04775     def as_expr(self):
04776         """Return goal `self` as a single Z3 expression.
04777         
04778         >>> x = Int('x')
04779         >>> g = Goal()
04780         >>> g.as_expr()
04781         True
04782         >>> g.add(x > 1)
04783         >>> g.as_expr()
04784         x > 1
04785         >>> g.add(x < 10)
04786         >>> g.as_expr()
04787         And(x > 1, x < 10)
04788         """
04789         sz = len(self)
04790         if sz == 0:
04791             return BoolVal(True, self.ctx)
04792         elif sz == 1:
04793             return self.get(0)
04794         else:
04795             return And([ self.get(i) for i in range(len(self)) ])

def assert_exprs (   self,
  args 
)
Assert constraints into the goal.

>>> x = Int('x')
>>> g = Goal()
>>> g.assert_exprs(x > 0, x < 2)
>>> g
[x > 0, x < 2]

Definition at line 4676 of file z3py.py.

Referenced by Goal.add(), Fixedpoint.add(), Goal.append(), Fixedpoint.append(), and Fixedpoint.insert().

04676 
04677     def assert_exprs(self, *args):
04678         """Assert constraints into the goal.
04679         
04680         >>> x = Int('x')
04681         >>> g = Goal()
04682         >>> g.assert_exprs(x > 0, x < 2)
04683         >>> g
04684         [x > 0, x < 2]
04685         """
04686         args = _get_args(args)
04687         s    = BoolSort(self.ctx)
04688         for arg in args:
04689             arg = s.cast(arg)
04690             Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())

def depth (   self)
Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.

>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x == 0, y >= x + 1)
>>> g.depth()
0
>>> r = Then('simplify', 'solve-eqs')(g)
>>> # r has 1 subgoal
>>> len(r)
1
>>> r[0].depth()
2

Definition at line 4557 of file z3py.py.

04557 
04558     def depth(self):
04559         """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
04560 
04561         >>> x, y = Ints('x y')
04562         >>> g = Goal()
04563         >>> g.add(x == 0, y >= x + 1)
04564         >>> g.depth()
04565         0
04566         >>> r = Then('simplify', 'solve-eqs')(g)
04567         >>> # r has 1 subgoal
04568         >>> len(r)
04569         1
04570         >>> r[0].depth()
04571         2
04572         """
04573         return int(Z3_goal_depth(self.ctx.ref(), self.goal))

def get (   self,
  i 
)
Return a constraint in the goal `self`.

>>> g = Goal()
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g.get(0)
x == 0
>>> g.get(1)
y > x

Definition at line 4648 of file z3py.py.

Referenced by Goal.__getitem__(), and Goal.as_expr().

04648 
04649     def get(self, i):
04650         """Return a constraint in the goal `self`.
04651         
04652         >>> g = Goal()
04653         >>> x, y = Ints('x y')
04654         >>> g.add(x == 0, y > x)
04655         >>> g.get(0)
04656         x == 0
04657         >>> g.get(1)
04658         y > x
04659         """
04660         return _to_expr_ref(Z3_goal_formula(self.ctx.ref(), self.goal, i), self.ctx)

def inconsistent (   self)
Return `True` if `self` contains the `False` constraints.

>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.inconsistent()
False
>>> g.add(x == 0, x == 1)
>>> g 
[x == 0, x == 1]
>>> g.inconsistent()
False
>>> g2 = Tactic('propagate-values')(g)[0]
>>> g2.inconsistent()
True

Definition at line 4574 of file z3py.py.

04574 
04575     def inconsistent(self):
04576         """Return `True` if `self` contains the `False` constraints.
04577         
04578         >>> x, y = Ints('x y')
04579         >>> g = Goal()
04580         >>> g.inconsistent()
04581         False
04582         >>> g.add(x == 0, x == 1)
04583         >>> g 
04584         [x == 0, x == 1]
04585         >>> g.inconsistent()
04586         False
04587         >>> g2 = Tactic('propagate-values')(g)[0]
04588         >>> g2.inconsistent()
04589         True
04590         """
04591         return Z3_goal_inconsistent(self.ctx.ref(), self.goal)

def insert (   self,
  args 
)
Add constraints.

>>> x = Int('x')
>>> g = Goal()
>>> g.insert(x > 0, x < 2)
>>> g
[x > 0, x < 2]

Definition at line 4702 of file z3py.py.

04702 
04703     def insert(self, *args):
04704         """Add constraints.
04705         
04706         >>> x = Int('x')
04707         >>> g = Goal()
04708         >>> g.insert(x > 0, x < 2)
04709         >>> g
04710         [x > 0, x < 2]
04711         """
04712         self.assert_exprs(*args)

def prec (   self)
Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.

>>> g = Goal()
>>> g.prec() == Z3_GOAL_PRECISE
True
>>> x, y = Ints('x y')
>>> g.add(x == y + 1)
>>> g.prec() == Z3_GOAL_PRECISE
True
>>> t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
>>> g2 = t(g)[0]
>>> g2
[x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
>>> g2.prec() == Z3_GOAL_PRECISE
False
>>> g2.prec() == Z3_GOAL_UNDER
True

Definition at line 4592 of file z3py.py.

Referenced by Goal.precision().

04592 
04593     def prec(self):
04594         """Return the precision (under-approximation, over-approximation, or precise) of the goal `self`.
04595         
04596         >>> g = Goal()
04597         >>> g.prec() == Z3_GOAL_PRECISE
04598         True
04599         >>> x, y = Ints('x y')
04600         >>> g.add(x == y + 1)
04601         >>> g.prec() == Z3_GOAL_PRECISE
04602         True
04603         >>> t  = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10)
04604         >>> g2 = t(g)[0]
04605         >>> g2
04606         [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0]
04607         >>> g2.prec() == Z3_GOAL_PRECISE
04608         False
04609         >>> g2.prec() == Z3_GOAL_UNDER
04610         True
04611         """
04612         return Z3_goal_precision(self.ctx.ref(), self.goal)

def precision (   self)
Alias for `prec()`.

>>> g = Goal()
>>> g.precision() == Z3_GOAL_PRECISE
True

Definition at line 4613 of file z3py.py.

04613 
04614     def precision(self):
04615         """Alias for `prec()`.
04616 
04617         >>> g = Goal()
04618         >>> g.precision() == Z3_GOAL_PRECISE
04619         True
04620         """
04621         return self.prec()

def sexpr (   self)
Return a textual representation of the s-expression representing the goal.

Definition at line 4727 of file z3py.py.

Referenced by Fixedpoint.__repr__().

04727 
04728     def sexpr(self):
04729         """Return a textual representation of the s-expression representing the goal."""
04730         return Z3_goal_to_string(self.ctx.ref(), self.goal)

def simplify (   self,
  arguments,
  keywords 
)
Return a new simplified goal.

This method is essentially invoking the simplify tactic.

>>> g = Goal()
>>> x = Int('x')
>>> g.add(x + 1 >= 2)
>>> g
[x + 1 >= 2]
>>> g2 = g.simplify()
>>> g2
[x >= 1]
>>> # g was not modified
>>> g
[x + 1 >= 2]

Definition at line 4754 of file z3py.py.

04754 
04755     def simplify(self, *arguments, **keywords):
04756         """Return a new simplified goal.
04757         
04758         This method is essentially invoking the simplify tactic.
04759         
04760         >>> g = Goal()
04761         >>> x = Int('x')
04762         >>> g.add(x + 1 >= 2)
04763         >>> g
04764         [x + 1 >= 2]
04765         >>> g2 = g.simplify()
04766         >>> g2
04767         [x >= 1]
04768         >>> # g was not modified
04769         >>> g
04770         [x + 1 >= 2]
04771         """
04772         t = Tactic('simplify')
04773         return t.apply(self, *arguments, **keywords)[0]

def size (   self)
Return the number of constraints in the goal `self`.

>>> g = Goal()
>>> g.size()
0
>>> x, y = Ints('x y')
>>> g.add(x == 0, y > x)
>>> g.size()
2

Definition at line 4622 of file z3py.py.

Referenced by Goal.__len__(), and BitVecNumRef.as_signed_long().

04622 
04623     def size(self):
04624         """Return the number of constraints in the goal `self`.
04625         
04626         >>> g = Goal()
04627         >>> g.size()
04628         0
04629         >>> x, y = Ints('x y')
04630         >>> g.add(x == 0, y > x)
04631         >>> g.size()
04632         2
04633         """
04634         return int(Z3_goal_size(self.ctx.ref(), self.goal))

def translate (   self,
  target 
)
Copy goal `self` to context `target`.

>>> x = Int('x')
>>> g = Goal()
>>> g.add(x > 10)
>>> g
[x > 10]
>>> c2 = Context()
>>> g2 = g.translate(c2)
>>> g2
[x > 10]
>>> g.ctx == main_ctx()
True
>>> g2.ctx == c2
True
>>> g2.ctx == main_ctx()
False

Definition at line 4731 of file z3py.py.

04731 
04732     def translate(self, target):
04733         """Copy goal `self` to context `target`.
04734         
04735         >>> x = Int('x')
04736         >>> g = Goal()
04737         >>> g.add(x > 10)
04738         >>> g
04739         [x > 10]
04740         >>> c2 = Context()
04741         >>> g2 = g.translate(c2)
04742         >>> g2
04743         [x > 10]
04744         >>> g.ctx == main_ctx()
04745         True
04746         >>> g2.ctx == c2
04747         True
04748         >>> g2.ctx == main_ctx()
04749         False
04750         """
04751         if __debug__:
04752             _z3_assert(isinstance(target, Context), "target must be a context")
04753         return Goal(goal=Z3_goal_translate(self.ctx.ref(), self.goal, target.ref()), ctx=target)


Field Documentation

ctx

Definition at line 4544 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(), Fixedpoint::add_rule(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), Goal::as_expr(), ApplyResult::as_expr(), Goal::assert_exprs(), Fixedpoint::assert_exprs(), QuantifierRef::body(), BoolSortRef::cast(), DatatypeSortRef::constructor(), ApplyResult::convert_model(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), Goal::get(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_rules(), SortRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Fixedpoint::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Fixedpoint::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Fixedpoint::statistics(), Solver::to_smt2(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines