mirror of
https://github.com/ellmau/adf-obdd.git
synced 2025-12-19 09:29:36 +01:00
Implementing nom-based parser (#5)
* Implemented a nom-based parser to read the adf * Grounded semantics (naive) re-implemented * Docs added * Updated Cargo.toml with more Manifest information * Version update * Added sort-methods to the parser, so the var-order can be adjusted * Added sort functionality to the main function * Added adf-instances as a submodule to the res-folder * Added README information for the extended integration tests * Rewritten main-function Closes #3
This commit is contained in:
Stefan Ellmauthaler
GitHub
parent
a34e711266
commit
0d5577e251
3
.github/workflows/build.yml
vendored
3
.github/workflows/build.yml
vendored
@ -1,3 +1,4 @@
|
|||||||
|
name: Build Releases
|
||||||
on:
|
on:
|
||||||
release:
|
release:
|
||||||
types: [created]
|
types: [created]
|
||||||
@ -9,7 +10,7 @@ jobs:
|
|||||||
strategy:
|
strategy:
|
||||||
fail-fast: false
|
fail-fast: false
|
||||||
matrix:
|
matrix:
|
||||||
target: [x86_64-pc-windows-gnu, x86_64-unknown-linux-musl]
|
target: [x86_64-pc-windows-gnu, x86_64-unknown-linux-musl,x86_64-apple-darwin]
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@master
|
- uses: actions/checkout@master
|
||||||
- name: Compile and release
|
- name: Compile and release
|
||||||
|
|||||||
3
.gitmodules
vendored
Normal file
3
.gitmodules
vendored
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
[submodule "res/adf-instances"]
|
||||||
|
path = res/adf-instances
|
||||||
|
url = https://github.com/ellmau/adf-instances.git
|
||||||
116
Cargo.lock
generated
116
Cargo.lock
generated
@ -8,8 +8,11 @@ version = "0.1.1"
|
|||||||
dependencies = [
|
dependencies = [
|
||||||
"clap",
|
"clap",
|
||||||
"env_logger",
|
"env_logger",
|
||||||
|
"lexical-sort",
|
||||||
"log",
|
"log",
|
||||||
"test-env-log",
|
"nom",
|
||||||
|
"test-generator",
|
||||||
|
"test-log",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -30,6 +33,12 @@ dependencies = [
|
|||||||
"winapi",
|
"winapi",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "any_ascii"
|
||||||
|
version = "0.1.7"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "70033777eb8b5124a81a1889416543dddef2de240019b674c81285a2635a7e1e"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "atty"
|
name = "atty"
|
||||||
version = "0.2.14"
|
version = "0.2.14"
|
||||||
@ -81,6 +90,12 @@ dependencies = [
|
|||||||
"termcolor",
|
"termcolor",
|
||||||
]
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "glob"
|
||||||
|
version = "0.3.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "9b919933a397b79c37e33b77bb2aa3dc8eb6e165ad809e58ff75bc7db2e34574"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "hermit-abi"
|
name = "hermit-abi"
|
||||||
version = "0.1.19"
|
version = "0.1.19"
|
||||||
@ -96,6 +111,15 @@ version = "2.1.0"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
|
checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "lexical-sort"
|
||||||
|
version = "0.3.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "c09e4591611e231daf4d4c685a66cb0410cc1e502027a20ae55f2bb9e997207a"
|
||||||
|
dependencies = [
|
||||||
|
"any_ascii",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "libc"
|
name = "libc"
|
||||||
version = "0.2.107"
|
version = "0.2.107"
|
||||||
@ -117,13 +141,48 @@ version = "2.4.1"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a"
|
checksum = "308cc39be01b73d0d18f82a0e7b2a3df85245f84af96fdddc5d202d27e47b86a"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "minimal-lexical"
|
||||||
|
version = "0.2.1"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "nom"
|
||||||
|
version = "7.1.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "1b1d11e1ef389c76fe5b81bcaf2ea32cf88b62bc494e19f493d0b30e7a930109"
|
||||||
|
dependencies = [
|
||||||
|
"memchr",
|
||||||
|
"minimal-lexical",
|
||||||
|
"version_check",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "proc-macro2"
|
||||||
|
version = "0.4.30"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "cf3d2011ab5c909338f7887f4fc896d35932e29146c12c8d01da6b22a80ba759"
|
||||||
|
dependencies = [
|
||||||
|
"unicode-xid 0.1.0",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "proc-macro2"
|
name = "proc-macro2"
|
||||||
version = "1.0.32"
|
version = "1.0.32"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "ba508cc11742c0dc5c1659771673afbab7a0efab23aa17e854cbab0837ed0b43"
|
checksum = "ba508cc11742c0dc5c1659771673afbab7a0efab23aa17e854cbab0837ed0b43"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"unicode-xid",
|
"unicode-xid 0.2.2",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "quote"
|
||||||
|
version = "0.6.13"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "6ce23b6b870e8f94f81fb0a363d65d86675884b34a09043c81e5562f11c1f8e1"
|
||||||
|
dependencies = [
|
||||||
|
"proc-macro2 0.4.30",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -132,7 +191,7 @@ version = "1.0.10"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05"
|
checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"proc-macro2",
|
"proc-macro2 1.0.32",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -158,15 +217,26 @@ version = "0.8.0"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
|
checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "syn"
|
||||||
|
version = "0.15.44"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "9ca4b3b69a77cbe1ffc9e198781b7acb0c7365a883670e8f1c1bc66fba79a5c5"
|
||||||
|
dependencies = [
|
||||||
|
"proc-macro2 0.4.30",
|
||||||
|
"quote 0.6.13",
|
||||||
|
"unicode-xid 0.1.0",
|
||||||
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "syn"
|
name = "syn"
|
||||||
version = "1.0.81"
|
version = "1.0.81"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "f2afee18b8beb5a596ecb4a2dce128c719b4ba399d34126b9e4396e3f9860966"
|
checksum = "f2afee18b8beb5a596ecb4a2dce128c719b4ba399d34126b9e4396e3f9860966"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"proc-macro2",
|
"proc-macro2 1.0.32",
|
||||||
"quote",
|
"quote 1.0.10",
|
||||||
"unicode-xid",
|
"unicode-xid 0.2.2",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -179,14 +249,26 @@ dependencies = [
|
|||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "test-env-log"
|
name = "test-generator"
|
||||||
|
version = "0.3.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "ea97be90349ab3574f6e74d1566e1c5dd3a4bc74b89f4af4cc10ca010af103c0"
|
||||||
|
dependencies = [
|
||||||
|
"glob",
|
||||||
|
"proc-macro2 0.4.30",
|
||||||
|
"quote 0.6.13",
|
||||||
|
"syn 0.15.44",
|
||||||
|
]
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "test-log"
|
||||||
version = "0.2.8"
|
version = "0.2.8"
|
||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "877189d680101869f65ef94168105d6c188b3a143c13a2d42cf8a09c4c704f8a"
|
checksum = "eb78caec569a40f42c078c798c0e35b922d9054ec28e166f0d6ac447563d91a4"
|
||||||
dependencies = [
|
dependencies = [
|
||||||
"proc-macro2",
|
"proc-macro2 1.0.32",
|
||||||
"quote",
|
"quote 1.0.10",
|
||||||
"syn",
|
"syn 1.0.81",
|
||||||
]
|
]
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
@ -204,6 +286,12 @@ version = "0.1.9"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
|
checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "unicode-xid"
|
||||||
|
version = "0.1.0"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "unicode-xid"
|
name = "unicode-xid"
|
||||||
version = "0.2.2"
|
version = "0.2.2"
|
||||||
@ -216,6 +304,12 @@ version = "0.8.2"
|
|||||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
|
checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191"
|
||||||
|
|
||||||
|
[[package]]
|
||||||
|
name = "version_check"
|
||||||
|
version = "0.9.3"
|
||||||
|
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||||
|
checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe"
|
||||||
|
|
||||||
[[package]]
|
[[package]]
|
||||||
name = "winapi"
|
name = "winapi"
|
||||||
version = "0.3.9"
|
version = "0.3.9"
|
||||||
|
|||||||
13
Cargo.toml
13
Cargo.toml
@ -1,9 +1,11 @@
|
|||||||
[package]
|
[package]
|
||||||
name = "adf_bdd"
|
name = "adf_bdd"
|
||||||
version = "0.1.1"
|
version = "0.1.2"
|
||||||
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
|
authors = ["Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>"]
|
||||||
edition = "2021"
|
edition = "2021"
|
||||||
|
repository = "https://github.com/ellmau/adf-obdd/"
|
||||||
license = "GPL-3.0-only"
|
license = "GPL-3.0-only"
|
||||||
|
exclude = ["res/", "./flake*", "*.nix", ".envrc", "_config.yml"]
|
||||||
|
|
||||||
description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams"
|
description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams"
|
||||||
|
|
||||||
@ -12,8 +14,11 @@ description = "Solver for ADFs grounded semantics by utilising OBDDs - ordered b
|
|||||||
|
|
||||||
[dependencies]
|
[dependencies]
|
||||||
clap = "2.33.*"
|
clap = "2.33.*"
|
||||||
log = "0.4"
|
log = { version = "0.4", features = [ "max_level_trace", "release_max_level_info" ] }
|
||||||
|
env_logger = "0.9"
|
||||||
|
nom = "7.1.0"
|
||||||
|
lexical-sort = "0.3.1"
|
||||||
|
|
||||||
[dev-dependencies]
|
[dev-dependencies]
|
||||||
env_logger = "*"
|
test-log = "0.2.*"
|
||||||
test-env-log = "0.2.*"
|
test-generator = "0.3.0"
|
||||||
|
|||||||
20
README.md
20
README.md
@ -1,4 +1,4 @@
|
|||||||
[](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml)  
|
[](https://github.com/ellmau/adf-obdd/actions/workflows/build.yml) [](https://coveralls.io/github/ellmau/adf-obdd)     
|
||||||
# Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams
|
# Solver for ADFs grounded semantics by utilising OBDDs - ordered binary decision diagrams
|
||||||
|
|
||||||
|
|
||||||
@ -17,3 +17,21 @@ The binary predicate ac relates each statement to one propositional formula in p
|
|||||||
- neg(x): classical negation
|
- neg(x): classical negation
|
||||||
- c(v): constant symbol "verum" - tautology/top
|
- c(v): constant symbol "verum" - tautology/top
|
||||||
- c(f): constant symbol "falsum" - inconsistency/bot
|
- c(f): constant symbol "falsum" - inconsistency/bot
|
||||||
|
|
||||||
|
# Development notes
|
||||||
|
To run all the tests placed in the submodule you need to run
|
||||||
|
```bash
|
||||||
|
$> git submodule init
|
||||||
|
```
|
||||||
|
at the first time.
|
||||||
|
Afterwards you need to update the content of the submodule to be on the currently used revision by
|
||||||
|
```bash
|
||||||
|
$> git submodule update
|
||||||
|
```
|
||||||
|
|
||||||
|
The tests can be started by using the test-framework of cargo, i.e.
|
||||||
|
```bash
|
||||||
|
$> cargo test
|
||||||
|
```
|
||||||
|
Note that some of the instances are quite big and it might take some time to finish all the tests.
|
||||||
|
If you do not initialise the submodule, tests will "only" run on the other unit-tests and (possibly forthcoming) other integration tests.
|
||||||
|
|||||||
@ -37,6 +37,8 @@
|
|||||||
pkgs.cargo-audit
|
pkgs.cargo-audit
|
||||||
pkgs.cargo-license
|
pkgs.cargo-license
|
||||||
pkgs.cargo-tarpaulin
|
pkgs.cargo-tarpaulin
|
||||||
|
pkgs.cargo-kcov
|
||||||
|
pkgs.kcov
|
||||||
];
|
];
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|||||||
1
res/adf-instances
Submodule
1
res/adf-instances
Submodule
@ -0,0 +1 @@
|
|||||||
|
Subproject commit 322d7d44662450f25caa09c569b5f8362547907b
|
||||||
591
src/adf.rs
591
src/adf.rs
@ -6,469 +6,202 @@
|
|||||||
//! - computing fixpoints
|
//! - computing fixpoints
|
||||||
//! - computing the least fixpoint by using a shortcut
|
//! - computing the least fixpoint by using a shortcut
|
||||||
|
|
||||||
#![warn(missing_docs)]
|
use crate::{
|
||||||
|
datatypes::{
|
||||||
use std::{
|
adf::{PrintableInterpretation, VarContainer},
|
||||||
collections::HashMap,
|
Term, Var,
|
||||||
str::{self, FromStr},
|
},
|
||||||
usize,
|
obdd::Bdd,
|
||||||
|
parser::{AdfParser, Formula},
|
||||||
};
|
};
|
||||||
|
/// Representation of an ADF, with an ordering and dictionary of statement <-> number relations, a binary decision diagram, and a list of acceptance functions in Term representation
|
||||||
use crate::datatypes::{Term, Var};
|
|
||||||
|
|
||||||
use crate::obdd::Bdd;
|
|
||||||
|
|
||||||
struct Statement {
|
|
||||||
label: String, // label of the statement
|
|
||||||
var: usize, // variable node in bdd
|
|
||||||
ac: Option<usize>, // node in bdd
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Statement {
|
|
||||||
pub fn new(label: &str, var: usize) -> Self {
|
|
||||||
Statement {
|
|
||||||
label: String::from_str(label).unwrap(),
|
|
||||||
var,
|
|
||||||
ac: None,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn _add_ac(&mut self, ac: usize) {
|
|
||||||
self.ac = Some(ac);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// ADF structure which offers some statice and instance methods for handling ADFs.
|
|
||||||
pub struct Adf {
|
pub struct Adf {
|
||||||
|
ordering: VarContainer,
|
||||||
bdd: Bdd,
|
bdd: Bdd,
|
||||||
stmts: Vec<Statement>,
|
ac: Vec<Term>,
|
||||||
dict: HashMap<String, usize>, // label to pos in vec
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Default for Adf {
|
|
||||||
fn default() -> Self {
|
|
||||||
Adf::new()
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Adf {
|
impl Adf {
|
||||||
/// Creates a new and empty ADF.
|
/// Instantiates a new ADF, based on the parser-data
|
||||||
///
|
pub fn from_parser(parser: &AdfParser) -> Self {
|
||||||
/// To add statements call [`init_statements`](Adf::init_statements()) and then add to each statement it's corresponding acceptance contidion via
|
log::info!("[Start] instantiating BDD");
|
||||||
/// [`add_ac`](Adf::add_ac()).
|
let mut result = Self {
|
||||||
pub fn new() -> Self {
|
ordering: VarContainer::from_parser(
|
||||||
Adf {
|
parser.namelist_rc_refcell(),
|
||||||
|
parser.dict_rc_refcell(),
|
||||||
|
),
|
||||||
bdd: Bdd::new(),
|
bdd: Bdd::new(),
|
||||||
stmts: Vec::new(),
|
ac: vec![Term(0); parser.namelist_rc_refcell().as_ref().borrow().len()],
|
||||||
dict: HashMap::new(),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn add_statement(&mut self, statement: &str) {
|
|
||||||
if self.dict.get(statement).is_none() {
|
|
||||||
let pos = self.stmts.len();
|
|
||||||
//self.bdd.variable(pos);
|
|
||||||
//self.stmts
|
|
||||||
// .push(Statement::new(statement, pos.clone()));
|
|
||||||
self.stmts.push(Statement::new(
|
|
||||||
statement,
|
|
||||||
self.bdd.variable(Var(pos)).value(),
|
|
||||||
));
|
|
||||||
self.dict.insert(self.stmts[pos].label.to_string(), pos);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Initialise statements
|
|
||||||
///
|
|
||||||
/// The order of statements given as a parameter will determine die ordering for the OBDD.
|
|
||||||
/// Note that only initialised statements will be regocnised as variables later on.
|
|
||||||
/// This method can be called multiple times to add more statements.
|
|
||||||
pub fn init_statements(&mut self, stmts: Vec<&str>) -> usize {
|
|
||||||
for i in stmts.iter() {
|
|
||||||
self.add_statement(*i);
|
|
||||||
}
|
|
||||||
self.stmts.len()
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Adds to a given statement its acceptance condition.
|
|
||||||
///
|
|
||||||
/// This ac needs to be in the prefix notation for ADFs as defined by the DIAMOND implementation.
|
|
||||||
/// Every statement needs to be initialised before by [`init_statements'](Adf::init_statements()).
|
|
||||||
pub fn add_ac(&mut self, statement: &str, ac: &str) {
|
|
||||||
if let Some(stmt) = self.dict.get(statement) {
|
|
||||||
let st = *stmt;
|
|
||||||
self.add_ac_by_number(st, ac)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn add_ac_by_number(&mut self, st: usize, ac: &str) {
|
|
||||||
let ac_num = self.parse_formula(ac);
|
|
||||||
self.set_ac(st, ac_num);
|
|
||||||
}
|
|
||||||
|
|
||||||
fn set_ac(&mut self, st: usize, ac: usize) {
|
|
||||||
self.stmts[st].ac = Some(ac);
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Computes the grounded model of the adf.
|
|
||||||
///
|
|
||||||
/// Note that this computation will shortcut interpretation updates and needs less steps than computing the least fixpoint by an usual fixpoint-construction
|
|
||||||
pub fn grounded(&mut self) -> Vec<usize> {
|
|
||||||
let mut interpretation: Vec<usize> = Vec::new();
|
|
||||||
let mut change: bool;
|
|
||||||
|
|
||||||
for it in self.stmts.iter() {
|
|
||||||
interpretation.push((*it).ac.unwrap())
|
|
||||||
}
|
|
||||||
loop {
|
|
||||||
change = false;
|
|
||||||
for pos in 0..self.stmts.len() - 1 {
|
|
||||||
let curint = interpretation.clone();
|
|
||||||
match Term(curint[pos]) {
|
|
||||||
Term::BOT => {
|
|
||||||
if let Some(n) = self.setvarvalue(
|
|
||||||
curint,
|
|
||||||
self.bdd.nodes[self.stmts[pos].var].var().value(),
|
|
||||||
false,
|
|
||||||
) {
|
|
||||||
interpretation.clone_from(&n);
|
|
||||||
change = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Term::TOP => {
|
|
||||||
if let Some(n) = self.setvarvalue(
|
|
||||||
curint,
|
|
||||||
self.bdd.nodes[self.stmts[pos].var].var().value(),
|
|
||||||
true,
|
|
||||||
) {
|
|
||||||
interpretation.clone_from(&n);
|
|
||||||
change = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
_ => (),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if !change {
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
interpretation
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Function not working - do not use
|
|
||||||
pub(crate) fn _complete(&mut self) -> Vec<Vec<usize>> {
|
|
||||||
let base_int = self.cur_interpretation();
|
|
||||||
let mut complete: Vec<Vec<usize>> = Vec::new();
|
|
||||||
let mut change: bool;
|
|
||||||
let mut pos: usize = 0;
|
|
||||||
let mut cache: HashMap<Vec<usize>, usize> = HashMap::new();
|
|
||||||
|
|
||||||
// compute grounded interpretation
|
|
||||||
complete.push(self.compute_fixpoint(base_int.as_ref()).unwrap());
|
|
||||||
loop {
|
|
||||||
change = false;
|
|
||||||
let interpr = complete.get(pos).unwrap().clone();
|
|
||||||
for (pos, it) in interpr.iter().enumerate() {
|
|
||||||
if *it > 1 {
|
|
||||||
let mut int1 = interpr.clone();
|
|
||||||
int1[pos] = 0;
|
|
||||||
if let Some(n) = self.compute_fixpoint(int1.as_ref()) {
|
|
||||||
if !cache.contains_key(&n) {
|
|
||||||
cache.insert(n.clone(), complete.len());
|
|
||||||
complete.push(n);
|
|
||||||
change = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
int1[pos] = 1;
|
|
||||||
if let Some(n) = self.compute_fixpoint(int1.as_ref()) {
|
|
||||||
if !cache.contains_key(&n) {
|
|
||||||
cache.insert(n.clone(), complete.len());
|
|
||||||
complete.push(n);
|
|
||||||
change = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if !change {
|
|
||||||
break;
|
|
||||||
};
|
};
|
||||||
pos += 1;
|
(0..parser.namelist_rc_refcell().borrow().len())
|
||||||
// println!("{}",complete.len());
|
.into_iter()
|
||||||
}
|
.for_each(|value| {
|
||||||
complete
|
log::trace!("adding variable {}", Var(value));
|
||||||
|
result.bdd.variable(Var(value));
|
||||||
|
});
|
||||||
|
log::debug!("[Start] adding acs");
|
||||||
|
parser
|
||||||
|
.formula_order()
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.for_each(|(insert_order, new_order)| {
|
||||||
|
log::trace!(
|
||||||
|
"Pos {}/{} formula {}, {:?}",
|
||||||
|
insert_order + 1,
|
||||||
|
parser.formula_count(),
|
||||||
|
new_order,
|
||||||
|
parser.ac_at(insert_order)
|
||||||
|
);
|
||||||
|
let result_term = result.term(&parser.ac_at(insert_order).unwrap());
|
||||||
|
result.ac[*new_order] = result_term;
|
||||||
|
});
|
||||||
|
log::info!("[Success] instantiated");
|
||||||
|
result
|
||||||
}
|
}
|
||||||
|
|
||||||
/// represents the starting interpretation due to the acceptance conditions. (i.e. the currently represented set of formulae)
|
fn term(&mut self, formula: &Formula) -> Term {
|
||||||
pub fn cur_interpretation(&self) -> Vec<usize> {
|
match formula {
|
||||||
let mut interpretation: Vec<usize> = Vec::new();
|
Formula::Bot => Bdd::constant(false),
|
||||||
for it in self.stmts.iter() {
|
Formula::Top => Bdd::constant(true),
|
||||||
interpretation.push((*it).ac.unwrap())
|
Formula::Atom(val) => {
|
||||||
|
let t1 = self.ordering.variable(val).unwrap();
|
||||||
|
self.bdd.variable(t1)
|
||||||
|
}
|
||||||
|
Formula::Not(val) => {
|
||||||
|
let t1 = self.term(val);
|
||||||
|
self.bdd.not(t1)
|
||||||
|
}
|
||||||
|
Formula::And(val1, val2) => {
|
||||||
|
let t1 = self.term(val1);
|
||||||
|
let t2 = self.term(val2);
|
||||||
|
self.bdd.and(t1, t2)
|
||||||
|
}
|
||||||
|
Formula::Or(val1, val2) => {
|
||||||
|
let t1 = self.term(val1);
|
||||||
|
let t2 = self.term(val2);
|
||||||
|
self.bdd.or(t1, t2)
|
||||||
|
}
|
||||||
|
Formula::Iff(val1, val2) => {
|
||||||
|
let t1 = self.term(val1);
|
||||||
|
let t2 = self.term(val2);
|
||||||
|
self.bdd.iff(t1, t2)
|
||||||
|
}
|
||||||
|
Formula::Xor(val1, val2) => {
|
||||||
|
let t1 = self.term(val1);
|
||||||
|
let t2 = self.term(val2);
|
||||||
|
self.bdd.xor(t1, t2)
|
||||||
|
}
|
||||||
|
Formula::Imp(val1, val2) => {
|
||||||
|
let t1 = self.term(val1);
|
||||||
|
let t2 = self.term(val2);
|
||||||
|
self.bdd.imp(t1, t2)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
interpretation
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Given an Interpretation, follow the `Γ`-Operator to a fixpoint. Returns `None` if no valid fixpoint can be reached from the given interpretation and
|
/// Computes the grounded extension and returns it as a list
|
||||||
/// the interpretation which represents the fixpoint otherwise.
|
pub fn grounded(&mut self) -> Vec<Term> {
|
||||||
#[allow(clippy::ptr_arg)]
|
log::info!("[Start] grounded");
|
||||||
pub fn compute_fixpoint(&mut self, interpretation: &Vec<usize>) -> Option<Vec<usize>> {
|
let mut t_vals: usize =
|
||||||
let new_interpretation = self.apply_interpretation(interpretation.as_ref());
|
self.ac.iter().fold(
|
||||||
match Adf::information_enh(interpretation, new_interpretation.as_ref()) {
|
0,
|
||||||
Some(n) => {
|
|acc, elem| {
|
||||||
if n {
|
if elem.is_truth_value() {
|
||||||
self.compute_fixpoint(new_interpretation.as_ref())
|
acc + 1
|
||||||
} else {
|
} else {
|
||||||
Some(new_interpretation)
|
acc
|
||||||
|
}
|
||||||
|
},
|
||||||
|
);
|
||||||
|
let mut new_interpretation = self.ac.clone();
|
||||||
|
loop {
|
||||||
|
let old_t_vals = t_vals;
|
||||||
|
for ac in new_interpretation
|
||||||
|
.iter_mut()
|
||||||
|
.filter(|term| !term.is_truth_value())
|
||||||
|
{
|
||||||
|
*ac = self.ac.iter().enumerate().fold(*ac, |acc, (var, term)| {
|
||||||
|
if term.is_truth_value() {
|
||||||
|
self.bdd.restrict(acc, Var(var), term.is_true())
|
||||||
|
} else {
|
||||||
|
acc
|
||||||
|
}
|
||||||
|
});
|
||||||
|
if ac.is_truth_value() {
|
||||||
|
t_vals += 1;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
None => None,
|
if t_vals == old_t_vals {
|
||||||
}
|
break;
|
||||||
}
|
|
||||||
|
|
||||||
#[allow(clippy::ptr_arg)]
|
|
||||||
fn apply_interpretation(&mut self, interpretation: &Vec<usize>) -> Vec<usize> {
|
|
||||||
let mut new_interpretation = interpretation.clone();
|
|
||||||
for (pos, it) in interpretation.iter().enumerate() {
|
|
||||||
match Term(*it) {
|
|
||||||
Term::BOT => {
|
|
||||||
if let Some(n) = self.setvarvalue(
|
|
||||||
new_interpretation.clone(),
|
|
||||||
self.bdd.nodes[self.stmts[pos].var].var().value(),
|
|
||||||
false,
|
|
||||||
) {
|
|
||||||
new_interpretation.clone_from(&n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Term::TOP => {
|
|
||||||
if let Some(n) = self.setvarvalue(
|
|
||||||
new_interpretation.clone(),
|
|
||||||
self.bdd.nodes[self.stmts[pos].var].var().value(),
|
|
||||||
true,
|
|
||||||
) {
|
|
||||||
new_interpretation.clone_from(&n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
_ => (),
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
log::info!("[Done] grounded");
|
||||||
new_interpretation
|
new_interpretation
|
||||||
}
|
}
|
||||||
|
|
||||||
#[allow(clippy::ptr_arg)]
|
/// creates a [PrintableInterpretation] for output purposes
|
||||||
fn information_enh(i1: &Vec<usize>, i2: &Vec<usize>) -> Option<bool> {
|
pub fn print_interpretation<'a, 'b>(
|
||||||
let mut enhanced = false;
|
&'a self,
|
||||||
for i in 0..i1.len() {
|
interpretation: &'b [Term],
|
||||||
if i1[i] < 2 {
|
) -> PrintableInterpretation<'b>
|
||||||
if i1[i] != i2[i] {
|
where
|
||||||
return None;
|
'a: 'b,
|
||||||
}
|
{
|
||||||
} else if (i1[i] >= 2) & (i2[i] < 2) {
|
PrintableInterpretation::new(interpretation, &self.ordering)
|
||||||
enhanced = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Some(enhanced)
|
|
||||||
}
|
|
||||||
|
|
||||||
fn setvarvalue(
|
|
||||||
&mut self,
|
|
||||||
interpretation: Vec<usize>,
|
|
||||||
var: usize,
|
|
||||||
val: bool,
|
|
||||||
) -> Option<Vec<usize>> {
|
|
||||||
let mut interpretation2: Vec<usize> = vec![0; interpretation.len()];
|
|
||||||
let mut change: bool = false;
|
|
||||||
for (pos, _it) in interpretation.iter().enumerate() {
|
|
||||||
interpretation2[pos] = self
|
|
||||||
.bdd
|
|
||||||
.restrict(Term(interpretation[pos]), Var(var), val)
|
|
||||||
.value();
|
|
||||||
if interpretation[pos] != interpretation2[pos] {
|
|
||||||
change = true
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if change {
|
|
||||||
Some(interpretation2)
|
|
||||||
} else {
|
|
||||||
None
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn parse_formula(&mut self, ac: &str) -> usize {
|
|
||||||
if ac.len() > 3 {
|
|
||||||
match &ac[..4] {
|
|
||||||
"and(" => {
|
|
||||||
let (left, right) = Adf::findpairs(&ac[4..]);
|
|
||||||
let lterm: Term = self.parse_formula(left).into();
|
|
||||||
let rterm: Term = self.parse_formula(right).into();
|
|
||||||
return self.bdd.and(lterm, rterm).value();
|
|
||||||
}
|
|
||||||
"iff(" => {
|
|
||||||
let (left, right) = Adf::findpairs(&ac[4..]);
|
|
||||||
let lterm: Term = self.parse_formula(left).into();
|
|
||||||
let rterm: Term = self.parse_formula(right).into();
|
|
||||||
return self.bdd.iff(lterm, rterm).value();
|
|
||||||
}
|
|
||||||
"xor(" => {
|
|
||||||
let (left, right) = Adf::findpairs(&ac[4..]);
|
|
||||||
let lterm: Term = self.parse_formula(left).into();
|
|
||||||
let rterm: Term = self.parse_formula(right).into();
|
|
||||||
return self.bdd.xor(lterm, rterm).value();
|
|
||||||
}
|
|
||||||
"imp(" => {
|
|
||||||
let (left, right) = Adf::findpairs(&ac[4..]);
|
|
||||||
let lterm: Term = self.parse_formula(left).into();
|
|
||||||
let rterm: Term = self.parse_formula(right).into();
|
|
||||||
return self.bdd.imp(lterm, rterm).value();
|
|
||||||
}
|
|
||||||
"neg(" => {
|
|
||||||
let pos = Adf::findterm(&ac[4..]).unwrap() + 4;
|
|
||||||
let term: Term = self.parse_formula(&ac[4..pos]).into();
|
|
||||||
return self.bdd.not(term).value();
|
|
||||||
}
|
|
||||||
"c(f)" => return Bdd::constant(false).value(),
|
|
||||||
"c(v)" => return Bdd::constant(true).value(),
|
|
||||||
_ if &ac[..3] == "or(" => {
|
|
||||||
let (left, right) = Adf::findpairs(&ac[3..]);
|
|
||||||
let lterm: Term = self.parse_formula(left).into();
|
|
||||||
let rterm: Term = self.parse_formula(right).into();
|
|
||||||
return self.bdd.or(lterm, rterm).value();
|
|
||||||
}
|
|
||||||
_ => (),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
match self.dict.get(ac) {
|
|
||||||
Some(it) => self.bdd.variable(Var(*it)).value(),
|
|
||||||
_ => {
|
|
||||||
println!("{}", ac);
|
|
||||||
unreachable!()
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Given a pair of literals, returns both literals as strings
|
|
||||||
/// # Example
|
|
||||||
/// ```rust
|
|
||||||
/// use adf_bdd::adf::Adf;
|
|
||||||
/// assert_eq!(Adf::findpairs("a,or(b,c))"), ("a", "or(b,c)"));
|
|
||||||
/// assert_eq!(Adf::findpairs("a,or(b,c)"), ("a", "or(b,c)"));
|
|
||||||
/// ```
|
|
||||||
pub fn findpairs(formula: &str) -> (&str, &str) {
|
|
||||||
let lpos = Adf::findterm(formula).unwrap();
|
|
||||||
let rpos = Adf::findterm(&formula[lpos + 1..]).unwrap() + lpos;
|
|
||||||
(&formula[..lpos], &formula[lpos + 1..rpos + 1])
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Returns the first term in the given slice as a string slice
|
|
||||||
/// # Example
|
|
||||||
/// ```rust
|
|
||||||
/// use adf_bdd::adf::Adf;
|
|
||||||
/// assert_eq!(Adf::findterm_str("formula"), "formula");
|
|
||||||
/// assert_eq!(Adf::findterm_str("and(a,b),or(a,b)"), "and(a,b)");
|
|
||||||
/// assert_eq!(Adf::findterm_str("neg(atom(a.d.ee))"), "neg(atom(a.d.ee))");
|
|
||||||
/// assert_eq!(Adf::findterm_str("formula)"), "formula");
|
|
||||||
/// ```
|
|
||||||
pub fn findterm_str(formula: &str) -> &str {
|
|
||||||
&formula[..Adf::findterm(formula).unwrap()]
|
|
||||||
}
|
|
||||||
|
|
||||||
fn findterm(formula: &str) -> Option<usize> {
|
|
||||||
let mut sqbrack: i16 = 0;
|
|
||||||
let mut cobrack: i16 = 0;
|
|
||||||
|
|
||||||
for (i, c) in formula.chars().enumerate() {
|
|
||||||
match c {
|
|
||||||
'(' => sqbrack += 1,
|
|
||||||
'[' => cobrack += 1,
|
|
||||||
',' => {
|
|
||||||
if sqbrack + cobrack == 0 {
|
|
||||||
return Some(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
')' => {
|
|
||||||
if sqbrack > 0 {
|
|
||||||
sqbrack -= 1;
|
|
||||||
} else {
|
|
||||||
return Some(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
']' => {
|
|
||||||
if cobrack > 0 {
|
|
||||||
cobrack -= 1;
|
|
||||||
} else {
|
|
||||||
return Some(i);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
_ => (),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Some(formula.len())
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod test {
|
mod test {
|
||||||
use super::*;
|
use super::*;
|
||||||
|
use test_log::test;
|
||||||
#[test]
|
#[test]
|
||||||
fn add_statement() {
|
fn from_parser() {
|
||||||
let mut adf = Adf::new();
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).s(e).s(d).ac(d,iff(imp(a,b),c)).ac(e,xor(d,e)).";
|
||||||
|
|
||||||
adf.add_statement("A");
|
parser.parse()(input).unwrap();
|
||||||
adf.add_statement("B");
|
|
||||||
adf.add_statement("A");
|
|
||||||
|
|
||||||
assert_eq!(adf.stmts.len(), 2);
|
let adf = Adf::from_parser(&parser);
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[1], "c");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[2], "b");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[3], "e");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[4], "d");
|
||||||
|
|
||||||
adf.add_statement("C");
|
assert_eq!(adf.ac, vec![Term(4), Term(2), Term(7), Term(15), Term(12)]);
|
||||||
assert_eq!(adf.stmts.len(), 3);
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).s(e).s(d).ac(d,iff(imp(a,b),c)).ac(e,xor(d,e)).";
|
||||||
|
|
||||||
|
parser.parse()(input).unwrap();
|
||||||
|
parser.varsort_alphanum();
|
||||||
|
|
||||||
|
let adf = Adf::from_parser(&parser);
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[0], "a");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[1], "b");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[2], "c");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[3], "d");
|
||||||
|
assert_eq!(adf.ordering.names().as_ref().borrow()[4], "e");
|
||||||
|
|
||||||
|
assert_eq!(adf.ac, vec![Term(3), Term(7), Term(2), Term(11), Term(13)]);
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn parse_formula() {
|
fn complete() {
|
||||||
let mut adf = Adf::new();
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()("s(a).s(b).s(c).s(d).ac(a,c(v)).ac(b,b).ac(c,and(a,b)).ac(d,neg(b)).\ns(e).ac(e,and(b,or(neg(b),c(f)))).s(f).\n\nac(f,xor(a,e)).")
|
||||||
|
.unwrap();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
let result = adf.grounded();
|
||||||
|
|
||||||
adf.add_statement("a");
|
assert_eq!(
|
||||||
adf.add_statement("b");
|
result,
|
||||||
adf.add_statement("c");
|
vec![Term(1), Term(3), Term(3), Term(9), Term(0), Term(1)]
|
||||||
|
);
|
||||||
assert_eq!(adf.parse_formula("and(a,or(b,c))"), 6);
|
assert_eq!(
|
||||||
assert_eq!(adf.parse_formula("xor(a,b)"), 8);
|
format!("{}", adf.print_interpretation(&result)),
|
||||||
assert_eq!(adf.parse_formula("or(c(f),b)"), 3); // is b
|
"T(a) u(b) u(c) u(d) F(e) T(f) \n"
|
||||||
|
);
|
||||||
adf.parse_formula("and(or(c(f),a),and(b,c))");
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
#[should_panic]
|
|
||||||
fn parse_formula_panic() {
|
|
||||||
let mut adf = Adf::new();
|
|
||||||
|
|
||||||
adf.add_statement("a");
|
|
||||||
adf.add_statement("b");
|
|
||||||
adf.add_statement("c");
|
|
||||||
|
|
||||||
adf.parse_formula("and(a,or(b,d))");
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn findterm() {
|
|
||||||
assert_eq!(Adf::findterm("formula"), Some(7));
|
|
||||||
assert_eq!(Adf::findterm("and(a,b),or(a,b)"), Some(8));
|
|
||||||
assert_eq!(Adf::findterm("neg(atom(a.d.ee))"), Some(17));
|
|
||||||
assert_eq!(Adf::findterm("formula)"), Some(7));
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn findpairs() {
|
|
||||||
assert_eq!(Adf::findpairs("a,or(b,c))"), ("a", "or(b,c)"));
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
|
||||||
fn init_statements() {
|
|
||||||
let mut adf = Adf::new();
|
|
||||||
|
|
||||||
let stmts: Vec<&str> = vec!["a", "b", "c", "extra long text type statement"];
|
|
||||||
|
|
||||||
assert_eq!(adf.init_statements(stmts), 4);
|
|
||||||
assert_eq!(adf.stmts[3].label, "extra long text type statement");
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
118
src/datatypes.rs
118
src/datatypes.rs
@ -1,114 +1,4 @@
|
|||||||
use std::{fmt::Display, ops::Deref};
|
//! A collection of all the necessary datatypes of the system.
|
||||||
|
pub mod adf;
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)]
|
mod bdd;
|
||||||
pub struct Term(pub usize);
|
pub use bdd::*;
|
||||||
|
|
||||||
impl Deref for Term {
|
|
||||||
type Target = usize;
|
|
||||||
fn deref(&self) -> &Self::Target {
|
|
||||||
&self.0
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl From<usize> for Term {
|
|
||||||
fn from(val: usize) -> Self {
|
|
||||||
Self(val)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Display for Term {
|
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
|
||||||
write!(f, "Term({})", self.0)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Term {
|
|
||||||
pub const BOT: Term = Term(0);
|
|
||||||
pub const TOP: Term = Term(1);
|
|
||||||
|
|
||||||
pub fn new(val: usize) -> Term {
|
|
||||||
Term(val)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn value(self) -> usize {
|
|
||||||
self.0
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
|
||||||
pub struct Var(pub usize);
|
|
||||||
|
|
||||||
impl Deref for Var {
|
|
||||||
type Target = usize;
|
|
||||||
fn deref(&self) -> &Self::Target {
|
|
||||||
&self.0
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl From<usize> for Var {
|
|
||||||
fn from(val: usize) -> Self {
|
|
||||||
Self(val)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Display for Var {
|
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
|
||||||
write!(f, "Var({})", self.0)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Var {
|
|
||||||
pub const TOP: Var = Var(usize::MAX);
|
|
||||||
pub const BOT: Var = Var(usize::MAX - 1);
|
|
||||||
|
|
||||||
pub fn value(self) -> usize {
|
|
||||||
self.0
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
|
||||||
pub(crate) struct BddNode {
|
|
||||||
var: Var,
|
|
||||||
lo: Term,
|
|
||||||
hi: Term,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Display for BddNode {
|
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
|
||||||
write!(f, "BddNode: {}, lo: {}, hi: {}", self.var, self.lo, self.hi)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl BddNode {
|
|
||||||
pub fn new(var: Var, lo: Term, hi: Term) -> Self {
|
|
||||||
Self { var, lo, hi }
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn var(self) -> Var {
|
|
||||||
self.var
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn lo(self) -> Term {
|
|
||||||
self.lo
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn hi(self) -> Term {
|
|
||||||
self.hi
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn bot_node() -> Self {
|
|
||||||
Self {
|
|
||||||
var: Var::BOT,
|
|
||||||
lo: Term::BOT,
|
|
||||||
hi: Term::BOT,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn top_node() -> Self {
|
|
||||||
Self {
|
|
||||||
var: Var::TOP,
|
|
||||||
lo: Term::TOP,
|
|
||||||
hi: Term::TOP,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|||||||
87
src/datatypes/adf.rs
Normal file
87
src/datatypes/adf.rs
Normal file
@ -0,0 +1,87 @@
|
|||||||
|
//! Repesentation of all needed ADF based datatypes
|
||||||
|
|
||||||
|
use std::{cell::RefCell, collections::HashMap, fmt::Display, rc::Rc};
|
||||||
|
|
||||||
|
use super::{Term, Var};
|
||||||
|
|
||||||
|
pub(crate) struct VarContainer {
|
||||||
|
names: Rc<RefCell<Vec<String>>>,
|
||||||
|
mapping: Rc<RefCell<HashMap<String, usize>>>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Default for VarContainer {
|
||||||
|
fn default() -> Self {
|
||||||
|
VarContainer {
|
||||||
|
names: Rc::new(RefCell::new(Vec::new())),
|
||||||
|
mapping: Rc::new(RefCell::new(HashMap::new())),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl VarContainer {
|
||||||
|
pub fn from_parser(
|
||||||
|
names: Rc<RefCell<Vec<String>>>,
|
||||||
|
mapping: Rc<RefCell<HashMap<String, usize>>>,
|
||||||
|
) -> VarContainer {
|
||||||
|
VarContainer { names, mapping }
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn variable(&self, name: &str) -> Option<Var> {
|
||||||
|
self.mapping.borrow().get(name).map(|val| Var(*val))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn name(&self, var: Var) -> Option<String> {
|
||||||
|
self.names.borrow().get(var.value()).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn names(&self) -> Rc<RefCell<Vec<String>>> {
|
||||||
|
Rc::clone(&self.names)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// A struct to print a representation, it will be instantiated by [Adf] by calling the method [`Adf::print_interpretation`].
|
||||||
|
pub struct PrintableInterpretation<'a> {
|
||||||
|
interpretation: &'a [Term],
|
||||||
|
ordering: &'a VarContainer,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a> PrintableInterpretation<'a> {
|
||||||
|
pub(crate) fn new(interpretation: &'a [Term], ordering: &'a VarContainer) -> Self {
|
||||||
|
Self {
|
||||||
|
interpretation,
|
||||||
|
ordering,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Display for PrintableInterpretation<'_> {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
self.interpretation
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.for_each(|(pos, term)| {
|
||||||
|
if term.is_truth_value() {
|
||||||
|
if term.is_true() {
|
||||||
|
write!(f, "T(").expect("writing Interpretation failed!");
|
||||||
|
} else {
|
||||||
|
write!(f, "F(").expect("writing Interpretation failed!");
|
||||||
|
}
|
||||||
|
} else {
|
||||||
|
write!(f, "u(").expect("writing Interpretation failed!");
|
||||||
|
}
|
||||||
|
write!(f, "{}) ", self.ordering.name(Var(pos)).unwrap())
|
||||||
|
.expect("writing Interpretation failed!");
|
||||||
|
});
|
||||||
|
writeln!(f)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#[cfg(test)]
|
||||||
|
mod test {
|
||||||
|
use super::*;
|
||||||
|
#[test]
|
||||||
|
fn init_varcontainer() {
|
||||||
|
let vc = VarContainer::default();
|
||||||
|
assert_eq!(vc.variable("foo"), None);
|
||||||
|
}
|
||||||
|
}
|
||||||
146
src/datatypes/bdd.rs
Normal file
146
src/datatypes/bdd.rs
Normal file
@ -0,0 +1,146 @@
|
|||||||
|
//! To represent a BDD, a couple of datatypes is needed.
|
||||||
|
//! This module consists of all internally and externally used datatypes, such as
|
||||||
|
//! [Term], [Var], and [BddNode]
|
||||||
|
use std::{fmt::Display, ops::Deref};
|
||||||
|
|
||||||
|
/// Representation of a Term
|
||||||
|
/// Each Term is represented in a number ([usize]) and relates to a
|
||||||
|
/// Node in the decision diagram
|
||||||
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Copy, Clone)]
|
||||||
|
pub struct Term(pub usize);
|
||||||
|
|
||||||
|
impl Deref for Term {
|
||||||
|
type Target = usize;
|
||||||
|
fn deref(&self) -> &Self::Target {
|
||||||
|
&self.0
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl From<usize> for Term {
|
||||||
|
fn from(val: usize) -> Self {
|
||||||
|
Self(val)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Display for Term {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
write!(f, "Term({})", self.0)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Term {
|
||||||
|
/// Represents the truth-value bottom, i.e. false
|
||||||
|
pub const BOT: Term = Term(0);
|
||||||
|
/// Represents the truth-value top, i.e. true
|
||||||
|
pub const TOP: Term = Term(1);
|
||||||
|
|
||||||
|
/// Get the value of the Term, i.e. the corresponding [usize]
|
||||||
|
pub fn value(self) -> usize {
|
||||||
|
self.0
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Checks if the [Term] represents a truth-value ([Term::TOP] or [Term::BOT]), or
|
||||||
|
/// another compound formula.
|
||||||
|
pub fn is_truth_value(&self) -> bool {
|
||||||
|
self.0 <= Term::TOP.0
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns true, if the Term is true, i.e. [Term::TOP]
|
||||||
|
pub fn is_true(&self) -> bool {
|
||||||
|
*self == Self::TOP
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Representation of Variables
|
||||||
|
/// Note that the algorithm only uses [usize] values to identify variables.
|
||||||
|
/// The order of these values will be defining for the Variable order of the decision diagram.
|
||||||
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
||||||
|
pub struct Var(pub usize);
|
||||||
|
|
||||||
|
impl Deref for Var {
|
||||||
|
type Target = usize;
|
||||||
|
fn deref(&self) -> &Self::Target {
|
||||||
|
&self.0
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl From<usize> for Var {
|
||||||
|
fn from(val: usize) -> Self {
|
||||||
|
Self(val)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Display for Var {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
write!(f, "Var({})", self.0)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Var {
|
||||||
|
/// Represents the constant symbol "Top"
|
||||||
|
pub const TOP: Var = Var(usize::MAX);
|
||||||
|
/// Represents the constant symbol "Bot"
|
||||||
|
pub const BOT: Var = Var(usize::MAX - 1);
|
||||||
|
|
||||||
|
/// Returns the value of the [Var] as [usize]
|
||||||
|
pub fn value(self) -> usize {
|
||||||
|
self.0
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// A [BddNode] is representing one Node in the decision diagram
|
||||||
|
///
|
||||||
|
/// Intuitively this is a binary tree structure, where the diagram is allowed to
|
||||||
|
/// pool same values to the same Node.
|
||||||
|
#[derive(Debug, Eq, PartialEq, PartialOrd, Ord, Hash, Clone, Copy)]
|
||||||
|
pub(crate) struct BddNode {
|
||||||
|
var: Var,
|
||||||
|
lo: Term,
|
||||||
|
hi: Term,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Display for BddNode {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
write!(f, "BddNode: {}, lo: {}, hi: {}", self.var, self.lo, self.hi)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl BddNode {
|
||||||
|
/// Creates a new Node
|
||||||
|
pub fn new(var: Var, lo: Term, hi: Term) -> Self {
|
||||||
|
Self { var, lo, hi }
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns the current Variable-value
|
||||||
|
pub fn var(self) -> Var {
|
||||||
|
self.var
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns the `lo`-branch
|
||||||
|
pub fn lo(self) -> Term {
|
||||||
|
self.lo
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns the `hi`-branch
|
||||||
|
pub fn hi(self) -> Term {
|
||||||
|
self.hi
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Creates a node, which represents the `Bot`-truth value
|
||||||
|
pub fn bot_node() -> Self {
|
||||||
|
Self {
|
||||||
|
var: Var::BOT,
|
||||||
|
lo: Term::BOT,
|
||||||
|
hi: Term::BOT,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Creates a node, which represents the `Top`-truth value
|
||||||
|
pub fn top_node() -> Self {
|
||||||
|
Self {
|
||||||
|
var: Var::TOP,
|
||||||
|
lo: Term::TOP,
|
||||||
|
hi: Term::TOP,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
15
src/lib.rs
15
src/lib.rs
@ -31,7 +31,22 @@
|
|||||||
//! ac(c,neg(b)).
|
//! ac(c,neg(b)).
|
||||||
//! ac(d,d).
|
//! ac(d,d).
|
||||||
//! ```
|
//! ```
|
||||||
|
#![deny(
|
||||||
|
missing_copy_implementations,
|
||||||
|
trivial_casts,
|
||||||
|
trivial_numeric_casts,
|
||||||
|
unsafe_code
|
||||||
|
)]
|
||||||
|
#![warn(
|
||||||
|
missing_docs,
|
||||||
|
unused_import_braces,
|
||||||
|
unused_qualifications,
|
||||||
|
unused_extern_crates,
|
||||||
|
variant_size_differences
|
||||||
|
)]
|
||||||
|
|
||||||
pub mod adf;
|
pub mod adf;
|
||||||
pub mod datatypes;
|
pub mod datatypes;
|
||||||
pub mod obdd;
|
pub mod obdd;
|
||||||
|
pub mod parser;
|
||||||
//pub mod obdd2;
|
//pub mod obdd2;
|
||||||
|
|||||||
171
src/main.rs
171
src/main.rs
@ -1,17 +1,14 @@
|
|||||||
use std::fs::File;
|
|
||||||
use std::io::{self, BufRead};
|
|
||||||
use std::path::Path;
|
|
||||||
use std::time::Instant;
|
|
||||||
use std::usize;
|
|
||||||
|
|
||||||
pub mod adf;
|
pub mod adf;
|
||||||
pub mod datatypes;
|
pub mod datatypes;
|
||||||
pub mod obdd;
|
pub mod obdd;
|
||||||
|
pub mod parser;
|
||||||
|
|
||||||
|
use std::str::FromStr;
|
||||||
|
|
||||||
use adf::Adf;
|
use adf::Adf;
|
||||||
|
|
||||||
#[macro_use]
|
use clap::{clap_app, crate_authors, crate_description, crate_name, crate_version};
|
||||||
extern crate clap;
|
use parser::AdfParser;
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
let matches = clap_app!(myapp =>
|
let matches = clap_app!(myapp =>
|
||||||
@ -19,116 +16,66 @@ fn main() {
|
|||||||
(author: crate_authors!())
|
(author: crate_authors!())
|
||||||
(name: crate_name!())
|
(name: crate_name!())
|
||||||
(about: crate_description!())
|
(about: crate_description!())
|
||||||
(@arg fast: -f --fast "fast algorithm instead of the direct fixpoint-computation")
|
//(@arg fast: -f --fast "fast algorithm instead of the direct fixpoint-computation")
|
||||||
(@arg verbose: -v +multiple "Sets verbosity")
|
(@arg verbose: -v +multiple "Sets log verbosity")
|
||||||
(@arg INPUT: +required "Input file")
|
(@arg INPUT: +required "Input file")
|
||||||
|
(@group sorting =>
|
||||||
|
(@arg sort_lex: --lx "Sorts variables in a lexicographic manner")
|
||||||
|
(@arg sort_alphan: --an "Sorts variables in an alphanumeric manner")
|
||||||
)
|
)
|
||||||
.get_matches();
|
)
|
||||||
let verbose = matches.occurrences_of("verbose") > 0;
|
.get_matches_safe()
|
||||||
let start_time = Instant::now();
|
.unwrap_or_else(|e| match e.kind {
|
||||||
//let args: Vec<String> = env::args().collect();
|
clap::ErrorKind::HelpDisplayed => {
|
||||||
//if args.len() != 2 {
|
e.exit();
|
||||||
// eprintln!("No Filename given");
|
|
||||||
// exit(1);
|
|
||||||
//}
|
|
||||||
let mut statements: Vec<String> = Vec::new();
|
|
||||||
let mut ac: Vec<(String, String)> = Vec::new();
|
|
||||||
let path = Path::new(matches.value_of("INPUT").unwrap());
|
|
||||||
if let Ok(lines) = read_lines(path) {
|
|
||||||
for line in lines.flatten() {
|
|
||||||
//if let Ok(line) = resline {
|
|
||||||
//let slice = line.as_str();
|
|
||||||
if line.starts_with("s(") {
|
|
||||||
// let slice = line.as_str();
|
|
||||||
// statements.push(Adf::findterm_str(&slice[2..]).clone());
|
|
||||||
statements
|
|
||||||
.push(Adf::findterm_str(line.strip_prefix("s(").unwrap()).replace(" ", ""));
|
|
||||||
} else if line.starts_with("ac(") {
|
|
||||||
let (s, c) = Adf::findpairs(line.strip_prefix("ac(").unwrap());
|
|
||||||
ac.push((s.replace(" ", ""), c.replace(" ", "")));
|
|
||||||
}
|
}
|
||||||
//}
|
clap::ErrorKind::VersionDisplayed => {
|
||||||
|
e.exit();
|
||||||
}
|
}
|
||||||
}
|
|
||||||
|
|
||||||
let file_read = start_time.elapsed();
|
|
||||||
let start_shortcut = Instant::now();
|
|
||||||
|
|
||||||
if verbose {
|
|
||||||
println!(
|
|
||||||
"parsed {} statements after {}ms",
|
|
||||||
statements.len(),
|
|
||||||
file_read.as_millis()
|
|
||||||
);
|
|
||||||
}
|
|
||||||
|
|
||||||
if !statements.is_empty() && !ac.is_empty() {
|
|
||||||
if matches.is_present("fast") {
|
|
||||||
let mut my_adf = Adf::new();
|
|
||||||
my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect());
|
|
||||||
for (s, c) in ac.clone() {
|
|
||||||
my_adf.add_ac(s.as_str(), c.as_str());
|
|
||||||
}
|
|
||||||
|
|
||||||
let result = my_adf.grounded();
|
|
||||||
print_interpretation(result);
|
|
||||||
if verbose {
|
|
||||||
println!("finished after {}ms", start_shortcut.elapsed().as_millis());
|
|
||||||
}
|
|
||||||
} else {
|
|
||||||
let start_fp = Instant::now();
|
|
||||||
|
|
||||||
let mut my_adf = Adf::default();
|
|
||||||
my_adf.init_statements(statements.iter().map(AsRef::as_ref).collect());
|
|
||||||
for (s, c) in ac.clone() {
|
|
||||||
my_adf.add_ac(s.as_str(), c.as_str());
|
|
||||||
}
|
|
||||||
let empty_int = my_adf.cur_interpretation();
|
|
||||||
let result = my_adf.compute_fixpoint(empty_int.as_ref()).unwrap();
|
|
||||||
|
|
||||||
print_interpretation(result);
|
|
||||||
if verbose {
|
|
||||||
println!("finished after {}ms", start_fp.elapsed().as_millis());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
// optional test of complete extensions
|
|
||||||
// let mut my_adf3 = Adf::default();
|
|
||||||
// my_adf3.init_statements(statements.iter().map(AsRef::as_ref).collect());
|
|
||||||
// for (s, c) in ac.clone() {
|
|
||||||
// my_adf3.add_ac(s.as_str(), c.as_str());
|
|
||||||
// }
|
|
||||||
|
|
||||||
// let result3 = my_adf3.complete();
|
|
||||||
// for it in result3.iter() {
|
|
||||||
// print_interpretation(it.to_vec());
|
|
||||||
// }
|
|
||||||
// println!("{}",result3.len());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn read_lines<P>(filename: P) -> io::Result<io::Lines<io::BufReader<File>>>
|
|
||||||
where
|
|
||||||
P: AsRef<Path>,
|
|
||||||
{
|
|
||||||
let file = File::open(filename)?;
|
|
||||||
Ok(io::BufReader::new(file).lines())
|
|
||||||
}
|
|
||||||
|
|
||||||
fn print_interpretation(interpretation: Vec<usize>) {
|
|
||||||
let mut stable = true;
|
|
||||||
for it in interpretation.iter() {
|
|
||||||
match *it {
|
|
||||||
0 => print!("f"),
|
|
||||||
1 => print!("t"),
|
|
||||||
_ => {
|
_ => {
|
||||||
print!("u");
|
eprintln!("{} Version {{{}}}", crate_name!(), crate_version!());
|
||||||
stable = false
|
e.exit();
|
||||||
}
|
}
|
||||||
}
|
});
|
||||||
}
|
let filter_level = match matches.occurrences_of("verbose") {
|
||||||
if stable {
|
1 => log::LevelFilter::Info,
|
||||||
println!(" stm");
|
2 => log::LevelFilter::Debug,
|
||||||
|
3 => log::LevelFilter::Trace,
|
||||||
|
_ => {
|
||||||
|
match std::env::vars().find_map(|(var, val)| {
|
||||||
|
if var.eq("RUST_LOG") {
|
||||||
|
Some(log::LevelFilter::from_str(val.as_str()))
|
||||||
} else {
|
} else {
|
||||||
println!();
|
None
|
||||||
|
}
|
||||||
|
}) {
|
||||||
|
Some(v) => v.unwrap_or(log::LevelFilter::Error),
|
||||||
|
None => log::LevelFilter::Error,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
};
|
||||||
|
env_logger::builder().filter_level(filter_level).init();
|
||||||
|
log::info!("Version: {}", crate_version!());
|
||||||
|
|
||||||
|
let input = std::fs::read_to_string(
|
||||||
|
matches
|
||||||
|
.value_of("INPUT")
|
||||||
|
.expect("Input Filename should be given"),
|
||||||
|
)
|
||||||
|
.expect("Error Reading File");
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
parser.parse()(&input).unwrap();
|
||||||
|
log::info!("[Done] parsing");
|
||||||
|
|
||||||
|
if matches.is_present("sort_lex") {
|
||||||
|
parser.varsort_lexi();
|
||||||
|
}
|
||||||
|
if matches.is_present("sort_alphan") {
|
||||||
|
parser.varsort_alphanum();
|
||||||
|
}
|
||||||
|
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
let grounded = adf.grounded();
|
||||||
|
|
||||||
|
println!("{}", adf.print_interpretation(&grounded));
|
||||||
|
}
|
||||||
|
|||||||
@ -1,3 +1,4 @@
|
|||||||
|
//! Represents an obdd
|
||||||
use crate::datatypes::*;
|
use crate::datatypes::*;
|
||||||
use std::{cmp::min, collections::HashMap, fmt::Display};
|
use std::{cmp::min, collections::HashMap, fmt::Display};
|
||||||
|
|
||||||
@ -198,6 +199,9 @@ mod test {
|
|||||||
let v1 = bdd.variable(Var(0));
|
let v1 = bdd.variable(Var(0));
|
||||||
let v2 = bdd.variable(Var(1));
|
let v2 = bdd.variable(Var(1));
|
||||||
|
|
||||||
|
assert_eq!(v1, Term(2));
|
||||||
|
assert_eq!(v2, Term(3));
|
||||||
|
|
||||||
let t1 = bdd.and(v1, v2);
|
let t1 = bdd.and(v1, v2);
|
||||||
let nt1 = bdd.not(t1);
|
let nt1 = bdd.not(t1);
|
||||||
let ft = bdd.or(v1, nt1);
|
let ft = bdd.or(v1, nt1);
|
||||||
|
|||||||
479
src/parser.rs
Normal file
479
src/parser.rs
Normal file
@ -0,0 +1,479 @@
|
|||||||
|
//! A Parser for ADFs with all needed helper-methods.
|
||||||
|
//! It utilises the [nom-crate](https://crates.io/crates/nom)
|
||||||
|
use lexical_sort::{natural_lexical_cmp, StringSort};
|
||||||
|
use nom::{
|
||||||
|
branch::alt,
|
||||||
|
bytes::complete::{tag, take_until},
|
||||||
|
character::complete::{alphanumeric1, multispace0},
|
||||||
|
combinator::{all_consuming, value},
|
||||||
|
multi::many1,
|
||||||
|
sequence::{delimited, preceded, separated_pair, terminated},
|
||||||
|
IResult,
|
||||||
|
};
|
||||||
|
use std::{cell::RefCell, collections::HashMap, rc::Rc};
|
||||||
|
|
||||||
|
/// A representation of a formula, still using the strings from the input
|
||||||
|
#[derive(Clone, PartialEq, Eq)]
|
||||||
|
pub enum Formula<'a> {
|
||||||
|
/// c(v) in the input format
|
||||||
|
Bot,
|
||||||
|
/// c(f) in the input format
|
||||||
|
Top,
|
||||||
|
/// Some atomic variable in the input format
|
||||||
|
Atom(&'a str),
|
||||||
|
/// Negation of a subformula
|
||||||
|
Not(Box<Formula<'a>>),
|
||||||
|
/// Conjunction of two subformulae
|
||||||
|
And(Box<Formula<'a>>, Box<Formula<'a>>),
|
||||||
|
/// Disjunction of two subformulae
|
||||||
|
Or(Box<Formula<'a>>, Box<Formula<'a>>),
|
||||||
|
/// Implication of two subformulae
|
||||||
|
Imp(Box<Formula<'a>>, Box<Formula<'a>>),
|
||||||
|
/// Exclusive-Or of two subformulae
|
||||||
|
Xor(Box<Formula<'a>>, Box<Formula<'a>>),
|
||||||
|
/// If and only if connective between two formulae
|
||||||
|
Iff(Box<Formula<'a>>, Box<Formula<'a>>),
|
||||||
|
}
|
||||||
|
|
||||||
|
impl std::fmt::Debug for Formula<'_> {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
match self {
|
||||||
|
Formula::Atom(a) => {
|
||||||
|
write!(f, "{}", a)?;
|
||||||
|
}
|
||||||
|
Formula::Not(n) => {
|
||||||
|
write!(f, "not({:?})", n)?;
|
||||||
|
}
|
||||||
|
Formula::And(f1, f2) => {
|
||||||
|
write!(f, "and({:?},{:?})", f1, f2)?;
|
||||||
|
}
|
||||||
|
Formula::Or(f1, f2) => {
|
||||||
|
write!(f, "or({:?},{:?})", f1, f2)?;
|
||||||
|
}
|
||||||
|
Formula::Imp(f1, f2) => {
|
||||||
|
write!(f, "imp({:?},{:?})", f1, f2)?;
|
||||||
|
}
|
||||||
|
Formula::Xor(f1, f2) => {
|
||||||
|
write!(f, "xor({:?},{:?})", f1, f2)?;
|
||||||
|
}
|
||||||
|
Formula::Iff(f1, f2) => {
|
||||||
|
write!(f, "iff({:?},{:?})", f1, f2)?;
|
||||||
|
}
|
||||||
|
Formula::Bot => {
|
||||||
|
write!(f, "Const(B)")?;
|
||||||
|
}
|
||||||
|
Formula::Top => {
|
||||||
|
write!(f, "Const(T)")?;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
write!(f, "")
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// A parse structure to hold all the information given by the input file in one place
|
||||||
|
/// Due to an internal representation with [RefCell][std::cell::RefCell] and [Rc][std::rc::Rc] the values can be
|
||||||
|
/// handed over to other structures without further storage needs.
|
||||||
|
///
|
||||||
|
/// Note that the parser can be utilised by an [ADF][`crate::datatypes::adf::Adf`] to initialise it with minimal overhead.
|
||||||
|
pub struct AdfParser<'a> {
|
||||||
|
namelist: Rc<RefCell<Vec<String>>>,
|
||||||
|
dict: Rc<RefCell<HashMap<String, usize>>>,
|
||||||
|
formulae: RefCell<Vec<Formula<'a>>>,
|
||||||
|
formulaname: RefCell<Vec<String>>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Default for AdfParser<'_> {
|
||||||
|
fn default() -> Self {
|
||||||
|
AdfParser {
|
||||||
|
namelist: Rc::new(RefCell::new(Vec::new())),
|
||||||
|
dict: Rc::new(RefCell::new(HashMap::new())),
|
||||||
|
formulae: RefCell::new(Vec::new()),
|
||||||
|
formulaname: RefCell::new(Vec::new()),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a, 'b> AdfParser<'b>
|
||||||
|
where
|
||||||
|
'a: 'b,
|
||||||
|
{
|
||||||
|
fn parse_statements(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
||||||
|
move |input| {
|
||||||
|
let (rem, _) = many1(self.parse_statement())(input)?;
|
||||||
|
Ok((rem, ()))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Parses a full input file and creates internal structures.
|
||||||
|
/// Note that this method returns a closure (see the following Example for the correct usage).
|
||||||
|
/// # Example
|
||||||
|
/// ```
|
||||||
|
/// let parser = adf_bdd::parser::AdfParser::default();
|
||||||
|
/// parser.parse()("s(a).ac(a,c(v)).s(b).ac(b,a).s(c).ac(c,neg(b)).");
|
||||||
|
/// let adf = adf_bdd::adf::Adf::from_parser(&parser);
|
||||||
|
/// ```
|
||||||
|
pub fn parse(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
||||||
|
log::info!("[Start] parsing");
|
||||||
|
|input| {
|
||||||
|
value(
|
||||||
|
(),
|
||||||
|
all_consuming(many1(alt((self.parse_statement(), self.parse_ac())))),
|
||||||
|
)(input)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn parse_statement(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
||||||
|
|input| {
|
||||||
|
let mut dict = self.dict.borrow_mut();
|
||||||
|
let mut namelist = self.namelist.borrow_mut();
|
||||||
|
let (remain, statement) =
|
||||||
|
terminated(AdfParser::statement, terminated(tag("."), multispace0))(input)?;
|
||||||
|
if !dict.contains_key(statement) {
|
||||||
|
let pos = namelist.len();
|
||||||
|
namelist.push(String::from(statement));
|
||||||
|
dict.insert(namelist[pos].clone(), pos);
|
||||||
|
}
|
||||||
|
Ok((remain, ()))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn parse_ac(&'a self) -> impl FnMut(&'a str) -> IResult<&'a str, ()> {
|
||||||
|
|input| {
|
||||||
|
let (remain, (name, formula)) =
|
||||||
|
terminated(AdfParser::ac, terminated(tag("."), multispace0))(input)?;
|
||||||
|
self.formulae.borrow_mut().push(formula);
|
||||||
|
self.formulaname.borrow_mut().push(String::from(name));
|
||||||
|
Ok((remain, ()))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl AdfParser<'_> {
|
||||||
|
/// after an update to the namelist, all indizes are updated
|
||||||
|
fn regenerate_indizes(&self) {
|
||||||
|
self.namelist
|
||||||
|
.as_ref()
|
||||||
|
.borrow()
|
||||||
|
.iter()
|
||||||
|
.enumerate()
|
||||||
|
.for_each(|(i, elem)| {
|
||||||
|
self.dict.as_ref().borrow_mut().insert(elem.clone(), i);
|
||||||
|
});
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Sort the variables in lexicographical order.
|
||||||
|
/// Results which got used before might become corrupted.
|
||||||
|
pub fn varsort_lexi(&self) -> &Self {
|
||||||
|
self.namelist.as_ref().borrow_mut().sort_unstable();
|
||||||
|
self.regenerate_indizes();
|
||||||
|
self
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Sort the variables in alphanumerical order
|
||||||
|
/// Results which got used before might become corrupted.
|
||||||
|
pub fn varsort_alphanum(&self) -> &Self {
|
||||||
|
self.namelist
|
||||||
|
.as_ref()
|
||||||
|
.borrow_mut()
|
||||||
|
.string_sort_unstable(natural_lexical_cmp);
|
||||||
|
self.regenerate_indizes();
|
||||||
|
self
|
||||||
|
}
|
||||||
|
|
||||||
|
fn statement(input: &str) -> IResult<&str, &str> {
|
||||||
|
preceded(tag("s"), delimited(tag("("), AdfParser::atomic, tag(")")))(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn ac(input: &str) -> IResult<&str, (&str, Formula)> {
|
||||||
|
preceded(
|
||||||
|
tag("ac"),
|
||||||
|
delimited(
|
||||||
|
tag("("),
|
||||||
|
separated_pair(
|
||||||
|
AdfParser::atomic,
|
||||||
|
delimited(multispace0, tag(","), multispace0),
|
||||||
|
AdfParser::formula,
|
||||||
|
),
|
||||||
|
tag(")"),
|
||||||
|
),
|
||||||
|
)(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn atomic_term(input: &str) -> IResult<&str, Formula> {
|
||||||
|
AdfParser::atomic(input).map(|(input, result)| (input, Formula::Atom(result)))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula(input: &str) -> IResult<&str, Formula> {
|
||||||
|
alt((
|
||||||
|
AdfParser::constant,
|
||||||
|
AdfParser::binary_op,
|
||||||
|
AdfParser::unary_op,
|
||||||
|
AdfParser::atomic_term,
|
||||||
|
))(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn unary_op(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(
|
||||||
|
tag("neg"),
|
||||||
|
delimited(tag("("), AdfParser::formula, tag(")")),
|
||||||
|
)(input)
|
||||||
|
.map(|(input, result)| (input, Formula::Not(Box::new(result))))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn constant(input: &str) -> IResult<&str, Formula> {
|
||||||
|
alt((
|
||||||
|
preceded(tag("c"), delimited(tag("("), tag("v"), tag(")"))),
|
||||||
|
preceded(tag("c"), delimited(tag("("), tag("f"), tag(")"))),
|
||||||
|
))(input)
|
||||||
|
.map(|(input, result)| {
|
||||||
|
(
|
||||||
|
input,
|
||||||
|
match result {
|
||||||
|
"v" => Formula::Top,
|
||||||
|
"f" => Formula::Bot,
|
||||||
|
_ => unreachable!(),
|
||||||
|
},
|
||||||
|
)
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
fn formula_pair(input: &str) -> IResult<&str, (Formula, Formula)> {
|
||||||
|
separated_pair(
|
||||||
|
preceded(tag("("), AdfParser::formula),
|
||||||
|
delimited(multispace0, tag(","), multispace0),
|
||||||
|
terminated(AdfParser::formula, tag(")")),
|
||||||
|
)(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn and(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(tag("and"), AdfParser::formula_pair)(input)
|
||||||
|
.map(|(input, (f1, f2))| (input, Formula::And(Box::new(f1), Box::new(f2))))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn or(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(tag("or"), AdfParser::formula_pair)(input)
|
||||||
|
.map(|(input, (f1, f2))| (input, Formula::Or(Box::new(f1), Box::new(f2))))
|
||||||
|
}
|
||||||
|
fn imp(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(tag("imp"), AdfParser::formula_pair)(input)
|
||||||
|
.map(|(input, (f1, f2))| (input, Formula::Imp(Box::new(f1), Box::new(f2))))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn xor(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(tag("xor"), AdfParser::formula_pair)(input)
|
||||||
|
.map(|(input, (f1, f2))| (input, Formula::Xor(Box::new(f1), Box::new(f2))))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn iff(input: &str) -> IResult<&str, Formula> {
|
||||||
|
preceded(tag("iff"), AdfParser::formula_pair)(input)
|
||||||
|
.map(|(input, (f1, f2))| (input, Formula::Iff(Box::new(f1), Box::new(f2))))
|
||||||
|
}
|
||||||
|
|
||||||
|
fn binary_op(input: &str) -> IResult<&str, Formula> {
|
||||||
|
alt((
|
||||||
|
AdfParser::and,
|
||||||
|
AdfParser::or,
|
||||||
|
AdfParser::imp,
|
||||||
|
AdfParser::xor,
|
||||||
|
AdfParser::iff,
|
||||||
|
))(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
fn atomic(input: &str) -> IResult<&str, &str> {
|
||||||
|
alt((
|
||||||
|
delimited(tag("\""), take_until("\""), tag("\"")),
|
||||||
|
alphanumeric1,
|
||||||
|
))(input)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Allows insight of the number of parsed Statements
|
||||||
|
pub fn dict_size(&self) -> usize {
|
||||||
|
//self.dict.borrow().len()
|
||||||
|
self.dict.as_ref().borrow().len()
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns the number-representation and position of a given variable/statement in string-representation
|
||||||
|
pub fn dict_value(&self, value: &str) -> Option<usize> {
|
||||||
|
self.dict.as_ref().borrow().get(value).copied()
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Returns the acceptance condition of a statement at the given positon
|
||||||
|
pub fn ac_at(&self, idx: usize) -> Option<Formula> {
|
||||||
|
self.formulae.borrow().get(idx).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub(crate) fn dict_rc_refcell(&self) -> Rc<RefCell<HashMap<String, usize>>> {
|
||||||
|
Rc::clone(&self.dict)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub(crate) fn namelist_rc_refcell(&self) -> Rc<RefCell<Vec<String>>> {
|
||||||
|
Rc::clone(&self.namelist)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub(crate) fn formula_count(&self) -> usize {
|
||||||
|
self.formulae.borrow().len()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub(crate) fn formula_order(&self) -> Vec<usize> {
|
||||||
|
self.formulaname
|
||||||
|
.borrow()
|
||||||
|
.iter()
|
||||||
|
.map(|name| *self.dict.as_ref().borrow().get(name).unwrap())
|
||||||
|
.collect()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#[cfg(test)]
|
||||||
|
mod test {
|
||||||
|
|
||||||
|
use clap::ErrorKind;
|
||||||
|
|
||||||
|
use super::*;
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn atomic_parse() {
|
||||||
|
assert_eq!(
|
||||||
|
AdfParser::atomic("\" 123 21 ())) ((( {}||| asfjklj fsajfj039409u902 jfi a \""),
|
||||||
|
Ok((
|
||||||
|
"",
|
||||||
|
" 123 21 ())) ((( {}||| asfjklj fsajfj039409u902 jfi a "
|
||||||
|
))
|
||||||
|
);
|
||||||
|
assert_eq!(AdfParser::atomic("foo"), Ok(("", "foo")));
|
||||||
|
assert_eq!(AdfParser::atomic("foo()"), Ok(("()", "foo")));
|
||||||
|
assert_eq!(
|
||||||
|
AdfParser::atomic("()foo"),
|
||||||
|
Err(nom::Err::Error(nom::error::Error::new(
|
||||||
|
"()foo",
|
||||||
|
nom::error::ErrorKind::AlphaNumeric
|
||||||
|
)))
|
||||||
|
);
|
||||||
|
assert!(AdfParser::atomic(" adf").is_err());
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn statement_parse() {
|
||||||
|
assert_eq!(AdfParser::statement("s(ab)"), Ok(("", "ab")));
|
||||||
|
assert_eq!(AdfParser::statement("s(\"a b\")"), Ok(("", "a b")));
|
||||||
|
assert!(AdfParser::statement("s(a_b)").is_err());
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn parse_statement() {
|
||||||
|
let parser: AdfParser = AdfParser::default();
|
||||||
|
|
||||||
|
let input = "s(a). s(b). s(c).s(d).s(b).s(c).";
|
||||||
|
// many1(parser.parse_statement())(input).unwrap();
|
||||||
|
let (_remain, _) = parser.parse_statement()(input).unwrap();
|
||||||
|
assert_eq!(parser.dict_size(), 1);
|
||||||
|
assert_eq!(parser.dict_value("c"), None);
|
||||||
|
|
||||||
|
let (_remain, _) = parser.parse_statements()(input).unwrap();
|
||||||
|
assert_eq!(parser.dict_size(), 4);
|
||||||
|
assert_eq!(parser.dict_value("c"), Some(2usize));
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn parse_formula() {
|
||||||
|
let input = "and(or(neg(a),iff(\" iff left \",b)),xor(imp(c,d),e))";
|
||||||
|
let (_remain, result) = AdfParser::formula(input).unwrap();
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
format!("{:?}", result),
|
||||||
|
"and(or(not(a),iff( iff left ,b)),xor(imp(c,d),e))"
|
||||||
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
AdfParser::formula("and(c(v),c(f))").unwrap(),
|
||||||
|
(
|
||||||
|
"",
|
||||||
|
Formula::And(Box::new(Formula::Top), Box::new(Formula::Bot))
|
||||||
|
)
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn parse() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).";
|
||||||
|
|
||||||
|
let (remain, _) = parser.parse()(input).unwrap();
|
||||||
|
assert_eq!(remain, "");
|
||||||
|
assert_eq!(parser.dict_size(), 3);
|
||||||
|
assert_eq!(parser.dict_value("b"), Some(2usize));
|
||||||
|
assert_eq!(
|
||||||
|
format!("{:?}", parser.ac_at(1).unwrap()),
|
||||||
|
format!("{:?}", Formula::Not(Box::new(Formula::Atom("a"))))
|
||||||
|
);
|
||||||
|
assert_eq!(parser.formula_count(), 3);
|
||||||
|
assert_eq!(parser.formula_order(), vec![0, 2, 1]);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn non_consuming_parse() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))). wee";
|
||||||
|
|
||||||
|
let x = parser.parse()(input);
|
||||||
|
assert!(x.is_err());
|
||||||
|
assert_eq!(
|
||||||
|
x.err().unwrap(),
|
||||||
|
nom::Err::Error(nom::error::Error::new("wee", nom::error::ErrorKind::Eof))
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn constant() {
|
||||||
|
assert_eq!(AdfParser::constant("c(v)").unwrap().1, Formula::Top);
|
||||||
|
assert_eq!(AdfParser::constant("c(f)").unwrap().1, Formula::Bot);
|
||||||
|
assert_eq!(format!("{:?}", Formula::Top), "Const(T)");
|
||||||
|
assert_eq!(format!("{:?}", Formula::Bot), "Const(B)");
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn sort_updates() {
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a).s(c).ac(a,b).ac(b,neg(a)).s(b).ac(c,and(c(v),or(c(f),a))).";
|
||||||
|
|
||||||
|
parser.parse()(input).unwrap();
|
||||||
|
assert_eq!(parser.dict_value("a"), Some(0));
|
||||||
|
assert_eq!(parser.dict_value("b"), Some(2));
|
||||||
|
assert_eq!(parser.dict_value("c"), Some(1));
|
||||||
|
|
||||||
|
parser.varsort_lexi();
|
||||||
|
|
||||||
|
assert_eq!(parser.dict_value("a"), Some(0));
|
||||||
|
assert_eq!(parser.dict_value("b"), Some(1));
|
||||||
|
assert_eq!(parser.dict_value("c"), Some(2));
|
||||||
|
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let input = "s(a2).s(0).s(1).s(2).s(10).s(11).s(20).ac(0,c(v)).ac(1,c(v)).ac(2,c(v)).ac(10,c(v)).ac(20,c(v)).ac(11,c(v)).ac(a2,c(f)).";
|
||||||
|
|
||||||
|
parser.parse()(input).unwrap();
|
||||||
|
assert_eq!(parser.dict_value("a2"), Some(0));
|
||||||
|
assert_eq!(parser.dict_value("0"), Some(1));
|
||||||
|
assert_eq!(parser.dict_value("1"), Some(2));
|
||||||
|
assert_eq!(parser.dict_value("2"), Some(3));
|
||||||
|
assert_eq!(parser.dict_value("10"), Some(4));
|
||||||
|
assert_eq!(parser.dict_value("11"), Some(5));
|
||||||
|
assert_eq!(parser.dict_value("20"), Some(6));
|
||||||
|
|
||||||
|
parser.varsort_lexi();
|
||||||
|
assert_eq!(parser.dict_value("0"), Some(0));
|
||||||
|
assert_eq!(parser.dict_value("1"), Some(1));
|
||||||
|
assert_eq!(parser.dict_value("2"), Some(4));
|
||||||
|
assert_eq!(parser.dict_value("10"), Some(2));
|
||||||
|
assert_eq!(parser.dict_value("11"), Some(3));
|
||||||
|
assert_eq!(parser.dict_value("20"), Some(5));
|
||||||
|
assert_eq!(parser.dict_value("a2"), Some(6));
|
||||||
|
|
||||||
|
parser.varsort_alphanum();
|
||||||
|
assert_eq!(parser.dict_value("0"), Some(0));
|
||||||
|
assert_eq!(parser.dict_value("1"), Some(1));
|
||||||
|
assert_eq!(parser.dict_value("2"), Some(2));
|
||||||
|
assert_eq!(parser.dict_value("10"), Some(3));
|
||||||
|
assert_eq!(parser.dict_value("11"), Some(4));
|
||||||
|
assert_eq!(parser.dict_value("20"), Some(5));
|
||||||
|
assert_eq!(parser.dict_value("a2"), Some(6));
|
||||||
|
}
|
||||||
|
}
|
||||||
26
tests/automated.rs
Normal file
26
tests/automated.rs
Normal file
@ -0,0 +1,26 @@
|
|||||||
|
use adf_bdd::{adf::Adf, parser::AdfParser};
|
||||||
|
use test_generator::test_resources;
|
||||||
|
use test_log::test;
|
||||||
|
|
||||||
|
#[test_resources("res/adf-instances/instances/*.adf")]
|
||||||
|
fn compute_grounded(resource: &str) {
|
||||||
|
let grounded = &[
|
||||||
|
"res/adf-instances/grounded-interpretations/",
|
||||||
|
&resource[28..resource.len() - 8],
|
||||||
|
".apx.adf-grounded.txt",
|
||||||
|
]
|
||||||
|
.concat();
|
||||||
|
log::debug!("Grounded: {}", grounded);
|
||||||
|
let parser = AdfParser::default();
|
||||||
|
let expected_result = std::fs::read_to_string(grounded);
|
||||||
|
assert!(expected_result.is_ok());
|
||||||
|
let input = std::fs::read_to_string(resource).unwrap();
|
||||||
|
parser.parse()(&input).unwrap();
|
||||||
|
parser.varsort_alphanum();
|
||||||
|
let mut adf = Adf::from_parser(&parser);
|
||||||
|
let grounded = adf.grounded();
|
||||||
|
assert_eq!(
|
||||||
|
format!("{}", adf.print_interpretation(&grounded)),
|
||||||
|
expected_result.unwrap()
|
||||||
|
);
|
||||||
|
}
|
||||||
Loading…
x
Reference in New Issue
Block a user