Fix README and more clippy warnings

Signed-off-by: edenfrenkel <[email protected]>
flyvy-verifier · Feb 22, 2024 · ad21d3a · ad21d3a
1 parent 043348a
commit ad21d3a
Show file tree

Hide file tree

Showing 6 changed files with 24 additions and 21 deletions.
diff --git a/README.md b/README.md
@@ -16,7 +16,7 @@ Run `./tools/download-solvers.sh` to get compatible versions of the supported SM
 ```sh
 cargo run -- verify temporal-verifier/examples/lockserver.fly
 
-cargo run -- infer qalpha temporal-verifier/examples/lockserver.fly --max-exist 0 --until-safe
+cargo run -- infer qalpha temporal-verifier/examples/lockserver.fly --quantifier "F node 2" --clause-size=3 --cubes=0
 
 # invariant inference with qalpha
 # note: this example takes several minutes to run

diff --git a/fly/src/rets.rs b/fly/src/rets.rs
@@ -651,20 +651,23 @@ mutable f(bool): s
         let model1 = Model::new(
             &module.signature,
             &vec![3],
-            vec![Interpretation::new(&vec![2, 3], |xs| {
-                if xs[0] == 0 {
-                    2
-                } else {
-                    0
-                }
-            })],
+            vec![Interpretation::new(
+                &[2, 3],
+                |xs| {
+                    if xs[0] == 0 {
+                        2
+                    } else {
+                        0
+                    }
+                },
+            )],
         );
 
         let back_convert_model = module.convert_non_bool_relations()?;
         let model2 = Model::new(
             &module.signature,
             &vec![3],
-            vec![Interpretation::new(&vec![2, 3, 2], |xs| match xs {
+            vec![Interpretation::new(&[2, 3, 2], |xs| match xs {
                 [0, 2] | [1, 0] => 1,
                 _ => 0,
             })],

diff --git a/fly/src/semantics.rs b/fly/src/semantics.rs
@@ -499,18 +499,18 @@ mod tests {
 
     #[test]
     fn test_interp_new() {
-        let interp = Interpretation::new(&vec![3], |_| 2);
+        let interp = Interpretation::new(&[3], |_| 2);
         assert_eq!(interp.get(&[]), 2);
         assert_eq!(interp.data, vec![2]);
 
-        let interp = Interpretation::new(&vec![3, 2, 4], |es| es[0] + es[1]);
+        let interp = Interpretation::new(&[3, 2, 4], |es| es[0] + es[1]);
         for i in 0..3 {
             for j in 0..2 {
                 assert_eq!(interp.get(&[i, j]), i + j, "wrong value at {i}, {j}");
             }
         }
 
-        let interp = Interpretation::new(&vec![3, 2, 4, 7], |es| es[0] + es[1] * es[2]);
+        let interp = Interpretation::new(&[3, 2, 4, 7], |es| es[0] + es[1] * es[2]);
         for i in 0..3 {
             for j in 0..2 {
                 for k in 0..4 {

diff --git a/inference/src/qalpha/language.rs b/inference/src/qalpha/language.rs
@@ -2497,10 +2497,10 @@ mod tests {
         assert_eq!(
             weakenings,
             HashSet::from_iter([
-                clause(vec![lit("a", true).into(), lit("b", false)]),
-                clause(vec![lit("a", true).into(), lit("c", false)]),
-                clause(vec![lit("b", true).into(), lit("a", false)]),
-                clause(vec![lit("b", true).into(), lit("c", false)]),
+                clause(vec![lit("a", true), lit("b", false)]),
+                clause(vec![lit("a", true), lit("c", false)]),
+                clause(vec![lit("b", true), lit("a", false)]),
+                clause(vec![lit("b", true), lit("c", false)]),
             ])
         );
 
@@ -2631,8 +2631,8 @@ mod tests {
             signature: sig.as_ref().clone(),
             universe: vec![t_count, s_count],
             interp: vec![
-                Interpretation::new(&vec![t_count, 2], |e| in_p.contains(&e[0]) as usize),
-                Interpretation::new(&vec![s_count, 2], |e| in_q.contains(&e[0]) as usize),
+                Interpretation::new(&[t_count, 2], |e| in_p.contains(&e[0]) as usize),
+                Interpretation::new(&[s_count, 2], |e| in_q.contains(&e[0]) as usize),
             ],
         };
 
@@ -2651,7 +2651,7 @@ mod tests {
         let weakenings = q_lang.weaken(&f, &m, &Assignment::new(), |_| false);
         for w in weakenings.iter().permutations(2) {
             assert!(w[0].eval(&m, &Assignment::new()));
-            assert!(!w[0].subsumes(&w[1]) || w[0] == w[1]);
+            assert!(!w[0].subsumes(w[1]) || w[0] == w[1]);
         }
     }
 }
diff --git a/inference/src/qalpha/lemmas.rs b/inference/src/qalpha/lemmas.rs
@@ -33,7 +33,7 @@ macro_rules! timed {
     }};
 }
 
-/// Manages multiple instances of [`PrefixLemmaSet`] and allows weakening them all simultaneously.
+/// Manages lemmas from a [`BoundedLanguage`] and allows weakening them simultaneously.
 pub struct WeakenLemmaSet<L: BoundedLanguage> {
     lang: Arc<L>,
     set: L::Set,

diff --git a/inference/src/qalpha/quant.rs b/inference/src/qalpha/quant.rs
@@ -536,7 +536,7 @@ sort C
             .trim(),
         );
 
-        let sort = |name| Sort::uninterpreted(name);
+        let sort = Sort::uninterpreted;
         let config = QuantifierConfig::new(
             Arc::new(signature),
             vec![None, None, None],