From 80c553d24a80b248c31fadbfd25a43d7ac62bc30 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 May 2025 00:20:30 +0100 Subject: [PATCH] missing file Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/randomizer.h | 146 +++++++++++++++++++++++++++++++ 1 file changed, 146 insertions(+) create mode 100644 src/ast/simplifiers/randomizer.h diff --git a/src/ast/simplifiers/randomizer.h b/src/ast/simplifiers/randomizer.h new file mode 100644 index 000000000..cc8c663d4 --- /dev/null +++ b/src/ast/simplifiers/randomizer.h @@ -0,0 +1,146 @@ + +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + randomizer.h + +Abstract: + + Simplifier that randomizes formulas by renaming uninterpreted functions and permuting arguments of associative and commutative functions. + +Author: + + Nikolaj Bjorner nbjorner 20-05-2025 + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "ast/simplifiers/dependent_expr_state.h" +#include "util/obj_hashtable.h" +#include + +class randomizer_simplifier : public dependent_expr_simplifier { + ast_manager& m; + obj_map m_rename; + ast_ref_vector m_ast_trail; + expr_ref_vector m_new_exprs; + ptr_vector m_todo, m_args; + random_gen m_rand; + + func_decl* get_random_func_decl(func_decl* f) { + func_decl* r = nullptr; + if (m_rename.find(f, r)) + return r; + // Create a new random name + 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_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(); + for (unsigned i = 0; i < f->get_arity(); ++i) + m_args.push_back(m.mk_var(i, f->get_domain(i))); + m_fmls.model_trail().hide(r); + m_fmls.model_trail().push(f, m.mk_app(r, m_args), nullptr, {}); + return r; + } + + void push_new_expr(expr* e, expr* new_e) { + m_new_exprs.setx(e->get_id(), new_e); + m_ast_trail.push_back(e); + m_trail.push(push_back_vector(m_ast_trail)); + m_trail.push(set_vector_idx_trail(m_new_exprs, e->get_id())); + m_todo.pop_back(); + } + + expr* get_new_expr(expr* e) { + return m_new_exprs.get(e->get_id(), nullptr); + } + + void randomize(expr* e) { + m_todo.push_back(e); + while (!m_todo.empty()) { + e = m_todo.back(); + if (get_new_expr(e)) + m_todo.pop_back(); + else if (is_app(e)) { + auto f = to_app(e)->get_decl(); + // If uninterpreted function, rename + if (is_uninterp(f)) + f = get_random_func_decl(f); + m_args.reset(); + auto arity = to_app(e)->get_num_args(); + for (expr* arg : *to_app(e)) { + expr* new_arg = get_new_expr(arg); + if (new_arg) + m_args.push_back(new_arg); + else + m_todo.push_back(arg); + } + if (m_args.size() < arity) + continue; + if (f->is_associative() && f->is_commutative() && arity > 1) + shuffle(m_args.size(), m_args.data(), m_rand); + expr_ref new_e(m.mk_app(f, m_args.size(), m_args.data()), m); + push_new_expr(e, new_e); + } + else if (is_quantifier(e)) { + quantifier* q = to_quantifier(e); + expr* body = q->get_expr(); + expr* new_body = get_new_expr(body); + if (new_body) { + expr_ref new_e(m.update_quantifier(q, new_body), m); + push_new_expr(e, new_e); + } + else + m_todo.push_back(body); + } + else + push_new_expr(e, e); + } + } + +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? + } + + char const* name() const override { return "randomizer"; } + + void reduce() override { + for (unsigned idx : indices()) { + auto d = m_fmls[idx]; + randomize(d.fml()); + m_fmls.update(idx, dependent_expr(m, get_new_expr(d.fml()), d.pr(), d.dep())); + } + unsigned num_fmls = qtail() - qhead(); + for (unsigned i = qhead(); i < qtail(); ++i) { + unsigned j = qhead() + m_rand(num_fmls); + if (i == j) + continue; + auto d1 = m_fmls[i]; + auto d2 = m_fmls[j]; + m_fmls.update(i, d2); + m_fmls.update(j, d1); + } + } + + bool supports_proofs() const override { return false; } +}; + +/* + ADD_SIMPLIFIER("randomizer", "shuffle assertions and rename uninterpreted functions.", "alloc(randomizer_simplifier, m, p, s)") +*/ \ No newline at end of file