Fixed formatting

.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/"
+          repository-url: "https://test.pypi.org/legacy/"

.github/workflows/test.yml

@@ -38,4 +38,4 @@ jobs:
       run: pre-commit run --all --show-diff-on-failure
 
     - name: run tests
-      run: nox
+      run: nox

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 <filenames> <n> <method> <options>
 ```
 
-+ `<filenames>`: has to be replaced by a list of all files or a single filename
-+ `<n>`: defines how many models are computed (Default=`1`, All=`0`)
-+ `<method>`: 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
-+ `<options>`: 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)
+- `<filenames>`: has to be replaced by a list of all files or a single filename
+- `<n>`: defines how many models are computed (Default=`1`, All=`0`)
+- `<method>`: 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
+- `<options>`: 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

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

examples/graph_coloring/README.md

@@ -1,59 +1,61 @@
 # 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
 
 ![](graph_coloring_example.svg)
 
 ## 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).
+  ```