Skip to content

Commit

Permalink
Merge branch 'main' into feature/maxsat-incremental-interface
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Sep 11, 2024
2 parents 0a80fb6 + 45448d9 commit 68f49ac
Show file tree
Hide file tree
Showing 53 changed files with 454 additions and 485 deletions.
31 changes: 10 additions & 21 deletions pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
<!-- Copyright 2023-20xx BooleWorks GmbH -->

<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/maven-v4_0_0.xsd">
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/maven-v4_0_0.xsd">
<modelVersion>4.0.0</modelVersion>
<groupId>com.booleworks</groupId>
<artifactId>logicng-core</artifactId>
Expand All @@ -12,7 +12,7 @@

<name>LogicNG</name>
<description>The Next Generation Logic Library</description>
<url>http://www.logicng.org</url>
<url>https://www.logicng.org</url>

<licenses>
<license>
Expand Down Expand Up @@ -48,13 +48,12 @@
<maven.compiler.target>11</maven.compiler.target>

<!-- Dependency Versions -->
<version.antlr>4.13.1</version.antlr>
<version.junit>5.10.1</version.junit>
<version.assertj>3.24.2</version.assertj>
<version.mockito>5.2.0</version.mockito>

<!-- Plugin Versions -->
<version.antlr-plugin>4.13.1</version.antlr-plugin>
<version.javacc>3.0.1</version.javacc>
<version.jacoco>0.8.11</version.jacoco>
<version.coveralls>4.3.0</version.coveralls>
<version.maven-compiler>3.13.0</version.maven-compiler>
Expand All @@ -80,19 +79,16 @@
</resources>

<plugins>
<!-- ANTLR4 (Parser Generation) -->
<!-- Parser Generation -->
<plugin>
<groupId>org.antlr</groupId>
<artifactId>antlr4-maven-plugin</artifactId>
<version>${version.antlr-plugin}</version>
<configuration>
<sourceDirectory>src/main/antlr</sourceDirectory>
<outputDirectory>target/generated-sources/antlr/com/booleworks/logicng/io/parsers</outputDirectory>
</configuration>
<groupId>org.codehaus.mojo</groupId>
<artifactId>javacc-maven-plugin</artifactId>
<version>${version.javacc}</version>
<executions>
<execution>
<id>javacc</id>
<goals>
<goal>antlr4</goal>
<goal>javacc</goal>
</goals>
</execution>
</executions>
Expand Down Expand Up @@ -234,7 +230,7 @@
<version>${version.coveralls}</version>
<configuration>
<sourceDirectories>
<sourceDirectory>target/generated-sources/antlr</sourceDirectory>
<sourceDirectory>target/generated-sources/parser</sourceDirectory>
</sourceDirectories>
</configuration>
</plugin>
Expand All @@ -255,13 +251,6 @@
</build>

<dependencies>
<!-- Parser -->
<dependency>
<groupId>org.antlr</groupId>
<artifactId>antlr4-runtime</artifactId>
<version>${version.antlr}</version>
</dependency>

<!-- Testing -->
<dependency>
<groupId>org.junit.jupiter</groupId>
Expand Down
95 changes: 0 additions & 95 deletions src/main/antlr/LogicNGPropositional.g4
View file

This file was deleted.

15 changes: 5 additions & 10 deletions src/main/java/com/booleworks/logicng/datastructures/ubtrees/UBTree.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
* A data structure for storing sets with efficient sub- and superset queries.
* C.f. `A New Method to Index and Query Sets`, Hoffmann and Koehler, 1999
* @param <T> the type of the elements (must be comparable)
* @version 2.0.0
* @version 3.0.0
* @since 1.5.0
*/
public final class UBTree<T extends Comparable<T>> {
Expand All @@ -38,11 +38,7 @@ public void addSet(final SortedSet<T> set) {
SortedMap<T, UBNode<T>> nodes = rootNodes;
UBNode<T> node = null;
for (final T element : set) {
node = nodes.get(element);
if (node == null) {
node = new UBNode<>(element);
nodes.put(element, node);
}
node = nodes.computeIfAbsent(element, UBNode::new);
nodes = node.children();
}
if (node != null) {
Expand All @@ -54,7 +50,7 @@ public void addSet(final SortedSet<T> set) {
* Returns the first subset of a given set in this UBTree.
* @param set the set to search for
* @return the first subset which is found for the given set or {@code null}
* if there is none
* if there is none
*/
public SortedSet<T> firstSubset(final SortedSet<T> set) {
if (rootNodes.isEmpty() || set == null || set.isEmpty()) {
Expand Down Expand Up @@ -138,7 +134,7 @@ private void allSubsets(final SortedSet<T> set, final SortedMap<T, UBNode<T>> fo

private void allSupersets(final SortedSet<T> set, final SortedMap<T, UBNode<T>> forest,
final Set<SortedSet<T>> supersets) {
final Set<UBNode<T>> nodes = getAllNodesContainingElementsLessThan(set, forest, set.first());
final Set<UBNode<T>> nodes = getAllNodesContainingElementsLessThan(forest, set.first());
for (final UBNode<T> node : nodes) {
allSupersets(set, node.children(), supersets);
}
Expand Down Expand Up @@ -172,8 +168,7 @@ private Set<UBNode<T>> getAllNodesContainingElements(final SortedSet<T> set, fin
return nodes;
}

private Set<UBNode<T>> getAllNodesContainingElementsLessThan(final SortedSet<T> set,
final SortedMap<T, UBNode<T>> forest,
private Set<UBNode<T>> getAllNodesContainingElementsLessThan(final SortedMap<T, UBNode<T>> forest,
final T element) {
final Set<UBNode<T>> nodes = new LinkedHashSet<>();
for (final UBNode<T> node : forest.values()) {
Expand Down
13 changes: 5 additions & 8 deletions src/main/java/com/booleworks/logicng/explanations/drup/DRUPTrim.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ private static int index(final int lit) {
* @param originalProblem the clauses of the original problem
* @param proof the clauses of the proof
* @return the result of the DRUP execution from which the UNSAT core can be
* generated
* generated
*/
public DRUPResult compute(final LNGVector<LNGIntVector> originalProblem, final LNGVector<LNGIntVector> proof) {
final DRUPResult result = new DRUPResult();
Expand All @@ -95,8 +95,6 @@ private static class Solver {
private final LNGVector<LNGIntVector> core;
private final boolean delete;
private LNGIntVector DB;
private int nVars;
private int nClauses;
private int[] falseStack;
private int[] reason;
private int[] internalFalse;
Expand All @@ -108,7 +106,6 @@ private static class Solver {
private int count;
private int adlemmas;
private int lemmas;
private int time;

private Solver(final LNGVector<LNGIntVector> originalProblem, final LNGVector<LNGIntVector> proof) {
this.originalProblem = originalProblem;
Expand Down Expand Up @@ -300,18 +297,18 @@ int matchClause(final LNGIntVector clauselist, final int[] _marks, final int mar
* Parses the input and returns {@code true} if further processing is
* required and {@code false} if the formula is trivially UNSAT.
* @return {@code true} if further processing is required and
* {@code false} if the formula is trivially UNSAT
* {@code false} if the formula is trivially UNSAT
*/
private boolean parse() {
nVars = 0;
int nVars = 0;
for (final LNGIntVector vector : originalProblem) {
for (int i = 0; i < vector.size(); i++) {
if (Math.abs(vector.get(i)) > nVars) {
nVars = Math.abs(vector.get(i));
}
}
}
nClauses = originalProblem.size();
final int nClauses = originalProblem.size();

boolean del = false;
int nZeros = nClauses;
Expand Down Expand Up @@ -426,7 +423,7 @@ private LNGVector<LNGIntVector> verify() {
final int endPtr = lemmas;
int checked = adlemmas;
final LNGIntVector buffer = new LNGIntVector();
time = DB.get(lemmasPtr - 1);
int time;

boolean gotoPostProcess = false;
if (processedPtr < assignedPtr) {
Expand Down
31 changes: 25 additions & 6 deletions src/main/java/com/booleworks/logicng/formulas/FormulaFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@
import com.booleworks.logicng.formulas.implementation.noncaching.NonCachingFormulaFactory;
import com.booleworks.logicng.formulas.printer.FormulaStringRepresentation;
import com.booleworks.logicng.functions.SubNodeFunction;
import com.booleworks.logicng.io.parsers.FormulaParser;
import com.booleworks.logicng.io.parsers.ParserException;
import com.booleworks.logicng.io.parsers.PropositionalParser;
import com.booleworks.logicng.solvers.functions.modelenumeration.ModelEnumerationConfig;
import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig;
import com.booleworks.logicng.solvers.sat.SATSolverConfig;
Expand Down Expand Up @@ -49,6 +51,7 @@
*/
public abstract class FormulaFactory {

protected FormulaParser parser;
protected final String name;
protected final FormulaStringRepresentation stringRepresentation;
protected final FormulaFactoryConfig.FormulaMergeStrategy formulaMergeStrategy;
Expand Down Expand Up @@ -93,7 +96,8 @@ protected FormulaFactory(final FormulaFactoryConfig config) {
auxVarCounters = new ConcurrentHashMap<>();
clear();
subformulaFunction = new SubNodeFunction(this);
auxVarPrefix = "@AUX_" + this.name + "_";
auxVarPrefix = "@AUX_" + name + "_";
parser = new PropositionalParser(this);
readOnly = false;
}

Expand Down Expand Up @@ -723,7 +727,7 @@ private Formula constructCCUnsafe(final CType comparator, final int rhs,
* @param coefficients the coefficients or {@code null} if there are no
* coefficients to test
* @return {@code true} if the given pseudo-Boolean constraint is a
* cardinality constraint, otherwise {@code false}
* cardinality constraint, otherwise {@code false}
*/
private static boolean isCC(final CType comparator, final int rhs, final Collection<? extends Literal> literals,
final List<Integer> coefficients) {
Expand Down Expand Up @@ -752,7 +756,7 @@ private static boolean isCC(final CType comparator, final int rhs, final Collect
* @param comparator the comparator
* @param rhs the right-hand side
* @return {@code true} if the trivial case is a tautology, {@code false} if
* the trivial case is a contradiction
* the trivial case is a contradiction
*/
private static boolean evaluateTrivialPBConstraint(final CType comparator, final int rhs) {
switch (comparator) {
Expand Down Expand Up @@ -909,13 +913,28 @@ public long numberOfNodes(final Formula formula) {
return formula.apply(subformulaFunction).size();
}

/**
* Sets a formula parser for this factory. By default, this will be the
* included JavaCC-based formula parser. But you could replace with an
* ANTLR-based parser or your application-specific parser.
* @param parser the formula parser
*/
public void setParser(final FormulaParser parser) {
this.parser = parser;
}

/**
* Parses a given string to a formula using a pseudo boolean parser.
* @param string a string representing the formula
* @return the formula
* @throws ParserException if the parser throws an exception
*/
public abstract Formula parse(final String string) throws ParserException;
public Formula parse(final String string) throws ParserException {
if (readOnly) {
throwReadOnlyException();
}
return parser.parse(string);
}

/**
* Adds a given formula to a list of operands. If the formula is the neutral
Expand Down Expand Up @@ -966,7 +985,7 @@ private byte addFormulaAnd(final LinkedHashSet<Formula> ops, final Formula formu
* @param formulas the list of formulas
* @param formula the formula
* @return {@code true} if a given list of formulas contains a given
* formula, {@code false} otherwise
* formula, {@code false} otherwise
*/
private boolean containsComplement(final LinkedHashSet<Formula> formulas, final Formula formula) {
if (!simplifyComplementaryOperands) {
Expand All @@ -981,7 +1000,7 @@ private boolean containsComplement(final LinkedHashSet<Formula> formulas, final
* otherwise {@code null} is returned.
* @param formula the formula
* @return the negated formula if the negation exists in the cache,
* otherwise {@code null}
* otherwise {@code null}
*/
protected abstract Formula negateOrNull(final Formula formula);

Expand Down
Loading

0 comments on commit 68f49ac

Please sign in to comment.