Only emit attributes used by some backend (#3983)

Automerge #3983: Only emit attributes used by some backend
runtimeverification · Feb 29, 2024 · dd9f6e7 · dd9f6e7
1 parent 4555a40
commit dd9f6e7
Show file tree

Hide file tree

Showing 3 changed files with 303 additions and 146 deletions.
diff --git a/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out b/k-distribution/tests/regression-new/set-symbolic-tests/inset-11-spec.k.out
@@ -8,12 +8,12 @@
     false
   #Equals
     X:MyId in SET
+    SetItem ( Z:MyId )
   }
 #And
   {
     false
   #Equals
     Z:MyId in SET
-    SetItem ( X:MyId )
   }
 [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -2013,7 +2013,10 @@ private void convert(
 
     for (Tuple2<Tuple2<Att.Key, String>, ?> attribute :
         // Sort to stabilize error messages
-        stream(att.att()).sorted(Comparator.comparing(Tuple2::toString)).toList()) {
+        stream(att.att())
+            .filter(e -> e._1._1.shouldEmit())
+            .sorted(Comparator.comparing(Tuple2::toString))
+            .toList()) {
       Att.Key key = attribute._1._1;
       String strKey = key.key();
       String clsName = attribute._1._2;