From 1cec3ef0e0f7aebfefb883ce6d48b177a1837634 Mon Sep 17 00:00:00 2001 From: Malte Tammena Date: Thu, 7 Dec 2023 15:54:49 +0100 Subject: [PATCH] chore: format, rename, simplify --- src/aba/mod.rs | 43 ++++++------------- src/aba/problems/admissibility.rs | 70 +++++++++++++++++-------------- src/aba/problems/conflict_free.rs | 49 ++++++++++------------ src/aba/problems/mod.rs | 2 + src/clauses.rs | 7 ++-- src/literal.rs | 24 ++++++++--- src/main.rs | 12 ++++-- src/tests/mod.rs | 28 +++++++------ 8 files changed, 120 insertions(+), 115 deletions(-) diff --git a/src/aba/mod.rs b/src/aba/mod.rs index e4c2bf0..152b8b4 100644 --- a/src/aba/mod.rs +++ b/src/aba/mod.rs @@ -2,7 +2,7 @@ use std::collections::{HashMap, HashSet}; use crate::{ clauses::{Atom, Clause, ClauseList}, - literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral, Literal}, + literal::{IntoLiteral, Literal, TheoryAtom}, }; pub mod problems; @@ -14,16 +14,10 @@ pub struct Aba { } #[derive(Debug)] -pub struct Inference(A); +pub struct Theory(A); #[derive(Debug)] -pub struct InferenceHelper(usize, A); - -#[derive(Debug)] -pub struct Inverse { - pub from: A, - pub to: A, -} +pub struct TheoryHelper(usize, A); impl Aba { #[cfg(test)] @@ -67,7 +61,6 @@ impl Aba { pub fn derive_clauses(&self) -> ClauseList { let mut clauses = ClauseList::new(); self.derive_rule_clauses().collect_into(&mut clauses); - self.derive_inverse_clauses().collect_into(&mut clauses); clauses } @@ -85,17 +78,7 @@ impl Aba { } fn derive_rule_clauses(&self) -> impl Iterator + '_ { - inference_helper::, _>(self) - } - - fn derive_inverse_clauses(&self) -> impl Iterator + '_ { - self.inverses.iter().map(|(from, to)| { - let inverse: Inverse = Inverse { - from: from.clone(), - to: to.clone(), - }; - Clause::from(vec![inverse.pos()]) - }) + inference_helper::, _>(self) } fn rule_heads(&self) -> impl Iterator + '_ { @@ -107,7 +90,7 @@ impl Aba { } } -fn body_to_clauses, A: Atom>(head: Literal, body: &HashSet) -> ClauseList { +fn body_to_clauses, A: Atom>(head: Literal, body: &HashSet) -> ClauseList { let mut clauses = vec![]; let mut left_implication: Clause = body.iter().map(|elem| I::new(elem.clone()).neg()).collect(); left_implication.push(head.clone().positive()); @@ -118,7 +101,7 @@ fn body_to_clauses, A: Atom>(head: Literal, body: &HashSet + IntoLiteral, A: Atom>( +pub fn inference_helper + IntoLiteral, A: Atom>( aba: &Aba, ) -> impl Iterator + '_ { let mut rules_combined = @@ -148,11 +131,11 @@ pub fn inference_helper + IntoLiteral, A: Atom>( .iter() .enumerate() .flat_map(|(idx, body)| { - body_to_clauses::(I::Helper::new(idx, head.clone()).pos(), body) + body_to_clauses::(I::new_helper(idx, head.clone()).pos(), body) }) .collect_into(&mut clauses); let helpers: Vec<_> = (0..bodies.len()) - .map(|idx| I::Helper::new(idx, head.clone()).pos()) + .map(|idx| I::new_helper(idx, head.clone()).pos()) .collect(); let mut right_implification: Clause = helpers.iter().cloned().collect(); right_implification.push(I::new(head.clone()).neg()); @@ -166,16 +149,14 @@ pub fn inference_helper + IntoLiteral, A: Atom>( }) } -impl InferenceAtom for Inference { - type Helper = InferenceHelper; +impl TheoryAtom for Theory { + type Helper = TheoryHelper; fn new(atom: A) -> Self { Self(atom) } -} -impl InferenceAtomHelper for InferenceHelper { - fn new(idx: usize, atom: A) -> Self { - Self(idx, atom) + fn new_helper(idx: usize, atom: A) -> Self::Helper { + TheoryHelper(idx, atom) } } diff --git a/src/aba/problems/admissibility.rs b/src/aba/problems/admissibility.rs index 92694a0..1e0df61 100644 --- a/src/aba/problems/admissibility.rs +++ b/src/aba/problems/admissibility.rs @@ -1,58 +1,68 @@ +//! Everything needed to solve problems around the admissibility semantics. use std::collections::HashSet; use crate::{ - aba::{inference_helper, Aba, Inference}, + aba::{inference_helper, Aba, Theory}, clauses::{Atom, Clause, ClauseList}, - literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral}, + literal::{IntoLiteral, TheoryAtom}, }; use super::{LoopControl, MultishotProblem, Problem, SolverState}; +/// Compute all admissible extensions for an [`Aba`] #[derive(Default, Debug)] -pub struct Admissibility { +pub struct EnumerateAdmissibleExtensions { found: Vec>, } -pub struct VerifyAdmissibility { +/// Sample an admissible extensions from an [`Aba`]. +/// Will only return the empty set if no other extension is found +#[derive(Debug, Default)] +pub struct SampleAdmissibleExtension; + +/// Verify wether `assumptions` is an admissible extension of an [`Aba`] +pub struct VerifyAdmissibleExtension { pub assumptions: Vec, } +/// *(Literal)* `A` is element of `th(S)` #[derive(Debug)] -pub struct SetInference(A); +pub struct SetTheory(A); +/// Helper for [`SetTheory`] #[derive(Debug)] -pub struct SetInferenceHelper(usize, A); +pub struct SetTheoryHelper(usize, A); fn initial_clauses(aba: &Aba) -> ClauseList { let mut clauses = vec![]; // Create inference for the problem set - inference_helper::, _>(aba).collect_into(&mut clauses); + inference_helper::, _>(aba).collect_into(&mut clauses); // Attack the inference of the aba, if an attack exists for (assumption, inverse) in &aba.inverses { [ // For any assumption `a` and it's inverse `b`: // Inference(a) <=> not SetInference(b) Clause::from(vec![ - Inference::new(assumption.clone()).pos(), - SetInference::new(inverse.clone()).pos(), + Theory::new(assumption.clone()).pos(), + SetTheory::new(inverse.clone()).pos(), ]), Clause::from(vec![ - Inference::new(assumption.clone()).neg(), - SetInference::new(inverse.clone()).neg(), + Theory::new(assumption.clone()).neg(), + SetTheory::new(inverse.clone()).neg(), ]), // Prevent attacks from the opponent to the selected set // For any assumption `a` and it's inverse `b`: // Inference(b) and SetInference(a) => bottom Clause::from(vec![ - Inference::new(inverse.clone()).neg(), - SetInference::new(assumption.clone()).neg(), + Theory::new(inverse.clone()).neg(), + SetTheory::new(assumption.clone()).neg(), ]), // Prevent self-attacks // For any assumption `a` and it's inverse `b`: // SetInference(a) and SetInference(b) => bottom Clause::from(vec![ - SetInference::new(assumption.clone()).neg(), - SetInference::new(inverse.clone()).neg(), + SetTheory::new(assumption.clone()).neg(), + SetTheory::new(inverse.clone()).neg(), ]), ] .into_iter() @@ -68,7 +78,7 @@ fn construct_found_set(state: SolverState<'_, A>) -> HashSet { .inverses .keys() .filter_map(|assumption| { - let literal = SetInference::new(assumption.clone()).pos(); + let literal = SetTheory::new(assumption.clone()).pos(); let raw = state.map.get_raw(&literal)?; match state.solver.value(raw) { Some(true) => Some(assumption.clone()), @@ -78,7 +88,7 @@ fn construct_found_set(state: SolverState<'_, A>) -> HashSet { .collect() } -impl Problem for Admissibility { +impl Problem for SampleAdmissibleExtension { type Output = HashSet; fn additional_clauses(&self, aba: &Aba) -> ClauseList { @@ -87,7 +97,7 @@ impl Problem for Admissibility { let no_empty_set: Clause = aba .inverses .keys() - .map(|assumption| SetInference::new(assumption.clone()).pos()) + .map(|assumption| SetTheory::new(assumption.clone()).pos()) .collect(); clauses.push(no_empty_set); clauses @@ -102,7 +112,7 @@ impl Problem for Admissibility { } } -impl MultishotProblem for Admissibility { +impl MultishotProblem for EnumerateAdmissibleExtensions { type Output = Vec>; fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList { @@ -113,7 +123,7 @@ impl MultishotProblem for Admissibility { let no_empty_set: Clause = aba .inverses .keys() - .map(|assumption| SetInference::new(assumption.clone()).pos()) + .map(|assumption| SetTheory::new(assumption.clone()).pos()) .collect(); clauses.push(no_empty_set); clauses @@ -128,9 +138,9 @@ impl MultishotProblem for Admissibility { .keys() .map(|assumption| { if just_found.contains(assumption) { - SetInference::new(assumption.clone()).neg() + SetTheory::new(assumption.clone()).neg() } else { - SetInference::new(assumption.clone()).pos() + SetTheory::new(assumption.clone()).pos() } }) .collect(); @@ -149,7 +159,7 @@ impl MultishotProblem for Admissibility { .inverses .keys() .filter_map(|assumption| { - let literal = SetInference::new(assumption.clone()).pos(); + let literal = SetTheory::new(assumption.clone()).pos(); let raw = state.map.get_raw(&literal)?; match state.solver.value(raw) { Some(true) => Some(assumption.clone()), @@ -172,14 +182,14 @@ impl MultishotProblem for Admissibility { } } -impl Problem for VerifyAdmissibility { +impl Problem for VerifyAdmissibleExtension { type Output = bool; fn additional_clauses(&self, aba: &Aba) -> crate::clauses::ClauseList { let mut clauses = initial_clauses(aba); // Force inference on all members of the set for assumption in aba.assumptions() { - let inf = SetInference::new(assumption.clone()); + let inf = SetTheory::new(assumption.clone()); if self.assumptions.contains(assumption) { clauses.push(Clause::from(vec![inf.pos()])) } else { @@ -199,16 +209,14 @@ impl Problem for VerifyAdmissibility { } } -impl InferenceAtom for SetInference { - type Helper = SetInferenceHelper; +impl TheoryAtom for SetTheory { + type Helper = SetTheoryHelper; fn new(atom: A) -> Self { Self(atom) } -} -impl InferenceAtomHelper for SetInferenceHelper { - fn new(idx: usize, atom: A) -> Self { - Self(idx, atom) + fn new_helper(idx: usize, atom: A) -> Self::Helper { + SetTheoryHelper(idx, atom) } } diff --git a/src/aba/problems/conflict_free.rs b/src/aba/problems/conflict_free.rs index c68d543..13a0d4d 100644 --- a/src/aba/problems/conflict_free.rs +++ b/src/aba/problems/conflict_free.rs @@ -1,52 +1,45 @@ +use std::collections::HashSet; + use crate::{ - aba::{Aba, Inference, Inverse}, - clauses::{Clause, ClauseList}, - literal::{InferenceAtom, IntoLiteral}, + aba::{Aba, Theory}, + clauses::{Atom, Clause, ClauseList}, + literal::{IntoLiteral, TheoryAtom}, }; use super::{Problem, SolverState}; -pub struct ConflictFreeness { - pub assumptions: Vec, +pub struct ConflictFreeness { + pub assumptions: HashSet, } -impl Problem for ConflictFreeness { +impl Problem for ConflictFreeness { type Output = bool; - fn additional_clauses(&self, aba: &Aba) -> ClauseList { + fn additional_clauses(&self, aba: &Aba) -> ClauseList { let mut clauses = vec![]; // Make sure that every assumption in our problem is inferred and every other not - for elem in self.assumptions.iter().copied() { - if aba.inverses.contains_key(&elem) { - clauses.push(vec![Inference::new(elem).pos()].into()) + for assumption in aba.assumptions() { + let theory = Theory::new(assumption.clone()); + if self.assumptions.contains(assumption) { + clauses.push(vec![theory.pos()].into()) } else { - clauses.push(vec![Inference::new(elem).neg()].into()) + clauses.push(vec![theory.neg()].into()) } } - // TODO: Minimize this loop - for elem in aba.universe().copied() { - for assumption in aba.assumptions().copied() { - // For every element e in our universe and every assumption a, we cannot have the following: - // e is the inverse of a and both are inferred (conflict!) - clauses.push(Clause::from(vec![ - Inference::new(assumption).neg(), - Inference::new(elem).neg(), - Inverse { - from: assumption, - to: elem, - } - .neg(), - ])) - } + for (assumption, inverse) in &aba.inverses { + clauses.push(Clause::from(vec![ + Theory::new(assumption.clone()).neg(), + Theory::new(inverse.clone()).neg(), + ])); } clauses } - fn construct_output(self, state: SolverState<'_, char>) -> Self::Output { + fn construct_output(self, state: SolverState<'_, A>) -> Self::Output { state.sat_result } - fn check(&self, aba: &Aba) -> bool { + fn check(&self, aba: &Aba) -> bool { // Make sure that every assumption is part of the ABA self.assumptions.iter().all(|a| aba.contains_assumption(a)) } diff --git a/src/aba/problems/mod.rs b/src/aba/problems/mod.rs index 180d4e6..4429c60 100644 --- a/src/aba/problems/mod.rs +++ b/src/aba/problems/mod.rs @@ -24,6 +24,7 @@ pub struct SolverState<'a, A: Atom + 'a> { map: &'a Mapper, } +#[doc(notable_trait)] pub trait Problem { type Output; fn additional_clauses(&self, aba: &Aba) -> ClauseList; @@ -34,6 +35,7 @@ pub trait Problem { } } +#[doc(notable_trait)] pub trait MultishotProblem { type Output; fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList; diff --git a/src/clauses.rs b/src/clauses.rs index 0586330..a7fec36 100644 --- a/src/clauses.rs +++ b/src/clauses.rs @@ -10,12 +10,13 @@ pub type ClauseList = Vec; pub type RawClause = Vec; pub type RawLiteral = i32; +/// Generic Atom that can be used to construct [`Clause`]s. +#[doc(notable_trait)] pub trait Atom: Debug + Display + Hash + Eq + Clone + 'static {} -impl Atom for String {} -impl Atom for char {} -impl Atom for u32 {} +impl Atom for A {} +/// A disjunction of [`Literal`]s. pub struct Clause { list: Vec, } diff --git a/src/literal.rs b/src/literal.rs index 5aa4a1e..c7ee945 100644 --- a/src/literal.rs +++ b/src/literal.rs @@ -5,38 +5,50 @@ use std::{ use crate::clauses::Atom; +/// A Literal can be used in SAT [`Clause`](crate::clauses::Clause)s #[derive(Clone)] pub enum Literal { Pos(RawLiteral), Neg(RawLiteral), } +/// New type to prevent creation of arbitrary SAT literals #[derive(Clone, Debug)] pub struct RawLiteral(String); +/// Convert the type into it's literal +#[doc(notable_trait)] pub trait IntoLiteral: Sized { + /// Actual transformation fn into_literal(self) -> RawLiteral; + /// Create a positive literal from this value fn pos(self) -> Literal { Literal::Pos(IntoLiteral::into_literal(self)) } + /// Create a negative literal from this value fn neg(self) -> Literal { Literal::Neg(IntoLiteral::into_literal(self)) } } +/// Implement [`IntoLiteral`] for all types that are 'static, sized and debuggable impl IntoLiteral for T { fn into_literal(self) -> RawLiteral { RawLiteral(format!("{:?}#{:?}", TypeId::of::(), self)) } } -pub trait InferenceAtom: Sized + IntoLiteral { - type Helper: InferenceAtomHelper; +/// ([`Literal`]) A literal that can be used to construct the logic behind +/// the theory of a (sub-)set of assumptions (`th(S)`) in an [`Aba`](crate::aba::Aba). +/// +/// See [`crate::aba::inference_helper`]. +pub trait TheoryAtom: Sized + IntoLiteral { + /// Helper type + type Helper: IntoLiteral; + /// Construct this [`Literal`] fn new(atom: A) -> Self; -} - -pub trait InferenceAtomHelper: Sized + IntoLiteral { - fn new(idx: usize, atom: A) -> Self; + /// Construct the helper [`Literal`] + fn new_helper(idx: usize, atom: A) -> Self::Helper; } impl Literal { diff --git a/src/main.rs b/src/main.rs index 9b33580..3ce691c 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,9 +1,12 @@ #![feature(iter_collect_into)] #![feature(iter_intersperse)] +#![feature(doc_notable_trait)] use std::{collections::HashSet, fmt::Write, fs::read_to_string}; -use aba::problems::admissibility::{Admissibility, VerifyAdmissibility}; +use aba::problems::admissibility::{ + EnumerateAdmissibleExtensions, SampleAdmissibleExtension, VerifyAdmissibleExtension, +}; use clap::Parser; use crate::error::{Error, Result}; @@ -40,7 +43,7 @@ fn __main() -> Result { match args.problem { args::Problems::VerifyAdmissibility { set } => { let result = aba::problems::solve( - VerifyAdmissibility { + VerifyAdmissibleExtension { assumptions: set.into_iter().collect(), }, &aba, @@ -48,11 +51,12 @@ fn __main() -> Result { print_bool_result(result); } args::Problems::EnumerateAdmissibility => { - let result = aba::problems::multishot_solve(Admissibility::default(), &aba)?; + let result = + aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)?; print_witnesses_result(result)?; } args::Problems::SampleAdmissibility => { - let result = aba::problems::solve(Admissibility::default(), &aba)?; + let result = aba::problems::solve(SampleAdmissibleExtension, &aba)?; print_witness_result(result)?; } } diff --git a/src/tests/mod.rs b/src/tests/mod.rs index 66f5001..1418738 100644 --- a/src/tests/mod.rs +++ b/src/tests/mod.rs @@ -2,7 +2,7 @@ use std::collections::HashSet; use crate::aba::{ problems::{ - admissibility::{Admissibility, VerifyAdmissibility}, + admissibility::{EnumerateAdmissibleExtensions, VerifyAdmissibleExtension}, conflict_free::ConflictFreeness, }, Aba, @@ -22,14 +22,14 @@ fn simple_aba_example_1() -> Aba { fn simple_conflict_free_verification() { let aba = simple_aba_example_1(); let set_checks = vec![ - (vec![], true), - (vec!['a'], true), - (vec!['b'], true), - (vec!['c'], true), - (vec!['a', 'b'], true), - (vec!['a', 'c'], true), - (vec!['b', 'c'], true), - (vec!['a', 'b', 'c'], false), + (set![], true), + (set!['a'], true), + (set!['b'], true), + (set!['c'], true), + (set!['a', 'b'], true), + (set!['a', 'c'], true), + (set!['b', 'c'], true), + (set!['a', 'b', 'c'], false), ]; set_checks @@ -56,7 +56,7 @@ fn simple_admissible_verification() { .for_each(|(assumptions, expectation)| { eprintln!("Checking set {assumptions:?}"); let result = - crate::aba::problems::solve(VerifyAdmissibility { assumptions: assumptions.clone() }, &aba).unwrap(); + crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: assumptions.clone() }, &aba).unwrap(); assert!( result == expectation, "Expected {expectation} from solver, but got {result} while checking {assumptions:?}" @@ -68,7 +68,9 @@ fn simple_admissible_verification() { fn simple_admissible_example() { let aba = simple_aba_example_1(); let expected: Vec> = vec![set!(), set!('b'), set!('b', 'c'), set!('c')]; - let result = crate::aba::problems::multishot_solve(Admissibility::default(), &aba).unwrap(); + let result = + crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba) + .unwrap(); for elem in &expected { assert!( result.contains(elem), @@ -87,7 +89,9 @@ fn simple_admissible_example() { fn simple_admissible_example_with_defense() { let aba = simple_aba_example_1().with_rule('t', vec!['a', 'b']); let expected: Vec> = vec![set!(), set!('a', 'b'), set!('b'), set!('b', 'c')]; - let result = crate::aba::problems::multishot_solve(Admissibility::default(), &aba).unwrap(); + let result = + crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba) + .unwrap(); for elem in &expected { assert!( result.contains(elem),