witness: parse multiple array updates

cucapra · Nov 20, 2023 · accfc15 · accfc15
1 parent 73fbccf
commit accfc15
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 2 deletions.
diff --git a/src/btor2/witness.rs b/src/btor2/witness.rs
@@ -107,7 +107,7 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
                         // we ignore anything but the starting state
                         let (ii, name, value) = parse_assignment(&tok.tokens);
                         ensure_space(&mut wit.init, ii);
-                        wit.init[ii] = Some(value);
+                        wit.init[ii] = Some(update_value(&wit.init[ii], value));
                         ensure_space(&mut wit.init_names, ii);
                         wit.init_names[ii] = Some(name.to_string());
                     }
@@ -129,7 +129,7 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
                     let tok = tokenize_line(line);
                     let (ii, name, value) = parse_assignment(&tok.tokens);
                     ensure_space(&mut inputs, ii);
-                    inputs[ii] = Some(value);
+                    inputs[ii] = Some(update_value(&inputs[ii], value));
                     if wit.inputs.is_empty() {
                         // the first time around, we save the names
                         ensure_space(&mut wit.input_names, ii);
@@ -145,6 +145,25 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result<Vec
     Ok(out)
 }
 
+// combines witness values (this is mostly relevant for arrays which might have several updates)
+fn update_value(old: &Option<WitnessValue>, new: WitnessValue) -> WitnessValue {
+    match (old, new) {
+        (None, n) => n,
+        (Some(WitnessValue::Array(oa)), WitnessValue::Array(mut na)) => {
+            assert!(na.default.is_none(), "cannot overwrite the default value!");
+            assert_eq!(oa.tpe, na.tpe);
+            let mut updates = oa.updates.clone();
+            updates.append(&mut na.updates);
+            WitnessValue::Array(WitnessArray {
+                tpe: oa.tpe,
+                default: oa.default.clone(),
+                updates,
+            })
+        }
+        (o, n) => panic!("Unexpected combination: {o:?} {n:?}"),
+    }
+}
+
 /// Expands the vector `v` if necessary to ensure that `index` is a valid entry.
 fn ensure_space<T: Default + Clone>(v: &mut Vec<T>, index: usize) {
     if index >= v.len() {

diff --git a/tests/btor2_witness_tests.rs b/tests/btor2_witness_tests.rs
@@ -25,6 +25,13 @@ fn test_const_array_example_witness() {
     insta::assert_snapshot!(serialized);
 }
 
+#[test]
+fn test_const_array_example_witness_2() {
+    let wit = btor2::parse_witness(&mut CONST_ARRAY_EXAMPLE_2.as_bytes()).unwrap();
+    let serialized = btor2::witness_to_string(&wit);
+    assert_eq!(serialized.trim(), CONST_ARRAY_EXAMPLE_2.trim());
+}
+
 #[test]
 fn test_multiple_witnesses() {
     let wit = btor2::parse_witness(&mut MULTIPLE.as_bytes()).unwrap();
@@ -72,6 +79,20 @@ b0
 .
 "#;
 
+// modified version of the original, to test multiple array updates
+const CONST_ARRAY_EXAMPLE_2: &str = r#"
+sat
+b0
+#0
+0 11111 addr#0
+1 11111111111111111111111111111111 data#0
+2 [11111] 11111111111111111111111111111110 mem#0
+2 [11110] 11111111111111111111111111111110 mem#0
+4 11111 a#0
+@0
+.
+"#;
+
 const MULTIPLE: &str = r#"
 sat
 b0