use aba for loop-finding, drop graph stuff
This commit is contained in:
parent
76dcb32dc5
commit
ef5f0606c0
144
Cargo.lock
generated
144
Cargo.lock
generated
|
|
@ -8,27 +8,11 @@ version = "0.1.0"
|
|||
dependencies = [
|
||||
"cadical",
|
||||
"clap",
|
||||
"graph-cycles",
|
||||
"iter_tools",
|
||||
"lazy_static",
|
||||
"nom",
|
||||
"petgraph",
|
||||
"thiserror",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ahash"
|
||||
version = "0.8.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"getrandom",
|
||||
"once_cell",
|
||||
"version_check",
|
||||
"zerocopy",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "anstream"
|
||||
version = "0.6.12"
|
||||
|
|
@ -102,12 +86,6 @@ dependencies = [
|
|||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "4.5.1"
|
||||
|
|
@ -155,18 +133,6 @@ version = "1.0.0"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
|
||||
|
||||
[[package]]
|
||||
name = "either"
|
||||
version = "1.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a"
|
||||
|
||||
[[package]]
|
||||
name = "equivalent"
|
||||
version = "1.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
|
||||
|
||||
[[package]]
|
||||
name = "errno"
|
||||
version = "0.3.8"
|
||||
|
|
@ -177,74 +143,12 @@ dependencies = [
|
|||
"windows-sys 0.52.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "fixedbitset"
|
||||
version = "0.4.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80"
|
||||
|
||||
[[package]]
|
||||
name = "getrandom"
|
||||
version = "0.2.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"wasi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "graph-cycles"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3a6ad932c6dd3cfaf16b66754a42f87bbeefd591530c4b6a8334270a7df3e853"
|
||||
dependencies = [
|
||||
"ahash",
|
||||
"petgraph",
|
||||
"thiserror",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "hashbrown"
|
||||
version = "0.14.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
|
||||
|
||||
[[package]]
|
||||
name = "heck"
|
||||
version = "0.4.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
|
||||
|
||||
[[package]]
|
||||
name = "indexmap"
|
||||
version = "2.2.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26"
|
||||
dependencies = [
|
||||
"equivalent",
|
||||
"hashbrown",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "iter_tools"
|
||||
version = "0.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "07a28265f753d634d09e32e5e38eb092fe003155ef6e32a0260906170a80eb48"
|
||||
dependencies = [
|
||||
"itertools",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
|
||||
dependencies = [
|
||||
"either",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "jobserver"
|
||||
version = "0.1.28"
|
||||
|
|
@ -294,22 +198,6 @@ dependencies = [
|
|||
"minimal-lexical",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "once_cell"
|
||||
version = "1.19.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92"
|
||||
|
||||
[[package]]
|
||||
name = "petgraph"
|
||||
version = "0.6.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9"
|
||||
dependencies = [
|
||||
"fixedbitset",
|
||||
"indexmap",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.78"
|
||||
|
|
@ -400,18 +288,6 @@ version = "0.2.1"
|
|||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||
|
||||
[[package]]
|
||||
name = "wasi"
|
||||
version = "0.11.0+wasi-snapshot-preview1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
|
||||
|
||||
[[package]]
|
||||
name = "windows-sys"
|
||||
version = "0.48.0"
|
||||
|
|
@ -543,23 +419,3 @@ name = "windows_x86_64_msvc"
|
|||
version = "0.52.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04"
|
||||
|
||||
[[package]]
|
||||
name = "zerocopy"
|
||||
version = "0.7.32"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be"
|
||||
dependencies = [
|
||||
"zerocopy-derive",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "zerocopy-derive"
|
||||
version = "0.7.32"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
|
|
|||
|
|
@ -12,9 +12,6 @@ default-run = "aba2sat"
|
|||
[dependencies]
|
||||
cadical = "0.1.14"
|
||||
clap = { version = "4.4.8", features = ["wrap_help", "derive"] }
|
||||
graph-cycles = "0.1.0"
|
||||
iter_tools = "0.10.0"
|
||||
lazy_static = "1.4.0"
|
||||
nom = "7.1.3"
|
||||
petgraph = "0.6.4"
|
||||
thiserror = "1.0.50"
|
||||
|
|
|
|||
|
|
@ -15,6 +15,8 @@ print_help_and_exit() {
|
|||
printf " The additional argument for the problem\n"
|
||||
printf " -f, --file\n"
|
||||
printf " The file containing the problem in ABA format\n"
|
||||
printf " -t, --time\n"
|
||||
printf " Execute hyperfine to determine runtimes\n"
|
||||
printf " --files-from\n"
|
||||
printf " Use the following dir to read files, specify a single file with --file instead\n"
|
||||
exit 1
|
||||
|
|
@ -41,22 +43,29 @@ run_dc_co() {
|
|||
print_help_and_exit "Parameter --file is missing!"
|
||||
fi
|
||||
printf "===== %s ==== " "$(basename "$ABA_FILE")"
|
||||
our_result=$("$ABA2SAT" --file "$ABA_FILE" dc-co --query "$ADDITIONAL_ARG" | tee "$OUTPUT_DIR/$(basename "$ABA_FILE")-aba2sat-result")
|
||||
our_result=$("$ABA2SAT" --max-loops 0 --file "$ABA_FILE" dc-co --query "$ADDITIONAL_ARG" | tee "$OUTPUT_DIR/$(basename "$ABA_FILE")-aba2sat-result")
|
||||
other_result=$("$ASPFORABA" --file "$ABA_FILE" --problem DC-CO --query "$ADDITIONAL_ARG" | tee "$OUTPUT_DIR/$(basename "$ABA_FILE")-aspforaba-result")
|
||||
$HYPERFINE --shell=none \
|
||||
--export-json "$JSON_FILE" \
|
||||
--command-name "aba2sat" \
|
||||
"$ABA2SAT --file \"$ABA_FILE\" dc-co --query \"$ADDITIONAL_ARG\"" \
|
||||
--command-name "aspforaba" \
|
||||
"$ASPFORABA --file \"$ABA_FILE\" --problem DC-CO --query \"$ADDITIONAL_ARG\"" 1>/dev/null 2>&1
|
||||
if [ "$our_result" != "$other_result" ]; then
|
||||
printf "❌\n"
|
||||
else
|
||||
printf "✅\n"
|
||||
fi
|
||||
printf "Argument: %s\n" "$ADDITIONAL_ARG"
|
||||
printf "Our: %3s %30s\n" "$our_result" "$(format_time "aba2sat" "$JSON_FILE")"
|
||||
printf "Their: %3s %30s\n" "$other_result" "$(format_time "aspforaba" "$JSON_FILE")"
|
||||
|
||||
if [ -n "$TIME_COMMANDS" ]; then
|
||||
$HYPERFINE --shell=none \
|
||||
--export-json "$JSON_FILE" \
|
||||
--command-name "aba2sat" \
|
||||
"$ABA2SAT --max-loops 0 --file \"$ABA_FILE\" dc-co --query \"$ADDITIONAL_ARG\"" \
|
||||
--command-name "aspforaba" \
|
||||
"$ASPFORABA --file \"$ABA_FILE\" --problem DC-CO --query \"$ADDITIONAL_ARG\"" 1>/dev/null 2>&1
|
||||
printf "Our: %3s %30s\n" "$our_result" "$(format_time "aba2sat" "$JSON_FILE")"
|
||||
printf "Their: %3s %30s\n" "$other_result" "$(format_time "aspforaba" "$JSON_FILE")"
|
||||
else
|
||||
printf "Our: %3s\n" "$our_result"
|
||||
printf "Their: %3s\n" "$other_result"
|
||||
fi
|
||||
|
||||
}
|
||||
|
||||
POSITIONAL_ARGS=()
|
||||
|
|
@ -68,6 +77,7 @@ ABA_FILE_EXT=aba
|
|||
HYPERFINE=hyperfine
|
||||
PROBLEM=
|
||||
ADDITIONAL_ARG=
|
||||
TIME_COMMANDS=
|
||||
|
||||
while [[ $# -gt 0 ]]; do
|
||||
case $1 in
|
||||
|
|
@ -111,6 +121,10 @@ while [[ $# -gt 0 ]]; do
|
|||
ADDITIONAL_ARG=$1
|
||||
shift
|
||||
;;
|
||||
-t | --time)
|
||||
shift
|
||||
TIME_COMMANDS=yes
|
||||
;;
|
||||
--aba2sat)
|
||||
shift
|
||||
ABA2SAT=$1
|
||||
|
|
|
|||
|
|
@ -31,12 +31,14 @@ use std::collections::{HashMap, HashSet};
|
|||
|
||||
use crate::literal::RawLiteral;
|
||||
|
||||
use self::prepared::PreparedAba;
|
||||
|
||||
pub mod debug;
|
||||
mod prepared;
|
||||
pub mod problems;
|
||||
mod theory;
|
||||
mod traverse;
|
||||
|
||||
pub use prepared::PreparedAba;
|
||||
pub use traverse::{loops_of, Loop, Loops};
|
||||
|
||||
pub type Rule = (Num, HashSet<Num>);
|
||||
pub type RuleList = Vec<Rule>;
|
||||
|
|
|
|||
|
|
@ -1,10 +1,7 @@
|
|||
use std::collections::{BTreeMap, HashSet};
|
||||
|
||||
use graph_cycles::Cycles;
|
||||
use iter_tools::Itertools;
|
||||
use std::collections::HashSet;
|
||||
|
||||
use crate::{
|
||||
aba::Num,
|
||||
aba::{traverse::loops_of, Num},
|
||||
clauses::Clause,
|
||||
literal::{
|
||||
lits::{LoopHelper, TheoryRuleBodyActive},
|
||||
|
|
@ -15,7 +12,7 @@ use crate::{
|
|||
use super::{theory::theory_helper, Aba, Context};
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||
struct r#Loop {
|
||||
struct Loop {
|
||||
heads: HashSet<Num>,
|
||||
support: Vec<usize>,
|
||||
}
|
||||
|
|
@ -23,14 +20,14 @@ struct r#Loop {
|
|||
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||
pub struct PreparedAba {
|
||||
aba: Aba,
|
||||
loops: Vec<r#Loop>,
|
||||
loops: Vec<Loop>,
|
||||
}
|
||||
|
||||
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);
|
||||
let loops = calculate_loops_and_their_support(&aba, max_loops).collect();
|
||||
PreparedAba { aba, loops }
|
||||
}
|
||||
/// Translate the ABA into base rules / definitions for SAT solving
|
||||
|
|
@ -167,64 +164,31 @@ fn trim_unreachable_rules(aba: &mut Aba) {
|
|||
});
|
||||
}
|
||||
|
||||
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()
|
||||
.unique()
|
||||
.scan(&mut graph, |graph, element| {
|
||||
let idx = graph.add_node(*element);
|
||||
Some((*element, idx))
|
||||
})
|
||||
.collect::<BTreeMap<_, _>>();
|
||||
aba.rules
|
||||
.iter()
|
||||
.flat_map(|(head, body)| body.iter().map(|body_element| (*body_element, *head)))
|
||||
.for_each(|(from, to)| {
|
||||
let from = universe.get(&from).unwrap();
|
||||
let to = universe.get(&to).unwrap();
|
||||
graph.update_edge(*from, *to, ());
|
||||
});
|
||||
#[cfg(debug_assertions)]
|
||||
{
|
||||
use std::{fs::File, io::Write};
|
||||
let mut file = File::create("./graph.gv").unwrap();
|
||||
let dot = petgraph::dot::Dot::with_config(&graph, &[petgraph::dot::Config::EdgeNoLabel]);
|
||||
write!(file, "{dot:?}").unwrap();
|
||||
}
|
||||
let mut loops = vec![];
|
||||
const LOOP_SIZE_IN_MULT_UNIVERSE_SIZE: f32 = 1.0;
|
||||
let max_loops = if let Some(max) = max_loops {
|
||||
max
|
||||
} else {
|
||||
(universe.len() as f32 * LOOP_SIZE_IN_MULT_UNIVERSE_SIZE) as usize
|
||||
};
|
||||
let mut output_printed = false;
|
||||
graph.visit_cycles(|graph, cycle| {
|
||||
let heads = cycle.iter().map(|idx| graph[*idx]).collect::<HashSet<_>>();
|
||||
let loop_rules = aba
|
||||
fn calculate_loops_and_their_support(
|
||||
aba: &Aba,
|
||||
max_loops: Option<usize>,
|
||||
) -> impl Iterator<Item = Loop> + '_ {
|
||||
let max_loops = max_loops.unwrap_or_else(|| aba.universe().collect::<HashSet<_>>().len());
|
||||
loops_of(aba).enumerate().map_while(move |(idx, l)| {
|
||||
if idx >= max_loops {
|
||||
eprintln!("Too many loops! {max_loops}");
|
||||
return None;
|
||||
}
|
||||
// Relevant rules are those that contain only elements from outside the loop
|
||||
// All other rules cannot influence the value of the loop
|
||||
let support = aba
|
||||
.rules
|
||||
.iter()
|
||||
.enumerate()
|
||||
.filter(|(_rule_id, (head, _body))| heads.contains(head));
|
||||
// Relevant rules are those that contain only elements from outside the loop
|
||||
// All other rules cannot influence the value of the loop
|
||||
let support = loop_rules
|
||||
.filter(|(_rule_id, (_head, body))| body.is_disjoint(&heads))
|
||||
.filter(|(_rule_id, (head, _body))| l.heads.contains(head))
|
||||
.filter(|(_rule_id, (_head, body))| body.is_disjoint(&l.heads))
|
||||
.map(|(rule_id, _)| rule_id)
|
||||
.collect();
|
||||
loops.push(r#Loop { heads, support });
|
||||
if loops.len() >= max_loops {
|
||||
if ! output_printed {
|
||||
eprintln!("Too... many... cycles... Aborting cycle detection with {} cycles. Solver? You're on your own now", loops.len());
|
||||
output_printed = true;
|
||||
}
|
||||
std::ops::ControlFlow::Break(())
|
||||
} else {
|
||||
std::ops::ControlFlow::Continue(())
|
||||
}
|
||||
});
|
||||
loops
|
||||
Some(Loop {
|
||||
heads: l.heads,
|
||||
support,
|
||||
})
|
||||
})
|
||||
}
|
||||
|
||||
impl std::ops::Deref for PreparedAba {
|
||||
|
|
|
|||
218
src/aba/traverse.rs
Normal file
218
src/aba/traverse.rs
Normal file
|
|
@ -0,0 +1,218 @@
|
|||
use std::collections::HashSet;
|
||||
|
||||
use super::{Aba, Num};
|
||||
|
||||
#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Ord, PartialOrd, Hash)]
|
||||
struct RuleIdx(usize);
|
||||
|
||||
impl RuleIdx {
|
||||
fn advance(&mut self) {
|
||||
self.0 += 1;
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Default, Clone, Copy, PartialEq, Eq, Ord, PartialOrd, Hash)]
|
||||
struct UniverseIdx(usize);
|
||||
|
||||
#[derive(Debug)]
|
||||
pub struct Loops<'a> {
|
||||
aba: &'a Aba,
|
||||
active: HashSet<Num>,
|
||||
rule_indices: Vec<RuleIdx>,
|
||||
found: Vec<Loop>,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq, Eq)]
|
||||
pub struct Loop {
|
||||
pub heads: HashSet<Num>,
|
||||
}
|
||||
|
||||
pub fn loops_of(aba: &Aba) -> Loops<'_> {
|
||||
let active = aba.assumptions().cloned().collect();
|
||||
Loops {
|
||||
aba,
|
||||
active,
|
||||
rule_indices: vec![RuleIdx(0)],
|
||||
found: vec![],
|
||||
}
|
||||
}
|
||||
|
||||
impl<'a> Iterator for Loops<'a> {
|
||||
type Item = Loop;
|
||||
|
||||
fn next(&mut self) -> Option<Self::Item> {
|
||||
loop {
|
||||
// Ensure that the rule_indices list is not empty, if it is, we're done
|
||||
if self.rule_indices.is_empty() {
|
||||
break None;
|
||||
}
|
||||
// Safe! We've exited already, if rule_indices is empty
|
||||
let rule_idx = self.rule_indices.last().unwrap();
|
||||
// Ensure that the rule_idx is valid, if it is not, backtrack
|
||||
if rule_idx.0 >= self.aba.rules.len() {
|
||||
// We're at the end of our rule list, backtrack
|
||||
self.rule_indices.pop();
|
||||
match self.rule_indices.last_mut() {
|
||||
Some(idx) => {
|
||||
let (head, _body) = &self.aba.rules[idx.0];
|
||||
self.active.remove(head);
|
||||
idx.advance();
|
||||
continue;
|
||||
}
|
||||
None => {
|
||||
// We popped the last rule, iterator ends here
|
||||
break None;
|
||||
}
|
||||
}
|
||||
}
|
||||
// Ensure that the rule_idx does not point to a rule that has been applied already
|
||||
if self.rule_indices[0..self.rule_indices.len() - 1].contains(rule_idx) {
|
||||
// The rule was applied before
|
||||
self.rule_indices.last_mut().unwrap().advance();
|
||||
continue;
|
||||
}
|
||||
// Ensure causality
|
||||
if self.rule_indices.len() >= 2 {
|
||||
// There was a rule before this one, ensure that the causality works
|
||||
// i.e. the next rule should contain the head of the last rule
|
||||
let last_rule_idx = self.rule_indices[self.rule_indices.len() - 2];
|
||||
let (last_rule_head, _) = self.aba.rules[last_rule_idx.0];
|
||||
if !self.aba.rules[rule_idx.0].1.contains(&last_rule_head) {
|
||||
self.rule_indices.last_mut().unwrap().advance();
|
||||
continue;
|
||||
}
|
||||
}
|
||||
// Still rules to try
|
||||
let (head, body) = &self.aba.rules[rule_idx.0];
|
||||
if body.is_subset(&self.active) {
|
||||
// The rule can be applied
|
||||
if self.active.contains(head) {
|
||||
// The rule head is already active, loop found!
|
||||
let heads = self.rule_indices[0..self.rule_indices.len() - 1]
|
||||
.iter()
|
||||
.rev()
|
||||
.map_while(|rule_idx| {
|
||||
let (old_head, _body) = &self.aba.rules[rule_idx.0];
|
||||
if *old_head != *head {
|
||||
Some(*old_head)
|
||||
} else {
|
||||
None
|
||||
}
|
||||
})
|
||||
// Add the current head to the loop, as it is not in the active list
|
||||
.chain(std::iter::once(*head))
|
||||
.collect();
|
||||
// Advance the rule index for the next call
|
||||
// Safe! No adjustment to the rule_indices since the last check at the start of the loop
|
||||
self.rule_indices.last_mut().unwrap().advance();
|
||||
let new_loop = Loop { heads };
|
||||
if !self.found.contains(&new_loop) {
|
||||
self.found.push(new_loop.clone());
|
||||
break Some(new_loop);
|
||||
} else {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
// The rule could be applied and does not cause a conflict
|
||||
// Go one level deeper
|
||||
self.rule_indices.push(RuleIdx(0));
|
||||
self.active.insert(*head);
|
||||
} else {
|
||||
self.rule_indices.last_mut().unwrap().advance();
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use crate::aba::debug::DebugAba;
|
||||
|
||||
use super::*;
|
||||
|
||||
#[test]
|
||||
fn no_loops() {
|
||||
let aba = Aba::default();
|
||||
let loops = loops_of(&aba).count();
|
||||
assert_eq!(loops, 0);
|
||||
|
||||
let mut loops = loops_of(&aba);
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn a_single_loop() {
|
||||
let aba = DebugAba::default()
|
||||
.with_assumption('a', 'q')
|
||||
.with_rule('p', ['q'])
|
||||
.with_rule('q', ['p'])
|
||||
.with_rule('p', ['a']);
|
||||
let the_loop = aba.forward_set(['p', 'q'].into_iter().collect()).unwrap();
|
||||
let loops = loops_of(aba.aba()).count();
|
||||
assert_eq!(loops, 1);
|
||||
|
||||
let mut loops = loops_of(&aba.aba());
|
||||
let first = loops.next().unwrap();
|
||||
assert_eq!(first.heads, the_loop);
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn two_loops() {
|
||||
let aba = DebugAba::default()
|
||||
.with_assumption('a', 'q')
|
||||
.with_rule('p', ['a'])
|
||||
.with_rule('q', ['p'])
|
||||
.with_rule('p', ['q'])
|
||||
.with_rule('r', ['q'])
|
||||
.with_rule('p', ['r']);
|
||||
let first_loop = aba.forward_set(['p', 'q'].into_iter().collect()).unwrap();
|
||||
let second_loop = aba
|
||||
.forward_set(['p', 'q', 'r'].into_iter().collect())
|
||||
.unwrap();
|
||||
let loops = loops_of(aba.aba()).count();
|
||||
assert_eq!(loops, 2);
|
||||
|
||||
let mut loops = loops_of(&aba.aba());
|
||||
let next = loops.next().unwrap();
|
||||
assert!(next.heads == first_loop || next.heads == second_loop);
|
||||
let next = loops.next().unwrap();
|
||||
assert!(next.heads == first_loop || next.heads == second_loop);
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn three_loops() {
|
||||
let aba = DebugAba::default()
|
||||
.with_assumption('a', 'q')
|
||||
.with_rule('p', ['a'])
|
||||
.with_rule('q', ['p'])
|
||||
.with_rule('p', ['q'])
|
||||
.with_rule('r', ['q'])
|
||||
.with_rule('p', ['r'])
|
||||
.with_rule('r', ['p']);
|
||||
let expected = [
|
||||
aba.forward_set(['p', 'q'].into_iter().collect()).unwrap(),
|
||||
aba.forward_set(['p', 'q', 'r'].into_iter().collect())
|
||||
.unwrap(),
|
||||
aba.forward_set(['p', 'r'].into_iter().collect()).unwrap(),
|
||||
];
|
||||
let mut loops = loops_of(&aba.aba());
|
||||
for _number in 0..expected.len() {
|
||||
let next = loops.next().unwrap();
|
||||
assert!(
|
||||
expected.contains(&next.heads),
|
||||
"Unexpected loop {:?}",
|
||||
next.heads
|
||||
);
|
||||
}
|
||||
// The iterator should be empty now
|
||||
assert!(matches!(loops.next(), None));
|
||||
assert!(matches!(loops.next(), None));
|
||||
}
|
||||
}
|
||||
|
|
@ -1,10 +1,5 @@
|
|||
use aba2sat::{
|
||||
aba::{Aba, Num},
|
||||
parser,
|
||||
};
|
||||
use graph_cycles::Cycles;
|
||||
use iter_tools::Itertools;
|
||||
use std::{collections::BTreeMap, path::PathBuf};
|
||||
use aba2sat::{aba::Aba, parser};
|
||||
use std::path::PathBuf;
|
||||
|
||||
use clap::{command, Parser};
|
||||
|
||||
|
|
@ -40,49 +35,9 @@ pub enum Error {
|
|||
}
|
||||
|
||||
fn count_loops(aba: &Aba, max_loops: Option<usize>) -> usize {
|
||||
let mut graph = petgraph::graph::DiGraph::<Num, ()>::new();
|
||||
let universe = aba
|
||||
.universe()
|
||||
.unique()
|
||||
.scan(&mut graph, |graph, element| {
|
||||
let idx = graph.add_node(*element);
|
||||
Some((*element, idx))
|
||||
})
|
||||
.collect::<BTreeMap<_, _>>();
|
||||
aba.rules
|
||||
.iter()
|
||||
.flat_map(|(head, body)| body.iter().map(|body_element| (*body_element, *head)))
|
||||
.for_each(|(from, to)| {
|
||||
let from = universe.get(&from).unwrap();
|
||||
let to = universe.get(&to).unwrap();
|
||||
graph.update_edge(*from, *to, ());
|
||||
});
|
||||
let mut loops = 0;
|
||||
let max_loops = if let Some(max) = max_loops {
|
||||
max
|
||||
} else {
|
||||
usize::MAX
|
||||
};
|
||||
let mut output_printed = false;
|
||||
graph.visit_cycles(|_graph, _cycle| {
|
||||
loops += 1;
|
||||
if loops % 100_000 == 0 {
|
||||
eprintln!("{loops}");
|
||||
}
|
||||
if loops >= max_loops {
|
||||
if !output_printed {
|
||||
eprintln!(
|
||||
"Too... many... cycles... Aborting cycle detection with {} cycles.",
|
||||
loops
|
||||
);
|
||||
output_printed = true;
|
||||
}
|
||||
std::ops::ControlFlow::Break(())
|
||||
} else {
|
||||
std::ops::ControlFlow::Continue(())
|
||||
}
|
||||
});
|
||||
loops
|
||||
aba2sat::aba::loops_of(aba)
|
||||
.take(max_loops.unwrap_or(usize::MAX))
|
||||
.count()
|
||||
}
|
||||
|
||||
fn __main() -> Result<(), Error> {
|
||||
|
|
@ -113,6 +68,7 @@ mod tests {
|
|||
pub fn one_loop() {
|
||||
let aba = DebugAba::default()
|
||||
.with_assumption('a', 'c')
|
||||
.with_rule('b', ['a'])
|
||||
.with_rule('b', ['c'])
|
||||
.with_rule('c', ['b']);
|
||||
assert_eq!(count_loops(aba.aba(), None), 1);
|
||||
|
|
|
|||
Loading…
Reference in a new issue