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
86
87
|
//! Global model reconstruction
use partial_ref::{partial, PartialRef};
use varisat_formula::Lit;
use varisat_internal_proof::ProofStep;
use crate::{
context::{parts::*, Context},
proof,
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;
}
|
