Module solver 

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

Re-exports

use std::io::BufRead; 🔒

use std::io::BufReader; 🔒

use std::io::Read; 🔒

use std::process::Child; 🔒

use std::process::ChildStdin; 🔒

use std::process::Output; 🔒

use std::sync::mpsc::Receiver; 🔒

use std::sync::mpsc::RecvTimeoutError; 🔒

use std::thread::JoinHandle; 🔒

use wait_timeout::ChildExt; 🔒

use fallback::checked_mul_guard_branch_model; 🔒

use fallback::constraints_prefer_hard_arith_fallback_first; 🔒

use normalize::NormalizationCache; 🔒

use normalize::constraints_are_directly_unsat; 🔒

use normalize::normalize_constraints_for_solver_cached; 🔒

use normalize::sorted_bool_exprs_are_subset; 🔒

use reasoning::CheckedXorResult; 🔒

use reasoning::checked_xor_result; 🔒

use reasoning::product_monotonic_unsat_normalized; 🔒

use reasoning::remove_implied_monotonic_constraints; 🔒

use smt::write_smt_assertions; 🔒

use super::*; 🔒

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

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

cache_result 🔒

collect_solver_vars 🔒

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

fallback_bounded_model 🔒

Searches a bounded Cartesian portfolio and returns only an evaluator-validated SAT witness.

fallback_single_var_model 🔒

format_solver_portfolio_summaries 🔒

Formats solver portfolio outcome diagnostics.

hard_arith_fallback_model 🔒

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_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_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.