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"
},
"locked": {
"lastModified": 1685518550,
"narHash": "sha256-o2d0KcvaXzTrPRIo0kOLV0/QXHhDQ5DTi+OxcjO8xqY=",
"lastModified": 1689068808,
"narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "a1720a10a6cfe8234c0e93907ffe81be440f4cef",
"rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
"type": "github"
},
"original": {
@ -38,11 +38,11 @@
},
"nixpkgs": {
"locked": {
"lastModified": 1686059680,
"narHash": "sha256-sp0WlCIeVczzB0G8f8iyRg3IYW7KG31mI66z7HIZwrI=",
"lastModified": 1690927903,
"narHash": "sha256-D5gCaCROnjEKDOel//8TO/pOP87pAEtT0uT8X+0Bj/U=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "a558f7ac29f50c4b937fb5c102f587678ae1c9fb",
"rev": "bd836ac5e5a7358dea73cb74a013ca32864ccb86",
"type": "github"
},
"original": {
@ -52,6 +52,22 @@
"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": {
"inputs": {
"flake-utils": "flake-utils",
@ -70,11 +86,11 @@
]
},
"locked": {
"lastModified": 1686191569,
"narHash": "sha256-8ey5FOXNms9piFGTn6vJeAQmSKk+NL7GTMSoVttsNTs=",
"lastModified": 1691029059,
"narHash": "sha256-QwVeE9YTgH3LmL7yw2V/hgswL6yorIvYSp4YGI8lZYM=",
"owner": "oxalica",
"repo": "rust-overlay",
"rev": "b4b71458b92294e8f1c3a112d972e3cff8a2ab71",
"rev": "99df4908445be37ddb2d332580365fce512a7dcf",
"type": "github"
},
"original": {

View File

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

File diff suppressed because it is too large Load Diff

View File

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