Fixed exponentation symbol for SMT

m^n is specified for m,n:int iff m # 0 OR n > 0 The operator has no counterpart in SMT, and no axiom is provided for reasoning, but at least we cannot prove statements like 0^(-1) \in Int.
ahelwer · Jan 26, 2024 · 035c39d · 035c39d
1 parent ac759fa
commit 035c39d
Show file tree

Hide file tree

Showing 9 changed files with 53 additions and 25 deletions.
diff --git a/src/encode.mli b/src/encode.mli
@@ -83,7 +83,7 @@ module Table : sig
     | TIntTimes
     | TIntQuotient
     | TIntRemainder
-    | TIntExp
+    (*| TIntExp*)
     | TIntLteq
     | TIntLt
     | TIntGteq

diff --git a/src/encode/n_axioms.ml b/src/encode/n_axioms.ml
@@ -2435,7 +2435,7 @@ let inttimes_typing () =
     ] %% []
   ) %% []
 
-let intexp_typing () =
+let intexp_typing ~noarith =
   quant Forall
   [ "x" ; "y" ] [ t_idv ; t_idv ]
   ~pats:[ [
@@ -2450,14 +2450,38 @@ let intexp_typing () =
         [ Ix 2 %% []
         ; apps T.IntSet [] %% []
         ] %% []
-      ; appb ~tys:[ t_idv ] B.Neq
-        [ Ix 2 %% []
-        ; apps (T.IntLit 0) [] %% []
-        ] %% []
       ; apps T.Mem
         [ Ix 1 %% []
         ; apps T.IntSet [] %% []
         ] %% []
+      ; begin
+        if noarith then
+          appb B.Disj
+          [ appb ~tys:[ t_idv ] B.Neq
+            [ Ix 2 %% []
+            ; apps (T.IntLit 0) [] %% []
+            ] %% []
+          ; apps T.IntLteq
+            [ apps (T.IntLit 1) [] %% []
+            ; Ix 1 %% []
+            ] %% []
+          ] %% []
+        else
+          appb B.Disj
+          [ appb ~tys:[ t_idv ] B.Neq
+            [ Ix 2 %% []
+            ; apps (T.Cast t_int)
+              [ apps (T.TIntLit 0) [] %% []
+              ] %% []
+            ] %% []
+          ; apps T.IntLteq
+            [ apps (T.Cast t_int)
+              [ apps (T.TIntLit 1) [] %% []
+              ] %% []
+            ; Ix 1 %% []
+            ] %% []
+          ] %% []
+        end
       ]) %% []
     ; apps T.Mem
       [ apps T.IntExp
@@ -4942,7 +4966,7 @@ let get_axm ~solver tla_smb =
   | T.IntTimesTyping -> inttimes_typing ()
   | T.IntQuotientTyping -> intquotient_typing ()
   | T.IntRemainderTyping -> intremainder_typing ()
-  | T.IntExpTyping -> intexp_typing ()
+  | T.IntExpTyping -> intexp_typing ~noarith
   | T.NatPlusTyping -> natplus_typing ()
   | T.NatTimesTyping -> nattimes_typing ()
   | T.IntRangeDef -> intrange_def ()

diff --git a/src/encode/n_axioms.mli b/src/encode/n_axioms.mli
@@ -133,7 +133,7 @@ val intminus_typing : unit -> expr
 val inttimes_typing : unit -> expr
 val intquotient_typing : unit -> expr
 val intremainder_typing : unit -> expr
-val intexp_typing : unit -> expr
+val intexp_typing : noarith:bool -> expr
 val natplus_typing : unit -> expr
 val nattimes_typing : unit -> expr
 

diff --git a/src/encode/n_data.ml b/src/encode/n_data.ml
@@ -209,9 +209,9 @@ let typed_data tla_smb =
   | TIntRemainder ->
       ("TIntRemainder", [ t_cst t_int ; t_cst t_int ],        t_int,
       IntRemainder)
-  | TIntExp ->
+  (*| TIntExp ->
       ("TIntExp",       [ t_cst t_int ; t_cst t_int ],        t_int,
-      IntExp)
+      IntExp)*)
   | TIntLteq ->
       ("TIntLteq",      [ t_cst t_int ; t_cst t_int ],        t_bol,
       IntLteq)
@@ -315,7 +315,7 @@ let get_data tla_smb =
       ; dat_tver = None
       }
   | TIntLit _ | TIntPlus | TIntUminus | TIntMinus | TIntTimes | TIntQuotient
-  | TIntRemainder | TIntExp | TIntLteq | TIntLt | TIntGteq | TIntGt | TFSCard _
+  | TIntRemainder (*| TIntExp*) | TIntLteq | TIntLt | TIntGteq | TIntGt | TFSCard _
   | TFSMem _ | TFSSubseteq _ | TFSEmpty _ | TFSSingleton _ | TFSAdd _ | TFSCup _
   | TFSCap _ | TFSSetminus _ ->
       let (nm, tins, tout, tver) = typed_data tla_smb in
@@ -475,7 +475,8 @@ let untyped_deps ~solver tla_smb s =
       ([ Mem ; IntSet ; NatSet ; IntLteq ; IntLit 0 ; IntLit 1 ;
           IntRange ; IntMinus ],              [ IntRemainderTyping ])
   | IntExp when noarith ->
-      ([ Mem ; IntSet ; IntLit 0 ],           [ IntExpTyping ])
+      ([ Mem ; IntSet ; IntLteq ; IntLit 0 ; IntLit 1 ],
+                                              [ IntExpTyping ])
   | IntLteq | IntLt | IntGteq | IntGt when noarith ->
       ([ Mem ; IntSet ],                      [ LteqReflexive ; LteqTransitive ; LteqAntisym ])
   | IntPlus ->
@@ -491,7 +492,10 @@ let untyped_deps ~solver tla_smb s =
   | IntRemainder ->
       ([ Cast (TAtm TAInt) ; TIntRemainder ], [ Typing TIntRemainder ])
   | IntExp ->
-      ([ Cast (TAtm TAInt) ; TIntExp ],       [ Typing TIntExp ])
+      (* NOTE SMT has no symbol for exponentiation *)
+      (*([ Cast (TAtm TAInt) ; TIntExp ],       [ Typing TIntExp ])*)
+      ([ Mem ; IntSet ; Cast (TAtm TAInt) ; TIntLteq ; TIntLit 0 ; TIntLit 1 ],
+                                              [ IntExpTyping ])
   | IntLteq ->
       ([ Cast (TAtm TAInt) ; TIntLteq ],      [ Typing TIntLteq ])
   | IntLt ->
@@ -636,8 +640,8 @@ let typed_deps tla_smb s =
       ([ IntQuotient ],                       [])
   | TIntRemainder ->
       ([ IntRemainder ],                      [])
-  | TIntExp ->
-      ([ IntExp ],                            [])
+  (*| TIntExp ->
+      ([ IntExp ],                            [])*)
   (* NOTE Best to declare only Lteq and not the four variants *)
   | TIntLteq ->
       ([ IntLteq ],                           [ Typing TIntLteq ])
@@ -700,7 +704,7 @@ let get_deps ~solver tla_smb s =
       ; dat_axms = axms
       }
   | TIntLit _ | TIntPlus | TIntUminus | TIntMinus | TIntTimes | TIntQuotient
-  | TIntRemainder | TIntExp | TIntLteq | TIntLt | TIntGteq | TIntGt
+  | TIntRemainder (*| TIntExp*) | TIntLteq | TIntLt | TIntGteq | TIntGt
   | TFSCard _ | TFSMem _ | TFSSubseteq _ | TFSEmpty _ | TFSSingleton _
   | TFSAdd _ | TFSCup _ | TFSCap _ | TFSSetminus _ ->
 

diff --git a/src/encode/n_standardize.ml b/src/encode/n_standardize.ml
@@ -150,7 +150,7 @@ let visitor = object (self : 'self)
           | Uminus,     Some [ TAtm TAInt ]   -> TIntUminus
           | Minus,      Some [ TAtm TAInt ]   -> TIntMinus
           | Times,      Some [ TAtm TAInt ]   -> TIntTimes
-          | Exp,        Some [ TAtm TAInt ]   -> TIntExp
+          (*| Exp,        Some [ TAtm TAInt ]   -> TIntExp*)
           | Quotient,   Some [ ]              -> TIntQuotient
           | Remainder,  Some [ ]              -> TIntRemainder
           | Lteq,       Some [ TAtm TAInt ]   -> TIntLteq

diff --git a/src/encode/n_table.ml b/src/encode/n_table.ml
@@ -82,7 +82,7 @@ type tla_smb =
   | TIntTimes
   | TIntQuotient
   | TIntRemainder
-  | TIntExp
+  (*| TIntExp*)
   | TIntLteq
   | TIntLt
   | TIntGteq
@@ -296,7 +296,7 @@ let tla_smb_desc = function
   | TIntTimes -> "TIntTimes"
   | TIntQuotient -> "TIntQuotient"
   | TIntRemainder -> "TIntRemainder"
-  | TIntExp -> "TIntExp"
+  (*| TIntExp -> "TIntExp"*)
   | TIntLteq -> "TIntLteq"
   | TIntLt -> "TIntLt"
   | TIntGteq -> "TIntGteq"

diff --git a/src/encode/n_table.mli b/src/encode/n_table.mli
@@ -101,7 +101,7 @@ type tla_smb =
   | TIntTimes
   | TIntQuotient
   | TIntRemainder
-  | TIntExp
+  (*| TIntExp*) (* disabled; no ^ in SMT-LIB *)
   | TIntLteq
   | TIntLt
   | TIntGteq

diff --git a/src/type/t_synth.ml b/src/type/t_synth.ml
@@ -1087,7 +1087,7 @@ and expr_aux scx oe =
       let ret = Internal B.Infinity @@ oe in
       (ret, TAtm TAIdv)
 
-  | Apply ({ core = Internal (B.Plus | B.Minus | B.Times | B.Exp) } as op, [ e ; f ]) ->
+  | Apply ({ core = Internal (B.Plus | B.Minus | B.Times) } as op, [ e ; f ]) ->
       let e, ty01 = expr scx e in
       let f, ty02 = expr scx f in
       begin match ty01, ty02 with
@@ -1120,11 +1120,11 @@ and expr_aux scx oe =
           (ret, TAtm TAIdv)
       end
 
-  | Apply ({ core = Internal (B.Quotient | B.Remainder) } as op, [ e ; f ]) ->
+  | Apply ({ core = Internal (B.Exp | B.Quotient | B.Remainder) } as op, [ e ; f ]) ->
       let e, ty01 = expr scx e in
       let f, ty02 = expr scx f in
       begin match ty01, ty02 with
-      (* FIXME disabled because unsound: Quotient and Remainder expect second arg to be > 0 *)
+      (* FIXME Check conditions for when Exp, Quotient and Remainder are specified in TLA+ *)
       (*| TAtm TAInt, TAtm TAInt when typelvl scx > 1 ->
           let op = assign op Props.tpars_prop [ ] in
           let ret = Apply (op, [ e ; f ]) @@ oe in

diff --git a/test/unit/e_arith/typingexp_test.tla b/test/unit/e_arith/typingexp_test.tla
@@ -3,8 +3,8 @@
 EXTENDS TLAPS, Integers
 
 THEOREM ASSUME NEW m \in Int,
-               m # 0,
-               NEW n \in Int
+               NEW n \in Int,
+               m # 0 \/ n > 0
         PROVE (m ^ n) \in Int
     OBVIOUS