Module normalize 

Constraint and expression normalization for solver queries.

Modules

polynomial 🔒

Bounded sparse-polynomial identity reasoning over EVM words.

rounding 🔒

Rounding relations between a rounded multiple and its original dividend.

Structs

ConstraintContext 🔒

Simple facts learned from the normalized conjunction currently being queried.

WordInterval 🔒

Constants

MAX_CONTEXTUAL_PASSES 🔒

MAX_LOCAL_ANALYSIS_NODES 🔒

Functions

bitwise_bool_word_fact 🔒

bool_expr_cmp 🔒

bool_structural_key 🔒

cmp_op_key 🔒

const_side_bound 🔒

constraints_are_directly_unsat 🔒

Returns whether canonically ordered normalized constraints contain a direct contradiction.

expr_binop_key 🔒

expr_ternop_key 🔒

mark_conjuncts 🔒

normalize_bool_for_solver 🔒

Normalizes one boolean expression into an equivalent, solver-friendlier form.

normalize_bool_node_for_solver 🔒

normalize_bounded_comparisons 🔒

Simplifies predicates using only the other, still-retained conjuncts.

normalize_cmp_for_solver 🔒

normalize_constraint_batch 🔒

normalize_constraints_for_solver_cached 🔒

Reuses context-free normalization results while retaining per-query contextual rewrites.

normalize_constraints_for_solver_with 🔒

normalize_expr_for_solver 🔒

Normalizes one word expression into an equivalent, solver-friendlier form.

normalize_expr_node_for_solver 🔒

normalize_ite_expr_for_solver 🔒

sort_dedup_bool_exprs 🔒

sorted_bool_exprs_are_subset 🔒

Returns whether every expression in subset appears in superset.

write_bool_structural_key 🔒

write_expr_structural_key 🔒

write_exprs_structural_key 🔒