Module solver 

Solver orchestration, query scheduling, caching, and model validation.

Modules

fallback 🔒

Bounded fallback model generation for hard arithmetic constraints.

normalize 🔒

Constraint and expression normalization for solver queries.

reasoning 🔒

Lightweight reasoning passes over normalized solver constraints.

smt 🔒

Query-level SMT-LIB assertion emission with common-subexpression bindings.

Structs

PortfolioDiagnostics

PortfolioScheduler 🔒

ScheduledSolver 🔒

SmtLibSubprocessSolver 🔒

SolverChild 🔒

SolverCommand 🔒

SolverCommandRun 🔒

SolverProcessResult 🔒

SolverRunSummary 🔒

Z3Session 🔒

Enums

BranchFeasibility 🔒

PortfolioSchedulerSignal 🔒

SolverConfigError 🔒

Errors that arise when parsing or constructing solver commands from configuration.

SolverOutcome 🔒

SolverProcessOutcome 🔒

Constants

Z3_QUERY_END 🔒

Functions

collect_solver_vars 🔒

Collects variables as the SMT writer sees them, stopping at opaque hash leaves.

first_solver_line 🔒

format_solver_portfolio_summaries 🔒

Formats solver portfolio outcome diagnostics.

merge_counts 🔒

model_satisfies_constraints 🔒

Returns whether a parsed model satisfies the current original constraints.

model_symbols_for_constraints 🔒

named_solver_command 🔒

Returns the default command for a known solver name.

next_portfolio_launch_wait 🔒

Returns how long the supervisor can wait before the next pending solver is due.

normalize_sat_constraints 🔒

Normalizes satisfiability constraints and removes soundly redundant constraints.

parse_and_validate_model 🔒

parse_model_values 🔒

parse_model_with_symbol 🔒

parse_model_with_symbols 🔒

portfolio_launch_delay 🔒

Returns when the solver at index should be started, relative to query start.

remove_witnessed_isolated_hash_constraints 🔒

Removes independently satisfiable constraints over one opaque hash symbol.

run_solver_commands 🔒

Runs one or more solver commands and returns the first decisive SMT-LIB response.

run_solver_process 🔒

Runs one solver process to completion, timeout, or cooperative cancellation.

scheduled_portfolio 🔒

Returns the staged launch plan for a configured portfolio.

solver_command_availability_error 🔒

Returns why command is not currently executable as an SMT solver.

solver_command_for_portfolio_entry 🔒

Returns the command for one configured portfolio entry.

solver_commands_for_config 🔒

Returns the subprocess commands for the configured SMT solver setup.

solver_exit_error 🔒

solver_output_is_sat 🔒

solver_output_is_unknown 🔒

solver_output_is_unsat 🔒

solver_portfolio_availability_warning 🔒

Returns a warning when a configured portfolio will run with unavailable solver entries.

solver_wait_duration 🔒

spawn_solver_process 🔒

split_solver_command 🔒

Splits a shell-like solver command into argv parts.

summary_for_cancelled_solver_result 🔒

Summarizes a solver result received after a portfolio winner was chosen.

summary_for_unstarted_solver 🔒

Summarizes a solver that was never launched because the portfolio already won.

validate_solver_model_output 🔒

validated_hard_arith_fallback_model 🔒

Returns a hard-arithmetic fallback model only after validating it against original constraints.

Type Aliases

QueryObserver 🔒