modernize parameter defaults

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/params/dyn_ack_params.h

@@ -27,21 +27,15 @@ enum class dyn_ack_strategy {
 };
 
 struct dyn_ack_params {
-    dyn_ack_strategy m_dack;
+    dyn_ack_strategy m_dack = dyn_ack_strategy::DACK_ROOT;
-    bool             m_dack_eq;
+    bool             m_dack_eq = false;
-    double           m_dack_factor;
+    double           m_dack_factor = 0.1;
-    unsigned         m_dack_threshold;
+    unsigned         m_dack_threshold = 10;
-    unsigned         m_dack_gc;
+    unsigned         m_dack_gc = 2000;
-    double           m_dack_gc_inv_decay;
+    double           m_dack_gc_inv_decay = 0.8;
 
 public:
-    dyn_ack_params(params_ref const & p = params_ref()) :
+    dyn_ack_params(params_ref const & p = params_ref()) {
-        m_dack(dyn_ack_strategy::DACK_ROOT),
-        m_dack_eq(false),
-        m_dack_factor(0.1),
-        m_dack_threshold(10),
-        m_dack_gc(2000), 
-        m_dack_gc_inv_decay(0.8) {
         updt_params(p);
     }
 

src/smt/params/theory_array_params.h

@@ -28,34 +28,20 @@ enum array_solver_id {
 };
 
 struct theory_array_params {
-    bool            m_array_canonize_simplify;
+    bool            m_array_canonize_simplify = false;
-    bool            m_array_simplify; // temporary hack for disabling array simplifier plugin.
+    bool            m_array_simplify = true; // temporary hack for disabling array simplifier plugin.
-    array_solver_id m_array_mode;
+    array_solver_id m_array_mode = array_solver_id::AR_FULL;
-    bool            m_array_weak;
+    bool            m_array_weak = false;
-    bool            m_array_extensional;
+    bool            m_array_extensional = true;
-    unsigned        m_array_laziness;
+    unsigned        m_array_laziness = 1;
-    bool            m_array_delay_exp_axiom;
+    bool            m_array_delay_exp_axiom = true;
-    bool            m_array_cg;
+    bool            m_array_cg = false;
-    bool            m_array_always_prop_upward;
+    bool            m_array_always_prop_upward = true;
-    bool            m_array_lazy_ieq;
+    bool            m_array_lazy_ieq = false;
-    unsigned        m_array_lazy_ieq_delay;
+    unsigned        m_array_lazy_ieq_delay = 10;
-    bool            m_array_fake_support;       // fake support for all array operations to pretend they are satisfiable.
+    bool            m_array_fake_support = false;       // fake support for all array operations to pretend they are satisfiable.
-
-    theory_array_params():
-        m_array_canonize_simplify(false),
-        m_array_simplify(true),
-        m_array_mode(array_solver_id::AR_FULL),
-        m_array_weak(false),
-        m_array_extensional(true),
-        m_array_laziness(1),
-        m_array_delay_exp_axiom(true),
-        m_array_cg(false),
-        m_array_always_prop_upward(true), // UPWARDs filter is broken... TODO: fix it
-        m_array_lazy_ieq(false),
-        m_array_lazy_ieq_delay(10),
-        m_array_fake_support(false) {
-    }
 
+    theory_array_params() {}
 
     void updt_params(params_ref const & _p);
 

src/smt/params/theory_bv_params.h

@@ -26,27 +26,17 @@ enum bv_solver_id {
 };
 
 struct theory_bv_params {
-    bv_solver_id m_bv_mode;
+    bv_solver_id m_bv_mode = bv_solver_id::BS_BLASTER;
-    bool  m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
+    bool         m_hi_div0 = false; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
-    bool         m_bv_reflect;
+    bool         m_bv_reflect = true;
-    bool         m_bv_lazy_le;
+    bool         m_bv_lazy_le = false;
-    bool         m_bv_cc;
+    bool         m_bv_cc = false;
-    bool         m_bv_eq_axioms;
+    bool         m_bv_eq_axioms = true;
-    unsigned     m_bv_blast_max_size;
+    unsigned     m_bv_blast_max_size = INT_MAX;
-    bool         m_bv_enable_int2bv2int;
+    bool         m_bv_enable_int2bv2int = true;
-    bool         m_bv_watch_diseq;
+    bool         m_bv_watch_diseq = false;
-    bool         m_bv_delay;
+    bool         m_bv_delay = true;
-    theory_bv_params(params_ref const & p = params_ref()):
+    theory_bv_params(params_ref const & p = params_ref()) {
-        m_bv_mode(bv_solver_id::BS_BLASTER),
-        m_hi_div0(false),
-        m_bv_reflect(true),
-        m_bv_lazy_le(false),
-        m_bv_cc(false),
-        m_bv_eq_axioms(true),
-        m_bv_blast_max_size(INT_MAX),
-        m_bv_enable_int2bv2int(true),
-        m_bv_watch_diseq(false),
-        m_bv_delay(true) {
         updt_params(p);
     }
     

src/smt/params/theory_pb_params.h

@@ -22,12 +22,11 @@ Revision History:
 
 
 struct theory_pb_params {
-    unsigned m_pb_conflict_frequency;
+    unsigned m_pb_conflict_frequency = 1000;
-    bool     m_pb_learn_complements;
+    bool     m_pb_learn_complements = true;
-    theory_pb_params(params_ref const & p = params_ref()):
+    theory_pb_params(params_ref const & p = params_ref()) {
-        m_pb_conflict_frequency(1000),
+        updt_params(p);
-        m_pb_learn_complements(true)
+    }
-    {}
     
     void updt_params(params_ref const & p);
 

src/smt/params/theory_seq_params.h

@@ -22,14 +22,10 @@ struct theory_seq_params {
     /*
      * Enable splitting guided by length constraints
      */
-    bool m_split_w_len;
+    bool m_split_w_len = false;
-    bool m_seq_validate;
+    bool m_seq_validate = false;
 
-
+    theory_seq_params(params_ref const & p = params_ref()) {
-    theory_seq_params(params_ref const & p = params_ref()):
-        m_split_w_len(false),
-        m_seq_validate(false)
-    {
         updt_params(p);
     }
 

src/smt/params/theory_str_params.h

@@ -27,108 +27,92 @@ struct theory_str_params {
      * This is a stronger version of the standard axiom.
      * The Z3str2 axioms can be simulated by setting this to false.
      */
-    bool m_StrongArrangements;
+    bool m_StrongArrangements = true;
 
     /*
      * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
      * to prioritize trying concrete length options over choosing the "more" option.
      */
-    bool m_AggressiveLengthTesting;
+    bool m_AggressiveLengthTesting = false;
 
     /*
      * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
      * to prioritize trying concrete value options over choosing the "more" option.
      */
-    bool m_AggressiveValueTesting;
+    bool m_AggressiveValueTesting = false;
 
     /*
      * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
      * to prioritize trying concrete unroll counts over choosing the "more" option.
      */
-    bool m_AggressiveUnrollTesting;
+    bool m_AggressiveUnrollTesting = true;
 
     /*
      * If UseFastLengthTesterCache is set to true,
      * length tester terms will not be generated from scratch each time they are needed,
      * but will be saved in a map and looked up.
      */
-    bool m_UseFastLengthTesterCache;
+    bool m_UseFastLengthTesterCache = false;
 
     /*
      * If UseFastValueTesterCache is set to true,
      * value tester terms will not be generated from scratch each time they are needed,
      * but will be saved in a map and looked up.
      */
-    bool m_UseFastValueTesterCache;
+    bool m_UseFastValueTesterCache = true;
 
     /*
      * If StringConstantCache is set to true,
      * all string constants in theory_str generated from anywhere will be cached and saved.
      */
-    bool m_StringConstantCache;
+    bool m_StringConstantCache = true;
 
-    double m_OverlapTheoryAwarePriority;
+    double m_OverlapTheoryAwarePriority = -0.1;
 
     /*
      * RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3
      * will not eagerly construct an automaton for a regular expression term.
      */
-    unsigned m_RegexAutomata_DifficultyThreshold;
+    unsigned m_RegexAutomata_DifficultyThreshold = 1000;
 
     /*
      * RegexAutomata_IntersectionDifficultyThreshold is the lowest difficulty above which Z3str3
      * will not eagerly intersect automata to check unsatisfiability.
      */
-    unsigned m_RegexAutomata_IntersectionDifficultyThreshold;
+    unsigned m_RegexAutomata_IntersectionDifficultyThreshold = 1000;
 
     /*
      * RegexAutomata_FailedAutomatonThreshold is the number of failed attempts to build an automaton
      * after which a full automaton (i.e. with no length information) will be built regardless of difficulty.
      */
-    unsigned m_RegexAutomata_FailedAutomatonThreshold;
+    unsigned m_RegexAutomata_FailedAutomatonThreshold = 10;
 
     /*
      * RegexAutomaton_FailedIntersectionThreshold is the number of failed attempts to perform automaton
      * intersection after which intersection will always be performed regardless of difficulty.
      */
-    unsigned m_RegexAutomata_FailedIntersectionThreshold;
+    unsigned m_RegexAutomata_FailedIntersectionThreshold = 10;
 
     /*
      * RegexAutomaton_LengthAttemptThreshold is the number of attempts to satisfy length/path constraints
      * before which we begin checking unsatisfiability of a regex term.
      */
-    unsigned m_RegexAutomata_LengthAttemptThreshold;
+    unsigned m_RegexAutomata_LengthAttemptThreshold = 10;
     /*
      * If FixedLengthRefinement is true and the fixed-length equation solver is enabled,
      * Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive
      * reductions to fixed-length formulas.
      */
-    bool m_FixedLengthRefinement;
+    bool m_FixedLengthRefinement = false;
 
     /*
      * If FixedLengthNaiveCounterexamples is true and the fixed-length equation solver is enabled,
      * Z3str3 will only construct simple counterexamples to block unsatisfiable length assignments
      * instead of attempting to learn more complex lessons.
      */
-    bool m_FixedLengthNaiveCounterexamples;
+    bool m_FixedLengthNaiveCounterexamples = true;
 
-    theory_str_params(params_ref const & p = params_ref()):
+    theory_str_params(params_ref const & p = params_ref()) {
-        m_StrongArrangements(true),
-        m_AggressiveLengthTesting(false),
-        m_AggressiveValueTesting(false),
-        m_AggressiveUnrollTesting(true),
-        m_UseFastLengthTesterCache(false),
-        m_UseFastValueTesterCache(true),
-        m_StringConstantCache(true),
-        m_OverlapTheoryAwarePriority(-0.1),
-        m_RegexAutomata_DifficultyThreshold(1000),
-        m_RegexAutomata_IntersectionDifficultyThreshold(1000),
-        m_RegexAutomata_FailedAutomatonThreshold(10),
-        m_RegexAutomata_FailedIntersectionThreshold(10),
-        m_RegexAutomata_LengthAttemptThreshold(10),
-        m_FixedLengthRefinement(false),
-        m_FixedLengthNaiveCounterexamples(true)
-    {
         updt_params(p);
     }