imported patch Simplify-exact.patch

prism/src/parser/ast/ASTElement.java

@@ -477,12 +477,18 @@ public abstract class ASTElement
 		return evaluatePartially(new EvaluateContextSubstate(substate, varMap));
 	}
 
+	public ASTElement simplify() throws PrismLangException
+	{
+		return simplify(false);
+	}
+	
 	/**
 	 * Simplify expressions (constant propagation, ...)
+	 * @param exact perform exact evaluation
 	 */
-	public ASTElement simplify() throws PrismLangException
+	public ASTElement simplify(boolean exact) throws PrismLangException
 	{
-		Simplify visitor = new Simplify();
+		Simplify visitor = new Simplify(exact);
 		return (ASTElement) accept(visitor);
 	}
 

prism/src/parser/visitor/Simplify.java

@@ -35,6 +35,13 @@ import prism.PrismLangException;
  */
 public class Simplify extends ASTTraverseModify
 {
+	private boolean exact = false;
+
+	public Simplify(boolean exact)
+	{
+		this.exact = exact;
+	}
+
 	public Object visit(ExpressionBinaryOp e) throws PrismLangException
 	{
 		// Apply recursively
@@ -42,7 +49,7 @@ public class Simplify extends ASTTraverseModify
 		e.setOperand2((Expression) (e.getOperand2().accept(this)));
 		// If all operands are literals, replace with literal
 		if (e.getOperand1() instanceof ExpressionLiteral && e.getOperand2() instanceof ExpressionLiteral) {
-			return new ExpressionLiteral(e.getType(), e.evaluate());
+			return new ExpressionLiteral(e.getType(), exact ? e.evaluateExact() : e.evaluate());
 		}
 		// Other special cases
 		switch (e.getOperator()) {
@@ -87,6 +94,8 @@ public class Simplify extends ASTTraverseModify
 				return e.getOperand2();
 			break;
 		case ExpressionBinaryOp.PLUS:
+			if (exact)
+				break;
 			if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 0)
 				return e.getOperand1();
 			if (Expression.isInt(e.getOperand1()) && e.getOperand1().evaluateInt() == 0)
@@ -103,6 +112,8 @@ public class Simplify extends ASTTraverseModify
 			}
 			break;
 		case ExpressionBinaryOp.MINUS:
+			if (exact)
+				break;
 			if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 0)
 				return e.getOperand1();
 			if (Expression.isInt(e.getOperand1()) && e.getOperand1().evaluateInt() == 0) {
@@ -124,6 +135,8 @@ public class Simplify extends ASTTraverseModify
 			}
 			break;
 		case ExpressionBinaryOp.TIMES:
+			if (exact)
+				break;
 			if (Expression.isInt(e.getOperand2()) && e.getOperand2().evaluateInt() == 1)
 				return e.getOperand1();
 			if (Expression.isInt(e.getOperand1()) && e.getOperand1().evaluateInt() == 1)
@@ -165,7 +178,7 @@ public class Simplify extends ASTTraverseModify
 		e.setOperand((Expression) (e.getOperand().accept(this)));
 		// If operand is a literal, replace with literal
 		if (e.getOperand() instanceof ExpressionLiteral) {
-			return new ExpressionLiteral(e.getType(), e.evaluate());
+			return new ExpressionLiteral(e.getType(), exact ? e.evaluateExact() : e.evaluate());
 		}
 		// Even if not a literal, remove any parentheses
 		if (e.getOperator() == ExpressionUnaryOp.PARENTH) {
@@ -213,7 +226,7 @@ public class Simplify extends ASTTraverseModify
 			}
 		}
 		if (literal) {
-			return new ExpressionLiteral(e.getType(), e.evaluate());
+			return new ExpressionLiteral(e.getType(), exact ? e.evaluateExact() : e.evaluate());
 		}
 		return e;
 	}