WIP: Binary for ICCMA 2025

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members=[ "lib", "bin", "server" ]
+members=[ "lib", "bin", "server" , "iccma-2025-bin"]
 default-members = [ "lib" ]
 
 [profile.release]

flake.lock

@@ -5,11 +5,11 @@
         "flake-utils": "flake-utils_2"
       },
       "locked": {
-        "lastModified": 1696331477,
-        "narHash": "sha256-YkbRa/1wQWdWkVJ01JvV+75KIdM37UErqKgTf0L54Fk=",
+        "lastModified": 1722363685,
+        "narHash": "sha256-XCf2PIAT6lH7BwytgioPmVf/wkzXjSKScC4KzcZgb64=",
         "owner": "gytis-ivaskevicius",
         "repo": "flake-utils-plus",
-        "rev": "bfc53579db89de750b25b0c5e7af299e0c06d7d3",
+        "rev": "6b10f51ff73a66bb29f3bc8151a59d217713f496",
         "type": "github"
       },
       "original": {
@@ -38,16 +38,16 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1704290814,
-        "narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=",
+        "lastModified": 1736200483,
+        "narHash": "sha256-JO+lFN2HsCwSLMUWXHeOad6QUxOuwe9UOAF/iSl1J4I=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421",
+        "rev": "3f0a8ac25fb674611b98089ca3a5dd6480175751",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixos-23.05",
+        "ref": "nixos-24.11",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -61,20 +61,16 @@
     },
     "rust-overlay": {
       "inputs": {
-        "flake-utils": [
-          "flake-utils",
-          "flake-utils"
-        ],
         "nixpkgs": [
           "nixpkgs"
         ]
       },
       "locked": {
-        "lastModified": 1704680242,
-        "narHash": "sha256-5bD6iSPDgVTLly2gy2oJVwzuyuFZOz2p4qt8c8UoYIE=",
+        "lastModified": 1736390353,
+        "narHash": "sha256-e2SP1zV9CISHlYZwEhwT53N9CW7yPh0tKTR0vuQqiWc=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "2037779e018ebc2d381001a891e2a793fce7a74f",
+        "rev": "1033caad3e26a56050de55ba0384df5ff0fa5ebd",
         "type": "github"
       },
       "original": {

flake.nix

@@ -2,7 +2,7 @@ rec {
   description = "adf-bdd, Abstract Dialectical Frameworks solved by Binary Decision Diagrams; developed in Dresden";
 
   inputs = {
-    nixpkgs.url = "github:NixOS/nixpkgs/nixos-23.05";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-24.11";
     rust-overlay = {
       url = "github:oxalica/rust-overlay";
       inputs = {

iccma-2025-bin/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "adf-bdd-iccma-2025-bin"
+version = "0.3.0-dev"
+authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>", "Lukas Gerlach <lukas.gerlach@tu-dresden.de>"]
+edition = "2021"
+
+[dependencies]
+adf_bdd = { version="0.3.1", path="../lib", default-features = false }
+clap = {version = "4.3.0", features = [ "derive", "cargo", "env" ]}
+

iccma-2025-bin/src/main.rs

@@ -0,0 +1,85 @@
+use std::path::PathBuf;
+use std::io::BufRead;
+use clap::{builder, Parser, ValueEnum};
+
+#[derive(ValueEnum, Clone)]
+enum Task {
+    #[value(name="DC-CO")]
+    DcCo,
+    #[value(name="DC-ST")]
+    DcSt,
+    #[value(name="DC-SST")]
+    DcSst,
+    #[value(name="DS-PR")]
+    DsPr,
+    #[value(name="DS-ST")]
+    DsSt,
+    #[value(name="DS-SST")]
+    DsSst,
+    #[value(name="SE-PR")]
+    SePr,
+    #[value(name="SE-ST")]
+    SeSt,
+    #[value(name="SE-SST")]
+    SeSst,
+    #[value(name="SE-ID")]
+    SeId,
+}
+
+#[derive(Parser)]
+#[command(author, version, arg_required_else_help(true), help_template("{name} {version}\n{author-with-newline}"))]
+struct App {
+    #[arg(long,exclusive(true))]
+    problems: bool,
+    #[arg(short = 'p', value_enum, required_unless_present("problems"))]
+    task: Option<Task>,
+    #[arg(short = 'f', value_parser, required_unless_present("problems"))]
+    input_file: Option<PathBuf>,
+    #[arg(short = 'a', required_if_eq_any([("task", "DC-CO"), ("task", "DC-ST"), ("task", "DC-SST"), ("task", "DS-PR"), ("task", "DS-ST"), ("task", "DS-SST")]))]
+    query: Option<usize>,
+}
+
+fn main() {
+    let app = App::parse();
+
+    if app.problems {
+        let possible_values: Vec<String> = Task::value_variants().into_iter().filter_map(Task::to_possible_value).map(|pv| builder::PossibleValue::get_name(&pv).to_string()).collect();
+        print!("[");
+        print!("{}", possible_values.join(","));
+        println!("]")
+    } else {
+        let task = app.task.expect("Task is required when \"problems\" flag is false.");
+        let file = app.input_file.expect("File is required when \"problems\" flag is false.");
+        let query = app.query;
+
+        let file = std::fs::File::open(file).expect("Error Reading File");
+        let mut lines = std::io::BufReader::new(file).lines();
+
+        let first_line = lines.next().expect("There must be at least one line in the file").expect("Error Reading Line");
+        let first_line: Vec<_> = first_line.split(" ").collect();
+        if first_line[0] != "p" || first_line[1] != "af" {
+            panic!("Expected first line to be of the form: p af <n>");
+        }
+
+        let num_arguments: usize = first_line[2].parse().expect("Could not convert number of arguments to u32; expected first line to be of the form: p af <n>");
+
+        let attacks: Vec<(usize, usize)> = lines.map(|line| line.expect("Error Reading Line")).filter(|line| !line.starts_with('#') || line.is_empty()).map(|line| {
+            let mut line = line.split(" ");
+            let a = line.next()?;
+            let b = line.next()?;
+            if line.next().is_some() {
+                None
+            } else {
+                Some((a.parse().ok()?, b.parse().ok()?))
+            }
+        }).map(|res_option| res_option.expect("Line must be of the form: n m")).collect();
+
+        // index in outer vector represents attacked element
+        let mut is_attacked_by: Vec<Vec<usize>> = vec![vec![]; num_arguments.try_into().unwrap()];
+        for (a, b) in attacks {
+            is_attacked_by[b-1].push(a-1); // we normalize names to be zero-indexed
+        }
+    }
+
+    //app.run();
+}

lib/src/adf.rs

@@ -1135,8 +1135,8 @@ mod test {
         let (s, r) = unbounded();
         adf.nogood_internal(
             &grounded,
-            crate::adf::heuristics::heu_simple,
-            crate::adf::Adf::stability_check,
+            heuristics::heu_simple,
+            Adf::stability_check,
             s,
         );
 
@@ -1172,8 +1172,8 @@ mod test {
         let (s, r) = unbounded();
         adf.nogood_internal(
             &grounded,
-            crate::adf::heuristics::heu_simple,
-            crate::adf::Adf::stability_check,
+            heuristics::heu_simple,
+            Adf::stability_check,
             s.clone(),
         );
         let stable_result = r.try_iter().collect::<Vec<_>>();

lib/src/adfbiodivine.rs

@@ -2,9 +2,11 @@
 //! utilising the biodivine-lib-bdd (see <https://github.com/sybila/biodivine-lib-bdd>) BDD implementation to compute various semantics.
 //!
 //! These are currently the
+//! 
 //!  - grounded
 //!  - stable
 //!  - complete
+//! 
 //! semantics of ADFs.
 
 use crate::{
@@ -89,7 +91,7 @@ impl Adf {
 
     pub(crate) fn stm_rewriting(&mut self, parser: &AdfParser) {
         let expr = parser.formula_order().iter().enumerate().fold(
-            biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
+            BooleanExpression::Const(true),
             |acc, (insert_order, new_order)| {
                 BooleanExpression::And(
                     Box::new(acc),
@@ -322,13 +324,13 @@ impl Adf {
         log::debug!("[Start] stable representation rewriting");
         self.ac.iter().enumerate().fold(
             self.varset.eval_expression(
-                &biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
+                &BooleanExpression::Const(true),
             ),
             |acc, (idx, formula)| {
                 acc.and(
                     &formula.iff(
                         &self.varset.eval_expression(
-                            &biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable(
+                            &BooleanExpression::Variable(
                                 self.ordering
                                     .name(crate::datatypes::Var(idx))
                                     .expect("Variable should exist"),
@@ -430,8 +432,8 @@ mod test {
         let c = variables.eval_expression_string("c");
         let d = variables.eval_expression_string("a & b & c");
         let e = variables.eval_expression_string("a ^ b");
-        let t = variables.eval_expression(&boolean_expression::BooleanExpression::Const(true));
-        let f = variables.eval_expression(&boolean_expression::BooleanExpression::Const(false));
+        let t = variables.eval_expression(&BooleanExpression::Const(true));
+        let f = variables.eval_expression(&BooleanExpression::Const(false));
 
         println!("{:?}", a.to_string());
         println!("{:?}", a.to_bytes());

lib/src/lib.rs

@@ -342,7 +342,6 @@ let parsed_adf: Adf = parsed_custom_adf.into();
 #![deny(
     missing_debug_implementations,
     missing_copy_implementations,
-    missing_copy_implementations,
     trivial_casts,
     trivial_numeric_casts,
     unsafe_code

lib/src/obdd/frontend.rs

@@ -33,6 +33,7 @@ impl super::Bdd {
     /// # Attention
     /// - Constants for [`⊤`][crate::datatypes::Term::TOP] and [`⊥`][crate::datatypes::Term::BOT] concepts are not sent, as they are considered to be existing in every [Bdd][super::Bdd] structure.
     /// - Mixing manipulating operations and utilising the communication channel for a receiving [roBDD][super::Bdd] may end up in inconsistent data.
+    /// 
     /// So far, only manipulate the [roBDD][super::Bdd] if no further [recv][Self::recv] will be called.
     pub fn with_sender_receiver(
         sender: crossbeam_channel::Sender<BddNode>,

lib/src/obdd/vectorize.rs

@@ -11,7 +11,7 @@ where
     V: Serialize + 'a,
 {
     let container: Vec<_> = target.into_iter().collect();
-    serde::Serialize::serialize(&container, ser)
+    Serialize::serialize(&container, ser)
 }
 
 /// Deserialize from a [Vector][std::vec::Vec] to a [Map][std::collections::HashMap].
@@ -22,6 +22,6 @@ where
     K: Deserialize<'de>,
     V: Deserialize<'de>,
 {
-    let container: Vec<_> = serde::Deserialize::deserialize(des)?;
+    let container: Vec<_> = Deserialize::deserialize(des)?;
     Ok(T::from_iter(container))
 }