varisat/
model.rs

1//! Global model reconstruction
2
3use partial_ref::{partial, PartialRef};
4
5use varisat_formula::Lit;
6use varisat_internal_proof::ProofStep;
7
8use crate::{
9    context::{parts::*, Context},
10    proof,
11    state::SatState,
12};
13
14/// Global model reconstruction
15#[derive(Default)]
16pub struct Model {
17    /// Assignment of the global model.
18    ///
19    /// Whenever the solver state is SAT this must be up to date.
20    assignment: Vec<Option<bool>>,
21}
22
23impl Model {
24    /// Assignment of the global model.
25    ///
26    /// Only valid if the solver state is SAT.
27    pub fn assignment(&self) -> &[Option<bool>] {
28        &self.assignment
29    }
30
31    /// Whether a given global literal is true in the model assignment.
32    ///
33    /// Only valid if the solver state is SAT.
34    pub fn lit_is_true(&self, global_lit: Lit) -> bool {
35        self.assignment[global_lit.index()] == Some(global_lit.is_positive())
36    }
37}
38
39pub fn reconstruct_global_model<'a>(
40    mut ctx: partial!(
41        Context<'a>,
42        mut ModelP,
43        mut ProofP<'a>,
44        mut SolverStateP,
45        mut TmpDataP,
46        AssignmentP,
47        VariablesP
48    ),
49) {
50    let (variables, mut ctx) = ctx.split_part(VariablesP);
51    let (model, mut ctx) = ctx.split_part_mut(ModelP);
52    let (tmp, mut ctx) = ctx.split_part_mut(TmpDataP);
53
54    let models_in_proof = ctx.part(ProofP).models_in_proof();
55
56    tmp.lits.clear();
57
58    model.assignment.clear();
59    model.assignment.resize(variables.global_watermark(), None);
60
61    for global_var in variables.global_var_iter() {
62        let value = if let Some(solver_var) = variables.solver_from_global().get(global_var) {
63            ctx.part(AssignmentP).var_value(solver_var)
64        } else {
65            Some(variables.var_data_global(global_var).unit.unwrap_or(false))
66        };
67
68        model.assignment[global_var.index()] = value;
69
70        if models_in_proof {
71            if let Some(value) = value {
72                tmp.lits.push(global_var.lit(value))
73            }
74        }
75    }
76
77    if models_in_proof {
78        proof::add_step(
79            ctx.borrow(),
80            false,
81            &ProofStep::Model {
82                assignment: &tmp.lits,
83            },
84        );
85    }
86    ctx.part_mut(SolverStateP).sat_state = SatState::Sat;
87}
varisat/model.rs

varisat/
model.rs
