DARPA's Cyber Assured Systems Engineering (CASE) project named Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT)
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:
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.
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.
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.
Added
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.
Class UBTree offers new method generateSubsumedUBTree to directly generate a subsumed UBTree for the given sets.
The DnnfFactory now offers a method to compile a DNNF with a DnnfCompilationHandler
The ModelCounter now offers a method to pass a DnnfCompilationHandler in order to control long-running computations
Changed
UBTree data structure now supports empty sets.
Added side effect note in SATSolver for the four assumption solving methods.
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.
BDDKernel.swapVariables for swapping two variables (or variable indices)
BDDKernel.reorder for automatically reordering the BDD
BDDKernel.activateReorderDuringBuild for activating reordering during build
BDDKernel.addVariableBlock for defining a variable block for reordering
BDDKernel.addAllVariablesAsBlock for defining one block for each variable (s.t. all variables are allowed to be reordered independently)
Significant performance improvements in the DTree generation for DNNFs
Minor performance improvements in some DNF/CNF generating algorithms by using faster cnf/dnf.
Fixed
The formula generation on BDDs was broken when the ordering was changed by BDDKernel.reorder or BDDKernel.swapVariables. This is now fixed.
v2.4.3-j11
Updated ANTLR to version 4.13.1
v2.4.2-j11
Changed
Changed artifact id to logicng-j11 (for Java 11 only)
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:
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.
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.
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.
Added
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.
Class UBTree offers new method generateSubsumedUBTree to directly generate a subsumed UBTree for the given sets.
The DnnfFactory now offers a method to compile a DNNF with a DnnfCompilationHandler
The ModelCounter now offers a method to pass a DnnfCompilationHandler in order to control long-running computations
Changed
UBTree data structure now supports empty sets.
Added side effect note in SATSolver for the four assumption solving methods.
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.
BDDKernel.swapVariables for swapping two variables (or variable indices)
BDDKernel.reorder for automatically reordering the BDD
BDDKernel.activateReorderDuringBuild for activating reordering during build
BDDKernel.addVariableBlock for defining a variable block for reordering
BDDKernel.addAllVariablesAsBlock for defining one block for each variable (s.t. all variables are allowed to be reordered independently)
Significant performance improvements in the DTree generation for DNNFs
Minor performance improvements in some DNF/CNF generating algorithms by using faster cnf/dnf.
Fixed
The formula generation on BDDs was broken when the ordering was changed by BDDKernel.reorder or BDDKernel.swapVariables. This is now fixed.
Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
- `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Bumps org.logicng:logicng from 2.4.1 to 2.5.0.
Release notes
Sourced from org.logicng:logicng's releases.
Changelog
Sourced from org.logicng:logicng's changelog.
Commits
e6f6024Updated CHANGELOG to 2.5.08577da0Merge pull request #52 from logic-ng/feature/remove-parser2b1b827Updated version to 2.5.04f47fcdSome clarifications in the CHANGELOG81624f1adjust changelog201585cgive surefire tests enough memorye17a890extracted the parser(s) to its own artifact org.logicng.logicng-parser-j8/11 ...bb7e1acMerge branch 'feature/unsafe-dnf' into developmentb2a8e7cRevert "fixed SATSolver#add: Ensure all variables are added to the internal s...87da23badded possibility to pass a DNNF handler to the model counterDependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting
@dependabot rebase.Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show