ellmau/adf-obdd
1
0
Fork 0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-18 09:19:38 +01:00
Code Issues Projects Releases Wiki Activity

Update versions and fix formatting and clippy issues

Browse Source 
flake.lock: Update

Flake lock file updates:

• Updated input 'flake-utils':
    'github:gytis-ivaskevicius/flake-utils-plus/bfc53579db89de750b25b0c5e7af299e0c06d7d3?narHash=sha256-YkbRa/1wQWdWkVJ01JvV%2B75KIdM37UErqKgTf0L54Fk%3D' (2023-10-03)
  → 'github:gytis-ivaskevicius/flake-utils-plus/afcb15b845e74ac5e998358709b2b5fe42a948d1?narHash=sha256-4WNeriUToshQ/L5J%2BdTSWC5OJIwT39SEP7V7oylndi8%3D' (2025-02-03)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/2037779e018ebc2d381001a891e2a793fce7a74f?narHash=sha256-5bD6iSPDgVTLly2gy2oJVwzuyuFZOz2p4qt8c8UoYIE%3D' (2024-01-08)
  → 'github:oxalica/rust-overlay/f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8?narHash=sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I%3D' (2025-03-13)
• Removed input 'rust-overlay/flake-utils'

Signed-off-by: Stefan Ellmauthaler <ellmauthaler@echo-intelligence.at>
This commit is contained in:
Stefan Ellmauthaler 2025-03-13 18:07:31 +01:00 committed by Stefan Ellmauthaler
parent 54e57e3820
commit ca6c94f2e5
9 changed files with 1336 additions and 736 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2001
Cargo.lock generated
View File

File diff suppressed because it is too large Load Diff

5
bin/src/main.rs
View File

@ -63,7 +63,6 @@ OPTIONS:
#![deny(
missing_debug_implementations,
missing_copy_implementations,
missing_copy_implementations,
trivial_casts,
trivial_numeric_casts,
unsafe_code
@ -181,7 +180,7 @@ impl App {
let input = std::fs::read_to_string(self.input.clone()).expect("Error Reading File");
match self.implementation.as_str() {
"hybrid" => {
let parser = adf_bdd::parser::AdfParser::default();
let parser = AdfParser::default();
match parser.parse()(&input) {
Ok(_) => log::info!("[Done] parsing"),
Err(e) => {
@ -283,7 +282,7 @@ impl App {
if self.counter.is_some() {
log::error!("Modelcounting not supported in biodivine mode");
}
let parser = adf_bdd::parser::AdfParser::default();
let parser = AdfParser::default();
match parser.parse()(&input) {
Ok(_) => log::info!("[Done] parsing"),
Err(e) => {

24
flake.lock generated
View File

@ -5,11 +5,11 @@
"flake-utils": "flake-utils_2"
},
"locked": {
"lastModified": 1696331477,
"narHash": "sha256-YkbRa/1wQWdWkVJ01JvV+75KIdM37UErqKgTf0L54Fk=",
"lastModified": 1738591040,
"narHash": "sha256-4WNeriUToshQ/L5J+dTSWC5OJIwT39SEP7V7oylndi8=",
"owner": "gytis-ivaskevicius",
"repo": "flake-utils-plus",
"rev": "bfc53579db89de750b25b0c5e7af299e0c06d7d3",
"rev": "afcb15b845e74ac5e998358709b2b5fe42a948d1",
"type": "github"
},
"original": {
@ -38,16 +38,16 @@
},
"nixpkgs": {
"locked": {
"lastModified": 1704290814,
"narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=",
"lastModified": 1741724370,
"narHash": "sha256-WsD+8uodhl58jzKKcPH4jH9dLTLFWZpVmGq4W1XDVF4=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421",
"rev": "95600680c021743fd87b3e2fe13be7c290e1cac4",
"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": 1741833135,
"narHash": "sha256-HUtFcF4NLwvu7CAowWgqCHXVkNj0EOc/W6Ism4biV6I=",
"owner": "oxalica",
"repo": "rust-overlay",
"rev": "2037779e018ebc2d381001a891e2a793fce7a74f",
"rev": "f3cd1e0feb994188fe3ad9a5c3ab021ed433b8c8",
"type": "github"
},
"original": {

2
flake.nix
View File

@ -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 = {

11
lib/src/adf.rs
View File

@ -1133,12 +1133,7 @@ mod test {
let grounded = adf.grounded();
let (s, r) = unbounded();
adf.nogood_internal(
&grounded,
crate::adf::heuristics::heu_simple,
crate::adf::Adf::stability_check,
s,
);
adf.nogood_internal(&grounded, heuristics::heu_simple, Adf::stability_check, s);
assert_eq!(
r.iter().collect::<Vec<_>>(),
@ -1172,8 +1167,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<_>>();

23
lib/src/adfbiodivine.rs
View File

@ -5,6 +5,7 @@
//! - grounded
//! - stable
//! - complete
//!
//! semantics of ADFs.
use crate::{
@ -89,7 +90,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),
@ -321,19 +322,15 @@ impl Adf {
fn stable_representation(&self) -> Bdd {
log::debug!("[Start] stable representation rewriting");
self.ac.iter().enumerate().fold(
self.varset.eval_expression(
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Const(true),
),
self.varset.eval_expression(&BooleanExpression::Const(true)),
|acc, (idx, formula)| {
acc.and(
&formula.iff(
&self.varset.eval_expression(
&biodivine_lib_bdd::boolean_expression::BooleanExpression::Variable(
self.ordering
.name(crate::datatypes::Var(idx))
.expect("Variable should exist"),
),
),
&self.varset.eval_expression(&BooleanExpression::Variable(
self.ordering
.name(crate::datatypes::Var(idx))
.expect("Variable should exist"),
)),
),
)
},
@ -430,8 +427,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());

1
lib/src/lib.rs
View File

@ -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

1
lib/src/obdd/frontend.rs
View File

@ -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>,

4
lib/src/obdd/vectorize.rs
View File

@ -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))
}