minor documentation fixes

Author: pvdhove

src/algos/beam_search/cache.rs

@@ -158,8 +158,8 @@ impl EnumFormulaCacheLine<BoolCharac> for BeamSearchBoolCacheLine<'_> {
     }
 }
 
-// Stores a SatVec together with the hash of the corresponding Boolean formula.
-// Used when removing dominated formulas in a single  to canonicalize the entries at the end of the push round.
+// Stores a SatVec together with the hash of the corresponding boolean formula.
+// Used when removing dominated formulas in a single pass to canonicalize the entries at the end of the push round.
 #[derive(Debug, PartialEq, Eq)]
 struct PcoBoolFormula {
     pub(crate) f: BoolFormula,

src/algos/beam_search/mod.rs

@@ -1,4 +1,4 @@
-//! Beam Search algorithm for Boolean Synthesis.
+//! Beam Search Algorithm for Boolean Set Cover.
 //!
 //! Bottom-up enumeration with fixed width.
 //! Implemented using a fixed-width cache ([`BeamSearchCache`])
@@ -22,7 +22,7 @@ use super::{BoolAlgoParams, meta::cache::InitialBoolCache};
 pub struct BeamSearchParams {
     /// Number of formulas to keep at each level.
     pub beam_width: usize,
-    /// Maximum enumeration size
+    /// Maximum enumeration size.
     pub max_size_bool: usize,
 }
 

src/algos/enumeration/aux.rs

@@ -130,7 +130,7 @@ where
                 continue;
             }
 
-            // For non-commutative operations
+            // For non-commutative operations.
             let g = apply_binary(op, f_r, f_l);
             if g.eq_target(target) {
                 return Ok(g);

src/algos/enumeration/mod.rs

@@ -1,4 +1,4 @@
-//! Semanting Enumration algorithm for LTL and Boolean Synthesis.
+//! Semantic Enumeration algorithm for LTL Learning and Boolean Set Cover.
 
 pub(crate) mod aux;
 

src/algos/meta/cache.rs

@@ -1,5 +1,5 @@
 //! Boolean cache used after LTL search
-//! given as input to the boolean algorithms.
+//! given as input to the boolean set cover algorithms.
 use std::{
     collections::BinaryHeap,
     hash::{Hash, Hasher},
@@ -138,24 +138,6 @@ impl InitialBoolCache {
             }
         }
 
-        // let (lines, best_sv) = (res.lines, res.best_sv);
-
-        // res.lines = lines
-        //     .into_iter()
-        //     .map(|l| {
-        //         l.into_iter()
-        //             .filter(|(_, lsv, _)| {
-        //                 best_sv[..lsv.size - 1]
-        //                     .iter()
-        //                     .flatten()
-        //                     .any(|lsv2| lsv2.dominates(lsv))
-        //             })
-        //             .collect_vec()
-        //     })
-        //     .collect();
-
-        // res.best_sv = best_sv;
-
         debug!("Creating Initial Cache: {count} formulas, {hits} cache hits");
 
         res
@@ -378,7 +360,7 @@ mod test {
             hash: 0,
         });
 
-        // Ensure that we get min popcount first
+        // Ensure that we get min popcount first.
         assert_eq!(h.pop().unwrap().popcount, 1);
     }
 }

src/algos/meta/mod.rs

@@ -35,9 +35,9 @@ where
     let start = Instant::now();
 
     let atoms = atoms(traces, atomic_propositions);
-    // Add initial formulas
+    // Add initial formulas.
     let (atom, mut ltl_cache) = create_initial_cache(atoms, &target);
-    // Check if target is an atom
+    // Check if target is an atom.
     if let Some(f) = atom {
         let ltl_time = start.elapsed();
         let f_str = rebuild_formula(&f, &ltl_cache);
@@ -51,7 +51,7 @@ where
         };
     }
 
-    // Ltl search
+    // LTL search
     let ltl_res = enum_aux(&mut ltl_cache, &operators, &target, max_size_ltl);
 
     let ltl_time = start.elapsed();
@@ -87,7 +87,7 @@ where
     }
 }
 
-/// Solve Boolean Synthesis problem using Divide and Conquer and the algorithm specified in `params`.
+/// Solve Boolean Set Cover problem using Divide and Conquer and the algorithm specified in `params`.
 ///
 /// If the number of traces is more than 128, split immediately.
 /// Otherwise, try to solve the instance with the algorithm implemented by `params`.
@@ -104,7 +104,7 @@ where
     P: BoolAlgoParams + Clone,
 {
     let nb_traces = target.len();
-    // Check whether the fom
+    // Check whether the formula is already in the cache.
     if let Some(f) = initial_cache.get_from_cv(target, target) {
         // Due to hash collisions, the formula may not be right; we check that
         // the formula has the right characteristic vector.
@@ -170,7 +170,7 @@ where
     })
 }
 
-/// Divide and conquer subrouting to split into two subproblems with clever merging.
+/// Divide and conquer subroutine to split into two subproblems with clever merging.
 ///
 /// We use [`find_split`] to get indices for the left subproblem, and solve it recursively.
 /// If we get a solution, use the set of unsatisfied indices for the right subproblem,
@@ -259,7 +259,7 @@ where
 /// of traces to keeps in each split.
 ///  
 /// If the split was on the positives, the returned operation is [`LtlBinaryOp::Or`],
-/// and otherwise it's [`LtlBinaryOp::And`].
+/// and otherwise it is [`LtlBinaryOp::And`].
 fn find_split(target: &[bool]) -> Option<(LtlBinaryOp, Vec<usize>, Vec<usize>)> {
     let nb_traces = target.len();
     let nb_pos = target.iter().filter(|b| **b).count();

src/algos/mod.rs

@@ -1,18 +1,18 @@
-//! (Meta-)Algorithms for LTL and Boolean Synthesis.
+//! (Meta-)Algorithms for LTL and Boolean Set Cover
 //!
 //! Meta-algorithms first run an LTL enumeration algorithm for a fixed number of iterations,
-//! if no solution is found, they run a Boolean Synthesis on the set of LTL formulas to
+//! if no solution is found, they run a Boolean Set Cover on the set of LTL formulas to
 //! find a solution.
 //!
 //! This module contains the following meta-algorithms:
 //! - [Divide and conquer](self::meta)
 //!
-//! This module contains the following Boolean Synthesis algorithms:
+//! This module contains the following Boolean Set Cover algorithms:
 //! - [Set Cover](self::set_cover)
 //! - [Semantic Enumeration](self::enumeration)
 //! - [Beam Search](self::beam_search)
 //!
-//! Implementing a Boolean Synthesis for use with meta-algorithms is done via
+//! Implementing a Boolean Set Cover for use with meta-algorithms is done via
 //! the [`BoolAlgoParams`] trait.
 use std::rc::Rc;
 
@@ -36,7 +36,7 @@ pub mod enumeration;
 pub mod meta;
 pub mod set_cover;
 
-/// Abstraction for the hyperparameters of Boolean Synthesis algo, used to launch multiple runs.
+/// Abstraction for the hyperparameters of Boolean Set Cover algorithm, used to launch multiple runs.
 pub trait BoolAlgoParams {
     /// Additional info returned by a run, e.g. for collecting data for experiments.
     /// If unneeded, just use `()`.
@@ -92,7 +92,7 @@ pub(crate) fn create_initial_cache(
     target: &[bool],
 ) -> (Option<LtlFormula>, LtlCache) {
     let mut ltl_cache = LtlCache::new();
-    // Add empty line for size 0 in cache
+    // Add empty line for size 0 in cache.
     ltl_cache.new_line(0);
 
     let mut initial_line = ltl_cache.new_line(1);

src/algos/set_cover/mod.rs

@@ -1,4 +1,4 @@
-//! Set cover algorithm for Boolean Synthesis.
+//! Set cover algorithm for Boolean Set Cover.
 //!
 //! Produces Or-of-And or And-of-Or formulas in a greedy fashion.
 

src/bin/experiments.rs

@@ -80,8 +80,8 @@ fn get_name_time_sol<P: BoolAlgoParams + Clone>(
 struct CliArgs {
     /// Name of the .json file to read.
     input_filename: PathBuf,
-    /// Run LTL enumeration until `max_size_ltl`
-    /// before switching to boolean algorithm.
+    /// Run LTL enumeration until size `max_size_ltl`
+    /// before switching to boolean set cover algorithm.
     max_size_ltl: usize,
     /// Number of candidates to use for domination checking
     /// in the step that converts LTL formulas to boolean formulas.

src/bool/cache.rs

@@ -189,8 +189,8 @@ impl EnumFormulaCacheLine<BoolCharac> for BoolCacheLine<'_> {
     }
 }
 
-/// Stores a SatVec together with the hash of the corresponding Boolean formula.
-/// Used when removing dominated formulas in a single  to canonicalize the entries at the end of the push round.
+/// Stores a SatVec together with the hash of the corresponding boolean formula.
+/// Used when removing dominated formulas in a single pass to canonicalize the entries at the end of the push round.
 #[derive(Debug, PartialEq, Eq)]
 pub(crate) struct SvHash {
     sv: SatVec,