diff --git a/src/adf.rs b/src/adf.rs index 6c3d527..958aeee 100644 --- a/src/adf.rs +++ b/src/adf.rs @@ -1,7 +1,4 @@ -use std::{ - collections::HashMap, - str::{self, FromStr}, -}; +use std::{collections::HashMap, str::{self, FromStr}, usize}; use super::obdd::Bdd; @@ -121,6 +118,64 @@ impl Adf { interpretation } + pub fn cur_interpretation(&self) -> Vec{ + let mut interpretation: Vec = Vec::new(); + for it in self.stmts.iter(){ + interpretation.push((*it).ac.unwrap()) + } + interpretation + } + + pub fn to_fixpoint(&mut self, interpretation:Vec) -> Option>{ + let new_interpretation = self.apply_interpretation(interpretation.as_ref()); + match Adf::information_enh(interpretation.as_ref(), new_interpretation.as_ref()){ + Some(n) => { + if n { + return self.to_fixpoint(new_interpretation); + }else{ + return Some(new_interpretation) + } + }, + None => None, + } + } + + fn apply_interpretation(&mut self, interpretation:&Vec) -> Vec{ + let mut new_interpretation = interpretation.clone(); + for (pos,it) in interpretation.iter().enumerate(){ + match *it { + super::obdd::BDD_BOT => { + if let Some(n) = self.setvarvalue(new_interpretation.clone(),self.bdd.nodes[self.stmts[pos].var].var(),false){ + new_interpretation.clone_from(&n); + + } + }, + super::obdd::BDD_TOP => { + if let Some(n) = self.setvarvalue(new_interpretation.clone(),self.bdd.nodes[self.stmts[pos].var].var(),true){ + new_interpretation.clone_from(&n); + } + }, + _ => (), + } + + } + new_interpretation + } + + fn information_enh(i1:&Vec,i2:&Vec) -> Option { + let mut enhanced = false; + for i in 0..i1.len(){ + if i1[i] < 2{ + if i1[i] != i2[i] { + return None; + } + } else if (i1[i]>=2) & (i2[i] < 2){ + enhanced = true; + } + } + Some(enhanced) + } + fn setvarvalue(&mut self,interpretation:Vec, var:usize, val:bool) -> Option>{ let mut interpretation2:Vec = vec![0;interpretation.len()]; let mut change: bool = false; diff --git a/src/main.rs b/src/main.rs index 12e1e0b..0db2d5d 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,63 +1,102 @@ -use std::{env, process::exit}; use std::fs::File; use std::io::{self, BufRead}; use std::path::Path; +use std::time::Instant; +use std::usize; +use std::{env, process::exit}; -pub mod obdd; pub mod adf; +pub mod obdd; use adf::Adf; fn main() { - let args:Vec = env::args().collect(); - if args.len() != 2 { - eprintln!("No Filename given"); - exit(1); - } - let mut statements: Vec = 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 line in lines.flatten() { - //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(Adf::findterm_str(line.strip_prefix("s(").unwrap()).replace(" ", "")); + let start_time = Instant::now(); + let args: Vec = env::args().collect(); + if args.len() != 2 { + eprintln!("No Filename given"); + exit(1); + } + let mut statements: Vec = 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 line in lines.flatten() { + //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(Adf::findterm_str(line.strip_prefix("s(").unwrap()).replace(" ", "")); + } else if line.starts_with("ac(") { + let (s, c) = Adf::findpairs(line.strip_prefix("ac(").unwrap()); + ac.push((s.replace(" ", ""), c.replace(" ", ""))); + } + //} } - else if line.starts_with("ac("){ - let (s,c) = Adf::findpairs(line.strip_prefix("ac(").unwrap()); - ac.push((s.replace(" ",""),c.replace(" ", ""))); + } + + let file_read = start_time.elapsed(); + let start_shortcut = Instant::now(); + + println!("parsed {} statements after {}ms", statements.len(), file_read.as_millis()); + if !statements.is_empty() && !ac.is_empty() { + let mut my_adf = Adf::new(); + my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect()); + for (s, c) in ac.clone() { + my_adf.add_ac(s.as_str(), c.as_str()); } - //} - } - } - println!("parsed {} statements", statements.len()); - if !statements.is_empty() && !ac.is_empty() { - let mut my_adf = Adf::new(); - my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect()); - for (s,c) in ac { - my_adf.add_ac(s.as_str(), c.as_str()); - } + let result = my_adf.grounded(); + //println!("{:?}",result); + // for (p, s) in statements.iter().enumerate() { + // match result[p] { + // 0 => print!("f("), + // 1 => print!("t("), + // _ => print!("u("), + // } + // println!("{}) ", *s); + // } + print_interpretation(result); + println!("finished after {}ms", start_shortcut.elapsed().as_millis()); + let start_fp = Instant::now(); - let result = my_adf.grounded(); - println!("{:?}",result); - for (p,s) in statements.iter().enumerate(){ - match result[p] { - 0 => print!("f("), - 1 => print!("t("), - _ => print!("u("), - } - print!("{}) ",*s); + let mut my_adf2 = Adf::default(); + my_adf2.init_statements(statements.iter().map(AsRef::as_ref).collect()); + for (s, c) in ac { + my_adf2.add_ac(s.as_str(), c.as_str()); + } + let empty_int = my_adf2.cur_interpretation().to_owned(); + let result2 = my_adf2.to_fixpoint(empty_int).unwrap(); + // for (p, s) in statements.iter().enumerate() { + // match result2[p] { + // 0 => print!("f("), + // 1 => print!("t("), + // _ => print!("u("), + // } + // println!("{}) ", *s); + // } + print_interpretation(result2); + println!("finished after {}ms", start_fp.elapsed().as_millis()); } - - } } fn read_lines

(filename: P) -> io::Result>> -where P: AsRef, { +where + P: AsRef, +{ let file = File::open(filename)?; Ok(io::BufReader::new(file).lines()) -} \ No newline at end of file +} + +fn print_interpretation(interpretation: Vec) { + for it in interpretation.iter() { + match *it { + 0 => print!("f"), + 1 => print!("t"), + _ => print!("u"), + } + } + println!(""); +}