From 37997ee9c7d1ff4b2b23f341219c0d39d91622ba Mon Sep 17 00:00:00 2001
From: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
Date: Fri, 2 Jul 2021 15:01:39 +0200
Subject: [PATCH] added naive and incomplete version of complete semantics

Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
---
 src/adf.rs  | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++--
 src/main.rs | 26 +++++++++++++++++++++++---
 2 files changed, 74 insertions(+), 5 deletions(-)

diff --git a/src/adf.rs b/src/adf.rs
index 958aeee..c1d9138 100644
--- a/src/adf.rs
+++ b/src/adf.rs
@@ -118,6 +118,55 @@ impl Adf {
         interpretation
     }
 
+    pub fn complete(&mut self) -> Vec<Vec<usize>> {
+        let base_int = self.cur_interpretation();
+        let mut complete: Vec<Vec<usize>> = Vec::new();
+        let mut change:bool;
+        let mut pos:usize=0;
+        let mut cache:HashMap<Vec<usize>,usize> = HashMap::new();
+
+        // compute grounded interpretation
+        complete.push(self.to_fixpoint(base_int.as_ref()).unwrap());
+        loop{
+            change = false;
+            let interpr = complete.get(pos).unwrap().clone();
+            for (pos, it) in interpr.iter().enumerate(){
+                if *it > 1 {
+                    let mut int1 = interpr.clone();
+                    int1[pos] = 0;
+                    match self.to_fixpoint(int1.as_ref()){
+                        Some(n) => {
+                            if !cache.contains_key(&n){
+                                cache.insert(n.clone(), complete.len());
+                                complete.push(n);
+                                change = true;
+                            }
+                        },
+                        None => (),
+                    }
+                    int1[pos] = 1;
+                    match self.to_fixpoint(int1.as_ref()){
+                        Some(n) => {
+                            if !cache.contains_key(&n){
+                                cache.insert(n.clone(), complete.len());
+                                complete.push(n);
+                                change = true;
+                            }
+                        },
+                        None => (),
+                    }
+
+                }
+            }
+            if !change {break};
+            pos += 1;
+           // println!("{}",complete.len());
+            
+        }
+        complete
+    }
+
+    /// represents the starting interpretation due to the acceptance conditions. (i.e. the currently represented set of formulae)
     pub fn cur_interpretation(&self) -> Vec<usize>{
         let mut interpretation: Vec<usize> = Vec::new();
         for it in self.stmts.iter(){
@@ -126,12 +175,12 @@ impl Adf {
         interpretation
     }
 
-    pub fn to_fixpoint(&mut self, interpretation:Vec<usize>) -> Option<Vec<usize>>{
+    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);
+                    return self.to_fixpoint(new_interpretation.as_ref());
                 }else{
                     return Some(new_interpretation)
                 }
diff --git a/src/main.rs b/src/main.rs
index 0db2d5d..b2898f1 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -64,11 +64,11 @@ fn main() {
 
         let mut my_adf2 = Adf::default();
         my_adf2.init_statements(statements.iter().map(AsRef::as_ref).collect());
-        for (s, c) in ac {
+        for (s, c) in ac.clone() {
             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();
+        let result2 = my_adf2.to_fixpoint(empty_int.as_ref()).unwrap();
         //   for (p, s) in statements.iter().enumerate() {
         //     match result2[p] {
         //         0 => print!("f("),
@@ -77,8 +77,23 @@ fn main() {
         //     }
         //     println!("{}) ", *s);
         // }
+
+        
         print_interpretation(result2);
         println!("finished after {}ms", start_fp.elapsed().as_millis());
+
+        // optional test of complete extensions
+        // let mut my_adf3 = Adf::default();
+        // my_adf3.init_statements(statements.iter().map(AsRef::as_ref).collect());
+        // for (s, c) in ac.clone() {
+        //     my_adf3.add_ac(s.as_str(), c.as_str());
+        // }
+
+        // let result3 = my_adf3.complete();
+        // for it in result3.iter() {
+        //     print_interpretation(it.to_vec());
+        // }
+        // println!("{}",result3.len());
     }
 }
 
@@ -91,12 +106,17 @@ where
 }
 
 fn print_interpretation(interpretation: Vec<usize>) {
+    let mut stable = true;
     for it in interpretation.iter() {
         match *it {
             0 => print!("f"),
             1 => print!("t"),
-            _ => print!("u"),
+            _ => {print!("u");stable=false},
         }
     }
+    if stable {
+        println!(" stm");
+    }else{
     println!("");
 }
+}