1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

//! Global model reconstruction

use partial_ref::{partial, PartialRef};

use varisat_formula::Lit;
use varisat_internal_proof::ProofStep;

use crate::context::{parts::*, Context};
use crate::proof;
use crate::state::SatState;

/// Global model reconstruction
#[derive(Default)]
pub struct Model {
    /// Assignment of the global model.
    ///
    /// Whenever the solver state is SAT this must be up to date.
    assignment: Vec<Option<bool>>,
}

impl Model {
    /// Assignment of the global model.
    ///
    /// Only valid if the solver state is SAT.
    pub fn assignment(&self) -> &[Option<bool>] {
        &self.assignment
    }

    /// Whether a given global literal is true in the model assignment.
    ///
    /// Only valid if the solver state is SAT.
    pub fn lit_is_true(&self, global_lit: Lit) -> bool {
        self.assignment[global_lit.index()] == Some(global_lit.is_positive())
    }
}

pub fn reconstruct_global_model<'a>(
    mut ctx: partial!(
        Context<'a>,
        mut ModelP,
        mut ProofP<'a>,
        mut SolverStateP,
        mut TmpDataP,
        AssignmentP,
        VariablesP
    ),
) {
    let (variables, mut ctx) = ctx.split_part(VariablesP);
    let (model, mut ctx) = ctx.split_part_mut(ModelP);
    let (tmp, mut ctx) = ctx.split_part_mut(TmpDataP);

    let models_in_proof = ctx.part(ProofP).models_in_proof();

    tmp.lits.clear();

    model.assignment.clear();
    model.assignment.resize(variables.global_watermark(), None);

    for global_var in variables.global_var_iter() {
        let value = if let Some(solver_var) = variables.solver_from_global().get(global_var) {
            ctx.part(AssignmentP).var_value(solver_var)
        } else {
            Some(variables.var_data_global(global_var).unit.unwrap_or(false))
        };

        model.assignment[global_var.index()] = value;

        if models_in_proof {
            if let Some(value) = value {
                tmp.lits.push(global_var.lit(value))
            }
        }
    }

    if models_in_proof {
        proof::add_step(
            ctx.borrow(),
            false,
            &ProofStep::Model {
                assignment: &tmp.lits,
            },
        );
    }
    ctx.part_mut(SolverStateP).sat_state = SatState::Sat;
}