From d766292dab83acbe32750dfb04af8b17421b21ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 May 2025 18:02:51 +0100 Subject: [PATCH] add seed parameter, fix trail undo order from insertion to ensure lifetime --- src/ast/simplifiers/randomizer.h | 12 +++++++----- src/params/tactic_params.pyg | 1 + 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifiers/randomizer.h b/src/ast/simplifiers/randomizer.h index cc8c663d4..dd3a7a630 100644 --- a/src/ast/simplifiers/randomizer.h +++ b/src/ast/simplifiers/randomizer.h @@ -22,6 +22,7 @@ Author: #include "ast/ast_pp.h" #include "ast/simplifiers/dependent_expr_state.h" #include "util/obj_hashtable.h" +#include "params/tactic_params.hpp" #include class randomizer_simplifier : public dependent_expr_simplifier { @@ -40,13 +41,13 @@ class randomizer_simplifier : public dependent_expr_simplifier { std::string rand_name = f->get_name().str() + "_rand_" + std::to_string(m_rand()); symbol new_sym(rand_name.c_str()); r = m.mk_func_decl(new_sym, f->get_arity(), f->get_domain(), f->get_range()); - m_rename.insert(f, r); m_ast_trail.push_back(r); m_ast_trail.push_back(f); - + m_rename.insert(f, r); + + m_trail.push(push_back_vector(m_ast_trail)); + m_trail.push(push_back_vector(m_ast_trail)); m_trail.push(insert_obj_map(m_rename, f)); - m_trail.push(push_back_vector(m_ast_trail)); - m_trail.push(push_back_vector(m_ast_trail)); m_args.reset(); @@ -115,7 +116,8 @@ class randomizer_simplifier : public dependent_expr_simplifier { public: randomizer_simplifier(ast_manager& m, params_ref const & p, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m(m), m_ast_trail(m), m_new_exprs(m) { - // set m_rand reading from parameter? + tactic_params tp(p); + m_rand.set_seed(tp.randomizer_seed()); // set random seed from parameter } char const* name() const override { return "randomizer"; } diff --git a/src/params/tactic_params.pyg b/src/params/tactic_params.pyg index 1614987dd..40ea5f535 100644 --- a/src/params/tactic_params.pyg +++ b/src/params/tactic_params.pyg @@ -11,6 +11,7 @@ def_module_params('tactic', ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."), ('lia2card.max_range', UINT, 100, "maximal range of integers to compilation into Booleans"), ('lia2card.max_ite_nesting', UINT, 4, "maximal nesting depth for ite expressions to be compiled into PB constraints"), + ('randomizer.seed', UINT, 0, "seed for randomizer pre-processor"), ('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"), # ('aig.per_assertion', BOOL, True, "process one assertion at a time"),