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

feat: restructure into lib/bin

Browse source
This commit is contained in:
Malte Tammena 2024-04-23 14:07:16 +02:00
parent 0e633b9a86
commit e99010873a
7 changed files with 92 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/aba/debug.rs
View file

@ -1,5 +1,3 @@
#![cfg(test)]
use std::collections::{BTreeMap, HashMap, HashSet};
use super::{Aba, Num};

12
src/aba/mod.rs
View file

@ -19,8 +19,10 @@
//!
//!
//! // Solve the problem whether the set of assumptions {'b'} is admissible
//! let atom = aba.forward_atom('b').unwrap();
//! let assumptions = vec![atom].into_iter().collect();
//! let result =
//! solve(VerifyAdmissibleExtension { assumptions: vec!['b'] }, &aba).unwrap();
//! solve(VerifyAdmissibleExtension { assumptions }, aba.aba().clone(), None).unwrap();
//!
//! // The result should be true
//! assert!(result)
@ -42,8 +44,8 @@ pub type Num = u32;
#[derive(Debug, Default, Clone, PartialEq, Eq)]
pub struct Aba {
rules: RuleList,
inverses: HashMap<Num, Num>,
pub rules: RuleList,
pub inverses: HashMap<Num, Num>,
}
impl Aba {
@ -97,8 +99,8 @@ impl Aba {
}
/// Prepare this aba for translation to SAT
pub fn prepare(self) -> PreparedAba {
PreparedAba::from(self)
pub fn prepare(self, max_loops: Option<usize>) -> PreparedAba {
PreparedAba::new(self, max_loops)
}
fn rule_heads(&self) -> impl Iterator<Item = &Num> + '_ {

21
src/aba/prepared.rs
View file

@ -5,7 +5,6 @@ use iter_tools::Itertools;
use crate::{
aba::Num,
args::ARGS,
clauses::Clause,
literal::{
lits::{LoopHelper, TheoryRuleBodyActive},
@ -28,6 +27,12 @@ pub struct PreparedAba {
}
impl PreparedAba {
/// Create a new [`PreparedAba`] from a raw [`Aba`]
pub fn new(mut aba: Aba, max_loops: Option<usize>) -> Self {
trim_unreachable_rules(&mut aba);
let loops = calculate_loops_and_their_support(&aba, max_loops);
PreparedAba { aba, loops }
}
/// Translate the ABA into base rules / definitions for SAT solving
pub fn derive_clauses<Ctx: Context>(&self) -> impl Iterator<Item = Clause> + '_ {
theory_helper::<Ctx>(self)
@ -55,7 +60,7 @@ impl PreparedAba {
/// ```
/// where body(h <- B) = B and and({a1, ..., ax}) = a1 and ... and ax.
///
/// This will lead to an exponential explosion when converted to naively CNF,
/// This will lead to an exponential explosion when converted to CNF naively,
/// since the formulas are mostly DNF. We use Tseitin's transformation to prevent this:
/// ```text
/// LH_i <=> RBA_1 or ... or RBA_n
@ -162,7 +167,7 @@ fn trim_unreachable_rules(aba: &mut Aba) {
});
}
fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
fn calculate_loops_and_their_support(aba: &Aba, max_loops: Option<usize>) -> Vec<r#Loop> {
let mut graph = petgraph::graph::DiGraph::<Num, ()>::new();
let universe = aba
.universe()
@ -189,7 +194,7 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
}
let mut loops = vec![];
const LOOP_SIZE_IN_MULT_UNIVERSE_SIZE: f32 = 1.0;
let max_loops = if let Some(max) = ARGS.as_ref().and_then(|args| args.max_loops) {
let max_loops = if let Some(max) = max_loops {
max
} else {
(universe.len() as f32 * LOOP_SIZE_IN_MULT_UNIVERSE_SIZE) as usize
@ -222,14 +227,6 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
loops
}
impl From<Aba> for PreparedAba {
fn from(mut aba: Aba) -> Self {
trim_unreachable_rules(&mut aba);
let loops = calculate_loops_and_their_support(&aba);
PreparedAba { aba, loops }
}
}
impl std::ops::Deref for PreparedAba {
type Target = Aba;

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

@ -49,8 +49,8 @@ pub trait MultishotProblem {
}
}
pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
let aba = aba.prepare();
pub fn solve<P: Problem>(problem: P, aba: Aba, max_loops: Option<usize>) -> Result<P::Output> {
let aba = aba.prepare(max_loops);
// Let the problem perform additional checks before starting the solver
problem.check(&aba)?;
// Create a map that will keep track of the translation between
@ -89,8 +89,12 @@ pub fn solve<P: Problem>(problem: P, aba: Aba) -> Result<P::Output> {
}
}
pub fn multishot_solve<P: MultishotProblem>(mut problem: P, aba: Aba) -> Result<P::Output> {
let aba = aba.prepare();
pub fn multishot_solve<P: MultishotProblem>(
mut problem: P,
aba: Aba,
max_loops: Option<usize>,
) -> Result<P::Output> {
let aba = aba.prepare(max_loops);
// Let the problem perform additional checks before starting the solver
problem.check(&aba)?;
// Create a map that will keep track of the translation between

22
src/lib.rs Normal file
View file

@ -0,0 +1,22 @@
#![feature(iter_collect_into)]
#![feature(iter_intersperse)]
#![feature(doc_notable_trait)]
#[cfg(test)]
macro_rules! set {
($($elem:expr),*) => {{
vec![$($elem),*].into_iter().collect()
}}
}
pub mod aba;
pub mod clauses;
pub mod error;
pub mod literal;
pub mod mapper;
pub mod parser;
#[cfg(test)]
mod tests;
pub use error::{Error, Result};

76
src/main.rs
View file

@ -4,37 +4,25 @@
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 aba2sat::{
aba::{
self,
problems::{
admissibility::{
DecideCredulousAdmissibility, EnumerateAdmissibleExtensions,
SampleAdmissibleExtension, VerifyAdmissibleExtension,
},
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
},
complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
Num,
},
Num,
Error,
};
use aba2sat::{parser, Result};
use args::ARGS;
use clap::Parser;
use crate::error::{Error, Result};
#[cfg(test)]
macro_rules! set {
($($elem:expr),*) => {{
vec![$($elem),*].into_iter().collect()
}}
}
mod aba;
mod args;
mod clauses;
mod error;
mod literal;
mod mapper;
mod parser;
#[cfg(test)]
mod tests;
trait IccmaFormattable {
fn fmt_iccma(&self) -> Result<String>;
@ -56,24 +44,36 @@ fn __main() -> Result {
assumptions: set.iter().cloned().collect(),
},
aba,
args.max_loops,
)?
.fmt_iccma(),
args::Problems::EnumerateAdmissibility => aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba,
args.max_loops,
)?
.fmt_iccma(),
args::Problems::EnumerateAdmissibility => {
aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)?
.fmt_iccma()
}
args::Problems::SampleAdmissibility => {
aba::problems::solve(SampleAdmissibleExtension, aba)?.fmt_iccma()
}
args::Problems::DecideCredulousAdmissibility { query } => {
aba::problems::solve(DecideCredulousAdmissibility { element: *query }, aba)?.fmt_iccma()
}
args::Problems::EnumerateComplete => {
aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), aba)?.fmt_iccma()
}
args::Problems::DecideCredulousComplete { query } => {
aba::problems::solve(DecideCredulousComplete { element: *query }, aba)?.fmt_iccma()
aba::problems::solve(SampleAdmissibleExtension, aba, args.max_loops)?.fmt_iccma()
}
args::Problems::DecideCredulousAdmissibility { query } => aba::problems::solve(
DecideCredulousAdmissibility { element: *query },
aba,
args.max_loops,
)?
.fmt_iccma(),
args::Problems::EnumerateComplete => aba::problems::multishot_solve(
EnumerateCompleteExtensions::default(),
aba,
args.max_loops,
)?
.fmt_iccma(),
args::Problems::DecideCredulousComplete { query } => aba::problems::solve(
DecideCredulousComplete { element: *query },
aba,
args.max_loops,
)?
.fmt_iccma(),
}?;
let mut stdout = std::io::stdout().lock();
match writeln!(stdout, "{}", result) {

11
src/tests/mod.rs
View file

@ -43,6 +43,7 @@ fn simple_conflict_free_verification() {
assumptions: translated,
},
aba.aba().clone(),
None
)
.unwrap();
assert!(
@ -67,7 +68,7 @@ fn simple_admissible_verification() {
eprintln!("Checking set {assumptions:?}");
let translated= aba.forward_set(assumptions.clone()).unwrap();
let result =
crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: translated }, aba.aba().clone()).unwrap();
crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: translated }, aba.aba().clone(), None).unwrap();
assert!(
result == expectation,
"Expected {expectation} from solver, but got {result} while checking {assumptions:?}"
@ -82,6 +83,7 @@ fn simple_admissible_example() {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
None,
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
@ -113,6 +115,7 @@ fn simple_admissible_example_with_defense() {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
None,
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
@ -143,6 +146,7 @@ fn simple_admissible_atomic() {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
None,
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
@ -173,6 +177,7 @@ fn a_chain_with_no_beginning() {
let result = crate::aba::problems::multishot_solve(
EnumerateAdmissibleExtensions::default(),
aba.aba().clone(),
None,
)
.unwrap();
for elem in aba.forward_sets(expected.clone()).unwrap() {
@ -199,7 +204,7 @@ fn loops_and_conflicts() {
.with_rule('d', ['b']);
let element = aba.forward_atom('d').unwrap();
let result =
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone())
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone(), None)
.unwrap();
assert!(!result, "d cannot be credulous complete");
}
@ -214,7 +219,7 @@ fn loops_and_conflicts_2() {
.with_rule('d', ['a']);
let element = aba.forward_atom('b').unwrap();
let result =
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone())
crate::aba::problems::solve(DecideCredulousComplete { element }, aba.aba().clone(), None)
.unwrap();
assert!(result, "b is credulous complete");
}