Skip to content

Commit

Permalink
resolved the linearterm trim and gcd bug
Browse files Browse the repository at this point in the history
  • Loading branch information
michaelhglass committed Jul 3, 2017
1 parent a16538b commit fec9af4
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 17 deletions.
57 changes: 41 additions & 16 deletions src/main/java/org/jreliability/bdd/BDDConstraint.java
Original file line number Diff line number Diff line change
Expand Up @@ -46,8 +46,8 @@ class BDDConstraint<T> {
protected Set<BDD<T>> variables = new HashSet<BDD<T>>();

/**
* Constructs a {@code BDDConstraint} with a given right-hand-side {@code rhs}
* and left-hand-side {@code lhs}.
* Constructs a {@code BDDConstraint} with a given right-hand-side
* {@code rhs} and left-hand-side {@code lhs}.
*
* @param rhs
* the right-hand-side
Expand All @@ -61,7 +61,8 @@ public BDDConstraint(int rhs, List<Literal<T>> lhs) {

/**
* Initializes the {@code BDDConstraint} with the normalizing operations
* proposed by {@code Een & Soerrensson 2006}.
* proposed by {@code Een & Soerrensson 2006} plus zero coefficient
* elimination.
*
* @param literals
* the literals
Expand All @@ -72,6 +73,7 @@ protected void initialize(List<Literal<T>> literals) {
checkAndAddVariable(literal);
}
trim();
eliminateZeroCoefficients();
gcd();
}

Expand Down Expand Up @@ -136,23 +138,44 @@ protected void trim() {
}

/**
* Determines the greatest-common-divisor ({@code gcd}) of all {@code
* coefficients} of the {@code lhs} and the {@code rhs} and updates the
* values.
* Eliminates variables on the {@code lhs} with a zero coefficient.
*/
protected void gcd() {
int gcd = lhs.get(0).getCoefficient();
protected void eliminateZeroCoefficients() {
Set<Literal<T>> zeroCoefficients = new HashSet<Literal<T>>();
for (Literal<T> literal : lhs) {
int coefficient = literal.getCoefficient();
gcd = gcdRec(gcd, coefficient);
if (coefficient == 0) {
zeroCoefficients.add(literal);
}
}
gcd = gcdRec(gcd, rhs);
rhs = rhs / gcd;
lhs.removeAll(zeroCoefficients);

for (Literal<T> literal : lhs) {
int coefficient = literal.getCoefficient();
int newCoefficient = coefficient / gcd;
literal.setCoefficient(newCoefficient);
}

/**
* Determines the greatest-common-divisor ({@code gcd}) of all {@code
* coefficients} of the {@code lhs} and the {@code rhs} and updates the
* values.
*/
protected void gcd() {
try {
int gcd = lhs.get(0).getCoefficient();
for (Literal<T> literal : lhs) {
int coefficient = literal.getCoefficient();
gcd = gcdRec(gcd, coefficient);
}
gcd = gcdRec(gcd, rhs);
assert gcd != 0;
rhs = rhs / gcd;

for (Literal<T> literal : lhs) {
int coefficient = literal.getCoefficient();
int newCoefficient = coefficient / gcd;
literal.setCoefficient(newCoefficient);
}
} catch (IndexOutOfBoundsException e) {
// do unless lhs is empty, i.e., 0
// this may be a result of applying eliminateZeroCoefficients()
}

}
Expand Down Expand Up @@ -266,7 +289,9 @@ public void setVariable(BDD<T> variable) {
this.variable = variable;
}

/* (non-Javadoc)
/*
* (non-Javadoc)
*
* @see java.lang.Object#toString()
*/
@Override
Expand Down
16 changes: 15 additions & 1 deletion src/main/java/org/jreliability/bdd/BDDs.java
Original file line number Diff line number Diff line change
Expand Up @@ -113,8 +113,22 @@ public static <T> BDD<T> getBDD(List<Integer> coeffs, List<BDD<T>> vars, LinearT
BDD<T> v = vars.get(i);
lits.add(new Literal<>(c, v));
}

BDDConstraint<T> constraint = new BDDConstraint<>(rhs, lits);
result = getConstraintBDD(constraint);

/* Handle the case that the lhs is empty and is, thus, 0!
* If 0 >= rhs, return true BDD; else return false BDD
*/
if(constraint.getLhs().isEmpty()) {
BDDProvider<T> provider = lits.get(0).getVariable().getProvider();
if(0 >= constraint.getRhs()) {
result = provider.one();
} else {
result = provider.zero();
}
} else{
result = getConstraintBDD(constraint);
}
break;
case LESS:
result = getBDD(coeffs, vars, LinearTerm.Comparator.LESSEQUAL, rhs - 1);
Expand Down

0 comments on commit fec9af4

Please sign in to comment.