reduce use of symbols in gparams

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

scripts/mk_genfile_common.py

@@ -644,7 +644,7 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
     for code in cmds:
         fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code)
     for (mod, code) in mod_cmds:
-        fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod))
+        fout.write('{ std::function<param_descrs *(void)> f = []() { auto* d = alloc(param_descrs); %s(*d); return d; }; gparams::register_module("%s", f); }\n' % (code, mod))
     for (mod, descr) in mod_descrs:
         fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr))
     fout.write('}\n')

src/util/gparams.cpp

@@ -17,9 +17,11 @@ Notes:
 
 --*/
 #include "util/gparams.h"
-#include "util/dictionary.h"
+#include "util/str_hashtable.h"
 #include "util/trace.h"
 #include "util/mutex.h"
+#include "util/region.h"
+#include "util/map.h"
 
 static DECLARE_MUTEX(gparams_mux);
 
@@ -28,7 +30,7 @@ extern void gparams_register_modules();
 static char const * g_old_params_names[] = {
     "arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", nullptr };
 
-static bool is_old_param_name(symbol const & name) {
+static bool is_old_param_name(std::string const & name) {
     char const * const * it = g_old_params_names;
     while (*it) {
         if (name == *it)
@@ -69,7 +71,7 @@ static char const * g_params_renames[] = {
     "pp_min_alias_size", "pp.min_alias_size",
     nullptr };
 
-static char const * get_new_param_name(symbol const & p) {
+static char const * get_new_param_name(std::string const & p) {
     char const * const * it = g_params_renames;
     while (*it) {
         if (p == *it) {
@@ -81,13 +83,60 @@ static char const * get_new_param_name(symbol const & p) {
     return nullptr;
 }
 
+template <typename T>
+class smap : public map<char const*, T, str_hash_proc, str_eq_proc> {};
+
+typedef std::function<param_descrs*(void)> lazy_descrs_t;
+
+class lazy_param_descrs {
+    param_descrs*      m_descrs;
+    ptr_vector<lazy_descrs_t>      m_mk;
+
+    void apply(lazy_descrs_t& f) {
+        param_descrs* d = f();
+        if (m_descrs) {
+            m_descrs->copy(*d);
+            dealloc(d);            
+        }
+        else {
+            m_descrs = d;
+        }
+    }
+    
+    void reset_mk() {
+        for (auto* f : m_mk) dealloc(f);
+        m_mk.reset();
+    }
+
+public:
+    lazy_param_descrs(lazy_descrs_t& f): m_descrs(nullptr) {
+        append(f);
+    }
+
+    ~lazy_param_descrs() { 
+        dealloc(m_descrs);  
+        reset_mk();
+    }
+
+    param_descrs* deref() {
+        for (auto* f : m_mk) apply(*f);
+        reset_mk();        
+        return m_descrs;
+    }
+
+    void append(lazy_descrs_t& f) {
+        m_mk.push_back(alloc(lazy_descrs_t, f));        
+    }
+};
+
 struct gparams::imp {
-    bool                      m_modules_registered;
+    bool                 m_modules_registered;
-    dictionary<param_descrs*> m_module_param_descrs;
+    smap<lazy_param_descrs*> m_module_param_descrs;
-    dictionary<char const *>  m_module_descrs;
+    smap<char const *>   m_module_descrs;
-    param_descrs              m_param_descrs;
+    param_descrs         m_param_descrs;
-    dictionary<params_ref *>  m_module_params;
+    smap<params_ref* >   m_module_params;
-    params_ref                m_params;
+    params_ref           m_params;
+    region               m_region;
 
     void check_registered() {
         if (m_modules_registered)
@@ -96,10 +145,29 @@ struct gparams::imp {
         gparams_register_modules();
     }
 
-    dictionary<param_descrs*> & get_module_param_descrs() { check_registered(); return m_module_param_descrs; }
+    smap<lazy_param_descrs*> & get_module_param_descrs() { 
-    dictionary<char const *> & get_module_descrs() { check_registered(); return m_module_descrs; }
+        check_registered(); return m_module_param_descrs; 
+    }
+
+    smap<char const *> & get_module_descrs() { check_registered(); return m_module_descrs; }
     param_descrs & get_param_descrs() { check_registered(); return m_param_descrs; }
 
+    char * cpy(char const* s) {
+        char * r = new (m_region) char[strlen(s)+1];
+        memcpy(r, s, strlen(s)+1);
+        return r;
+    }
+
+    bool get_module_param_descr(std::string const& m, param_descrs*& d) {
+        return get_module_param_descr(m.c_str(), d);
+    }
+
+    bool get_module_param_descr(char const* m, param_descrs*& d) {
+        check_registered(); 
+        lazy_param_descrs* ld;
+        return m_module_param_descrs.find(m, ld) && (d = ld->deref(), true);
+    }
+
 public:
     imp():
         m_modules_registered(false) {
@@ -119,6 +187,7 @@ public:
             dealloc(kv.m_value);
         }
         m_module_params.reset();        
+        m_region.reset();
     }
 
     // -----------------------------------------------
@@ -134,24 +203,26 @@ public:
         m_param_descrs.copy(d);
     }
 
-    void register_module(char const * module_name, param_descrs * d) {
+    void register_module(char const * module_name, lazy_descrs_t& f) {
         // Don't need synchronization here, this method
         // is invoked from check_registered that is already protected.
-        symbol s(module_name);
+        
-        param_descrs * old_d;
+        lazy_param_descrs * ld;
-        if (m_module_param_descrs.find(s, old_d)) {
+        if (m_module_param_descrs.find(module_name, ld)) {
-            old_d->copy(*d);
+            ld->append(f);
-            dealloc(d);
         }
         else {
-            m_module_param_descrs.insert(s, d);
+            ld = alloc(lazy_param_descrs, f);
+            m_module_param_descrs.insert(cpy(module_name), ld);
         }
     }
 
     void register_module_descr(char const * module_name, char const * descr) {
         // Don't need synchronization here, this method
         // is invoked from check_registered that is already protected.
-        m_module_descrs.insert(symbol(module_name), descr);
+        if (!m_module_descrs.contains(module_name)) {
+            m_module_descrs.insert(cpy(module_name), descr);
+        }
     }
 
     // -----------------------------------------------
@@ -160,7 +231,7 @@ public:
     //
     // -----------------------------------------------
 
-    void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) {
+    void normalize(char const * name, /* out */ std::string & mod_name, /* out */ std::string & param_name) {
         if (*name == ':')
             name++;
         std::string tmp = name;
@@ -175,31 +246,31 @@ public:
             if (tmp[i] == '.') {
                 param_name = tmp.c_str() + i + 1;
                 tmp.resize(i);
-                mod_name   = tmp.c_str();
+                mod_name   = tmp;
                 return;
             }
         }
-        param_name = tmp.c_str();
+        param_name = tmp;
-        mod_name   = symbol::null;
+        mod_name   = "";
     }
 
-    params_ref & get_params(symbol const & mod_name) {
+    params_ref & get_params(std::string const& mod_name) {
-        if (mod_name == symbol::null) {
+        if (!mod_name[0]) {
             return m_params;
         }
         else {
             params_ref * p = nullptr;
-            if (!m_module_params.find(mod_name, p)) {
+            if (!m_module_params.find(mod_name.c_str(), p)) {
                 p = alloc(params_ref);
-                m_module_params.insert(mod_name, p);
+                m_module_params.insert(cpy(mod_name.c_str()), p);                
             }
-            SASSERT(p != 0);
+            SASSERT(p);
             return *p;
         }
     }
 
-    void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) {
+    void throw_unknown_parameter(std::string const& param_name, param_descrs const& d, std::string const& mod_name) {
-        if (mod_name == symbol::null) {
+        if (!mod_name[0]) {
             char const * new_name = get_new_param_name(param_name);
             if (new_name) {
                 std::stringstream strm;
@@ -232,8 +303,8 @@ public:
         }
     }
 
-    void validate_type(symbol const& name, char const* value, param_descrs const& d) {
+    void validate_type(std::string& name, char const* value, param_descrs const& d) {
-        param_kind k = d.get_kind(name);
+        param_kind k = d.get_kind(name.c_str());
         std::stringstream strm;
         char const* _value = value;
         switch (k) {
@@ -269,11 +340,12 @@ public:
     }
 
 
-    void set(param_descrs const & d, symbol const & param_name, char const * value, symbol const & mod_name) {
+    void set(param_descrs const & d, std::string const & _param_name, char const * value, std::string const & mod_name) {
+        char const* param_name = _param_name.c_str();
         param_kind k = d.get_kind(param_name);
         params_ref & ps = get_params(mod_name);
         if (k == CPK_INVALID) {
-            throw_unknown_parameter(param_name, d, mod_name);
+            throw_unknown_parameter(_param_name, d, mod_name);
         }
         else if (k == CPK_UINT) {
             long val = strtol(value, nullptr, 10);
@@ -294,7 +366,7 @@ public:
             else {
                 std::stringstream strm;
                 strm << "invalid value '" << value << "' for Boolean parameter '" << param_name << "'";                
-                if (mod_name == symbol::null) {
+                if (mod_name[0]) {
                     strm << " at module '" << mod_name << "'";
                 }
                 throw default_exception(strm.str());
@@ -305,20 +377,13 @@ public:
         }
         else if (k == CPK_STRING) {
             // There is no guarantee that (external) callers will not delete value after invoking gparams::set.
-            // I see two solutions:
+            // the value is copied to internal region.
-            //    1) Modify params_ref to create a copy of set_str parameters.
+            ps.set_str(param_name, cpy(value));
-            //       This solution is not nice since we create copies and move the params_ref around.
-            //       We would have to keep copying the strings.
-            //       Moreover, when we use params_ref internally, the value is usually a static value. 
-            //       So, we would be paying this price for nothing.
-            //    2) "Copy" value by transforming it into a symbol. 
-            //       I'm using this solution for now.
-            ps.set_str(param_name, symbol(value).bare_str());
         }
         else {
             std::stringstream strm;
             strm << "unsupported parameter type '" << param_name << "'";            
-            if (mod_name == symbol::null) {
+            if (mod_name[0]) {
                 strm << " at module '" << mod_name << "'";            
             }
             throw exception(strm.str());
@@ -326,16 +391,16 @@ public:
     }
 
     void set(char const * name, char const * value) {
-        lock_guard lock(*gparams_mux);
+        std::string m, p;
-        symbol m, p;
         normalize(name, m, p);
-        if (m == symbol::null) {
+        lock_guard lock(*gparams_mux);
+        if (!m[0]) {
             validate_type(p, value, get_param_descrs());
             set(get_param_descrs(), p, value, m);
         }
         else {
             param_descrs * d;
-            if (get_module_param_descrs().find(m, d)) {
+            if (get_module_param_descr(m, d)) {
                 validate_type(p, value, *d);
                 set(*d, p, value, m);
             }
@@ -347,28 +412,31 @@ public:
         }
     }
 
-    std::string get_value(params_ref const & ps, symbol const & p) {
+    std::string get_value(params_ref const & ps, std::string const & p) {
+        symbol sp(p.c_str());
         std::ostringstream buffer;
-        ps.display(buffer, p);
+        ps.display(buffer, sp);
         return buffer.str();
     }
 
-    std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) {
+    std::string get_default(param_descrs const & d, std::string const & p, std::string const & m) {
-        if (!d.contains(p)) {
+        symbol sp(p.c_str());
+        if (!d.contains(sp)) {
             throw_unknown_parameter(p, d, m);
         }
-        char const * r = d.get_default(p);
+        char const * r = d.get_default(sp);
         if (r == nullptr)
             return "default";
         return r;
     }
 
     std::string get_value(char const * name) {
-        lock_guard lock(*gparams_mux);
+        std::string m, p;
-        symbol m, p;
         normalize(name, m, p);
-        if (m == symbol::null) {
+        lock_guard lock(*gparams_mux);
-            if (m_params.contains(p)) {
+        symbol sp(p.c_str());
+        if (!m[0]) {
+            if (m_params.contains(sp)) {
                 return get_value(m_params, p);
             }
             else {
@@ -377,12 +445,12 @@ public:
         }
         else {
             params_ref * ps = nullptr;
-            if (m_module_params.find(m, ps) && ps->contains(p)) {
+            if (m_module_params.find(m.c_str(), ps) && ps->contains(sp)) {
                 return get_value(*ps, p);
             }
             else {
                 param_descrs * d;
-                if (get_module_param_descrs().find(m, d)) {
+                if (get_module_param_descr(m, d)) {
                     return get_default(*d, p, m);
                 }
             }
@@ -394,7 +462,7 @@ public:
 
     // unfortunately, params_ref is not thread safe
     // so better create a local copy of the parameters.
-    params_ref get_module(symbol const & module_name) {
+    params_ref get_module(char const* module_name) {
         params_ref result;
         params_ref * ps = nullptr;
         {
@@ -433,7 +501,8 @@ public:
                 out << ", description: " << descr;
             }
             out << "\n";
-            kv.m_value->display(out, indent + 4, smt2_style, include_descr);
+            auto* d = kv.m_value->deref();
+            d->display(out, indent + 4, smt2_style, include_descr);
         }
     }
 
@@ -449,10 +518,10 @@ public:
         }
     }
 
-    void display_module(std::ostream & out, symbol const & module_name) {
+    void display_module(std::ostream & out, char const* module_name) {
         lock_guard lock(*gparams_mux);
         param_descrs * d = nullptr;
-        if (!get_module_param_descrs().find(module_name, d)) {
+        if (!get_module_param_descr(module_name, d)) {
             std::stringstream strm;
             strm << "unknown module '" << module_name << "'";                    
             throw exception(strm.str());
@@ -466,110 +535,108 @@ public:
         d->display(out, 4, false);
     }
 
-    void display_parameter(std::ostream & out, char const * name) {
+    void display_parameter(std::ostream & out, char const * name) {        
-        lock_guard lock(*gparams_mux);
+        std::string m, p;
-        symbol m, p;
         normalize(name, m, p);
+        symbol sp(p.c_str());
+        lock_guard lock(*gparams_mux);
         out << name << " " << m << " " << p << "\n";
         param_descrs * d;
-        if (m == symbol::null) {
+        if (!m[0]) {
             d = &get_param_descrs();
         }
         else {
-            if (!get_module_param_descrs().find(m, d)) {
+            if (!get_module_param_descr(m, d)) {
                 std::stringstream strm;
                 strm << "unknown module '" << m << "'";                    
                 throw exception(strm.str());
             }
         }
-        if (!d->contains(p))
+        if (!d->contains(sp))
             throw_unknown_parameter(p, *d, m);
         out << "  name:           " << p << "\n";
-        if (m != symbol::null) {
+        if (m[0]) {
             out << "  module:         " << m << "\n";
             out << "  qualified name: " << m << "." << p << "\n";
         }
-        out << "  type:           " << d->get_kind(p) << "\n";
+        out << "  type:           " << d->get_kind(sp) << "\n";
-        out << "  description:    " << d->get_descr(p) << "\n";
+        out << "  description:    " << d->get_descr(sp) << "\n";
-        out << "  default value:  " << d->get_default(p) << "\n";
+        out << "  default value:  " << d->get_default(sp) << "\n";
     }
 };
 
 gparams::imp * gparams::g_imp = nullptr;
 
 void gparams::reset() {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->reset();
 }
 
 void gparams::set(char const * name, char const * value) {
     TRACE("gparams", tout << "setting [" << name << "] <- '" << value << "'\n";);
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->set(name, value);
 }
 
 void gparams::set(symbol const & name, char const * value) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->set(name.bare_str(), value);
 }
 
 std::string gparams::get_value(char const * name) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     return g_imp->get_value(name);
 }
 
 std::string gparams::get_value(symbol const & name) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     return g_imp->get_value(name.bare_str());
 }
 
 void gparams::register_global(param_descrs & d) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->register_global(d);
 }
 
-void gparams::register_module(char const * module_name, param_descrs * d) {
+void gparams::register_module(char const * module_name, lazy_descrs_t& f) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
-    g_imp->register_module(module_name, d);
+    g_imp->register_module(module_name, f);
 }
 
 void gparams::register_module_descr(char const * module_name, char const * descr) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->register_module_descr(module_name, descr);
 }
 
 params_ref gparams::get_module(char const * module_name) {
-    return get_module(symbol(module_name));
+    SASSERT(g_imp);
-}
-
-params_ref gparams::get_module(symbol const & module_name) {
-    SASSERT(g_imp != 0);
     return g_imp->get_module(module_name);
 }
 
+
 params_ref const& gparams::get_ref() {
     TRACE("gparams", tout << "gparams::get_ref()\n";);
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     return g_imp->get_ref();
 }
 
 void gparams::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->display(out, indent, smt2_style, include_descr);
 }
 
 void gparams::display_modules(std::ostream & out) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->display_modules(out);
 }
 
 void gparams::display_module(std::ostream & out, char const * module_name) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
-    g_imp->display_module(out, symbol(module_name));
+    g_imp->display_module(out, module_name);
 }
 
 void gparams::display_parameter(std::ostream & out, char const * name) {
-    SASSERT(g_imp != 0);
+    SASSERT(g_imp);
     g_imp->display_parameter(out, name);
 }
 

src/util/gparams.h

@@ -82,7 +82,9 @@ public:
        "tells" the automatic code generator how to register the parameters for the given
        module.
     */
-    static void register_module(char const * module_name, param_descrs * d); 
+
+    typedef std::function<param_descrs*(void)> lazy_descrs_t;
+    static void register_module(char const* module_name, lazy_descrs_t& get_descrs);
 
     /**
        \brief Add a (small) description to the given module.
@@ -101,8 +103,6 @@ public:
        params_ref const & p = get_module_params("pp")
     */
     static params_ref get_module(char const * module_name);
-    static params_ref get_module(symbol const & module_name);
-
     /**
        \brief Return the global parameter set (i.e., parameters that are not associated with any particular module).
     */