btor2: add array ite to parser

cucapra · Nov 29, 2023 · a71aa1c · a71aa1c
1 parent a9ff34d
commit a71aa1c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/src/btor2/parse.rs b/src/btor2/parse.rs
@@ -371,7 +371,7 @@ impl<'a> Parser<'a> {
                 if tpe.is_bit_vector() {
                     self.ctx.bv_ite(a, b, c)
                 } else {
-                    todo!("Array ITE")
+                    self.ctx.array_ite(a, b, c)
                 }
             }
             "write" => self.ctx.array_store(a, b, c),

diff --git a/src/ir/expr.rs b/src/ir/expr.rs
@@ -59,6 +59,9 @@ pub trait ExprNodeConstruction:
     fn bv_ite(&mut self, cond: ExprRef, tru: ExprRef, fals: ExprRef) -> ExprRef {
         self.add_node(Expr::BVIte { cond, tru, fals })
     }
+    fn array_ite(&mut self, cond: ExprRef, tru: ExprRef, fals: ExprRef) -> ExprRef {
+        self.add_node(Expr::ArrayIte { cond, tru, fals })
+    }
     fn implies(&mut self, a: ExprRef, b: ExprRef) -> ExprRef {
         self.add_node(Expr::BVImplies(a, b))
     }