serialize witness in btor format

examples/bmc.rs

@@ -48,7 +48,7 @@ fn main() {
             println!("unsat");
         }
         mc::ModelCheckResult::Fail(wit) => {
-            print_witness(&mut std::io::stdout(), &wit).unwrap();
+            print_witness(&mut std::io::stdout(), &wit, &sys, &ctx).unwrap();
         }
     }
 }

src/btor2/witness.rs

@@ -3,6 +3,8 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::btor2::parse::tokenize_line;
+use crate::ir;
+use crate::ir::{SignalKind, TypeCheck};
 use crate::mc::{State, Value, Witness};
 use std::io::{BufRead, Write};
 
@@ -153,8 +155,61 @@ fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option<V
     (index, name, value, array_index)
 }
 
-pub fn print_witness(out: &mut impl Write, witness: &Witness) -> std::io::Result<()> {
+pub fn print_witness(
+    out: &mut impl Write,
+    witness: &Witness,
+    sys: &ir::TransitionSystem,
+    ctx: &ir::Context,
+) -> std::io::Result<()> {
     writeln!(out, "sat")?;
 
+    // declare failed properties
+    for (ii, bad_id) in witness.failed_safety.iter().enumerate() {
+        let is_last = ii + 1 == witness.failed_safety.len();
+        write!(out, "b{bad_id}")?;
+        if is_last {
+            writeln!(out, "")?;
+        } else {
+            write!(out, " ")?;
+        }
+    }
+
+    // print starting state (if non-empty)
+    if !witness.init.is_empty() {
+        writeln!(out, "#0")?;
+        for (id, (maybe_value, state)) in witness.init.iter().zip(sys.states()).enumerate() {
+            if let Some(value) = maybe_value {
+                let width = state.symbol.get_type(ctx).get_bit_vector_width().unwrap();
+                let name = state.symbol.get_symbol_name(ctx).unwrap();
+                writeln!(
+                    out,
+                    "{id} {} {}@0",
+                    value.to_bit_string(width).unwrap(),
+                    name
+                )?;
+            }
+        }
+    }
+
+    // print inputs
+    let inputs = sys.get_signals(|s| s.kind == SignalKind::Input);
+    for (k, values) in witness.inputs.iter().enumerate() {
+        writeln!(out, "@{k}")?;
+        for (id, (maybe_value, (input_sym, _))) in values.iter().zip(inputs.iter()).enumerate() {
+            if let Some(value) = maybe_value {
+                let width = input_sym.get_type(ctx).get_bit_vector_width().unwrap();
+                let name = input_sym.get_symbol_name(ctx).unwrap();
+                writeln!(
+                    out,
+                    "{id} {} {}@0",
+                    value.to_bit_string(width).unwrap(),
+                    name
+                )?;
+            }
+        }
+    }
+
+    writeln!(out, ".")?;
+
     Ok(())
 }

src/ir/smt.rs

@@ -425,6 +425,13 @@ impl Type {
             Type::Array(_) => false,
         }
     }
+
+    pub fn get_bit_vector_width(&self) -> Option<WidthInt> {
+        match &self {
+            Type::BV(width) => Some(*width),
+            Type::Array(_) => None,
+        }
+    }
 }
 
 impl std::fmt::Display for Type {

src/mc/smt.rs

@@ -3,7 +3,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use crate::ir;
-use crate::ir::{Expr, ExprRef, GetNode, SignalKind, Type, TypeCheck};
+use crate::ir::{Expr, ExprRef, GetNode, SignalInfo, SignalKind, Type, TypeCheck};
 use std::borrow::Cow;
 
 use crate::ir::SignalKind::Input;
@@ -83,7 +83,7 @@ impl SmtModelChecker {
         for k in 0..=k_max {
             // assume all constraints hold in this step
             for (expr_ref, _) in constraints.iter() {
-                let expr = enc.get_constraint(&mut smt_ctx, *expr_ref);
+                let expr = enc.get_at(&mut smt_ctx, *expr_ref, k);
                 smt_ctx.assert(expr)?;
             }
 
@@ -100,24 +100,24 @@ impl SmtModelChecker {
 
             if self.opts.check_bad_states_individually {
                 for (_bs_id, (expr_ref, _)) in bad_states.iter().enumerate() {
-                    let expr = enc.get_bad_state(&mut smt_ctx, *expr_ref);
+                    let expr = enc.get_at(&mut smt_ctx, *expr_ref, k);
                     let res = smt_ctx.check_assuming([expr])?;
 
                     if res == smt::Response::Sat {
-                        let wit = self.get_witness(sys, &mut smt_ctx, &enc, k)?;
+                        let wit = self.get_witness(sys, &mut smt_ctx, &enc, k, &bad_states)?;
                         return Ok(ModelCheckResult::Fail(wit));
                     }
                 }
             } else {
                 let all_bads = bad_states
                     .iter()
-                    .map(|(expr_ref, _)| enc.get_bad_state(&mut smt_ctx, *expr_ref))
+                    .map(|(expr_ref, _)| enc.get_at(&mut smt_ctx, *expr_ref, k))
                     .collect::<Vec<_>>();
                 let any_bad = smt_ctx.or_many(all_bads);
                 let res = smt_ctx.check_assuming([any_bad])?;
 
                 if res == smt::Response::Sat {
-                    let wit = self.get_witness(sys, &mut smt_ctx, &enc, k)?;
+                    let wit = self.get_witness(sys, &mut smt_ctx, &enc, k, &bad_states)?;
                     return Ok(ModelCheckResult::Fail(wit));
                 }
             }
@@ -136,11 +136,23 @@ impl SmtModelChecker {
         smt_ctx: &mut smt::Context,
         enc: &UnrollSmtEncoding,
         k_max: u64,
+        bad_states: &[(ExprRef, SignalInfo)],
     ) -> Result<Witness> {
         let mut wit = Witness::default();
+
+        // which bad states did we hit?
+        for (bad_idx, (expr, _)) in bad_states.iter().enumerate() {
+            let sym_at = enc.get_at(smt_ctx, *expr, k_max);
+            let value = get_smt_value(smt_ctx, sym_at)?;
+            if !value.is_zero() {
+                // was the bad state condition fulfilled?
+                wit.failed_safety.push(bad_idx as u32);
+            }
+        }
+
         // collect initial values
         for (state_idx, state) in sys.states().enumerate() {
-            let sym_at = enc.get_symbol_at(smt_ctx, state.symbol, 0);
+            let sym_at = enc.get_at(smt_ctx, state.symbol, 0);
             let value = get_smt_value(smt_ctx, sym_at)?;
             wit.init.insert(state_idx, value);
         }
@@ -150,7 +162,7 @@ impl SmtModelChecker {
         for k in 0..=k_max {
             let mut input_values = State::default();
             for (input_idx, (input, _)) in inputs.iter().enumerate() {
-                let sym_at = enc.get_symbol_at(smt_ctx, *input, k);
+                let sym_at = enc.get_at(smt_ctx, *input, k);
                 let value = get_smt_value(smt_ctx, sym_at)?;
                 input_values.insert(input_idx, value);
             }
@@ -201,9 +213,8 @@ pub trait TransitionSystemEncoding {
     fn define_header(&self, smt_ctx: &mut smt::Context) -> Result<()>;
     fn init(&mut self, smt_ctx: &mut smt::Context) -> Result<()>;
     fn unroll(&mut self, smt_ctx: &mut smt::Context) -> Result<()>;
-    fn get_constraint(&self, smt_ctx: &mut smt::Context, e: ExprRef) -> smt::SExpr;
-    fn get_bad_state(&self, smt_ctx: &mut smt::Context, e: ExprRef) -> smt::SExpr;
-    fn get_symbol_at(&self, smt_ctx: &mut smt::Context, sym: ExprRef, k: u64) -> smt::SExpr;
+    /// Allows access to inputs, states, constraints and bad_state expressions.
+    fn get_at(&self, smt_ctx: &mut smt::Context, expr: ExprRef, k: u64) -> smt::SExpr;
 }
 
 pub struct UnrollSmtEncoding<'a> {
@@ -262,15 +273,21 @@ impl<'a> UnrollSmtEncoding<'a> {
         e: ExprRef,
         k: u64,
     ) -> smt::SExpr {
-        // find our local name
-        let base_name: &str = self
-            .signals
-            .iter()
-            .find(|(id, _)| *id == e)
-            .map(|(_, n)| n)
-            .unwrap();
-        let name = format!("{}@{}", base_name, k);
-        smt_ctx.atom(escape_smt_identifier(&name))
+        // is it already a symbol?
+        if e.is_symbol(self.ctx) {
+            let name = self.name_at(e, k);
+            smt_ctx.atom(escape_smt_identifier(&name))
+        } else {
+            // find our local name
+            let base_name: &str = self
+                .signals
+                .iter()
+                .find(|(id, _)| *id == e)
+                .map(|(_, n)| n)
+                .unwrap();
+            let name = format!("{}@{}", base_name, k);
+            smt_ctx.atom(escape_smt_identifier(&name))
+        }
     }
 
     fn expr_in_step(&self, smt_ctx: &mut smt::Context, expr: ExprRef, step: u64) -> smt::SExpr {
@@ -454,20 +471,9 @@ impl<'a> TransitionSystemEncoding for UnrollSmtEncoding<'a> {
         self.current_step = Some(next_step);
         Ok(())
     }
-
-    fn get_constraint(&self, smt_ctx: &mut smt::Context, e: ExprRef) -> smt::SExpr {
-        self.get_local_expr_symbol_at(smt_ctx, e, self.current_step.unwrap())
-    }
-
-    fn get_bad_state(&self, smt_ctx: &mut smt::Context, e: ExprRef) -> smt::SExpr {
-        self.get_local_expr_symbol_at(smt_ctx, e, self.current_step.unwrap())
-    }
-
-    fn get_symbol_at(&self, smt_ctx: &mut smt::Context, sym: ExprRef, k: u64) -> smt::SExpr {
-        assert!(sym.is_symbol(self.ctx));
+    fn get_at(&self, smt_ctx: &mut smt::Context, expr: ExprRef, k: u64) -> smt::SExpr {
         assert!(k <= self.current_step.unwrap_or(0));
-        let name = self.name_at(sym, k);
-        smt_ctx.atom(escape_smt_identifier(&name))
+        self.get_local_expr_symbol_at(smt_ctx, expr, self.current_step.unwrap())
     }
 }
 

src/mc/state.rs

@@ -2,9 +2,9 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 
-use crate::ir::Type;
+use crate::ir::{Type, WidthInt};
 use num_bigint::BigUint;
-use num_traits::Num;
+use num_traits::{Num, Zero};
 
 /// Contains the initial state and the inputs over `len` cycles.
 #[derive(Debug, Default)]
@@ -100,6 +100,10 @@ impl State {
 
     pub fn get(&self, index: usize) -> Option<ValueRef> {
         let meta = self.meta.get(index)?;
+        self.get_from_meta(meta)
+    }
+
+    fn get_from_meta(&self, meta: &StorageMetaData) -> Option<ValueRef> {
         if !meta.is_valid {
             return None;
         }
@@ -136,6 +140,33 @@ impl State {
     pub fn is_empty(&self) -> bool {
         self.meta.is_empty()
     }
+
+    pub fn iter(&self) -> StateIter<'_> {
+        StateIter::new(&self)
+    }
+}
+
+pub struct StateIter<'a> {
+    state: &'a State,
+    underlying: std::slice::Iter<'a, StorageMetaData>,
+}
+
+impl<'a> StateIter<'a> {
+    fn new(state: &'a State) -> Self {
+        let underlying = state.meta.iter();
+        Self { state, underlying }
+    }
+}
+
+impl<'a> Iterator for StateIter<'a> {
+    type Item = Option<ValueRef<'a>>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        match self.underlying.next() {
+            None => return None, // we are done!
+            Some(m) => Some(self.state.get_from_meta(m)),
+        }
+    }
 }
 
 #[derive(Debug, PartialEq, Clone)]
@@ -168,6 +199,32 @@ impl Value {
             Err(_) => Value::Big(BigUint::from_str_radix(value, 10).unwrap()),
         }
     }
+
+    pub fn is_zero(&self) -> bool {
+        match &self {
+            Value::Long(value) => *value == 0,
+            Value::Big(value) => value.is_zero(),
+        }
+    }
+
+    /// Returns the value as a fixed with bit string. Returns None if the value is an array.
+    pub fn to_bit_string(&self, width: WidthInt) -> Option<String> {
+        let base_str = match &self {
+            Value::Long(value) => format!("{value:b}"),
+            Value::Big(value) => value.to_str_radix(2),
+        };
+        let base_len = base_str.len();
+        if base_len == width as usize {
+            Some(base_str)
+        } else {
+            // pad with zeros
+            assert!(base_len < width as usize);
+            let zeros = width as usize - base_len;
+            let mut out = "0".repeat(zeros);
+            out.push_str(&base_str);
+            Some(out)
+        }
+    }
 }
 
 #[derive(Debug, PartialEq)]
@@ -177,12 +234,24 @@ pub enum ValueRef<'a> {
 }
 
 impl<'a> ValueRef<'a> {
-    fn cloned(&self) -> Value {
+    pub fn cloned(&self) -> Value {
         match self {
             ValueRef::Long(value) => Value::Long(*value),
             ValueRef::Big(value) => Value::Big((*value).clone()),
         }
     }
+
+    pub fn is_zero(&self) -> bool {
+        match self {
+            ValueRef::Long(value) => *value == 0,
+            ValueRef::Big(value) => value.is_zero(),
+        }
+    }
+
+    /// Returns the value as a fixed with bit string. Returns None if the value is an array.
+    pub fn to_bit_string(&self, width: WidthInt) -> Option<String> {
+        self.cloned().to_bit_string(width) // TODO: optimize
+    }
 }
 
 #[cfg(test)]