enable context pruning

FStarLang · Sep 5, 2024 · 3668e72 · 3668e72
1 parent eea1d86
commit 3668e72
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 5 deletions.
diff --git a/Pulse.fst.config.json b/Pulse.fst.config.json
@@ -3,7 +3,9 @@
   "options": [
     "--query_cache",
     "--load_cmxs",
-    "pulse"
+    "pulse",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
     "lib/pulse",

diff --git a/lib/pulse/core/Pulse.fst.config.json b/lib/pulse/core/Pulse.fst.config.json
@@ -1,7 +1,9 @@
 {
 	"fstar_exe": "fstar.exe",
 	"options": [
-		"--query_cache"
+		"--query_cache",
+		"--ext",
+		"context_pruning"
 	],
 	"include_dirs": [
 	]

diff --git a/share/pulse/Makefile.include-base b/share/pulse/Makefile.include-base
@@ -19,7 +19,7 @@ else
 USE_HINTS:=
 endif
 
-FSTAR_OPTIONS += $(USE_HINTS)
+FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning
 
 # A place to put all build artifacts
 ifneq (,$(OUTPUT_DIRECTORY))

diff --git a/share/pulse/examples/Pulse.fst.config.json b/share/pulse/examples/Pulse.fst.config.json
@@ -7,7 +7,9 @@
     "--cache_dir",
     "_output/cache",
     "--warn_error", 
-    "-249"
+    "-249",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
     "../../../lib/pulse",

diff --git a/src/checker/PulseChecker.fst.config.json b/src/checker/PulseChecker.fst.config.json
@@ -1,7 +1,9 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
-    "--query_cache"
+    "--query_cache",
+    "--ext",
+    "context_pruning"
   ],
   "include_dirs": [
   ]