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

rewrite, simplify

Browse source
This commit is contained in:
Malte Tammena 2024-03-13 22:26:04 +01:00
parent a1a779c404
commit 1ab554fc8e
10 changed files with 340 additions and 250 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
src/aba/debug.rs Normal file
View file

@ -0,0 +1,82 @@
#![cfg(test)]
use std::collections::{BTreeMap, HashMap, HashSet};
use super::{Aba, Num};
#[derive(Debug, Default, Clone)]
pub struct DebugAba {
aba: Aba,
forward_map: HashMap<char, Num>,
backward_map: BTreeMap<Num, char>,
next: Num,
}
impl DebugAba {
pub fn with_assumption(mut self, assumption: char, inverse: char) -> Self {
let assumption = self.forward(assumption);
let inverse = self.forward(inverse);
self.aba = self.aba.with_assumption(assumption, inverse);
self
}
pub fn with_rule<'n, B: IntoIterator<Item = char>>(mut self, head: char, body: B) -> Self {
let head = self.forward(head);
let body: Vec<_> = body
.into_iter()
.scan(&mut self, |aba, elem| {
let elem = aba.forward(elem);
Some(elem)
})
.collect();
self.aba = self.aba.with_rule(head, body);
self
}
pub fn aba(&self) -> &Aba {
&self.aba
}
pub fn forward_atom(&self, atom: char) -> Option<Num> {
self.forward_map.get(&atom).cloned()
}
pub fn forward_set(&self, set: HashSet<char>) -> Option<HashSet<Num>> {
set.into_iter()
.map(|atom| self.forward_atom(atom))
.collect()
}
pub fn forward_sets<S: IntoIterator<Item = HashSet<char>>>(
&self,
sets: S,
) -> Option<Vec<HashSet<Num>>> {
sets.into_iter().map(|set| self.forward_set(set)).collect()
}
pub fn backward_sets<S: IntoIterator<Item = HashSet<Num>>>(
&self,
sets: S,
) -> Option<Vec<HashSet<char>>> {
sets.into_iter()
.map(|set| {
set.into_iter()
.map(|atom| self.backward_map.get(&atom).cloned())
.collect()
})
.collect()
}
fn forward(&mut self, atom: char) -> Num {
match self.forward_map.get(&atom) {
Some(atom) => *atom,
None => {
let next = self.next;
self.next += 1;
self.forward_map.insert(atom, next);
self.backward_map.insert(next, atom);
next
}
}
}
}

91
src/aba/mod.rs
View file

@ -4,12 +4,12 @@
//!
//! ## Example
//! ```
//! # use aba2sat::aba::Aba;
//! # use aba2sat::aba::debug::DebugAba;
//! # use aba2sat::aba::problems::solve;
//! # use aba2sat::aba::problems::admissibility::VerifyAdmissibleExtension;
//! let aba =
//! // Start with an empty framework
//! Aba::default()
//! DebugAba::default()
//! // Add an assumption 'a' with inverse 'p'
//! .with_assumption('a', 'p')
//! // Add an assumption 'b' with inverse 'q'
@ -35,38 +35,44 @@ use crate::{
literal::{IntoLiteral, Literal, TheoryAtom},
};
pub mod debug;
pub mod problems;
pub type Rule<A> = (A, HashSet<A>);
pub type RuleList<A> = Vec<Rule<A>>;
#[derive(Debug, Default, Clone, PartialEq)]
pub struct Aba<A: Atom> {
pub rules: RuleList<A>,
pub inverses: HashMap<A, A>,
}
#[derive(Debug)]
pub struct Theory<A: Atom>(A);
pub struct Theory(Num);
impl<A: Atom> From<A> for Theory<A> {
fn from(value: A) -> Self {
impl From<Num> for Theory {
fn from(value: Num) -> Self {
Self(value)
}
}
impl<A: Atom> Aba<A> {
pub fn with_assumption(mut self, assumption: A, inverse: A) -> Self {
pub type Rule<A> = (A, HashSet<A>);
pub type RuleList<A> = Vec<Rule<A>>;
pub type Num = u32;
#[derive(Debug, Default, Clone, PartialEq)]
pub struct Aba {
rules: RuleList<Num>,
inverses: HashMap<Num, Num>,
}
impl Aba {
pub fn with_assumption(mut self, assumption: Num, inverse: Num) -> Self {
self.inverses.insert(assumption, inverse);
self
}
pub fn with_rule<B: IntoIterator<Item = A>>(mut self, head: A, body: B) -> Self {
self.rules.push((head, body.into_iter().collect()));
pub fn with_rule<B: IntoIterator<Item = Num>>(mut self, head: Num, body: B) -> Self {
let mut body_trans = HashSet::new();
body.into_iter().for_each(|elem| {
body_trans.insert(elem);
});
self.rules.push((head, body_trans));
self
}
pub fn universe(&self) -> impl Iterator<Item = &A> {
pub fn universe(&self) -> impl Iterator<Item = &Num> {
// List of all elements of our ABA, basically our L (universe)
self.inverses
.keys()
@ -75,11 +81,11 @@ impl<A: Atom> Aba<A> {
.chain(self.rules.iter().map(|(head, _)| head))
}
pub fn assumptions(&self) -> impl Iterator<Item = &A> {
pub fn assumptions(&self) -> impl Iterator<Item = &Num> {
self.inverses.keys()
}
pub fn contains_assumption(&self, a: &A) -> bool {
pub fn contains_assumption(&self, a: &Num) -> bool {
self.inverses.contains_key(a)
}
@ -120,7 +126,7 @@ impl<A: Atom> Aba<A> {
}
if body.iter().all(|atom| reachable.contains(atom)) {
marked_any = true;
reachable.insert(head.clone());
reachable.insert(*head);
}
}
if !marked_any {
@ -135,29 +141,21 @@ impl<A: Atom> Aba<A> {
}
fn derive_rule_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Theory<_>, _>(self)
theory_helper::<Theory>(self)
}
fn rule_heads(&self) -> impl Iterator<Item = &A> + '_ {
fn rule_heads(&self) -> impl Iterator<Item = &Num> + '_ {
self.rules.iter().map(|(head, _)| head)
}
fn has_assumption(&self, atom: &A) -> bool {
self.inverses.contains_key(atom)
}
fn has_element(&self, element: &A) -> bool {
self.universe().any(|e| element == e)
}
}
fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>) -> ClauseList {
fn body_to_clauses<I: TheoryAtom>(head: Literal, body: &HashSet<Num>) -> ClauseList {
let mut clauses = vec![];
let mut left_implication: Clause = body.iter().map(|elem| I::new(elem.clone()).neg()).collect();
let mut left_implication: Clause = body.iter().map(|elem| I::new(*elem).neg()).collect();
left_implication.push(head.clone().positive());
clauses.push(left_implication);
body.iter()
.map(|elem| vec![head.clone().negative(), I::new(elem.clone()).pos()].into())
.map(|elem| vec![head.clone().negative(), I::new(*elem).pos()].into())
.collect_into(&mut clauses);
clauses
}
@ -187,7 +185,7 @@ fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>)
/// A lot of the overhead is due to the fact that multiple bodies are an option, if that's
/// not given for a head `p` we use the simplified translation logic where `p` is true iff
/// `bodies(p)` is true.
pub fn theory_helper<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> impl Iterator<Item = Clause> + '_ {
pub fn theory_helper<I: TheoryAtom>(aba: &Aba) -> impl Iterator<Item = Clause> + '_ {
// The combined list of rules, such that every
// head is unique and possible contains a list of bodies
let mut rules_combined =
@ -203,7 +201,7 @@ pub fn theory_helper<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> impl Iterator<I
// such that it cannot be derived at all. This is to prevent the solver from
// guessing this atom on it's own
aba.universe()
.filter(|atom| !aba.has_assumption(atom))
.filter(|atom| !aba.contains_assumption(atom))
.filter(|atom| !rule_heads.contains(atom))
.map(|atom| (atom, vec![]))
.collect_into(&mut rules_combined);
@ -214,10 +212,10 @@ pub fn theory_helper<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> impl Iterator<I
.flat_map(|(head, bodies)| match &bodies[..] {
// No bodies, add a clause that prevents the head from accuring in the theory
[] => {
vec![Clause::from(vec![I::new(head.clone()).neg()])]
vec![Clause::from(vec![I::new(*head).neg()])]
}
// A single body only, this is equivalent to a head that can only be derived by a single rule
[body] => body_to_clauses::<I, _>(I::new(head.clone()).pos(), body),
[body] => body_to_clauses::<I>(I::new(*head).pos(), body),
// n bodies, we'll need to take extra care to allow any number of bodies to derive this
// head without logic errors
bodies => {
@ -226,21 +224,18 @@ pub fn theory_helper<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> impl Iterator<I
.iter()
.enumerate()
.flat_map(|(idx, body)| {
body_to_clauses::<I, _>(
TheoryHelper::<I, _>::new(idx, head.clone()).pos(),
body,
)
body_to_clauses::<I>(TheoryHelper::<I, _>::new(idx, *head).pos(), body)
})
.collect_into(&mut clauses);
let helpers: Vec<_> = (0..bodies.len())
.map(|idx| TheoryHelper::<I, _>::new(idx, head.clone()).pos())
.map(|idx| TheoryHelper::<I, _>::new(idx, *head).pos())
.collect();
let mut right_implification: Clause = helpers.iter().cloned().collect();
right_implification.push(I::new(head.clone()).neg());
right_implification.push(I::new(*head).neg());
clauses.push(right_implification);
helpers
.into_iter()
.map(|helper| Clause::from(vec![I::new(head.clone()).pos(), helper.negative()]))
.map(|helper| Clause::from(vec![I::new(*head).pos(), helper.negative()]))
.collect_into(&mut clauses);
clauses
}
@ -248,13 +243,13 @@ pub fn theory_helper<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> impl Iterator<I
}
#[derive(Debug)]
struct TheoryHelper<T: TheoryAtom<A>, A: Atom> {
struct TheoryHelper<T: TheoryAtom, A: Atom> {
_idx: usize,
_atom: A,
inner: PhantomData<T>,
}
impl<T: TheoryAtom<A>, A: Atom> TheoryHelper<T, A> {
impl<T: TheoryAtom, A: Atom> TheoryHelper<T, A> {
fn new(idx: usize, atom: A) -> Self {
Self {
_idx: idx,

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

@ -2,8 +2,8 @@
use std::collections::HashSet;
use crate::{
aba::{theory_helper, Aba, Theory},
clauses::{Atom, Clause, ClauseList},
aba::{theory_helper, Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
Result,
@ -13,8 +13,8 @@ use super::{LoopControl, MultishotProblem, Problem, SetTheory, SolverState};
/// Compute all admissible extensions for an [`Aba`]
#[derive(Default, Debug)]
pub struct EnumerateAdmissibleExtensions<A: Atom> {
found: Vec<HashSet<A>>,
pub struct EnumerateAdmissibleExtensions {
found: Vec<HashSet<Num>>,
}
/// Sample an admissible extensions from an [`Aba`].
@ -23,88 +23,86 @@ pub struct EnumerateAdmissibleExtensions<A: Atom> {
pub struct SampleAdmissibleExtension;
/// Verify wether `assumptions` is an admissible extension of an [`Aba`]
pub struct VerifyAdmissibleExtension<A: Atom> {
pub assumptions: Vec<A>,
pub struct VerifyAdmissibleExtension {
pub assumptions: HashSet<Num>,
}
/// Decide whether `assumption` is credulously admissible in an [`Aba`]
pub struct DecideCredulousAdmissibility<A> {
pub element: A,
pub struct DecideCredulousAdmissibility {
pub element: Num,
}
pub fn initial_admissibility_clauses<I: std::fmt::Debug + 'static + TheoryAtom<A>, A: Atom>(
aba: &Aba<A>,
pub fn initial_admissibility_clauses<I: std::fmt::Debug + 'static + TheoryAtom>(
aba: &Aba,
) -> ClauseList {
let mut clauses = vec![];
// Create inference for the problem set
theory_helper::<I, _>(aba).collect_into(&mut clauses);
theory_helper::<I>(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`:
// a in th(A) <=> b not in th(S)
Clause::from(vec![
Theory::new(assumption.clone()).pos(),
SetTheory::new(inverse.clone()).pos(),
Theory::new(*assumption).pos(),
SetTheory::new(*inverse).pos(),
]),
Clause::from(vec![
Theory::new(assumption.clone()).neg(),
SetTheory::new(inverse.clone()).neg(),
Theory::new(*assumption).neg(),
SetTheory::new(*inverse).neg(),
]),
// Prevent attacks from the opponent to the selected set
// For any assumption `a` and it's inverse `b`:
// b in th(A) and a in th(S) => bottom
Clause::from(vec![
Theory::new(inverse.clone()).neg(),
SetTheory::new(assumption.clone()).neg(),
Theory::new(*inverse).neg(),
SetTheory::new(*assumption).neg(),
]),
// Prevent self-attacks
// For any assumption `a` and it's inverse `b`:
// a in th(S) and b in th(S) => bottom
Clause::from(vec![
SetTheory::new(assumption.clone()).neg(),
SetTheory::new(inverse.clone()).neg(),
SetTheory::new(*assumption).neg(),
SetTheory::new(*inverse).neg(),
]),
]
.into_iter()
.collect_into(&mut clauses);
}
clauses
}
fn construct_found_set<A: Atom>(state: SolverState<'_, A>) -> HashSet<A> {
fn construct_found_set(state: SolverState<'_>) -> HashSet<Num> {
state
.aba
.inverses
.keys()
.assumptions()
.filter_map(|assumption| {
let literal = SetTheory::new(assumption.clone()).pos();
let literal = SetTheory::new(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(assumption.clone()),
Some(true) => Some(*assumption),
_ => None,
}
})
.collect()
}
impl<A: Atom> Problem<A> for SampleAdmissibleExtension {
type Output = HashSet<A>;
impl Problem for SampleAdmissibleExtension {
type Output = HashSet<Num>;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetTheory::new(assumption.clone()).pos())
.map(|assumption| SetTheory::new(*assumption).pos())
.collect();
clauses.push(no_empty_set);
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
fn construct_output(self, state: SolverState<'_>) -> Self::Output {
if state.sat_result {
construct_found_set(state)
} else {
@ -113,18 +111,18 @@ impl<A: Atom> Problem<A> for SampleAdmissibleExtension {
}
}
impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
type Output = Vec<HashSet<A>>;
impl MultishotProblem<Num> for EnumerateAdmissibleExtensions {
type Output = Vec<HashSet<Num>>;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList {
match iteration {
0 => {
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Prevent the empty set
let no_empty_set: Clause = aba
.inverses
.keys()
.map(|assumption| SetTheory::new(assumption.clone()).pos())
.map(|assumption| SetTheory::new(*assumption).pos())
.collect();
clauses.push(no_empty_set);
clauses
@ -135,13 +133,12 @@ impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
// {-a, b, -c, -d, e, f} must be true
let just_found = &self.found[idx - 1];
let new_clause = aba
.inverses
.keys()
.assumptions()
.map(|assumption| {
if just_found.contains(assumption) {
SetTheory::new(assumption.clone()).neg()
SetTheory::new(*assumption).neg()
} else {
SetTheory::new(assumption.clone()).pos()
SetTheory::new(*assumption).pos()
}
})
.collect();
@ -150,7 +147,7 @@ impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
}
}
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl {
fn feedback(&mut self, state: SolverState<'_>) -> LoopControl {
if !state.sat_result {
return LoopControl::Stop;
}
@ -160,10 +157,10 @@ impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetTheory::new(assumption.clone()).pos();
let literal = SetTheory::new(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(assumption.clone()),
Some(true) => Some(*assumption),
_ => None,
}
})
@ -174,23 +171,26 @@ impl<A: Atom> MultishotProblem<A> for EnumerateAdmissibleExtensions<A> {
fn construct_output(
mut self,
_state: SolverState<'_, A>,
_state: SolverState<'_>,
_total_iterations: usize,
) -> Self::Output {
// Re-Add the empty set
self.found.push(HashSet::new());
self.found
.into_iter()
.map(|set| set.into_iter().collect())
.collect()
}
}
impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
impl Problem for VerifyAdmissibleExtension {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> crate::clauses::ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
fn additional_clauses(&self, aba: &Aba) -> crate::clauses::ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Force inference on all members of the set
for assumption in aba.assumptions() {
let inf = SetTheory::new(assumption.clone());
let inf = SetTheory::new(*assumption);
if self.assumptions.contains(assumption) {
clauses.push(Clause::from(vec![inf.pos()]))
} else {
@ -200,16 +200,16 @@ impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
fn construct_output(self, state: SolverState<'_>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<A>) -> Result {
fn check(&self, aba: &Aba) -> Result {
// Make sure that every assumption is part of the ABA
match self
.assumptions
.iter()
.find(|a| !aba.contains_assumption(a))
.find(|assumption| !aba.contains_assumption(assumption))
{
Some(assumption) => Err(Error::ProblemCheckFailed(format!(
"Assumption {assumption:?} not present in ABA framework"
@ -219,21 +219,21 @@ impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
}
}
impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
impl Problem for DecideCredulousAdmissibility {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
fn construct_output(self, state: SolverState<'_>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<A>) -> Result {
if aba.has_assumption(&self.element) {
fn check(&self, aba: &Aba) -> Result {
if aba.contains_assumption(&self.element) {
Ok(())
} else {
Err(Error::ProblemCheckFailed(format!(

57
src/aba/problems/complete.rs
View file

@ -1,8 +1,8 @@
use std::collections::HashSet;
use crate::{
aba::{Aba, Theory},
clauses::{Atom, Clause, ClauseList},
aba::{Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
Result,
@ -14,34 +14,34 @@ use super::{
};
#[derive(Debug, Default)]
pub struct EnumerateCompleteExtensions<A> {
found: Vec<HashSet<A>>,
pub struct EnumerateCompleteExtensions {
found: Vec<HashSet<Num>>,
}
/// Decide whether `assumption` is credulously complete in an [`Aba`]
pub struct DecideCredulousComplete<A> {
pub element: A,
pub struct DecideCredulousComplete {
pub element: Num,
}
fn initial_complete_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
fn initial_complete_clauses(aba: &Aba) -> ClauseList {
// Take everything from admissibility
let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
let mut clauses = initial_admissibility_clauses::<SetTheory>(aba);
// Additional complete logic
for (assumption, inverse) in &aba.inverses {
// For any assumption `a` and it's inverse `b`:
// b not in th(A) => a in th(S)
clauses.push(Clause::from(vec![
Theory(inverse.clone()).pos(),
SetTheory(assumption.clone()).pos(),
Theory(*inverse).pos(),
SetTheory(*assumption).pos(),
]));
}
clauses
}
impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
type Output = Vec<HashSet<A>>;
impl MultishotProblem<Num> for EnumerateCompleteExtensions {
type Output = Vec<HashSet<Num>>;
fn additional_clauses(&self, aba: &Aba<A>, iteration: usize) -> ClauseList {
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList {
match iteration {
0 => initial_complete_clauses(aba),
idx => {
@ -50,13 +50,12 @@ impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
// {-a, b, -c, -d, e, f} must be true
let just_found = &self.found[idx - 1];
let new_clause = aba
.inverses
.keys()
.assumptions()
.map(|assumption| {
if just_found.contains(assumption) {
SetTheory::new(assumption.clone()).neg()
SetTheory::new(*assumption).neg()
} else {
SetTheory::new(assumption.clone()).pos()
SetTheory::new(*assumption).pos()
}
})
.collect();
@ -65,7 +64,7 @@ impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
}
}
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl {
fn feedback(&mut self, state: SolverState<'_>) -> LoopControl {
if !state.sat_result {
return LoopControl::Stop;
}
@ -75,10 +74,10 @@ impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
.inverses
.keys()
.filter_map(|assumption| {
let literal = SetTheory::new(assumption.clone()).pos();
let literal = SetTheory::new(*assumption).pos();
let raw = state.map.get_raw(&literal)?;
match state.solver.value(raw) {
Some(true) => Some(assumption.clone()),
Some(true) => Some(*assumption),
_ => None,
}
})
@ -87,30 +86,26 @@ impl<A: Atom> MultishotProblem<A> for EnumerateCompleteExtensions<A> {
LoopControl::Continue
}
fn construct_output(
self,
_state: SolverState<'_, A>,
_total_iterations: usize,
) -> Self::Output {
fn construct_output(self, _state: SolverState<'_>, _total_iterations: usize) -> Self::Output {
self.found
}
}
impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
impl Problem for DecideCredulousComplete {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
fn additional_clauses(&self, aba: &Aba) -> ClauseList {
let mut clauses = initial_complete_clauses(aba);
clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
clauses.push(Clause::from(vec![SetTheory(self.element).pos()]));
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
fn construct_output(self, state: SolverState<'_>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<A>) -> Result {
if aba.has_element(&self.element) {
fn check(&self, aba: &Aba) -> Result {
if aba.contains_assumption(&self.element) {
Ok(())
} else {
Err(Error::ProblemCheckFailed(format!(

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

@ -1,8 +1,8 @@
use std::collections::HashSet;
use crate::{
aba::{Aba, Theory},
clauses::{Atom, Clause, ClauseList},
aba::{Aba, Num, Theory},
clauses::{Clause, ClauseList},
error::Error,
literal::{IntoLiteral, TheoryAtom},
Result,
@ -10,18 +10,18 @@ use crate::{
use super::{Problem, SolverState};
pub struct ConflictFreeness<A: Atom> {
pub assumptions: HashSet<A>,
pub struct ConflictFreeness {
pub assumptions: HashSet<Num>,
}
impl<A: Atom> Problem<A> for ConflictFreeness<A> {
impl Problem for ConflictFreeness {
type Output = bool;
fn additional_clauses(&self, aba: &Aba<A>) -> 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 assumption in aba.assumptions() {
let theory = Theory::new(assumption.clone());
let theory = Theory::new(*assumption);
if self.assumptions.contains(assumption) {
clauses.push(vec![theory.pos()].into())
} else {
@ -30,23 +30,23 @@ impl<A: Atom> Problem<A> for ConflictFreeness<A> {
}
for (assumption, inverse) in &aba.inverses {
clauses.push(Clause::from(vec![
Theory::new(assumption.clone()).neg(),
Theory::new(inverse.clone()).neg(),
Theory::new(*assumption).neg(),
Theory::new(*inverse).neg(),
]));
}
clauses
}
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
fn construct_output(self, state: SolverState<'_>) -> Self::Output {
state.sat_result
}
fn check(&self, aba: &Aba<A>) -> Result {
fn check(&self, aba: &Aba) -> Result {
// Make sure that every assumption is part of the ABA
match self
.assumptions
.iter()
.find(|a| !aba.contains_assumption(a))
.find(|assumption| !aba.contains_assumption(assumption))
{
Some(assumption) => Err(Error::ProblemCheckFailed(format!(
"Assumption {:?} not present in ABA framework",

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

@ -6,7 +6,7 @@ use crate::{
mapper::Mapper,
};
use super::Aba;
use super::{Aba, Num};
pub mod admissibility;
pub mod complete;
@ -18,20 +18,20 @@ pub enum LoopControl {
Stop,
}
pub struct SolverState<'a, A: Atom + 'a> {
aba: &'a Aba<A>,
pub struct SolverState<'a> {
aba: &'a Aba,
sat_result: bool,
solver: &'a Solver,
map: &'a Mapper,
}
#[doc(notable_trait)]
pub trait Problem<A: Atom> {
pub trait Problem {
type Output;
fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList;
fn construct_output(self, state: SolverState<'_, A>) -> Self::Output;
fn additional_clauses(&self, aba: &Aba) -> ClauseList;
fn construct_output(self, state: SolverState<'_>) -> Self::Output;
fn check(&self, _aba: &Aba<A>) -> Result {
fn check(&self, _aba: &Aba) -> Result {
Ok(())
}
}
@ -39,26 +39,26 @@ 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;
fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl;
fn construct_output(self, state: SolverState<'_, A>, total_iterations: usize) -> Self::Output;
fn additional_clauses(&self, aba: &Aba, iteration: usize) -> ClauseList;
fn feedback(&mut self, state: SolverState<'_>) -> LoopControl;
fn construct_output(self, state: SolverState<'_>, total_iterations: usize) -> Self::Output;
fn check(&self, _aba: &Aba<A>) -> Result {
fn check(&self, _aba: &Aba) -> Result {
Ok(())
}
}
/// *(Literal)* `A` is element of `th(S)`
#[derive(Debug)]
pub struct SetTheory<A: Atom>(A);
pub struct SetTheory(Num);
impl<A: Atom> From<A> for SetTheory<A> {
fn from(value: A) -> Self {
impl From<Num> for SetTheory {
fn from(value: Num) -> Self {
Self(value)
}
}
pub fn solve<A: Atom, P: Problem<A>>(problem: P, mut aba: Aba<A>) -> Result<P::Output> {
pub fn solve<P: Problem>(problem: P, mut aba: Aba) -> Result<P::Output> {
// Trim the ABA, this is always safe
aba.trim();
// Let the problem perform additional checks before starting the solver
@ -101,7 +101,7 @@ pub fn solve<A: Atom, P: Problem<A>>(problem: P, mut aba: Aba<A>) -> Result<P::O
pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
mut problem: P,
mut aba: Aba<A>,
mut aba: Aba,
) -> Result<P::Output> {
// Trim the ABA, this is always safe
aba.trim();

11
src/literal.rs
View file

@ -3,7 +3,7 @@ use std::{
fmt::Debug,
};
use crate::clauses::Atom;
use crate::aba::Num;
/// A Literal can be used in SAT [`Clause`](crate::clauses::Clause)s
#[derive(Clone)]
@ -42,11 +42,12 @@ impl<T: Any + Debug + Sized> IntoLiteral for T {
/// the theory of a (sub-)set of assumptions (`th(S)`) in an [`Aba`](crate::aba::Aba).
///
/// See [`crate::aba::theory_helper`].
pub trait TheoryAtom<A: Atom>: Sized + IntoLiteral + std::fmt::Debug + 'static {
fn new(atom: A) -> Self;
pub trait TheoryAtom: Sized + IntoLiteral + std::fmt::Debug + 'static {
fn new(atom: Num) -> Self;
}
impl<A: Atom, T: From<A> + Sized + IntoLiteral + std::fmt::Debug + 'static> TheoryAtom<A> for T {
fn new(atom: A) -> Self {
impl<T: From<Num> + Sized + IntoLiteral + std::fmt::Debug + 'static> TheoryAtom for T {
fn new(atom: Num) -> Self {
Self::from(atom)
}
}

24
src/main.rs
View file

@ -4,12 +4,15 @@
use std::{collections::HashSet, fmt::Write as WriteFmt, fs::read_to_string, io::Write as WriteIo};
use aba::problems::{
admissibility::{
DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, SampleAdmissibleExtension,
VerifyAdmissibleExtension,
use aba::{
problems::{
admissibility::{
DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, SampleAdmissibleExtension,
VerifyAdmissibleExtension,
},
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
},
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
Num,
};
use clap::Parser;
@ -22,13 +25,6 @@ macro_rules! set {
}}
}
#[cfg(test)]
macro_rules! map {
($($from:expr => $to:expr),*) => {{
vec![$(($from, $to)),*].into_iter().collect()
}}
}
mod aba;
mod args;
mod clauses;
@ -88,7 +84,7 @@ fn main() -> Result {
__main().inspect_err(|why| eprintln!("Error: {why}"))
}
impl IccmaFormattable for Vec<HashSet<u32>> {
impl IccmaFormattable for Vec<HashSet<Num>> {
fn fmt_iccma(&self) -> Result<String> {
let output = self
.iter()
@ -102,7 +98,7 @@ impl IccmaFormattable for Vec<HashSet<u32>> {
}
}
impl IccmaFormattable for HashSet<u32> {
impl IccmaFormattable for HashSet<Num> {
fn fmt_iccma(&self) -> Result<String> {
let set = self
.iter()

32
src/parser.rs
View file

@ -35,10 +35,10 @@ use nom::multi::fold_many0;
use nom::sequence::{preceded, terminated, tuple};
use nom::IResult;
use crate::aba::Aba;
use crate::aba::{Aba, Num};
use crate::error::Result;
pub fn aba_file(input: &str) -> Result<Aba<u32>> {
pub fn aba_file(input: &str) -> Result<Aba> {
let (input, number_of_atoms) = p_line(input)?;
let (_, aba) = all_consuming(aba)(input)?;
#[cfg(debug_assertions)]
@ -68,12 +68,12 @@ fn p_line(input: &str) -> IResult<&str, u32> {
#[derive(Debug, PartialEq)]
enum AbaLine {
Comment,
Assumption(u32),
Inverse(u32, u32),
Rule(u32, HashSet<u32>),
Assumption(Num),
Inverse(Num, Num),
Rule(Num, HashSet<Num>),
}
fn aba(input: &str) -> IResult<&str, Aba<u32>> {
fn aba(input: &str) -> IResult<&str, Aba> {
let parse_aba_line = terminated(alt((assumption, comment, inverse, rule)), eol_or_eoi);
let collect_aba = fold_many0(
parse_aba_line,
@ -133,15 +133,15 @@ fn eol_or_eoi(input: &str) -> IResult<&str, &str> {
alt((newline, eof))(input)
}
fn atom(input: &str) -> IResult<&str, u32> {
verify(complete::u32, |&num| num != 0)(input)
fn atom(input: &str) -> IResult<&str, Num> {
map(verify(complete::u32, |&num| num != 0), |atom| atom as Num)(input)
}
#[cfg(test)]
mod tests {
use nom::combinator::all_consuming;
use crate::aba::Aba;
use crate::aba::{Aba, Num};
fn assert_parse<F, T>(parser: F, input: &str, expected: T)
where
@ -149,7 +149,7 @@ mod tests {
T: std::fmt::Debug + PartialEq,
{
let (_rest, result) =
all_consuming(parser)(input).expect(&format!("Failed to parse {input:?}"));
all_consuming(parser)(input).unwrap_or_else(|_| panic!("Failed to parse {input:?}"));
assert_eq!(result, expected);
}
@ -198,7 +198,7 @@ mod tests {
fn assumption() {
use super::AbaLine::Assumption;
assert_parse(super::assumption, "a 1", Assumption(1));
assert_parse(super::assumption, "a 4294967295", Assumption(u32::MAX));
assert_parse(super::assumption, "a 4294967295", Assumption(Num::MAX));
assert_parse(super::assumption, "a\t1", Assumption(1));
assert_parse(super::assumption, "a\t 1", Assumption(1));
assert_parse(super::assumption, "a\t 1 ", Assumption(1));
@ -243,10 +243,7 @@ mod tests {
r#"a 2
c 2 1
r 1 2 3"#,
Aba {
rules: vec![(1, set!(2, 3))],
inverses: map![2 => 1],
},
Aba::default().with_assumption(2, 1).with_rule(1, [2, 3]),
)
}
@ -262,10 +259,7 @@ r 1 2 3
.unwrap();
assert_eq!(
res,
Aba {
rules: vec![(1, set!(2, 3))],
inverses: map![2 => 1],
}
Aba::default().with_assumption(2, 1).with_rule(1, [2, 3])
)
}
}

121
src/tests/mod.rs
View file

@ -1,16 +1,16 @@
use std::collections::HashSet;
use crate::aba::{
debug::DebugAba,
problems::{
admissibility::{EnumerateAdmissibleExtensions, VerifyAdmissibleExtension},
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
complete::DecideCredulousComplete,
conflict_free::ConflictFreeness,
},
Aba,
};
fn simple_aba_example_1() -> Aba<char> {
Aba::default()
fn simple_aba_example_1() -> DebugAba {
DebugAba::default()
.with_assumption('a', 'r')
.with_assumption('b', 's')
.with_assumption('c', 't')
@ -35,11 +35,20 @@ fn simple_conflict_free_verification() {
set_checks
.into_iter()
.for_each(|(assumptions, expectation)| {
.for_each(|(assumptions, expectation): (HashSet<char>, _)| {
eprintln!("Checking set {assumptions:?}");
let result =
crate::aba::problems::solve(ConflictFreeness { assumptions }, aba.clone()).unwrap();
assert!(result == expectation);
let translated = aba.forward_set(assumptions.clone()).unwrap();
let result = crate::aba::problems::solve(
ConflictFreeness {
assumptions: translated,
},
aba.aba().clone(),
)
.unwrap();
assert!(
result == expectation,
"Expected {expectation} from solver, but got {result} while checking {assumptions:?}"
);
})
}
@ -47,17 +56,18 @@ fn simple_conflict_free_verification() {
fn simple_admissible_verification() {
let aba = simple_aba_example_1();
let set_checks = vec![
(vec![], true),
(vec!['a', 'b'], false),
(vec!['a'], false),
(vec!['b'], true),
(set![], true),
(set!['a', 'b'], false),
(set!['a'], false),
(set!['b'], true),
];
set_checks
.into_iter()
.for_each(|(assumptions, expectation)| {
.for_each(|(assumptions, expectation): (HashSet<char>, _)| {
eprintln!("Checking set {assumptions:?}");
let translated= aba.forward_set(assumptions.clone()).unwrap();
let result =
crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: assumptions.clone() }, aba.clone()).unwrap();
crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: translated }, aba.aba().clone()).unwrap();
assert!(
result == expectation,
"Expected {expectation} from solver, but got {result} while checking {assumptions:?}"
@ -69,18 +79,20 @@ 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(EnumerateAdmissibleExtensions::default(), aba)
.unwrap();
for elem in &expected {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(elem),
result.contains(&elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
for elem in aba.backward_sets(result).unwrap() {
assert!(
expected.contains(elem),
expected.contains(&elem),
"{elem:?} was found in the result, but is not expected!"
);
}
@ -88,20 +100,29 @@ fn simple_admissible_example() {
#[test]
fn simple_admissible_example_with_defense() {
let aba = simple_aba_example_1().with_rule('t', vec!['a', 'b']);
let aba = DebugAba::default()
.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('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(EnumerateAdmissibleExtensions::default(), aba)
.unwrap();
for elem in &expected {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(elem),
result.contains(&elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
for elem in aba.backward_sets(result).unwrap() {
assert!(
expected.contains(elem),
expected.contains(&elem),
"{elem:?} was found in the result, but is not expected!"
);
}
@ -109,7 +130,7 @@ fn simple_admissible_example_with_defense() {
#[test]
fn simple_admissible_atomic() {
let aba = Aba::default()
let aba = DebugAba::default()
.with_assumption('a', 'p')
.with_assumption('b', 'q')
.with_assumption('c', 'r')
@ -117,18 +138,20 @@ fn simple_admissible_atomic() {
.with_rule('q', ['a', 'c']);
let expected: Vec<HashSet<char>> =
vec![set!(), set!('b'), set!('c'), set!('a', 'c'), set!('b', 'c')];
let result =
crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
.unwrap();
for elem in &expected {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(elem),
result.contains(&elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
for elem in aba.backward_sets(result).unwrap() {
assert!(
expected.contains(elem),
expected.contains(&elem),
"{elem:?} was found in the result, but is not expected!"
);
}
@ -137,25 +160,27 @@ fn simple_admissible_atomic() {
#[test]
fn a_chain_with_no_beginning() {
// found this while grinding against ASPforABA (5aa9201)
let aba = Aba::default()
let aba = DebugAba::default()
.with_assumption('a', 'b')
.with_assumption('b', 'c')
.with_rule('c', ['a', 'd'])
.with_rule('d', ['c']);
let expected: Vec<HashSet<char>> = vec![set!(), set!('b')];
// 'a' cannot be defended against b since c is not derivable
let result =
crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
.unwrap();
for elem in &expected {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
assert!(
result.contains(elem),
result.contains(&elem),
"{elem:?} was expected but not found in result"
);
}
for elem in &result {
for elem in aba.backward_sets(result).unwrap() {
assert!(
expected.contains(elem),
expected.contains(&elem),
"{elem:?} was found in the result, but is not expected!"
);
}
@ -164,13 +189,15 @@ fn a_chain_with_no_beginning() {
#[test]
#[ignore]
fn loops_and_conflicts() {
let aba = Aba::default()
let aba = DebugAba::default()
.with_assumption('a', 'b')
.with_rule('b', ['a'])
.with_rule('b', ['c'])
.with_rule('c', ['b'])
.with_rule('d', ['b']);
let element = aba.forward_atom('d').unwrap();
let result =
crate::aba::problems::solve(DecideCredulousComplete { element: 'd' }, aba).unwrap();
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone())
.unwrap();
assert!(!result, "d cannot be credulous complete");
}