fix(rust): fix model checking output

example-files/simple/seminars.csv

@@ -0,0 +1,8 @@
+W Sem 0;2;W;
+W Sem 1;2;W;
+W Sem 2;2;W;
+W Sem 3;3;W;
+P Sem 0;2;P;
+P Sem 1;2;P;
+P Sem 2;2;P;
+P Sem 3;3;P;

example-files/simple/votes.csv

@@ -0,0 +1,5 @@
+Student 1;1;2;3;1;2;3;
+Student 2;3;2;1;1;2;3;
+Student 3;3;2;1;1;2;3;
+Student 4;3;2;1;1;2;3;
+Student 5;1;2;3;1;2;3;

rust/src/rism_model_checking/mod.rs

@@ -3,15 +3,15 @@ mod seminars;
 
 use std::ops::Add;
 use crate::constants::Points;
-use crate::types::{Seminar, Student, RismResult, SeminarType};
+use crate::types::{Seminar, Student, RismResult, SeminarType, Assignment};
 use z3::{Config, Context, Optimize, SatResult};
 use z3::ast::{Int, Bool, Ast};
 use crate::rism_model_checking::seminars::sort_votes_to_seminars;
 use crate::rism_model_checking::students::{votes_to_string_id, student_to_points_id, assert_student_votes, assert_student_points};
 
-pub fn run_model_check<'a>(students: &Vec<Student>, seminars: &Vec<Seminar>, points: Points) -> Option<RismResult<'a>> {
+pub fn run_model_check<'a>(students: &'a Vec<Student>, seminars: &'a Vec<Seminar>, points: Points) -> Option<RismResult<'a>> {
     z3::set_global_param("parallel.enable", "true");
-    
+
     let mut cfg = Config::new();
     cfg.set_model_generation(true);
     let ctx = Context::new(&cfg);
@@ -55,11 +55,11 @@ pub fn run_model_check<'a>(students: &Vec<Student>, seminars: &Vec<Seminar>, poi
     sort_votes_to_seminars(&votes, students, seminars)
         .iter()
         .for_each(|(seminar, votes)| {
-        let t: Vec<(&Bool, i32)> = votes.iter().map(|(_, b)| (*b, 1)).collect();
-        opt.assert(
-            &Bool::pb_le(&ctx,&*t,seminar.capacity as i32)
-        )
-    });
+            let t: Vec<(&Bool, i32)> = votes.iter().map(|(_, b)| (*b, 1)).collect();
+            opt.assert(
+                &Bool::pb_le(&ctx, &*t, seminar.capacity as i32)
+            )
+        });
 
     // opt.assert(&total_points.lt(&Int::from_u64(&ctx, 300)));
     opt.minimize(&total_points);
@@ -68,24 +68,54 @@ pub fn run_model_check<'a>(students: &Vec<Student>, seminars: &Vec<Seminar>, poi
         let model = opt.get_model().unwrap();
         // println!("{:?}", model);
 
-        let s = &students[0];
-        println!("Details for {}", s.name);
-        println!("Practical: {:?}",
-                 votes_to_string_id(s, &SeminarType::Practical)
-                     .iter()
-                     .map(|s| votes.get(s).unwrap())
-                     .map(|v| model.get_const_interp(v).unwrap())
-                     .collect::<Vec<Bool>>());
-        println!("Scientific: {:?}",
-                 votes_to_string_id(s, &SeminarType::Scientific)
-                     .iter()
-                     .map(|s| votes.get(s).unwrap())
-                     .map(|v| model.get_const_interp(v).unwrap())
-                     .collect::<Vec<Bool>>());
-        println!("Practical points: {:?}", model.get_const_interp(student_points.get(&student_to_points_id(s, SeminarType::Practical)).unwrap()));
-        println!("Scientific points: {:?}", model.get_const_interp(student_points.get(&student_to_points_id(s, SeminarType::Scientific)).unwrap()));
-
-        println!("Total Points: {:?}", opt.get_model().unwrap().get_const_interp(&total_points));
+        let capacities: Vec<Option<u16>> = seminars.iter().map(|_| Some(0)).collect();
+
+        let assignments: Vec<Assignment> = students.iter().map(|student| {
+            let p_points = model.get_const_interp(student_points.get(&student_to_points_id(student, SeminarType::Practical)).unwrap()).unwrap();
+            let w_points = model.get_const_interp(student_points.get(&student_to_points_id(student, SeminarType::Scientific)).unwrap()).unwrap();
+
+            let mut a = Assignment::new(student);
+            let total_points = w_points.as_u64().unwrap() + p_points.as_u64().unwrap();
+            a.points = u16::try_from(total_points).unwrap();
+
+            let p_results =
+                votes_to_string_id(student, &SeminarType::Practical)
+                    .iter()
+                    .map(|s| votes.get(s).unwrap())
+                    .map(|v| model.get_const_interp(v).unwrap())
+                    .collect::<Vec<Bool>>();
+            let w_results =
+                votes_to_string_id(student, &SeminarType::Scientific)
+                    .iter()
+                    .map(|s| votes.get(s).unwrap())
+                    .map(|v| model.get_const_interp(v).unwrap())
+                    .collect::<Vec<Bool>>();
+
+            for (ind, p_result) in p_results.iter().enumerate() {
+                if p_result.as_bool().unwrap() {
+                    if ind < student.p_wishes.len(){
+                        a.p_seminar = Some(&student.p_wishes[ind]);
+                    }else {
+                        a.p_seminar = None;
+                    }
+                    break;
+                }
+            }
+            for (ind, w_result) in w_results.iter().enumerate() {
+                if w_result.as_bool().unwrap() {
+                    if ind < student.w_wishes.len() {
+                        a.w_seminar = Some(&student.w_wishes[ind])
+                    }else {
+                        a.w_seminar = None;
+                    }
+                }
+            }
+            return a;
+        }).collect();
+
+        let mut res = RismResult::new(assignments, seminars, capacities);
+        res.calculate_points();
+        return Some(res);
     } else {
         // println!("{:?}", opt.get_proof().unwrap());
         println!("Unsatisfieable or unknown result!")