Skip to content

Commit

Permalink
Clean up code
Browse files Browse the repository at this point in the history
  • Loading branch information
Apfelbeet committed May 1, 2024
1 parent 5675842 commit 4c19bb8
Show file tree
Hide file tree
Showing 12 changed files with 136 additions and 197 deletions.
26 changes: 7 additions & 19 deletions src/main/java/com/booleworks/logicng/csp/Csp.java
Original file line number Diff line number Diff line change
Expand Up @@ -14,27 +14,23 @@ public class Csp {
private final Set<IntegerVariable> integerVariables;
private final Set<Variable> booleanVariables;
private Set<IntegerClause> clauses;
private final CspFactory f;

private Csp(final CspFactory f) {
private Csp() {
this.integerVariables = new TreeSet<>();
this.booleanVariables = new TreeSet<>();
this.clauses = new TreeSet<>();
this.f = f;
}

private Csp(final Csp other) {
this.integerVariables = new TreeSet<>(other.integerVariables);
this.booleanVariables = new TreeSet<>(other.booleanVariables);
this.clauses = new TreeSet<>(other.clauses);
this.f = other.f;
}

public Csp(final CspFactory f, final Set<IntegerVariable> integerVariables, final Set<Variable> booleanVariables, final Set<IntegerClause> clauses) {
public Csp(final Set<IntegerVariable> integerVariables, final Set<Variable> booleanVariables, final Set<IntegerClause> clauses) {
this.integerVariables = integerVariables;
this.booleanVariables = booleanVariables;
this.clauses = clauses;
this.f = f;
}

public Set<IntegerVariable> getIntegerVariables() {
Expand All @@ -49,10 +45,6 @@ public Set<IntegerClause> getClauses() {
return clauses;
}

public CspFactory getCspFactory() {
return f;
}

@Override
public String toString() {
return "Csp{" +
Expand All @@ -62,14 +54,14 @@ public String toString() {
'}';
}

public static Csp fromClauses(final CspFactory f, final Set<IntegerClause> clauses) {
public static Csp fromClauses(final Set<IntegerClause> clauses) {
final Set<IntegerVariable> intVars = new TreeSet<>();
final Set<Variable> boolVars = new TreeSet<>();
for (final IntegerClause clause : clauses) {
intVars.addAll(clause.getArithmeticLiterals().stream().flatMap(v -> v.getVariables().stream()).collect(Collectors.toSet()));
boolVars.addAll(clause.getBoolLiterals().stream().map(Literal::variable).collect(Collectors.toSet()));
}
return new Csp(f, intVars, boolVars, clauses);
return new Csp(intVars, boolVars, clauses);
}

public static Csp merge(final CspFactory f, final Csp... csps) {
Expand All @@ -78,11 +70,11 @@ public static Csp merge(final CspFactory f, final Csp... csps) {

public static Csp merge(final CspFactory f, final Collection<Csp> csps) {
if (csps.isEmpty()) {
return new Csp(f);
return new Csp();
} else if (csps.size() == 1) {
return csps.iterator().next();
} else {
final Csp newCsp = new Csp(f);
final Csp newCsp = new Csp();
for (final Csp csp : csps) {
newCsp.integerVariables.addAll(csp.integerVariables);
newCsp.booleanVariables.addAll(csp.booleanVariables);
Expand All @@ -96,7 +88,7 @@ public static class Builder {
private Csp csp;

public Builder(final CspFactory f) {
csp = new Csp(f);
csp = new Csp();
}

public Builder(final Csp csp) {
Expand Down Expand Up @@ -139,10 +131,6 @@ public Set<IntegerClause> getClauses() {
return csp.clauses;
}

public CspFactory getCspFactory() {
return csp.f;
}

@Override
public String toString() {
return csp.toString();
Expand Down
104 changes: 61 additions & 43 deletions src/main/java/com/booleworks/logicng/csp/CspFactory.java
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
package com.booleworks.logicng.csp;

import com.booleworks.logicng.csp.encodings.CspEncoder;
import com.booleworks.logicng.csp.encodings.CspEncodingContext;
import com.booleworks.logicng.csp.encodings.OrderDecoding;
import com.booleworks.logicng.csp.encodings.OrderEncoding;
import com.booleworks.logicng.csp.encodings.OrderReduction;
import com.booleworks.logicng.csp.predicates.AllDifferentPredicate;
Expand All @@ -14,6 +14,7 @@
import com.booleworks.logicng.csp.terms.NegationFunction;
import com.booleworks.logicng.csp.terms.SubtractionFunction;
import com.booleworks.logicng.csp.terms.Term;
import com.booleworks.logicng.datastructures.Assignment;
import com.booleworks.logicng.datastructures.EncodingResult;
import com.booleworks.logicng.formulas.Formula;
import com.booleworks.logicng.formulas.FormulaFactory;
Expand Down Expand Up @@ -73,6 +74,28 @@ public CspFactory(final FormulaFactory formulaFactory) {
this.integerConstants.put(1, this.one);
}

public CspFactory(final CspFactory other, final FormulaFactory formulaFactory) {
this.formulaFactory = formulaFactory;
this.integerConstants = new HashMap<>(other.integerConstants);
this.integerVariables = new HashMap<>(other.integerVariables);
this.unaryMinusTerms = new HashMap<>(other.unaryMinusTerms);
this.addTerms = new HashMap<>(other.addTerms);
this.subTerms = new HashMap<>(other.subTerms);
this.mulTerms = new HashMap<>(other.mulTerms);
this.eqPredicates = new HashMap<>(other.eqPredicates);
this.nePredicates = new HashMap<>(other.nePredicates);
this.lePredicates = new HashMap<>(other.lePredicates);
this.ltPredicates = new HashMap<>(other.ltPredicates);
this.gePredicates = new HashMap<>(other.gePredicates);
this.gtPredicates = new HashMap<>(other.gtPredicates);
this.allDifferentPredicates = new HashMap<>(other.allDifferentPredicates);
this.auxCounter = other.auxCounter;
this.zero = new IntegerConstant(this, 0);
this.one = new IntegerConstant(this, 1);
this.integerConstants.put(0, this.zero);
this.integerConstants.put(1, this.one);
}

public IntegerConstant zero() {
return zero;
}
Expand Down Expand Up @@ -272,15 +295,6 @@ public ComparisonPredicate eq(final Term left, final Term right) {
if (foundFormula != null) {
return foundFormula;
}
//if (left.equals(right)) {
// eqPredicates.put(operands, formulaFactory.verum());
// return formulaFactory.verum();
//}
//if (left instanceof IntegerConstant && right instanceof IntegerConstant) {
// final Constant constant = formulaFactory.constant(((IntegerConstant) left).getValue() == ((IntegerConstant) right).getValue());
// eqPredicates.put(operands, constant);
// return constant;
//}
final ComparisonPredicate predicate = new ComparisonPredicate(this, CspPredicate.Type.EQ, left, right);
eqPredicates.put(operands, predicate);
return predicate;
Expand All @@ -292,11 +306,6 @@ public ComparisonPredicate ne(final Term left, final Term right) {
if (foundFormula != null) {
return foundFormula;
}
//if (left instanceof IntegerConstant && right instanceof IntegerConstant) {
// final Constant constant = formulaFactory.constant(((IntegerConstant) left).getValue() != ((IntegerConstant) right).getValue());
// nePredicates.put(operands, constant);
// return constant;
//}
final ComparisonPredicate predicate = new ComparisonPredicate(this, CspPredicate.Type.NE, left, right);
nePredicates.put(operands, predicate);
return predicate;
Expand Down Expand Up @@ -325,11 +334,6 @@ private ComparisonPredicate processComparison(final Term left, final Term right,
if (foundFormula != null) {
return foundFormula;
}
//if (left instanceof IntegerConstant && right instanceof IntegerConstant) {
// final Constant constant = formulaFactory.constant(test.test((IntegerConstant) left, (IntegerConstant) right));
// cache.put(operands, constant);
// return constant;
//}
final ComparisonPredicate predicate = new ComparisonPredicate(this, type, left, right);
cache.put(operands, predicate);
return predicate;
Expand All @@ -341,57 +345,71 @@ public AllDifferentPredicate allDifferent(final Collection<Term> terms) {
if (foundFormula != null) {
return foundFormula;
}
// zero or one terms always have different values
//if (terms.size() <= 1) {
// allDifferentPredicates.put(operands, formulaFactory.verum());
// return formulaFactory.verum();
//}
final AllDifferentPredicate predicate = new AllDifferentPredicate(this, operands);
allDifferentPredicates.put(operands, predicate);
return predicate;
}

public FormulaFactory getFormulaFactory() {
public FormulaFactory formulaFactory() {
return formulaFactory;
}

public Csp buildCsp(final Collection<CspPredicate> predicates) {
final Set<IntegerClause> clauses = predicates.stream().flatMap(p -> p.decompose().stream()).collect(Collectors.toSet());
return Csp.fromClauses(this, clauses);
return Csp.fromClauses(clauses);
}

public Csp buildCsp(final CspPredicate... predicates) {
return buildCsp(Arrays.asList(predicates));
}

public List<Formula> encodeCsp(final Csp csp, final CspEncodingContext context, final CspEncoder.Algorithm algorithm) {
CspEncoder encoder = new CspEncoder(csp, algorithm);
EncodingResult result = EncodingResult.resultForFormula(context.factory().getFormulaFactory());
encoder.encode(context, result);
return result.result();
public List<Formula> encodeCsp(final Csp csp, final CspEncodingContext context) {
final Csp newCsp;
final EncodingResult result = EncodingResult.resultForFormula(formulaFactory);
switch (context.getAlgorithm()) {
case Order:
newCsp = OrderReduction.reduce(csp, context, formulaFactory);
OrderEncoding.encode(newCsp, context, result, this);
return result.result();
default:
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + context.getAlgorithm());
}
}

public List<Formula> encodeVariable(final IntegerVariable variable, final CspEncodingContext context, final CspEncoder.Algorithm algorithm) {
final EncodingResult result = EncodingResult.resultForFormula(context.factory().getFormulaFactory());
switch (algorithm) {
public List<Formula> encodeVariable(final IntegerVariable variable, final CspEncodingContext context) {
final EncodingResult result = EncodingResult.resultForFormula(formulaFactory);
switch (context.getAlgorithm()) {
case Order:
OrderEncoding.encodeVariable(variable, context, result);
OrderEncoding.encodeVariable(variable, context, result, this);
return result.result();
default:
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + algorithm);
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + context.getAlgorithm());
}
}

public List<Formula> encodeConstraint(final CspPredicate predicate, final CspEncodingContext context, final CspEncoder.Algorithm algorithm) {
public List<Formula> encodeConstraint(final CspPredicate predicate, final CspEncodingContext context) {
Set<IntegerClause> clauses = predicate.decompose();
EncodingResult result = EncodingResult.resultForFormula(context.factory().getFormulaFactory());
switch (algorithm) {
final EncodingResult result = EncodingResult.resultForFormula(formulaFactory);
switch (context.getAlgorithm()) {
case Order:
clauses = OrderReduction.reduce(clauses, context);
OrderEncoding.encodeClauses(clauses, context, result);
clauses = OrderReduction.reduce(clauses, context, formulaFactory);
OrderEncoding.encodeClauses(clauses, context, result, this);
return result.result();
default:
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + algorithm);
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + context.getAlgorithm());
}
}

public CspAssignment decode(final Assignment model, final Csp csp, final CspEncodingContext context) {
return decode(model, csp.getIntegerVariables(), context);
}

public CspAssignment decode(final Assignment model, final Collection<IntegerVariable> variables, final CspEncodingContext context) {
switch (context.getAlgorithm()) {
case Order:
return OrderDecoding.decode(model, variables, context, this);
default:
throw new UnsupportedOperationException("Unsupported csp encoding algorithm: " + context.getAlgorithm());
}
}
}
Expand Down
6 changes: 3 additions & 3 deletions src/main/java/com/booleworks/logicng/csp/CspPropagation.java
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,21 @@
import java.util.stream.Collectors;

public class CspPropagation {
public static Csp propagate(final Csp csp) {
public static Csp propagate(final Csp csp, final CspFactory cf) {
final Map<IntegerVariable, IntegerVariable> restrictions = new TreeMap<>();
boolean changed = true;
while (changed) {
changed = false;
for (final IntegerClause clause : csp.getClauses()) {
if (calculateNewBounds(clause, restrictions, csp.getCspFactory())) {
if (calculateNewBounds(clause, restrictions, cf)) {
changed = true;
}
}
}
if (!restrictions.isEmpty()) {
final Set<IntegerClause> newClauses =
csp.getClauses().stream().map(c -> rebuildClause(c, restrictions)).filter(c -> !c.isValid()).collect(Collectors.toSet());
return Csp.fromClauses(csp.getCspFactory(), newClauses);
return Csp.fromClauses(newClauses);
} else {
return csp;
}
Expand Down
11 changes: 5 additions & 6 deletions src/main/java/com/booleworks/logicng/csp/LinearExpression.java
Original file line number Diff line number Diff line change
Expand Up @@ -225,23 +225,22 @@ public int hashCode() {
@Override
public String toString() {
final StringBuilder sb = new StringBuilder();
sb.append("(add ");
sb.append("Add<");
for (final IntegerVariable v : coef.keySet()) {
final long c = getA(v);
if (c == 0) {
} else if (c == 1) {
sb.append(v.toString());
} else {
sb.append("(mul ");
sb.append("Mul<");
sb.append(c);
sb.append(" ");
sb.append(",");
sb.append(v.toString());
sb.append(")");
sb.append(">");
}
sb.append(" ");
}
sb.append(b);
sb.append(")");
sb.append(">");
return sb.toString();
}

Expand Down
62 changes: 0 additions & 62 deletions src/main/java/com/booleworks/logicng/csp/encodings/CspEncoder.java

This file was deleted.

Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
package com.booleworks.logicng.csp.encodings;

public enum CspEncodingAlgorithm {
Order
}
Loading

0 comments on commit 4c19bb8

Please sign in to comment.