1 files changed, 259 insertions, 0 deletions
diff --git a/vendor/varisat/src/load.rs b/vendor/varisat/src/load.rs
new file mode 100644
index 000000000..43415dbfb
--- /dev/null
+++ b/vendor/varisat/src/load.rs
@@ -0,0 +1,259 @@
+//! Loading a formula into the solver.
+use vec_mut_scan::VecMutScan;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+    clause::{db, ClauseHeader, Tier},
+    context::{parts::*, Context},
+    proof,
+    prop::{assignment, full_restart, Reason},
+    state::SatState,
+    unit_simplify::resurrect_unit,
+    variables,
+};
+
+/// Adds a clause to the current formula.
+///
+/// The input uses user variable names.
+///
+/// Removes duplicated literals, ignores tautological clauses (eg. x v -x v y), handles empty
+/// clauses and dispatches among unit, binary and long clauses.
+pub fn load_clause<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut AnalyzeConflictP,
+        mut AssignmentP,
+        mut AssumptionsP,
+        mut BinaryClausesP,
+        mut ClauseAllocP,
+        mut ClauseDbP,
+        mut ImplGraphP,
+        mut ProofP<'a>,
+        mut SolverStateP,
+        mut TmpDataP,
+        mut TmpFlagsP,
+        mut TrailP,
+        mut VariablesP,
+        mut VsidsP,
+        mut WatchlistsP,
+    ),
+    user_lits: &[Lit],
+) {
+    match ctx.part(SolverStateP).sat_state {
+        SatState::Unsat => return,
+        SatState::Sat => {
+            ctx.part_mut(SolverStateP).sat_state = SatState::Unknown;
+        }
+        _ => {}
+    }
+
+    ctx.part_mut(SolverStateP).formula_is_empty = false;
+
+    // Restart the search when the user adds new clauses.
+    full_restart(ctx.borrow());
+
+    // Convert the clause from user to solver literals.
+    let (tmp_data, mut ctx_variables) = ctx.split_part_mut(TmpDataP);
+    variables::solver_from_user_lits(ctx_variables.borrow(), &mut tmp_data.lits, user_lits, true);
+
+    let (tmp_data, mut ctx) = ctx.split_part_mut(TmpDataP);
+
+    let lits = &mut tmp_data.lits;
+    let false_lits = &mut tmp_data.lits_2;
+
+    lits.sort_unstable();
+    lits.dedup();
+
+    proof::add_clause(ctx.borrow(), &lits);
+
+    // Detect tautological clauses
+    let mut last = None;
+
+    for &lit in lits.iter() {
+        if last == Some(!lit) {
+            return;
+        }
+        last = Some(lit);
+    }
+
+    // If we're not a unit clause the contained variables are not isolated anymore.
+    if lits.len() > 1 {
+        for &lit in lits.iter() {
+            ctx.part_mut(VariablesP)
+                .var_data_solver_mut(lit.var())
+                .isolated = false;
+        }
+    }
+
+    // Remove satisfied clauses and handle false literals.
+    //
+    // Proof generation expects us to start with the actual input clauses. If we would remove false
+    // literals we would have to generate proof steps for that. This would result in derived clauses
+    // being added during loading. If we're running proof processors on the fly, they'd see those
+    // derived clauses interspersed with the input clauses.
+    //
+    // We don't want to require each proof processor to handle dervied clause additions during
+    // loading of the initial formula. Thus we need to handle clauses with false literals here.
+    false_lits.clear();
+
+    let mut lits_scan = VecMutScan::new(lits);
+
+    let mut clause_is_true = false;
+
+    // We move unassigned literals to the beginning to make sure we're going to watch unassigned
+    // literals.
+    while let Some(lit) = lits_scan.next() {
+        match ctx.part(AssignmentP).lit_value(*lit) {
+            Some(true) => {
+                clause_is_true = true;
+                break;
+            }
+            Some(false) => {
+                false_lits.push(lit.remove());
+            }
+            None => (),
+        }
+    }
+
+    drop(lits_scan);
+
+    let will_conflict = lits.is_empty();
+
+    // We resurrect any removed false literals to ensure propagation by this new clause. This is
+    // also required to eventually simplify this clause.
+    for &lit in false_lits.iter() {
+        resurrect_unit(ctx.borrow(), !lit);
+    }
+
+    lits.extend_from_slice(&false_lits);
+
+    if clause_is_true {
+        if lits.len() > 1 {
+            proof::add_step(
+                ctx.borrow(),
+                true,
+                &ProofStep::DeleteClause {
+                    clause: lits,
+                    proof: DeleteClauseProof::Satisfied,
+                },
+            );
+        }
+        return;
+    }
+
+    match lits[..] {
+        [] => ctx.part_mut(SolverStateP).sat_state = SatState::Unsat,
+        [lit] => {
+            if will_conflict {
+                ctx.part_mut(SolverStateP).sat_state = SatState::Unsat
+            } else {
+                assignment::enqueue_assignment(ctx.borrow(), lit, Reason::Unit)
+            }
+        }
+        [lit_0, lit_1] => {
+            ctx.part_mut(BinaryClausesP)
+                .add_binary_clause([lit_0, lit_1]);
+        }
+        _ => {
+            let mut header = ClauseHeader::new();
+            header.set_tier(Tier::Irred);
+
+            db::add_clause(ctx.borrow(), header, lits);
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    use partial_ref::IntoPartialRefMut;
+
+    use varisat_formula::lits;
+
+    use crate::clause::Tier;
+
+    #[test]
+    fn unsat_on_empty_clause() {
+        let mut ctx = Context::default();
+        let mut ctx = ctx.into_partial_ref_mut();
+
+        load_clause(ctx.borrow(), &[]);
+
+        assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+    }
+
+    #[test]
+    fn unit_clauses() {
+        let mut ctx = Context::default();
+        let mut ctx = ctx.into_partial_ref_mut();
+
+        load_clause(ctx.borrow(), &lits![1]);
+
+        assert_eq!(ctx.part(TrailP).trail().len(), 1);
+
+        load_clause(ctx.borrow(), &lits![3, -3]);
+
+        assert_eq!(ctx.part(TrailP).trail().len(), 1);
+
+        load_clause(ctx.borrow(), &lits![-2]);
+
+        assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+        load_clause(ctx.borrow(), &lits![1, 1]);
+
+        assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+        assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+        load_clause(ctx.borrow(), &lits![2]);
+
+        assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+        assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+    }
+
+    #[test]
+    fn binary_clauses() {
+        let mut ctx = Context::default();
+        let mut ctx = ctx.into_partial_ref_mut();
+
+        load_clause(ctx.borrow(), &lits![1, 2]);
+
+        assert_eq!(ctx.part(BinaryClausesP).count(), 1);
+
+        load_clause(ctx.borrow(), &lits![-1, 3, 3]);
+
+        assert_eq!(ctx.part(BinaryClausesP).count(), 2);
+
+        load_clause(ctx.borrow(), &lits![4, -4]);
+
+        assert_eq!(ctx.part(BinaryClausesP).count(), 2);
+
+        assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+    }
+
+    #[test]
+    fn long_clauses() {
+        let mut ctx = Context::default();
+        let mut ctx = ctx.into_partial_ref_mut();
+
+        load_clause(ctx.borrow(), &lits![1, 2, 3]);
+
+        assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 1);
+
+        load_clause(ctx.borrow(), &lits![-2, 3, 3, 4]);
+
+        assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 2);
+
+        load_clause(ctx.borrow(), &lits![4, -5, 5, 2]);
+
+        assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 2);
+
+        assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+    }
+}