1 files changed, 87 insertions, 0 deletions
diff --git a/vendor/varisat/src/model.rs b/vendor/varisat/src/model.rs
new file mode 100644
index 000000000..d4f269f6f
--- /dev/null
+++ b/vendor/varisat/src/model.rs
@@ -0,0 +1,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;
+}