From 18e4546404026a995f5eed0ff2da412c57c819e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Sep 2021 17:42:36 -0700 Subject: [PATCH] modernize parameter defaults Signed-off-by: Nikolaj Bjorner --- src/smt/params/dyn_ack_params.h | 20 ++++-------- src/smt/params/theory_array_params.h | 40 ++++++++--------------- src/smt/params/theory_bv_params.h | 32 +++++++------------ src/smt/params/theory_pb_params.h | 11 +++---- src/smt/params/theory_seq_params.h | 10 ++---- src/smt/params/theory_str_params.h | 48 ++++++++++------------------ 6 files changed, 55 insertions(+), 106 deletions(-) diff --git a/src/smt/params/dyn_ack_params.h b/src/smt/params/dyn_ack_params.h index ce5a685bf..81211e9cd 100644 --- a/src/smt/params/dyn_ack_params.h +++ b/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; - bool m_dack_eq; - double m_dack_factor; - unsigned m_dack_threshold; - unsigned m_dack_gc; - double m_dack_gc_inv_decay; + dyn_ack_strategy m_dack = dyn_ack_strategy::DACK_ROOT; + bool m_dack_eq = false; + double m_dack_factor = 0.1; + unsigned m_dack_threshold = 10; + unsigned m_dack_gc = 2000; + double m_dack_gc_inv_decay = 0.8; public: - 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) { + dyn_ack_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_array_params.h b/src/smt/params/theory_array_params.h index 250d17ffb..b6da32ba5 100644 --- a/src/smt/params/theory_array_params.h +++ b/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_simplify; // temporary hack for disabling array simplifier plugin. - array_solver_id m_array_mode; - bool m_array_weak; - bool m_array_extensional; - unsigned m_array_laziness; - bool m_array_delay_exp_axiom; - bool m_array_cg; - bool m_array_always_prop_upward; - bool m_array_lazy_ieq; - unsigned m_array_lazy_ieq_delay; - bool m_array_fake_support; // 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) { - } + bool m_array_canonize_simplify = false; + bool m_array_simplify = true; // temporary hack for disabling array simplifier plugin. + array_solver_id m_array_mode = array_solver_id::AR_FULL; + bool m_array_weak = false; + bool m_array_extensional = true; + unsigned m_array_laziness = 1; + bool m_array_delay_exp_axiom = true; + bool m_array_cg = false; + bool m_array_always_prop_upward = true; + bool m_array_lazy_ieq = false; + unsigned m_array_lazy_ieq_delay = 10; + bool m_array_fake_support = false; // fake support for all array operations to pretend they are satisfiable. + theory_array_params() {} void updt_params(params_ref const & _p); diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index 1fc477c79..57ec16b6a 100644 --- a/src/smt/params/theory_bv_params.h +++ b/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; - bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. - bool m_bv_reflect; - bool m_bv_lazy_le; - bool m_bv_cc; - bool m_bv_eq_axioms; - unsigned m_bv_blast_max_size; - bool m_bv_enable_int2bv2int; - bool m_bv_watch_diseq; - bool m_bv_delay; - 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) { + bv_solver_id m_bv_mode = bv_solver_id::BS_BLASTER; + 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 = true; + bool m_bv_lazy_le = false; + bool m_bv_cc = false; + bool m_bv_eq_axioms = true; + unsigned m_bv_blast_max_size = INT_MAX; + bool m_bv_enable_int2bv2int = true; + bool m_bv_watch_diseq = false; + bool m_bv_delay = true; + theory_bv_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h index a706f844b..2922ca5ef 100644 --- a/src/smt/params/theory_pb_params.h +++ b/src/smt/params/theory_pb_params.h @@ -22,12 +22,11 @@ Revision History: struct theory_pb_params { - unsigned m_pb_conflict_frequency; - bool m_pb_learn_complements; - theory_pb_params(params_ref const & p = params_ref()): - m_pb_conflict_frequency(1000), - m_pb_learn_complements(true) - {} + unsigned m_pb_conflict_frequency = 1000; + bool m_pb_learn_complements = true; + theory_pb_params(params_ref const & p = params_ref()) { + updt_params(p); + } void updt_params(params_ref const & p); diff --git a/src/smt/params/theory_seq_params.h b/src/smt/params/theory_seq_params.h index 002d6c9e6..84437fa15 100644 --- a/src/smt/params/theory_seq_params.h +++ b/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_seq_validate; + bool m_split_w_len = false; + bool m_seq_validate = false; - - theory_seq_params(params_ref const & p = params_ref()): - m_split_w_len(false), - m_seq_validate(false) - { + theory_seq_params(params_ref const & p = params_ref()) { updt_params(p); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 971f4ba18..0dd5e51f6 100644 --- a/src/smt/params/theory_str_params.h +++ b/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()): - 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) - { + theory_str_params(params_ref const & p = params_ref()) { updt_params(p); }