SMT-LIB Proposal: Integer Arithmetic with Exponentials
24 views
Skip to first unread message
Florian Frohn
Nov 20, 2025, 4:31:15 AM11/20/25
to SMT-LIB
Dear all,
I attached a proposal for integrating exponentiation into the Ints theory. In a nutshell, the proposal is to introduce a new function
(** Int Int Int)
with the following semantics:
- (** x y) = x^y if y >= 0
- (** x y) = 1 div x^(-y) if y < 0
All the details are in the attached PDF, and there's also a corresponding issue on GitHub.
If you're interested, please comment, ideally before Christmas. The goal is to stabilize the proposal by the end of the year.
Best
Florian
I attached a proposal for integrating exponentiation into the Ints theory. In a nutshell, the proposal is to introduce a new function
(** Int Int Int)
with the following semantics:
- (** x y) = x^y if y >= 0
- (** x y) = 1 div x^(-y) if y < 0
All the details are in the attached PDF, and there's also a corresponding issue on GitHub.
If you're interested, please comment, ideally before Christmas. The goal is to stabilize the proposal by the end of the year.
Best
Florian
Reply all
Reply to author
Forward
0 new messages