diff --git a/prism/src/param/CachedFunction.java b/prism/src/param/CachedFunction.java index 5f829ae8..f54e22c1 100644 --- a/prism/src/param/CachedFunction.java +++ b/prism/src/param/CachedFunction.java @@ -156,4 +156,10 @@ final class CachedFunction extends Function { public boolean isZero() { return factory.isZero(this); } + + @Override + public boolean isConstant() + { + return factory.isConstant(this); + } } diff --git a/prism/src/param/CachedFunctionFactory.java b/prism/src/param/CachedFunctionFactory.java index aff80d09..133f4cd1 100644 --- a/prism/src/param/CachedFunctionFactory.java +++ b/prism/src/param/CachedFunctionFactory.java @@ -320,6 +320,11 @@ final class CachedFunctionFactory extends FunctionFactory { return function.isZero(); } + public boolean isConstant(CachedFunction cached) { + Function function = getFunctionFromCache(cached); + return function.isConstant(); + } + @Override Function getNaN() { return makeUnique(context.getNaN()); diff --git a/prism/src/param/DagFunction.java b/prism/src/param/DagFunction.java index 4bb2866a..265f37b0 100644 --- a/prism/src/param/DagFunction.java +++ b/prism/src/param/DagFunction.java @@ -170,4 +170,13 @@ public class DagFunction extends Function { public int getType() { return type; } + + @Override + public boolean isConstant() + { + if (type != NORMAL) + return true; + + return dagFactory.isConstant(num) && dagFactory.isConstant(den); + } } diff --git a/prism/src/param/DagFunctionFactory.java b/prism/src/param/DagFunctionFactory.java index 8da974d8..a5fd2999 100644 --- a/prism/src/param/DagFunctionFactory.java +++ b/prism/src/param/DagFunctionFactory.java @@ -334,6 +334,29 @@ class DagFunctionFactory extends FunctionFactory { return op == zero; } + /** + * Returns true if the tree rooted in {@code op} + * is guaranteed to represent a constant value. + */ + public boolean isConstant(DagOperator op) { + if (op instanceof Number) { + return true; + } else if (op instanceof Variable) { + return false; + } else if (op instanceof Negate) { + Negate opNegate = (Negate) op; + return isConstant(opNegate.getWhat()); + } else if (op instanceof Add) { + Add opAdd = (Add) op; + return isConstant(opAdd.getOp1()) && isConstant(opAdd.getOp2()); + } else if (op instanceof Multiply) { + Multiply opMultiply = (Multiply) op; + return isConstant(opMultiply.getOp1()) && isConstant(opMultiply.getOp2()); + } else { + throw new RuntimeException("invalid operator"); + } + } + public String toString(DagFunction op) { return "(" + op.getNum().toString() + ")/(" + op.getDen().toString() + ")"; } diff --git a/prism/src/param/Function.java b/prism/src/param/Function.java index 10559d43..d6eaa7a1 100644 --- a/prism/src/param/Function.java +++ b/prism/src/param/Function.java @@ -174,6 +174,12 @@ public abstract class Function extends StateValue */ abstract boolean isZero(); + /** + * Returns true iff this function is guaranteed to return a constant value. + * @return true iff this function is guaranteed to return a constant value + */ + abstract public boolean isConstant(); + /** * Multiplies {@code byNumber} with this function. * diff --git a/prism/src/param/JasFunction.java b/prism/src/param/JasFunction.java index 2b06b567..411999b7 100644 --- a/prism/src/param/JasFunction.java +++ b/prism/src/param/JasFunction.java @@ -343,4 +343,16 @@ final class JasFunction extends Function { } return jas.isZERO(); } + + @Override + public boolean isConstant() + { + // inf, NaN are constant + if (type != NORMAL) + return true; + + return jas.isConstant(); + } + + }