Skip to content

Commit

Permalink
removed an ugly spot in the formula factory code
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Jan 19, 2020
1 parent 10af7d1 commit b98bf36
Showing 1 changed file with 33 additions and 43 deletions.
76 changes: 33 additions & 43 deletions src/main/java/org/logicng/formulas/FormulaFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,6 @@ public class FormulaFactory {
private final PBEncoder pbEncoder;
private final CNFEncoder cnfEncoder;
private final PseudoBooleanParser parser;
private final boolean[] formulaAdditionResult;
Map<String, Variable> posLiterals;
Map<String, Literal> negLiterals;
Set<Variable> generatedVariables;
Expand Down Expand Up @@ -121,7 +120,6 @@ public FormulaFactory(final String name, final FormulaStringRepresentation strin
this.cFalse = new CFalse(this);
this.cTrue = new CTrue(this);
this.clear();
this.formulaAdditionResult = new boolean[2];
this.stringRepresentation = stringRepresentation;
this.configurations = new EnumMap<>(ConfigurationType.class);
this.cnfEncoder = new CNFEncoder(this);
Expand Down Expand Up @@ -365,7 +363,7 @@ public CFalse falsum() {
* @return the constant
*/
public Constant constant(final boolean value) {
return value ? cTrue : cFalse;
return value ? this.cTrue : this.cFalse;
}

/**
Expand Down Expand Up @@ -899,20 +897,20 @@ private LinkedHashSet<Formula> condenseOperandsOr(final Collection<? extends For
for (final Formula form : operands) {
if (form.type() == OR) {
for (final Formula f : ((NAryOperator) form).operands) {
this.addFormulaOr(ops, f);
if (!this.formulaAdditionResult[0]) {
final byte ret = this.addFormulaOr(ops, f);
if (ret == 0x00) {
return null;
}
if (!this.formulaAdditionResult[1]) {
if (ret == 0x02) {
this.cnfCheck = false;
}
}
} else {
this.addFormulaOr(ops, form);
if (!this.formulaAdditionResult[0]) {
final byte ret = this.addFormulaOr(ops, form);
if (ret == 0x00) {
return null;
}
if (!this.formulaAdditionResult[1]) {
if (ret == 0x02) {
this.cnfCheck = false;
}
}
Expand All @@ -931,20 +929,20 @@ private LinkedHashSet<Formula> condenseOperandsAnd(final Collection<? extends Fo
for (final Formula form : operands) {
if (form.type() == AND) {
for (final Formula f : ((NAryOperator) form).operands) {
this.addFormulaAnd(ops, f);
if (!this.formulaAdditionResult[0]) {
final byte ret = this.addFormulaAnd(ops, f);
if (ret == 0x00) {
return null;
}
if (!this.formulaAdditionResult[1]) {
if (ret == 0x02) {
this.cnfCheck = false;
}
}
} else {
this.addFormulaAnd(ops, form);
if (!this.formulaAdditionResult[0]) {
final byte ret = this.addFormulaAnd(ops, form);
if (ret == 0x00) {
return null;
}
if (!this.formulaAdditionResult[1]) {
if (ret == 0x02) {
this.cnfCheck = false;
}
}
Expand Down Expand Up @@ -983,46 +981,38 @@ public Formula parse(final String string) throws ParserException {
/**
* Adds a given formula to a list of operands. If the formula is the neutral element for the respective n-ary
* operation it will be skipped. If a complementary formula is already present in the list of operands or the
* formula is the dual element, {@code false} is stored as first element of the result array,
* otherwise {@code true} is the first element of the result array. If the added formula was a literal, the second
* element in the result array is {@code true}, {@code false} otherwise.
* formula is the dual element, 0x00 is returned. If the added formula was a literal 0x01 is returned,
* otherwise 0x02 is returned.
* @param ops the list of operands
* @param f the formula
*/
private void addFormulaOr(final LinkedHashSet<Formula> ops, final Formula f) {
private byte addFormulaOr(final LinkedHashSet<Formula> ops, final Formula f) {
if (f.type == FALSE) {
this.formulaAdditionResult[0] = true;
this.formulaAdditionResult[1] = true;
return 0x01;
} else if (f.type == TRUE || containsComplement(ops, f)) {
this.formulaAdditionResult[0] = false;
this.formulaAdditionResult[1] = false;
return 0x00;
} else {
ops.add(f);
this.formulaAdditionResult[0] = true;
this.formulaAdditionResult[1] = f.type == LITERAL;
return (byte) (f.type == LITERAL ? 0x01 : 0x02);
}
}

/**
* Adds a given formula to a list of operands. If the formula is the neutral element for the respective n-ary
* operation it will be skipped. If a complementary formula is already present in the list of operands or the
* formula is the dual element, {@code false} is stored as first element of the result array,
* otherwise {@code true} is the first element of the result array. If the added formula was a clause, the second
* element in the result array is {@code true}, {@code false} otherwise.
* formula is the dual element, 0x00 is returned. If the added formula was a clause, 0x01 is returned,
* otherwise 0x02 is returned.
* @param ops the list of operands
* @param f the formula
*/
private void addFormulaAnd(final LinkedHashSet<Formula> ops, final Formula f) {
private byte addFormulaAnd(final LinkedHashSet<Formula> ops, final Formula f) {
if (f.type() == TRUE) {
this.formulaAdditionResult[0] = true;
this.formulaAdditionResult[1] = true;
return 0x01;
} else if (f.type == FALSE || containsComplement(ops, f)) {
this.formulaAdditionResult[0] = false;
this.formulaAdditionResult[1] = false;
return 0x00;
} else {
ops.add(f);
this.formulaAdditionResult[0] = true;
this.formulaAdditionResult[1] = f.type == LITERAL || f.type == OR && ((Or) f).isCNFClause();
return (byte) (f.type == LITERAL || f.type == OR && ((Or) f).isCNFClause() ? 0x01 : 0x02);
}
}

Expand All @@ -1041,25 +1031,25 @@ public Formula importFormula(final Formula formula) {
return imported;
}

private void adjustCounters(Formula formula) {
for (Variable variable : formula.variables()) {
private void adjustCounters(final Formula formula) {
for (final Variable variable : formula.variables()) {
if (variable.name().startsWith(CC_PREFIX)) {
String[] tokens = variable.name().split("_");
int counter = Integer.parseInt(tokens[tokens.length - 1]);
final String[] tokens = variable.name().split("_");
final int counter = Integer.parseInt(tokens[tokens.length - 1]);
if (this.ccCounter < counter) {
this.ccCounter = counter + 1;
}
}
if (variable.name().startsWith(CNF_PREFIX)) {
String[] tokens = variable.name().split("_");
int counter = Integer.parseInt(tokens[tokens.length - 1]);
final String[] tokens = variable.name().split("_");
final int counter = Integer.parseInt(tokens[tokens.length - 1]);
if (this.cnfCounter < counter) {
this.cnfCounter = counter + 1;
}
}
if (variable.name().startsWith(PB_PREFIX)) {
String[] tokens = variable.name().split("_");
int counter = Integer.parseInt(tokens[tokens.length - 1]);
final String[] tokens = variable.name().split("_");
final int counter = Integer.parseInt(tokens[tokens.length - 1]);
if (this.pbCounter < counter) {
this.pbCounter = counter + 1;
}
Expand Down

0 comments on commit b98bf36

Please sign in to comment.