From 6387348e2ddedf625f1d458bd2a68b5295d9d12a Mon Sep 17 00:00:00 2001 From: Hannes Weichelt Date: Fri, 26 Apr 2024 22:05:02 +0200 Subject: [PATCH] Fixed formatting --- .github/workflows/deploy.yml | 2 +- .github/workflows/test.yml | 2 +- README.md | 120 ++++++++++-------- TODO.md | 92 +++++++------- examples/graph_coloring/README.md | 78 ++++++------ examples/graph_coloring/encoding.lp | 2 +- .../graph_coloring/graph_coloring_example.svg | 2 +- examples/graph_coloring/instance.lp | 2 +- examples/misc/bad_mucs.lp | 2 +- examples/misc/simple.lp | 2 +- examples/misc/soup.lp | 2 +- examples/misc/test/blob.lp | 2 +- examples/misc/test_inert.lp | 2 +- examples/misc/x.lp | 1 - examples/misc/zero_arity_assumptions.lp | 2 +- examples/queens/README.md | 26 ++-- examples/queens/encoding.lp | 2 +- examples/queens/instance.lp | 2 +- examples/queens/queens_example.svg | 2 +- examples/sudoku/README.md | 39 +++--- examples/sudoku/sudoku_example.svg | 2 +- src/clingexplaid/cli/clingo_app.py | 10 +- src/clingexplaid/muc/core_computer.py | 2 +- .../propagators/propagator_decision_order.py | 4 +- .../transformers/transformer_assumption.py | 2 +- .../transformers/transformer_constraint.py | 2 +- .../transformers/transformer_fact.py | 2 +- .../transformers/transformer_rule_splitter.py | 2 +- .../unsat_constraint_computer.py | 8 +- src/clingexplaid/utils/__init__.py | 6 +- src/clingexplaid/utils/types.py | 2 +- tests/clingexplaid/res/test_program.lp | 2 +- .../res/test_program_constants.lp | 2 +- .../res/test_program_constraints.lp | 2 +- .../res/test_program_decision_order.lp | 2 +- .../res/test_program_multi_muc.lp | 2 +- .../res/test_program_optimization.lp | 2 +- tests/clingexplaid/res/test_program_rules.lp | 2 +- .../res/test_program_unsat_constraints.lp | 2 +- .../transformed_program_assumptions_all.lp | 2 +- ..._program_assumptions_certain_signatures.lp | 2 +- .../res/transformed_program_constraints.lp | 2 +- .../res/transformed_program_constraints_id.lp | 2 +- .../res/transformed_program_facts.lp | 2 +- .../res/transformed_program_optimization.lp | 2 +- .../res/transformed_program_rule_ids.lp | 2 +- .../res/transformed_program_rules_split.lp | 2 +- tests/clingexplaid/test_muc.py | 4 +- tests/clingexplaid/test_transformers.py | 9 +- tests/clingexplaid/test_utils.py | 2 +- 50 files changed, 243 insertions(+), 230 deletions(-) diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 7eff365..16bd7b3 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -48,4 +48,4 @@ jobs: if: ${{ github.event_name == 'workflow_dispatch' }} uses: pypa/gh-action-pypi-publish@release/v1 with: - repository-url: "https://test.pypi.org/legacy/" \ No newline at end of file + repository-url: "https://test.pypi.org/legacy/" diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 7877cdf..a82da54 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -38,4 +38,4 @@ jobs: run: pre-commit run --all --show-diff-on-failure - name: run tests - run: nox \ No newline at end of file + run: nox diff --git a/README.md b/README.md index 873bb1b..2c1cc62 100644 --- a/README.md +++ b/README.md @@ -8,33 +8,37 @@ Run the following for basic usage information: clingexplaid -h ``` -The clingexplaid CLI (based on the `clingo.Application` class) can be called using this generic command. +The clingexplaid CLI (based on the `clingo.Application` class) can be called +using this generic command. ```bash clingexplaid ``` -+ ``: has to be replaced by a list of all files or a single filename -+ ``: defines how many models are computed (Default=`1`, All=`0`) -+ ``: specifies which Clingexplaid method is used (Required) - + Options: - + `--muc`: - + Computes the Minimal Unsatisfiable Cores (MUCs) of the provided unsatisfiable program - + `--unsat-constraints`: - + Computes the Unsatisfiable Constraints of the unsatisfiable program provided. - + `--show-decisions`: - + Visualizes the decision process of clasp -+ ``: Additional options for the different methods - + For `--muc`: - + `-a`, `--assumption-signature`: limits which facts of the current program are converted to choices/assumptions for - finding the MUCs (Default: all facts are converted) - + For `--show-decisions`: - + `--decision-signature`: limits which decisions are shown in the visualization (Default: all atom's decisions are - shown) +- ``: has to be replaced by a list of all files or a single filename +- ``: defines how many models are computed (Default=`1`, All=`0`) +- ``: specifies which Clingexplaid method is used (Required) + - Options: + - `--muc`: + - Computes the Minimal Unsatisfiable Cores (MUCs) of the provided + unsatisfiable program + - `--unsat-constraints`: + - Computes the Unsatisfiable Constraints of the unsatisfiable program + provided. + - `--show-decisions`: + - Visualizes the decision process of clasp +- ``: Additional options for the different methods + - For `--muc`: + - `-a`, `--assumption-signature`: limits which facts of the current program + are converted to choices/assumptions for finding the MUCs (Default: all + facts are converted) + - For `--show-decisions`: + - `--decision-signature`: limits which decisions are shown in the + visualization (Default: all atom's decisions are shown) ### Examples -+ A selection of examples can be found [here](examples) +- A selection of examples can be found [here](examples) ## Development @@ -46,7 +50,6 @@ To install the project, run pip install . ``` - To improve code quality, we run linters, type checkers, and unit tests. The tools can be run using [nox]. We recommend installing nox using [pipx] to have it available globally: @@ -108,32 +111,35 @@ This blackens the source code whenever `git commit` is used. **Important Notes:** -+ The Meta-encoding approach as it stands is not fully functional +- The Meta-encoding approach as it stands is not fully functional **Problem:** - + In the meta encoding all facts (or a selection matching a certain signature) are - transformed into assumptions which are then used as the assumption set for finding - the MUC - + During the MUC search when subsets of this assumption set are fixed for satisfiability - checking it is important that even though they are not fixed, the other assumptions - are not assumed as false but as undefined - + This is currently not possible with the meta-encoding, since assumptions are chosen - through a choice rule and all assumptions that aren't selected are defaulted to false - + This doesn't allow for properly checking if such subsets entail unsatisfiability and - thus prevents us from finding the proper MUCs + +- In the meta encoding all facts (or a selection matching a certain signature) + are transformed into assumptions which are then used as the assumption set + for finding the MUC +- During the MUC search when subsets of this assumption set are fixed for + satisfiability checking it is important that even though they are not fixed, + the other assumptions are not assumed as false but as undefined +- This is currently not possible with the meta-encoding, since assumptions are + chosen through a choice rule and all assumptions that aren't selected are + defaulted to false +- This doesn't allow for properly checking if such subsets entail + unsatisfiability and thus prevents us from finding the proper MUCs ### Specifying Assumption Set using only Signatures **Important Notes:** -+ clingo-explaid provides the `--muc` mode which gives you Minimal Unsatisfiable Cores for a given set of assumption - signatures that can be defined with `-a` -+ These signatures though allow not always for finding the best fitting MUC for a given encoding, compared - to an assumption set generated by hand +- clingo-explaid provides the `--muc` mode which gives you Minimal + Unsatisfiable Cores for a given set of assumption signatures that can be + defined with `-a` +- These signatures though allow not always for finding the best fitting MUC for + a given encoding, compared to an assumption set generated by hand **Problem:** -+ Imagine this [example encoding](examples/misc/bad_mucs.lp): +- Imagine this [example encoding](examples/misc/bad_mucs.lp): ```MATLAB a(1..3). @@ -143,41 +149,43 @@ unsat. :- unsat. ``` -+ So when I execute `clingexplaid examples/misc/bad_mucs.lp --muc 0` I get the MUCs: +- So when I execute `clingexplaid examples/misc/bad_mucs.lp --muc 0` I get the + MUCs: ``` -MUC 1 +MUC 1 a(3) -MUC 2 +MUC 2 a(2) -MUC 3 +MUC 3 a(1) -MUC 4 +MUC 4 unsat ``` -+ So you would generally expect that executing `clingexplaid examples/misc/bad_mucs.lp --muc 0 -a/1` would return the - first 3 found MUCs from before -+ But what actually happens is that there are no MUCs detected: +- So you would generally expect that executing + `clingexplaid examples/misc/bad_mucs.lp --muc 0 -a/1` would return the first + 3 found MUCs from before +- But what actually happens is that there are no MUCs detected: ``` NO MUCS CONTAINED: The unsatisfiability of this program is not induced by the provided assumptions UNSATISFIABLE ``` -+ This is actually due to an implicit `(unsat, False)` in the first 3 MUCs that isn't printed -+ Since the standard mode of `--muc` converts all facts to choices when no `-a` is provided `a(1)`, `a(2)`, `a(3)`, - and `unsat` are all converted to choices -+ We know that for the program to become satisfiable `unsat` cannot be true (line 4) -+ But since it is provided as a fact the choice rule conversion is necessary for the iterative deletion algorithm to - find any MUCs -+ This holds vice versa for the last MUC 4 just so that all `a/1` need to be converted to choice rules for the MUC to be - found +- This is actually due to an implicit `(unsat, False)` in the first 3 MUCs that + isn't printed +- Since the standard mode of `--muc` converts all facts to choices when no `-a` + is provided `a(1)`, `a(2)`, `a(3)`, and `unsat` are all converted to choices +- We know that for the program to become satisfiable `unsat` cannot be true + (line 4) +- But since it is provided as a fact the choice rule conversion is necessary + for the iterative deletion algorithm to find any MUCs +- This holds vice versa for the last MUC 4 just so that all `a/1` need to be + converted to choice rules for the MUC to be found - -[doc]: https://potassco.org/clingo/python-api/current/ +[black]: https://black.readthedocs.io/en/stable/ +[editable]: https://setuptools.pypa.io/en/latest/userguide/development_mode.html [nox]: https://nox.thea.codes/en/stable/index.html [pipx]: https://pypa.github.io/pipx/ [pre]: https://pre-commit.com/ -[black]: https://black.readthedocs.io/en/stable/ -[editable]: https://setuptools.pypa.io/en/latest/userguide/development_mode.html diff --git a/TODO.md b/TODO.md index 9c8f594..066d820 100644 --- a/TODO.md +++ b/TODO.md @@ -4,56 +4,60 @@ `2023` -+ [x] New CLI structure - + different modes: - + MUC - + UNSAT-CONSTRAINTS - + can be enabled through flags -+ [x] Iterative Deltion for Multiple MUCs - + variation of the QuickXplain algorithm : `SKIPPED` -+ [x] Finish unsat-constraints implementation for the API - +- [x] New CLI structure + - different modes: + - MUC + - UNSAT-CONSTRAINTS + - can be enabled through flags +- [x] Iterative Deltion for Multiple MUCs + - variation of the QuickXplain algorithm : `SKIPPED` +- [x] Finish unsat-constraints implementation for the API + `2024 - JAN` -+ [x] New option to enable verbose derivation output - + `--show-decisions` with more fine grained `--decision-signature` option -+ [x] Make `--show-decisions` its own mode -+ [x] Give a warning in Transformer if control is not grounded yet -+ [x] Documentation - + [x] Proper README - + [x] Docstrings for all API functions - + [x] CLI documentation with examples - + [x] Examples folder - + [x] Sudoku - + [x] Graph Coloring - + [x] N-Queens -+ [x] Error when calling `--muc` constants aren't properly kept: - + The problem was in `AssumptionTransformer` where get_assumptions didn't have proper access to constants defined over - the CL and the program constants -+ [x] `AssumptionTransformer` doesn't work properly on included files - + It actually did work fine +- [x] New option to enable verbose derivation output + - `--show-decisions` with more fine grained `--decision-signature` option +- [x] Make `--show-decisions` its own mode +- [x] Give a warning in Transformer if control is not grounded yet +- [x] Documentation + - [x] Proper README + - [x] Docstrings for all API functions + - [x] CLI documentation with examples + - [x] Examples folder + - [x] Sudoku + - [x] Graph Coloring + - [x] N-Queens +- [x] Error when calling `--muc` constants aren't properly kept: + - The problem was in `AssumptionTransformer` where get_assumptions didn't + have proper access to constants defined over the CL and the program + constants +- [x] `AssumptionTransformer` doesn't work properly on included files + - It actually did work fine `2024 - FEB` -+ [x] In `--show-decisions` hide INTERNAL when `--decision-signature` is active -+ [x] cleanup `DecisionOrderPropagator` print functions -+ [x] Features for `--unsat-constraints` - + [x] File + Line (Clickable link) -+ [x] Confusing Optimization prints during `--muc` when finding mucs in optimized Programs -+ [x] File-Link test with space in filename - + with `urllib.parsequote` -+ [x] Write up why negated assumptions in MUC's are a problem - + One which is currently not addressed by clingo-explaid -+ [x] Remove minimization also from `--unsat-constaints` mode -+ [x] Change file identification to use `clingo.ast.Location` instead of the subtring search and own built file tree -+ [x] Add spaces around Link to make it clickable on MAC +- [x] In `--show-decisions` hide INTERNAL when `--decision-signature` is active +- [x] cleanup `DecisionOrderPropagator` print functions +- [x] Features for `--unsat-constraints` + - [x] File + Line (Clickable link) +- [x] Confusing Optimization prints during `--muc` when finding mucs in + optimized Programs +- [x] File-Link test with space in filename + - with `urllib.parsequote` +- [x] Write up why negated assumptions in MUC's are a problem + - One which is currently not addressed by clingo-explaid +- [x] Remove minimization also from `--unsat-constaints` mode +- [x] Change file identification to use `clingo.ast.Location` instead of the + subtring search and own built file tree +- [x] Add spaces around Link to make it clickable on MAC `2024 - MAR` -+ [x] Add way for `-a` to allow for signatures without variables (`test/0`) - +- [x] Add way for `-a` to allow for signatures without variables (`test/0`) + ### Extra Features -+ [ ] `--unsat-constraints`: - + [ ] Access comments in the same line as constraint - + [ ] Currently, for multiline constraints a line number cannot be found -+ [ ] Timeout + +- [ ] `--unsat-constraints`: + - [ ] Access comments in the same line as constraint + - [ ] Currently, for multiline constraints a line number cannot be found +- [ ] Timeout diff --git a/examples/graph_coloring/README.md b/examples/graph_coloring/README.md index ac07418..3270dbd 100644 --- a/examples/graph_coloring/README.md +++ b/examples/graph_coloring/README.md @@ -1,9 +1,11 @@ # Example : Graph Coloring -+ This example encodes the classic graph coloring problem together with an unsatisfiable instance -+ Here for the sake of illustration some of the graph nodes are already assigned a color from the start, which is where the conflict occurs -+ Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable Cores (MUCs) and their respective unsatisfiable constraints - +- This example encodes the classic graph coloring problem together with an + unsatisfiable instance +- Here for the sake of illustration some of the graph nodes are already + assigned a color from the start, which is where the conflict occurs +- Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable + Cores (MUCs) and their respective unsatisfiable constraints ## Visualization @@ -11,49 +13,49 @@ ## Run -+ Finding all MUCs +- Finding all MUCs - ```bash - clingexplaid 0 encoding.lp instance.lp --muc -a assign/2 - ``` - - Expected Output: + ```bash + clingexplaid 0 encoding.lp instance.lp --muc -a assign/2 + ``` - ```bash - MUC 1 - assign(1,green) assign(5,red) assign(7,green) - MUC 2 - assign(1,green) assign(2,blue) assign(5,red) - ``` + Expected Output: -+ Finding the unsatisfiable constraints + ```bash + MUC 1 + assign(1,green) assign(5,red) assign(7,green) + MUC 2 + assign(1,green) assign(2,blue) assign(5,red) + ``` - ```bash - clingexplaid 0 encoding.lp instance.lp --unsat-constraints - ``` +- Finding the unsatisfiable constraints - Expected Output: + ```bash + clingexplaid 0 encoding.lp instance.lp --unsat-constraints + ``` - ```bash - Unsat Constraints - :- edge(N1,N2); assign(N1,C); assign(N2,C). - ``` + Expected Output: + + ```bash + Unsat Constraints + :- edge(N1,N2); assign(N1,C); assign(N2,C). + ``` + +- Combined call with unsatisfiable constraints for every found MUC -+ Combined call with unsatisfiable constraints for every found MUC ```bash clingexplaid 0 encoding.lp instance.lp --muc --unsat-constraints -a assign/2 ``` - - Expected Output: - ```bash - MUC 1 - assign(1,green) assign(5,red) assign(7,green) - ├── Unsat Constraints - ├──:- edge(N1,N2); assign(N1,C); assign(N2,C). - MUC 2 - assign(1,green) assign(2,blue) assign(5,red) - ├── Unsat Constraints - ├──:- edge(N1,N2); assign(N1,C); assign(N2,C). - ``` + Expected Output: + ```bash + MUC 1 + assign(1,green) assign(5,red) assign(7,green) + ├── Unsat Constraints + ├──:- edge(N1,N2); assign(N1,C); assign(N2,C). + MUC 2 + assign(1,green) assign(2,blue) assign(5,red) + ├── Unsat Constraints + ├──:- edge(N1,N2); assign(N1,C); assign(N2,C). + ``` diff --git a/examples/graph_coloring/encoding.lp b/examples/graph_coloring/encoding.lp index d8f947a..720b282 100644 --- a/examples/graph_coloring/encoding.lp +++ b/examples/graph_coloring/encoding.lp @@ -2,4 +2,4 @@ :- edge(N1, N2), assign(N1, C), assign(N2, C). -#show assign/2. \ No newline at end of file +#show assign/2. diff --git a/examples/graph_coloring/graph_coloring_example.svg b/examples/graph_coloring/graph_coloring_example.svg index 23f9c81..5bc3a03 100644 --- a/examples/graph_coloring/graph_coloring_example.svg +++ b/examples/graph_coloring/graph_coloring_example.svg @@ -1,4 +1,4 @@ -
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
Original
Original
MUC 1
MUC 1
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
MUC 2
MUC 2Text is not SVG - cannot display \ No newline at end of file +
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
Original
Original
MUC 1
MUC 1
1
1
3
3
5
5
4
4
2
2
6
6
9
9
8
8
7
7
MUC 2
MUC 2Text is not SVG - cannot display diff --git a/examples/graph_coloring/instance.lp b/examples/graph_coloring/instance.lp index 35b5e8f..887091b 100644 --- a/examples/graph_coloring/instance.lp +++ b/examples/graph_coloring/instance.lp @@ -17,4 +17,4 @@ color(red; green; blue). assign(1,green). assign(2,blue). assign(5,red). -assign(7,green). \ No newline at end of file +assign(7,green). diff --git a/examples/misc/bad_mucs.lp b/examples/misc/bad_mucs.lp index b371215..ba25841 100644 --- a/examples/misc/bad_mucs.lp +++ b/examples/misc/bad_mucs.lp @@ -2,4 +2,4 @@ a(1..3). :- a(X). unsat. -:- unsat. \ No newline at end of file +:- unsat. diff --git a/examples/misc/simple.lp b/examples/misc/simple.lp index bc2baa3..dc11992 100644 --- a/examples/misc/simple.lp +++ b/examples/misc/simple.lp @@ -1,4 +1,4 @@ a(1..5). b(5..10). -:- a(X), b(X). \ No newline at end of file +:- a(X), b(X). diff --git a/examples/misc/soup.lp b/examples/misc/soup.lp index 5a14062..000d273 100644 --- a/examples/misc/soup.lp +++ b/examples/misc/soup.lp @@ -1,3 +1,3 @@ #include "test/blob.lp". -soup(10). \ No newline at end of file +soup(10). diff --git a/examples/misc/test/blob.lp b/examples/misc/test/blob.lp index f9461b3..6a2b617 100644 --- a/examples/misc/test/blob.lp +++ b/examples/misc/test/blob.lp @@ -1,3 +1,3 @@ #include "../test_inert.lp". -blob(123). \ No newline at end of file +blob(123). diff --git a/examples/misc/test_inert.lp b/examples/misc/test_inert.lp index d179321..61ec2d7 100644 --- a/examples/misc/test_inert.lp +++ b/examples/misc/test_inert.lp @@ -1 +1 @@ -blub(42). \ No newline at end of file +blub(42). diff --git a/examples/misc/x.lp b/examples/misc/x.lp index 5378bb7..4e1eab3 100644 --- a/examples/misc/x.lp +++ b/examples/misc/x.lp @@ -29,4 +29,3 @@ _muc(initial(3,3,1)) :- initial(3,3,1). _assumption(initial(3,4,3)). _muc(initial(3,4,3)) :- initial(3,4,3). #show initial/3. - diff --git a/examples/misc/zero_arity_assumptions.lp b/examples/misc/zero_arity_assumptions.lp index e009fe7..b3a6686 100644 --- a/examples/misc/zero_arity_assumptions.lp +++ b/examples/misc/zero_arity_assumptions.lp @@ -2,4 +2,4 @@ test. not_test :- not test. -:- not not_test. \ No newline at end of file +:- not not_test. diff --git a/examples/queens/README.md b/examples/queens/README.md index b162c44..4957355 100644 --- a/examples/queens/README.md +++ b/examples/queens/README.md @@ -1,9 +1,9 @@ # Example : N Queens Problem -+ This example encodes the classic n queens problem -+ The correct problem encoding is provided with an unsatisfiable instance -+ Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable Cores (MUCs) and their respective unsatisfiable constraints - +- This example encodes the classic n queens problem +- The correct problem encoding is provided with an unsatisfiable instance +- Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable + Cores (MUCs) and their respective unsatisfiable constraints ## Visualization @@ -11,20 +11,20 @@ ## Run -+ Finding all MUCs +- Finding all MUCs ```bash clingexplaid 0 encoding.lp instance.lp --muc -a queen/2 ``` - + Expected Output: ```bash - MUC 1 + MUC 1 queen(1,1) queen(2,5) ``` -+ Finding the unsatisfiable constraints +- Finding the unsatisfiable constraints ```bash clingexplaid 0 encoding.lp instance.lp --unsat-constraints @@ -33,12 +33,13 @@ Expected Output: ```bash - Unsat Constraints + Unsat Constraints :- 2 <= { queen((D-J),J) }; D = (2..(2*n)). :- 2 <= { queen((D+J),J) }; D = ((1-n)..(n-1)). ``` -+ Combined call with unsatisfiable constraints for every found MUC +- Combined call with unsatisfiable constraints for every found MUC + ```bash clingexplaid 0 encoding.lp instance.lp --muc --unsat-constraints -a queen/2 ``` @@ -46,9 +47,8 @@ Expected Output: ```bash - MUC 1 + MUC 1 queen(1,1) queen(2,5) - ├── Unsat Constraints + ├── Unsat Constraints ├──:- 2 <= { queen((D-J),J) }; D = (2..(2*n)). ``` - diff --git a/examples/queens/encoding.lp b/examples/queens/encoding.lp index 902106b..f16fe72 100644 --- a/examples/queens/encoding.lp +++ b/examples/queens/encoding.lp @@ -6,4 +6,4 @@ cell(X,Y) :- number(X), number(Y). 1 { queen(X,Y): number(X) } 1 :- number(Y). :- 2 { queen(D-J,J) }, D = 2..2*n. -:- 2 { queen(D+J,J) }, D = 1-n..n-1. \ No newline at end of file +:- 2 { queen(D+J,J) }, D = 1-n..n-1. diff --git a/examples/queens/instance.lp b/examples/queens/instance.lp index e8c874e..f7b8d79 100644 --- a/examples/queens/instance.lp +++ b/examples/queens/instance.lp @@ -1,3 +1,3 @@ queen(1,1). queen(2,5). -queen(3,2). \ No newline at end of file +queen(3,2). diff --git a/examples/queens/queens_example.svg b/examples/queens/queens_example.svg index b98e149..81cf985 100644 --- a/examples/queens/queens_example.svg +++ b/examples/queens/queens_example.svg @@ -1,4 +1,4 @@ -
Original
Original
MUC 1
MUC 1Text is not SVG - cannot display \ No newline at end of file +
Original
Original
MUC 1
MUC 1Text is not SVG - cannot display diff --git a/examples/sudoku/README.md b/examples/sudoku/README.md index ddd6cf7..3eb7231 100644 --- a/examples/sudoku/README.md +++ b/examples/sudoku/README.md @@ -1,7 +1,9 @@ # Example : Sudoku -+ This example is a 4 by 4 sudoku encoding which is given an unsatisfiable instance -+ Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable Cores (MUCs) and their respective unsatisfiable constraints +- This example is a 4 by 4 sudoku encoding which is given an unsatisfiable + instance +- Using `clingexplaid` we can discover the underlying Minimal Unsatisfiable + Cores (MUCs) and their respective unsatisfiable constraints ## Visualization @@ -9,52 +11,55 @@ ## Run -+ Finding all MUCs +- Finding all MUCs ```bash clingexplaid 0 encoding.lp instance.lp --muc -a initial/3 ``` + Expected Output: ```bash - MUC 1 + MUC 1 initial(4,1,4) initial(3,3,1) initial(3,4,3) - MUC 2 + MUC 2 initial(1,1,4) initial(1,4,2) initial(2,3,3) initial(3,3,1) - MUC 3 + MUC 3 initial(1,1,4) initial(4,1,4) ``` -+ Finding the unsatisfiable constraints +- Finding the unsatisfiable constraints ```bash clingexplaid 0 encoding.lp instance.lp --unsat-constraints ``` + Expected Output: ```bash - Unsat Constraints + Unsat Constraints :- solution(X1,Y,N); solution(X2,Y,N); X1 != X2. ``` -+ Combined call with unsatisfiable constraints for every found MUC +- Combined call with unsatisfiable constraints for every found MUC + ```bash clingexplaid 0 encoding.lp instance.lp --muc --unsat-constraints -a initial/3 ``` - + Expected Output: ```bash - MUC 1 + MUC 1 initial(4,1,4) initial(3,3,1) initial(3,4,3) - ├── Unsat Constraints + ├── Unsat Constraints ├──:- solution(X,Y1,N); solution(X,Y2,N); Y1 != Y2. - MUC 2 + MUC 2 initial(1,1,4) initial(1,4,2) initial(2,3,3) initial(3,3,1) - ├── Unsat Constraints + ├── Unsat Constraints ├──:- solution(X,Y1,N); solution(X,Y2,N); Y1 != Y2. - MUC 3 + MUC 3 initial(1,1,4) initial(4,1,4) - ├── Unsat Constraints + ├── Unsat Constraints ├──:- solution(X1,Y,N); solution(X2,Y,N); X1 != X2. - ``` \ No newline at end of file + ``` diff --git a/examples/sudoku/sudoku_example.svg b/examples/sudoku/sudoku_example.svg index 2414a8a..e7474d9 100644 --- a/examples/sudoku/sudoku_example.svg +++ b/examples/sudoku/sudoku_example.svg @@ -1,4 +1,4 @@ -
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
Original
Original
MUC 3
MUC 3
MUC 1
MUC 1
MUC 2
MUC 2Text is not SVG - cannot display \ No newline at end of file +
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
4
4
3
3
2
2
4
4
1
1
3
3
Original
Original
MUC 3
MUC 3
MUC 1
MUC 1
MUC 2
MUC 2Text is not SVG - cannot display diff --git a/src/clingexplaid/cli/clingo_app.py b/src/clingexplaid/cli/clingo_app.py index e6b6b83..80930d0 100644 --- a/src/clingexplaid/cli/clingo_app.py +++ b/src/clingexplaid/cli/clingo_app.py @@ -6,22 +6,18 @@ import sys from importlib.metadata import version from pathlib import Path -from typing import Dict, List, Tuple, Optional, Set, Callable, Sequence +from typing import Callable, Dict, List, Optional, Sequence, Set, Tuple from warnings import warn - import clingo from clingo.application import Application, Flag from ..muc import CoreComputer from ..propagators import DecisionOrderPropagator +from ..transformers import AssumptionTransformer, OptimizationRemover from ..unsat_constraints import UnsatConstraintComputer -from ..utils import ( - get_constants_from_arguments, -) +from ..utils import get_constants_from_arguments from ..utils.logging import BACKGROUND_COLORS, COLORS -from ..transformers import AssumptionTransformer, OptimizationRemover - HYPERLINK_MASK = "\033]8;{};{}\033\\{}\033]8;;\033\\" diff --git a/src/clingexplaid/muc/core_computer.py b/src/clingexplaid/muc/core_computer.py index bd6b7cb..d892043 100644 --- a/src/clingexplaid/muc/core_computer.py +++ b/src/clingexplaid/muc/core_computer.py @@ -3,7 +3,7 @@ """ from itertools import chain, combinations -from typing import Optional, Set, Tuple, Generator, List, Dict +from typing import Dict, Generator, List, Optional, Set, Tuple import clingo diff --git a/src/clingexplaid/propagators/propagator_decision_order.py b/src/clingexplaid/propagators/propagator_decision_order.py index 106c0fc..1e12f48 100644 --- a/src/clingexplaid/propagators/propagator_decision_order.py +++ b/src/clingexplaid/propagators/propagator_decision_order.py @@ -2,12 +2,12 @@ Propagator Module: Decision Order """ -from typing import Optional, Tuple, Set, Dict, List, Sequence, Union +from typing import Dict, List, Optional, Sequence, Set, Tuple, Union import clingo -from .constants import UNKNOWN_SYMBOL_TOKEN, INDENT_STEP, INDENT_START, INDENT_END from ..utils.logging import COLORS +from .constants import INDENT_END, INDENT_START, INDENT_STEP, UNKNOWN_SYMBOL_TOKEN class DecisionOrderPropagator: diff --git a/src/clingexplaid/transformers/transformer_assumption.py b/src/clingexplaid/transformers/transformer_assumption.py index f1f10c9..738364b 100644 --- a/src/clingexplaid/transformers/transformer_assumption.py +++ b/src/clingexplaid/transformers/transformer_assumption.py @@ -8,8 +8,8 @@ import clingo import clingo.ast as _ast -from .exceptions import NotGroundedException, UntransformedException from ..utils import match_ast_symbolic_atom_signature +from .exceptions import NotGroundedException, UntransformedException class AssumptionTransformer(_ast.Transformer): diff --git a/src/clingexplaid/transformers/transformer_constraint.py b/src/clingexplaid/transformers/transformer_constraint.py index 86b37f0..d69bc28 100644 --- a/src/clingexplaid/transformers/transformer_constraint.py +++ b/src/clingexplaid/transformers/transformer_constraint.py @@ -3,7 +3,7 @@ """ from pathlib import Path -from typing import Sequence, Union, Dict +from typing import Dict, Sequence, Union import clingo import clingo.ast as _ast diff --git a/src/clingexplaid/transformers/transformer_fact.py b/src/clingexplaid/transformers/transformer_fact.py index 0b07be8..ca1ad0a 100644 --- a/src/clingexplaid/transformers/transformer_fact.py +++ b/src/clingexplaid/transformers/transformer_fact.py @@ -8,8 +8,8 @@ import clingo from clingo import ast -from .constants import REMOVED_TOKEN from ..utils import match_ast_symbolic_atom_signature +from .constants import REMOVED_TOKEN class FactTransformer(ast.Transformer): diff --git a/src/clingexplaid/transformers/transformer_rule_splitter.py b/src/clingexplaid/transformers/transformer_rule_splitter.py index e09145e..441b6c5 100644 --- a/src/clingexplaid/transformers/transformer_rule_splitter.py +++ b/src/clingexplaid/transformers/transformer_rule_splitter.py @@ -4,7 +4,7 @@ import base64 from pathlib import Path -from typing import Union, List +from typing import List, Union import clingo import clingo.ast as _ast diff --git a/src/clingexplaid/unsat_constraints/unsat_constraint_computer.py b/src/clingexplaid/unsat_constraints/unsat_constraint_computer.py index b61fcac..b504702 100644 --- a/src/clingexplaid/unsat_constraints/unsat_constraint_computer.py +++ b/src/clingexplaid/unsat_constraints/unsat_constraint_computer.py @@ -3,14 +3,14 @@ """ import re -from typing import List, Optional, Dict +from typing import Dict, List, Optional import clingo from clingo.ast import Location -from .constants import UNSAT_CONSTRAINT_SIGNATURE from ..transformers import ConstraintTransformer, FactTransformer, OptimizationRemover from ..utils import get_signatures_from_model_string +from .constants import UNSAT_CONSTRAINT_SIGNATURE class UnsatConstraintComputer: @@ -91,9 +91,7 @@ def get_unsat_constraints(self, assumption_string: Optional[str] = None) -> Dict # create a rule lookup for every constraint in the program associated with it's unsat id constraint_lookup = {} for line in program_string.split("\n"): - id_re = re.compile( - f"{UNSAT_CONSTRAINT_SIGNATURE}[(]([1-9][0-9]*)[)]" - ) + id_re = re.compile(f"{UNSAT_CONSTRAINT_SIGNATURE}[(]([1-9][0-9]*)[)]") match_result = id_re.match(line) if match_result is None: continue diff --git a/src/clingexplaid/utils/__init__.py b/src/clingexplaid/utils/__init__.py index 7c661b5..939d256 100644 --- a/src/clingexplaid/utils/__init__.py +++ b/src/clingexplaid/utils/__init__.py @@ -3,15 +3,13 @@ """ import re -from typing import Dict, Set, Tuple, List +from typing import Dict, List, Set, Tuple import clingo from clingo.ast import ASTType -def match_ast_symbolic_atom_signature( - ast_symbol: ASTType.SymbolicAtom, signature: Tuple[str, int] -) -> bool: +def match_ast_symbolic_atom_signature(ast_symbol: ASTType.SymbolicAtom, signature: Tuple[str, int]) -> bool: """ Function to match the signature of an AST SymbolicAtom to a tuple containing a string and int value, representing a matching signature. diff --git a/src/clingexplaid/utils/types.py b/src/clingexplaid/utils/types.py index 7ef7eb2..663491a 100644 --- a/src/clingexplaid/utils/types.py +++ b/src/clingexplaid/utils/types.py @@ -2,7 +2,7 @@ Custom types for clingexplaid """ -from typing import Set, Tuple, Union, Iterable +from typing import Iterable, Set, Tuple, Union import clingo diff --git a/tests/clingexplaid/res/test_program.lp b/tests/clingexplaid/res/test_program.lp index 70536c4..95ffbc1 100644 --- a/tests/clingexplaid/res/test_program.lp +++ b/tests/clingexplaid/res/test_program.lp @@ -4,4 +4,4 @@ c(3); c(4) :- x. d(10..15). e(16). f(17); f(18) :- e(16). -x(19). \ No newline at end of file +x(19). diff --git a/tests/clingexplaid/res/test_program_constants.lp b/tests/clingexplaid/res/test_program_constants.lp index 17d5808..76d7157 100644 --- a/tests/clingexplaid/res/test_program_constants.lp +++ b/tests/clingexplaid/res/test_program_constants.lp @@ -1,2 +1,2 @@ #const number=42. -#const message=helloworld. \ No newline at end of file +#const message=helloworld. diff --git a/tests/clingexplaid/res/test_program_constraints.lp b/tests/clingexplaid/res/test_program_constraints.lp index c9149a4..f159dbe 100644 --- a/tests/clingexplaid/res/test_program_constraints.lp +++ b/tests/clingexplaid/res/test_program_constraints.lp @@ -2,4 +2,4 @@ x(1). #true :- x(2). :- a; b; c. -:- a; d. \ No newline at end of file +:- a; d. diff --git a/tests/clingexplaid/res/test_program_decision_order.lp b/tests/clingexplaid/res/test_program_decision_order.lp index 63c3b84..8f87691 100644 --- a/tests/clingexplaid/res/test_program_decision_order.lp +++ b/tests/clingexplaid/res/test_program_decision_order.lp @@ -1,4 +1,4 @@ {a}. {b} :- a. :- not a. -x. \ No newline at end of file +x. diff --git a/tests/clingexplaid/res/test_program_multi_muc.lp b/tests/clingexplaid/res/test_program_multi_muc.lp index d5bd004..d2bd6e8 100644 --- a/tests/clingexplaid/res/test_program_multi_muc.lp +++ b/tests/clingexplaid/res/test_program_multi_muc.lp @@ -3,4 +3,4 @@ a(1..10). :- a(1), a(2). :- a(5), a(8), a(3). :- a(1), a(9). -:- a(1), a(9), a(4). \ No newline at end of file +:- a(1), a(9), a(4). diff --git a/tests/clingexplaid/res/test_program_optimization.lp b/tests/clingexplaid/res/test_program_optimization.lp index aad8c05..77367ed 100644 --- a/tests/clingexplaid/res/test_program_optimization.lp +++ b/tests/clingexplaid/res/test_program_optimization.lp @@ -2,4 +2,4 @@ a_count(C) :- C=#count{X: a(X)}. #minimize{C@2: a_count(C)}. a_sum(S) :- S=#sum{X: a(X)}. -#maximize{S@1: a_sum(S)}. \ No newline at end of file +#maximize{S@1: a_sum(S)}. diff --git a/tests/clingexplaid/res/test_program_rules.lp b/tests/clingexplaid/res/test_program_rules.lp index 3543e09..b42bab4 100644 --- a/tests/clingexplaid/res/test_program_rules.lp +++ b/tests/clingexplaid/res/test_program_rules.lp @@ -2,4 +2,4 @@ constant. head(1) :- body(1). head(2) :- body(2,X,Y). head(3) :- body(X). -:- constraint. \ No newline at end of file +:- constraint. diff --git a/tests/clingexplaid/res/test_program_unsat_constraints.lp b/tests/clingexplaid/res/test_program_unsat_constraints.lp index 8ded791..e239f7b 100644 --- a/tests/clingexplaid/res/test_program_unsat_constraints.lp +++ b/tests/clingexplaid/res/test_program_unsat_constraints.lp @@ -1,4 +1,4 @@ {a;b;c;d}. :- a. -:- not a. \ No newline at end of file +:- not a. diff --git a/tests/clingexplaid/res/transformed_program_assumptions_all.lp b/tests/clingexplaid/res/transformed_program_assumptions_all.lp index e04b6f2..6811a3e 100644 --- a/tests/clingexplaid/res/transformed_program_assumptions_all.lp +++ b/tests/clingexplaid/res/transformed_program_assumptions_all.lp @@ -5,4 +5,4 @@ c(3); c(4) :- x. { d((10..15)) }. { e(16) }. f(17); f(18) :- e(16). -{ x(19) }. \ No newline at end of file +{ x(19) }. diff --git a/tests/clingexplaid/res/transformed_program_assumptions_certain_signatures.lp b/tests/clingexplaid/res/transformed_program_assumptions_certain_signatures.lp index 801c7a6..596e4d4 100644 --- a/tests/clingexplaid/res/transformed_program_assumptions_certain_signatures.lp +++ b/tests/clingexplaid/res/transformed_program_assumptions_certain_signatures.lp @@ -5,4 +5,4 @@ c(3); c(4) :- x. { d((10..15)) }. { e(16) }. f(17); f(18) :- e(16). -x(19). \ No newline at end of file +x(19). diff --git a/tests/clingexplaid/res/transformed_program_constraints.lp b/tests/clingexplaid/res/transformed_program_constraints.lp index 55abe48..1e70070 100644 --- a/tests/clingexplaid/res/transformed_program_constraints.lp +++ b/tests/clingexplaid/res/transformed_program_constraints.lp @@ -3,4 +3,4 @@ x(1). #true :- x(2). unsat :- a; b; c. -unsat :- a; d. \ No newline at end of file +unsat :- a; d. diff --git a/tests/clingexplaid/res/transformed_program_constraints_id.lp b/tests/clingexplaid/res/transformed_program_constraints_id.lp index d7d339a..ab048ff 100644 --- a/tests/clingexplaid/res/transformed_program_constraints_id.lp +++ b/tests/clingexplaid/res/transformed_program_constraints_id.lp @@ -3,4 +3,4 @@ x(1). #true :- x(2). unsat(1) :- a; b; c. -unsat(2) :- a; d. \ No newline at end of file +unsat(2) :- a; d. diff --git a/tests/clingexplaid/res/transformed_program_facts.lp b/tests/clingexplaid/res/transformed_program_facts.lp index 356e5e0..c7639aa 100644 --- a/tests/clingexplaid/res/transformed_program_facts.lp +++ b/tests/clingexplaid/res/transformed_program_facts.lp @@ -2,4 +2,4 @@ b(2) :- x. c(3); c(4) :- x. f(17); f(18) :- e(16). -x(19). \ No newline at end of file +x(19). diff --git a/tests/clingexplaid/res/transformed_program_optimization.lp b/tests/clingexplaid/res/transformed_program_optimization.lp index 6e270d9..aa9eb2a 100644 --- a/tests/clingexplaid/res/transformed_program_optimization.lp +++ b/tests/clingexplaid/res/transformed_program_optimization.lp @@ -1,4 +1,4 @@ #program base. 1 <= { a((1..10)) }. a_count(C) :- C = #count { X: a(X) }. -a_sum(S) :- S = #sum { X: a(X) }. \ No newline at end of file +a_sum(S) :- S = #sum { X: a(X) }. diff --git a/tests/clingexplaid/res/transformed_program_rule_ids.lp b/tests/clingexplaid/res/transformed_program_rule_ids.lp index a831fc2..e74c3b7 100644 --- a/tests/clingexplaid/res/transformed_program_rule_ids.lp +++ b/tests/clingexplaid/res/transformed_program_rule_ids.lp @@ -6,4 +6,4 @@ d((10..15)) :- _rule(4). e(16) :- _rule(5). f(17); f(18) :- e(16); _rule(6). x(19) :- _rule(7). -{_rule(1..7)} % Choice rule to allow all _rule atoms to become assumptions \ No newline at end of file +{_rule(1..7)} % Choice rule to allow all _rule atoms to become assumptions diff --git a/tests/clingexplaid/res/transformed_program_rules_split.lp b/tests/clingexplaid/res/transformed_program_rules_split.lp index 7e745f2..90893a2 100644 --- a/tests/clingexplaid/res/transformed_program_rules_split.lp +++ b/tests/clingexplaid/res/transformed_program_rules_split.lp @@ -7,4 +7,4 @@ _body("Y29uc3RyYWludA==",()) :- constraint. head(1) :- _body("Ym9keSgxKQ==",(1,)). head(2) :- _body("Ym9keSgyLFgsWSk=",(X,Y,2)). head(3) :- _body("Ym9keShYKQ==",(X,)). -#false :- _body("Y29uc3RyYWludA==",()). \ No newline at end of file +#false :- _body("Y29uc3RyYWludA==",()). diff --git a/tests/clingexplaid/test_muc.py b/tests/clingexplaid/test_muc.py index 2476ed2..9467304 100644 --- a/tests/clingexplaid/test_muc.py +++ b/tests/clingexplaid/test_muc.py @@ -1,11 +1,13 @@ """ Tests for the muc package """ + import random -from typing import Set, Tuple, Optional, List +from typing import List, Optional, Set, Tuple from unittest import TestCase import clingo + from clingexplaid.muc import CoreComputer from clingexplaid.transformers import AssumptionTransformer from clingexplaid.utils.types import AssumptionSet diff --git a/tests/clingexplaid/test_transformers.py b/tests/clingexplaid/test_transformers.py index 9a20738..5795f24 100644 --- a/tests/clingexplaid/test_transformers.py +++ b/tests/clingexplaid/test_transformers.py @@ -5,15 +5,16 @@ from unittest import TestCase import clingo + from clingexplaid.transformers import ( AssumptionTransformer, - RuleIDTransformer, ConstraintTransformer, - RuleSplitter, - OptimizationRemover, FactTransformer, + OptimizationRemover, + RuleIDTransformer, + RuleSplitter, ) -from clingexplaid.transformers.exceptions import UntransformedException, NotGroundedException +from clingexplaid.transformers.exceptions import NotGroundedException, UntransformedException from .test_main import TEST_DIR, read_file diff --git a/tests/clingexplaid/test_utils.py b/tests/clingexplaid/test_utils.py index 7b3e30f..1229def 100644 --- a/tests/clingexplaid/test_utils.py +++ b/tests/clingexplaid/test_utils.py @@ -4,7 +4,7 @@ from unittest import TestCase -from clingexplaid.utils import get_signatures_from_model_string, get_constants_from_arguments +from clingexplaid.utils import get_constants_from_arguments, get_signatures_from_model_string class TestUtils(TestCase):