Symbolic testing

Cargo.toml

@@ -5,5 +5,5 @@ members = ["crates/*"]
 opt-level = 3
 
 [profile.dev]
-# Speeds up the build. May need to diable for debugging.
+# Speeds up the build. May need to disable for debugging.
 debug = 0

crates/analyzer/src/db.rs

@@ -110,6 +110,8 @@ pub trait AnalyzerDb: SourceDb + Upcast<dyn SourceDb> + UpcastMut<dyn SourceDb>
     fn module_submodules(&self, module: ModuleId) -> Rc<[ModuleId]>;
     #[salsa::invoke(queries::module::module_tests)]
     fn module_tests(&self, module: ModuleId) -> Vec<FunctionId>;
+    #[salsa::invoke(queries::module::module_invariants)]
+    fn module_invariants(&self, module: ModuleId) -> Vec<FunctionId>;
 
     // Module Constant
     #[salsa::cycle(queries::module::module_constant_type_cycle)]

crates/analyzer/src/db/queries/module.rs

@@ -760,3 +760,12 @@ pub fn module_tests(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
         .filter(|function| function.is_test(db))
         .collect()
 }
+
+pub fn module_invariants(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
+    ingot
+        .all_functions(db)
+        .iter()
+        .copied()
+        .filter(|function| function.is_invariant(db))
+        .collect()
+}