move value parsing methods into state.rs

src/btor2/witness.rs

@@ -4,8 +4,6 @@
 
 use crate::btor2::parse::tokenize_line;
 use crate::mc::{State, Value, Witness};
-use num_bigint::BigUint;
-use num_traits::Num;
 use std::io::BufRead;
 
 enum ParserState {
@@ -147,19 +145,10 @@ fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option<V
     let (value, array_index) = if is_array {
         let index_str = tokens[1];
         assert!(index_str.starts_with("[") && index_str.ends_with("]"));
-        let array_index = parse_bit_vec(&index_str[1..index_str.len() - 1]);
-        (parse_bit_vec(tokens[2]), Some(array_index))
+        let array_index = Value::from_bit_string(&index_str[1..index_str.len() - 1]);
+        (Value::from_bit_string(tokens[2]), Some(array_index))
     } else {
-        (parse_bit_vec(tokens[1]), None)
+        (Value::from_bit_string(tokens[1]), None)
     };
     (index, name, value, array_index)
 }
-
-/// parses a string of 1s and 0s into a value.
-fn parse_bit_vec(value: &str) -> Value {
-    if value.len() <= 64 {
-        Value::Long(u64::from_str_radix(value, 2).unwrap())
-    } else {
-        Value::Big(BigUint::from_str_radix(value, 2).unwrap())
-    }
-}

src/mc/smt.rs

@@ -9,8 +9,6 @@ use std::borrow::Cow;
 use crate::ir::SignalKind::Input;
 use crate::mc::{State, Value, Witness};
 use easy_smt as smt;
-use num_bigint::BigUint;
-use num_traits::Num;
 
 #[derive(Debug, Clone, Copy)]
 pub struct SmtSolverCmd {
@@ -175,26 +173,15 @@ fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result<Value>
 
 fn smt_bit_vec_str_to_value(a: &str) -> Value {
     if let Some(suffix) = a.strip_prefix("#b") {
-        if suffix.len() <= 64 {
-            Value::Long(u64::from_str_radix(suffix, 2).unwrap())
-        } else {
-            Value::Big(BigUint::from_str_radix(suffix, 2).unwrap())
-        }
+        Value::from_bit_string(suffix)
     } else if let Some(suffix) = a.strip_prefix("#x") {
-        if suffix.len() <= (64 / 4) {
-            Value::Long(u64::from_str_radix(suffix, 16).unwrap())
-        } else {
-            Value::Big(BigUint::from_str_radix(suffix, 16).unwrap())
-        }
+        Value::from_hex_string(suffix)
     } else if a == "true" {
         Value::Long(1)
     } else if a == "false" {
         Value::Long(0)
     } else {
-        match u64::from_str_radix(a, 10) {
-            Ok(value) => Value::Long(value),
-            Err(_) => Value::Big(BigUint::from_str_radix(a, 10).unwrap()),
-        }
+        Value::from_decimal_string(a)
     }
 }
 

src/mc/state.rs

@@ -4,6 +4,7 @@
 
 use crate::ir::Type;
 use num_bigint::BigUint;
+use num_traits::Num;
 
 /// Contains the initial state and the inputs over `len` cycles.
 #[derive(Debug, Default)]
@@ -143,6 +144,32 @@ pub enum Value {
     Big(BigUint),
 }
 
+impl Value {
+    /// parses a string of 1s and 0s into a value.
+    pub fn from_bit_string(value: &str) -> Self {
+        if value.len() <= 64 {
+            Value::Long(u64::from_str_radix(value, 2).unwrap())
+        } else {
+            Value::Big(BigUint::from_str_radix(value, 2).unwrap())
+        }
+    }
+
+    pub fn from_hex_string(value: &str) -> Self {
+        if value.len() <= (64 / 4) {
+            Value::Long(u64::from_str_radix(value, 16).unwrap())
+        } else {
+            Value::Big(BigUint::from_str_radix(value, 16).unwrap())
+        }
+    }
+
+    pub fn from_decimal_string(value: &str) -> Self {
+        match u64::from_str_radix(value, 10) {
+            Ok(value) => Value::Long(value),
+            Err(_) => Value::Big(BigUint::from_str_radix(value, 10).unwrap()),
+        }
+    }
+}
+
 #[derive(Debug, PartialEq)]
 pub enum ValueRef<'a> {
     Long(u64),