expr/ts: make string function public and add add_output helper method

cucapra · Dec 10, 2024 · 075b7ac · 075b7ac
1 parent 2b71fc3
commit 075b7ac
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/patronus/Cargo.toml b/patronus/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "patronus"
-version = "0.28.0"
+version = "0.28.1"
 description = "Hardware bug-finding toolkit."
 homepage = "https://kevinlaeufer.com"
 keywords = ["RTL", "btor", "model-checking", "SMT", "bit-vector"]

diff --git a/patronus/src/expr/context.rs b/patronus/src/expr/context.rs
@@ -105,7 +105,7 @@ impl Context {
         ExprRef::from_index(index)
     }
 
-    pub(crate) fn string(&mut self, value: std::borrow::Cow<str>) -> StringRef {
+    pub fn string(&mut self, value: std::borrow::Cow<str>) -> StringRef {
         if let Some(index) = self.strings.get_index_of(value.as_ref()) {
             StringRef::from_index(index)
         } else {

diff --git a/patronus/src/system/transition_system.rs b/patronus/src/system/transition_system.rs
@@ -82,6 +82,11 @@ impl TransitionSystem {
         self.names[symbol] = name;
     }
 
+    pub fn add_output(&mut self, ctx: &mut Context, name: std::borrow::Cow<str>, expr: ExprRef) {
+        let name = ctx.string(name);
+        self.outputs.push(Output { name, expr });
+    }
+
     pub fn add_state(&mut self, ctx: &Context, state: impl Into<State>) -> StateRef {
         let state = state.into();
         assert!(ctx[state.symbol].is_symbol());