Parser for new json format and new operators (Implies and Equiv)

Author: GBathie

Cargo.toml

@@ -15,6 +15,8 @@ fxhash = "0.2.1"
 itertools = "0.14.0"
 log = "0.4.27"
 ordered-float = "5.0.0"
+serde = { version = "1.0.219", features = ["derive"] }
+serde_json = "1.0.140"
 thiserror = "2.0.12"
 
 [dev-dependencies]

src/algos/meta/mod.rs

@@ -89,7 +89,7 @@ where
 
 /// Solve Boolean Synthesis problem using Divide and Conquer and the algorithm specified in `params`.
 ///
-/// If the number of traces is more than 128 split immediately.
+/// If the number of traces is more than 128, split immediately.
 /// Otherwise, try to solve the instance with the algorithm implemented by `params`.
 /// If no solution is found, try to find one by splitting recursively.
 /// Splitting is handled using [`split_and_solve_non_overlapping`].

src/bin/experiments.rs

@@ -16,32 +16,32 @@ fn main() {
     env_logger::init();
 
     let args = CliArgs::parse();
-    let (traces, alphabet, target, operators) = traces_from_file(&args.input_filename);
+    let instance = traces_from_file(&args.input_filename);
 
     let (time, sol, name) = match args.command {
         AlgoCommand::Enum(p) => get_name_time_sol(
-            traces,
-            alphabet,
-            operators,
-            target,
+            instance.traces,
+            instance.atomic_propositions,
+            instance.operators,
+            instance.target,
             args.max_size_ltl,
             args.domin_nb,
             p,
         ),
         AlgoCommand::SetCover(p) => get_name_time_sol(
-            traces,
-            alphabet,
-            operators,
-            target,
+            instance.traces,
+            instance.atomic_propositions,
+            instance.operators,
+            instance.target,
             args.max_size_ltl,
             args.domin_nb,
             p,
         ),
         AlgoCommand::BeamSearch(p) => get_name_time_sol(
-            traces,
-            alphabet,
-            operators,
-            target,
+            instance.traces,
+            instance.atomic_propositions,
+            instance.operators,
+            instance.target,
             args.max_size_ltl,
             args.domin_nb,
             p,

src/ltl/cm.rs

@@ -78,4 +78,6 @@ impl CharMatrix {
     binop_for_cm!(bitor as or);
     binop_for_cm!(bitand as and);
     binop_for_cm!(until);
+    binop_for_cm!(implies);
+    binop_for_cm!(equiv);
 }

src/ltl/cs.rs

@@ -2,13 +2,13 @@
 //! and related operators.
 use std::{
     fmt::{Debug, Display},
-    ops::{BitAnd, BitOr, Not},
+    ops::{BitAnd, BitOr, BitXor, Not},
 };
 
 /// Characteristic sequence of an LTL formula on a trace.
 #[derive(Clone, Copy, PartialEq, Eq, Hash)]
 pub struct CharSeq {
-    values: u64,
+    pub(crate) values: u64,
     length: usize,
 }
 
@@ -74,6 +74,41 @@ impl CharSeq {
         (self.values & 1) == 1
     }
 
+    /// Boolean implication operator (->)
+    #[inline]
+    pub(crate) fn implies(self, rhs: Self) -> Self {
+        let CharSeq { values: x, length } = self;
+        let CharSeq {
+            values: y,
+            length: _l2,
+        } = rhs;
+        // x -> y <=> !x or y
+        let values = x.not().bitor(y);
+        let values = if self.length < 64 {
+            values & ((1u64 << self.length) - 1)
+        } else {
+            values
+        };
+        CharSeq { values, length }
+    }
+
+    /// Boolean equivalence operator (<->)
+    #[inline]
+    pub(crate) fn equiv(self, rhs: Self) -> Self {
+        let CharSeq { values: x, length } = self;
+        let CharSeq {
+            values: y,
+            length: _l2,
+        } = rhs;
+        let values = (x.bitxor(y)).not();
+        let values = if self.length < 64 {
+            values & ((1u64 << self.length) - 1)
+        } else {
+            values
+        };
+        CharSeq { values, length }
+    }
+
     /// LTL Next operator (X)
     #[inline]
     pub(crate) fn next(mut self) -> Self {
@@ -167,7 +202,7 @@ impl FromIterator<bool> for CharSeq {
 
 #[cfg(test)]
 mod tests {
-    use rand::{rng, Rng};
+    use rand::{Rng, rng};
 
     use super::*;
 
@@ -320,4 +355,44 @@ mod tests {
             assert_eq!(U(x, y), y | (x & X(U(x, y))));
         }
     }
+
+    #[test]
+    fn x_implies_x() {
+        for _ in 0..100 {
+            let x = random_seq();
+            assert_eq!(x.implies(x).values, (1 << x.length) - 1);
+        }
+    }
+
+    #[test]
+    fn implies_def() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.implies(y), x.not() | y);
+        }
+    }
+
+    #[test]
+    fn x_equiv_x() {
+        for _ in 0..100 {
+            let x = random_seq();
+            assert_eq!(x.equiv(x).values, (1 << x.length) - 1);
+        }
+    }
+
+    #[test]
+    fn equiv_iff_double_implies() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.equiv(y), x.implies(y) & y.implies(x));
+        }
+    }
+
+    #[test]
+    fn equiv_def() {
+        for _ in 0..100 {
+            let (x, y) = random_pair();
+            assert_eq!(x.equiv(y), (x & y) | (x.not() & y.not()));
+        }
+    }
 }