Add liveness to safety construction for supporting temporal proofs

fly/src/printer.rs

@@ -45,7 +45,8 @@ fn left_associative(_op: &BinOp) -> bool {
     false
 }
 
-fn binder(b: &Binder) -> String {
+/// Pretty-print a binder
+pub fn binder(b: &Binder) -> String {
     format!("{}:{}", b.name, sort(&b.sort))
 }
 

fly/src/semantics.rs

@@ -518,6 +518,10 @@ mod tests {
     #[test]
     #[allow(clippy::redundant_clone)]
     fn test_eval() {
+        // TODO(oded): we should also test evaluation in the presence of
+        // quantifiers that shadow each other, e.g. evaluate:
+        // forall x. exists x. p(x).
+
         let sort = |n: usize| Sort::Uninterpreted(format!("T{n}"));
 
         let sig = Signature {

fly/src/syntax.rs

@@ -41,12 +41,20 @@ impl Sort {
 
 impl From<&str> for Sort {
     /// This is mostly for the Binder smart constructor, making it possible to
-    /// pass either Sort, &Sort, or &str
+    /// pass either Sort, &Sort, &str, or &String
     fn from(value: &str) -> Self {
         Self::uninterpreted(value)
     }
 }
 
+impl From<&String> for Sort {
+    /// This is mostly for the Binder smart constructor, making it possible to
+    /// pass either Sort, &Sort, &str, or &String
+    fn from(value: &String) -> Self {
+        Self::uninterpreted(value)
+    }
+}
+
 impl From<&Sort> for Sort {
     /// This is mostly for the Binder smart constructor, making it possible to
     /// pass either Sort, &Sort, or &str

verify/src/lib.rs

@@ -17,3 +17,4 @@
 pub mod error;
 pub mod module;
 pub mod safety;
+pub mod temporal;

verify/src/safety.rs

@@ -12,7 +12,8 @@ use fly::transitions::{MaybeSpannedTerm, Proof};
 /// A temporal property expressed as an invariant problem.
 #[derive(Debug, Clone)]
 pub struct InvariantAssertion {
-    sig: Signature,
+    /// The signature
+    pub sig: Signature,
     /// The initial states
     pub init: Term,
     /// The states reachable in one step