From a1f85989eb22d34f25aaf69c2008f56929acbd08 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Jan 2025 13:16:35 -1000 Subject: [PATCH] debug with magic_call Signed-off-by: Lev Nachmanson --- src/ast/sls/sls_bv_lookahead.cpp | 2 +- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_context.cpp | 4 +-- src/util/util.h | 37 ++++++++++++++++++++++++++-- 6 files changed, 41 insertions(+), 5 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 93192aefd..c5de16d02 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -653,7 +653,7 @@ namespace sls { return false; SASSERT(is_uninterp(t)); - SASSERT(m_restore.empty()); +// SASSERT(m_restore.empty()); if (bv.is_bv(t)) { wval(t).eval = new_value; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index bfa310866..3924fa5f5 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -25,6 +25,7 @@ void smt_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams. m_random_seed = p.random_seed(); + m_magic_call = p.magic_call(); m_relevancy_lvl = p.relevancy(); m_ematching = p.ematching(); m_induction = p.induction(); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 7a14aa1da..c9d5c1328 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -92,6 +92,7 @@ struct smt_params : public preprocessor_params, unsigned m_relevancy_lvl = 2; bool m_relevancy_lemma = false; unsigned m_random_seed = 0; + unsigned m_magic_call = 0; double m_random_var_freq = 0.01; double m_inv_decay = 1.052; unsigned m_clause_decay = 1; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 23ea55af6..d1b5b407d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -5,6 +5,7 @@ def_module_params(module_name='smt', params=(('auto_config', BOOL, True, 'automatically configure solver'), ('logic', SYMBOL, '', 'logic used to setup the SMT solver'), ('random_seed', UINT, 0, 'random seed for the smt solver'), + ('magic_call', UINT, 0, 'random magic call'), ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'), ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'), ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 96b66149a..e9b819c1b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -60,8 +60,8 @@ namespace smt { m_model_generator(alloc(model_generator, m)), m_relevancy_propagator(mk_relevancy_propagator(*this)), m_user_propagator(nullptr), - m_random(p.m_random_seed), - m_flushing(false), + m_random(p.m_random_seed, p.m_magic_call), + m_flushing(false), m_lemma_id(0), m_progress_callback(nullptr), m_next_progress_sample(0), diff --git a/src/util/util.h b/src/util/util.h index 7d1265b33..a26142698 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -336,10 +336,10 @@ public: T const* end() const { return e; } }; -class random_gen { +class random_gen_orig { unsigned m_data; public: - random_gen(unsigned seed = 0): + random_gen_orig(unsigned seed = 0): m_data(seed) { } @@ -359,6 +359,39 @@ public: } }; +class random_gen { + unsigned m_data = 0; + unsigned m_calls = 0; + unsigned m_magic_call = 0; +public: + random_gen(unsigned seed = 0): + m_data(seed) { + } + random_gen(unsigned seed, unsigned magic_call): + m_data(seed), m_magic_call(magic_call) { + } + + + void set_seed(unsigned s) { m_data = s; } + + int operator()() { + if (m_magic_call && ++m_calls == m_magic_call) { + m_data = m_data * 214013L + 2531011L; + return (int)m_magic_call; + } + return ((m_data = m_data * 214013L + 2531011L) >> 16) & 0x7fff; + } + + unsigned operator()(unsigned u) { + unsigned r = static_cast((*this)()); + return r % u; + } + + static int max_value() { + return 0x7fff; + } +}; + template void shuffle(unsigned sz, T * array, random_gen & gen) { int n = sz;