Struct SatSolver 

pub struct SatSolver { /* private fields */ }

A constraint problem as a CNF, ready to be searched and sampled.

Implementations

impl SatSolver

pub fn new( var_tys: &[Ty], states: &[Option<BigUint>], conjuncts: &[Expr], ) -> Result<SatSolver, SolveError>

Blasts the conjunction of conjuncts over variables of types var_tys (state variables fixed to states, as super::bdd::compile) with the default SatLimits.

pub fn with_limits( var_tys: &[Ty], states: &[Option<BigUint>], conjuncts: &[Expr], limits: SatLimits, ) -> Result<SatSolver, SolveError>

As SatSolver::new with explicit limits.

pub fn num_clauses(&self) -> usize

The number of clauses of the CNF.

pub fn is_contradiction(&self) -> bool

Whether the CNF is trivially contradictory (a conjunct folded to false).

pub fn accepts(&self, values: &[BigUint]) -> Result<bool, SolveError>

Whether the assignment values (one per variable) is a model, decided by the CNF and the solver (so it tests the encoding, unlike eval).

pub fn sample( &self, order: &[VarId], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>

Draws one legal assignment, fixing variables in order, then any variable order omits in id order. Approximately uniform (module docs).

pub fn sample_groups( &self, groups: &[Vec<VarId>], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>

As super::solve::Solver::sample_groups.

pub fn sample_plan( &self, plan: &Plan, randc_states: &mut [RandcState], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>

Draws one assignment following plan, as super::solve::Solver::sample_plan but with the SAT sampler’s approximate uniformity and limits (module docs). randc_states is advanced only for variables that were drawn.

Trait Implementations

impl Debug for SatSolver

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

Formats the value using the given formatter.