mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-20 09:39:38 +01:00
Compare commits
4 Commits
ae1ca8bacb
...
d0e513451e
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
d0e513451e | ||
|
|
63e051b439 | ||
|
|
5b72e09741 | ||
|
|
479fa7bfbd |
6
.github/workflows/devskim.yml
vendored
6
.github/workflows/devskim.yml
vendored
@ -16,19 +16,19 @@ on:
|
|||||||
jobs:
|
jobs:
|
||||||
lint:
|
lint:
|
||||||
name: DevSkim
|
name: DevSkim
|
||||||
runs-on: ubuntu-20.04
|
runs-on: ubuntu-latest
|
||||||
permissions:
|
permissions:
|
||||||
actions: read
|
actions: read
|
||||||
contents: read
|
contents: read
|
||||||
security-events: write
|
security-events: write
|
||||||
steps:
|
steps:
|
||||||
- name: Checkout code
|
- name: Checkout code
|
||||||
uses: actions/checkout@v3
|
uses: actions/checkout@v4
|
||||||
|
|
||||||
- name: Run DevSkim scanner
|
- name: Run DevSkim scanner
|
||||||
uses: microsoft/DevSkim-Action@v1
|
uses: microsoft/DevSkim-Action@v1
|
||||||
|
|
||||||
- name: Upload DevSkim scan results to GitHub Security tab
|
- name: Upload DevSkim scan results to GitHub Security tab
|
||||||
uses: github/codeql-action/upload-sarif@v2
|
uses: github/codeql-action/upload-sarif@v3
|
||||||
with:
|
with:
|
||||||
sarif_file: devskim-results.sarif
|
sarif_file: devskim-results.sarif
|
||||||
|
|||||||
@ -204,14 +204,14 @@ impl App {
|
|||||||
Some("nai") => {
|
Some("nai") => {
|
||||||
let naive_adf = adf.hybrid_step_opt(false);
|
let naive_adf = adf.hybrid_step_opt(false);
|
||||||
for ac_counts in naive_adf.formulacounts(false) {
|
for ac_counts in naive_adf.formulacounts(false) {
|
||||||
print!("{:?} ", ac_counts);
|
print!("{ac_counts:?} ");
|
||||||
}
|
}
|
||||||
println!();
|
println!();
|
||||||
}
|
}
|
||||||
Some("mem") => {
|
Some("mem") => {
|
||||||
let naive_adf = adf.hybrid_step_opt(false);
|
let naive_adf = adf.hybrid_step_opt(false);
|
||||||
for ac_counts in naive_adf.formulacounts(true) {
|
for ac_counts in naive_adf.formulacounts(true) {
|
||||||
print!("{:?}", ac_counts);
|
print!("{ac_counts:?}");
|
||||||
}
|
}
|
||||||
println!();
|
println!();
|
||||||
}
|
}
|
||||||
@ -383,13 +383,13 @@ impl App {
|
|||||||
match self.counter.as_deref() {
|
match self.counter.as_deref() {
|
||||||
Some("nai") => {
|
Some("nai") => {
|
||||||
for ac_counts in adf.formulacounts(false) {
|
for ac_counts in adf.formulacounts(false) {
|
||||||
print!("{:?} ", ac_counts);
|
print!("{ac_counts:?} ");
|
||||||
}
|
}
|
||||||
println!();
|
println!();
|
||||||
}
|
}
|
||||||
Some("mem") => {
|
Some("mem") => {
|
||||||
for ac_counts in adf.formulacounts(true) {
|
for ac_counts in adf.formulacounts(true) {
|
||||||
print!("{:?}", ac_counts);
|
print!("{ac_counts:?}");
|
||||||
}
|
}
|
||||||
println!();
|
println!();
|
||||||
}
|
}
|
||||||
|
|||||||
12
flake.lock
generated
12
flake.lock
generated
@ -38,11 +38,11 @@
|
|||||||
},
|
},
|
||||||
"nixpkgs": {
|
"nixpkgs": {
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1749024892,
|
"lastModified": 1750969886,
|
||||||
"narHash": "sha256-OGcDEz60TXQC+gVz5sdtgGJdKVYr6rwdzQKuZAJQpCA=",
|
"narHash": "sha256-zW/OFnotiz/ndPFdebpo3X0CrbVNf22n4DjN2vxlb58=",
|
||||||
"owner": "NixOS",
|
"owner": "NixOS",
|
||||||
"repo": "nixpkgs",
|
"repo": "nixpkgs",
|
||||||
"rev": "8f1b52b04f2cb6e5ead50bd28d76528a2f0380ef",
|
"rev": "a676066377a2fe7457369dd37c31fd2263b662f4",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
@ -66,11 +66,11 @@
|
|||||||
]
|
]
|
||||||
},
|
},
|
||||||
"locked": {
|
"locked": {
|
||||||
"lastModified": 1749091064,
|
"lastModified": 1751251399,
|
||||||
"narHash": "sha256-TGtYjzRX0sueFhwYsnNNFF5TTKnpnloznpIghLzxeXo=",
|
"narHash": "sha256-y+viCuy/eKKpkX1K2gDvXIJI/yzvy6zA3HObapz9XZ0=",
|
||||||
"owner": "oxalica",
|
"owner": "oxalica",
|
||||||
"repo": "rust-overlay",
|
"repo": "rust-overlay",
|
||||||
"rev": "12419593ce78f2e8e1e89a373c6515885e218acb",
|
"rev": "b22d5ee8c60ed1291521f2dde48784edd6bf695b",
|
||||||
"type": "github"
|
"type": "github"
|
||||||
},
|
},
|
||||||
"original": {
|
"original": {
|
||||||
|
|||||||
@ -275,8 +275,8 @@ mod test {
|
|||||||
let term: Term = Term::from(value);
|
let term: Term = Term::from(value);
|
||||||
let var = Var::from(value);
|
let var = Var::from(value);
|
||||||
// display
|
// display
|
||||||
assert_eq!(format!("{}", term), format!("Term({})", value));
|
assert_eq!(format!("{term}"), format!("Term({})", value));
|
||||||
assert_eq!(format!("{}", var), format!("Var({})", value));
|
assert_eq!(format!("{var}"), format!("Var({})", value));
|
||||||
//deref
|
//deref
|
||||||
assert_eq!(value, *term);
|
assert_eq!(value, *term);
|
||||||
true
|
true
|
||||||
|
|||||||
@ -690,7 +690,7 @@ mod test {
|
|||||||
let a1 = bdd.and(v1, v2);
|
let a1 = bdd.and(v1, v2);
|
||||||
let _a2 = bdd.or(a1, v3);
|
let _a2 = bdd.or(a1, v3);
|
||||||
|
|
||||||
assert_eq!(format!("{}", bdd), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n");
|
assert_eq!(format!("{bdd}"), " \n0 BddNode: Var(18446744073709551614), lo: Term(0), hi: Term(0)\n1 BddNode: Var(18446744073709551615), lo: Term(1), hi: Term(1)\n2 BddNode: Var(0), lo: Term(0), hi: Term(1)\n3 BddNode: Var(1), lo: Term(0), hi: Term(1)\n4 BddNode: Var(2), lo: Term(0), hi: Term(1)\n5 BddNode: Var(0), lo: Term(0), hi: Term(3)\n6 BddNode: Var(1), lo: Term(4), hi: Term(1)\n7 BddNode: Var(0), lo: Term(4), hi: Term(6)\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
|
|||||||
@ -94,25 +94,25 @@ impl std::fmt::Debug for Formula {
|
|||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Formula::Atom(a) => {
|
Formula::Atom(a) => {
|
||||||
write!(f, "{}", a)?;
|
write!(f, "{a}")?;
|
||||||
}
|
}
|
||||||
Formula::Not(n) => {
|
Formula::Not(n) => {
|
||||||
write!(f, "not({:?})", n)?;
|
write!(f, "not({n:?})")?;
|
||||||
}
|
}
|
||||||
Formula::And(f1, f2) => {
|
Formula::And(f1, f2) => {
|
||||||
write!(f, "and({:?},{:?})", f1, f2)?;
|
write!(f, "and({f1:?},{f2:?})")?;
|
||||||
}
|
}
|
||||||
Formula::Or(f1, f2) => {
|
Formula::Or(f1, f2) => {
|
||||||
write!(f, "or({:?},{:?})", f1, f2)?;
|
write!(f, "or({f1:?},{f2:?})")?;
|
||||||
}
|
}
|
||||||
Formula::Imp(f1, f2) => {
|
Formula::Imp(f1, f2) => {
|
||||||
write!(f, "imp({:?},{:?})", f1, f2)?;
|
write!(f, "imp({f1:?},{f2:?})")?;
|
||||||
}
|
}
|
||||||
Formula::Xor(f1, f2) => {
|
Formula::Xor(f1, f2) => {
|
||||||
write!(f, "xor({:?},{:?})", f1, f2)?;
|
write!(f, "xor({f1:?},{f2:?})")?;
|
||||||
}
|
}
|
||||||
Formula::Iff(f1, f2) => {
|
Formula::Iff(f1, f2) => {
|
||||||
write!(f, "iff({:?},{:?})", f1, f2)?;
|
write!(f, "iff({f1:?},{f2:?})")?;
|
||||||
}
|
}
|
||||||
Formula::Bot => {
|
Formula::Bot => {
|
||||||
write!(f, "Const(B)")?;
|
write!(f, "Const(B)")?;
|
||||||
@ -481,7 +481,7 @@ mod test {
|
|||||||
let (_remain, result) = AdfParser::formula(input).unwrap();
|
let (_remain, result) = AdfParser::formula(input).unwrap();
|
||||||
|
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
format!("{:?}", result),
|
format!("{result:?}"),
|
||||||
"and(or(not(a),iff( iff left ,b)),xor(imp(c,d),e))"
|
"and(or(not(a),iff( iff left ,b)),xor(imp(c,d),e))"
|
||||||
);
|
);
|
||||||
|
|
||||||
|
|||||||
@ -304,18 +304,14 @@ impl From<AF> for AdfParser {
|
|||||||
.0
|
.0
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(|attackers| {
|
.map(|attackers| {
|
||||||
attackers.into_iter().fold(
|
attackers.into_iter().fold(Formula::Top, |acc, attacker| {
|
||||||
// TODO: is it correct to use Top here? what if something is not attacked at all?
|
|
||||||
Formula::Top,
|
|
||||||
|acc, attacker| {
|
|
||||||
Formula::And(
|
Formula::And(
|
||||||
Box::new(acc),
|
Box::new(acc),
|
||||||
Box::new(Formula::Not(Box::new(Formula::Atom(
|
Box::new(Formula::Not(Box::new(Formula::Atom(
|
||||||
(attacker + 1).to_string(),
|
(attacker + 1).to_string(),
|
||||||
)))),
|
)))),
|
||||||
)
|
)
|
||||||
},
|
})
|
||||||
)
|
|
||||||
})
|
})
|
||||||
.collect();
|
.collect();
|
||||||
let formulanames = names.clone();
|
let formulanames = names.clone();
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user