mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Implement Stable Models based on lazy evaluated iterators (#13)
Implements #12 * Implement Stable Models based on lazy evaluated iterators * Adjustment of the internal computation of the grounded interpretation * Update build.rs to replace "@" in test-instance names with "at" * Implement de-/serialization of the adf (in OBDD representation) in library * Adjust tests * Add more style-restrictions to compiler
This commit is contained in:
parent
a95f88dee4
commit
07d15167fe
45
Cargo.lock
generated
45
Cargo.lock
generated
@ -16,6 +16,8 @@ dependencies = [
|
|||||||
"predicates",
|
"predicates",
|
||||||
"quickcheck",
|
"quickcheck",
|
||||||
"quickcheck_macros",
|
"quickcheck_macros",
|
||||||
|
"serde",
|
||||||
|
"serde_json",
|
||||||
"test-log",
|
"test-log",
|
||||||
]
|
]
|
||||||
|
|
||||||
@ -269,6 +271,12 @@ dependencies = [
|
|||||||
"either",
|
"either",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "itoa"
|
||||||
|
version = "1.0.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "1aab8fc367588b89dcee83ab0fd66b72b50b72fa1904d7095045ace2b0c81c35"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "lazy_static"
|
name = "lazy_static"
|
||||||
version = "1.4.0"
|
version = "1.4.0"
|
||||||
@ -500,6 +508,12 @@ dependencies = [
|
|||||||
"winapi",
|
"winapi",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "ryu"
|
||||||
|
version = "1.0.9"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "73b4b750c782965c211b42f022f59af1fbceabdd026623714f104152f1ec149f"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "same-file"
|
name = "same-file"
|
||||||
version = "1.0.6"
|
version = "1.0.6"
|
||||||
@ -509,6 +523,37 @@ dependencies = [
|
|||||||
"winapi-util",
|
"winapi-util",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "serde"
|
||||||
|
version = "1.0.133"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "97565067517b60e2d1ea8b268e59ce036de907ac523ad83a0475da04e818989a"
|
||||||
|
dependencies = [
|
||||||
|
"serde_derive",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "serde_derive"
|
||||||
|
version = "1.0.133"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "ed201699328568d8d08208fdd080e3ff594e6c422e438b6705905da01005d537"
|
||||||
|
dependencies = [
|
||||||
|
"proc-macro2",
|
||||||
|
"quote",
|
||||||
|
"syn",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "serde_json"
|
||||||
|
version = "1.0.74"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "ee2bb9cd061c5865d345bb02ca49fcef1391741b672b54a0bf7b679badec3142"
|
||||||
|
dependencies = [
|
||||||
|
"itoa",
|
||||||
|
"ryu",
|
||||||
|
"serde",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "strsim"
|
name = "strsim"
|
||||||
version = "0.8.0"
|
version = "0.8.0"
|
||||||
|
|||||||
@ -1,6 +1,6 @@
|
|||||||
[package]
|
[package]
|
||||||
name = "adf_bdd"
|
name = "adf_bdd"
|
||||||
version = "0.1.2"
|
version = "0.1.3"
|
||||||
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
|
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
|
||||||
edition = "2021"
|
edition = "2021"
|
||||||
repository = "https://github.com/ellmau/adf-obdd/"
|
repository = "https://github.com/ellmau/adf-obdd/"
|
||||||
@ -19,6 +19,8 @@ log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info
|
|||||||
env_logger = "0.9"
|
env_logger = "0.9"
|
||||||
nom = "7.1.0"
|
nom = "7.1.0"
|
||||||
lexical-sort = "0.3.1"
|
lexical-sort = "0.3.1"
|
||||||
|
serde = { version = "1.0", features = ["derive","rc"] }
|
||||||
|
serde_json = "1.0"
|
||||||
|
|
||||||
[dev-dependencies]
|
[dev-dependencies]
|
||||||
test-log = "0.2.*"
|
test-log = "0.2.*"
|
||||||
|
|||||||
1
build.rs
1
build.rs
@ -33,6 +33,7 @@ fn write_test(test_file: &mut File, file: &DirEntry) {
|
|||||||
let test_name = format!("{}", file.file_name().unwrap().to_string_lossy())
|
let test_name = format!("{}", file.file_name().unwrap().to_string_lossy())
|
||||||
.replace(".", "_")
|
.replace(".", "_")
|
||||||
.replace("-", "_")
|
.replace("-", "_")
|
||||||
|
.replace("@", "at")
|
||||||
.to_lowercase();
|
.to_lowercase();
|
||||||
let grounded_name = format!(
|
let grounded_name = format!(
|
||||||
"{}-grounded.txt",
|
"{}-grounded.txt",
|
||||||
|
|||||||
@ -1 +1 @@
|
|||||||
Subproject commit 322d7d44662450f25caa09c569b5f8362547907b
|
Subproject commit a5548233eca5ecd15e0a2113ab6759f6a4751b3f
|
||||||
186
src/adf.rs
186
src/adf.rs
@ -5,15 +5,18 @@
|
|||||||
//! - computing interpretations
|
//! - computing interpretations
|
||||||
//! - computing fixpoints
|
//! - computing fixpoints
|
||||||
//! - computing the least fixpoint by using a shortcut
|
//! - computing the least fixpoint by using a shortcut
|
||||||
|
use serde::{Deserialize, Serialize};
|
||||||
|
|
||||||
use crate::{
|
use crate::{
|
||||||
datatypes::{
|
datatypes::{
|
||||||
adf::{PrintableInterpretation, VarContainer},
|
adf::{PrintableInterpretation, TwoValuedInterpretationsIterator, VarContainer},
|
||||||
Term, Var,
|
Term, Var,
|
||||||
},
|
},
|
||||||
obdd::Bdd,
|
obdd::Bdd,
|
||||||
parser::{AdfParser, Formula},
|
parser::{AdfParser, Formula},
|
||||||
};
|
};
|
||||||
|
|
||||||
|
#[derive(Serialize, Deserialize, Debug)]
|
||||||
/// Representation of an ADF, with an ordering and dictionary of statement <-> number relations, a binary decision diagram, and a list of acceptance functions in Term representation
|
/// Representation of an ADF, with an ordering and dictionary of statement <-> number relations, a binary decision diagram, and a list of acceptance functions in Term representation
|
||||||
pub struct Adf {
|
pub struct Adf {
|
||||||
ordering: VarContainer,
|
ordering: VarContainer,
|
||||||
@ -101,26 +104,28 @@ impl Adf {
|
|||||||
|
|
||||||
/// Computes the grounded extension and returns it as a list
|
/// Computes the grounded extension and returns it as a list
|
||||||
pub fn grounded(&mut self) -> Vec<Term> {
|
pub fn grounded(&mut self) -> Vec<Term> {
|
||||||
log::info!("[Start] grounded");
|
let ac = &self.ac.clone();
|
||||||
let mut t_vals: usize =
|
self.grounded_internal(ac)
|
||||||
self.ac.iter().fold(
|
|
||||||
0,
|
|
||||||
|acc, elem| {
|
|
||||||
if elem.is_truth_value() {
|
|
||||||
acc + 1
|
|
||||||
} else {
|
|
||||||
acc
|
|
||||||
}
|
}
|
||||||
},
|
|
||||||
);
|
fn grounded_internal(&mut self, interpretation: &[Term]) -> Vec<Term> {
|
||||||
let mut new_interpretation = self.ac.clone();
|
log::info!("[Start] grounded");
|
||||||
|
let mut t_vals: usize = interpretation
|
||||||
|
.iter()
|
||||||
|
.filter(|elem| elem.is_truth_value())
|
||||||
|
.count();
|
||||||
|
let mut new_interpretation: Vec<Term> = interpretation.into();
|
||||||
loop {
|
loop {
|
||||||
|
let curr_interpretation = new_interpretation.clone();
|
||||||
let old_t_vals = t_vals;
|
let old_t_vals = t_vals;
|
||||||
for ac in new_interpretation
|
for ac in new_interpretation
|
||||||
.iter_mut()
|
.iter_mut()
|
||||||
.filter(|term| !term.is_truth_value())
|
.filter(|term| !term.is_truth_value())
|
||||||
{
|
{
|
||||||
*ac = self.ac.iter().enumerate().fold(*ac, |acc, (var, term)| {
|
*ac = curr_interpretation
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.fold(*ac, |acc, (var, term)| {
|
||||||
if term.is_truth_value() {
|
if term.is_truth_value() {
|
||||||
self.bdd.restrict(acc, Var(var), term.is_true())
|
self.bdd.restrict(acc, Var(var), term.is_true())
|
||||||
} else {
|
} else {
|
||||||
@ -131,6 +136,12 @@ impl Adf {
|
|||||||
t_vals += 1;
|
t_vals += 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
log::debug!(
|
||||||
|
"old-int: {:?}, {} constants",
|
||||||
|
curr_interpretation,
|
||||||
|
old_t_vals
|
||||||
|
);
|
||||||
|
log::debug!("new-int: {:?}, {} constants", new_interpretation, t_vals);
|
||||||
if t_vals == old_t_vals {
|
if t_vals == old_t_vals {
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
@ -139,6 +150,62 @@ impl Adf {
|
|||||||
new_interpretation
|
new_interpretation
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Computes the first `max_values` stable models
|
||||||
|
/// if max_values is 0, then all will be computed
|
||||||
|
pub fn stable(&mut self, max_values: usize) -> Vec<Vec<Term>> {
|
||||||
|
let grounded = self.grounded();
|
||||||
|
if max_values == 0 {
|
||||||
|
self.stable_iter(&grounded).collect()
|
||||||
|
} else {
|
||||||
|
self.stable_iter(&grounded)
|
||||||
|
.enumerate()
|
||||||
|
.take_while(|(idx, _elem)| *idx < max_values)
|
||||||
|
.map(|(_, elem)| elem)
|
||||||
|
.collect()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Computes the stable models
|
||||||
|
/// Returns an Iterator which contains all stable models
|
||||||
|
fn stable_iter<'a, 'b, 'c>(
|
||||||
|
&'a mut self,
|
||||||
|
grounded: &'b [Term],
|
||||||
|
) -> impl Iterator<Item = Vec<Term>> + 'c
|
||||||
|
where
|
||||||
|
'a: 'c,
|
||||||
|
'b: 'c,
|
||||||
|
{
|
||||||
|
TwoValuedInterpretationsIterator::new(grounded)
|
||||||
|
.map(|interpretation| {
|
||||||
|
let mut interpr = self.ac.clone();
|
||||||
|
for ac in interpr.iter_mut() {
|
||||||
|
*ac = interpretation
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.fold(*ac, |acc, (var, term)| {
|
||||||
|
if term.is_truth_value() && !term.is_true() {
|
||||||
|
self.bdd.restrict(acc, Var(var), false)
|
||||||
|
} else {
|
||||||
|
acc
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
let grounded_check = self.grounded_internal(&interpr);
|
||||||
|
log::debug!(
|
||||||
|
"grounded candidate\n{:?}\n{:?}",
|
||||||
|
interpretation,
|
||||||
|
grounded_check
|
||||||
|
);
|
||||||
|
(interpretation, grounded_check)
|
||||||
|
})
|
||||||
|
.filter(|(int, grd)| {
|
||||||
|
int.iter()
|
||||||
|
.zip(grd.iter())
|
||||||
|
.all(|(it, gr)| it.compare_inf(gr))
|
||||||
|
})
|
||||||
|
.map(|(int, _grd)| int)
|
||||||
|
}
|
||||||
|
|
||||||
/// creates a [PrintableInterpretation] for output purposes
|
/// creates a [PrintableInterpretation] for output purposes
|
||||||
pub fn print_interpretation<'a, 'b>(
|
pub fn print_interpretation<'a, 'b>(
|
||||||
&'a self,
|
&'a self,
|
||||||
@ -188,7 +255,31 @@ mod test {
|
|||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn complete() {
|
fn serialize() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).s(e).s(d).ac(d,iff(imp(a,b),c)).ac(e,xor(d,e)).";
|
||||||
|
|
||||||
|
parser.parse()(input).unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
|
||||||
|
let grounded = adf.grounded();
|
||||||
|
|
||||||
|
let serialized = serde_json::to_string(&adf).unwrap();
|
||||||
|
log::debug!("Serialized to {}", serialized);
|
||||||
|
let result = r#"{"ordering":{"names":["a","c","b","e","d"],"mapping":{"b":2,"a":0,"e":3,"c":1,"d":4}},"bdd":{"nodes":[{"var":18446744073709551614,"lo":0,"hi":0},{"var":18446744073709551615,"lo":1,"hi":1},{"var":0,"lo":0,"hi":1},{"var":1,"lo":0,"hi":1},{"var":2,"lo":0,"hi":1},{"var":3,"lo":0,"hi":1},{"var":4,"lo":0,"hi":1},{"var":0,"lo":1,"hi":0},{"var":0,"lo":1,"hi":4},{"var":1,"lo":1,"hi":0},{"var":2,"lo":1,"hi":0},{"var":1,"lo":10,"hi":4},{"var":0,"lo":3,"hi":11},{"var":3,"lo":1,"hi":0},{"var":4,"lo":1,"hi":0},{"var":3,"lo":6,"hi":14}],"cache":[[{"var":3,"lo":1,"hi":0},13],[{"var":3,"lo":6,"hi":14},15],[{"var":4,"lo":0,"hi":1},6],[{"var":0,"lo":0,"hi":1},2],[{"var":4,"lo":1,"hi":0},14],[{"var":2,"lo":0,"hi":1},4],[{"var":1,"lo":0,"hi":1},3],[{"var":0,"lo":1,"hi":4},8],[{"var":3,"lo":0,"hi":1},5],[{"var":0,"lo":1,"hi":0},7],[{"var":2,"lo":1,"hi":0},10],[{"var":0,"lo":3,"hi":11},12],[{"var":1,"lo":1,"hi":0},9],[{"var":1,"lo":10,"hi":4},11]]},"ac":[4,2,7,15,12]}"#;
|
||||||
|
let mut deserialized: Adf = serde_json::from_str(&result).unwrap();
|
||||||
|
assert_eq!(adf.ac, deserialized.ac);
|
||||||
|
let grounded_import = deserialized.grounded();
|
||||||
|
|
||||||
|
assert_eq!(grounded, grounded_import);
|
||||||
|
assert_eq!(
|
||||||
|
format!("{}", adf.print_interpretation(&grounded)),
|
||||||
|
format!("{}", deserialized.print_interpretation(&grounded_import))
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn grounded() {
|
||||||
let parser = AdfParser::default();
|
let parser = AdfParser::default();
|
||||||
parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).")
|
parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).")
|
||||||
.unwrap();
|
.unwrap();
|
||||||
@ -203,5 +294,70 @@ mod test {
|
|||||||
format!("{}", adf.print_interpretation(&result)),
|
format!("{}", adf.print_interpretation(&result)),
|
||||||
"T(a) u(b) u(c) u(d) F(e) T(f) \n"
|
"T(a) u(b) u(c) u(d) F(e) T(f) \n"
|
||||||
);
|
);
|
||||||
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()(
|
||||||
|
"s(a).s(b).s(c).s(d).s(e).ac(a,c(v)).ac(b,a).ac(c,b).ac(d,neg(c)).ac(e,and(a,d)).",
|
||||||
|
)
|
||||||
|
.unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
let result = adf.grounded();
|
||||||
|
assert_eq!(result, vec![Term(1), Term(1), Term(1), Term(0), Term(0)]);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn stable() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).")
|
||||||
|
.unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
adf.stable(0),
|
||||||
|
vec![vec![
|
||||||
|
Term::TOP,
|
||||||
|
Term::BOT,
|
||||||
|
Term::BOT,
|
||||||
|
Term::TOP,
|
||||||
|
Term::BOT,
|
||||||
|
Term::TOP
|
||||||
|
]]
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
adf.stable(10),
|
||||||
|
vec![vec![
|
||||||
|
Term::TOP,
|
||||||
|
Term::BOT,
|
||||||
|
Term::BOT,
|
||||||
|
Term::TOP,
|
||||||
|
Term::BOT,
|
||||||
|
Term::TOP
|
||||||
|
]]
|
||||||
|
);
|
||||||
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).ac(a,neg(b)).ac(b,neg(a)).").unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
|
||||||
|
assert_eq!(adf.stable(1), vec![vec![Term::BOT, Term::TOP]]);
|
||||||
|
assert_eq!(adf.stable(2), adf.stable(0));
|
||||||
|
assert_eq!(
|
||||||
|
adf.stable(0),
|
||||||
|
vec![vec![Term::BOT, Term::TOP], vec![Term::TOP, Term::BOT]]
|
||||||
|
);
|
||||||
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).ac(a,b).ac(b,a).").unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
|
||||||
|
assert_eq!(adf.stable(0), vec![vec![Term::BOT, Term::BOT]]);
|
||||||
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).ac(a,neg(a)).ac(b,a).").unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
|
||||||
|
let empty: Vec<Vec<Term>> = Vec::new();
|
||||||
|
assert_eq!(adf.stable(0), empty);
|
||||||
|
assert_eq!(adf.stable(99999), empty);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@ -1,9 +1,11 @@
|
|||||||
//! Repesentation of all needed ADF based datatypes
|
//! Repesentation of all needed ADF based datatypes
|
||||||
|
|
||||||
|
use serde::{Deserialize, Serialize};
|
||||||
use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc};
|
use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc};
|
||||||
|
|
||||||
use super::{Term, Var};
|
use super::{Term, Var};
|
||||||
|
|
||||||
|
#[derive(Serialize, Deserialize,Debug)]
|
||||||
pub(crate) struct VarContainer {
|
pub(crate) struct VarContainer {
|
||||||
names: Rc<RefCell<Vec<String>>>,
|
names: Rc<RefCell<Vec<String>>>,
|
||||||
mapping: Rc<RefCell<HashMap<String, usize>>>,
|
mapping: Rc<RefCell<HashMap<String, usize>>>,
|
||||||
@ -40,6 +42,7 @@ impl VarContainer {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/// A struct to print a representation, it will be instantiated by [Adf] by calling the method [`Adf::print_interpretation`].
|
/// A struct to print a representation, it will be instantiated by [Adf] by calling the method [`Adf::print_interpretation`].
|
||||||
|
#[derive(Debug)]
|
||||||
pub struct PrintableInterpretation<'a> {
|
pub struct PrintableInterpretation<'a> {
|
||||||
interpretation: &'a [Term],
|
interpretation: &'a [Term],
|
||||||
ordering: &'a VarContainer,
|
ordering: &'a VarContainer,
|
||||||
@ -76,6 +79,69 @@ impl Display for PrintableInterpretation<'_> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Provides an Iterator, which contains all two valued Interpretations, with respect to the given
|
||||||
|
/// 3-valued interpretation.
|
||||||
|
|
||||||
|
#[derive(Debug)]
|
||||||
|
pub struct TwoValuedInterpretationsIterator {
|
||||||
|
indexes: Vec<usize>,
|
||||||
|
current: Option<Vec<Term>>,
|
||||||
|
started: bool,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl TwoValuedInterpretationsIterator {
|
||||||
|
/// Creates a new iterable structure, which represents all two-valued interpretations wrt. the given 3-valued interpretation
|
||||||
|
pub fn new(term: &[Term]) -> Self {
|
||||||
|
let indexes = term
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.filter_map(|(idx, &v)| (!v.is_truth_value()).then(|| idx))
|
||||||
|
.rev()
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
let current = term
|
||||||
|
.iter()
|
||||||
|
.map(|&v| if !v.is_truth_value() { Term::BOT } else { v })
|
||||||
|
.collect::<Vec<_>>();
|
||||||
|
|
||||||
|
Self {
|
||||||
|
indexes,
|
||||||
|
started: false,
|
||||||
|
current: Some(current),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Iterator for TwoValuedInterpretationsIterator {
|
||||||
|
type Item = Vec<Term>;
|
||||||
|
|
||||||
|
fn next(&mut self) -> Option<Self::Item> {
|
||||||
|
if self.started {
|
||||||
|
if let Some(current) = &self.current {
|
||||||
|
if let Some((idx, &at)) = self
|
||||||
|
.indexes
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.find(|(_, &idx)| current[idx] == Term::BOT)
|
||||||
|
{
|
||||||
|
let mut result = current.clone();
|
||||||
|
result[at] = Term::TOP;
|
||||||
|
for &at in self.indexes[0..idx].iter() {
|
||||||
|
result[at] = Term::BOT;
|
||||||
|
}
|
||||||
|
log::trace!("{:?} -> {:?}", current, result);
|
||||||
|
self.current = Some(result);
|
||||||
|
} else {
|
||||||
|
self.current = None;
|
||||||
|
}
|
||||||
|
};
|
||||||
|
} else {
|
||||||
|
self.started = true;
|
||||||
|
}
|
||||||
|
|
||||||
|
self.current.clone()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod test {
|
mod test {
|
||||||
use super::*;
|
use super::*;
|
||||||
@ -84,4 +150,35 @@ mod test {
|
|||||||
let vc = VarContainer::default();
|
let vc = VarContainer::default();
|
||||||
assert_eq!(vc.variable("foo"), None);
|
assert_eq!(vc.variable("foo"), None);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn two_valued_interpretations() {
|
||||||
|
let testinterpretation = vec![Term::TOP, Term(22), Term::BOT, Term(12), Term::TOP];
|
||||||
|
let mut iter = TwoValuedInterpretationsIterator::new(&testinterpretation);
|
||||||
|
assert_eq!(
|
||||||
|
iter.next(),
|
||||||
|
Some(vec![Term::TOP, Term::BOT, Term::BOT, Term::BOT, Term::TOP])
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
iter.next(),
|
||||||
|
Some(vec![Term::TOP, Term::BOT, Term::BOT, Term::TOP, Term::TOP])
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
iter.next(),
|
||||||
|
Some(vec![Term::TOP, Term::TOP, Term::BOT, Term::BOT, Term::TOP])
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
iter.next(),
|
||||||
|
Some(vec![Term::TOP, Term::TOP, Term::BOT, Term::TOP, Term::TOP])
|
||||||
|
);
|
||||||
|
assert_eq!(iter.next(), None);
|
||||||
|
|
||||||
|
let testinterpretation = vec![Term(22), Term(12)];
|
||||||
|
let mut iter = TwoValuedInterpretationsIterator::new(&testinterpretation);
|
||||||
|
assert_eq!(iter.next(), Some(vec![Term::BOT, Term::BOT]));
|
||||||
|
assert_eq!(iter.next(), Some(vec![Term::BOT, Term::TOP]));
|
||||||
|
assert_eq!(iter.next(), Some(vec![Term::TOP, Term::BOT]));
|
||||||
|
assert_eq!(iter.next(), Some(vec![Term::TOP, Term::TOP]));
|
||||||
|
assert_eq!(iter.next(), None);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@ -1,12 +1,13 @@
|
|||||||
//! To represent a BDD, a couple of datatypes is needed.
|
//! To represent a BDD, a couple of datatypes is needed.
|
||||||
//! This module consists of all internally and externally used datatypes, such as
|
//! This module consists of all internally and externally used datatypes, such as
|
||||||
//! [Term], [Var], and [BddNode]
|
//! [Term], [Var], and [BddNode]
|
||||||
|
use serde::{Deserialize, Serialize};
|
||||||
use std::{fmt::Display, ops::Deref};
|
use std::{fmt::Display, ops::Deref};
|
||||||
|
|
||||||
/// Representation of a Term
|
/// Representation of a Term
|
||||||
/// Each Term is represented in a number ([usize]) and relates to a
|
/// Each Term is represented in a number ([usize]) and relates to a
|
||||||
/// Node in the decision diagram
|
/// Node in the decision diagram
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)]
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone, Serialize, Deserialize)]
|
||||||
pub struct Term(pub usize);
|
pub struct Term(pub usize);
|
||||||
|
|
||||||
impl Deref for Term {
|
impl Deref for Term {
|
||||||
@ -49,12 +50,17 @@ impl Term {
|
|||||||
pub fn is_true(&self) -> bool {
|
pub fn is_true(&self) -> bool {
|
||||||
*self == Self::TOP
|
*self == Self::TOP
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Returns true, if the Terms have the same information-value
|
||||||
|
pub fn compare_inf(&self, other: &Self) -> bool {
|
||||||
|
self.is_truth_value() == other.is_truth_value() && self.is_true() == other.is_true()
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Representation of Variables
|
/// Representation of Variables
|
||||||
/// Note that the algorithm only uses [usize] values to identify variables.
|
/// Note that the algorithm only uses [usize] values to identify variables.
|
||||||
/// The order of these values will be defining for the Variable order of the decision diagram.
|
/// The order of these values will be defining for the Variable order of the decision diagram.
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy, Serialize, Deserialize)]
|
||||||
pub struct Var(pub usize);
|
pub struct Var(pub usize);
|
||||||
|
|
||||||
impl Deref for Var {
|
impl Deref for Var {
|
||||||
@ -92,7 +98,7 @@ impl Var {
|
|||||||
///
|
///
|
||||||
/// Intuitively this is a binary tree structure, where the diagram is allowed to
|
/// Intuitively this is a binary tree structure, where the diagram is allowed to
|
||||||
/// pool same values to the same Node.
|
/// pool same values to the same Node.
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy, Serialize, Deserialize)]
|
||||||
pub(crate) struct BddNode {
|
pub(crate) struct BddNode {
|
||||||
var: Var,
|
var: Var,
|
||||||
lo: Term,
|
lo: Term,
|
||||||
@ -151,6 +157,18 @@ mod test {
|
|||||||
use quickcheck_macros::quickcheck;
|
use quickcheck_macros::quickcheck;
|
||||||
use test_log::test;
|
use test_log::test;
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn cmp() {
|
||||||
|
assert!(!Term::BOT.compare_inf(&Term::TOP));
|
||||||
|
assert!(!Term::TOP.compare_inf(&Term::BOT));
|
||||||
|
assert!(!Term::TOP.compare_inf(&Term(22)));
|
||||||
|
assert!(!Term(22).compare_inf(&Term::BOT));
|
||||||
|
assert!(Term(22).compare_inf(&Term(12323)));
|
||||||
|
assert!(Term::TOP.compare_inf(&Term::TOP));
|
||||||
|
assert!(Term::BOT.compare_inf(&Term::BOT));
|
||||||
|
assert!(Term(22).compare_inf(&Term(22)));
|
||||||
|
}
|
||||||
|
|
||||||
#[quickcheck]
|
#[quickcheck]
|
||||||
fn deref_display_from(value: usize) -> bool {
|
fn deref_display_from(value: usize) -> bool {
|
||||||
// from
|
// from
|
||||||
|
|||||||
@ -32,6 +32,8 @@
|
|||||||
//! ac(d,d).
|
//! ac(d,d).
|
||||||
//! ```
|
//! ```
|
||||||
#![deny(
|
#![deny(
|
||||||
|
missing_debug_implementations,
|
||||||
|
missing_copy_implementations,
|
||||||
missing_copy_implementations,
|
missing_copy_implementations,
|
||||||
trivial_casts,
|
trivial_casts,
|
||||||
trivial_numeric_casts,
|
trivial_numeric_casts,
|
||||||
|
|||||||
11
src/main.rs
11
src/main.rs
@ -23,6 +23,8 @@ fn main() {
|
|||||||
(@arg sort_lex: --lx "Sorts variables in a lexicographic manner")
|
(@arg sort_lex: --lx "Sorts variables in a lexicographic manner")
|
||||||
(@arg sort_alphan: --an "Sorts variables in an alphanumeric manner")
|
(@arg sort_alphan: --an "Sorts variables in an alphanumeric manner")
|
||||||
)
|
)
|
||||||
|
(@arg grounded: --grd "Compute the grounded model")
|
||||||
|
(@arg stable: --stm "Compute the stable models")
|
||||||
)
|
)
|
||||||
.get_matches_safe()
|
.get_matches_safe()
|
||||||
.unwrap_or_else(|e| match e.kind {
|
.unwrap_or_else(|e| match e.kind {
|
||||||
@ -75,7 +77,14 @@ fn main() {
|
|||||||
}
|
}
|
||||||
|
|
||||||
let mut adf = Adf::from_parser(&parser);
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
if matches.is_present("grounded") {
|
||||||
let grounded = adf.grounded();
|
let grounded = adf.grounded();
|
||||||
|
|
||||||
println!("{}", adf.print_interpretation(&grounded));
|
println!("{}", adf.print_interpretation(&grounded));
|
||||||
|
}
|
||||||
|
if matches.is_present("stable") {
|
||||||
|
let stable = adf.stable(1);
|
||||||
|
for model in stable {
|
||||||
|
println!("{}", adf.print_interpretation(&model));
|
||||||
|
}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
34
src/obdd.rs
34
src/obdd.rs
@ -1,10 +1,12 @@
|
|||||||
//! Represents an obdd
|
//! Represents an obdd
|
||||||
use crate::datatypes::*;
|
use crate::datatypes::*;
|
||||||
|
use serde::{Deserialize, Serialize};
|
||||||
use std::{cmp::min, collections::HashMap, fmt::Display};
|
use std::{cmp::min, collections::HashMap, fmt::Display};
|
||||||
|
|
||||||
#[derive(Debug)]
|
#[derive(Debug, Serialize, Deserialize)]
|
||||||
pub(crate) struct Bdd {
|
pub(crate) struct Bdd {
|
||||||
pub(crate) nodes: Vec<BddNode>,
|
pub(crate) nodes: Vec<BddNode>,
|
||||||
|
#[serde(with = "vectorize")]
|
||||||
cache: HashMap<BddNode, Term>,
|
cache: HashMap<BddNode, Term>,
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -226,3 +228,33 @@ mod test {
|
|||||||
assert_eq!(x, Term(2));
|
assert_eq!(x, Term(2));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// vectorize maps with non-standard keys
|
||||||
|
pub mod vectorize {
|
||||||
|
use serde::{Deserialize, Deserializer, Serialize, Serializer};
|
||||||
|
use std::iter::FromIterator;
|
||||||
|
|
||||||
|
/// Serialise into a Vector from a Map
|
||||||
|
pub fn serialize<'a, T, K, V, S>(target: T, ser: S) -> Result<S::Ok, S::Error>
|
||||||
|
where
|
||||||
|
S: Serializer,
|
||||||
|
T: IntoIterator<Item = (&'a K, &'a V)>,
|
||||||
|
K: Serialize + 'a,
|
||||||
|
V: Serialize + 'a,
|
||||||
|
{
|
||||||
|
let container: Vec<_> = target.into_iter().collect();
|
||||||
|
serde::Serialize::serialize(&container, ser)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Deserialize from a Vector to a Map
|
||||||
|
pub fn deserialize<'de, T, K, V, D>(des: D) -> Result<T, D::Error>
|
||||||
|
where
|
||||||
|
D: Deserializer<'de>,
|
||||||
|
T: FromIterator<(K, V)>,
|
||||||
|
K: Deserialize<'de>,
|
||||||
|
V: Deserialize<'de>,
|
||||||
|
{
|
||||||
|
let container: Vec<_> = serde::Deserialize::deserialize(des)?;
|
||||||
|
Ok(T::from_iter(container.into_iter()))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|||||||
@ -75,6 +75,7 @@ impl std::fmt::Debug for Formula<'_> {
|
|||||||
/// handed over to other structures without further storage needs.
|
/// handed over to other structures without further storage needs.
|
||||||
///
|
///
|
||||||
/// Note that the parser can be utilised by an [ADF][`crate::datatypes::adf::Adf`] to initialise it with minimal overhead.
|
/// Note that the parser can be utilised by an [ADF][`crate::datatypes::adf::Adf`] to initialise it with minimal overhead.
|
||||||
|
#[derive(Debug)]
|
||||||
pub struct AdfParser<'a> {
|
pub struct AdfParser<'a> {
|
||||||
namelist: Rc<RefCell<Vec<String>>>,
|
namelist: Rc<RefCell<Vec<String>>>,
|
||||||
dict: Rc<RefCell<HashMap<String, usize>>>,
|
dict: Rc<RefCell<HashMap<String, usize>>>,
|
||||||
@ -97,6 +98,7 @@ impl<'a, 'b> AdfParser<'b>
|
|||||||
where
|
where
|
||||||
'a: 'b,
|
'a: 'b,
|
||||||
{
|
{
|
||||||
|
#[allow(dead_code)]
|
||||||
fn parse_statements(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
fn parse_statements(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
||||||
move |input| {
|
move |input| {
|
||||||
let (rem, _) = many1(self.parse_statement())(input)?;
|
let (rem, _) = many1(self.parse_statement())(input)?;
|
||||||
|
|||||||
@ -46,21 +46,21 @@ fn runs() -> Result<(), Box<dyn std::error::Error>> {
|
|||||||
.stderr(predicate::str::contains("code: Eof"));
|
.stderr(predicate::str::contains("code: Eof"));
|
||||||
|
|
||||||
cmd = Command::cargo_bin("adf_bdd")?;
|
cmd = Command::cargo_bin("adf_bdd")?;
|
||||||
cmd.arg(file.path()).arg("-vv");
|
cmd.arg(file.path()).arg("-vv").arg("--grd");
|
||||||
cmd.assert().success().stdout(predicate::str::contains(
|
cmd.assert().success().stdout(predicate::str::contains(
|
||||||
"u(7) F(4) u(8) u(3) F(5) u(9) u(10) u(1) u(6) u(2)",
|
"u(7) F(4) u(8) u(3) F(5) u(9) u(10) u(1) u(6) u(2)",
|
||||||
));
|
));
|
||||||
|
|
||||||
cmd = Command::cargo_bin("adf_bdd")?;
|
cmd = Command::cargo_bin("adf_bdd")?;
|
||||||
cmd.arg(file.path()).arg("--lx").arg("-v");
|
cmd.arg(file.path()).arg("--lx").arg("-v").arg("--grd");
|
||||||
cmd.assert().success().stdout(predicate::str::contains(
|
cmd.assert().success().stdout(predicate::str::contains(
|
||||||
"u(1) u(10) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9)",
|
"u(1) u(10) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9)",
|
||||||
));
|
));
|
||||||
|
|
||||||
cmd = Command::cargo_bin("adf_bdd")?;
|
cmd = Command::cargo_bin("adf_bdd")?;
|
||||||
cmd.arg(file.path()).arg("--an");
|
cmd.arg(file.path()).arg("--an").arg("--grd").arg("--stm");
|
||||||
cmd.assert().success().stdout(predicate::str::contains(
|
cmd.assert().success().stdout(predicate::str::contains(
|
||||||
"u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10)",
|
"u(1) u(2) u(3) F(4) F(5) u(6) u(7) u(8) u(9) u(10) \n\n",
|
||||||
));
|
));
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|||||||
@ -14,7 +14,7 @@ fn {name}() {{
|
|||||||
let grounded = adf.grounded();
|
let grounded = adf.grounded();
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
format!("{{}}", adf.print_interpretation(&grounded)),
|
format!("{{}}", adf.print_interpretation(&grounded)),
|
||||||
expected_result.unwrap()
|
format!("{{}}\n",expected_result.unwrap())
|
||||||
);
|
);
|
||||||
}}
|
}}
|
||||||
|
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user