param.Function: add isConstant() method

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11643 bbc10eb1-c90d-0410-af57-cb519fbb1720

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);
+	}
 }

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());

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);
+	}
 }

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() + ")";
 	}

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.
 	 * 

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();
+	}
+
+
 }