mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 01:32:17 +00:00
Code Activity

fix implication order of projection

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-21 09:15:27 -07:00
parent b85a60de5c
commit 8f2ffb3b04
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/synth_solver.h
View file

@ -39,12 +39,12 @@ Example setting:
- f(x,y): - f(x,y):
- Set x, y, f to shared, - Set x, y, f to shared,
- u, z g are not shared - u, z g are not shared
- Phi1[x,y,f(x,y)] := Project u, z, g from Phi - Phi1[x,y,f(x,y)] := Project u, z, g from Phi, such that Phi => Phi1
- Set x, y to shared - Set x, y to shared
- realizer t[x,y] := Project f(x,y) from Phi1 - realizer t[x,y] := Project f(x,y) from Phi1
- g(x,z): - g(x,z):
- set x, z, g to shared - set x, z, g to shared
- Phi2 := Project u, y, f from Phi - Phi2 := Project u, y, f from Phi, such that Phi => Phi2
- Set x, z to shared - Set x, z to shared
- realizer s[x,z] := Project g(x, z) from Phi2 - realizer s[x,z] := Project g(x, z) from Phi2
- Let Theta1, Theta2 be such that - Let Theta1, Theta2 be such that