wip: print witness function

examples/bmc.rs

@@ -3,6 +3,7 @@
 // author: Kevin Laeufer <[email protected]>
 
 use clap::Parser;
+use libpatron::btor2::print_witness;
 use libpatron::ir::*;
 use libpatron::*;
 
@@ -45,9 +46,8 @@ fn main() {
         mc::ModelCheckResult::Success => {
             println!("unsat");
         }
-        mc::ModelCheckResult::Fail(_) => {
-            println!("sat");
-            println!("TODO: print witness")
+        mc::ModelCheckResult::Fail(wit) => {
+            print_witness(&mut std::io::stdout(), &wit).unwrap();
         }
     }
 }

src/btor2/mod.rs

@@ -7,4 +7,4 @@ mod witness;
 
 pub use parse::{parse_file, parse_str};
 pub use serialize::{serialize, serialize_to_str};
-pub use witness::{parse_witness, parse_witnesses};
+pub use witness::{parse_witness, parse_witnesses, print_witness};

src/btor2/witness.rs

@@ -4,7 +4,7 @@
 
 use crate::btor2::parse::tokenize_line;
 use crate::mc::{State, Value, Witness};
-use std::io::BufRead;
+use std::io::{BufRead, Write};
 
 enum ParserState {
     Start,
@@ -152,3 +152,9 @@ 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<()> {
+    writeln!(out, "sat")?;
+
+    Ok(())
+}