Merge branch 'master' into feature/choice-filtering

Cargo.toml

@@ -25,6 +25,7 @@ regex.workspace = true
 rayon.workspace = true
 argfile.workspace = true
 wild.workspace = true
+anyhow.workspace = true
 
 [dev-dependencies]
 glob.workspace = true

queentest.txt

@@ -0,0 +1,54 @@
+"Generated by n-queens-gen version 0.10.4 queens=7 "
+
+"every diagonal must contain at most one queen (direction 1)"
+[v_0,v_8,v_16,v_24,v_32,v_40,v_48,] <= 1 &
+[v_1,v_9,v_17,v_25,v_33,v_41,] <= 1 &
+[v_2,v_10,v_18,v_26,v_34,] <= 1 &
+[v_3,v_11,v_19,v_27,] <= 1 &
+[v_4,v_12,v_20,] <= 1 &
+[v_5,v_13,] <= 1 &
+[v_6,] <= 1 &
+
+[v_7,v_15,v_23,v_31,v_39,v_47,] <= 1 &
+[v_14,v_22,v_30,v_38,v_46,] <= 1 &
+[v_21,v_29,v_37,v_45,] <= 1 &
+[v_28,v_36,v_44,] <= 1 &
+[v_35,v_43,] <= 1 &
+[v_42,] <= 1 &
+
+"every diagonal must contain at most one queen (direction 2)"
+[v_0,] <= 1 &
+[v_1,v_7,] <= 1 &
+[v_2,v_8,v_14,] <= 1 &
+[v_3,v_9,v_15,v_21,] <= 1 &
+[v_4,v_10,v_16,v_22,v_28,] <= 1 &
+[v_5,v_11,v_17,v_23,v_29,v_35,] <= 1 &
+[v_6,v_12,v_18,v_24,v_30,v_36,v_42,] <= 1 &
+
+[v_48,] <= 1 &
+[v_47,v_41,] <= 1 &
+[v_46,v_40,v_34,] <= 1 &
+[v_45,v_39,v_33,v_27,] <= 1 &
+[v_44,v_38,v_32,v_26,v_20,] <= 1 &
+[v_43,v_37,v_31,v_25,v_19,v_13,] <= 1 &
+
+"every row must contain exactly one queen"
+[v_0,v_1,v_2,v_3,v_4,v_5,v_6,] = 1 &
+[v_7,v_8,v_9,v_10,v_11,v_12,v_13,] = 1 &
+[v_14,v_15,v_16,v_17,v_18,v_19,v_20,] = 1 &
+[v_21,v_22,v_23,v_24,v_25,v_26,v_27,] = 1 &
+[v_28,v_29,v_30,v_31,v_32,v_33,v_34,] = 1 &
+[v_35,v_36,v_37,v_38,v_39,v_40,v_41,] = 1 &
+[v_42,v_43,v_44,v_45,v_46,v_47,v_48,] = 1 &
+
+"every column must contain exactly one queen"
+[v_0,v_7,v_14,v_21,v_28,v_35,v_42,] = 1 &
+[v_1,v_8,v_15,v_22,v_29,v_36,v_43,] = 1 &
+[v_2,v_9,v_16,v_23,v_30,v_37,v_44,] = 1 &
+[v_3,v_10,v_17,v_24,v_31,v_38,v_45,] = 1 &
+[v_4,v_11,v_18,v_25,v_32,v_39,v_46,] = 1 &
+[v_5,v_12,v_19,v_26,v_33,v_40,v_47,] = 1 &
+[v_6,v_13,v_20,v_27,v_34,v_41,v_48,] = 1 &
+
+"end"
+true

src/bdd.rs

@@ -1,12 +1,12 @@
 use itertools::Itertools;
 use rustc_hash::{FxHashMap, FxHasher};
 use std::cell::RefCell;
-use std::error::Error;
-use std::fmt;
-use std::fmt::{Debug, Display};
+
+use std::fmt::Debug;
 use std::hash::{Hash, Hasher};
 use std::rc::Rc;
-use std::str::FromStr;
+
+use crate::{BDDSymbol, NamedSymbol, TruthTableEntry};
 
 #[macro_export]
 macro_rules! bdd {
@@ -19,54 +19,6 @@ macro_rules! bdd {
     }};
 }
 
-pub trait BDDSymbol: Ord + Display + Debug + Clone + Hash {}
-
-impl<T> BDDSymbol for T where T: Ord + Display + Debug + Clone + Hash {}
-
-#[derive(Debug, Clone)]
-pub struct NamedSymbol {
-    pub name: Rc<String>,
-    pub id: usize,
-}
-
-impl fmt::Display for NamedSymbol {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        fmt::Display::fmt(&self.name, f)
-    }
-}
-
-impl Hash for NamedSymbol {
-    fn hash<H: Hasher>(&self, state: &mut H) {
-        self.id.hash(state);
-    }
-}
-
-impl PartialEq for NamedSymbol {
-    fn eq(&self, other: &Self) -> bool {
-        self.id == other.id
-    }
-}
-
-impl Eq for NamedSymbol {}
-
-impl Ord for NamedSymbol {
-    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
-        self.id.cmp(&other.id)
-    }
-}
-
-impl PartialOrd for NamedSymbol {
-    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        Some(self.cmp(other))
-    }
-}
-
-impl From<NamedSymbol> for usize {
-    fn from(ns: NamedSymbol) -> Self {
-        ns.id
-    }
-}
-
 #[derive(Debug, Clone, Default, Eq, PartialEq, Hash)]
 pub enum BDD<Symbol: BDDSymbol> {
     #[default]
@@ -128,79 +80,6 @@ impl From<BDD<NamedSymbol>> for BDD<usize> {
     }
 }
 
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-/// Single variable assignment in a truth table.
-///
-/// The variable assignments in a truth table can be one of True, False or Any.
-/// [`True`] is assigned when the variable can only be assigned a 'true' value;
-/// [`False`] is assigned when the variable can only be 'false'.
-/// When the variable can either be true or false, the truth table can either consist of
-/// both options (as separate models), or assign [`Any`].
-///
-/// [`Any`]: TruthTableEntry::Any
-/// [`True`]: TruthTableEntry::True
-/// [`False`]: TruthTableEntry::False
-pub enum TruthTableEntry {
-    /// Assigned when the variable can only be true
-    True,
-    /// Assigned when the variable can only be false
-    False,
-    /// Assigned when the variable can either be true or false
-    Any,
-}
-
-impl TruthTableEntry {
-    pub fn is_true(self) -> bool {
-        self == TruthTableEntry::True
-    }
-
-    pub fn is_false(self) -> bool {
-        self == TruthTableEntry::False
-    }
-
-    pub fn is_any(self) -> bool {
-        self == TruthTableEntry::Any
-    }
-}
-
-#[derive(Debug)]
-pub struct TruthTableEntryParseError {
-    pub input: String,
-}
-
-impl Error for TruthTableEntryParseError {}
-
-impl Display for TruthTableEntryParseError {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "Could not parse truth table entry: {}", self.input)
-    }
-}
-
-impl FromStr for TruthTableEntry {
-    type Err = TruthTableEntryParseError;
-
-    fn from_str(s: &str) -> Result<Self, Self::Err> {
-        match s {
-            "true" | "True" | "t" | "T" | "1" => Ok(TruthTableEntry::True),
-            "false" | "False" | "f" | "F" | "0" => Ok(TruthTableEntry::False),
-            "any" | "Any" | "a" | "A" => Ok(TruthTableEntry::Any),
-            _ => Err(TruthTableEntryParseError {
-                input: s.to_string(),
-            }),
-        }
-    }
-}
-
-impl Display for TruthTableEntry {
-    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        f.pad(match self {
-            TruthTableEntry::True => "True",
-            TruthTableEntry::False => "False",
-            TruthTableEntry::Any => "Any",
-        })
-    }
-}
-
 impl<S: BDDSymbol> BDD<S> {
     pub fn get_hash(&self) -> u64 {
         let mut s = FxHasher::default();

src/bdd_io.rs

@@ -1,6 +1,6 @@
 extern crate dot;
 
-use crate::bdd::*;
+use crate::{bdd::*, BDDSymbol, TruthTableEntry};
 use itertools::Itertools;
 use std::borrow::Cow;
 use std::io;

src/bin/rsbdd.rs

@@ -4,6 +4,9 @@ use rsbdd::bdd_io::*;
 use rsbdd::parser::*;
 use rsbdd::parser_io::*;
 use rsbdd::plot::*;
+use rsbdd::BDDSymbol;
+use rsbdd::NamedSymbol;
+use rsbdd::TruthTableEntry;
 use std::cmp::max;
 use std::fmt::Display;
 use std::fs::File;

src/lib.rs

@@ -6,3 +6,9 @@ pub mod parser;
 pub mod parser_io;
 pub mod plot;
 pub mod set;
+
+mod truth_table;
+pub use truth_table::TruthTableEntry;
+
+mod symbols;
+pub use symbols::*;

src/parser.rs

@@ -1,4 +1,5 @@
-use crate::bdd::{BDDEnv, NamedSymbol, BDD};
+use crate::bdd::{BDDEnv, BDD};
+use crate::NamedSymbol;
 use itertools::Itertools;
 use lazy_static::lazy_static;
 use regex::Regex;

src/symbols.rs

@@ -0,0 +1,53 @@
+use std::{
+    fmt::{self, Debug, Display},
+    hash::{Hash, Hasher},
+    rc::Rc,
+};
+
+pub trait BDDSymbol: Ord + Display + Debug + Clone + Hash {}
+
+impl<T> BDDSymbol for T where T: Ord + Display + Debug + Clone + Hash {}
+
+#[derive(Debug, Clone)]
+pub struct NamedSymbol {
+    pub name: Rc<String>,
+    pub id: usize,
+}
+
+impl fmt::Display for NamedSymbol {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        fmt::Display::fmt(&self.name, f)
+    }
+}
+
+impl Hash for NamedSymbol {
+    fn hash<H: Hasher>(&self, state: &mut H) {
+        self.id.hash(state);
+    }
+}
+
+impl PartialEq for NamedSymbol {
+    fn eq(&self, other: &Self) -> bool {
+        self.id == other.id
+    }
+}
+
+impl Eq for NamedSymbol {}
+
+impl Ord for NamedSymbol {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.id.cmp(&other.id)
+    }
+}
+
+impl PartialOrd for NamedSymbol {
+    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
+impl From<NamedSymbol> for usize {
+    fn from(ns: NamedSymbol) -> Self {
+        ns.id
+    }
+}

src/truth_table.rs

@@ -0,0 +1,73 @@
+use std::{
+    fmt::{self, Display},
+    str::FromStr,
+};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+/// Single variable assignment in a truth table.
+///
+/// The variable assignments in a truth table can be one of True, False or Any.
+/// [`True`] is assigned when the variable can only be assigned a 'true' value;
+/// [`False`] is assigned when the variable can only be 'false'.
+/// When the variable can either be true or false, the truth table can either consist of
+/// both options (as separate models), or assign [`Any`].
+///
+/// [`Any`]: TruthTableEntry::Any
+/// [`True`]: TruthTableEntry::True
+/// [`False`]: TruthTableEntry::False
+pub enum TruthTableEntry {
+    /// Assigned when the variable can only be true
+    True,
+    /// Assigned when the variable can only be false
+    False,
+    /// Assigned when the variable can either be true or false
+    Any,
+}
+
+impl TruthTableEntry {
+    fn variants<'a>() -> &'a [Self] {
+        &[Self::True, Self::False, Self::Any]
+    }
+
+    fn matches(&self, s: &str) -> bool {
+        match self {
+            TruthTableEntry::True => matches!(s, "true" | "True" | "t" | "T" | "1"),
+            TruthTableEntry::False => matches!(s, "false" | "False" | "f" | "F" | "0"),
+            TruthTableEntry::Any => matches!(s, "any" | "Any" | "a" | "A" | "*"),
+        }
+    }
+
+    pub fn is_true(self) -> bool {
+        self == TruthTableEntry::True
+    }
+
+    pub fn is_false(self) -> bool {
+        self == TruthTableEntry::False
+    }
+
+    pub fn is_any(self) -> bool {
+        self == TruthTableEntry::Any
+    }
+}
+
+impl Display for TruthTableEntry {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        f.pad(match self {
+            TruthTableEntry::True => "True",
+            TruthTableEntry::False => "False",
+            TruthTableEntry::Any => "Any",
+        })
+    }
+}
+
+impl FromStr for TruthTableEntry {
+    type Err = anyhow::Error;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        Self::variants()
+            .iter()
+            .find(|variant| variant.matches(s))
+            .ok_or(anyhow::anyhow!("cannot parse {s} as truth-table entry"))
+            .copied()
+    }
+}

tests/bdd_test.rs

@@ -1,5 +1,5 @@
-use rsbdd::bdd;
 use rsbdd::bdd::*;
+use rsbdd::{bdd, TruthTableEntry};
 use std::rc::Rc;
 
 use rsbdd::bdd_io::*;