Module hard_arith_fallback 

Structs

FallbackSearch 🔒

Holds immutable state for recursive hard-arithmetic fallback search.

MaskHints 🔒

Functions

bool_contains_hard_arith 🔒

Returns the bool_contains_hard_arith solver helper result.

bool_contains_symbolic_hash 🔒

Returns whether the boolean expression contains symbolic hash variables.

bool_contains_var 🔒

Returns the bool_contains_var solver helper result.

collect_bool_constants 🔒

Implements the collect_bool_constants solver helper.

collect_bool_fallback_vars 🔒

Collects variables that local hard-arithmetic search can assign directly.

collect_expr_constants 🔒

Implements the collect_expr_constants solver helper.

collect_expr_fallback_vars 🔒

Collects assignable variables from an expression, recursing into recomputable hashes.

constraints_prefer_hard_arith_fallback_first 🔒

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

expr_contains_hard_arith 🔒

Returns the expr_contains_hard_arith solver helper result.

expr_contains_symbolic_hash 🔒

Returns whether the expression contains symbolic hash variables that local search should avoid.

expr_contains_var 🔒

Returns the expr_contains_var solver helper result.

fallback_candidates_for_var 🔒

Returns deterministic local-search candidates for one symbolic variable.

fallback_model_satisfies_all_constraints 🔒

Checks all constraints before returning a hard-arithmetic fallback witness.

fallback_partial_model_satisfies_known_constraints 🔒

Checks constraints that depend only on already-assigned fallback variables.

fallback_search_vars 🔒

Selects direct symbolic inputs for bounded fallback search.

hard_arith_fallback_model 🔒

Implements the hard_arith_fallback_model solver helper.

push_fallback_candidate 🔒

Applies the push_fallback_candidate solver helper.

zero_mask_equality 🔒

Implements the zero_mask_equality solver helper.