From 5d179e7df311f0d51435e19cb29e5044deeefd01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= <laeufer@cs.berkeley.edu>
Date: Thu, 16 Nov 2023 09:23:15 -0500
Subject: [PATCH] read simple witness

---
 examples/bmc.rs | 24 +++++++++++++++---------
 src/mc/smt.rs   | 48 +++++++++++++++++++++++++++++++++++++++++++++---
 2 files changed, 60 insertions(+), 12 deletions(-)

diff --git a/examples/bmc.rs b/examples/bmc.rs
index e64fd83..cd65fdc 100644
--- a/examples/bmc.rs
+++ b/examples/bmc.rs
@@ -12,6 +12,8 @@ use libpatron::*;
 #[command(version)]
 #[command(about = "Performs bounded model checking on a btor2 file.", long_about = None)]
 struct Args {
+    #[arg(short, long)]
+    verbose: bool,
     #[arg(value_name = "BTOR2", index = 1)]
     filename: String,
 }
@@ -19,20 +21,24 @@ struct Args {
 fn main() {
     let args = Args::parse();
     let (ctx, sys) = btor2::parse_file(&args.filename).expect("Failed to load btor2 file!");
-    println!("Loaded: {}", sys.name);
-    println!("{}", sys.serialize_to_str(&ctx));
-    println!();
-    println!();
+    if args.verbose {
+        println!("Loaded: {}", sys.name);
+        println!("{}", sys.serialize_to_str(&ctx));
+        println!();
+        println!();
+    }
     let k_max = 25;
     let checker_opts = mc::SmtModelCheckerOptions {
         check_constraints: true,
         check_bad_states_individually: true,
     };
     let solver = mc::BITWUZLA_CMD;
-    println!(
-        "Checking up to {k_max} using {} and the following options:\n{checker_opts:?}",
-        solver.name
-    );
+    if args.verbose {
+        println!(
+            "Checking up to {k_max} using {} and the following options:\n{checker_opts:?}",
+            solver.name
+        );
+    }
     let checker = mc::SmtModelChecker::new(solver, checker_opts);
     let res = checker.check(&ctx, &sys, k_max).unwrap();
     match res {
@@ -41,7 +47,7 @@ fn main() {
         }
         mc::ModelCheckResult::Fail(_) => {
             println!("sat");
-            todo!("print witness")
+            println!("TODO: print witness")
         }
     }
 }
diff --git a/src/mc/smt.rs b/src/mc/smt.rs
index 7e601f6..b0eefc3 100644
--- a/src/mc/smt.rs
+++ b/src/mc/smt.rs
@@ -9,6 +9,8 @@ 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 {
@@ -156,7 +158,44 @@ impl SmtModelChecker {
 
 fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result<Value> {
     let smt_value = smt_ctx.get_value(vec![expr])?[0].1;
-    todo!("Convert: {:?}", smt_ctx.display(smt_value).to_string())
+    let atom = smt_ctx.get(smt_value);
+    match atom {
+        smt::SExprData::Atom(a) => {
+            let value = smt_bit_vec_str_to_value(a);
+            Ok(value)
+        }
+        smt::SExprData::List(elements) => {
+            todo!(
+                "Deal with list value: {}",
+                smt_ctx.display(smt_value).to_string()
+            )
+        }
+    }
+}
+
+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())
+        }
+    } 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())
+        }
+    } 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()),
+        }
+    }
 }
 
 pub enum ModelCheckResult {
@@ -502,8 +541,8 @@ fn unescape_smt_identifier(id: &str) -> &str {
 
 #[cfg(test)]
 mod tests {
-    use easy_smt::*;
     use super::*;
+    use easy_smt::*;
 
     #[test]
     fn easy_smt_symbol_escaping() {
@@ -517,6 +556,9 @@ mod tests {
 
     #[test]
     fn test_our_escaping() {
-        assert_eq!(unescape_smt_identifier(&escape_smt_identifier("a b")), "a b");
+        assert_eq!(
+            unescape_smt_identifier(&escape_smt_identifier("a b")),
+            "a b"
+        );
     }
 }