wip: SMT BMC

.gitignore

@@ -1,3 +1,4 @@
 /target
 /Cargo.lock
 /.idea/
+/*.smt

examples/bmc.rs

@@ -3,7 +3,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use clap::Parser;
-use libpatron::ir::SerializableIrNode;
+use libpatron::ir::*;
 use libpatron::*;
 
 #[derive(Parser, Debug)]
@@ -21,4 +21,27 @@ fn main() {
     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!();
+    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
+    );
+    let checker = mc::SmtModelChecker::new(solver, checker_opts);
+    let res = checker.check(&ctx, &sys, k_max).unwrap();
+    match res {
+        mc::ModelCheckResult::Success => {
+            println!("unsat");
+        }
+        mc::ModelCheckResult::Fail(_) => {
+            println!("sat");
+            todo!("print witness")
+        }
+    }
 }

src/ir/serialize.rs

@@ -470,16 +470,9 @@ impl SerializableIrNode for TransitionSystem {
             };
 
         // signals
-        for (ii, signal) in self
-            .signals
-            .iter()
-            .enumerate()
-            .flat_map(|(ii, maybe_signal)| maybe_signal.as_ref().and_then(|s| Some((ii, s))))
-            // do not explicitly print states
-            .filter(|(_, s)| !matches!(s.kind, SignalKind::State))
-        {
+        for (ii, signal) in self.get_signals(|s| !matches!(s.kind, SignalKind::State)) {
             // we deduce the expression id from the index
-            let expr = ctx.get(ExprRef::from_index(ii));
+            let expr = ctx.get(ii);
 
             // skip symbols and literals
             if inline_expr_for_transition_system(expr) {
@@ -493,7 +486,7 @@ impl SerializableIrNode for TransitionSystem {
             if let Some(name_ref) = signal.name {
                 write!(writer, "{}", ctx.get(name_ref))?;
             } else {
-                write!(writer, "%{}", ii)?;
+                write!(writer, "%{}", ii.index())?;
             }
 
             // print the type
@@ -511,7 +504,7 @@ impl SerializableIrNode for TransitionSystem {
         }
 
         // states
-        for state in self.states.iter() {
+        for state in self.states() {
             let name = state
                 .symbol
                 .get_symbol_name(ctx)

src/ir/smt.rs

@@ -198,6 +198,12 @@ impl GetNode<str, StringRef> for Context {
     }
 }
 
+impl GetNode<str, &StringRef> for Context {
+    fn get(&self, reference: &StringRef) -> &str {
+        self.get(*reference)
+    }
+}
+
 impl AddNode<Expr, ExprRef> for Context {
     fn add_node(&mut self, value: Expr) -> ExprRef {
         let (index, _) = self.exprs.insert_full(value);
@@ -395,6 +401,16 @@ pub struct ArrayType {
     pub index_width: WidthInt,
     pub data_width: WidthInt,
 }
+
+impl ArrayType {
+    pub fn data_type(&self) -> Type {
+        Type::BV(self.data_width)
+    }
+    pub fn index_type(&self) -> Type {
+        Type::BV(self.index_width)
+    }
+}
+
 #[derive(Debug, PartialEq, Eq, Clone, Copy, Hash)]
 pub enum Type {
     BV(WidthInt),

src/ir/transition_system.rs

@@ -74,9 +74,9 @@ pub struct InputRef(usize);
 #[derive(Debug, PartialEq, Eq)]
 pub struct TransitionSystem {
     pub name: String,
-    pub(crate) states: Vec<State>,
+    states: Vec<State>,
     /// signal meta-data stored in a dense hash map, matching the index of the corresponding expression
-    pub(crate) signals: Vec<Option<SignalInfo>>,
+    signals: Vec<Option<SignalInfo>>,
 }
 
 impl TransitionSystem {
@@ -127,6 +127,32 @@ impl TransitionSystem {
     {
         modify(self.states.get_mut(reference.0).unwrap())
     }
+
+    pub fn states(&self) -> core::slice::Iter<'_, State> {
+        self.states.iter()
+    }
+
+    pub fn get_signals(&self, filter: fn(&SignalInfo) -> bool) -> Vec<(ExprRef, SignalInfo)> {
+        self.signals
+            .iter()
+            .enumerate()
+            .filter(|(_, opt)| opt.as_ref().map(|i| filter(i)).unwrap_or(false))
+            .map(|(index, opt_info)| {
+                (
+                    ExprRef::from_index(index),
+                    opt_info.as_ref().unwrap().clone(),
+                )
+            })
+            .collect::<Vec<_>>()
+    }
+
+    pub fn constraints(&self) -> Vec<(ExprRef, SignalInfo)> {
+        self.get_signals(|info| info.kind == SignalKind::Constraint)
+    }
+
+    pub fn bad_states(&self) -> Vec<(ExprRef, SignalInfo)> {
+        self.get_signals(|info| info.kind == SignalKind::Bad)
+    }
 }
 
 impl GetNode<SignalInfo, ExprRef> for TransitionSystem {

src/lib.rs

@@ -6,5 +6,4 @@ extern crate lazy_static;
 
 pub mod btor2;
 pub mod ir;
-mod mc;
-mod smt;
+pub mod mc;

src/mc/mod.rs

@@ -1,7 +1,10 @@
 // Copyright 2023 The Regents of the University of California
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
-mod state;
 mod smt;
+mod state;
 
+pub use smt::{
+    ModelCheckResult, SmtModelChecker, SmtModelCheckerOptions, SmtSolverCmd, BITWUZLA_CMD,
+};
 pub use state::{State, Value, ValueRef, Witness};