Fixing some bugs in linear constraint util, and constraints

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
   }

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

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

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 {