Skip to content

Commit

Permalink
update expected
Browse files Browse the repository at this point in the history
  • Loading branch information
NikolajBjorner committed Apr 28, 2020
1 parent 97fe2c8 commit a1928a2
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/api/python/z3/z3.py
Original file line number Diff line number Diff line change
Expand Up @@ -859,13 +859,14 @@ def RecFunction(name, *sig):

def RecAddDefinition(f, args, body):
"""Set the body of a recursive function.
Recursive definitions are only unfolded during search.
Recursive definitions can be simplified if they are applied to ground
arguments.
>>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx)
>>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
>>> simplify(fac(5))
fac(5)
120
>>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3)
>>> s.check()
Expand Down

0 comments on commit a1928a2

Please sign in to comment.