From a68dc72b510e67b3aa82189c2c9700e8048ec0ab Mon Sep 17 00:00:00 2001 From: "Hichem R. A." Date: Wed, 24 Jun 2026 14:48:01 +0200 Subject: [PATCH 1/3] Add support for `int.pow2` --- src/lib/frontend/translate.ml | 15 +++++++++++++-- src/lib/reasoners/arith.ml | 7 ++++++- src/lib/reasoners/intervalCalculus.ml | 5 +++++ src/lib/structures/symbols.ml | 11 +++++++---- src/lib/structures/symbols.mli | 1 + tests/arith/int_pow2_sym.expected | 2 ++ tests/arith/int_pow2_sym.smt2 | 4 ++++ 7 files changed, 38 insertions(+), 7 deletions(-) create mode 100644 tests/arith/int_pow2_sym.expected create mode 100644 tests/arith/int_pow2_sym.smt2 diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 20c1b3f73d..61dd6638fa 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -149,6 +149,7 @@ type _ DStd.Builtin.t += Not_theory_constant | Is_theory_constant | Linear_dependency + | Int_pow2 let builtin_term t = Dl.Typer.T.builtin_term t @@ -268,7 +269,7 @@ let ae_fpa_builtins = let a = Var.mk "alpha" in op ~tyvars:[a] "is_theory_constant" Is_theory_constant ([of_var a] ->. prop) in - let fpa_builtins = + let additional_builtins = let open DT in DStd.Id.Map.empty |> add_rounding_modes (* the first argument is mantissas' size (including the implicit bit), the @@ -316,13 +317,15 @@ let ae_fpa_builtins = |> op "integer_log2" Integer_log2 ([real] ->. int) (* only used for arithmetic. It should not be used for x in float(x) to enable computations modulo equality *) + |> op "int.pow2" Int_pow2 ([int] ->. int) + (* computes 2 to the power of a given integer. *) |> op "not_theory_constant" Not_theory_constant ([real] ->. prop) |> is_theory_constant |> op "linear_dependency" Linear_dependency ([real; real] ->. prop) in fun env s -> let search_id id = - try DStd.Id.Map.find_exn id fpa_builtins env s + try DStd.Id.Map.find_exn id additional_builtins env s with Not_found -> `Not_found in match s with @@ -336,6 +339,10 @@ let smt_fpa_builtins = Dl.Typer.T.builtin_term @@ Dolmen_type.Base.term_app2 (module Dl.Typer.T) env s f in + let int_pow2_cst = + let ty = DT.arrow [DT.int] DT.int in + DE.Id.mk ~name:"int.pow2" ~builtin:Int_pow2 (DStd.Path.global "int.pow2") ty + in let other_builtins = DStd.Id.Map.empty |> add_rounding_modes in fun env s -> match s with @@ -359,6 +366,9 @@ let smt_fpa_builtins = term_app env s DE.Term.Int.pow | Id { ns = Term; name = Simple "ae.pow_real" } -> term_app env s DE.Term.Real.pow + | Id { ns = Term; name = Simple "int.pow2" } -> + Dl.Typer.T.builtin_term + @@ Dolmen_type.Base.term_app_cst (module Dl.Typer.T) env int_pow2_cst | Dl.Typer.T.Id id -> begin match DStd.Id.Map.find_exn id other_builtins env s with | e -> e @@ -1211,6 +1221,7 @@ let rec mk_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) | Max_int, _ -> op Max_int | Min_int, _ -> op Min_int | Integer_log2, _ -> op Integer_log2 + | Int_pow2, _ -> op Int_pow2 | Not_theory_constant, _ -> op Not_theory_constant | Is_theory_constant, _ -> op Is_theory_constant | Linear_dependency, _ -> op Linear_dependency diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 8cc6e020c8..18fd8963e5 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -119,7 +119,7 @@ struct ( Plus | Minus | Mult | Div | Modulo | Float | Abs_int | Abs_real | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real | Pow - | Integer_log2 | Int2BV _ | Integer_round ) -> + | Integer_log2 | Int_pow2 | Int2BV _ | Integer_round ) -> true | _ -> false @@ -328,6 +328,11 @@ struct Q.from_int (Fpa_rounding.integer_log_2 q) in mk_partial_interpretation_1 aux_func coef p ty t x, ctx + | Sy.Op Sy.Int_pow2, [x] -> + ( mk_partial_interpretation_1 + (fun x -> calc_power (Q.from_int 2) x ty) + coef p ty t x, + ctx ) | Sy.Op Sy.Pow, [x; y] -> ( mk_partial_interpretation_2 (fun x y -> calc_power x y ty) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index ef6924c042..9bb37469fa 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -677,12 +677,17 @@ let delayed_integer_log2 uf _op = function Some (res, exx)) | _ -> assert false +let delayed_int_pow2 uf _op = function + | [x] -> calc_pow (E.Ints.of_int 2) x Ty.Tint uf + | _ -> assert false + (* These are the partially interpreted functions that we know how to compute. They will be computed immediately if possible, or as soon as we learn the value of their arguments. *) let dispatch = function | Symbols.Pow -> Some delayed_pow | Symbols.Integer_log2 -> Some delayed_integer_log2 + | Symbols.Int_pow2 -> Some delayed_int_pow2 | Symbols.Int_floor -> Some (delayed_op1 ~ty:Tint Numbers.Q.floor) | Symbols.Int_ceil -> Some (delayed_op1 ~ty:Tint Numbers.Q.ceiling) | Symbols.Min_int -> Some (delayed_op2 ~ty:Tint Q.min) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index c7cbd480b2..685965edbe 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,6 +79,7 @@ type operator = | Int_floor | Int_ceil | Integer_log2 + | Int_pow2 | Max_real | Max_int | Min_real @@ -238,10 +239,10 @@ let compare_operators op1 op2 = | Sign_extend _ | Repeat _ | Get | Set | Float | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int - | Integer_log2 | Pow | Integer_round | BVnot | BVand | BVor | BVxor - | BVadd | BVsub | BVmul | BVudiv | BVurem | BVshl | BVlshr | Int2BV _ - | BV2Nat | Not_theory_constant | Is_theory_constant | Linear_dependency - | Constr _ | Destruct _ | Tite ) ) -> + | Integer_log2 | Int_pow2 | Pow | Integer_round | BVnot | BVand | BVor + | BVxor | BVadd | BVsub | BVmul | BVudiv | BVurem | BVshl | BVlshr + | Int2BV _ | BV2Nat | Not_theory_constant | Is_theory_constant + | Linear_dependency | Constr _ | Destruct _ | Tite ) ) -> assert false) let compare_builtin b1 b2 = @@ -372,6 +373,7 @@ module AEPrinter = struct | Min_int -> Fmt.pf ppf "min_int" | Integer_log2 -> Fmt.pf ppf "integer_log2" | Integer_round -> Fmt.pf ppf "integer_round" + | Int_pow2 -> Fmt.pf ppf "int.pow2" (* Reals_Ints theory *) | Abs_int -> Fmt.pf ppf "abs_int" | Abs_real -> Fmt.pf ppf "abs_real" @@ -509,6 +511,7 @@ module SmtPrinter = struct | Min_real -> Fmt.pf ppf "ae.min_real" | Min_int -> Fmt.pf ppf "ae.min_int" | Integer_log2 -> Fmt.pf ppf "ae.integer_log2" + | Int_pow2 -> Fmt.pf ppf "ae.int_pow2" | Integer_round -> Fmt.pf ppf "ae.integer_round" | Pow -> Fmt.pf ppf "ae.pow" end diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index b221a989b3..1618e204d2 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -77,6 +77,7 @@ type operator = | Int_floor | Int_ceil | Integer_log2 + | Int_pow2 | Max_real | Max_int | Min_real diff --git a/tests/arith/int_pow2_sym.expected b/tests/arith/int_pow2_sym.expected new file mode 100644 index 0000000000..6f99ff0f44 --- /dev/null +++ b/tests/arith/int_pow2_sym.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/arith/int_pow2_sym.smt2 b/tests/arith/int_pow2_sym.smt2 new file mode 100644 index 0000000000..41fa81b365 --- /dev/null +++ b/tests/arith/int_pow2_sym.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-const n Int) +(assert (not (= (int.pow2 n) (ae.pow_int 2 n)))) +(check-sat) From 4ba0229ec189ad10bb21ee0521767670b9ff044e Mon Sep 17 00:00:00 2001 From: "Hichem R. A." Date: Mon, 29 Jun 2026 10:57:22 +0200 Subject: [PATCH 2/3] Support `int.pow2 n` by simply rewriting it as `pow 2 n` --- src/lib/frontend/translate.ml | 5 ++++- src/lib/reasoners/arith.ml | 7 +------ src/lib/reasoners/intervalCalculus.ml | 5 ----- src/lib/structures/symbols.ml | 11 ++++------- src/lib/structures/symbols.mli | 1 - 5 files changed, 9 insertions(+), 20 deletions(-) diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml index 61dd6638fa..b9a064e8e9 100644 --- a/src/lib/frontend/translate.ml +++ b/src/lib/frontend/translate.ml @@ -1221,7 +1221,10 @@ let rec mk_expr ?(loc = Loc.dummy) ?(name_base = "") ?(toplevel = false) | Max_int, _ -> op Max_int | Min_int, _ -> op Min_int | Integer_log2, _ -> op Integer_log2 - | Int_pow2, _ -> op Int_pow2 + | Int_pow2, [n] -> + E.mk_term (Sy.Op Sy.Pow) + [E.Ints.of_int 2; aux_mk_expr n] + (dty_to_ty term_ty) | Not_theory_constant, _ -> op Not_theory_constant | Is_theory_constant, _ -> op Is_theory_constant | Linear_dependency, _ -> op Linear_dependency diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 18fd8963e5..8cc6e020c8 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -119,7 +119,7 @@ struct ( Plus | Minus | Mult | Div | Modulo | Float | Abs_int | Abs_real | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real | Pow - | Integer_log2 | Int_pow2 | Int2BV _ | Integer_round ) -> + | Integer_log2 | Int2BV _ | Integer_round ) -> true | _ -> false @@ -328,11 +328,6 @@ struct Q.from_int (Fpa_rounding.integer_log_2 q) in mk_partial_interpretation_1 aux_func coef p ty t x, ctx - | Sy.Op Sy.Int_pow2, [x] -> - ( mk_partial_interpretation_1 - (fun x -> calc_power (Q.from_int 2) x ty) - coef p ty t x, - ctx ) | Sy.Op Sy.Pow, [x; y] -> ( mk_partial_interpretation_2 (fun x y -> calc_power x y ty) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 9bb37469fa..ef6924c042 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -677,17 +677,12 @@ let delayed_integer_log2 uf _op = function Some (res, exx)) | _ -> assert false -let delayed_int_pow2 uf _op = function - | [x] -> calc_pow (E.Ints.of_int 2) x Ty.Tint uf - | _ -> assert false - (* These are the partially interpreted functions that we know how to compute. They will be computed immediately if possible, or as soon as we learn the value of their arguments. *) let dispatch = function | Symbols.Pow -> Some delayed_pow | Symbols.Integer_log2 -> Some delayed_integer_log2 - | Symbols.Int_pow2 -> Some delayed_int_pow2 | Symbols.Int_floor -> Some (delayed_op1 ~ty:Tint Numbers.Q.floor) | Symbols.Int_ceil -> Some (delayed_op1 ~ty:Tint Numbers.Q.ceiling) | Symbols.Min_int -> Some (delayed_op2 ~ty:Tint Q.min) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 685965edbe..c7cbd480b2 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -79,7 +79,6 @@ type operator = | Int_floor | Int_ceil | Integer_log2 - | Int_pow2 | Max_real | Max_int | Min_real @@ -239,10 +238,10 @@ let compare_operators op1 op2 = | Sign_extend _ | Repeat _ | Get | Set | Float | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int - | Integer_log2 | Int_pow2 | Pow | Integer_round | BVnot | BVand | BVor - | BVxor | BVadd | BVsub | BVmul | BVudiv | BVurem | BVshl | BVlshr - | Int2BV _ | BV2Nat | Not_theory_constant | Is_theory_constant - | Linear_dependency | Constr _ | Destruct _ | Tite ) ) -> + | Integer_log2 | Pow | Integer_round | BVnot | BVand | BVor | BVxor + | BVadd | BVsub | BVmul | BVudiv | BVurem | BVshl | BVlshr | Int2BV _ + | BV2Nat | Not_theory_constant | Is_theory_constant | Linear_dependency + | Constr _ | Destruct _ | Tite ) ) -> assert false) let compare_builtin b1 b2 = @@ -373,7 +372,6 @@ module AEPrinter = struct | Min_int -> Fmt.pf ppf "min_int" | Integer_log2 -> Fmt.pf ppf "integer_log2" | Integer_round -> Fmt.pf ppf "integer_round" - | Int_pow2 -> Fmt.pf ppf "int.pow2" (* Reals_Ints theory *) | Abs_int -> Fmt.pf ppf "abs_int" | Abs_real -> Fmt.pf ppf "abs_real" @@ -511,7 +509,6 @@ module SmtPrinter = struct | Min_real -> Fmt.pf ppf "ae.min_real" | Min_int -> Fmt.pf ppf "ae.min_int" | Integer_log2 -> Fmt.pf ppf "ae.integer_log2" - | Int_pow2 -> Fmt.pf ppf "ae.int_pow2" | Integer_round -> Fmt.pf ppf "ae.integer_round" | Pow -> Fmt.pf ppf "ae.pow" end diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 1618e204d2..b221a989b3 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -77,7 +77,6 @@ type operator = | Int_floor | Int_ceil | Integer_log2 - | Int_pow2 | Max_real | Max_int | Min_real From 39532bbf493b9846027a851742e6d61e19b465f8 Mon Sep 17 00:00:00 2001 From: "Hichem R. A." Date: Tue, 30 Jun 2026 14:05:04 +0200 Subject: [PATCH 3/3] Update Changes.md --- CHANGES.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index eaa355eef5..8ff9fe7cf5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,10 @@ ## unreleased + - Support the `int.pow2` function, which takes an integer `n` and computes + `ae.pow_int 2 n` (#1365) - Support parsing of SMT-LIB FPA Theory literals and add the theory `smt.float` - that enables thte support for the SMT-LIB FPA, and that can be used with the - cmdline option `--enable-theory smt.float` (#1358) + that enables the support for the SMT-LIB FPA Theory, and that can be used + with the cmdline option `--enable-theory smt.float` (#1358) - Bump minimal cmdliner version to 2.0 (#1340) ## v2.6.2