Skip to content

Commit

Permalink
add universe arguments to Prims.precedes in SMT encoding
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikswamy
nikswamy committed Jan 11, 2025
1 parent c8d08cb commit ff16b6e
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 36 deletions.
8 changes: 4 additions & 4 deletions src/smtencoding/FStarC.SMTEncoding.Encode.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ let primitive_type_axioms : env -> lident -> string -> term -> list decl =
let a = mkFreeV aa in
let bb = mk_fv ("b", Int_sort) in
let b = mkFreeV bb in
let precedes_y_x = mk_Valid <| mkApp("Prims.precedes", [lex_t; lex_t;y;x]) in
let precedes_y_x = mk_Valid <| mkApp("Prims.precedes", [mk_U_zero; mk_U_zero; lex_t; lex_t;y;x]) in
[Util.mkAssume(mkForall (Env.get_range env) ([[Term.boxInt b]], [bb], mk_HasType (Term.boxInt b) tt), Some "int typing", "int_typing");
Util.mkAssume(mkForall_fuel env (Env.get_range env) ([[typing_pred]], [xx], mkImp(typing_pred, mk_tester (fst boxIntFun) x)), Some "int inversion", "int_inversion");
Util.mkAssume(mkForall_fuel env (Env.get_range env) ([[typing_pred; typing_pred_y;precedes_y_x]],
Expand Down Expand Up @@ -1465,7 +1465,7 @@ let encode_datacon (env:env_t) (se:sigelt)
(* it's a parameter, so it's inaccessible and no need for a sub-term ordering on it *)
if i < n_tps
then []
else [mk_Precedes lex_t lex_t (mkFreeV v) dapp])
else [mk_Precedes mk_U_zero mk_U_zero lex_t lex_t (mkFreeV v) dapp])
|> List.flatten
in
Util.mkAssume(mkForall (Ident.range_of_lid d)
Expand Down Expand Up @@ -1556,13 +1556,13 @@ let encode_datacon (env:env_t) (se:sigelt)
let bs', guards', _env', bs_decls, _ = encode_binders None bs env' in
let fun_app = mk_Apply (mkFreeV var) bs' in
mkForall (Ident.range_of_lid d)
([[mk_Precedes lex_t lex_t fun_app dapp]],
([[mk_Precedes mk_U_zero mk_U_zero lex_t lex_t fun_app dapp]],
bs',
//need to use ty_pred' here, to avoid variable capture
//Note, ty_pred' is indexed by fuel, not S_fuel
//That's ok, since the outer pattern is guarded on S_fuel
mkImp (mk_and_l (ty_pred'::guards'),
mk_Precedes lex_t lex_t fun_app dapp))
mk_Precedes mk_U_zero mk_U_zero lex_t lex_t fun_app dapp))
:: codomain_prec_l,
bs_decls @ cod_decls)
([],[])
Expand Down
10 changes: 0 additions & 10 deletions src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1127,16 +1127,6 @@ and encode_term (t:typ) (env:env_t) : (term (* encoding of t, expects t
let v2, decls2 = encode_term v2 env in
mk_LexCons v0 v1 v2, decls0@decls1@decls2
| Tm_uinst({n=Tm_fvar fv}, _), [(v0, _); (v1, _); (v2, _); (v3, _)]
| Tm_fvar fv, [(v0, _); (v1, _); (v2, _); (v3, _)]
when S.fv_eq_lid fv Const.precedes_lid ->
//precedes is primitive
let v0, decls0 = encode_term v0 env in
let v1, decls1 = encode_term v1 env in
let v2, decls2 = encode_term v2 env in
let v3, decls3 = encode_term v3 env in
mk_Precedes_term v0 v1 v2 v3 Range.dummyRange, decls0@decls1@decls2@decls3
| Tm_constant Const_range_of, [(arg, _)] ->
encode_const (Const_range arg.pos) env
Expand Down
38 changes: 19 additions & 19 deletions src/smtencoding/FStarC.SMTEncoding.Term.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -976,7 +976,7 @@ and mkPrelude z3options =
(declare-fun ConsFuel (Fuel Term) Term)\n\
(declare-fun Tm_uvar (Int) Term)\n\
(define-fun Reify ((x Term)) Term x)\n\
(declare-fun Prims.precedes (Term Term Term Term) Term)\n\
(declare-fun Prims.precedes (Universe Universe Term Term Term Term) Term)\n\
(declare-fun Range_const (Int) Term)\n\
(declare-fun _mul (Int Int) Int)\n\
(declare-fun _div (Int Int) Int)\n\
Expand Down Expand Up @@ -1015,17 +1015,17 @@ and mkPrelude z3options =
|> List.map (declToSmt z3options) |> String.concat "\n" in
let precedes_partial_app = "\n\
(declare-fun Prims.precedes@tok () Term)\n\
(declare-fun Prims.precedes@tok (Universe Universe) Term)\n\
(assert\n\
(forall ((@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))\n\
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT Prims.precedes@tok\n\
(forall ((u0 Universe) (u1 Universe) (@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))\n\
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1)\n\
@x0)\n\
@x1)\n\
@x2)\n\
@x3)\n\
(Prims.precedes @x0 @x1 @x2 @x3))\n\
(Prims.precedes u0 u1 @x0 @x1 @x2 @x3))\n\
\n\
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT Prims.precedes@tok\n\
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1)\n\
@x0)\n\
@x1)\n\
@x2)\n\
Expand All @@ -1035,19 +1035,19 @@ and mkPrelude z3options =
(is-LexCons t))\n\
(declare-fun Prims.lex_t () Term)\n\
(declare-fun LexTop () Term)\n\
(assert (forall ((t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))\n\
(iff (Valid (Prims.precedes Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))\n\
(or (Valid (Prims.precedes t1 t2 x1 y1))\n\
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))\n\
(iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))\n\
(or (Valid (Prims.precedes u0 u1 t1 t2 x1 y1))\n\
(and (= x1 y1)\n\
(Valid (Prims.precedes Prims.lex_t Prims.lex_t x2 y2)))))))\n\
(assert (forall ((t1 Term) (t2 Term) (e1 Term) (e2 Term))\n\
(! (iff (Valid (Prims.precedes t1 t2 e1 e2))\n\
(Valid (Prims.precedes Prims.lex_t Prims.lex_t e1 e2)))\n\
:pattern (Prims.precedes t1 t2 e1 e2))))\n\
(assert (forall ((t1 Term) (t2 Term))\n\
(! (iff (Valid (Prims.precedes Prims.lex_t Prims.lex_t t1 t2)) \n\
(Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t x2 y2)))))))\n\
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (e1 Term) (e2 Term))\n\
(! (iff (Valid (Prims.precedes u0 u1 t1 t2 e1 e2))\n\
(Valid (Prims.precedes U_zero U_zero Prims.lex_t Prims.lex_t e1 e2)))\n\
:pattern (Prims.precedes u0 u1 t1 t2 e1 e2))))\n\
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term))\n\
(! (iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)) \n\
(Prec t1 t2))\n\
:pattern ((Prims.precedes Prims.lex_t Prims.lex_t t1 t2)))))\n" in
:pattern ((Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)))))\n" in
let valid_intro =
"(assert (forall ((e Term) (t Term))\n\
Expand Down Expand Up @@ -1191,8 +1191,8 @@ let mk_tester n t = mkApp("is-"^n, [t]) t.rng
let mk_ApplyTF t t' = mkApp("ApplyTF", [t;t']) t.rng
let mk_ApplyTT t t' r = mkApp("ApplyTT", [t;t']) r
let mk_String_const s r = mkApp ("FString_const", [mk (String s) r]) r
let mk_Precedes_term x1 x2 x3 x4 r = mkApp("Prims.precedes", [x1;x2;x3;x4]) r
let mk_Precedes x1 x2 x3 x4 r = mk_Valid (mk_Precedes_term x1 x2 x3 x4 r)
let mk_Precedes_term u0 u1 x1 x2 x3 x4 r = mkApp("Prims.precedes", [u0;u1;x1;x2;x3;x4]) r
let mk_Precedes u0 u1 x1 x2 x3 x4 r = mk_Valid (mk_Precedes_term u0 u1 x1 x2 x3 x4 r)
let mk_lex_t r = mkApp("Prims.lex_t", []) r
let mk_LexCons x1 x2 x3 r = mkApp("LexCons", [x1;x2;x3]) r
let mk_LexTop r = mkApp("LexTop", []) r
Expand Down
4 changes: 2 additions & 2 deletions src/smtencoding/FStarC.SMTEncoding.Term.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -321,8 +321,8 @@ val mk_Term_type: term -> term
val mk_ApplyTF: term -> term -> term
val mk_ApplyTT: term -> term -> Range.range -> term
val mk_String_const: string -> Range.range -> term
val mk_Precedes_term:term -> term -> term -> term -> Range.range -> term
val mk_Precedes: term -> term -> term -> term -> Range.range -> term
val mk_Precedes_term:term -> term -> term -> term -> term -> term -> Range.range -> term
val mk_Precedes: term -> term -> term -> term -> term -> term -> Range.range -> term
val mk_lex_t: Range.range -> term
val mk_LexCons: term -> term -> term -> Range.range -> term
val mk_LexTop: Range.range -> term
Expand Down
2 changes: 1 addition & 1 deletion src/smtencoding/FStarC.SMTEncoding.Util.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ let mk_and_l = norng mk_and_l
let mk_or_l = norng mk_or_l
let mk_ApplyTT = norng2 mk_ApplyTT
let mk_String_const = norng mk_String_const
let mk_Precedes = norng4 mk_Precedes
let mk_Precedes u0 u1 = norng4 (mk_Precedes u0 u1)
let mk_LexCons = norng3 mk_LexCons
let mk_lex_t = mk_lex_t Range.dummyRange
let mk_LexTop = mk_LexTop Range.dummyRange
Expand Down

0 comments on commit ff16b6e

Please sign in to comment.