Merge pull request #2776 from FStarLang/guido_smt

A synchronous mode for SMT queries (+ tactic), plus a change to `--split_queries`
FStarLang · Apr 18, 2023 · 4354a71 · 4354a71
2 parents b07d0e2 + 07c0872
commit 4354a71
Show file tree

Hide file tree

Showing 25 changed files with 2,666 additions and 1,980 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -569,6 +569,14 @@ Guidelines for the changelog:
      which to enable profiling. The output of F* on its finished
      message changed to not print the time it took to verify a module.
 
+   * [PR #2776](https://github.com/FStarLang/FStar/pull/2776): The
+     `--split_queries` option now takes an argument, one of `no`,
+     `on_failure` and `always`. The default is `on_failure`, with
+     the same behavior as previously (split a query and retry when
+     the SMT solver does not return a helpful error). Using
+     `--split_queries always` mimics the old `--split_queries`,
+     splitting all queries eagerly. Using `--split_queries no` disables
+     splitting altogether.
 
 ## Editors
 

diff --git a/doc/book/code/Alex.fst b/doc/book/code/Alex.fst
@@ -7,7 +7,7 @@ val f : (f:(nat -> int){unbounded f})
 
 let g : (nat -> int) = fun x -> f (x+1)
 
-#push-options "--query_stats --fuel 0 --ifuel 0 --split_queries"
+#push-options "--query_stats --fuel 0 --ifuel 0 --split_queries always"
 let find_above_for_g (m:nat) : Lemma(exists (i:nat). abs(g i) > m) = 
   assert (unbounded f); // apply forall to m
   eliminate exists (n:nat). abs(f n) > m

diff --git a/doc/book/under_the_hood/uth_smt.rst b/doc/book/under_the_hood/uth_smt.rst
@@ -1600,8 +1600,8 @@ F* reports:
     (Warning 349) The verification condition succeeded after splitting
     it to localize potential errors, although the original non-split
     verification condition failed. If you want to rely on splitting
-    queries for verifying your program please use the --split_queries
-    option rather than relying on it implicitly.
+    queries for verifying your program please use the '--split_queries
+    always' option rather than relying on it implicitly.
 
 By default, F* collects all the proof obligations in a top-level F*
 definition and presents it to Z3 in a single query with several
@@ -1625,7 +1625,7 @@ any. However, sometimes, when tried in this mode, the proof of all
 conjuncts can succeed.
 
 One way to respond to Warning 349 is to follow what it says and enable
-``--split_queries`` explicitly, at least for the program fragment in
+``--split_queries always`` explicitly, at least for the program fragment in
 question. This can sometimes stabilize a previously unstable
 proof. However, it may also end up deferring an underlying
 proof-performance problem. Besides, even putting stability aside,

diff --git a/ocaml/fstar-lib/FStar_Tactics_Builtins.ml b/ocaml/fstar-lib/FStar_Tactics_Builtins.ml
@@ -170,6 +170,9 @@ let push_bv_dsenv           = from_tac_2 B.push_bv_dsenv
 let term_to_string          = from_tac_1 B.term_to_string
 let comp_to_string          = from_tac_1 B.comp_to_string
 let term_eq_old             = from_tac_2 B.term_eq_old
+let get_vconfig             = from_tac_1 B.get_vconfig
+let set_vconfig             = from_tac_1 B.set_vconfig
+let t_smt_sync              = from_tac_1 B.t_smt_sync
 
 let with_compat_pre_core (n:Prims.int) (f: unit -> 'a __tac) : 'a __tac =
   from_tac_2 B.with_compat_pre_core n (to_tac_0 (f ()))

diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml