« Changelog History


LogicNG v2.3.0 Release Notes

Release Date: 2022-07-18 // almost 2 years ago

  • ➕ Added

    • Overloaded method createAssignment in MiniSat by flag whether the created assignment should be a fast evaluable assignment.
    • 🏗 Extended ModelEnumerationFunction.Builder by flag fastEvaulable which indicates whether the created assignments should be a fast evaluable assignment.
    • Convenience methods isNNF(), isDNF() and isCNF() in class Formula
    • Two new constructors for Substitutions and a new method getMapping() to get the internal mapping
    • Method getSubstitution on Anonymizer to get the mapping from original variable to anonymized one
    • A DNF from BDD function BDDDNFFunction, a subclass of the newly added class BDDNormalFormFunction
    • A DNF from BDD formula transformation BDDDNFTransformation, a subclass of the newly added class BDDNormalFormTransforamtion
    • A canonical CNF enumeration CanonicalCNFEnumeration, a subclass of the newly added class CanonicalEnumeration.

    🔄 Changed

    • 👌 Improved methods intersection and union in CollectionHelper by using bounded wildcards.
    • 👌 Improved performance of hashCode and equals in Assignment by avoiding redundant hash set creation.
    • Method BDD#dnf() uses the newly introduced BDDDNFFunction to obtain a smaller DNF instead of a canonical DNF
    • Class BDDCNFFunction uses the singleton pattern
    • 0️⃣ All functions/transformations/predicates with only a default constructor introduce a static get() method with the singleton pattern. The public constructors are now deprecated and will be removed with LogicNG 3.0
    • 🔧 Always use the default configuration of algorithms from the formula factory and do not construct them in the respective classes separately.

    🛠 Fixed

    • Minor edge case issue in NegationSimplifier which yielded a larger result formula than input formula.
    • ✅ The TermPredicate logic was inverted. In detail, the minterm predicate TermPredicate#getMintermPredicate() tested for a maxterm and the TermPredicate#getMaxtermPredicate() tested for a minterm. To prevent silent errors for callers of these predicates, the factory method names were changed to minterm() and maxterm(), respectively. Thus, an intentional breaking change on compile time level has been introduced to force callers to adjust their logic.
    • Minor edge case issue in MiniSat when performing assumption solving with proof tracing.
    • 🛠 Fixed two bugs in the backbone computation on the MiniCard solver.