ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00
Code Issues Projects Releases Wiki Activity

Try stable nogood for iccma binary

Browse Source
This commit is contained in:
monsterkrampe 2025-04-09 15:54:43 +02:00
parent 97b27d1251
commit 677533e998
No known key found for this signature in database
GPG Key ID: B8ADC1F5A5CE5057
2 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
iccma-2025-bin/src/main.rs
View File

@ -185,7 +185,7 @@ fn main() {
let printer = adf.print_dictionary(); let printer = adf.print_dictionary();
if let Some(fst) = target_var.and_then(|tv| { if let Some(fst) = target_var.and_then(|tv| {
adf.stable().find(|m| { adf.stable_nogood(Default::default()).find(|m| {
let term = m[tv.value()]; let term = m[tv.value()];
term.is_truth_value() && term.is_true() term.is_truth_value() && term.is_true()
}) })
@ -238,7 +238,7 @@ fn main() {
let query: usize = app.query.expect("Query is required for current task."); let query: usize = app.query.expect("Query is required for current task.");
let target_var = adf.ordering.variable(&query.to_string()); let target_var = adf.ordering.variable(&query.to_string());
let printer = adf.print_dictionary(); let printer = adf.print_dictionary();
let mut models = adf.stable(); let mut models = adf.stable_nogood(Default::default());
let witness = if let Some(tv) = target_var { let witness = if let Some(tv) = target_var {
models.find(|m| { models.find(|m| {
@ -287,7 +287,7 @@ fn main() {
} }
Task::SeSt => { Task::SeSt => {
let printer = adf.print_dictionary(); let printer = adf.print_dictionary();
let mut models = adf.stable(); let mut models = adf.stable_nogood(Default::default());
if let Some(fst) = models.next() { if let Some(fst) = models.next() {
println!("w {}", printer.print_truthy_statements(&fst).join(" ")); println!("w {}", printer.print_truthy_statements(&fst).join(" "));
} else { } else {

4
lib/src/adf.rs
View File

@ -787,7 +787,9 @@ impl Adf {
let grounded = self.grounded(); let grounded = self.grounded();
let heu = heuristic.get_heuristic(); let heu = heuristic.get_heuristic();
let (s, r) = crossbeam_channel::unbounded::<Vec<Term>>(); let (s, r) = crossbeam_channel::unbounded::<Vec<Term>>();
self.stable_nogood_get_vec(&grounded, heu, s, r).into_iter() // self.stable_nogood_get_vec(&grounded, heu, s, r).into_iter()
self.nogood_internal(&grounded, heu, Self::stability_check, s);
r.into_iter()
} }
/// Computes the stable extension of a given [`Adf`], using the [`NoGood`]-learner. /// Computes the stable extension of a given [`Adf`], using the [`NoGood`]-learner.