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

First fully running version of the prototype

Browse Source 
Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
This commit is contained in:
Stefan Ellmauthaler 2021-06-30 10:05:02 +02:00
parent b4f1dd263e
commit d4cbec0a76
4 changed files with 259 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
README.md
View File

@ -1,3 +1,20 @@
# OBDD - ordered binary decision diagram
# Prototype-solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams
## Abstract Dialectical Frameworks
An abstract dialectical framework (ADF) consists of abstract statements. Each statement has an unique label and might be related to other statements (s) in the ADF. This relation is defined by a so-called acceptance condition (ac), which intuitively is a propositional formula, where the variable symbols are the labels of the statements. An interpretation is a three valued function which maps to each statement a truth value (true, false, undecided). We call such an interpretation a model, if each acceptance condition agrees to the interpration.
## ordered Binary Decision Diagram
An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap.
## Input-file format:
Each statement is defined by an ASP-style unary predicate s, where the enclosed term represents the label of the statement.
The binary predicate ac relates each statement to one propositional formula in prefix notation, with the logical operations and constants as follows:
- and(x,y): conjunction
- or(x,y): disjunctin
- iff(x,Y): if and only if
- xor(x,y): exclusive or
- neg(x): classical negation
- c(v): constant symbol "verum" - tautology/top
- c(f): constant symbol "falsum" - inconsistency/bot
An ordered binary decision diagram is a normalised representation of binary functions, where satisfiability- and validity checks can be done relatively cheap.

209
src/adf.rs
View File

@ -27,7 +27,7 @@ impl Statement {
}
}
struct Adf {
pub struct Adf {
bdd: Bdd,
stmts: Vec<Statement>,
dict: HashMap<String, usize>, // label to pos in vec
@ -37,7 +37,7 @@ impl Adf {
pub fn new() -> Self {
Adf {
bdd: Bdd::new(),
stmts: Vec::new(),
stmts: Vec::new(),
dict: HashMap::new(),
}
}
@ -45,12 +45,19 @@ impl Adf {
fn add_statement(&mut self, statement: &str) {
if self.dict.get(statement).is_none() {
let pos = self.stmts.len();
//self.bdd.variable(pos);
//self.stmts
// .push(Statement::new(statement, pos.clone()));
self.stmts
.push(Statement::new(statement, self.bdd.variable(pos).clone()));
.push(Statement::new(statement, self.bdd.variable(pos).clone()));
self.dict.insert(self.stmts[pos].label.to_string(), pos);
}
}
/// Initialise statements
///
/// The order of statements given as a parameter will determine die ordering for the OBDD.
/// Note that only initialised statements will regocnised as variables later on
pub fn init_statements(&mut self, stmts: Vec<&str>) -> usize {
for i in stmts.iter() {
self.add_statement(*i);
@ -58,6 +65,9 @@ impl Adf {
self.stmts.len()
}
/// Adds to a given statement its acceptance condition.
///
/// This ac needs to be in the prefix notation for ADFs as defined by the DIAMOND implementation.
pub fn add_ac(&mut self, statement: &str, ac: &str) {
if let Some(stmt) = self.dict.get(statement) {
self.add_ac_by_number(*stmt, ac)
@ -73,49 +83,149 @@ impl Adf {
self.stmts[st].ac = Some(ac);
}
fn parseformula(&mut self, ac: &str) -> usize {
if let Some(split) = ac.find(',') {
let (l, r) = ac.split_at(split);
let rterm = self.parseformula(&r[1..r.len() - 1]);
if ac.starts_with("and(") {
let lterm = self.parseformula(&l[4..]);
self.bdd.and(lterm, rterm)
} else if ac.starts_with("or(") {
let lterm = self.parseformula(&l[3..]);
self.bdd.or(lterm, rterm)
} else if ac.starts_with("iff(") {
let lterm = self.parseformula(&l[4..]);
let neglterm = self.bdd.not(lterm);
let negrterm = self.bdd.not(rterm);
let con1 = self.bdd.and(lterm, rterm);
let con2 = self.bdd.and(neglterm, negrterm);
pub fn grounded(&mut self) -> Vec<usize> {
let mut interpretation: Vec<usize> = Vec::new();
let mut change:bool = false;
self.bdd.or(con1, con2)
} else {
//if ac.starts_with("xor("){
let lterm = self.parseformula(&l[4..]);
let neglterm = self.bdd.not(lterm);
let negrterm = self.bdd.not(rterm);
let con1 = self.bdd.and(neglterm, rterm);
let con2 = self.bdd.and(lterm, negrterm);
self.bdd.or(con1, con2)
}
} else {
if ac.starts_with("neg(") {
let term = self.parseformula(&ac[4..ac.len() - 1]);
self.bdd.not(term)
} else if ac.eq("c(v)") {
self.bdd.constant(true)
} else if ac.eq("c(f)") {
self.bdd.constant(false)
} else {
match self.dict.get(ac) {
Some(it) => self.stmts[*it].var,
_ => unreachable!(),
for it in self.stmts.iter(){
interpretation.push((*it).ac.unwrap())
}
loop{
change = false;
for pos in 0..self.stmts.len()-1{
let curint = interpretation.clone();
match curint[pos] {
super::obdd::BDD_BOT => {
if let Some(n) = self.setvarvalue(curint,self.bdd.nodes[self.stmts[pos].var].var(),false){
interpretation.clone_from(&n);
change = true;
}
},
super::obdd::BDD_TOP => {
if let Some(n) = self.setvarvalue(curint,self.bdd.nodes[self.stmts[pos].var].var(),true){
interpretation.clone_from(&n);
change = true;
}
},
_ => (),
}
}
if !change {break;}
println!("bla");
}
interpretation
}
fn setvarvalue(&mut self,interpretation:Vec<usize>, var:usize, val:bool) -> Option<Vec<usize>>{
let mut interpretation2:Vec<usize> = vec![0;interpretation.len()];
let mut change: bool = false;
for (pos,it) in interpretation.iter().enumerate(){
interpretation2[pos] = self.bdd.restrict(interpretation[pos], var, val);
if interpretation[pos] != interpretation2[pos]{
change = true
}
}
if change{
Some(interpretation2)
}else{
None
}
}
fn parseformula(&mut self, ac: &str) -> usize {
if ac.len() > 3 {
match &ac[..4] {
"and(" => {
let (left, right) = Adf::findpairs(&ac[4..]);
let lterm = self.parseformula(left);
let rterm = self.parseformula(right);
return self.bdd.and(lterm, rterm);
},
"iff(" => {
let (left, right) = Adf::findpairs(&ac[4..]);
let lterm = self.parseformula(left);
let rterm = self.parseformula(right);
let notlt = self.bdd.not(lterm);
let notrt = self.bdd.not(rterm);
let con1 = self.bdd.and(lterm, rterm);
let con2 = self.bdd.and(notlt,notrt);
return self.bdd.or(con1,con2);
},
"xor(" => {
let (left, right) = Adf::findpairs(&ac[4..]);
let lterm = self.parseformula(left);
let rterm = self.parseformula(right);
let notlt = self.bdd.not(lterm);
let notrt = self.bdd.not(rterm);
let con1 = self.bdd.and(notlt, rterm);
let con2 = self.bdd.and(lterm,notrt);
return self.bdd.or(con1,con2);
},
"neg(" => {
let pos = Adf::findterm(&ac[4..]).unwrap()+4;
let term = self.parseformula(&ac[4..pos]);
return self.bdd.not(term);
},
"c(f)" => return self.bdd.constant(false),
"c(v)" => return self.bdd.constant(true),
_ if &ac[..3] == "or(" => {
let (left, right) = Adf::findpairs(&ac[3..]);
let lterm = self.parseformula(left);
let rterm = self.parseformula(right);
return self.bdd.or(lterm, rterm);
},
_ => (),
}
}
match self.dict.get(ac) {
Some(it) => self.bdd.variable(*it),
_ => {println!("{}",ac); unreachable!()}
}
}
pub fn findpairs<'a>(formula: &'a str) -> (&'a str,&'a str){
let lpos = Adf::findterm(formula).unwrap();
let rpos = Adf::findterm(&formula[lpos+1..]).unwrap() + lpos;
(&formula[..lpos],&formula[lpos+1..rpos+1])
}
pub fn findterm_str<'a> (formula: &'a str) -> &'a str{
&formula[..Adf::findterm(formula).unwrap()]
}
fn findterm(formula: &str) -> Option<usize> {
let mut sqbrack: i16 = 0;
let mut cobrack: i16 = 0;
for (i,c) in formula.chars().enumerate() {
match c {
'(' => sqbrack += 1,
'[' => cobrack += 1,
',' => {
if sqbrack + cobrack == 0 {
return Some(i);
}
}
')' => {
if sqbrack > 0 {
sqbrack -= 1;
}else{
return Some(i);
}
}
']' => {
if cobrack > 0 {
cobrack -= 1;
}else{
return Some(i);
}
}
_ => (),
}
}
Some(formula.len())
}
}
@ -148,6 +258,8 @@ mod test {
assert_eq!(adf.parseformula("and(a,or(b,c))"), 6);
assert_eq!(adf.parseformula("xor(a,b)"), 11);
assert_eq!(adf.parseformula("or(c(f),b)"), 3); // is b
adf.parseformula("and(or(c(f),a),and(b,c))");
}
#[test]
@ -162,6 +274,19 @@ mod test {
adf.parseformula("and(a,or(b,d))");
}
#[test]
fn findterm() {
assert_eq!(Adf::findterm("formula"),Some(7));
assert_eq!(Adf::findterm("and(a,b),or(a,b)"),Some(8));
assert_eq!(Adf::findterm("neg(atom(a.d.ee))"),Some(17));
assert_eq!(Adf::findterm("formula)"),Some(7));
}
#[test]
fn findpairs() {
assert_eq!(Adf::findpairs("a,or(b,c))"),("a","or(b,c)"));
}
#[test]
fn init_statements() {
let mut adf = Adf::new();

64
src/main.rs Normal file
View File

@ -0,0 +1,64 @@
use std::borrow::Borrow;
use std::{env, process::exit};
use std::fs::File;
use std::io::{self, BufRead};
use std::path::Path;
pub mod obdd;
pub mod adf;
use adf::Adf;
fn main() {
let args:Vec<String> = env::args().collect();
if args.len() != 2 {
eprintln!("No Filename given");
exit(1);
}
let mut statements: Vec<String> = Vec::new();
let mut ac: Vec<(String,String)> = Vec::new();
let path = Path::new(args[1].as_str());
if let Ok(lines) = read_lines(path){
for resline in lines {
if let Ok(line) = resline {
//let slice = line.as_str();
if line.starts_with("s("){
// let slice = line.as_str();
// statements.push(Adf::findterm_str(&slice[2..]).clone());
statements.push(String::from(Adf::findterm_str(&line[2..]).replace(" ", "")));
}
else if line.starts_with("ac("){
let (s,c) = Adf::findpairs(&line[3..]);
ac.push((String::from(s.replace(" ","")),String::from(c.replace(" ", ""))));
}
}
}
}
println!("parsed {} statements", statements.len());
if statements.len() > 0 && ac.len() > 0 {
let mut myAdf = Adf::new();
myAdf.init_statements(statements.iter().map(AsRef::as_ref).collect());
for (s,c) in ac {
myAdf.add_ac(s.as_str(), c.as_str());
}
let result = myAdf.grounded();
println!("{:?}",result);
for (p,s) in statements.iter().enumerate(){
match result[p] {
0 => print!("f("),
1 => print!("t("),
_ => print!("u("),
}
print!("{}) ",*s);
}
}
}
fn read_lines<P>(filename: P) -> io::Result<io::Lines<io::BufReader<File>>>
where P: AsRef<Path>, {
let file = File::open(filename)?;
Ok(io::BufReader::new(file).lines())
}

12
src/obdd.rs
View File

@ -8,7 +8,7 @@ use std::collections::HashMap;
type Term = usize;
#[derive(Eq, PartialEq, Hash, Clone, Copy)]
struct BddNode {
pub (crate) struct BddNode {
var: usize,
lo: Term,
hi: Term,
@ -20,8 +20,14 @@ impl std::fmt::Display for BddNode {
}
}
impl BddNode{
pub fn var(self)->usize{
self.var
}
}
pub (crate) struct Bdd {
nodes: Vec<BddNode>,
pub (crate) nodes: Vec<BddNode>,
hash: HashMap<BddNode, Term>,
}
@ -79,7 +85,7 @@ impl Bdd {
}
}
fn restrict(&mut self, subtree: Term, var: usize, val: bool) -> Term {
pub fn restrict(&mut self, subtree: Term, var: usize, val: bool) -> Term {
let treenode = self.nodes[subtree];
if treenode.var > var || treenode.var == usize::MAX {
subtree