mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 09:11:17 +00:00
Code Activity

Register max_bv_sharing simplifier via ADD_SIMPLIFIER

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 23:26:47 +00:00
parent db533abed5
commit ce905f91c3
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/max_bv_sharing.h
View file

@ -23,3 +23,7 @@ Author:
#include "ast/simplifiers/dependent_expr_state.h"
dependent_expr_simplifier * mk_max_bv_sharing(ast_manager & m, params_ref const & p, dependent_expr_state& fmls);
/*
ADD_SIMPLIFIER("max-bv-sharing", "use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.", "mk_max_bv_sharing(m, p, s)")
*/