revise univ encoding

Author: nikswamy

pulse/lib/pulse/lib/Pulse.Lib.Array.Core.fst

@@ -292,6 +292,7 @@ ghost fn pcm_rw u#a (#t: Type u#a)
   fold pts_to_mask a2 #p2 s2 m2;
 }
 
+#push-options "--z3rlimit 20 --fuel 1 --ifuel 1 --z3version 4.15.3"
 ghost fn pcm_share u#a (#t: Type u#a) #l
     (a: array t) p s m
     (a1: array t) p1 s1 m1
@@ -330,7 +331,9 @@ ghost fn pcm_share u#a (#t: Type u#a) #l
     Some? (Map.sel (mk_carrier' a p s m (a.vis l)) (i2 + a2.offset)));
   fold pts_to_mask a2 #p2 s2 m2;
 }
+#pop-options
 
+#push-options "--z3rlimit 20 --fuel 1 --ifuel 1 --z3version 4.15.3"
 ghost fn pcm_gather u#a (#t: Type u#a) #l
     (a: array t) p s m
     (a1: array t) p1 s1 m1
@@ -371,7 +374,9 @@ ghost fn pcm_gather u#a (#t: Type u#a) #l
     Map.sel (mk_carrier' a p s m (a.vis l)) (i + a.offset) == Some ((Seq.index s i, a.vis l), p));
   fold pts_to_mask a #p s m;
 }
+#pop-options
 
+#push-options "--z3rlimit 40 --fuel 0 --ifuel 0 --z3version 4.15.3"
 ghost
 fn mask_share_gen u#a (#a: Type u#a) (arr:array a) #s #p (p1: perm) (p2: perm) #mask
   requires pts_to_mask arr #p s mask
@@ -386,6 +391,7 @@ fn mask_share_gen u#a (#a: Type u#a) (arr:array a) #s #p (p1: perm) (p2: perm) #
     arr p1 s mask
     arr p2 s mask;
 }
+#pop-options
 
 ghost
 fn mask_share u#a (#a: Type u#a) (arr:array a) #s #p #mask
@@ -418,6 +424,7 @@ ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #m
       Some ((Seq.index s1 i, process_of l), p1));
 }
 
+#push-options "--z3rlimit 40 --z3refresh --fuel 1 --ifuel 1 --z3version 4.15.3"
 ghost fn split_mask u#a (#t: Type u#a) (arr: array t) #f #v #mask (pred: nat -> prop)
   requires pts_to_mask arr #f v mask
   ensures pts_to_mask arr #f v (mask_isect mask pred)
@@ -430,6 +437,7 @@ ghost fn split_mask u#a (#t: Type u#a) (arr: array t) #f #v #mask (pred: nat ->
     arr f v (mask_isect mask pred)
     arr f v (mask_diff mask pred);
 }
+#pop-options
 
 let mix #t (v1: Seq.seq t) (v2: Seq.seq t { Seq.length v1 == Seq.length v2 }) (mask: nat -> prop) :
     GTot (res: Seq.seq t { Seq.length res == Seq.length v1 /\
@@ -439,6 +447,7 @@ let mix #t (v1: Seq.seq t) (v2: Seq.seq t { Seq.length v1 == Seq.length v2 }) (m
   Seq.init_ghost (Seq.length v1) fun i ->
     if IndefiniteDescription.strong_excluded_middle (mask i) then Seq.index v1 i else Seq.index v2 i
 
+#push-options "--z3rlimit 40 --fuel 0 --ifuel 0 --z3version 4.15.3"
 [@@allow_ambiguous]
 ghost fn join_mask u#a (#t: Type u#a) (arr: array t) #f #v1 #v2 #mask1 #mask2
   requires pts_to_mask arr #f v1 mask1
@@ -461,6 +470,7 @@ ghost fn join_mask u#a (#t: Type u#a) (arr: array t) #f #v1 #v2 #mask1 #mask2
     arr f v1 mask1
     arr f v2 mask2;
 }
+#pop-options
 
 [@@allow_ambiguous]
 ghost fn join_mask' u#a (#t: Type u#a) (arr: array t) #f #v #mask1 #mask2

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -1981,9 +1981,7 @@ let encode_env_bindings (env:env_t) (bindings:list S.binding) : ML (decls_t & en
     let encode_binding b (i, decls, env) = match b with
         | S.Binding_univ u ->
           let u_fv, u_tm = EncodeTerm.encode_univ_name u in
-          let decls' = [
-            Term.DeclFun(fv_name u_fv, [], univ_sort, Some "universe local constant");
-            Util.mkAssume (mkApp("univ_ok", [u_tm]), Some ("univ_ok_" ^ fv_name u_fv), "univ_ok_" ^ fv_name u_fv)] |> mk_decls_trivial in
+          let decls' = [Term.DeclFun(fv_name u_fv, [], univ_sort, Some "universe local constant")] |> mk_decls_trivial in
           i+1, decls@decls', env
 
         | S.Binding_var x ->

src/smtencoding/FStarC.SMTEncoding.Term.fst

@@ -966,22 +966,20 @@ and mkPrelude z3options : ML string =
                 (declare-fun FString_constr_id (FString) Int)\n\
                 \n\
                 (declare-sort Term)\n\
-                (declare-datatypes () ((Universe \n\
-                                        (Univ (ulevel Int)))))\n\
-                (define-fun imax ((i Int) (j Int)) Int \n\
-                  (ite (<= i 0) j \n\
-                    (ite (<= j 0) i \n\
-                      (ite (<= i j) j i)))) \n\
-                (define-fun U_zero () Universe (Univ 0))\n\
-                (define-fun U_succ ((u Universe)) Universe\n\
-                  (Univ (+ (ulevel u) 1)))\n\
-                (declare-fun U_max (Universe Universe) Universe) \n\
-                (assert (forall ((u1 Universe) (u2 Universe)) \n\
-                                (! (= (U_max u1 u2)\n\
-                                      (Univ (imax (ulevel u1) (ulevel u2))))\n\
-                                 :pattern ((U_max u1 u2)))))\n\
-                (define-fun univ_ok ((u Universe)) Bool\n\
-                    (>= (ulevel u) 0))\n\
+                (declare-datatypes () ((Universe (U_zero) (U_succ (prev Universe)))))\n\
+                (declare-fun ulevel ((Universe)) Int)\n\
+                (declare-fun Univ (Int) Universe)\n\
+                (assert (= (ulevel U_zero) 0))\n\
+                (assert (forall ((u Universe)) (! (= (ulevel (U_succ u)) (+ 1 (ulevel u))) :weight 0 :pattern ((ulevel (U_succ u))))))\n\
+                (assert (forall ((u Universe)) (! (>= (ulevel u) 0) :weight 0 :pattern ((ulevel u)))))\n\
+                (assert (forall ((u Universe)) (! (= (Univ (ulevel u)) u) :weight 0 :pattern ((ulevel u)))))\n\
+                (assert (forall ((i Int)) (! (implies (>= i 0) (= (ulevel (Univ i)) i)) :weight 0 :pattern ((Univ i)))))\n\
+                (declare-fun U_max (Universe Universe) Universe)\n\
+                (assert (forall ((u1 Universe) (u2 Universe))\n\
+                  (! (= (U_max u1 u2)\n\
+                        (ite (<= (ulevel u1) (ulevel u2)) u2 u1))\n\
+                    :weight 0\n\
+                    :pattern ((U_max u1 u2)))))\n\
                 (declare-fun U_unif (Int) Universe)\n\
                 (declare-fun U_unknown () Universe)\n\
                 (declare-fun Term_constr_id (Term) Int)\n\