Module solver 

Modules

hard_arith_fallback 🔒

monotonic_product 🔒

normalize 🔒

Structs

PortfolioDiagnostics

PortfolioScheduler 🔒

ScheduledSolver 🔒

SmtLibSubprocessSolver 🔒

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

cache_key_bool 🔒

Returns a conservative canonical boolean expression for cache-key equality.

cache_key_cmp 🔒

Returns a conservative canonical comparison for cache-key equality.

cache_key_expr 🔒

Returns a conservative canonical word expression for cache-key equality.

collect_cache_key_conjunct 🔒

Collects cache-key conjuncts, flattening conjunctions because path constraints are conjunctive.

constraint_cache_key 🔒

Returns a structural key for normalized solver cache lookups.

constraints_are_directly_unsat 🔒

Returns whether normalized conjunctive constraints contain a direct contradiction.

expr_op_is_commutative 🔒

Returns whether a word operation is safe to reorder for cache-key equality.

first_solver_line 🔒

format_solver_portfolio_summaries 🔒

Formats solver portfolio outcome diagnostics.

join_pipe_output 🔒

kill_and_reap_solver_process 🔒

merge_counts 🔒

model_satisfies_constraints 🔒

Returns whether a parsed model satisfies the current original 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.

parse_and_validate_model 🔒

parse_model 🔒

Returns the parse_model solver helper result.

portfolio_launch_delay 🔒

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

read_pipe_to_string 🔒

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.

sorted_bool_exprs_are_subset 🔒

Returns whether every expression in sorted subset appears in sorted superset.

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 🔒