megamanmalte/aba2sat
0
0
Fork 0
Code Issues Pull requests Packages Projects Releases Wiki Activity

chore: format, rename, simplify

Browse source
This commit is contained in:
Malte Tammena 2023-12-07 15:54:49 +01:00
parent 328cd79636
commit 1cec3ef0e0
8 changed files with 120 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/aba/mod.rs
View file

@ -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<A: Atom> {
}
#[derive(Debug)]
pub struct Inference<A: Atom>(A);
pub struct Theory<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,
}
pub struct TheoryHelper<A: Atom>(usize, A);
impl<A: Atom> Aba<A> {
#[cfg(test)]
@ -67,7 +61,6 @@ impl<A: Atom> Aba<A> {
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<A: Atom> Aba<A> {
}
fn derive_rule_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
inference_helper::<Inference<_>, _>(self)
}
fn derive_inverse_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
self.inverses.iter().map(|(from, to)| {
let inverse: Inverse<A> = Inverse {
from: from.clone(),
to: to.clone(),
};
Clause::from(vec![inverse.pos()])
})
inference_helper::<Theory<_>, _>(self)
}
fn rule_heads(&self) -> impl Iterator<Item = &A> + '_ {
@ -107,7 +90,7 @@ impl<A: Atom> Aba<A> {
}
}
fn body_to_clauses<I: InferenceAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>) -> ClauseList {
fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>) -> 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<I: InferenceAtom<A>, A: Atom>(head: Literal, body: &HashSet<A
clauses
}
pub fn inference_helper<I: InferenceAtom<A> + IntoLiteral, A: Atom>(
pub fn inference_helper<I: TheoryAtom<A> + IntoLiteral, A: Atom>(
aba: &Aba<A>,
) -> impl Iterator<Item = Clause> + '_ {
let mut rules_combined =
@ -148,11 +131,11 @@ pub fn inference_helper<I: InferenceAtom<A> + IntoLiteral, A: Atom>(
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<I, _>(I::Helper::new(idx, head.clone()).pos(), body)
body_to_clauses::<I, _>(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<I: InferenceAtom<A> + IntoLiteral, A: Atom>(
})
}
impl<A: Atom> InferenceAtom<A> for Inference<A> {
type Helper = InferenceHelper<A>;
impl<A: Atom> TheoryAtom<A> for Theory<A> {
type Helper = TheoryHelper<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)
fn new_helper(idx: usize, atom: A) -> Self::Helper {
TheoryHelper(idx, atom)
}
}

70
src/aba/problems/admissibility.rs
View file

@ -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<A: Atom> {
pub struct EnumerateAdmissibleExtensions<A: Atom> {
found: Vec<HashSet<A>>,
}
pub struct VerifyAdmissibility<A: Atom> {
/// 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<A: Atom> {
pub assumptions: Vec<A>,
}
/// *(Literal)* `A` is element of `th(S)`
#[derive(Debug)]
pub struct SetInference<A: Atom>(A);
pub struct SetTheory<A: Atom>(A);
/// Helper for [`SetTheory`]
#[derive(Debug)]
pub struct SetInferenceHelper<A: Atom>(usize, A);
pub struct SetTheoryHelper<A: Atom>(usize, A);
fn initial_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
inference_helper::<SetInference<_>, _>(aba).collect_into(&mut clauses);
inference_helper::<SetTheory<_>, _>(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<A: Atom>(state: SolverState<'_, A>) -> HashSet<A> {
.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<A: Atom>(state: SolverState<'_, A>) -> HashSet<A> {
.collect()
}
impl<A: Atom> Problem<A> for Admissibility<A> {
impl<A: Atom> Problem<A> for SampleAdmissibleExtension {
type Output = HashSet<A>;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
@ -87,7 +97,7 @@ impl<A: Atom> Problem<A> for Admissibility<A> {
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<A: Atom> Problem<A> for Admissibility<A> {
}
}
impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
type Output = Vec<HashSet<A>>;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
@ -113,7 +123,7 @@ impl<A: Atom> MultishotProblem<A> for Admissibility<A> {
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<A: Atom> MultishotProblem<A> for Admissibility<A> {
.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<A: Atom> MultishotProblem<A> for Admissibility<A> {
.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<A: Atom> MultishotProblem<A> for Admissibility<A> {
}
}
impl<A: Atom> Problem<A> for VerifyAdmissibility<A> {
impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> 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<A: Atom> Problem<A> for VerifyAdmissibility<A> {
}
}
impl<A: Atom> InferenceAtom<A> for SetInference<A> {
type Helper = SetInferenceHelper<A>;
impl<A: Atom> TheoryAtom<A> for SetTheory<A> {
type Helper = SetTheoryHelper<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)
fn new_helper(idx: usize, atom: A) -> Self::Helper {
SetTheoryHelper(idx, atom)
}
}

49
src/aba/problems/conflict_free.rs
View file

@ -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<char>,
pub struct ConflictFreeness<A: Atom> {
pub assumptions: HashSet<A>,
}
impl Problem<char> for ConflictFreeness {
impl<A: Atom> Problem<A> for ConflictFreeness<A> {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<char>) -> ClauseList {
fn additional_clauses(&self, aba: &Aba<A>) -> 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<char>) -> bool {
fn check(&self, aba: &Aba<A>) -> bool {
// Make sure that every assumption is part of the ABA
self.assumptions.iter().all(|a| aba.contains_assumption(a))
}

2
src/aba/problems/mod.rs
View file

@ -24,6 +24,7 @@ pub struct SolverState<'a, A: Atom + 'a> {
map: &'a Mapper,
}
#[doc(notable_trait)]
pub trait Problem<A: Atom> {
type Output;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList;
@ -34,6 +35,7 @@ pub trait Problem<A: Atom> {
}
}
#[doc(notable_trait)]
pub trait MultishotProblem<A: Atom> {
type Output;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList;

7
src/clauses.rs
View file

@ -10,12 +10,13 @@ pub type ClauseList = Vec<Clause>;
pub type RawClause = Vec<RawLiteral>;
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<A: Debug + Display + Hash + Eq + Clone + 'static> Atom for A {}
/// A disjunction of [`Literal`]s.
pub struct Clause {
list: Vec<Literal>,
}

24
src/literal.rs
View file

@ -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<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>;
/// ([`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<A: Atom>: Sized + IntoLiteral {
/// Helper type
type Helper: IntoLiteral;
/// Construct this [`Literal`]
fn new(atom: A) -> Self;
}
pub trait InferenceAtomHelper<A: Atom>: Sized + IntoLiteral {
fn new(idx: usize, atom: A) -> Self;
/// Construct the helper [`Literal`]
fn new_helper(idx: usize, atom: A) -> Self::Helper;
}
impl Literal {

12
src/main.rs
View file

@ -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)?;
}
}

28
src/tests/mod.rs
View file

@ -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<char> {
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<HashSet<char>> = 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<HashSet<char>> = 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),