various fixes and reworks

flake.lock

@@ -8,11 +8,11 @@
         "rust-analyzer-src": "rust-analyzer-src"
       },
       "locked": {
-        "lastModified": 1699078825,
+        "lastModified": 1701757414,
-        "narHash": "sha256-Np1XuKxZG1J4AdMm6m9PogFTWHnvKvmyoILvAXUahFM=",
+        "narHash": "sha256-63epDkdiHYkiOLg061HsMK5Of4s4M4sUAWteZrkWynE=",
         "owner": "nix-community",
         "repo": "fenix",
-        "rev": "ec493cf412f94155daac4b95c95eb11ddcb347e5",
+        "rev": "3d2215d896636efe29b71c8b9b2857d3d093f9c9",
         "type": "github"
       },
       "original": {
@@ -210,11 +210,11 @@
     "rust-analyzer-src": {
       "flake": false,
       "locked": {
-        "lastModified": 1698994377,
+        "lastModified": 1701721820,
-        "narHash": "sha256-PY6A0JiJmv5ef0uf10ediOznKbqCKlqgT3Vtu+Z5fRQ=",
+        "narHash": "sha256-fKcg/YWrCc2ZT4hUvx2bPd+xCTAnQYcd0oDI1cpN07U=",
         "owner": "rust-lang",
         "repo": "rust-analyzer",
-        "rev": "0fec61aabf62faab0c9f9b33b40ea5d5977792c8",
+        "rev": "2d66f6df252896cfbd7bd24be6ee0c124369b1b7",
         "type": "github"
       },
       "original": {

src/aba/mod.rs

@@ -2,7 +2,7 @@ use std::collections::{HashMap, HashSet};
 
 use crate::{
     clauses::{Atom, Clause, ClauseList},
-    literal::{Inference, InferenceAtom, InferenceAtomHelper, IntoLiteral, Inverse, Literal},
+    literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral, Literal},
 };
 
 pub mod problems;
@@ -13,7 +13,20 @@ pub struct Aba<A: Atom> {
     pub inverses: HashMap<A, A>,
 }
 
+#[derive(Debug)]
+pub struct Inference<A: Atom>(A);
+
+#[derive(Debug)]
+pub struct InferenceHelper<A: Atom>(usize, A);
+
+#[derive(Debug)]
+pub struct Inverse<A: Atom> {
+    pub from: A,
+    pub to: A,
+}
+
 impl<A: Atom> Aba<A> {
+    #[cfg(test)]
     pub fn new() -> Self {
         Aba {
             rules: vec![],
@@ -152,3 +165,17 @@ pub fn inference_helper<I: InferenceAtom<A> + IntoLiteral, A: Atom>(
             }
         })
 }
+
+impl<A: Atom> InferenceAtom<A> for Inference<A> {
+    type Helper = InferenceHelper<A>;
+
+    fn new(atom: A) -> Self {
+        Self(atom)
+    }
+}
+
+impl<A: Atom> InferenceAtomHelper<A> for InferenceHelper<A> {
+    fn new(idx: usize, atom: A) -> Self {
+        Self(idx, atom)
+    }
+}

src/aba/problems/admissibility.rs

@@ -1,9 +1,9 @@
 use std::collections::HashSet;
 
 use crate::{
-    aba::{inference_helper, Aba},
+    aba::{inference_helper, Aba, Inference},
     clauses::{Atom, Clause, ClauseList},
-    literal::{Inference, IntoLiteral, SetInference},
+    literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral},
     mapper::Mapper,
 };
 
@@ -14,6 +14,12 @@ pub struct Admissibility<A: Atom> {
     found: Vec<HashSet<A>>,
 }
 
+#[derive(Debug)]
+pub struct SetInference<A: Atom>(A);
+
+#[derive(Debug)]
+pub struct SetInferenceHelper<A: Atom>(usize, A);
+
 impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
     type Output = Vec<HashSet<A>>;
 
@@ -136,3 +142,17 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
         self.found
     }
 }
+
+impl<A: Atom> InferenceAtom<A> for SetInference<A> {
+    type Helper = SetInferenceHelper<A>;
+
+    fn new(atom: A) -> Self {
+        Self(atom)
+    }
+}
+
+impl<A: Atom> InferenceAtomHelper<A> for SetInferenceHelper<A> {
+    fn new(idx: usize, atom: A) -> Self {
+        Self(idx, atom)
+    }
+}

src/aba/problems/conflict_free.rs

@@ -1,9 +1,9 @@
 use cadical::Solver;
 
 use crate::{
-    aba::Aba,
+    aba::{Aba, Inference, Inverse},
     clauses::{Clause, ClauseList},
-    literal::{Inference, IntoLiteral, Inverse},
+    literal::{InferenceAtom, IntoLiteral},
 };
 
 use super::Problem;
@@ -33,7 +33,11 @@ impl Problem<char> for ConflictFreeness {
                 clauses.push(Clause::from(vec![
                     Inference::new(assumption).neg(),
                     Inference::new(elem).neg(),
-                    Inverse::new(assumption, elem).neg(),
+                    Inverse {
+                        from: assumption,
+                        to: elem,
+                    }
+                    .neg(),
                 ]))
             }
         }

src/aba/problems/mod.rs

@@ -8,13 +8,9 @@ use crate::{
 
 use super::Aba;
 
-mod admissibility;
+pub mod admissibility;
-mod conflict_free;
+pub mod conflict_free;
-mod verify_admissibility;
+pub mod verify_admissibility;
-
-pub use admissibility::Admissibility;
-pub use conflict_free::ConflictFreeness;
-pub use verify_admissibility::VerifyAdmissibility;
 
 #[derive(Debug, PartialEq, Eq, Clone, Copy)]
 pub enum LoopControl {
@@ -93,6 +89,11 @@ pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
         map.as_raw_iter(&additional_clauses)
             .for_each(|raw| sat.add_clause(raw));
         let sat_result = sat.solve().ok_or(Error::SatCallInterrupted)?;
+        #[cfg(debug_assertions)]
+        if sat_result {
+            let rec = map.reconstruct(&sat).collect::<Vec<_>>();
+            eprintln!("{rec:#?}");
+        }
         let control = problem.feedback(aba, sat_result, &sat, &map);
         if control == LoopControl::Stop {
             break sat_result;

src/aba/problems/verify_admissibility.rs

@@ -1,10 +1,10 @@
 use crate::{
-    aba::{inference_helper, Aba},
+    aba::{inference_helper, Aba, Inference, Inverse},
     clauses::{Atom, Clause},
-    literal::{Inference, IntoLiteral, Inverse, SetInference},
+    literal::{InferenceAtom, IntoLiteral},
 };
 
-use super::Problem;
+use super::{admissibility::SetInference, Problem};
 
 pub struct VerifyAdmissibility<A: Atom> {
     pub assumptions: Vec<A>,
@@ -34,14 +34,22 @@ impl<A: Atom> Problem<A> for VerifyAdmissibility<A> {
             for assumption in self.assumptions.iter() {
                 clauses.push(Clause::from(vec![
                     SetInference::new(assumption.clone()).neg(),
-                    Inverse::new(assumption.clone(), elem.clone()).neg(),
+                    Inverse {
+                        from: assumption.clone(),
+                        to: elem.clone(),
+                    }
+                    .neg(),
                     Inference::new(elem.clone()).neg(),
                 ]))
             }
             for assumption in aba.assumptions() {
                 clauses.push(Clause::from(vec![
                     SetInference::new(assumption.clone()).neg(),
-                    Inverse::new(assumption.clone(), elem.clone()).neg(),
+                    Inverse {
+                        from: assumption.clone(),
+                        to: elem.clone(),
+                    }
+                    .neg(),
                     SetInference::new(elem.clone()).neg(),
                 ]))
             }

src/clauses.rs

@@ -10,7 +10,7 @@ pub type ClauseList = Vec<Clause>;
 pub type RawClause = Vec<RawLiteral>;
 pub type RawLiteral = i32;
 
-pub trait Atom: Debug + Display + Hash + Eq + Clone {}
+pub trait Atom: Debug + Display + Hash + Eq + Clone + 'static {}
 
 impl Atom for String {}
 impl Atom for char {}
@@ -20,15 +20,6 @@ pub struct Clause {
     list: Vec<Literal>,
 }
 
-impl std::fmt::Debug for Literal {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self {
-            Literal::Pos(str) => write!(f, "+{str}"),
-            Literal::Neg(str) => write!(f, "-{str}"),
-        }
-    }
-}
-
 impl std::fmt::Debug for Clause {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         write!(f, "{{")?;
@@ -41,16 +32,6 @@ impl std::fmt::Debug for Clause {
     }
 }
 
-impl std::ops::Deref for Literal {
-    type Target = String;
-
-    fn deref(&self) -> &Self::Target {
-        match self {
-            Literal::Pos(inner) | Literal::Neg(inner) => inner,
-        }
-    }
-}
-
 impl Deref for Clause {
     type Target = Vec<Literal>;
 

src/literal.rs

@@ -1,19 +1,21 @@
+use std::{
+    any::{Any, TypeId},
+    fmt::Debug,
+};
+
 use crate::clauses::Atom;
 
-mod private {
-    pub trait Private {}
-}
-
-use self::private::Private;
-
 #[derive(Clone)]
 pub enum Literal {
-    Pos(String),
+    Pos(RawLiteral),
-    Neg(String),
+    Neg(RawLiteral),
 }
 
-pub trait IntoLiteral: Sized + private::Private {
+#[derive(Clone, Debug)]
-    fn into_literal(self) -> String;
+pub struct RawLiteral(String);
+
+pub trait IntoLiteral: Sized {
+    fn into_literal(self) -> RawLiteral;
     fn pos(self) -> Literal {
         Literal::Pos(IntoLiteral::into_literal(self))
     }
@@ -22,12 +24,18 @@ pub trait IntoLiteral: Sized + private::Private {
     }
 }
 
-pub trait InferenceAtom<A: Atom>: Sized + private::Private + IntoLiteral {
+impl<T: Any + Debug + Sized> IntoLiteral for T {
+    fn into_literal(self) -> RawLiteral {
+        RawLiteral(format!("{:?}#{:?}", TypeId::of::<T>(), self))
+    }
+}
+
+pub trait InferenceAtom<A: Atom>: Sized + IntoLiteral {
     type Helper: InferenceAtomHelper<A>;
     fn new(atom: A) -> Self;
 }
 
-pub trait InferenceAtomHelper<A: Atom>: Sized + private::Private + IntoLiteral {
+pub trait InferenceAtomHelper<A: Atom>: Sized + IntoLiteral {
     fn new(idx: usize, atom: A) -> Self;
 }
 
@@ -40,195 +48,42 @@ impl Literal {
         Self::Pos(self.into_inner())
     }
 
-    pub fn into_inner(self) -> String {
+    pub fn into_inner(self) -> RawLiteral {
         match self {
             Literal::Pos(inner) | Literal::Neg(inner) => inner,
         }
     }
 }
 
-pub struct Inference<A: Atom> {
+impl std::ops::Deref for Literal {
-    pub elem: A,
+    type Target = String;
-}
 
-impl<A: Atom> Inference<A> {
+    fn deref(&self) -> &Self::Target {
-    pub fn new(elem: A) -> Self {
+        match self {
-        Self { elem }
+            Literal::Pos(inner) | Literal::Neg(inner) => inner,
+        }
     }
 }
 
-pub struct InferenceHelper<A: Atom> {
+impl std::fmt::Debug for Literal {
-    pub idx: usize,
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-    pub head: A,
+        match self {
-}
+            Literal::Pos(str) => write!(f, "+{str}"),
-
+            Literal::Neg(str) => write!(f, "-{str}"),
-impl<A: Atom> InferenceHelper<A> {
+        }
-    pub fn new(idx: usize, head: A) -> Self {
-        Self { idx, head }
     }
 }
 
-// TODO: Let the problems define these things
+impl std::ops::Deref for RawLiteral {
-pub struct SetInference<A: Atom> {
+    type Target = String;
-    pub elem: A,
-}
 
-impl<A: Atom> SetInference<A> {
+    fn deref(&self) -> &Self::Target {
-    pub fn new(elem: A) -> Self {
+        &self.0
-        Self { elem }
     }
 }
 
-pub struct SetInferenceHelper<A: Atom> {
+impl std::fmt::Display for RawLiteral {
-    pub idx: usize,
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-    pub head: A,
+        std::fmt::Display::fmt(&self.0, f)
-}
-
-impl<A: Atom> SetInferenceHelper<A> {
-    pub fn new(idx: usize, head: A) -> Self {
-        Self { idx, head }
-    }
-}
-
-// TODO: Let the problems define these things
-pub struct OpponentInference<A: Atom> {
-    pub elem: A,
-}
-
-impl<A: Atom> OpponentInference<A> {
-    pub fn new(elem: A) -> Self {
-        Self { elem }
-    }
-}
-
-pub struct OpponentInferenceHelper<A: Atom> {
-    pub idx: usize,
-    pub head: A,
-}
-
-impl<A: Atom> OpponentInferenceHelper<A> {
-    pub fn new(idx: usize, head: A) -> Self {
-        Self { idx, head }
-    }
-}
-
-pub struct Inverse<A: Atom> {
-    pub from: A,
-    pub to: A,
-}
-
-impl<A: Atom> Inverse<A> {
-    pub fn new(from: A, to: A) -> Self {
-        Self { from, to }
-    }
-}
-
-pub struct SetAttack<A: Atom> {
-    pub against: A,
-}
-
-impl<A: Atom> SetAttack<A> {
-    pub fn new(against: A) -> Self {
-        Self { against }
-    }
-}
-
-impl<A: Atom> Private for Inference<A> {}
-impl<A: Atom> IntoLiteral for Inference<A> {
-    fn into_literal(self) -> String {
-        let Self { elem } = self;
-        format!("inference_{elem}")
-    }
-}
-impl<A: Atom> InferenceAtom<A> for Inference<A> {
-    type Helper = InferenceHelper<A>;
-
-    fn new(atom: A) -> Self {
-        Self::new(atom)
-    }
-}
-
-impl<A: Atom> Private for InferenceHelper<A> {}
-impl<A: Atom> IntoLiteral for InferenceHelper<A> {
-    fn into_literal(self) -> String {
-        let Self { idx, head } = self;
-        format!("inference_helper_{idx}_{head}")
-    }
-}
-impl<A: Atom> InferenceAtomHelper<A> for InferenceHelper<A> {
-    fn new(idx: usize, atom: A) -> Self {
-        Self::new(idx, atom)
-    }
-}
-
-impl<A: Atom> Private for SetInference<A> {}
-impl<A: Atom> IntoLiteral for SetInference<A> {
-    fn into_literal(self) -> String {
-        let Self { elem } = self;
-        format!("set_inference_{elem}")
-    }
-}
-impl<A: Atom> InferenceAtom<A> for SetInference<A> {
-    type Helper = SetInferenceHelper<A>;
-
-    fn new(atom: A) -> Self {
-        Self::new(atom)
-    }
-}
-
-impl<A: Atom> Private for SetInferenceHelper<A> {}
-impl<A: Atom> IntoLiteral for SetInferenceHelper<A> {
-    fn into_literal(self) -> String {
-        let Self { idx, head } = self;
-        format!("set_inference_helper_{idx}_{head}")
-    }
-}
-impl<A: Atom> InferenceAtomHelper<A> for SetInferenceHelper<A> {
-    fn new(idx: usize, atom: A) -> Self {
-        Self::new(idx, atom)
-    }
-}
-
-impl<A: Atom> Private for OpponentInference<A> {}
-impl<A: Atom> IntoLiteral for OpponentInference<A> {
-    fn into_literal(self) -> String {
-        let Self { elem } = self;
-        format!("set_inference_{elem}")
-    }
-}
-impl<A: Atom> InferenceAtom<A> for OpponentInference<A> {
-    type Helper = OpponentInferenceHelper<A>;
-
-    fn new(atom: A) -> Self {
-        Self::new(atom)
-    }
-}
-
-impl<A: Atom> Private for OpponentInferenceHelper<A> {}
-impl<A: Atom> IntoLiteral for OpponentInferenceHelper<A> {
-    fn into_literal(self) -> String {
-        let Self { idx, head } = self;
-        format!("set_inference_helper_{idx}_{head}")
-    }
-}
-impl<A: Atom> InferenceAtomHelper<A> for OpponentInferenceHelper<A> {
-    fn new(idx: usize, atom: A) -> Self {
-        Self::new(idx, atom)
-    }
-}
-
-impl<A: Atom> Private for Inverse<A> {}
-impl<A: Atom> IntoLiteral for Inverse<A> {
-    fn into_literal(self) -> String {
-        let Self { from, to } = self;
-        format!("inv_{from}_{to}")
-    }
-}
-
-impl<A: Atom> Private for SetAttack<A> {}
-impl<A: Atom> IntoLiteral for SetAttack<A> {
-    fn into_literal(self) -> String {
-        let Self { against } = self;
-        format!("set_attack_{against}")
     }
 }

src/main.rs

@@ -1,16 +1,12 @@
 #![feature(iter_collect_into)]
 #![feature(iter_intersperse)]
-#![feature(result_option_inspect)]
 
 use std::{collections::HashSet, fmt::Write, fs::read_to_string};
 
-use aba::problems::VerifyAdmissibility;
+use aba::problems::{admissibility::Admissibility, verify_admissibility::VerifyAdmissibility};
 use clap::Parser;
 
-use crate::{
+use crate::error::{Error, Result};
-    aba::problems::Admissibility,
-    error::{Error, Result},
-};
 
 #[cfg(test)]
 macro_rules! set {
@@ -26,13 +22,13 @@ macro_rules! map {
     }}
 }
 
-pub mod aba;
+mod aba;
-pub mod args;
+mod args;
-pub mod clauses;
+mod clauses;
-pub mod error;
+mod error;
-pub mod literal;
+mod literal;
-pub mod mapper;
+mod mapper;
-pub mod parser;
+mod parser;
 #[cfg(test)]
 mod tests;
 

src/mapper.rs

@@ -12,6 +12,11 @@ pub struct Mapper {
     map: HashMap<String, u32>,
 }
 
+pub enum ReconstructedLiteral {
+    Pos(String),
+    Neg(String),
+}
+
 impl Mapper {
     pub fn new() -> Self {
         Mapper {
@@ -41,11 +46,15 @@ impl Mapper {
         }
     }
 
-    pub fn reconstruct<'s>(&'s self, sat: &'s Solver) -> impl Iterator<Item = Literal> + 's {
+    pub fn reconstruct<'s>(
+        &'s self,
+        sat: &'s Solver,
+    ) -> impl Iterator<Item = ReconstructedLiteral> + 's {
         self.map.iter().flat_map(|(lit, raw)| {
+            let (_, lit) = lit.split_once('#').expect("All literals must contain a #");
             sat.value(*raw as i32).map(|result| match result {
-                true => Literal::Pos(lit.clone()),
+                true => ReconstructedLiteral::Pos(lit.to_owned()),
-                false => Literal::Neg(lit.clone()),
+                false => ReconstructedLiteral::Neg(lit.to_owned()),
             })
         })
     }
@@ -54,3 +63,12 @@ impl Mapper {
         self.map.get(lit.as_str()).map(|&raw| raw as i32)
     }
 }
+
+impl std::fmt::Debug for ReconstructedLiteral {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            ReconstructedLiteral::Pos(str) => write!(f, "+{str}"),
+            ReconstructedLiteral::Neg(str) => write!(f, "-{str}"),
+        }
+    }
+}

src/tests/mod.rs

@@ -1,7 +1,10 @@
 use std::collections::HashSet;
 
 use crate::aba::{
-    problems::{Admissibility, ConflictFreeness, VerifyAdmissibility},
+    problems::{
+        admissibility::Admissibility, conflict_free::ConflictFreeness,
+        verify_admissibility::VerifyAdmissibility,
+    },
     Aba,
 };