1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-20 09:39:38 +01:00

Compare commits

..

6 Commits

Author SHA1 Message Date
19a49c7844
Add flake app and packages for adf-bdd 2023-08-04 11:37:04 +02:00
dependabot[bot]
fc0042fcd1
Bump serde from 1.0.180 to 1.0.181 (#166) 2023-08-04 09:28:10 +00:00
dependabot[bot]
bc403d10cb
Merge pull request #165 from ellmau/dependabot/npm_and_yarn/frontend/semver-6.3.1 2023-08-04 09:20:41 +00:00
dependabot[bot]
34d3af0c0d
Bump semver from 6.3.0 to 6.3.1 in /frontend
Bumps [semver](https://github.com/npm/node-semver) from 6.3.0 to 6.3.1.
- [Release notes](https://github.com/npm/node-semver/releases)
- [Changelog](https://github.com/npm/node-semver/blob/v6.3.1/CHANGELOG.md)
- [Commits](https://github.com/npm/node-semver/compare/v6.3.0...v6.3.1)

---
updated-dependencies:
- dependency-name: semver
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
2023-08-04 09:11:03 +00:00
monsterkrampe
8cafca22eb Fix typo in info text 2023-08-04 11:09:08 +02:00
monsterkrampe
3979f77d03 Upgrade dependencies 2023-08-04 10:59:27 +02:00
6 changed files with 1528 additions and 1458 deletions

835
Cargo.lock generated

File diff suppressed because it is too large Load Diff

34
flake.lock generated
View File

@ -23,11 +23,11 @@
"systems": "systems" "systems": "systems"
}, },
"locked": { "locked": {
"lastModified": 1685518550, "lastModified": 1689068808,
"narHash": "sha256-o2d0KcvaXzTrPRIo0kOLV0/QXHhDQ5DTi+OxcjO8xqY=", "narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
"owner": "numtide", "owner": "numtide",
"repo": "flake-utils", "repo": "flake-utils",
"rev": "a1720a10a6cfe8234c0e93907ffe81be440f4cef", "rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -38,11 +38,11 @@
}, },
"nixpkgs": { "nixpkgs": {
"locked": { "locked": {
"lastModified": 1686059680, "lastModified": 1690927903,
"narHash": "sha256-sp0WlCIeVczzB0G8f8iyRg3IYW7KG31mI66z7HIZwrI=", "narHash": "sha256-D5gCaCROnjEKDOel//8TO/pOP87pAEtT0uT8X+0Bj/U=",
"owner": "NixOS", "owner": "NixOS",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "a558f7ac29f50c4b937fb5c102f587678ae1c9fb", "rev": "bd836ac5e5a7358dea73cb74a013ca32864ccb86",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -52,6 +52,22 @@
"type": "github" "type": "github"
} }
}, },
"nixpkgs-unstable": {
"locked": {
"lastModified": 1690881714,
"narHash": "sha256-h/nXluEqdiQHs1oSgkOOWF+j8gcJMWhwnZ9PFabN6q0=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "9e1960bc196baf6881340d53dccb203a951745a2",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": { "root": {
"inputs": { "inputs": {
"flake-utils": "flake-utils", "flake-utils": "flake-utils",
@ -70,11 +86,11 @@
] ]
}, },
"locked": { "locked": {
"lastModified": 1686191569, "lastModified": 1691029059,
"narHash": "sha256-8ey5FOXNms9piFGTn6vJeAQmSKk+NL7GTMSoVttsNTs=", "narHash": "sha256-QwVeE9YTgH3LmL7yw2V/hgswL6yorIvYSp4YGI8lZYM=",
"owner": "oxalica", "owner": "oxalica",
"repo": "rust-overlay", "repo": "rust-overlay",
"rev": "b4b71458b92294e8f1c3a112d972e3cff8a2ab71", "rev": "99df4908445be37ddb2d332580365fce512a7dcf",
"type": "github" "type": "github"
}, },
"original": { "original": {

View File

@ -9,32 +9,32 @@
"build": "parcel build" "build": "parcel build"
}, },
"devDependencies": { "devDependencies": {
"@parcel/transformer-inline-string": "2.8.3", "@parcel/transformer-inline-string": "2.9.3",
"@types/node": "^18.15.11", "@types/node": "^20.4.6",
"@types/react": "^18.0.26", "@types/react": "^18.2.18",
"@types/react-dom": "^18.0.10", "@types/react-dom": "^18.2.7",
"@typescript-eslint/eslint-plugin": "^5.48.1", "@typescript-eslint/eslint-plugin": "^6.2.1",
"@typescript-eslint/parser": "^5.48.1", "@typescript-eslint/parser": "^6.2.1",
"eslint": "^8.31.0", "eslint": "^8.46.0",
"eslint-config-airbnb": "^19.0.4", "eslint-config-airbnb": "^19.0.4",
"eslint-config-airbnb-typescript": "^17.0.0", "eslint-config-airbnb-typescript": "^17.1.0",
"eslint-plugin-import": "^2.27.4", "eslint-plugin-import": "^2.28.0",
"eslint-plugin-jsx-a11y": "^6.7.1", "eslint-plugin-jsx-a11y": "^6.7.1",
"eslint-plugin-react": "^7.32.0", "eslint-plugin-react": "^7.33.1",
"parcel": "^2.8.2", "parcel": "^2.9.3",
"process": "^0.11.10", "process": "^0.11.10",
"typescript": "^4.9.4" "typescript": "^5.1.6"
}, },
"dependencies": { "dependencies": {
"@antv/g6": "^4.8.3", "@antv/g6": "^4.8.20",
"@emotion/react": "^11.10.5", "@emotion/react": "^11.11.1",
"@emotion/styled": "^11.10.5", "@emotion/styled": "^11.11.0",
"@fontsource/roboto": "^4.5.8", "@fontsource/roboto": "^5.0.6",
"@mui/icons-material": "^5.11.16", "@mui/icons-material": "^5.14.3",
"@mui/material": "^5.11.4", "@mui/material": "^5.14.3",
"markdown-to-jsx": "^7.2.0", "markdown-to-jsx": "^7.2.1",
"react": "^18.2.0", "react": "^18.2.0",
"react-dom": "^18.2.0", "react-dom": "^18.2.0",
"react-router-dom": "^6.10.0" "react-router-dom": "^6.14.2"
} }
} }

View File

@ -3,7 +3,7 @@ The Web UI mimics many options of the CLI version of the [underlying adf-bdd too
In the below form, you can either type/paste your `code` or upload a file in the same format. In the below form, you can either type/paste your `code` or upload a file in the same format.
To put it briefly, an ADF consists of statements and accectance conditions for these statements. To put it briefly, an ADF consists of statements and accectance conditions for these statements.
For instance, the following code indicates that `a,b,c,d` are statements, that `a` is assumed to be true (verum), `b` is true if is true (which is tautological), `c` is true if `a` and `b` are true, and `d` is true if `b` is false. For instance, the following code indicates that `a,b,c,d` are statements, that `a` is assumed to be true (verum), `b` is true if `b` is true (which is self-supporting), `c` is true if `a` and `b` are true, and `d` is true if `b` is false.
``` ```
s(a). s(a).

File diff suppressed because it is too large Load Diff

View File

@ -1,7 +1,6 @@
//! Collection of all nogood-related structures. //! Collection of all nogood-related structures.
use std::{ use std::{
borrow::Borrow,
fmt::{Debug, Display}, fmt::{Debug, Display},
ops::{BitAnd, BitOr, BitXor, BitXorAssign}, ops::{BitAnd, BitOr, BitXor, BitXorAssign},
}; };
@ -23,11 +22,8 @@ pub struct NoGood {
impl Eq for NoGood {} impl Eq for NoGood {}
impl PartialEq for NoGood { impl PartialEq for NoGood {
fn eq(&self, other: &Self) -> bool { fn eq(&self, other: &Self) -> bool {
self.active (&self.active).bitxor(&other.active).is_empty()
.borrow() && (&self.value).bitxor(&other.value).is_empty()
.bitxor(other.active.borrow())
.is_empty()
&& self.value.borrow().bitxor(other.value.borrow()).is_empty()
} }
} }
@ -113,15 +109,11 @@ impl NoGood {
/// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one. /// Given a [NoGood] and another one, conclude a non-conflicting value which can be concluded on basis of the given one.
pub fn conclude(&self, other: &NoGood) -> Option<(usize, bool)> { pub fn conclude(&self, other: &NoGood) -> Option<(usize, bool)> {
log::debug!("conclude: {:?} other {:?}", self, other); log::debug!("conclude: {:?} other {:?}", self, other);
let implication = self let implication = (&self.active).bitxor(&other.active).bitand(&self.active);
.active
.borrow()
.bitxor(other.active.borrow())
.bitand(self.active.borrow());
let bothactive = self.active.borrow().bitand(other.active.borrow()); let bothactive = (&self.active).bitand(&other.active);
let mut no_matches = bothactive.borrow().bitand(other.value.borrow()); let mut no_matches = (&bothactive).bitand(&other.value);
no_matches.bitxor_assign(bothactive.bitand(self.value.borrow())); no_matches.bitxor_assign(bothactive.bitand(&self.value));
if implication.len() == 1 && no_matches.is_empty() { if implication.len() == 1 && no_matches.is_empty() {
let pos = implication let pos = implication
@ -140,16 +132,16 @@ impl NoGood {
/// Updates the [NoGood] and a second one in a disjunctive (bitor) manner. /// Updates the [NoGood] and a second one in a disjunctive (bitor) manner.
pub fn disjunction(&mut self, other: &NoGood) { pub fn disjunction(&mut self, other: &NoGood) {
self.active = self.active.borrow().bitor(&other.active); self.active = (&self.active).bitor(&other.active);
self.value = self.value.borrow().bitor(&other.value); self.value = (&self.value).bitor(&other.value);
} }
/// Returns [true] if the other [Interpretation] matches with all the assignments of the current [NoGood]. /// Returns [true] if the other [Interpretation] matches with all the assignments of the current [NoGood].
pub fn is_violating(&self, other: &Interpretation) -> bool { pub fn is_violating(&self, other: &Interpretation) -> bool {
let active = self.active.borrow().bitand(other.active.borrow()); let active = (&self.active).bitand(&other.active);
if self.active.len() == active.len() { if self.active.len() == active.len() {
let lhs = active.borrow().bitand(self.value.borrow()); let lhs = (&active).bitand(&self.value);
let rhs = active.borrow().bitand(other.value.borrow()); let rhs = (&active).bitand(&other.value);
if lhs.bitxor(rhs).is_empty() { if lhs.bitxor(rhs).is_empty() {
return true; return true;
} }