Module solver 

Modules

hard_arith_fallback 🔒

monotonic_product 🔒

opt 🔒

Structs

PortfolioDiagnostics

PortfolioScheduler 🔒

ScheduledSolver 🔒

SmtLibSubprocessSolver 🔒

SolverChild 🔒

SolverCommand 🔒

SolverCommandRun 🔒

SolverProcessResult 🔒

SolverRunSummary 🔒

Enums

PortfolioSchedulerSignal 🔒

SolverConfigError 🔒

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

SolverOutcome 🔒

SolverProcessOutcome 🔒

Traits

SymbolicSolver 🔒

Minimal solver backend interface used by the symbolic executor.

Functions

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 implied nonlinear comparisons.

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.

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 🔒

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 🔒