Enum Engine 

pub enum Engine {
    Exact(Solver),
    Sat(SatSolver),
}

The solver randomize() uses: the exact BDD Solver when the problem fits its node budget, the approximate SatSolver when it does not (plan section 3.4, ledger XC-063). Both take the same Plan and obey the same contracts; what differs is exactness of the distribution and what the SAT side refuses (SolveError::SatUnsupported; super::sat module docs).

Variants

Exact(Solver)

The problem fit the BDD node budget: exactly uniform.

Sat(SatSolver)

It did not: approximately uniform.

Implementations

impl Engine

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

Compiles the conjunction of conjuncts with the default BDD budget and SAT limits.

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

As Engine::new with an explicit BDD node budget and SAT limits.

pub fn is_sat(&self) -> bool

Whether this problem fell back to SAT.

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

As Solver::sample_plan (exact) or SatSolver::sample_plan.

Trait Implementations

impl Debug for Engine

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

Formats the value using the given formatter.