feat(planning): make explanations deal with assumptions better

solver/src/core/state/cause.rs

@@ -8,7 +8,7 @@ use crate::reasoners::ReasonerId;
 pub enum Cause {
     /// Event caused by a decision.
     Decision,
-    /// TODO.
+    /// Event caused by an assumption.
     Assumption,
     /// Event that resulted from the encoding of a constraint.
     /// This should only occur at the root decision level.

solver/src/core/state/domains.rs

@@ -428,17 +428,21 @@ impl Domains {
         explanation.push(!literal);
         explanation.push(self.presence(literal));
 
+        if cause != Origin::ASSUMPTION {
         // However, `literal` does not hold in the current state and we need to replace it.
         // Thus we replace it with a set of literals `x_1 & ... & x_m` such that
         // `x_1 & ... & x_m -> literal`
-
         self.add_implying_literals_to_explanation(literal, cause, &mut explanation, explainer);
         debug_assert!(explanation.lits.iter().copied().all(|l| self.entails(l)));
-
+        }
         // now all disjuncts hold in the current state
         // we then transform this clause to be in the first unique implication point (1UIP) form.
+        let mut conflict = self.refine_explanation(explanation, explainer);
 
-        self.refine_explanation(explanation, explainer)
+        if cause == Origin::ASSUMPTION {
+            conflict.clause = Disjunction::new([conflict.clause.literals(), &vec![!literal]].concat());
+        }
+        conflict
     }
 
     /// Refines an explanation into an asserting clause.
@@ -531,13 +535,21 @@ impl Domains {
         Conflict { clause, resolved }
     }
 
-    pub fn extract_unsat_core(&mut self, conflict: Conflict, explainer: &mut impl Explainer) -> Explanation { //FIXME: Explanation {
+    pub fn extract_unsat_core(&mut self, conflict: Conflict, explainer: &mut impl Explainer) -> Explanation {
 
-        // `conflict` must originate from `refine_explanation` (or `clause_for_invalid_update`).
+        // `conflict` must originate from `clause_for_invalid_update`.
         let clause = conflict.clause;
 
-        let mut explanation = Explanation::with_capacity(clause.len());
-        for &lit in clause.literals() { explanation.push(!lit); }
+        let mut explanation = Explanation::new(); // FIXME possible improvement ? with_capacity(clause.len()); ?
+        let mut result_as_litset = LitSet::new(); // FIXME possible improvement ? with_capacity(clause.len()); ?
+
+        for &lit in clause.literals() {
+            if self.entails(!lit) {
+                explanation.push(!lit)
+            } else {
+                result_as_litset.insert(!lit);
+            }
+        }
 
         self.queue.clear();
         let mut result_as_litset = LitSet::new();// ::with_capacity(num_assumptions);

solver/src/solver/solver_impl.rs

@@ -577,15 +577,13 @@ impl<Lbl: Label> Solver<Lbl> {
             match self.assume(lit) {
                 Ok(_) => {
                     if let Err(conflict) = self.propagate_and_backtrack_to_consistent(self.current_decision_level()) {
-                        let mut unsat_core = self.model.state.extract_unsat_core(conflict, &mut self.reasoners);
-                        unsat_core.push(lit);
+                       let unsat_core = self.model.state.extract_unsat_core(conflict, &mut self.reasoners);
                         return Ok(Err(unsat_core));
                     }
                 },
                 Err(failed) => {
                     let conflict = self.model.state.clause_for_invalid_update(failed, &mut self.reasoners);
-                    let mut unsat_core = self.model.state.extract_unsat_core(conflict, &mut self.reasoners);
-                    unsat_core.push(lit);
+                    let unsat_core = self.model.state.extract_unsat_core(conflict, &mut self.reasoners);
                     return Ok(Err(unsat_core));
                 },
             }