diff --git a/src/main/java/org/jreliability/bdd/BDDConstraint.java b/src/main/java/org/jreliability/bdd/BDDConstraint.java index 828a249..9a3590f 100644 --- a/src/main/java/org/jreliability/bdd/BDDConstraint.java +++ b/src/main/java/org/jreliability/bdd/BDDConstraint.java @@ -158,7 +158,7 @@ protected void eliminateZeroCoefficients() { * values. */ protected void gcd() { - try { + if(!lhs.isEmpty()){ int gcd = lhs.get(0).getCoefficient(); for (Literal literal : lhs) { int coefficient = literal.getCoefficient(); @@ -173,11 +173,7 @@ protected void gcd() { 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() } - } /** diff --git a/src/main/java/org/jreliability/bdd/BDDTTRF.java b/src/main/java/org/jreliability/bdd/BDDTTRF.java index 45e4fb9..eec3fde 100644 --- a/src/main/java/org/jreliability/bdd/BDDTTRF.java +++ b/src/main/java/org/jreliability/bdd/BDDTTRF.java @@ -67,8 +67,7 @@ public BDDTTRF(BDDProvider provider) { * booleanfunction.Term, org.apache.commons.collections15.Transformer) */ @Override - public ReliabilityFunction convert(Term term, - Transformer functionTransformer) { + public ReliabilityFunction convert(Term term, Transformer functionTransformer) { return convert(term, functionTransformer, null); } @@ -80,8 +79,7 @@ public ReliabilityFunction convert(Term term, * org.apache.commons.collections15.Predicate) */ @Override - public ReliabilityFunction convert(Term term, - Transformer functionTransformer, + public ReliabilityFunction convert(Term term, Transformer functionTransformer, Predicate existsPredicate) { BDD bdd = convertToBDD(term, existsPredicate); return convert(bdd, functionTransformer); @@ -98,10 +96,8 @@ public ReliabilityFunction convert(Term term, * @return a reliability function from the given bdd and function * functionTransformer */ - public ReliabilityFunction convert(BDD bdd, - Transformer functionTransformer) { - BDDReliabilityFunction function = new BDDReliabilityFunction(bdd, - functionTransformer); + public ReliabilityFunction convert(BDD bdd, Transformer functionTransformer) { + BDDReliabilityFunction function = new BDDReliabilityFunction(bdd, functionTransformer); bdd.free(); return function; } @@ -174,8 +170,7 @@ protected BDD transform(Term term) { NOTTerm notTerm = (NOTTerm) term; bdd = transformNOT(notTerm); } else { - throw new IllegalArgumentException( - "Unknown Term class in boolean function."); + throw new IllegalArgumentException("Unknown Term class in boolean function."); } return bdd; } @@ -232,7 +227,7 @@ protected BDD transformLinear(LinearTerm term) { } Comparator comparator = term.getComparator(); int rhs = term.getRHS(); - return BDDs.getBDD(coefficients, bdds, comparator, rhs); + return BDDs.getBDD(coefficients, bdds, comparator, rhs, provider); } /** diff --git a/src/main/java/org/jreliability/bdd/BDDs.java b/src/main/java/org/jreliability/bdd/BDDs.java index aa866f5..035d3cd 100644 --- a/src/main/java/org/jreliability/bdd/BDDs.java +++ b/src/main/java/org/jreliability/bdd/BDDs.java @@ -91,20 +91,20 @@ public static Set> getNodes(T t, BDD bdd) { * the right hand side value * @return the BDD representing this linear constraint */ - public static BDD getBDD(List coeffs, List> vars, LinearTerm.Comparator comp, int rhs) { + public static BDD getBDD(List coeffs, List> vars, LinearTerm.Comparator comp, int rhs, BDDProvider provider) { assert (coeffs.size() == vars.size()); BDD result; switch (comp) { case EQUAL: - BDD ge = getBDD(coeffs, vars, LinearTerm.Comparator.GREATEREQUAL, rhs); - BDD le = getBDD(coeffs, vars, LinearTerm.Comparator.LESSEQUAL, rhs); + BDD ge = getBDD(coeffs, vars, LinearTerm.Comparator.GREATEREQUAL, rhs, provider); + BDD le = getBDD(coeffs, vars, LinearTerm.Comparator.LESSEQUAL, rhs, provider); ge.andWith(le); result = ge; break; case GREATER: - result = getBDD(coeffs, vars, LinearTerm.Comparator.GREATEREQUAL, rhs + 1); + result = getBDD(coeffs, vars, LinearTerm.Comparator.GREATEREQUAL, rhs + 1, provider); break; case GREATEREQUAL: List> lits = new ArrayList<>(); @@ -120,25 +120,24 @@ public static BDD getBDD(List coeffs, List> vars, LinearT * If 0 >= rhs, return true BDD; else return false BDD */ if(constraint.getLhs().isEmpty()) { - BDDProvider provider = lits.get(0).getVariable().getProvider(); if(0 >= constraint.getRhs()) { result = provider.one(); } else { result = provider.zero(); } } else{ - result = getConstraintBDD(constraint); + result = getConstraintBDD(constraint, provider); } break; case LESS: - result = getBDD(coeffs, vars, LinearTerm.Comparator.LESSEQUAL, rhs - 1); + result = getBDD(coeffs, vars, LinearTerm.Comparator.LESSEQUAL, rhs - 1, provider); break; case LESSEQUAL: List negativeCoeffs = new ArrayList<>(); for (int c : coeffs) { negativeCoeffs.add(-c); } - result = getBDD(negativeCoeffs, vars, LinearTerm.Comparator.GREATEREQUAL, -rhs); + result = getBDD(negativeCoeffs, vars, LinearTerm.Comparator.GREATEREQUAL, -rhs, provider); break; default: throw new IllegalArgumentException("Unknown comparator in LinearTerm: " + comp); @@ -156,7 +155,7 @@ public static BDD getBDD(List coeffs, List> vars, LinearT * the greater-equal constraint * @return the bdd representation of the given constraint */ - protected static BDD getConstraintBDD(BDDConstraint constraint) { + protected static BDD getConstraintBDD(BDDConstraint constraint, BDDProvider provider) { List> literals = constraint.getLhs(); Collections.sort(literals, new Comparator>() { @@ -167,7 +166,6 @@ public int compare(Literal o1, Literal o2) { }); int materialLeft = 0; - BDDProvider provider = literals.get(0).getVariable().getProvider(); for (Literal literal : literals) { int coefficient = literal.getCoefficient(); materialLeft += coefficient; diff --git a/src/test/java/org/jreliability/bdd/AbstractBDDOperatorTest.java b/src/test/java/org/jreliability/bdd/AbstractBDDOperatorTest.java index 9317cd2..5c6abbc 100644 --- a/src/test/java/org/jreliability/bdd/AbstractBDDOperatorTest.java +++ b/src/test/java/org/jreliability/bdd/AbstractBDDOperatorTest.java @@ -397,7 +397,7 @@ public void testGetBDDGreaterEqual() { BDD a = provider.get("a"); BDD b = provider.get("b"); BDD c = provider.get("c"); - BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.GREATEREQUAL, 2); + BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.GREATEREQUAL, 2, provider); BDD ref1 = a.and(b); BDD ref2 = b.and(c); @@ -419,7 +419,7 @@ public void testGetBDDGreater() { BDD a = provider.get("a"); BDD b = provider.get("b"); BDD c = provider.get("c"); - BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.GREATER, 2); + BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.GREATER, 2, provider); BDD ref1 = a.and(b).and(c); Assert.assertEquals(test, ref1); @@ -437,7 +437,7 @@ public void testGetBDDLess() { BDD a = provider.get("a"); BDD b = provider.get("b"); BDD c = provider.get("c"); - BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.LESS, 1); + BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.LESS, 1, provider); BDD ref1 = a.not().and(b.not()).and(c.not()); Assert.assertEquals(test, ref1); @@ -455,7 +455,7 @@ public void testGetBDDLessEqual() { BDD a = provider.get("a"); BDD b = provider.get("b"); BDD c = provider.get("c"); - BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.LESSEQUAL, 0); + BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.LESSEQUAL, 0, provider); BDD ref1 = a.not().and(b.not()).and(c.not()); Assert.assertEquals(test, ref1); @@ -473,7 +473,7 @@ public void testGetBDDEqual() { BDD a = provider.get("a"); BDD b = provider.get("b"); BDD c = provider.get("c"); - BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.EQUAL, 1); + BDD test = BDDs.getBDD(Arrays.asList(1, 1, 1), Arrays.asList(a, b, c), Comparator.EQUAL, 1, provider); BDD ref1 = a.and(b.not()).and(c.not()); BDD ref2 = a.not().and(b).and(c.not());