Disable MBQI for z3

cargo-creusot/src/why3_launcher.rs

@@ -49,9 +49,12 @@ impl Why3Launcher {
         std::fs::create_dir(&prelude_dir)?;
 
         PRELUDE
-            .extract(prelude_dir)
+            .extract(&prelude_dir)
             .expect("can't launch why3, could extract prelude into temp dir");
 
+        let mut conf_path = prelude_dir;
+        conf_path.push("creusot-why3.conf");
+
         let mut command =
             if let Some(p) = &self.why3_path { Command::new(p) } else { Command::new("why3") };
         command
@@ -63,7 +66,9 @@ impl Why3Launcher {
                 "-L",
             ])
             .arg(temp_dir.as_os_str())
-            .arg(&self.output_file);
+            .arg(&self.output_file)
+            .arg("--extra-config")
+            .arg(conf_path.as_os_str());
         if let Some(cfg) = &self.config_file {
             command.arg("-C").arg(cfg);
         }

creusot/src/run_why3.rs

@@ -17,7 +17,7 @@ use rustc_span::{
 use serde_json::Deserializer;
 use std::{
     collections::{hash_map::Entry, HashMap},
-    fmt::{Display, Formatter, Write},
+    fmt::Write,
     io::BufReader,
     path::PathBuf,
     process::{Command, Stdio},
@@ -27,12 +27,12 @@ use why3::ce_models::{ConcreteTerm, FunLitElt, Goal, Loc, ProverResult, TBool, T
 
 static PRELUDE: Dir<'static> = include_dir!("$CARGO_MANIFEST_DIR/../prelude");
 
-impl Display for Why3Sub {
-    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+impl Why3Sub {
+    fn to_str(&self) -> &str {
         match self {
-            Why3Sub::Prove => f.write_str("prove"),
-            Why3Sub::Ide => f.write_str("ide"),
-            Why3Sub::Replay => f.write_str("replay"),
+            Why3Sub::Prove => "prove",
+            Why3Sub::Ide => "ide",
+            Why3Sub::Replay => "replay",
         }
     }
 }
@@ -51,6 +51,8 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
     std::fs::create_dir(&prelude_dir).unwrap();
 
     PRELUDE.extract(&prelude_dir).expect("could extract prelude into temp dir");
+    let mut conf_path = prelude_dir;
+    conf_path.push("creusot-why3.conf");
     let mut command = Command::new(&why3_cmd.path);
     command
         .args([
@@ -59,11 +61,13 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
             "--warn-off=unused_variable",
             "--warn-off=clone_not_abstract",
             "--warn-off=axiom_abstract",
-            &why3_cmd.sub.to_string(),
+            why3_cmd.sub.to_str(),
             "-L",
         ])
         .arg(temp_dir.path().as_os_str())
         .arg(&output_file)
+        .arg("--extra-config")
+        .arg(conf_path.as_os_str())
         .args(why3_cmd.args.split_ascii_whitespace());
 
     if matches!(why3_cmd.sub, Why3Sub::Prove) {

prelude/creusot-why3.conf

@@ -0,0 +1,3 @@
+[prover_modifiers]
+name = "Z3"
+driver = "z3_nombqi.drv"

prelude/z3_nombqi.drv

@@ -0,0 +1,36 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+   License, v. 2.0. If a copy of the MPL was not distributed with this
+   file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+   Copyright (c) 2011-2021 ETH Zurich.
+*)
+
+theory BuiltIn
+  meta "select_inst_default" "all"
+  meta "select_lskept_default" "all"
+  meta "select_lsinst_default" "all"
+  meta "select_kept_default" "local"
+end
+
+theory map.Const
+  syntax function const "((as const %t0) %1)"
+end
+
+theory seq.Seq
+  remove prop set'def
+  remove prop ([..])'def
+end
+
+prelude ";;; generated by no_mbqi extension"
+prelude "(set-option :smt.AUTO_CONFIG false)"
+prelude "(set-option :smt.PHASE_SELECTION 0)"
+prelude "(set-option :smt.RESTART_STRATEGY 0)"
+prelude "(set-option :smt.RESTART_FACTOR 1.5)"
+prelude "(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)"
+prelude "(set-option :smt.CASE_SPLIT 3)"
+prelude "(set-option :smt.DELAY_UNITS true)"
+prelude "(set-option :NNF.SK_HACK true)"
+prelude "(set-option :smt.MBQI false)"
+prelude "(set-option :smt.BV.REFLECT true)"
+prelude "(set-option :smt.qi.max_multi_patterns 1000)"
+prelude "(set-option :smt.QI.EAGER_THRESHOLD 10)"