diff --git a/patronus/Cargo.toml b/patronus/Cargo.toml index 60b3e2e..7300e69 100644 --- 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 index 2b3cde2..7e693a7 100644 --- 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) -> StringRef { + pub fn string(&mut self, value: std::borrow::Cow) -> 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 index f663a91..ca19348 100644 --- 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, expr: ExprRef) { + let name = ctx.string(name); + self.outputs.push(Output { name, expr }); + } + pub fn add_state(&mut self, ctx: &Context, state: impl Into) -> StateRef { let state = state.into(); assert!(ctx[state.symbol].is_symbol());