From f0513eeaa5392b3f67290f2cf76afa24a36bf7a2 Mon Sep 17 00:00:00 2001
From: Alex Fischman <alexdfischman@gmail.com>
Date: Fri, 21 Jul 2023 15:21:27 -0700
Subject: [PATCH] Split valuation to model conversion into a new function

Signed-off-by: Alex Fischman <alexdfischman@gmail.com>
---
 bounded/src/bdd.rs | 52 +++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/bounded/src/bdd.rs b/bounded/src/bdd.rs
index 3d1abdad..7169b42a 100644
--- a/bounded/src/bdd.rs
+++ b/bounded/src/bdd.rs
@@ -168,39 +168,39 @@ impl Context<'_> {
         }
 
         // Convert valuations to models
-        let valuations: Vec<_> = valuations.into_iter().map(Option::unwrap).collect();
+        valuations
+            .into_iter()
+            .map(|valuation| self.convert_valuation(valuation.unwrap()))
+            .collect()
+    }
+
+    fn convert_valuation(&self, valuation: BddValuation) -> Model {
         let universe = self
             .signature
             .sorts
             .iter()
             .map(|s| self.universe[s])
             .collect();
-        valuations
-            .into_iter()
-            .map(|valuation| {
-                Model::new(
-                    self.signature,
-                    &universe,
-                    self.signature
-                        .relations
+        Model::new(
+            self.signature,
+            &universe,
+            self.signature
+                .relations
+                .iter()
+                .map(|r| {
+                    let shape = r
+                        .args
                         .iter()
-                        .map(|r| {
-                            let shape = r
-                                .args
-                                .iter()
-                                .map(|s| cardinality(self.universe, s))
-                                .chain([2])
-                                .collect();
-                            Interpretation::new(&shape, |elements| {
-                                valuation
-                                    .value(self.vars[self.indices[r.name.as_str()][elements].0])
-                                    as usize
-                            })
-                        })
-                        .collect(),
-                )
-            })
-            .collect()
+                        .map(|s| cardinality(self.universe, s))
+                        .chain([2])
+                        .collect();
+                    Interpretation::new(&shape, |elements| {
+                        valuation.value(self.vars[self.indices[r.name.as_str()][elements].0])
+                            as usize
+                    })
+                })
+                .collect(),
+        )
     }
 
     fn mk_bool(&self, value: bool) -> Bdd {