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

computing grounded with a shortcut and a "normal" computation

Browse Source 
shortcut is slighty faster, has in all tested instances the same result.

Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
This commit is contained in:
Stefan Ellmauthaler 2021-06-30 16:05:15 +02:00
parent c424d0222a
commit b566837593
2 changed files with 142 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
src/adf.rs
View File

@ -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<usize>{
let mut interpretation: Vec<usize> = Vec::new();
for it in self.stmts.iter(){
interpretation.push((*it).ac.unwrap())
}
interpretation
}
pub fn to_fixpoint(&mut self, interpretation:Vec<usize>) -> Option<Vec<usize>>{
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<usize>) -> Vec<usize>{
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<usize>,i2:&Vec<usize>) -> Option<bool> {
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<usize>, var:usize, val:bool) -> Option<Vec<usize>>{
let mut interpretation2:Vec<usize> = vec![0;interpretation.len()];
let mut change: bool = false;

125
src/main.rs
View File

@ -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<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 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<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 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<P>(filename: P) -> io::Result<io::Lines<io::BufReader<File>>>
where P: AsRef<Path>, {
where
P: AsRef<Path>,
{
let file = File::open(filename)?;
Ok(io::BufReader::new(file).lines())
}
fn print_interpretation(interpretation: Vec<usize>) {
for it in interpretation.iter() {
match *it {
0 => print!("f"),
1 => print!("t"),
_ => print!("u"),
}
}
println!("");
}