From d00fb016e2a3d86a6ebc25af94f03286f296b048 Mon Sep 17 00:00:00 2001
From: Ravi <ravi.kandhadai@epfl.ch>
Date: Mon, 25 Jan 2016 01:40:35 +0100
Subject: [PATCH] Fixing some bugs in linear constraint util, and constraints
---
.../leon/invariant/structure/Constraint.scala | 44 +++++++++----------
.../structure/LinearConstraintUtil.scala | 32 +++++++++++---
.../util/ExpressionTransformer.scala | 15 ++++---
.../scala/leon/purescala/Expressions.scala | 9 ++--
4 files changed, 57 insertions(+), 43 deletions(-)
diff --git a/src/main/scala/leon/invariant/structure/Constraint.scala b/src/main/scala/leon/invariant/structure/Constraint.scala
index 9644ff5c4..b2226b132 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 a69ecb45d..dfdace00b 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 c2909ced2..6886b98bd 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 e4191ff73..5042413fc 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 {
--
GitLab