Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

I was wonering about the status of the rewrite/substitution discussed in this thread. #6059

Closed
jparsert opened this issue May 30, 2022 · 3 comments

Comments

@jparsert
Copy link
Contributor

jparsert commented May 30, 2022

Leo de Moura presented a nice implementation of a rewrite
here. Supposedly an addition to the API was discussed in the responses but it is not clear to me whether it ended up being implemented.

NikolajBjorner added a commit that referenced this issue May 30, 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

from z3 import *

def rewrite(t, f, g):
    return substitute_funs(t, [(f, g)])
    
f = Function('f', IntSort(), IntSort())
a, b = Ints('a b')
s = Or(f(a) == 0, f(a) == 1, f(a+a) == 2)
# Example 1: replace all f-applications with b
print(rewrite(s, f, b))

# Example 2: replace all f-applications f(t) with g(t+1)
g = Function('g', IntSort(), IntSort())
x = Var(0, IntSort())
print(rewrite(s, f, g(x + 1)))

# Now, f and g are binary functions.
f = Function('f', IntSort(), IntSort(), IntSort())
g = Function('g', IntSort(), IntSort(), IntSort())

# Example 3: replace all f-applications f(t1, t2) with g(t2, t1)
s = Or(f(a, f(a, b)) == 0, f(b, a) == 1, f(f(1,0), 0) == 2)
# The first argument is variable 0, and the second is variable 1.
y = Var(1, IntSort())
print (rewrite(s, f, g(y, x)))

# Example 4: quantifiers
s = ForAll([a], f(a, b) >= 0)
print (rewrite(s, f, g(y, x + 1)))

@NikolajBjorner
Copy link
Contributor

added

@jparsert
Copy link
Contributor Author

jparsert commented Dec 9, 2022

Is it possible to add this to the c++ API as well?

NikolajBjorner added a commit that referenced this issue Dec 9, 2022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants