Struct Solver 

pub struct Solver { /* private fields */ }

Available on crate feature solver only.

Main CDCL(T) SMT Solver

Implementations

impl Solver

pub fn new() -> Solver

Create a new solver

pub fn with_config(config: SolverConfig) -> Solver

Create a new solver with configuration

pub fn get_proof(&self) -> Option<&Proof>

Get the proof (if proof generation is enabled and the result is unsat)

pub fn get_statistics(&self) -> &Statistics

Get the solver statistics

pub fn reset_statistics(&mut self)

Reset the solver statistics

pub fn set_theory_aware_branching(&mut self, enabled: bool)

Enable or disable theory-aware branching

pub fn theory_aware_branching(&self) -> bool

Check if theory-aware branching is enabled

pub fn set_produce_unsat_cores(&mut self, produce: bool)

Enable or disable unsat core production

pub fn set_logic(&mut self, logic: &str)

Set the logic

pub fn assert(&mut self, term: TermId, manager: &mut TermManager)

Assert a term

pub fn assert_named( &mut self, term: TermId, name: &str, manager: &mut TermManager, )

Assert a named term (for unsat core tracking)

pub fn get_unsat_core(&self) -> Option<&UnsatCore>

Get the unsat core (after check() returned Unsat)

pub fn check(&mut self, manager: &mut TermManager) -> SolverResult

Check satisfiability

pub fn check_with_assumptions( &mut self, assumptions: &[TermId], manager: &mut TermManager, ) -> SolverResult

Check satisfiability under assumptions Assumptions are temporary constraints that don’t modify the assertion stack

pub fn check_sat_only(&mut self, manager: &mut TermManager) -> SolverResult

Check satisfiability (pure SAT, no theory integration) Useful for benchmarking or when theories are not needed

pub fn enable_assumption_based_cores(&mut self)

Enable assumption-based unsat core tracking This creates assumption variables for each assertion which can be used to efficiently extract minimal unsat cores

pub fn minimize_unsat_core( &mut self, manager: &mut TermManager, ) -> Option<UnsatCore>

Minimize an unsat core using greedy deletion This creates a minimal (but not necessarily minimum) unsatisfiable subset

pub fn model(&self) -> Option<&Model>

Get the model (if sat)

pub fn assert_many(&mut self, terms: &[TermId], manager: &mut TermManager)

Assert multiple terms at once This is more efficient than calling assert() multiple times

pub fn num_assertions(&self) -> usize

Get the number of assertions in the solver

pub fn num_variables(&self) -> usize

Get the number of variables in the SAT solver

pub fn has_assertions(&self) -> bool

Check if the solver has any assertions

pub fn context_level(&self) -> usize

Get the current context level (push/pop depth)

pub fn push(&mut self)

Push a context level

pub fn pop(&mut self)

Pop a context level using trail-based undo

pub fn reset(&mut self)

Reset the solver

pub fn config(&self) -> &SolverConfig

Get the configuration

pub fn set_config(&mut self, config: SolverConfig)

Set configuration

pub fn stats(&self) -> &SolverStats

Get solver statistics

Trait Implementations

impl Debug for Solver

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for Solver

fn default() -> Solver

Returns the “default value” for a type.