From 328cd79636c6074bf5cb71a8369a3ba9b11aac62 Mon Sep 17 00:00:00 2001 From: Malte Tammena Date: Thu, 7 Dec 2023 15:13:15 +0100 Subject: [PATCH] fix admissibility, unify with verification --- src/aba/problems/admissibility.rs | 182 +++++++++++++++-------- src/aba/problems/conflict_free.rs | 8 +- src/aba/problems/mod.rs | 50 ++++--- src/aba/problems/verify_admissibility.rs | 74 --------- src/args.rs | 4 + src/main.rs | 34 +++-- src/tests/mod.rs | 66 ++++---- 7 files changed, 213 insertions(+), 205 deletions(-) delete mode 100644 src/aba/problems/verify_admissibility.rs diff --git a/src/aba/problems/admissibility.rs b/src/aba/problems/admissibility.rs index 76e174f..92694a0 100644 --- a/src/aba/problems/admissibility.rs +++ b/src/aba/problems/admissibility.rs @@ -4,31 +4,111 @@ use crate::{ aba::{inference_helper, Aba, Inference}, clauses::{Atom, Clause, ClauseList}, literal::{InferenceAtom, InferenceAtomHelper, IntoLiteral}, - mapper::Mapper, }; -use super::{LoopControl, MultishotProblem}; +use super::{LoopControl, MultishotProblem, Problem, SolverState}; #[derive(Default, Debug)] pub struct Admissibility { found: Vec>, } +pub struct VerifyAdmissibility { + pub assumptions: Vec, +} + #[derive(Debug)] pub struct SetInference(A); #[derive(Debug)] pub struct SetInferenceHelper(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); + // 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(), + ]), + Clause::from(vec![ + Inference::new(assumption.clone()).neg(), + SetInference::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(), + ]), + // 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(), + ]), + ] + .into_iter() + .collect_into(&mut clauses); + } + + clauses +} + +fn construct_found_set(state: SolverState<'_, A>) -> HashSet { + state + .aba + .inverses + .keys() + .filter_map(|assumption| { + let literal = SetInference::new(assumption.clone()).pos(); + let raw = state.map.get_raw(&literal)?; + match state.solver.value(raw) { + Some(true) => Some(assumption.clone()), + _ => None, + } + }) + .collect() +} + +impl Problem for Admissibility { + type Output = HashSet; + + fn additional_clauses(&self, aba: &Aba) -> ClauseList { + let mut clauses = initial_clauses(aba); + // Prevent the empty set + let no_empty_set: Clause = aba + .inverses + .keys() + .map(|assumption| SetInference::new(assumption.clone()).pos()) + .collect(); + clauses.push(no_empty_set); + clauses + } + + fn construct_output(self, state: SolverState<'_, A>) -> Self::Output { + if state.sat_result { + construct_found_set(state) + } else { + HashSet::new() + } + } +} + impl MultishotProblem for Admissibility { type Output = Vec>; fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList { match iteration { 0 => { - let mut clauses = vec![]; - // Create inference for the problem set - inference_helper::, _>(aba).collect_into(&mut clauses); + let mut clauses = initial_clauses(aba); // Prevent the empty set let no_empty_set: Clause = aba .inverses @@ -36,50 +116,6 @@ impl MultishotProblem for Admissibility { .map(|assumption| SetInference::new(assumption.clone()).pos()) .collect(); clauses.push(no_empty_set); - // 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) and not SetInference(a) - Clause::from(vec![ - Inference::new(assumption.clone()).neg(), - SetInference::new(inverse.clone()).neg(), - ]), - Clause::from(vec![ - Inference::new(assumption.clone()).neg(), - SetInference::new(assumption.clone()).neg(), - ]), - Clause::from(vec![ - SetInference::new(inverse.clone()).pos(), - SetInference::new(assumption.clone()).pos(), - Inference::new(assumption.clone()).pos(), - ]), - // 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(), - ]), - // 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(), - ]), - // Prevent attacks from the set to the opponent - // For any assumption `a` and it's inverse `b`: - // Inference(a) and SetInference(b) => bottom - Clause::from(vec![ - Inference::new(assumption.clone()).neg(), - SetInference::new(inverse.clone()).neg(), - ]), - ] - .into_iter() - .collect_into(&mut clauses); - } - clauses } idx => { @@ -103,24 +139,19 @@ impl MultishotProblem for Admissibility { } } - fn feedback( - &mut self, - aba: &Aba, - sat_result: bool, - solver: &cadical::Solver, - map: &Mapper, - ) -> LoopControl { - if !sat_result { + fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl { + if !state.sat_result { return LoopControl::Stop; } // TODO: Somehow query the mapper about things instead of this - let found = aba + let found = state + .aba .inverses .keys() .filter_map(|assumption| { let literal = SetInference::new(assumption.clone()).pos(); - let raw = map.get_raw(&literal)?; - match solver.value(raw) { + let raw = state.map.get_raw(&literal)?; + match state.solver.value(raw) { Some(true) => Some(assumption.clone()), _ => None, } @@ -132,9 +163,7 @@ impl MultishotProblem for Admissibility { fn construct_output( mut self, - _aba: &Aba, - _sat_result: bool, - _solver: &cadical::Solver, + _state: SolverState<'_, A>, _total_iterations: usize, ) -> Self::Output { // Re-Add the empty set @@ -143,6 +172,33 @@ impl MultishotProblem for Admissibility { } } +impl Problem for VerifyAdmissibility { + 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()); + if self.assumptions.contains(assumption) { + clauses.push(Clause::from(vec![inf.pos()])) + } else { + clauses.push(Clause::from(vec![inf.neg()])) + } + } + clauses + } + + fn construct_output(self, state: SolverState<'_, A>) -> Self::Output { + state.sat_result + } + + 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)) + } +} + impl InferenceAtom for SetInference { type Helper = SetInferenceHelper; diff --git a/src/aba/problems/conflict_free.rs b/src/aba/problems/conflict_free.rs index 3f013e3..c68d543 100644 --- a/src/aba/problems/conflict_free.rs +++ b/src/aba/problems/conflict_free.rs @@ -1,12 +1,10 @@ -use cadical::Solver; - use crate::{ aba::{Aba, Inference, Inverse}, clauses::{Clause, ClauseList}, literal::{InferenceAtom, IntoLiteral}, }; -use super::Problem; +use super::{Problem, SolverState}; pub struct ConflictFreeness { pub assumptions: Vec, @@ -44,8 +42,8 @@ impl Problem for ConflictFreeness { clauses } - fn construct_output(self, sat_result: bool, _: &Aba, _: &Solver) -> Self::Output { - sat_result + fn construct_output(self, state: SolverState<'_, char>) -> Self::Output { + state.sat_result } fn check(&self, aba: &Aba) -> bool { diff --git a/src/aba/problems/mod.rs b/src/aba/problems/mod.rs index 93fbf3d..180d4e6 100644 --- a/src/aba/problems/mod.rs +++ b/src/aba/problems/mod.rs @@ -10,7 +10,6 @@ use super::Aba; pub mod admissibility; pub mod conflict_free; -pub mod verify_admissibility; #[derive(Debug, PartialEq, Eq, Clone, Copy)] pub enum LoopControl { @@ -18,10 +17,17 @@ pub enum LoopControl { Stop, } +pub struct SolverState<'a, A: Atom + 'a> { + aba: &'a Aba, + sat_result: bool, + solver: &'a Solver, + map: &'a Mapper, +} + pub trait Problem { type Output; fn additional_clauses(&self, aba: &Aba) -> ClauseList; - fn construct_output(self, sat_result: bool, aba: &Aba, solver: &Solver) -> Self::Output; + fn construct_output(self, state: SolverState<'_, A>) -> Self::Output; fn check(&self, _aba: &Aba) -> bool { true @@ -31,20 +37,8 @@ pub trait Problem { pub trait MultishotProblem { type Output; fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList; - fn feedback( - &mut self, - aba: &Aba, - sat_result: bool, - solver: &Solver, - map: &Mapper, - ) -> LoopControl; - fn construct_output( - self, - aba: &Aba, - sat_result: bool, - solver: &Solver, - total_iterations: usize, - ) -> Self::Output; + fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl; + fn construct_output(self, state: SolverState<'_, A>, total_iterations: usize) -> Self::Output; fn check(&self, _aba: &Aba) -> bool { true @@ -62,7 +56,12 @@ pub fn solve>(problem: P, aba: &Aba) -> Result>( let rec = map.reconstruct(&sat).collect::>(); eprintln!("{rec:#?}"); } - let control = problem.feedback(aba, sat_result, &sat, &map); + let control = problem.feedback(SolverState { + aba, + sat_result, + solver: &sat, + map: &map, + }); if control == LoopControl::Stop { break sat_result; } iteration += 1; }; - Ok(problem.construct_output(aba, final_result, &sat, iteration)) + Ok(problem.construct_output( + SolverState { + aba, + sat_result: final_result, + solver: &sat, + map: &map, + }, + iteration, + )) } diff --git a/src/aba/problems/verify_admissibility.rs b/src/aba/problems/verify_admissibility.rs deleted file mode 100644 index 9090acd..0000000 --- a/src/aba/problems/verify_admissibility.rs +++ /dev/null @@ -1,74 +0,0 @@ -use crate::{ - aba::{inference_helper, Aba, Inference, Inverse}, - clauses::{Atom, Clause}, - literal::{InferenceAtom, IntoLiteral}, -}; - -use super::{admissibility::SetInference, Problem}; - -pub struct VerifyAdmissibility { - pub assumptions: Vec, -} - -impl Problem for VerifyAdmissibility { - type Output = bool; - - fn additional_clauses(&self, aba: &Aba) -> crate::clauses::ClauseList { - let mut clauses = vec![]; - // Create inference for the problem set - inference_helper::, _>(aba).collect_into(&mut clauses); - // Force inference on all members of the set - aba.inverses - .keys() - .cloned() - .map(|assumption| { - if self.assumptions.contains(&assumption) { - Clause::from(vec![SetInference::new(assumption).pos()]) - } else { - Clause::from(vec![SetInference::new(assumption).neg()]) - } - }) - .collect_into(&mut clauses); - // Attack the inference of the aba, if an attack exists - for elem in aba.universe() { - for assumption in self.assumptions.iter() { - clauses.push(Clause::from(vec![ - SetInference::new(assumption.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 { - from: assumption.clone(), - to: elem.clone(), - } - .neg(), - SetInference::new(elem.clone()).neg(), - ])) - } - } - - clauses - } - - fn construct_output( - self, - sat_result: bool, - _: &crate::aba::Aba, - _: &cadical::Solver, - ) -> Self::Output { - sat_result - } - - 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/args.rs b/src/args.rs index 4e699bc..5f66972 100644 --- a/src/args.rs +++ b/src/args.rs @@ -21,6 +21,7 @@ pub struct Args { pub file: PathBuf, } +#[allow(clippy::enum_variant_names)] #[derive(Debug, Subcommand)] pub enum Problems { #[clap(visible_alias = "ve-ad")] @@ -30,4 +31,7 @@ pub enum Problems { }, #[clap(visible_alias = "ee-ad")] EnumerateAdmissibility, + /// Will only return the empty extension if no other is found + #[clap(visible_alias = "se-ad")] + SampleAdmissibility, } diff --git a/src/main.rs b/src/main.rs index edd4ad9..9b33580 100644 --- a/src/main.rs +++ b/src/main.rs @@ -3,7 +3,7 @@ use std::{collections::HashSet, fmt::Write, fs::read_to_string}; -use aba::problems::{admissibility::Admissibility, verify_admissibility::VerifyAdmissibility}; +use aba::problems::admissibility::{Admissibility, VerifyAdmissibility}; use clap::Parser; use crate::error::{Error, Result}; @@ -35,10 +35,10 @@ mod tests; fn __main() -> Result { let args = args::Args::parse(); + let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?; + let aba = parser::aba_file(&content)?; match args.problem { args::Problems::VerifyAdmissibility { set } => { - let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?; - let aba = parser::aba_file(&content)?; let result = aba::problems::solve( VerifyAdmissibility { assumptions: set.into_iter().collect(), @@ -48,11 +48,13 @@ fn __main() -> Result { print_bool_result(result); } args::Problems::EnumerateAdmissibility => { - let content = read_to_string(&args.file).map_err(Error::OpeningAbaFile)?; - let aba = parser::aba_file(&content)?; let result = aba::problems::multishot_solve(Admissibility::default(), &aba)?; print_witnesses_result(result)?; } + args::Problems::SampleAdmissibility => { + let result = aba::problems::solve(Admissibility::default(), &aba)?; + print_witness_result(result)?; + } } Ok(()) } @@ -69,14 +71,16 @@ fn print_bool_result(result: bool) { } fn print_witnesses_result(result: Vec>) -> Result { - result.into_iter().try_for_each(|set| { - let set = set - .into_iter() - .try_fold(String::new(), |mut list, num| -> Result<_, Error> { - write!(list, " {num}")?; - Result::Ok(list) - })?; - println!("w{set}"); - Ok(()) - }) + result.into_iter().try_for_each(print_witness_result) +} + +fn print_witness_result(result: HashSet) -> Result { + let set = result + .into_iter() + .try_fold(String::new(), |mut list, num| -> Result<_, Error> { + write!(list, " {num}")?; + Result::Ok(list) + })?; + println!("w{set}"); + Ok(()) } diff --git a/src/tests/mod.rs b/src/tests/mod.rs index aad9997..66f5001 100644 --- a/src/tests/mod.rs +++ b/src/tests/mod.rs @@ -2,21 +2,25 @@ use std::collections::HashSet; use crate::aba::{ problems::{ - admissibility::Admissibility, conflict_free::ConflictFreeness, - verify_admissibility::VerifyAdmissibility, + admissibility::{Admissibility, VerifyAdmissibility}, + conflict_free::ConflictFreeness, }, Aba, }; -#[test] -fn simple_conflict_free_verification() { - let aba = Aba::new() +fn simple_aba_example_1() -> Aba { + Aba::new() .with_assumption('a', 'r') .with_assumption('b', 's') .with_assumption('c', 't') .with_rule('p', ['q', 'a']) .with_rule('q', []) - .with_rule('r', ['b', 'c']); + .with_rule('r', ['b', 'c']) +} + +#[test] +fn simple_conflict_free_verification() { + let aba = simple_aba_example_1(); let set_checks = vec![ (vec![], true), (vec!['a'], true), @@ -40,12 +44,7 @@ fn simple_conflict_free_verification() { #[test] fn simple_admissible_verification() { - let aba = Aba::new() - .with_assumption('a', 'c') - .with_assumption('b', 'd') - .with_rule('c', vec!['a']) - .with_rule('c', vec!['b']) - .with_rule('d', vec!['a']); + let aba = simple_aba_example_1(); let set_checks = vec![ (vec![], true), (vec!['a', 'b'], false), @@ -66,25 +65,34 @@ fn simple_admissible_verification() { } #[test] -fn simple_admissible_thing() { - let aba = Aba::new() - .with_assumption('a', 'r') - .with_assumption('b', 's') - .with_assumption('c', 't') - .with_rule('p', vec!['q', 'a']) - .with_rule('q', vec![]) - .with_rule('r', vec!['b', 'c']); - let expected: Vec> = vec![ - set!(), - set!('a', 'b'), - set!('a', 'c'), - set!('b'), - set!('b', 'c'), - set!('c'), - ]; +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(); for elem in &expected { - assert!(result.contains(elem)); + assert!( + result.contains(elem), + "{elem:?} was expected but not found in result" + ); + } + for elem in &result { + assert!( + expected.contains(elem), + "{elem:?} was found in the result, but is not expected!" + ); + } +} + +#[test] +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(); + for elem in &expected { + assert!( + result.contains(elem), + "{elem:?} was expected but not found in result" + ); } for elem in &result { assert!(