1
0
mirror of https://github.com/ellmau/adf-obdd.git synced 2025-12-19 09:29:36 +01:00

21 Commits

Author SHA1 Message Date
Stefan Ellmauthaler
1596dc6818
Prepare files to publish the adf-bdd-bin package (#89)
* Prepare files to publish the adf-bdd-bin package
2022-08-02 15:09:48 +02:00
Stefan Ellmauthaler
d7e71e5da7
milestone/nogoods (#74)
* Add NoGood and NoGoodStore (#65)
* Update Flake to nix 22.05
* Add nogood-algorithm to the ADF
* Add public api for the nogood-learner
* Add direnv to gitignore
* Avoid a Box, support custom heuristics functions
* Add ng option with heu to binary
* Introduce a new flag to handle big instances (modelcount vs adhoccount)
Note that adhoccount without modelcount will not produce correct modelcounts if memoization is used
* Add new heuristic
* Add crossbeam-channel to represent an output-stream of stable models
Uses a crossbeam-channel to fill a Queue, which can be used safely
from outside the function.
This rework is done to also allow ad-hoc output of results in a
potentially multi-threaded setup.
* Added documentation on this new feature on the module-page
* Fix broken links in rust-doc
* Update Readme for lib to reflect the new NoGood API
* Add metadata to bin/Cargo.toml, add features
* added a benchmark feature, to easily compile benchmark-releases
* Fix facet count tests
* Add multithread-safe functionality for the dictionary/ordering
* Streamline a couple of API calls
* Expose more structs and methods to the public API
* Breaking some API (though nothing which is currently used in the binary)
* Simple version of gh pages
* Added more links and information to the landing page
* Fix badges in the app-doc
* Add two valued interpretation
Parameterised the stable-nogood algorithm to allow a variable
stability check function.
* Refactor nogood-algorithm name
* Update README.md and documentation (`docu` folder)
`README.md` on the `/` level is now presenting the same information
which is provided in `docs/index.md`
* Update main
- Update main functionality
- Update naming
* Fix cli-test
* Update Version to 0.3.0
Due to braking API changes and reaching a milestone, the version is
incremented to
0.3.0 (beta)
* Update Documentation navigation (#81)
* flake.lock: Update
Flake lock file updates:
• Updated input 'flake-utils':
    'github:numtide/flake-utils/1ed9fb1935d260de5fe1c2f7ee0ebaae17ed2fa1' (2022-05-30)
  → 'github:numtide/flake-utils/7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249' (2022-07-04)
• Updated input 'gitignoresrc':
    'github:hercules-ci/gitignore.nix/bff2832ec341cf30acb3a4d3e2e7f1f7b590116a' (2022-03-05)
  → 'github:hercules-ci/gitignore.nix/f2ea0f8ff1bce948ccb6b893d15d5ea3efaf1364' (2022-07-21)
• Updated input 'nixpkgs':
    'github:NixOS/nixpkgs/8b538fcb329a7bc3d153962f17c509ee49166973' (2022-06-15)
  → 'github:NixOS/nixpkgs/e43cf1748462c81202a32b26294e9f8eefcc3462' (2022-08-01)
• Updated input 'nixpkgs-unstable':
    'github:NixOS/nixpkgs/b1957596ff1c7aa8c55c4512b7ad1c9672502e8e' (2022-06-15)
  → 'github:NixOS/nixpkgs/7b9be38c7250b22d829ab6effdee90d5e40c6e5c' (2022-07-30)
• Updated input 'rust-overlay':
    'github:oxalica/rust-overlay/9eea93067eff400846c36f57b7499df9ef428ba0' (2022-06-17)
  → 'github:oxalica/rust-overlay/9055cb4f33f062c0dd33aa7e3c89140da8f70057' (2022-08-02)
* Add type alias for NoGood
Add a type alias `Interpretation` for NoGood to reflect the duality
where an Interpretation might become a NoGood.
* Add documentation information about later revisions on VarContainer

Co-authored-by: Maximilian Marx <mmarx@wh2.tu-dresden.de>
2022-08-02 14:02:00 +02:00
Stefan Ellmauthaler
6d09e71ba6
Add badges to readme (#61)
* Add badges to readme

* Format and reorder badges
2022-05-04 12:01:27 +02:00
9f4689ad45
Fix link location in all readme files for KBS 2022-04-28 09:51:26 +02:00
Stefan Ellmauthaler
43da337ce9
Add acknowledgements (#55)
Update Acknowledgements and Legal Disclaimer
2022-04-27 11:56:24 +02:00
Stefan Ellmauthaler
75a85203b0
Polish documentation (#51) 2022-04-21 14:18:59 +02:00
Stefan Ellmauthaler
081584e634
Update README.md
Fix links for badges and rephrased a weird sentence.
2022-03-16 15:25:47 +01:00
Stefan Ellmauthaler
6fb4acd46f
Add contribution information in Readme 2022-03-15 12:40:43 +01:00
Stefan Ellmauthaler
80915b1df8
code-style and documentation tidying (#34)
* Remove `unwrap()` from code
Remove `unwrap()` from the code (except tests).
Replaced it by either using `expect()` or handling the error more
gracefully.

* Improve documentation
Add examples on how to use the library
Add explanaitions on the dual use of crate::datatypes::Term
Relates to #33 

* Update README
* Add contributing guidelines
2022-03-14 21:05:53 +01:00
Stefan Ellmauthaler
c6837ff7eb
Feature/issue 22 extra binary (#24)
Split lib and bin into two directories

* modified workflow, readmes, documentation, ...
* excluded flake.lock from the package
* SET new patch version
2022-02-23 15:06:46 +01:00
Stefan Ellmauthaler
e110b72115
0.2.0 optimisations (#19)
Implemented various optimisations of the 0.2.0 version, including different filtering and rewriting approaches for model enumerations

* ADD prefilter for stable model computation (hybrid and naive)

* ADD implementation with one big rewritten formula instead of many

* ADD second version of bdd rewriting method

* FIX documentation, UPD flake

* UPD Readme, usage

* ADD hybrid options for grounded and transformation
2022-02-16 16:54:39 +01:00
Stefan Ellmauthaler
1edfe43985
Feature/issue 17 biodivine (#18)
State of the art BDD library, naive implementation, and Hybrid-approach available in the first beta-release version 0.2.0

* ADD biodivine as an obdd library to adf-obdd

* Implement restrict-wrapper on Biodivine

* Testcases changed to use biodivine for grounded.

* API unified

* ADD stable and complete with biodivine

* moved main.rs to bin folder

* ADD biodivine -> naive translation

* ADD hybrid approach
  instantiation + grounded by biodivine, then naive approach with memoization

* TIDY Readme, doc, tests
2022-01-27 12:23:12 +01:00
Stefan Ellmauthaler
9c9e85e107
Update README.md 2022-01-03 15:50:49 +01:00
Stefan Ellmauthaler
0d5577e251
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
2022-01-03 15:21:11 +01:00
92b111861b added badges to readme
Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
2021-07-21 10:53:15 +02:00
275adbe7f1 Tidied up the application
added documentation
added clap for program argument handling
fully clippy approved (except where it shall not be changed)
updated workflow for win and linux builds

Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
2021-07-20 16:51:14 +02:00
Stefan Ellmauthaler
68ab296171
Update README.md 2021-07-01 12:20:55 +02:00
Stefan Ellmauthaler
cfb82e8561
Update README.md 2021-07-01 12:20:45 +02:00
d4cbec0a76 First fully running version of the prototype
Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
2021-06-30 10:05:02 +02:00
7d9e99b900 first implementation of a restricted ordered bdd.
Signed-off-by: Stefan Ellmauthaler <stefan.ellmauthaler@tu-dresden.de>
2021-06-14 16:56:15 +02:00
Stefan Ellmauthaler
317a01a701
Initial commit 2021-06-11 12:31:36 +02:00