more renames

src/ir/mod.rs

@@ -1,15 +1,15 @@
 // Copyright 2023 The Regents of the University of California
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
+mod expr;
 mod serialize;
-mod smt;
 mod transition_system;
 mod type_check;
 
-pub use serialize::SerializableIrNode;
-pub use smt::{
+pub use expr::{
     bv_value_fits_width, AddNode, ArrayType, BVLiteralInt, Context, Expr, ExprNodeConstruction,
     ExprRef, GetNode, StringRef, Type, WidthInt,
 };
+pub use serialize::SerializableIrNode;
 pub use transition_system::{SignalInfo, SignalKind, State, StateRef, TransitionSystem};
 pub use type_check::{TypeCheck, TypeCheckError};

src/mc/mod.rs

@@ -1,10 +1,6 @@
-// Copyright 2023 The Regents of the University of California
-// released under BSD 3-Clause License
-// author: Kevin Laeufer <[email protected]>
-mod sim;
 mod smt;
 
-pub use sim::Simulator;
+pub use crate::sim::interpreter::Simulator;
 pub use smt::{
     ModelCheckResult, SmtModelChecker, SmtModelCheckerOptions, SmtSolverCmd, BITWUZLA_CMD,
 };

src/mc/sim.rs → src/sim/interpreter.rs

@@ -5,17 +5,28 @@
 use crate::ir::*;
 use crate::sim::ValueStore;
 
+pub trait Simulator {
+    /// Advance the state.
+    fn step(&mut self);
+}
+
 /// Interpreter based simulator for a transition system.
-pub struct Simulator<'a> {
+pub struct Interpreter<'a> {
     ctx: &'a Context,
     sys: &'a TransitionSystem,
     state: ValueStore,
 }
 
-impl<'a> Simulator<'a> {
+impl<'a> Interpreter<'a> {
     pub fn new(ctx: &'a Context, sys: &'a TransitionSystem) -> Self {
         let types = sys.states().map(|s| s.symbol.get_type(ctx));
         let state = ValueStore::new(types);
         Self { ctx, sys, state }
     }
 }
+
+impl<'a> Simulator for Interpreter<'a> {
+    fn step(&mut self) {
+        todo!()
+    }
+}

src/sim/mod.rs

@@ -2,5 +2,9 @@
 // released under BSD 3-Clause License
 // author: Kevin Laeufer <[email protected]>
 mod values;
+// Copyright 2023 The Regents of the University of California
+// released under BSD 3-Clause License
+// author: Kevin Laeufer <[email protected]>
+pub mod interpreter;
 
 pub use values::{Value, ValueRef, ValueStore, Witness};