varisat/
decision.rs

1//! Decision heuristics.
2
3use partial_ref::{partial, PartialRef};
4
5use varisat_formula::Var;
6
7use crate::{
8    context::{parts::*, Context},
9    prop::{enqueue_assignment, Reason},
10};
11
12pub mod vsids;
13
14/// Make a decision and enqueue it.
15///
16/// Returns `false` if no decision was made because all variables are assigned.
17pub fn make_decision(
18    mut ctx: partial!(
19        Context,
20        mut AssignmentP,
21        mut ImplGraphP,
22        mut TrailP,
23        mut VsidsP
24    ),
25) -> bool {
26    let (vsids, mut ctx) = ctx.split_part_mut(VsidsP);
27
28    if let Some(decision_var) = vsids.find(|&var| ctx.part(AssignmentP).var_value(var).is_none()) {
29        let decision = decision_var.lit(ctx.part(AssignmentP).last_var_value(decision_var));
30
31        ctx.part_mut(TrailP).new_decision_level();
32
33        enqueue_assignment(ctx.borrow(), decision, Reason::Unit);
34
35        true
36    } else {
37        false
38    }
39}
40
41/// Make a variable available for decisions.
42pub fn make_available(mut ctx: partial!(Context, mut VsidsP), var: Var) {
43    ctx.part_mut(VsidsP).make_available(var);
44}
45
46/// Initialize decision heuristics for a new variable.
47pub fn initialize_var(mut ctx: partial!(Context, mut VsidsP), var: Var, available: bool) {
48    ctx.part_mut(VsidsP).reset(var);
49
50    if available {
51        make_available(ctx.borrow(), var);
52    }
53}
54
55/// Remove a variable from the decision heuristics.
56pub fn remove_var(mut ctx: partial!(Context, mut VsidsP), var: Var) {
57    ctx.part_mut(VsidsP).make_unavailable(var);
58}
varisat/decision.rs

varisat/
decision.rs
