remove reduce operators from IR and fix an infinite loop bug

src/btor2/parse.rs

@@ -175,13 +175,9 @@ impl<'a> Parser<'a> {
         expected_type: Type,
     ) -> ParseLineResult<ExprRef> {
         // first we check for internal consitency
-        match expr.type_check(self.ctx) {
-            Err(e) => {
-                let _ =
-                    self.add_error(line, line, format!("Failed to type check: {}", e.get_msg()));
-                return Err(());
-            }
-            Ok(_) => {}
+        if let Err(e) = expr.type_check(self.ctx) {
+            self.add_error(line, line, format!("Failed to type check: {}", e.get_msg()));
+            return Err(());
         }
         // then we make sure that the type of the expression is actually the type that was
         // declared in the btor2 line
@@ -251,7 +247,28 @@ impl<'a> Parser<'a> {
                 let by = self.parse_width_int(line, tokens[4], "extension amount")?;
                 self.ctx.sign_extend(e, by)
             }
-            other => panic!("unexpected binary op: {other}"),
+            "redor" => {
+                let width = e.get_type(self.ctx).get_bit_vector_width().unwrap();
+                if width == 1 {
+                    e
+                } else {
+                    // redor is true iff at least one bit is a one
+                    let zero = self.ctx.zero(width);
+                    let eq_zero = self.ctx.bv_equal(e, zero);
+                    self.ctx.not(eq_zero)
+                }
+            }
+            "redand" => {
+                let width = e.get_type(self.ctx).get_bit_vector_width().unwrap();
+                if width == 1 {
+                    e
+                } else {
+                    // redand is true iff all bits are one
+                    let mask = self.ctx.mask(width);
+                    self.ctx.bv_equal(e, mask)
+                }
+            }
+            other => panic!("unexpected unary op: {other}"),
         };
         self.check_expr_type(res, line, tpe)
     }

src/ir/analysis.rs

@@ -113,15 +113,6 @@ impl ForEachChild<ExprRef> for Expr {
             Expr::BVNegate(e, _) => {
                 (visitor)(e);
             }
-            Expr::BVReduceOr(e) => {
-                (visitor)(e);
-            }
-            Expr::BVReduceAnd(e) => {
-                (visitor)(e);
-            }
-            Expr::BVReduceXor(e) => {
-                (visitor)(e);
-            }
             Expr::BVEqual(a, b) => {
                 (visitor)(a);
                 (visitor)(b);

src/ir/expr.rs

@@ -46,6 +46,10 @@ pub trait ExprNodeConstruction:
     fn zero(&mut self, width: WidthInt) -> ExprRef {
         self.bv_lit(0, width)
     }
+    fn mask(&mut self, width: WidthInt) -> ExprRef {
+        let value = ((1 as BVLiteralInt) << width) - 1;
+        self.bv_lit(value, width)
+    }
     fn one(&mut self, width: WidthInt) -> ExprRef {
         self.bv_lit(1, width)
     }
@@ -180,7 +184,7 @@ impl Context {
     pub fn add_unique_str(&mut self, value: &str) -> StringRef {
         let mut name: String = value.to_string();
         let mut count: usize = 0;
-        while self.is_interned(value) {
+        while self.is_interned(&name) {
             name = format!("{value}_{count}");
             count += 1;
         }
@@ -290,9 +294,6 @@ pub enum Expr {
     },
     BVNot(ExprRef, WidthInt),
     BVNegate(ExprRef, WidthInt),
-    BVReduceOr(ExprRef),
-    BVReduceAnd(ExprRef),
-    BVReduceXor(ExprRef),
     // binary operations
     BVEqual(ExprRef, ExprRef),
     BVImplies(ExprRef, ExprRef),

src/ir/serialize.rs

@@ -83,27 +83,6 @@ where
             }
             write!(writer, ")")
         }
-        Expr::BVReduceOr(e) => {
-            write!(writer, "redor(")?;
-            if (serialize_child)(e, ctx, writer)? {
-                serialize_expr_ref(e, ctx, writer, serialize_child)?;
-            }
-            write!(writer, ")")
-        }
-        Expr::BVReduceAnd(e) => {
-            write!(writer, "redand(")?;
-            if (serialize_child)(e, ctx, writer)? {
-                serialize_expr_ref(e, ctx, writer, serialize_child)?;
-            }
-            write!(writer, ")")
-        }
-        Expr::BVReduceXor(e) => {
-            write!(writer, "redxor(")?;
-            if (serialize_child)(e, ctx, writer)? {
-                serialize_expr_ref(e, ctx, writer, serialize_child)?;
-            }
-            write!(writer, ")")
-        }
         Expr::BVEqual(a, b) => {
             write!(writer, "eq(")?;
             if (serialize_child)(a, ctx, writer)? {

src/ir/type_check.rs

@@ -136,18 +136,6 @@ impl TypeCheck for Expr {
             }
             Expr::BVNot(e, width) => Ok(e.get_type(ctx).expect_bv_of(width, "not")?),
             Expr::BVNegate(e, width) => Ok(e.get_type(ctx).expect_bv_of(width, "not")?),
-            Expr::BVReduceOr(e) => {
-                e.get_type(ctx).expect_bv("or reduction")?;
-                Ok(Type::BV(1))
-            }
-            Expr::BVReduceAnd(e) => {
-                e.get_type(ctx).expect_bv("and reduction")?;
-                Ok(Type::BV(1))
-            }
-            Expr::BVReduceXor(e) => {
-                e.get_type(ctx).expect_bv("xor reduction")?;
-                Ok(Type::BV(1))
-            }
             Expr::BVEqual(a, b) => {
                 expect_same_width_bvs(ctx, "bit-vector equality", a, b)?;
                 Ok(Type::BV(1))
@@ -291,9 +279,6 @@ impl TypeCheck for Expr {
             Expr::BVSlice { e: _, hi, lo } => Type::BV(hi - lo + 1),
             Expr::BVNot(_, width) => Type::BV(width),
             Expr::BVNegate(_, width) => Type::BV(width),
-            Expr::BVReduceOr(_) => Type::BV(1),
-            Expr::BVReduceAnd(_) => Type::BV(1),
-            Expr::BVReduceXor(_) => Type::BV(1),
             Expr::BVEqual(_, _) => Type::BV(1),
             Expr::BVImplies(_, _) => Type::BV(1),
             Expr::BVGreater(_, _) => Type::BV(1),

src/mc/smt.rs

@@ -520,9 +520,6 @@ where
             }
         }
         Expr::BVNegate(_, _) => todo!(),
-        Expr::BVReduceOr(_) => todo!(),
-        Expr::BVReduceAnd(_) => todo!(),
-        Expr::BVReduceXor(_) => todo!(),
         Expr::BVEqual(a_ref, b_ref) => {
             let a = convert_expr(smt_ctx, ctx, *a_ref, rename_sym);
             let b = convert_expr(smt_ctx, ctx, *b_ref, rename_sym);