Skip to content

Commit

Permalink
CryptolTC.z3: Don't bother defining a prime table
Browse files Browse the repository at this point in the history
`prime` is usually called on large primes, so it's not worth the effort of
defining a lookup table for small prime numbers. Either way, this is unlikely
to have a noticeable effect on performance.
  • Loading branch information
RyanGlScott committed Nov 27, 2024
1 parent bcf5672 commit f8dffb9
Showing 1 changed file with 1 addition and 9 deletions.
10 changes: 1 addition & 9 deletions lib/CryptolTC.z3
Original file line number Diff line number Diff line change
Expand Up @@ -78,17 +78,9 @@

(declare-fun cryPrimeUnknown (Int) Bool)

(define-fun cryPrimeTable ((x Int)) Bool
(or (= x 2)
(or (= x 3)
(or (= x 5)
(or (= x 7)
(cryPrimeUnknown x)))))
)

(define-fun cryPrime ((x InfNat)) MaybeBool
(ite (isErr x) cryErrProp
(cryBool (and (isFin x) (cryPrimeTable (value x)))))
(cryBool (and (isFin x) (cryPrimeUnknown (value x)))))
)


Expand Down

0 comments on commit f8dffb9

Please sign in to comment.