Module fallback 

Bounded fallback model generation for hard arithmetic constraints.

Structs

FallbackSearch 🔒

MaskHints 🔒

Constants

MAX_CHECKED_MUL_SUPPORT_VISITS 🔒

Functions

add_zero_invalid_support_vars 🔒

assign_checked_add_base 🔒

assign_checked_sub_minuend 🔒

bool_expr_binds_single_var 🔒

bool_expr_has_two_var_relation 🔒

charge_support_constraint 🔒

checked_mul_guard_branch 🔒

checked_mul_guard_branch_model 🔒

Constructs and validates a concrete model for a checked-multiply guard branch.

checked_mul_guard_conjunction 🔒

checked_mul_guard_operands 🔒

checked_mul_guard_word_comparison 🔒

collect_bool_constants 🔒

collect_bool_fallback_vars 🔒

collect_bool_hard_arith_vars 🔒

collect_expr_fallback_vars 🔒

complete_checked_add_guard 🔒

complete_checked_sub_guard 🔒

complete_default_support_comparison 🔒

complete_default_support_constraint 🔒

complete_fallback_support_model 🔒

complete_model_with_zeroes 🔒

complete_support_bool 🔒

complete_support_comparison 🔒

complete_support_constraint 🔒

complete_support_constraints_once 🔒

constraints_bind_each_search_var 🔒

constraints_have_two_var_relation 🔒

constraints_prefer_hard_arith_fallback_first 🔒

Returns whether local hard-arithmetic search should run before asking the solver.

expr_contains_const 🔒

fallback_candidates_for_var 🔒

fallback_partial_model_satisfies_known_constraints 🔒

fallback_search_vars 🔒

fallback_single_var_model 🔒

fallback_two_var_model 🔒

hard_arith_fallback_model 🔒

hard_arith_fallback_vars 🔒

is_hard_arith_node 🔒

is_single_bit 🔒

propagate_fallback_support_constraints 🔒

push_fallback_candidate 🔒

seed_bounded_support_vars 🔒

Seeds only unassigned scalar variables; every resulting witness is still fully validated.

support_cmp_op 🔒

support_target_for_known_left 🔒

support_target_for_known_right 🔒

zero_mask_equality 🔒