ir: do not print bv literal or symbol nodes

cucapra · Nov 14, 2023 · 7c9b211 · 7c9b211
1 parent 5ea62f5
commit 7c9b211
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 8 deletions.
diff --git a/src/ir/serialize.rs b/src/ir/serialize.rs
@@ -295,6 +295,14 @@ impl SerializableIrNode for TransitionSystem {
             // do not explicitly print states
             .filter(|(_, s)| !matches!(s.kind, SignalKind::State))
         {
+            // we deduce the expression id from the index
+            let expr = ctx.get(ExprRef::from_index(ii));
+
+            // skip symbols and literals
+            if expr.is_symbol(ctx) || expr.is_bv_lit(ctx) {
+                continue;
+            }
+
             // print the kind
             write!(writer, "{} ", signal.kind)?;
 
@@ -304,8 +312,6 @@ impl SerializableIrNode for TransitionSystem {
             } else {
                 write!(writer, "%{}", ii)?;
             }
-            // we deduce the expression id from the index
-            let expr = ExprRef::from_index(ii);
 
             // print the type
             let tpe = expr.get_type(ctx);

diff --git a/src/ir/smt.rs b/src/ir/smt.rs
@@ -349,6 +349,7 @@ impl Expr {
 
 pub trait ExprIntrospection {
     fn is_symbol(&self, ctx: &impl GetNode<Expr, ExprRef>) -> bool;
+    fn is_bv_lit(&self, _ctx: &impl GetNode<Expr, ExprRef>) -> bool;
     fn get_symbol_name<'a>(
         &self,
         ctx: &'a (impl GetNode<Expr, ExprRef> + GetNode<str, StringRef>),
@@ -362,12 +363,8 @@ impl ExprIntrospection for Expr {
         matches!(self, Expr::BVSymbol { .. } | Expr::ArraySymbol { .. })
     }
 
-    fn get_symbol_name_ref(&self, _ctx: &impl GetNode<Expr, ExprRef>) -> Option<StringRef> {
-        match self {
-            Expr::BVSymbol { name, .. } => Some(*name),
-            Expr::ArraySymbol { name, .. } => Some(*name),
-            _ => None,
-        }
+    fn is_bv_lit(&self, _ctx: &impl GetNode<Expr, ExprRef>) -> bool {
+        matches!(self, Expr::BVLiteral { .. })
     }
 
     fn get_symbol_name<'a>(
@@ -376,13 +373,25 @@ impl ExprIntrospection for Expr {
     ) -> Option<&'a str> {
         self.get_symbol_name_ref(ctx).map(|r| ctx.get(r))
     }
+
+    fn get_symbol_name_ref(&self, _ctx: &impl GetNode<Expr, ExprRef>) -> Option<StringRef> {
+        match self {
+            Expr::BVSymbol { name, .. } => Some(*name),
+            Expr::ArraySymbol { name, .. } => Some(*name),
+            _ => None,
+        }
+    }
 }
 
 impl ExprIntrospection for ExprRef {
     fn is_symbol(&self, ctx: &impl GetNode<Expr, ExprRef>) -> bool {
         ctx.get(*self).is_symbol(ctx)
     }
 
+    fn is_bv_lit(&self, ctx: &impl GetNode<Expr, ExprRef>) -> bool {
+        ctx.get(*self).is_bv_lit(ctx)
+    }
+
     fn get_symbol_name_ref(&self, ctx: &impl GetNode<Expr, ExprRef>) -> Option<StringRef> {
         ctx.get(*self).get_symbol_name_ref(ctx)
     }