GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Update solver definitions related to /^ and %^.

Browse Source
This commit is contained in:
Rob Dockins 2021-06-30 13:18:12 -07:00
parent acb3ca9fae
commit b3c4317784
1 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
lib/CryptolTC.z3
View File

@ -293,15 +293,19 @@
)
(define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat
(ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
(ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y)))))
)
(ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
(ite (= (value y) 0) cryErr
(ite (not (isFin x)) cryInf
(cryNat (- (div (- (value x)) (value y))))
)))
)
(define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat
(ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
(ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y))))
)
(ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
(ite (= (value y) 0) cryErr
(ite (not (isFin x)) (cryNat 0)
(cryNat (mod (- (value x)) (value y)))
)))
)
(define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat