mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

update expected

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-04-28 15:54:48 -07:00
parent 97fe2c8609
commit a1928a2438
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/python/z3/z3.py
View file

@ -859,13 +859,14 @@ def RecFunction(name, *sig):
def RecAddDefinition(f, args, body): def RecAddDefinition(f, args, body):
"""Set the body of a recursive function. """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() >>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx) >>> n = Int('n', ctx)
>>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
>>> simplify(fac(5)) >>> simplify(fac(5))
fac(5) 120
>>> s = Solver(ctx=ctx) >>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3) >>> s.add(fac(n) < 3)
>>> s.check() >>> s.check()