mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

add seed parameter, fix trail undo order from insertion to ensure lifetime

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-27 18:02:51 +01:00
parent b44c897a59
commit d766292dab
2 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/simplifiers/randomizer.h
View file

@ -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 <algorithm>
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"; }

1
src/params/tactic_params.pyg
View file

@ -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"),