feat!: add evaluate, replacing is_sat

solvertests/src/integration.rs

@@ -38,7 +38,7 @@ pub fn base(input: IntegrationInput) -> TokenStream {
                 if $res == rustsat::solvers::SolverResult::Sat {
                     let sol = rustsat::solvers::Solve::solution(&solver, inst.max_var().expect("no variables in instance"))
                         .expect("failed to get solution from solver");
-                    assert!(inst.is_sat(&sol));
+                    assert_eq!(inst.evaluate(&sol), rustsat::types::TernaryVal::True);
                 }
             }};
         }

src/instances/fio.rs

@@ -277,7 +277,7 @@ mod tests {
         .unwrap();
         let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
-            assert!(instance.is_sat(&sol));
+            assert_eq!(instance.evaluate(&sol), TernaryVal::True);
         } else {
             panic!()
         }
@@ -288,7 +288,7 @@ mod tests {
         .unwrap();
         let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
-            assert!(instance.is_sat(&sol));
+            assert_eq!(instance.evaluate(&sol), TernaryVal::True);
         } else {
             panic!()
         }
@@ -299,7 +299,7 @@ mod tests {
         .unwrap();
         let res = parse_sat_solver_output(&mut reader).unwrap();
         if let SolverOutput::Sat(sol) = res {
-            assert!(instance.is_sat(&sol));
+            assert_eq!(instance.evaluate(&sol), TernaryVal::True);
         } else {
             panic!()
         }

src/instances/multiopt.rs

@@ -6,7 +6,7 @@ use crate::{
     encodings::{card, pb},
     types::{
         constraints::{CardConstraint, PbConstraint},
-        Assignment, Lit, Var, WClsIter, WLitIter,
+        Assignment, Lit, TernaryVal, Var, WClsIter, WLitIter,
     },
     RequiresClausal, RequiresSoftLits,
 };
@@ -454,7 +454,7 @@ impl<VM: ManageVars> MultiOptInstance<VM> {
     /// Calculates the objective values of an assignment. Returns [`None`] if the
     /// assignment is not a solution.
     pub fn cost(&self, assign: &Assignment) -> Option<Vec<isize>> {
-        if !self.constrs.is_sat(assign) {
+        if self.constrs.evaluate(assign) != TernaryVal::True {
             return None;
         }
         Some(self.objs.iter().map(|o| o.evaluate(assign)).collect())

src/instances/opt.rs

@@ -1394,7 +1394,7 @@ impl<VM: ManageVars> Instance<VM> {
     /// Calculates the objective value of an assignment. Returns [`None`] if the
     /// assignment is not a solution.
     pub fn cost(&self, assign: &Assignment) -> Option<isize> {
-        if !self.constrs.is_sat(assign) {
+        if self.constrs.evaluate(assign) != TernaryVal::True {
             return None;
         }
         Some(self.obj.evaluate(assign))

src/instances/sat.rs

@@ -8,7 +8,7 @@ use crate::{
     lit,
     types::{
         constraints::{CardConstraint, PbConstraint},
-        Assignment, Clause, Lit, Var,
+        Assignment, Clause, Lit, TernaryVal, Var,
     },
     utils::{unreachable_err, LimitedIter},
     RequiresClausal,
@@ -234,15 +234,28 @@ impl Cnf {
         fio::dimacs::write_cnf_annotated(writer, self, n_vars)
     }
 
-    /// Checks whether the CNF is satisfied by the given assignment
+    /// Checks the value of the CNF under a given assignment
     #[must_use]
-    pub fn is_sat(&self, assign: &Assignment) -> bool {
+    pub fn evaluate(&self, assign: &Assignment) -> TernaryVal {
+        let mut val = TernaryVal::True;
         for clause in &self.clauses {
-            if !clause.is_sat(assign) {
-                return false;
+            match clause.evaluate(assign) {
+                TernaryVal::True => (),
+                TernaryVal::False => return TernaryVal::False,
+                TernaryVal::DontCare => val = TernaryVal::DontCare,
             }
         }
-        true
+        val
+    }
+
+    /// Checks whether the CNF is satisfied by the given assignment
+    #[deprecated(
+        since = "0.6.0",
+        note = "use `evaluate` instead and check against `TernaryVal::True`"
+    )]
+    #[must_use]
+    pub fn is_sat(&self, assign: &Assignment) -> bool {
+        self.evaluate(assign) == TernaryVal::True
     }
 }
 
@@ -965,23 +978,40 @@ impl<VM: ManageVars> Instance<VM> {
         }
     }
 
-    /// Checks whether the instance is satisfied by the given assignment
+    /// Computes the value of the instance under a given assignment
     #[must_use]
-    pub fn is_sat(&self, assign: &Assignment) -> bool {
-        if !self.cnf.is_sat(assign) {
-            return false;
+    pub fn evaluate(&self, assign: &Assignment) -> TernaryVal {
+        let mut val = TernaryVal::True;
+        match self.cnf.evaluate(assign) {
+            TernaryVal::True => (),
+            TernaryVal::False => return TernaryVal::False,
+            TernaryVal::DontCare => val = TernaryVal::DontCare,
         }
         for card in &self.cards {
-            if !card.is_sat(assign) {
-                return false;
+            match card.evaluate(assign) {
+                TernaryVal::True => (),
+                TernaryVal::False => return TernaryVal::False,
+                TernaryVal::DontCare => val = TernaryVal::DontCare,
             }
         }
         for pb in &self.pbs {
-            if !pb.is_sat(assign) {
-                return false;
+            match pb.evaluate(assign) {
+                TernaryVal::True => (),
+                TernaryVal::False => return TernaryVal::False,
+                TernaryVal::DontCare => val = TernaryVal::DontCare,
             }
         }
-        true
+        val
+    }
+
+    /// Checks whether the instance is satisfied by the given assignment
+    #[deprecated(
+        since = "0.6.0",
+        note = "use `evaluate` instead and check against `TernaryVal::True`"
+    )]
+    #[must_use]
+    pub fn is_sat(&self, assign: &Assignment) -> bool {
+        self.evaluate(assign) == TernaryVal::True
     }
 }
 

src/types/constraints.rs

@@ -376,6 +376,10 @@ impl Cl {
 
     /// Checks wheter the clause is satisfied
     #[must_use]
+    #[deprecated(
+        since = "0.6.0",
+        note = "use `evaluate` instead and check against `TernaryVal::True`"
+    )]
     pub fn is_sat(&self, assignment: &Assignment) -> bool {
         self.evaluate(assignment) == TernaryVal::True
     }
@@ -541,6 +545,16 @@ impl CardConstraint {
         }
     }
 
+    /// Gets the bound of the constraint
+    #[must_use]
+    pub fn bound(&self) -> usize {
+        match self {
+            CardConstraint::Ub(CardUbConstr { b, .. })
+            | CardConstraint::Lb(CardLbConstr { b, .. })
+            | CardConstraint::Eq(CardEqConstr { b, .. }) => *b,
+        }
+    }
+
     /// Changes the bound on the constraint
     pub fn change_bound(&mut self, b: usize) {
         match self {
@@ -677,19 +691,34 @@ impl CardConstraint {
 
     /// Checks whether the cardinality constraint is satisfied by the given assignment
     #[must_use]
-    pub fn is_sat(&self, assign: &Assignment) -> bool {
-        let count = self.iter().fold(0, |cnt, lit| {
-            if assign.lit_value(*lit) == TernaryVal::True {
-                return cnt + 1;
-            }
-            cnt
-        });
+    pub fn evaluate(&self, assign: &Assignment) -> TernaryVal {
+        #[allow(clippy::range_plus_one)]
+        let range = self
+            .iter()
+            .fold(0..0, |rng, &lit| match assign.lit_value(lit) {
+                TernaryVal::True => rng.start + 1..rng.end + 1,
+                TernaryVal::False => rng,
+                TernaryVal::DontCare => rng.start..rng.end + 1,
+            });
+        if range.contains(&self.bound()) {
+            return TernaryVal::DontCare;
+        }
         match self {
-            CardConstraint::Ub(constr) => count <= constr.b,
-            CardConstraint::Lb(constr) => count >= constr.b,
-            CardConstraint::Eq(constr) => count == constr.b,
+            CardConstraint::Ub(CardUbConstr { b, .. }) => (range.start <= *b).into(),
+            CardConstraint::Lb(CardLbConstr { b, .. }) => (range.start >= *b).into(),
+            CardConstraint::Eq(CardEqConstr { b, .. }) => (range.start == *b).into(),
         }
     }
+
+    /// Checks whether the cardinality constraint is satisfied by the given assignment
+    #[deprecated(
+        since = "0.6.0",
+        note = "use `evaluate` instead and check against `TernaryVal::True`"
+    )]
+    #[must_use]
+    pub fn is_sat(&self, assign: &Assignment) -> bool {
+        self.evaluate(assign) == TernaryVal::True
+    }
 }
 
 impl<'slf> IntoIterator for &'slf CardConstraint {
@@ -958,6 +987,16 @@ impl PbConstraint {
         *b += b_add;
     }
 
+    /// Gets the bound of the constraint
+    #[must_use]
+    pub fn bound(&self) -> isize {
+        match self {
+            PbConstraint::Ub(PbUbConstr { b, .. })
+            | PbConstraint::Lb(PbLbConstr { b, .. })
+            | PbConstraint::Eq(PbEqConstr { b, .. }) => *b,
+        }
+    }
+
     /// Checks if the constraint is always satisfied
     #[must_use]
     pub fn is_tautology(&self) -> bool {
@@ -1187,37 +1226,54 @@ impl PbConstraint {
 
     /// Checks whether the PB constraint is satisfied by the given assignment
     #[must_use]
-    pub fn is_sat(&self, assign: &Assignment) -> bool {
-        let sum = self.iter().fold(0, |sum, (lit, coeff)| {
-            if assign.lit_value(*lit) == TernaryVal::True {
-                return sum + coeff;
-            }
-            sum
-        });
-        match self {
-            PbConstraint::Ub(constr) => {
-                if let Ok(sum) = <usize as TryInto<isize>>::try_into(sum) {
-                    sum <= constr.b
-                } else {
-                    false
+    pub fn evaluate(&self, assign: &Assignment) -> TernaryVal {
+        #[allow(clippy::range_plus_one)]
+        let range = self
+            .iter()
+            .fold(0..0, |rng, &(lit, coeff)| match assign.lit_value(lit) {
+                TernaryVal::True => rng.start + coeff..rng.end + coeff,
+                TernaryVal::False => rng,
+                TernaryVal::DontCare => rng.start..rng.end + coeff,
+            });
+        match (isize::try_from(range.start), isize::try_from(range.end)) {
+            (Ok(start), Ok(end)) => {
+                if (start..end).contains(&self.bound()) {
+                    return TernaryVal::DontCare;
                 }
-            }
-            PbConstraint::Lb(constr) => {
-                if let Ok(sum) = <usize as TryInto<isize>>::try_into(sum) {
-                    sum >= constr.b
-                } else {
-                    true
+                match self {
+                    PBConstraint::Ub(PbUbConstr { b, .. }) => (start <= *b).into(),
+                    PBConstraint::Lb(PbLbConstr { b, .. }) => (start >= *b).into(),
+                    PBConstraint::Eq(PbEqConstr { b, .. }) => (start == *b).into(),
                 }
             }
-            PbConstraint::Eq(constr) => {
-                if let Ok(sum) = <usize as TryInto<isize>>::try_into(sum) {
-                    sum == constr.b
-                } else {
-                    false
+            (Ok(start), Err(_)) => match self {
+                PbConstraint::Ub(PbUbConstr { b, .. }) => {
+                    if (start..).contains(b) {
+                        return TernaryVal::DontCare;
+                    }
+                    TernaryVal::True
                 }
-            }
+                PbConstraint::Lb(PbLbConstr { b, .. }) | PbConstraint::Eq(PbEqConstr { b, .. }) => {
+                    if (start..).contains(b) {
+                        return TernaryVal::DontCare;
+                    }
+                    TernaryVal::False
+                }
+            },
+            (Err(_), Err(_)) => matches!(self, PbConstraint::Lb(_)).into(),
+            (Err(_), Ok(_)) => unreachable!(), // since end >= start
         }
     }
+
+    /// Checks whether the PB constraint is satisfied by the given assignment
+    #[deprecated(
+        since = "0.6.0",
+        note = "use `evaluate` instead and check against `TernaryVal::True`"
+    )]
+    #[must_use]
+    pub fn is_sat(&self, assign: &Assignment) -> bool {
+        self.evaluate(assign) == TernaryVal::True
+    }
 }
 
 impl<'slf> IntoIterator for &'slf PbConstraint {
@@ -1495,7 +1551,11 @@ impl PbEqConstr {
 #[cfg(test)]
 mod tests {
     use super::{CardConstraint, Cl, PbConstraint};
-    use crate::{lit, types::Assignment, var};
+    use crate::{
+        lit,
+        types::{Assignment, TernaryVal},
+        var,
+    };
 
     #[test]
     fn clause_remove() {
@@ -1550,16 +1610,20 @@ mod tests {
     }
 
     #[test]
-    fn clause_is_sat() {
+    fn clause_evaluate() {
         let cl = clause![lit![0], lit![1], lit![2]];
-        assert!(!cl.is_sat(&assign!(0b000)));
-        assert!(cl.is_sat(&assign!(0b001)));
-        assert!(cl.is_sat(&assign!(0b010)));
-        assert!(cl.is_sat(&assign!(0b011)));
-        assert!(cl.is_sat(&assign!(0b100)));
-        assert!(cl.is_sat(&assign!(0b101)));
-        assert!(cl.is_sat(&assign!(0b110)));
-        assert!(cl.is_sat(&assign!(0b111)));
+        assert_eq!(cl.evaluate(&assign!(0b000)), TernaryVal::False);
+        assert_eq!(cl.evaluate(&assign!(0b001)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b010)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b011)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b100)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b101)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b110)), TernaryVal::True);
+        assert_eq!(cl.evaluate(&assign!(0b111)), TernaryVal::True);
+        assert_eq!(
+            cl.evaluate(&assign!(0b000).truncate(var![1])),
+            TernaryVal::DontCare
+        );
     }
 
     #[test]