pub struct Solver { /* private fields */ }Expand description
A compiled, counted constraint problem, ready to sample.
Implementations§
Source§impl Solver
impl Solver
Sourcepub fn new(
var_tys: &[Ty],
states: &[Option<BigUint>],
conjuncts: &[Expr],
) -> Result<Solver, SolveError>
pub fn new( var_tys: &[Ty], states: &[Option<BigUint>], conjuncts: &[Expr], ) -> Result<Solver, SolveError>
Compiles the conjunction of conjuncts with the default node budget.
Sourcepub fn with_budget(
var_tys: &[Ty],
states: &[Option<BigUint>],
conjuncts: &[Expr],
budget: usize,
) -> Result<Solver, SolveError>
pub fn with_budget( var_tys: &[Ty], states: &[Option<BigUint>], conjuncts: &[Expr], budget: usize, ) -> Result<Solver, SolveError>
As Solver::new with an explicit per-BDD node budget.
Sourcepub fn sample(
&self,
order: &[VarId],
seed: &mut u64,
) -> Result<Vec<BigUint>, SolveError>
pub fn sample( &self, order: &[VarId], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>
Draws one assignment uniformly from all models (module docs), fixing
variables in order, then any variable order omits in id order.
Returns one value per variable, indexed by VarId.
Sourcepub fn sample_groups(
&self,
groups: &[Vec<VarId>],
seed: &mut u64,
) -> Result<Vec<BigUint>, SolveError>
pub fn sample_groups( &self, groups: &[Vec<VarId>], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>
Draws one assignment solving the variables group by group, in the
order of groups (solve ... before, LRM 18.5.9; super::order
builds them).
Each group is sampled uniformly over its own distinct feasible value
tuples: the variables of every later group are existentially
projected away, so a group value is feasible when some assignment of
the later groups completes it, and its probability does not depend on
how many completions it has. That is the LRM’s solve s before d
(Table 18-2: s is 50/50 although s == 1 has a single completion
and s == 0 has 2^32). The chosen values are then fixed in the full
constraint set and the next group is drawn from what remains. Inside a
group the per-bit walk of Solver::sample applies, so a group is
uniform over its tuples whatever its internal order.
Any variable groups omits is solved with the last group (LRM
18.5.9: unordered variables are solved with the last set of ordered
variables), in id order. A variable listed twice is
SolveError::BadOrder.
Sourcepub fn sample_plan(
&self,
plan: &Plan,
randc_states: &mut [RandcState],
seed: &mut u64,
) -> Result<Vec<BigUint>, SolveError>
pub fn sample_plan( &self, plan: &Plan, randc_states: &mut [RandcState], seed: &mut u64, ) -> Result<Vec<BigUint>, SolveError>
Draws one assignment following plan (see Plan): first the randc
variables, each from its own cycle state (randc_states[i] belongs to
plan.randc[i]; super::randc), then the ordered groups, each with
its weighted variables before its uniform ones. A state is only
advanced for a variable that was drawn, so a caller that must not
commit a failed call clones the states first.