diff --git a/src/main/scala/leon/invariant/structure/Constraint.scala b/src/main/scala/leon/invariant/structure/Constraint.scala
index 9644ff5c4685a229356f5d3a92feadbb46dd054a..b2226b13238d239d1860e09fe0609c8dafa17b91 100644
--- a/src/main/scala/leon/invariant/structure/Constraint.scala
+++ b/src/main/scala/leon/invariant/structure/Constraint.scala
@@ -251,15 +251,11 @@ case class Call(retexpr: Expr, fi: FunctionInvocation) extends Constraint {
}
object SetConstraint {
- def isSetOp(e: Expr) =
- e match {
- case SetUnion(_, _) | FiniteSet(_, _) | ElementOfSet(_, _) | SubsetOf(_, _) | Variable(_) =>
- true
- case _ => false
- }
-
def setConstraintOfBase(e: Expr) = e match {
- case Equals(Variable(_), rhs) if isSetOp(rhs) => true
+ case Equals(lhs@Variable(_), _) if lhs.getType.isInstanceOf[SetType] =>
+ true
+ case Equals(Variable(_), SetUnion(_, _) | FiniteSet(_, _) | ElementOfSet(_, _) | SubsetOf(_, _)) =>
+ true
case _ => false
}
@@ -273,22 +269,22 @@ object SetConstraint {
}
case class SetConstraint(expr: Expr) extends Constraint {
-// var union = false
-// var newset = false
-// var equal = false
-// var elemof = false
-// var subset = false
-// // TODO: add more operations here
-// expr match {
-// case Equals(Variable(_), rhs) =>
-// rhs match {
-// case SetUnion(_, _) => union = true
-// case FiniteSet(_, _) => newset = true
-// case ElementOfSet(_, _) => elemof = true
-// case SubsetOf(_, _) => subset = true
-// case Variable(_) => equal = true
-// }
-// }
+ var union = false
+ var newset = false
+ var equal = false
+ var elemof = false
+ var subset = false
+ // TODO: add more operations here
+ expr match {
+ case Equals(Variable(_), rhs) =>
+ rhs match {
+ case SetUnion(_, _) => union = true
+ case FiniteSet(_, _) => newset = true
+ case ElementOfSet(_, _) => elemof = true
+ case SubsetOf(_, _) => subset = true
+ case Variable(_) => equal = true
+ }
+ }
override def toString(): String = {
expr.toString
}
diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
index a69ecb45da412977f7342536387ffeef3cc87eb1..dfdace00bf024e9e6dda8894dbf428de00581de0 100644
--- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
+++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala
@@ -167,18 +167,30 @@ object LinearConstraintUtil {
}
}
+ import leon.purescala.Types._
//we assume that ine is in linear form
def PushTimes(mul: Expr, ine: Expr): Expr = {
+ val isReal = ine.getType == RealType && mul.getType == RealType
+ val timesCons =
+ if(isReal) RealTimes
+ else Times
ine match {
- case t: Terminal => Times(mul, t)
- case fi @ FunctionInvocation(fdef, args) => Times(mul, fi)
+ case t: Terminal => timesCons(mul, t)
+ case fi @ FunctionInvocation(fdef, ars) => timesCons(mul, fi)
case Plus(e1, e2) => Plus(PushTimes(mul, e1), PushTimes(mul, e2))
- case RealPlus(e1, e2) => Plus(PushTimes(mul, e1), PushTimes(mul, e2))
+ case RealPlus(e1, e2) =>
+ val r1 = PushTimes(mul, e1)
+ val r2 = PushTimes(mul, e2)
+ if (isReal) RealPlus(r1, r2)
+ else Plus(r1, r2)
case Times(e1, e2) => {
//here push the times into the coefficient which should be the first expression
Times(PushTimes(mul, e1), e2)
}
- case RealTimes(e1, e2) => Times(PushTimes(mul, e1), e2)
+ case RealTimes(e1, e2) =>
+ val r = PushTimes(mul, e1)
+ if(isReal) RealTimes(r, e2)
+ else Times(r, e2)
case _ => throw new NotImplementedException("PushTimes -- Operators not yet handled: " + ine)
}
}
@@ -206,7 +218,8 @@ object LinearConstraintUtil {
}
def mkLinearRecur(inExpr: Expr): Expr = {
- inExpr match {
+ //println("inExpr: "+inExpr + " tpe: "+inExpr.getType)
+ val res = inExpr match {
case e @ Operator(Seq(e1, e2), op)
if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
|| e.isInstanceOf[LessEquals] || e.isInstanceOf[GreaterThan]
@@ -259,12 +272,17 @@ object LinearConstraintUtil {
}
case Plus(e1, e2) => Plus(mkLinearRecur(e1), mkLinearRecur(e2))
case rp@RealPlus(e1, e2) =>
- println(s"Expr: $rp arg1: $e1 arg2: $e2")
- RealPlus(mkLinearRecur(e1), mkLinearRecur(e2))
+ //println(s"Expr: $rp arg1: $e1 tpe: ${e1.getType} arg2: $e2 tpe: ${e2.getType}")
+ val r1 = mkLinearRecur(e1)
+ val r2 = mkLinearRecur(e2)
+ //println(s"Res1: $r1 tpe: ${r1.getType} Res2: $r2 tpe: ${r2.getType}")
+ RealPlus(r1, r2)
case t: Terminal => t
case fi: FunctionInvocation => fi
case _ => throw new IllegalStateException("Expression not linear: " + inExpr)
}
+ //println("Res: "+res+" tpe: "+res.getType)
+ res
}
val rese = mkLinearRecur(atom)
rese
diff --git a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
index c2909ced299be6296f25e35046349fe055c2c3dc..6886b98bd77fabf7c13ce7cdcd88c1361245b49e 100644
--- a/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
+++ b/src/main/scala/leon/invariant/util/ExpressionTransformer.scala
@@ -339,10 +339,10 @@ object ExpressionTransformer {
*/
def TransformNot(expr: Expr, retainNEQ: Boolean = false): Expr = { // retainIff : Boolean = false
def nnf(inExpr: Expr): Expr = {
- if(inExpr.getType == Untyped){
- testHelp(inExpr)
- println(s"Warning: $inExpr is untyped")
- }
+// if(inExpr.getType == Untyped){
+// testHelp(inExpr)
+// println(s"Warning: $inExpr is untyped")
+// }
if (inExpr.getType != BooleanType) inExpr
else {
inExpr match {
@@ -373,9 +373,10 @@ object ExpressionTransformer {
} else {
//in this case e is a binary operation over ADTs
e match {
+ // TODO: is this a bug ?
case ninst @ Not(IsInstanceOf(e1, cd)) => Not(IsInstanceOf(nnf(e1), cd))
- case Not(SubsetOf(_, _)) | Not(ElementOfSet(_, _)) | Not(SetUnion(_, _)) | Not(FiniteSet(_, _)) =>
- e
+ case SubsetOf(_, _) | ElementOfSet(_, _) | SetUnion(_, _) | FiniteSet(_, _) =>
+ Not(e)
case e: Equals => Not(Equals(nnf(e1), nnf(e2)))
case _ => throw new IllegalStateException("Unknown operation on algebraic data types: " + e)
}
@@ -475,7 +476,7 @@ object ExpressionTransformer {
//println("NNFexpr: " + ScalaPrinter(nnfExpr) + "\n")
//flatten all function calls
val flatExpr = FlattenFunction(nnfExpr)
- println("Flatexpr: " + ScalaPrinter(flatExpr) + "\n")
+ //println("Flatexpr: " + ScalaPrinter(flatExpr) + "\n")
//perform additional simplification
val simpExpr = pullAndOrs(TransformNot(flatExpr))
simpExpr
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index e4191ff73d2f6c58435a7ab41b94e2e67e48ee08..5042413fc537df0eb20f27888efb934a68c8e0b8 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -495,11 +495,10 @@ object Expressions {
*/
case class And(exprs: Seq[Expr]) extends Expr {
require(exprs.size >= 2)
-// val getType = {
-// if (exprs forall (_.getType == BooleanType)) BooleanType
-// else Untyped
-// }
- val getType = BooleanType
+ val getType = {
+ if (exprs forall (_.getType == BooleanType)) BooleanType
+ else Untyped
+ }
}
object And {