diff --git a/src/aba/problems/admissibility.rs b/src/aba/problems/admissibility.rs index c642d17..29726d5 100644 --- a/src/aba/problems/admissibility.rs +++ b/src/aba/problems/admissibility.rs @@ -31,8 +31,8 @@ impl MultishotProblem for Admissibility { .collect(); clauses.push(no_empty_set); // Attack the inference of the aba, if an attack exists - for elem in aba.universe() { - for assumption in aba.inverses.keys() { + for assumption in aba.inverses.keys() { + for elem in aba.universe() { clauses.push(Clause::from(vec![ SetInference::new(assumption.clone()).neg(), Inverse::new(assumption.clone(), elem.clone()).neg(), @@ -42,8 +42,22 @@ impl MultishotProblem for Admissibility { SetInference::new(assumption.clone()).neg(), Inverse::new(assumption.clone(), elem.clone()).neg(), Inference::new(elem.clone()).neg(), - ])) + ])); + clauses.push(Clause::from(vec![ + Inference::new(assumption.clone()).neg(), + Inverse::new(assumption.clone(), elem.clone()).neg(), + SetInference::new(elem.clone()).neg(), + ])); } + // If an assumption is in the set, it must not be in the attack + clauses.push(Clause::from(vec![ + Inference::new(assumption.clone()).neg(), + SetInference::new(assumption.clone()).neg(), + ])); + // clauses.push(Clause::from(vec![ + // Inference::new(assumption.clone()).pos(), + // SetInference::new(assumption.clone()).pos(), + // ])) } clauses diff --git a/src/main.rs b/src/main.rs index 539bfdc..44bc310 100644 --- a/src/main.rs +++ b/src/main.rs @@ -9,6 +9,20 @@ use clap::Parser; use crate::error::{Error, Result}; +#[cfg(test)] +macro_rules! set { + ($($elem:expr),*) => {{ + vec![$($elem),*].into_iter().collect() + }} +} + +#[cfg(test)] +macro_rules! map { + ($($from:expr => $to:expr),*) => {{ + vec![$(($from, $to)),*].into_iter().collect() + }} +} + pub mod aba; pub mod args; pub mod clauses; diff --git a/src/parser.rs b/src/parser.rs index f1bf679..c538dc6 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -143,18 +143,6 @@ mod tests { use crate::aba::Aba; - macro_rules! set { - ($($elem:expr),*) => {{ - vec![$($elem),*].into_iter().collect() - }} - } - - macro_rules! map { - ($($from:expr => $to:expr),*) => {{ - vec![$(($from, $to)),*].into_iter().collect() - }} - } - fn assert_parse(parser: F, input: &str, expected: T) where F: FnMut(&str) -> nom::IResult<&str, T>,