Make code public

Author: GBathie

.gitignore

@@ -11,11 +11,4 @@ Cargo.lock
 **/*.rs.bk
 
 # MSVC Windows builds of rustc generate these, which store debugging information
-*.pdb
-
-# RustRover
-#  JetBrains specific template is maintained in a separate JetBrains.gitignore that can
-#  be found at https://github.com/github/gitignore/blob/main/Global/JetBrains.gitignore
-#  and can be added to the global gitignore or merged into this file.  For a more nuclear
-#  option (not recommended) you can uncomment the following to ignore the entire idea folder.
-#.idea/
+*.pdb

Cargo.toml

@@ -0,0 +1,19 @@
+[package]
+name = "ltl-rs"
+version = "0.1.0"
+edition = "2021"
+default-run= "ltl-rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+clap = { version = "4.5.1", features = ["derive"] }
+env_logger = "0.11.2"
+fxhash = "0.2.1"
+itertools = "0.13.0"
+log = "0.4.20"
+ordered-float = "4.2.1"
+thiserror = "1.0.64"
+
+[dev-dependencies]
+rand = "0.8.5"

src/algos/beam_search/cache.rs

@@ -0,0 +1,190 @@
+use std::{
+    cmp::Ordering,
+    collections::{hash_map::Entry, BinaryHeap},
+};
+
+use fxhash::FxHashMap;
+use itertools::Itertools;
+
+use crate::{
+    cache::{EnumFormulaCache, EnumFormulaCacheLine, FormulaCache},
+    traits::Hashed,
+};
+
+use crate::bool::{charac::BoolCharac, BoolFormula};
+
+/// Keeps a hashmap for observational equivalence,
+/// and only the `max_line_size` formulas with highest density of each size.
+/// Computes domination over the line size.
+#[derive(Debug)]
+pub struct BeamSearchCache {
+    entries: FxHashMap<<BoolCharac as Hashed>::HashType, BoolFormula>,
+    lines: Vec<BinaryHeap<PcoBoolFormula>>,
+    max_line_size: usize,
+}
+
+impl BeamSearchCache {
+    pub(crate) fn new(max_line_size: usize) -> Self {
+        Self {
+            entries: Default::default(),
+            lines: vec![],
+            max_line_size,
+        }
+    }
+}
+
+impl FormulaCache<BoolCharac> for BeamSearchCache {
+    fn len(&self) -> usize {
+        self.lines.iter().map(|l| l.len()).sum()
+    }
+
+    fn get(&self, hash: &<BoolCharac as Hashed>::HashType) -> Option<&BoolFormula> {
+        self.entries.get(hash)
+    }
+}
+
+impl EnumFormulaCache<BoolCharac> for BeamSearchCache {
+    type CacheLine<'a> = BeamSearchBoolCacheLine<'a>;
+
+    fn iter_size<'a>(&'a self, size: usize) -> impl Iterator<Item = &'a BoolFormula>
+    where
+        BoolCharac: 'a,
+    {
+        self.lines[size].iter().map(|pf| &pf.f)
+    }
+
+    fn new_line_and_iter_size<'a>(
+        &'a mut self,
+        size: usize,
+    ) -> (
+        impl Iterator<Item = &'a BoolFormula>,
+        impl Iterator<Item = (&'a BoolFormula, &'a BoolFormula)>,
+        Self::CacheLine<'a>,
+    )
+    where
+        BoolCharac: 'a,
+    {
+        self.lines.push(BinaryHeap::new());
+        let (old_lines, new) = self.lines.split_at_mut(size);
+
+        let new_line = BeamSearchBoolCacheLine {
+            line: &mut new[0],
+            hashes: &mut self.entries,
+            max_line_size: self.max_line_size,
+        };
+
+        let iter_size = size - 1;
+        let iter_formulas = old_lines[iter_size].iter().map(|pf| &pf.f);
+
+        let iter_pairs_size = (size + 1) / 2;
+        let iter_pairs = old_lines
+            .iter()
+            .zip(old_lines.iter().rev())
+            .take(iter_pairs_size)
+            .flat_map(|(i1, i2)| i1.iter().cartesian_product(i2))
+            .map(|(pf1, pf2)| (&pf1.f, &pf2.f));
+        (iter_formulas, iter_pairs, new_line)
+    }
+
+    fn new_line<'a>(&'a mut self, size: usize) -> Self::CacheLine<'a>
+    where
+        BoolCharac: 'a,
+    {
+        self.lines.push(BinaryHeap::new());
+
+        BeamSearchBoolCacheLine {
+            line: &mut self.lines[size],
+            hashes: &mut self.entries,
+            max_line_size: self.max_line_size,
+        }
+    }
+
+    fn nb_lines(&self) -> usize {
+        self.lines.len()
+    }
+}
+
+impl IntoIterator for BeamSearchCache {
+    type Item = BoolFormula;
+
+    type IntoIter = Box<dyn Iterator<Item = BoolFormula>>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        Box::new(self.lines.into_iter().flatten().map(|pf| pf.f))
+    }
+}
+
+pub(crate) struct BeamSearchBoolCacheLine<'a> {
+    line: &'a mut BinaryHeap<PcoBoolFormula>,
+    hashes: &'a mut FxHashMap<<BoolCharac as Hashed>::HashType, BoolFormula>,
+    max_line_size: usize,
+}
+
+impl<'a> BeamSearchBoolCacheLine<'a> {
+    fn dominates(&self, f: &BoolFormula) -> Option<<BoolCharac as Hashed>::HashType> {
+        self.line.iter().find_map(|sv| {
+            if sv.dominates(f) {
+                Some(sv.f.hashed())
+            } else {
+                None
+            }
+        })
+    }
+}
+
+impl<'a> EnumFormulaCacheLine<BoolCharac> for BeamSearchBoolCacheLine<'a> {
+    fn push(&mut self, f: BoolFormula) -> bool {
+        if self.dominates(&f).is_some() {
+            return false;
+        }
+
+        let hash = f.hashed();
+        let removed = match self.hashes.entry(hash) {
+            Entry::Occupied(_) => return false,
+            Entry::Vacant(e) => {
+                e.insert(f.clone());
+                self.line.push(PcoBoolFormula { f });
+                if self.line.len() > self.max_line_size {
+                    self.line.pop()
+                } else {
+                    return true;
+                }
+            }
+        };
+
+        self.hashes.remove(&removed.unwrap().f.hashed());
+
+        true
+    }
+}
+
+// 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.
+#[derive(Debug, PartialEq, Eq)]
+struct PcoBoolFormula {
+    pub(crate) f: BoolFormula,
+}
+
+impl PartialOrd for PcoBoolFormula {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+/// Order by max popcount.
+impl Ord for PcoBoolFormula {
+    fn cmp(&self, other: &Self) -> Ordering {
+        other
+            .f
+            .charac
+            .sv
+            .popcount()
+            .cmp(&self.f.charac.sv.popcount())
+    }
+}
+
+impl PcoBoolFormula {
+    pub(crate) fn dominates(&self, f: &BoolFormula) -> bool {
+        self.f.charac.sv.dominates(f.charac.sv)
+    }
+}

src/algos/beam_search/mod.rs

@@ -0,0 +1,75 @@
+//! Beam Search algorithm for Boolean Synthesis.
+//!
+//! Bottom-up enumeration with fixed width.
+//! Implemented using a fixed-width cache ([`BeamSearchCache`])
+//! and the enumeration algorithm.
+use cache::BeamSearchCache;
+use clap::Args;
+
+use crate::{
+    algos::enumeration::aux::enum_aux,
+    bool::{charac::BoolCharac, cv::CharVec, BoolFormula},
+    cache::{EnumFormulaCache, EnumFormulaCacheLine},
+    formula::{rebuild_formula, tree::FormulaTree},
+    ltl::trace::Operators,
+};
+
+pub mod cache;
+
+use super::{meta::cache::InitialBoolCache, BoolAlgoParams};
+
+#[derive(Args, Clone, Copy)]
+pub struct BeamSearchParams {
+    /// Number of formulas to keep at each level.
+    beam_width: usize,
+    /// Maximum enumeration size
+    max_size_bool: usize,
+}
+
+impl BoolAlgoParams for BeamSearchParams {
+    type Data = ();
+
+    fn run(
+        &self,
+        cache: InitialBoolCache,
+        operators: Operators,
+        target: &[bool],
+    ) -> (Option<FormulaTree>, Self::Data) {
+        let bool_target = target.iter().copied().collect();
+        let bool_operators = operators.filter_bool();
+        let mut cache = convert_cache_beam_search(cache, self.beam_width, bool_target);
+        let f = enum_aux(
+            &mut cache,
+            &bool_operators,
+            &bool_target,
+            self.max_size_bool,
+        );
+
+        let f_str = f.map(|f| rebuild_formula(&f, &cache));
+        (f_str, ())
+    }
+
+    fn name() -> &'static str {
+        "beam_search"
+    }
+}
+
+fn convert_cache_beam_search(
+    cache: InitialBoolCache,
+    max_line_size: usize,
+    target: CharVec,
+) -> BeamSearchCache {
+    let mut bs_cache = BeamSearchCache::new(max_line_size);
+
+    for (size, cache) in cache.iter_lines().into_iter().enumerate() {
+        let mut new_line = bs_cache.new_line(size);
+
+        for (cv, t, size) in cache {
+            let cv = cv.into_iter().collect();
+            let f = BoolFormula::new_base(BoolCharac::from_cv(cv, target), size, t);
+            new_line.push(f);
+        }
+    }
+
+    bs_cache
+}