feat: is_sat for Cnf and Assignment ergonomics

src/instances/sat.rs

@@ -233,6 +233,17 @@ impl Cnf {
     pub fn write_dimacs<W: io::Write>(&self, writer: &mut W, n_vars: u32) -> Result<(), io::Error> {
         fio::dimacs::write_cnf_annotated(writer, self, n_vars)
     }
+
+    /// Checks whether the CNF is satisfied by the given assignment
+    #[must_use]
+    pub fn is_sat(&self, assign: &Assignment) -> bool {
+        for clause in &self.clauses {
+            if !clause.is_sat(assign) {
+                return false;
+            }
+        }
+        true
+    }
 }
 
 impl<'slf> IntoIterator for &'slf Cnf {
@@ -955,11 +966,10 @@ impl<VM: ManageVars> Instance<VM> {
     }
 
     /// Checks whether the instance is satisfied by the given assignment
+    #[must_use]
     pub fn is_sat(&self, assign: &Assignment) -> bool {
-        for clause in &self.cnf {
-            if !clause.is_sat(assign) {
-                return false;
-            }
+        if !self.cnf.is_sat(assign) {
+            return false;
         }
         for card in &self.cards {
             if !card.is_sat(assign) {

src/types.rs

@@ -879,6 +879,7 @@ impl Assignment {
     }
 
     /// Gets an iterator over literals assigned to true
+    #[allow(clippy::cast_possible_truncation)]
     pub fn iter(&self) -> impl Iterator<Item = Lit> + '_ {
         self.assignment
             .iter()
@@ -891,6 +892,14 @@ impl Assignment {
     }
 }
 
+#[cfg(kani)]
+impl Assignment {
+    /// Generates a random assignment with the given number of variables
+    pub fn arbitrary(n_vars: u32) -> Self {
+        Self::from_iter((0..n_vars).map(|_| <bool as kani::Arbitrary>::any()))
+    }
+}
+
 impl fmt::Debug for Assignment {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         self.assignment.iter().try_for_each(|tv| write!(f, "{tv}"))
@@ -932,6 +941,18 @@ impl FromIterator<Lit> for Assignment {
     }
 }
 
+impl FromIterator<TernaryVal> for Assignment {
+    fn from_iter<T: IntoIterator<Item = TernaryVal>>(iter: T) -> Self {
+        Self::from(iter.into_iter().collect::<Vec<_>>())
+    }
+}
+
+impl FromIterator<bool> for Assignment {
+    fn from_iter<T: IntoIterator<Item = bool>>(iter: T) -> Self {
+        iter.into_iter().map(TernaryVal::from).collect()
+    }
+}
+
 impl From<Vec<TernaryVal>> for Assignment {
     fn from(assignment: Vec<TernaryVal>) -> Self {
         Self { assignment }