Skip to content

Commit e2703bd

Browse files
committed
Merge branch 'master' into feature/dnnf-model-enumeration
2 parents ef1a693 + 47d1db3 commit e2703bd

File tree

120 files changed

+3365
-2484
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

120 files changed

+3365
-2484
lines changed

Diff for: .github/workflows/build.yml

+3-6
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,7 @@ jobs:
1616
java-version: 1.8
1717
- name: Build with Maven
1818
run: mvn -B package
19-
- name: Upload coverage to codecov.io
20-
uses: codecov/codecov-action@v1
19+
- name: Upload coverage reports to Codecov
20+
uses: codecov/codecov-action@v4.0.1
2121
with:
22-
name: LogicNG
23-
file: ./target/site/jacoco/jacoco.xml
24-
flags: unittests
25-
env_vars: OS
22+
token: ${{ secrets.CODECOV_TOKEN }}

Diff for: .github/workflows/mattermost.yml

-13
This file was deleted.

Diff for: CHANGELOG.md

+55-1
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,61 @@
22

33
LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
44

5+
## [2.6.0] - 2024-09-10
6+
7+
### Added
8+
9+
- New class `OptimizationConfig` used to configure optimization computations in various algorithms. It allows to configure the following aspects:
10+
- the `optimizationType` (either SAT-based optimization or a MaxSAT algorithm)
11+
- the `maxSATConfig` to further configure the MaxSAT algorithm
12+
- the `optimizationHandler` to use
13+
- the `maxSATHandler` to use
14+
- Added three new configuration options to `AdvancedSimplifierConfig`:
15+
- `minimalDnfCover` determines whether the step for computing the minimal DNF cover should be performed. Default is `true`.
16+
- `returnIntermediateResult` allows to return an intermediate result from the `AdvancedSimplifier` if the computation was aborted by a handler. Default is `false`.
17+
- `optimizationConfig` can be used to configure the algorithms in the simplifier which perform optimizations, also the `OptimizationHandler handler` moved into this config
18+
19+
## [2.5.1] - 2024-07-31
20+
21+
### Changed
22+
23+
- Changed visibility from some methods from package-private to public for formula and solver serializiation via the
24+
new https://github.com/logic-ng/serialization library
25+
26+
27+
## [2.5.0] - 2024-05-02
28+
29+
### Removed (Potentially Breaking Change!)
30+
31+
- All parser classes from `org.logicng.io.parsers` (including in particular the two main parsers `PropositionalParser` and `PseudoBooleanParser`) as well as the class `org.logicng.io.readers.FormulaReader` were moved to the new artifacts `org.logicng.logicng-parser-j8` (or `org.logicng.logicng-parser-j11` for Java 11). So LogicNG now consists of two artifacts:
32+
- All the core functionality of LogicNG except for the parser is located in the "old" `org.logicng:logicng` artifact. This artifact does *not* depend on ANTLR anymore (which was the reason for splitting the library). This library will stay on Java 8, but nothing should prevent its usage in higher Java versions.
33+
- The parser functionality is located in `org.logicng:logicng-parser-j8` (for Java 8 and ANTLR 4.9.3) and `org.logicng:logicng-parser-j11` (for Java 11 and the most recent ANTLR version). The version of this library will stay in sync with the core library.
34+
- The method `FormulaFactory.parse()` was removed. If you're using this method you should include one of the new parser artefacts and then just create your own `PropositionalParser` or `PseudoBooleanParser` and call `parse()` on them.
35+
36+
### Added
37+
38+
- Added unsafe methods `term` and `dnf` to the `FormulaFactory` to create a term (conjunction of literals) or a DNF (c.f. with method `FormulaFactory#clause` and `FormulaFactory#cnf`). Both methods do not perform reduction operations and therefore are faster. Only use these methods if you are sure the input is free of complementary and redundant operands.
39+
- Class `UBTree` offers new method `generateSubsumedUBTree` to directly generate a subsumed UBTree for the given sets.
40+
- The `DnnfFactory` now offers a method to compile a DNNF with a `DnnfCompilationHandler`
41+
- The `ModelCounter` now offers a method to pass a `DnnfCompilationHandler` in order to control long-running computations
42+
43+
### Changed
44+
45+
- UBTree data structure now supports empty sets.
46+
- Added side effect note in `SATSolver` for the four assumption solving methods.
47+
- Methods for reordering and swapping variables on BDD were refactored: `BDD.getReordering`, `BDDKernel.getReordering`, and `BDD.swapVariables` are now deprecated and should not be used anymore. Instead, there are new methods on the `BDDKernel`. Note that these actions affect all BDDs generated by the kernel.
48+
- `BDDKernel.swapVariables` for swapping two variables (or variable indices)
49+
- `BDDKernel.reorder` for automatically reordering the BDD
50+
- `BDDKernel.activateReorderDuringBuild` for activating reordering during build
51+
- `BDDKernel.addVariableBlock` for defining a variable block for reordering
52+
- `BDDKernel.addAllVariablesAsBlock` for defining one block for each variable (s.t. all variables are allowed to be reordered independently)
53+
- Significant performance improvements in the DTree generation for DNNFs
54+
- Minor performance improvements in some DNF/CNF generating algorithms by using faster `cnf`/`dnf`.
55+
56+
### Fixed
57+
58+
- The formula generation on BDDs was broken when the ordering was changed by `BDDKernel.reorder` or `BDDKernel.swapVariables`. This is now fixed.
59+
560
## [2.4.1] - 2022-12-01
661

762
### Changed
@@ -359,4 +414,3 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
359414
### Added
360415

361416
- Initial Release of LogicNG
362-

Diff for: README.md

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
![build](https://github.com/logic-ng/LogicNG/workflows/build/badge.svg) [![codecov](https://codecov.io/gh/logic-ng/LogicNG/branch/development/graph/badge.svg)](https://codecov.io/gh/logic-ng/LogicNG) ![License](https://img.shields.io/badge/license-Apache%202-ff69b4.svg) [![Maven Central](https://img.shields.io/maven-central/v/org.logicng/logicng.svg?label=Maven%20Central)](https://search.maven.org/search?q=g:%22org.logicng%22%20AND%20a:%22logicng%22)
1+
![build](https://github.com/logic-ng/LogicNG/workflows/build/badge.svg) [![codecov](https://codecov.io/gh/logic-ng/LogicNG/branch/master/graph/badge.svg?token=RMmCetIVYf)](https://codecov.io/gh/logic-ng/LogicNG) ![License](https://img.shields.io/badge/license-Apache%202-ff69b4.svg) [![Maven Central](https://img.shields.io/maven-central/v/org.logicng/logicng.svg?label=Maven%20Central)](https://search.maven.org/search?q=g:%22org.logicng%22%20AND%20a:%22logicng%22)
22

33

44
<a href="https://www.logicng.org"><img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300"></a>
@@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add
3434
<dependency>
3535
<groupId>org.logicng</groupId>
3636
<artifactId>logicng</artifactId>
37-
<version>2.4.1</version>
37+
<version>2.6.0</version>
3838
</dependency>
3939
```
4040

0 commit comments

Comments
 (0)