Merge pull request #2453 from FStarLang/afromher_smthandle

Hook to handle SMT goal by tactic
FStarLang · Feb 28, 2022 · 89ed54c · 89ed54c
2 parents ebb4027 + 50bab39
commit 89ed54c
Show file tree

Hide file tree

Showing 19 changed files with 305 additions and 63 deletions.
diff --git a/examples/tactics/HandleSmtGoal.fst b/examples/tactics/HandleSmtGoal.fst
@@ -0,0 +1,24 @@
+module HandleSmtGoal
+
+open FStar.Tactics
+
+[@@ handle_smt_goals]
+let tac () : Tac unit =
+  dump "now"
+
+let f (x:int) : Pure unit (requires x == 2) (ensures fun _ -> True) =
+  assert (x == 2);
+  ()
+
+(* A bogus lemma, used only to obtain a simple goal that will not be solvable
+   if handle_smt_goal does not trigger. It also has a trivially true precondition,
+   but that is sent to SMT*)
+assume
+val test_lemma (_:unit) : Lemma (requires forall (x:nat). x >= 0) (ensures False)
+
+[@@ handle_smt_goals]
+let tac2 () : Tac unit =
+  apply_lemma (`test_lemma)
+
+let g () : Tot unit =
+  assert (False)
diff --git a/src/fstar/FStar.Universal.fs b/src/fstar/FStar.Universal.fs
@@ -115,7 +115,10 @@ let init_env deps : TcEnv.env =
   let solver =
     if Options.lax()
     then SMT.dummy
-    else {SMT.solver with preprocess=FStar.Tactics.Hooks.preprocess} in
+    else {SMT.solver with
+      preprocess=FStar.Tactics.Hooks.preprocess;
+      handle_smt_goal=FStar.Tactics.Hooks.handle_smt_goal
+    } in
   let env =
       TcEnv.initial_env
         deps

diff --git a/src/ocaml-output/FStar_Parser_Const.ml b/src/ocaml-output/FStar_Parser_Const.ml
diff --git a/src/ocaml-output/FStar_Pervasives.ml b/src/ocaml-output/FStar_Pervasives.ml
diff --git a/src/ocaml-output/FStar_SMTEncoding_Solver.ml b/src/ocaml-output/FStar_SMTEncoding_Solver.ml
diff --git a/src/ocaml-output/FStar_Tactics_Hooks.ml b/src/ocaml-output/FStar_Tactics_Hooks.ml
diff --git a/src/ocaml-output/FStar_TypeChecker_Env.ml b/src/ocaml-output/FStar_TypeChecker_Env.ml
diff --git a/src/ocaml-output/FStar_TypeChecker_Rel.ml b/src/ocaml-output/FStar_TypeChecker_Rel.ml
diff --git a/src/ocaml-output/FStar_Universal.ml b/src/ocaml-output/FStar_Universal.ml
diff --git a/src/parser/FStar.Parser.Const.fs b/src/parser/FStar.Parser.Const.fs
@@ -341,6 +341,8 @@ let dm4f_bind_range_attr = p2l ["FStar"; "Pervasives"; "dm4f_bind_range"]
 let must_erase_for_extraction_attr = psconst "must_erase_for_extraction"
 let strict_on_arguments_attr = p2l ["FStar"; "Pervasives"; "strict_on_arguments"]
 let resolve_implicits_attr_string = "FStar.Pervasives.resolve_implicits"
+let handle_smt_goals_attr = psconst "handle_smt_goals"
+let handle_smt_goals_attr_string = "FStar.Pervasives.handle_smt_goals"
 let erasable_attr = p2l ["FStar"; "Pervasives"; "erasable"]
 let comment_attr = p2l ["FStar"; "Pervasives"; "Comment"]
 let fail_attr      = psconst "expect_failure"

diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fs b/src/smtencoding/FStar.SMTEncoding.Solver.fs
@@ -957,6 +957,7 @@ let solver = {
     rollback=Encode.rollback;
     encode_sig=Encode.encode_sig;
     preprocess=(fun e g -> [e,g, FStar.Options.peek ()]);
+    handle_smt_goal=(fun e g -> [e,g]);
     solve=solve;
     finish=Z3.finish;
     refresh=Z3.refresh;
@@ -969,6 +970,7 @@ let dummy = {
     rollback=(fun _ _ -> ());
     encode_sig=(fun _ _ -> ());
     preprocess=(fun e g -> [e,g, FStar.Options.peek ()]);
+    handle_smt_goal=(fun e g -> [e,g]);
     solve=(fun _ _ _ -> ());
     finish=(fun () -> ());
     refresh=(fun () -> ());