Merge pull request #694 from viperproject/meilers_z3_update

Z3 option update

Author: marcoeilers

src/main/resources/z3config.smt2

@@ -2,7 +2,7 @@
 ; 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/.
 
-; Requires Z3 >= 4.3.2
+; Tested with Z3 4.8.7 and 4.12.1
 
 ; ATTENTION: Continuing multi-line statements must be indented with at least
 ;            one tab or two spaces. All other lines must not start with tabs
@@ -12,53 +12,19 @@
 ; setting options, is answered by a success (or error) reply from Z3. Silicon currently relies on
 ; these replies when it interacts with Z3 via stdio.
 (set-option :print-success true) ; Boogie: false
+(set-option :global-decls true) ; Necessary for push pop mode
 
-(set-option :global-decls true) ; Boogie: default
-(set-option :auto_config false) ; Usually a good idea
-
-(set-option :smt.restart_strategy 0)
-(set-option :smt.restart_factor |1.5|)
+; These options are taken from Dafny 4.0.0 and proven to work decently well with up-to-date Z3 (currently 4.12.1),
+; unlike the options used previously.
+(set-option :auto_config false)
 (set-option :smt.case_split 3)
 (set-option :smt.delay_units true)
-(set-option :smt.delay_units_threshold 16)
-(set-option :nnf.sk_hack true)
 (set-option :type_check true)
-(set-option :smt.bv.reflect true)
-
 (set-option :smt.mbqi false)
+(set-option :pp.bv_literals false)
 (set-option :smt.qi.eager_threshold 100)
-; (set-option :smt.qi.lazy_threshold 1000000000)
-(set-option :smt.qi.cost "(+ weight generation)")
-(set-option :smt.qi.max_multi_patterns 1000)
-; (set-option :smt.qi.profile true)
-; (set-option :smt.qi.profile_freq 100000)
-
-;; [2019-07-31 Malte] The next block of options are all randomness-related options that I could
-;; find in the description Z3 -pd emits. If not stated otherwise, the options are merely explicitly
-;; set to their default values.
-(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
-(set-option :sat.phase caching)
-(set-option :sat.random_seed 0)
-(set-option :nlsat.randomize true)
-(set-option :nlsat.seed 0)
-(set-option :nlsat.shuffle_vars false)
-(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
-(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
-(set-option :smt.arith.random_initial_value true) ; Boogie: true
-(set-option :smt.random_seed 0)
-(set-option :sls.random_offset true)
-(set-option :sls.random_seed 0)
-(set-option :sls.restart_init false)
-(set-option :sls.walksat_ucb true)
-
-; (set-option :smt.macro_finder true)
-; (set-option :combined_solver.solver2_timeout 500)
-; (set-option :combined_solver.solver2_unknown 2)
-; (set-option :smt.arith.nl false)
-; (set-option :smt.arith.nl.gb false)
-    ; See http://stackoverflow.com/questions/28210673
-
-; (set-option :produce-models true)
-; (set-option :model false)
+(set-option :smt.arith.solver 2)
 (set-option :model.v2 true)
-; (set-option :model.compact true)
+
+; We want unlimited multipatterns
+(set-option :smt.qi.max_multi_patterns 1000)

src/main/scala/decider/Z3ProverAPI.scala

@@ -47,37 +47,23 @@ object Z3ProverAPI {
   val boolParams = Map(
     "smt.delay_units" -> true,
     "delay_units" -> true,
-    "nnf.sk_hack" -> true,
     "smt.mbqi" -> false,
     "mbqi" -> false,
-    "nlsat.randomize" -> true,
-    "nlsat.shuffle_vars" -> false,
-    "smt.arith.random_initial_value" -> true,
-    "arith.random_initial_value" -> true,
-    "bv.reflect" -> true,
+    //"pp.bv_literals" -> false,  // This is part of z3config.smt2 but Z3 won't accept it via API.
+    "model.v2" -> true
   )
   val intParams = Map(
-    "smt.restart_strategy" -> 0,
-    "restart_strategy" -> 0,
     "smt.case_split" -> 3,
     "case_split" -> 3,
-    "smt.delay_units_threshold" -> 16,
-    "delay_units_threshold" -> 16,
     "smt.qi.max_multi_patterns" -> 1000,
     "qi.max_multi_patterns" -> 1000,
-    "smt.phase_selection" -> 0,
-    "phase_selection" -> 0,
-    "sat.random_seed" -> 0,
-    "nlsat.seed" -> 0,
-    "random_seed" -> 0,
+    "smt.arith.solver" -> 2,
+    "arith.solver" -> 2
   )
-  val stringParams = Map(
-    //"smt.qi.cost" -> "(+ weight generation)", // cannot set this for some reason, but this is the default value anyway.
-    "sat.phase" -> "caching"
+  val stringParams: Map[String, String] = Map(
+    // currently none
   )
   val doubleParams = Map(
-    "smt.restart_factor" -> 1.5,
-    "restart_factor" -> 1.5,
     "smt.qi.eager_threshold" -> 100.0,
     "qi.eager_threshold" -> 100.0,
   )