From 1a0b5d8ea70391100e5d3b7b08bc8b228f4627ee Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Fri, 24 May 2024 03:42:12 +1200
Subject: [PATCH] write_btor: Include `$assert` and `$assume` cells in -ywmap
 output

---
 backends/btor/btor.cc | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index bba7249c7..ca7cf8a7f 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -98,6 +98,8 @@ struct BtorWorker
 	vector<ywmap_btor_sig> ywmap_states;
 	dict<SigBit, int> ywmap_clock_bits;
 	dict<SigBit, int> ywmap_clock_inputs;
+	vector<Cell *> ywmap_asserts;
+	vector<Cell *> ywmap_assumes;
 
 
 	PrettyJson ywmap_json;
@@ -1280,6 +1282,8 @@ struct BtorWorker
 				btorf("%d or %d %d %d\n", nid_a_or_not_en, sid, nid_a, nid_not_en);
 				btorf("%d constraint %d\n", nid, nid_a_or_not_en);
 
+				if (ywmap_json.active()) ywmap_assumes.emplace_back(cell);
+
 				btorf_pop(log_id(cell));
 			}
 
@@ -1304,6 +1308,8 @@ struct BtorWorker
 					} else {
 						int nid = next_nid++;
 						btorf("%d bad %d%s\n", nid, nid_en_and_not_a, getinfo(cell, true));
+
+						if (ywmap_json.active()) ywmap_asserts.emplace_back(cell);
 					}
 				}
 
@@ -1461,6 +1467,7 @@ struct BtorWorker
 				log_assert(cursor == 0);
 				log_assert(GetSize(todo) == 1);
 				btorf("%d bad %d\n", nid, todo[cursor]);
+				// What do we do with ywmap_asserts when using single_bad?
 			}
 		}
 
@@ -1526,6 +1533,18 @@ struct BtorWorker
 				emit_ywmap_btor_sig(entry);
 			ywmap_json.end_array();
 
+			ywmap_json.name("asserts");
+			ywmap_json.begin_array();
+			for (Cell *cell : ywmap_asserts)
+				ywmap_json.value(witness_path(cell));
+			ywmap_json.end_array();
+
+			ywmap_json.name("assumes");
+			ywmap_json.begin_array();
+			for (Cell *cell : ywmap_assumes)
+				ywmap_json.value(witness_path(cell));
+			ywmap_json.end_array();
+
 			ywmap_json.end_object();
 		}
 	}