From 035c39d5b92dc1cbf473e27512f2814c63eb4b27 Mon Sep 17 00:00:00 2001 From: rosalie Date: Fri, 26 Jan 2024 14:59:22 +0100 Subject: [PATCH] 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. --- src/encode.mli | 2 +- src/encode/n_axioms.ml | 36 +++++++++++++++++++++++----- src/encode/n_axioms.mli | 2 +- src/encode/n_data.ml | 20 +++++++++------- src/encode/n_standardize.ml | 2 +- src/encode/n_table.ml | 4 ++-- src/encode/n_table.mli | 2 +- src/type/t_synth.ml | 6 ++--- test/unit/e_arith/typingexp_test.tla | 4 ++-- 9 files changed, 53 insertions(+), 25 deletions(-) diff --git a/src/encode.mli b/src/encode.mli index 6525c847..1459b318 100644 --- 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 index c1fb7db3..85c08feb 100644 --- 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 index c303e64a..708471a9 100644 --- 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 index 0828c085..982cdfe2 100644 --- 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 index c7942e20..2211b1c9 100644 --- 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 index a950108d..2354b528 100644 --- 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 index 86a8330d..13c64700 100644 --- 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 index 33e6725a..95b7c3de 100644 --- 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 index af6d9037..7360618e 100644 --- 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