diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala
index 036d35771..213dcd278 100644
--- a/library/leon/math/package.scala
+++ b/library/leon/math/package.scala
@@ -2,6 +2,7 @@
package leon
import leon.annotation._
+import leon.collection._
package object math {
@@ -16,7 +17,308 @@ package object math {
@library
def max(i1: BigInt, i2: BigInt) = if (i1 >= i2) i1 else i2
+
+ @library
+ def abs(i: BigInt) = if(i < BigInt(0)) -i else i
+
+ @library
+ @annotation.isabelle.noBody()
+ // Computes the vectorial product of two lists.
+ def vectorialProduct(a: List[BigInt], b: List[BigInt]): BigInt = {
+ require(a.length == b.length)
+ a match {
+ case Nil() => 0
+ case Cons(ael, aq) => ael * b.head + vectorialProduct(aq, b.tail)
+ }
+ }
+
+ @library
+ @annotation.isabelle.noBody()
+ def isGCDable(l: List[BigInt]): Boolean = l match {
+ case Cons(x, b) if x == BigInt(0) => isGCDable(b)
+ case Cons(x, b) => true
+ case Nil() => false
+ }
+
+ /** Computes the GCD between numbers */
+ @library
+ @annotation.isabelle.noBody()
+ def gcdlist(l:List[BigInt]):BigInt = {
+ require(l.length > 0 && isGCDable(l))
+ l match {
+ case Cons(a, Nil()) => if(a < 0) -a else a
+ case Cons(z, q) if z == BigInt(0) => gcdlist(q)
+ case Cons(a, Cons(b, q)) => gcdlist(gcd(a,b)::q)
+ }
+ }
+
+ /** Computes the LCM between numbers */
+ @library
+ @annotation.isabelle.noBody()
+ def lcmlist(l:List[BigInt]):BigInt = {
+ require(l.length > 0 && isGCDable(l))
+ l match {
+ case Cons(a, Nil()) => if(a < 0) -a else a
+ case Cons(z, q) if z == BigInt(0) => lcmlist(q)
+ case Cons(a, Cons(b, q)) => lcmlist(lcm(a,b)::q)
+ }
+ }
+
+ /** Computes the GCD between two numbers */
+ @library
+ @annotation.isabelle.noBody()
+ def gcd(x:BigInt, y:BigInt): BigInt = {
+ require(x != 0 || y != 0)
+ if (x==BigInt(0)) abs(y)
+ else if (x<0) gcd(-x, y)
+ else if (y<0) gcd(x, -y)
+ else gcd(y%x, x)
+ } ensuring { (res: BigInt) =>
+ x % res == 0 && y % res == 0 && res > 0
+ }
+
+ /** Computes the LCM between two numbers */
+ @library
+ @annotation.isabelle.noBody()
+ def lcm(x: BigInt, y: BigInt): BigInt = {
+ require(x != 0 || y != 0)
+ abs(x * y) / gcd(x, y)
+ } ensuring { (res: BigInt) =>
+ res % x == 0 && res % y == 0 && res > 0
+ }
+
+ /** Computes the GCD between two numbers. Axponential speed-up.*/
+ /*@library
+ def binaryGcd(a:BigInt, b:BigInt):BigInt = {
+ var g = BigInt(1)
+ var (u, v) = (a, b)
+ while(u%2 == 0 && v%2 == 0) {
+ u = u/2
+ v = v/2
+ g = 2*g
+ }
+ while(u != 0) {
+ if(u % 2 == 0) u = u/2
+ else if(v % 2 == 0) v = v/2
+ else {
+ val t = abs(u-v)/2
+ if(u >= v) u = t else v = t
+ }
+ }
+ g*v
+ }*/
+
+ /*@library
+ def bezout(e: BigInt, a : List[BigInt]):List[BigInt] = {
+ require(a.length > 0 && isGCDable(a))
+ bezoutMM(a, e / gcdlist(a))
+ }*/
+
+ @library
+ @annotation.isabelle.noBody()
+ def bezoutWithBase(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = {
+ require(isNonZero(a) && a.nonEmpty)
+ bezoutWithBaseMMFunc(e, a)
+ }
+
+ /** Finds (x1, x2, k) such that x1.a + x2.b + gcd(a,b) = 0 and k = gcd(a ,b) */
+ /*@library
+ def extendedEuclid(a_in: BigInt, b_in: BigInt):(BigInt, BigInt, BigInt) = {
+ var (x, lastx) = (BigInt(0), BigInt(1))
+ var (y, lasty) = (BigInt(1), BigInt(0))
+ var (a, b) = (a_in, b_in)
+ var (quotient, temp) = (BigInt(0), BigInt(0))
+ while(b != 0) {
+ val amodb = (abs(b) + a%b)%b
+ quotient = (a - amodb)/b
+ a = b
+ b = amodb
+ temp = x
+ x = lastx-quotient*x
+ lastx = temp
+ temp = y
+ y = lasty-quotient*y
+ lasty = temp
+ }
+ if(a < 0)
+ (lastx, lasty, -a)
+ else
+ (-lastx, -lasty, a)
+ }*/
+
+ // Finds coefficients x such that k*gcd(a_in) + x.a_in = 0
+ /*@library
+ def bezoutMM(a_in: List[BigInt], k: BigInt):List[BigInt] = {
+ var a = a_in
+ var a_in_gcds = a_in.foldRight(List[BigInt]()){
+ case (i, Nil()) => List(i)
+ case (i, a::q) => gcd(a, i)::a::q
+ }
+ var result:List[BigInt] = Nil()
+ var last_coef = BigInt(-1)
+ while(a.nonEmpty) {
+ a match {
+ case Cons(x, Nil()) if x == BigInt(0) =>
+ result = Cons(BigInt(0), result)
+ a = Nil()
+ case Cons(el, Nil()) =>
+ // Solution is -el/abs(el)
+ result = (k*(-last_coef * (-el/abs(el))))::result
+ a = Nil()
+ case Cons(el1, Cons(el2, Nil())) =>
+ val (u, v, _) = extendedEuclid(el1, el2)
+ result = (-v*k*last_coef)::(-u*k*last_coef)::result
+ a = Nil()
+ case (el1::q) =>
+ val el2 = a_in_gcds.tail.head
+ val (u, v, _) = extendedEuclid(el1, el2)
+ result = (-u*k*last_coef)::result
+ last_coef = -v*last_coef
+ a = q
+ a_in_gcds = a_in_gcds.tail
+ }
+ }
+ result.reverse
+ }*/
+
+ // Finds coefficients x such that gcd(a_in) + x.a_in = 0
+ /*@library
+ def bezoutMM(a_in: List[BigInt]):List[BigInt] = bezoutMM(a_in, BigInt(1))*/
+ /*@library
+ def bezoutWithBaseMM(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = {
+ var coefs = a
+ var coefs_gcd = coefs.foldRight(List[BigInt]()){
+ case (i, Nil()) => List(abs(i))
+ case (i, Cons(a, q)) => gcd(a, i)::a::q
+ }
+ var n = a.length
+ var result = List(bezoutMM(a, e/coefs_gcd.head)) // The gcd of all coefs divides e.
+ var i = BigInt(1)
+ var zeros:List[BigInt] = Nil()
+ while(i <= n-BigInt(1)) {
+ val kii = coefs_gcd.tail.head / coefs_gcd.head
+ val kijs = bezoutMM(coefs.tail, coefs.head/coefs_gcd.head)
+ result = Cons((zeros ++ Cons(kii, kijs)), result)
+ coefs = coefs.tail
+ coefs_gcd = coefs_gcd.tail
+ zeros = Cons(BigInt(0), zeros)
+ i += 1
+ }
+ result.reverse
+ }*/
+
+ @library
+ @annotation.isabelle.noBody()
+ def extendedEuclidFunc(a_in: BigInt, b_in: BigInt):(BigInt, BigInt, BigInt) = {
+ require(a_in != 0 || b_in != 0)
+ val (x, lastx) = (BigInt(0), BigInt(1))
+ val (y, lasty) = (BigInt(1), BigInt(0))
+ val (a, b) = (a_in, b_in)
+ def aux(a: BigInt, b: BigInt, x: BigInt, y: BigInt, lastx: BigInt, lasty: BigInt): (BigInt, BigInt, BigInt) = {
+ if (b == 0) {
+ if(a < 0)
+ (lastx, lasty, -a)
+ else
+ (-lastx, -lasty, a)
+ } else {
+ val amodb = (abs(b) + a%b)%b
+ val quotient = (a - amodb)/b
+ aux(b, amodb, lastx-quotient*x, lasty-quotient*y, x, y)
+ }
+ }
+ aux(a, b, x, y, lastx, lasty)
+ }/* ensuring { res =>
+ val (x1, x2, k) = res
+ x1 * a_in + x2 * b_in + k == 0 && k == gcd(a_in, b_in)
+ }*/
+
+ @library
+ @annotation.isabelle.noBody()
+ def isPositive(l: List[BigInt]): Boolean = l match {
+ case Cons(a, b) => a > 0 && isPositive(b)
+ case Nil() => true
+ }
+ @library
+ @annotation.isabelle.noBody()
+ def isNonZero(l: List[BigInt]): Boolean = l match {
+ case Cons(a, b) => a != 0 && isNonZero(b)
+ case Nil() => true
+ }
@library
- def abs(n: BigInt) = if(n < 0) -n else n
+ @annotation.isabelle.noBody()
+ def foldRightGcds(es: List[BigInt]): List[BigInt] = {
+ require(isNonZero(es))
+ ((es match {
+ case Cons(i, aq) => foldRightGcds(aq) match {
+ case Cons(a, q) => gcd(a, i)::a::q
+ case Nil() => List(abs(i))
+ }
+ case Nil() => Nil()
+ }): List[BigInt])} ensuring {
+ (res: List[BigInt]) =>
+ isPositive(res) && res.length == es.length
+ }
+
+ @library
+ @annotation.isabelle.noBody()
+ def bezoutMMFunc(a_in: List[BigInt], k: BigInt):List[BigInt] = {
+ require(isNonZero(a_in) && a_in.length > 0)
+ val a = a_in
+
+ val a_in_gcds = foldRightGcds(a_in)
+ val result:List[BigInt] = Nil()
+ val last_coef = BigInt(-1)
+ def aux(a: List[BigInt], a_in_gcds: List[BigInt], result: List[BigInt], last_coef: BigInt): List[BigInt] = {
+ require(isNonZero(a) && a_in_gcds == foldRightGcds(a))
+ if(a.isEmpty) result.reverse
+ else {
+ a match {
+ /*case Cons(x, Nil()) if x == BigInt(0) =>
+ aux(Nil(), a_in_gcds, Cons(BigInt(0), result), last_coef)*/
+ case Cons(el, Nil()) =>
+ // Solution is -el/abs(el)
+ aux(Nil(), a_in_gcds, (k*(-last_coef * (-el/abs(el))))::result, last_coef)
+ case Cons(el1, Cons(el2, Nil())) =>
+ val (u, v, _) = extendedEuclidFunc(el1, el2)
+ aux(Nil(), a_in_gcds, (-v*k*last_coef)::(-u*k*last_coef)::result, last_coef)
+ case (el1::q) =>
+ val el2 = a_in_gcds.tail.head
+ val (u, v, _) = extendedEuclidFunc(el1, el2)
+ aux(q, a_in_gcds.tail, (-u*k*last_coef)::result, -v*last_coef)
+ }
+ }
+ } ensuring {
+ (res: List[BigInt]) => true
+ }
+ aux(a_in, a_in_gcds, result, last_coef)
+ }/* ensuring {
+ (x: List[BigInt]) =>
+ vectorialProduct(x, a_in) + k*gcdlist(a_in) == 0
+ }*/
+
+ @library
+ @annotation.isabelle.noBody()
+ def bezoutWithBaseMMFunc(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = {
+ require(isNonZero(a) && a.nonEmpty)
+ val coefs = a
+ val coefs_gcd = foldRightGcds(coefs)
+ val n = a.length
+ val result = List(bezoutMMFunc(a, e/coefs_gcd.head)) // The gcd of all coefs divides e.
+ val i = BigInt(1)
+ val zeros:List[BigInt] = Nil()
+ def aux(i: BigInt, result: List[List[BigInt]], coefs: List[BigInt], coefs_gcd: List[BigInt], zeros: List[BigInt])
+ : List[List[BigInt]] = {
+ require(i <= n && coefs.length + i == a.length + BigInt(1) && isNonZero(coefs) && isPositive(coefs_gcd) && coefs_gcd == foldRightGcds(coefs) && (i == n || (coefs_gcd.length >= 2 && coefs.length >= 1)))
+ if (i > n-BigInt(1)) {
+ result.reverse
+ } else {
+ val kii = coefs_gcd.tail.head / coefs_gcd.head
+ val kijs = bezoutMMFunc(coefs.tail, coefs.head/coefs_gcd.head)
+ aux(i + 1, Cons((zeros ++ Cons(kii, kijs)), result), coefs.tail, coefs_gcd.tail, Cons(BigInt(0), zeros))
+ }
+ }
+ aux(i, result, coefs, coefs_gcd, zeros)
+ }
}
+
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 7b34157d3..d914d7861 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -117,7 +117,7 @@ object Constructors {
*/
def functionInvocation(fd : FunDef, args : Seq[Expr]) = {
- require(fd.params.length == args.length, "Invoking function with incorrect number of arguments")
+ require(fd.params.length == args.length, s"Invoking function ${fd.id.name} with incorrect number of arguments. Expected ${fd.params.length}, got $args.")
val formalType = tupleTypeWrap(fd.params map { _.getType })
val actualType = tupleTypeWrap(args map { _.getType })
@@ -125,7 +125,7 @@ object Constructors {
canBeSupertypeOf(formalType, actualType) match {
case Some(tmap) =>
FunctionInvocation(fd.typed(fd.tparams map { tpd => tmap.getOrElse(tpd.tp, tpd.tp) }), args)
- case None => throw LeonFatalError(s"$args:$actualType cannot be a subtype of $formalType!")
+ case None => throw LeonFatalError(s"$args:$actualType cannot be a subtype of $formalType!. Indeed " + ExprOps.explainTyping(tupleWrap(args)))
}
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 36b0887dc..7a02a36d5 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -308,6 +308,7 @@ object Extractors {
object TopLevelAnds { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Let(i, e, TopLevelAnds(bs)) => Some(bs map (let(i,e,_)))
+ case LetTuple(is, e, TopLevelAnds(bs)) => Some(bs map (letTuple(is, e, _)))
case And(exprs) =>
Some(exprs.flatMap(unapply).flatten)
case e =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b60a3d006..195564fe7 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -256,8 +256,11 @@ class PrettyPrinter(opts: PrinterOptions,
optP { p"$a $op $b" }
case FcallMethodInvocation(rec, fd, id, tps, args) if (fd.annotations.contains("library") || !(opts.printRunnableCode)) =>
-
- p"$rec.$id${nary(tps, ", ", "[", "]")}"
+ p"$rec"
+ if(id.name != "apply") {
+ p".$id"
+ }
+ p"${nary(tps, ", ", "[", "]")}"
if (fd.isRealFunction) {
// The non-present arguments are synthetic function invocations
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 2f463a038..03f9feaf1 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -48,6 +48,7 @@ object Rules {
//HOFDecomp,
//ExampleGuidedTermExploration,
//BottomUpETE,
+ IntegerEquality,
IfSplit,
InputSplit,
UnusedInput,
diff --git a/src/main/scala/leon/synthesis/comfusy/APAAbstractions.scala b/src/main/scala/leon/synthesis/comfusy/APAAbstractions.scala
new file mode 100644
index 000000000..9d755b50f
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APAAbstractions.scala
@@ -0,0 +1,372 @@
+package leon.synthesis.comfusy
+
+/*****************************
+ * Expression abstractions *
+ *****************************/
+
+// dummy
+object APAAbstractions
+
+/** This object provides methods for creating sign abstractions
+ * from integer arithmetic expressions of sign abstractions.
+ * Sign abstraction are typically applied to input terms.
+ *
+ * @author Mikaël Mayer
+ */
+object SignAbstraction {
+
+ /** Creates a sign abstraction from the sum of two sign abstractions.
+ */
+ def addSign(a: SignAbstraction, b: SignAbstraction):ASign = {
+ ASign((a.can_be_positive || b.can_be_positive), (a.can_be_zero && b.can_be_zero) || (a.can_be_positive && b.can_be_negative) || (b.can_be_positive && a.can_be_negative), (a.can_be_negative || b.can_be_negative))
+ }
+
+ /** Creates a sign abstraction from the sum of any number of sign abstractions.
+ */
+ def addSign(l: List[SignAbstraction]):ASign = {
+ l.foldLeft(ASign(false, true, false))(addSign(_, _))
+ }
+
+ /** Creates a sign abstraction from the product of two sign abstractions.
+ */
+ def multSign(a: SignAbstraction, b: SignAbstraction):ASign = {
+ val result = ASign((a.can_be_positive && b.can_be_positive) || (a.can_be_negative && b.can_be_negative), (a.can_be_zero || b.can_be_zero), (a.can_be_positive && b.can_be_negative) || (a.can_be_negative && b.can_be_positive))
+ result
+ }
+
+ /** Creates a sign abstraction from the product of any number of sign abstractions.
+ */
+ def multSign(l: List[SignAbstraction]):ASign = {
+ l.foldLeft(ASign(true, false, false))(multSign(_, _))
+ }
+
+ /** Creates a sign abstraction from the division of sign abstractions.
+ * Raises an error if the divisor can be zero.
+ */
+ def divSign(a: SignAbstraction, b: SignAbstraction):ASign = {
+ if(b.can_be_zero)
+ throw new Exception("Error : "+b+" can be zero")
+ ASign((a.can_be_positive && b.can_be_positive) || (a.can_be_negative && b.can_be_negative), (a.can_be_positive || a.can_be_negative || a.can_be_zero) && (b.can_be_positive || b.can_be_negative || b.can_be_zero), (a.can_be_positive && b.can_be_negative) || (a.can_be_negative && b.can_be_positive))
+ }
+
+ /** Creates a sign abstraction from the opposite of a sign abstraction.
+ */
+ def oppSign(a: SignAbstraction):ASign = {
+ ASign(a.can_be_negative, a.can_be_zero, a.can_be_positive)
+ }
+
+ /** Creates a sign abstraction from the absolute value of a sign abstraction.
+ */
+ def absSign(a: SignAbstraction):ASign = {
+ ASign(a.can_be_negative || a.can_be_positive, a.can_be_zero, false)
+ }
+
+ /** Creates a sign abstraction from a number.
+ */
+ def number(i: Int):ASign = {
+ ASign(i > 0, i == 0, i < 0)
+ }
+
+ /** Creates a sign abstraction from a linear combination of sign abstractions.
+ * i + l1*s1 + l2*s2 + l3*s3 ... + ln * sn
+ *
+ * @param i The constant coefficient of the linear combination
+ * @param l The list of pairs (l_i, s_i) where l_i is an integer and s_i a
+ * sign abstraction.
+ */
+ def linearCombinationSign(i: Int, l: List[(Int, SignAbstraction)]):ASign = {
+ val l_sign = l map { case (i, sa) => multSign(number(i), sa)}
+ addSign(number(i)::l_sign)
+ }
+ def mergeSign(a: SignAbstraction, b: SignAbstraction):ASign = {
+ ASign(a.can_be_positive && b.can_be_positive, a.can_be_zero && b.can_be_zero, a.can_be_negative && b.can_be_negative)
+ }
+}
+
+/** Class SignAbstraction represents a sign abstraction (>0, =0 and <0).
+ * Any class that extends it should implement the method normalClone()
+ * returning a clone from itself.
+ * The following methods are available:
+ * - Methods assume* (assumeZero, assumePositive...) to clone the expression with a more specialized abstraction
+ * - Methods is* (isPositive, isNegativeZero) which check the sign abstraction capacities.
+ * - The method ropagateSign can be overriden to propagate sign properties to sub-expressions.
+ *
+ * @author Mikaël Mayer
+ */
+trait SignAbstraction {
+
+ //@{ Private section
+ /** Private variables containing the abstraction. */
+ private var private_pos: Boolean = true
+ private var private_nul: Boolean = true
+ private var private_neg: Boolean = true
+
+ /** Clones the expression with a new abstraction. */
+ private def cloneWithSign(a: SignAbstraction):this.type = {
+ this.cloneWithSign(a.can_be_positive, a.can_be_zero, a.can_be_negative)
+ }
+
+ /** Clones the expression with a new abstraction where the signs are given. */
+ private def cloneWithSign(pos_ : Boolean, nul_ : Boolean, neg_ : Boolean):this.type = {
+ val result = normalClone().asInstanceOf[SignAbstraction]
+ result.setSign(pos_, nul_, neg_)
+ result.asInstanceOf[this.type]
+ }
+ //@}
+
+ //@{ Protected section
+ /** A direct method to set up the sign.
+ * Used by subclasses methods only.*/
+ protected def setSign(pos_ :Boolean, nul_ :Boolean, neg_ :Boolean):Unit = {
+ private_pos = pos_
+ private_nul = nul_
+ private_neg = neg_
+ }
+ /** A direct method to set up the sign according to an integer.
+ * Used by subclasses methods only. */
+ protected def setSign(i: Int):Unit = {
+ setSign(i > 0, i == 0, i < 0)
+ }
+
+ /** A direct method to set up the sign according to an existing abstraction.
+ * Used by subclasses methods only. */
+ protected def setSign(i: SignAbstraction):Unit = {
+ setSign(i.can_be_positive, i.can_be_zero, i.can_be_negative)
+ }
+
+ /** Returns a clone of the expression updated with a better or new knowledge about the sign. */
+ protected def propagateSign_internal(i: SignAbstraction):this.type = {
+ cloneWithSign(can_be_positive && i.can_be_positive, can_be_zero && i.can_be_zero, can_be_negative && i.can_be_negative)
+ }
+ //@}
+
+ //@{ Sign check methods
+ /** Returns true if the expression can be positive. */
+ def can_be_positive:Boolean = private_pos
+
+ /** Returns true if the expression can be zero. */
+ def can_be_zero:Boolean = private_nul
+
+ /** Returns true if the expression can be negative. */
+ def can_be_negative:Boolean = private_neg
+
+ /** Returns true if the expression is defined and positive. */
+ def isPositive() = can_be_positive && !can_be_negative && !can_be_zero
+
+ /** Returns true if the expression is defined and negative. */
+ def isNegative() = !can_be_positive && can_be_negative && !can_be_zero
+
+ /** Returns true if the expression is defined and (positive or zero). */
+ def isPositiveZero() = (can_be_positive || can_be_zero) && !can_be_negative
+
+ /** Returns true if the expression cannot be positive nor zero. */
+ def isNotPositiveZero() = !can_be_positive && !can_be_zero
+
+ /** Returns true if the expression is defined and (negative or zero). */
+ def isNegativeZero() = (can_be_negative || can_be_zero) && !can_be_positive
+
+ /** Returns true if the expression cannot be negative nor zero. */
+ def isNotNegativeZero() = !can_be_negative && !can_be_zero
+
+ /** Returns true if the expression cannot be positive. */
+ def isNotPositive() = !can_be_positive
+
+ /** Returns true if the expression cannot be negative. */
+ def isNotNegative() = !can_be_negative
+
+ /** Returns true if the expression is defined an is zero. */
+ def isZero() = can_be_zero && !can_be_positive && !can_be_negative
+
+ /** Returns true if the expression cannot be zero. */
+ def isNotZero() = !can_be_zero
+
+ /** Returns true if the expression is not defined. */
+ def isNotDefined() = !can_be_positive && !can_be_negative && !can_be_zero
+ //@}
+
+ //@{ Assuming sign methods
+ /** Assumes the sign of a integer. */
+ def assumeSign(i: Int):this.type = {
+ propagateSign(ASign(i > 0, i == 0, i < 0))
+ }
+
+ /** Assumes a sign == 0. */
+ def assumeZero():this.type = {
+ assumeSign(0)
+ }
+
+ /** Assumes a sign > 0 */
+ def assumePositive():this.type = {
+ assumeSign(1)
+ }
+
+ /** Assumes a sign < 0 */
+ def assumeNegative():this.type = {
+ assumeSign(-1)
+ }
+
+ /** Assumes a sign >= 0 */
+ def assumePositiveZero():this.type = {
+ propagateSign(ASign(true, true, false))
+ }
+
+ /** Assumes a sign <= 0 */
+ def assumeNegativeZero():this.type = {
+ propagateSign(ASign(false, true, true))
+ }
+
+ /** Assumes a sign != 0 */
+ def assumeNotZero():this.type = {
+ propagateSign(ASign(true, false, true))
+ }
+
+ /** Assumes a sign from a sign abstraction */
+ def assumeSign(i: SignAbstraction):this.type = {
+ propagateSign(ASign(i.can_be_positive, i.can_be_zero, i.can_be_negative))
+ }
+
+ /** Assumes a potential zero sign from a sign abstraction
+ * This is used products : a has the same zero-sign as a*b. */
+ def assumeNotzerobility(i: SignAbstraction):this.type = {
+ propagateSign(ASign(true, i.can_be_zero, true))
+ }
+ //@}
+
+ //@{ Methods to specialize
+ /** A cloning method to implement in order to use this class. */
+ def normalClone():this.type
+
+ /** A method which processes the sign propagation of an expression.
+ * Can be overriden to propagate the sign within sub-elements of the expression. */
+ def propagateSign(i: SignAbstraction):this.type = {
+ propagateSign_internal(i)
+ }
+ //@}
+}
+
+
+/** The simplest class to implement a sign abstraction. */
+case class ASign(pos_ : Boolean, nul_ : Boolean, neg_ : Boolean) extends SignAbstraction {
+ setSign(pos_, nul_, neg_)
+ def normalClone():this.type = ASign(pos_, nul_, neg_).asInstanceOf[this.type]
+}
+
+/** The simplest class to implement a positive or zero sign abstraction. */
+case class PositiveZeroSign() extends SignAbstraction {
+ setSign(true, true, false)
+ def normalClone():this.type = PositiveZeroSign().asInstanceOf[this.type]
+}
+
+/** Class CoefficientAbstraction represents an all-zero coefficients abstraction.
+ * The coefficients of a linear combination c_0 + c_1*y_1 + ... c_n*y_n are (c_1, ..., c_n)
+ * where the c_i are input terms and the y_i are output variables.
+ * Any class that extends CoefficientAbstraction should implement the method normalClone()
+ * returning a clone from itself.
+ * The following methods are available:
+ * - Methods assume* (assumeAllCoefficientsAreZero, ...) to clone the expression with a more specialized abstraction
+ * - Checks Methods (allCoefficientsAreZero ...) which check the coefficient abstraction capacities.
+ *
+ * @author Mikaël Mayer
+ */
+trait CoefficientAbstraction {
+
+ //@{ Private section
+ /** Private variables containing the abstraction. */
+ private var p_allCoefficientsCanBeZero: Boolean = true
+ private var p_oneCoefficientsCanBeNonZero: Boolean = true
+
+ private def cloneWithCoefficientAbstraction(c: CoefficientAbstraction):this.type = {
+ this.cloneWithCoefficientAbstraction(c.p_allCoefficientsCanBeZero, c.p_oneCoefficientsCanBeNonZero)
+ }
+ private def cloneWithCoefficientAbstraction(allCoefficientsCanBeZero_ : Boolean, oneCoefficientsCanBeNonZero_ : Boolean):this.type = {
+ val result = normalClone().asInstanceOf[CoefficientAbstraction]
+ result.setCoefficients(allCoefficientsCanBeZero_, oneCoefficientsCanBeNonZero_)
+ result.asInstanceOf[this.type]
+ }
+ //@}
+
+ //@{ Protected section
+ /** A direct method to set up coefficient abstraction.
+ * Used by subclasses methods only. */
+ protected def setNotAllCoefficientsAreZero() = {
+ setCoefficients(false, true)
+ }
+
+ /** A direct method to set up coefficient abstraction.
+ * Used by subclasses methods only. */
+ protected def setNoCoefficients() = {
+ setCoefficients(true, true)
+ }
+
+ /** A direct method to set up coefficient abstraction.
+ * Used by subclasses methods only. */
+ protected def setCoefficients(a: Boolean, n: Boolean) = {
+ p_allCoefficientsCanBeZero = a
+ p_oneCoefficientsCanBeNonZero = n
+ }
+
+ /** A method to clone the expression with the knowledge of another coefficient abstraction. */
+ protected def propagateCoefficientAbstraction(o : CoefficientAbstraction):this.type = {
+ cloneWithCoefficientAbstraction(allCoefficientsCanBeZero && o.allCoefficientsCanBeZero,
+ oneCoefficientsCanBeNonZero && o.oneCoefficientsCanBeNonZero)
+ }
+ //@}
+
+ //@{ Coefficient check methods
+ /** Returns true if all the coefficients are zero. */
+ def allCoefficientsAreZero = p_allCoefficientsCanBeZero && !p_oneCoefficientsCanBeNonZero
+
+ /** Returns true if not all the coefficients are zero. */
+ def notAllCoefficientsAreZero = p_oneCoefficientsCanBeNonZero && !p_allCoefficientsCanBeZero
+
+ /** Returns true if all the coefficients are zero. */
+ def allCoefficientsCanBeZero = p_allCoefficientsCanBeZero
+
+ /** Returns true if not all the coefficients are zero. */
+ def oneCoefficientsCanBeNonZero = p_oneCoefficientsCanBeNonZero
+ //@}
+
+ //@{ Assuming coefficients methods
+ /** Assumes that all coefficients are zero. */
+ def assumeAllCoefficientsAreZero : this.type = {
+ propagateCoefficientAbstraction(ACoef(true, false))
+ }
+
+ /** Assumes that not all coefficients are zero. */
+ def assumeNotAllCoefficientsAreZero : this.type = {
+ cloneWithCoefficientAbstraction(ACoef(false, true))
+ }
+
+ /** Assumes a coefficient abstraction of a sum. */
+ def assumeSumCoefficientAbstraction(a: CoefficientAbstraction, o: CoefficientAbstraction):this.type = {
+ if(a.allCoefficientsAreZero && o.allCoefficientsAreZero) {
+ assumeAllCoefficientsAreZero
+ } else if(a.allCoefficientsAreZero) {
+ propagateCoefficientAbstraction(o)
+ } else if(o.allCoefficientsAreZero) {
+ propagateCoefficientAbstraction(a)
+ } else this
+ }
+
+ /** Assumes a coefficient abstraction of a multiplication by an integer. */
+ def assumeMultCoefficientAbstraction(o: CoefficientAbstraction, i: Int):this.type = {
+ if(i==0) {
+ assumeAllCoefficientsAreZero
+ } else {
+ propagateCoefficientAbstraction(o)
+ }
+ }
+ //@}
+
+
+ //@{ Methods to specialize
+ /** A cloning method to implement in order to use this class. */
+ def normalClone():this.type
+ //@}
+}
+
+/** The simplest class to implement a coefficient abstraction. */
+case class ACoef(a: Boolean, n: Boolean) extends CoefficientAbstraction {
+ setCoefficients(a, n)
+ def normalClone():this.type = ACoef(a, n).asInstanceOf[this.type]
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/synthesis/comfusy/APACondition.scala b/src/main/scala/leon/synthesis/comfusy/APACondition.scala
new file mode 100644
index 000000000..1bc4995f5
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APACondition.scala
@@ -0,0 +1,287 @@
+package leon.synthesis.comfusy
+
+/** An abstract precondition or specification representation.
+ * Such preconditions are commonly associated to a program which correctly executes if the condition is true.
+ *
+ * @author Mikaël Mayer
+ */
+sealed abstract class APAAbstractCondition {
+
+ /** Returns a string representing the condition in current rendering mode.
+ * See APASynthesis.rendering_mode to change it. */
+ def toCommonString : String
+
+ /** Returns the boolean value of this condition under a certain variable mapping. */
+ def execute(l: Map[InputVar, Int]): Boolean
+
+ /** Returns the list of input variables contained in this conditions. */
+ def input_variables: List[InputVar]
+}
+
+
+/** This object provides optimization and default values for conditions.
+ *
+ * @author Mikaël Mayer
+ */
+object APACondition {
+
+ /** Returns a typical false precondition. */
+ def False: APACondition = APACondition(Nil, APAFalse(), APAEmptySplitCondition())
+
+ /** Creates a new APACondition after optimizing the arguments
+ *
+ * @param input_assignment The list of input assignments to change if necessary.
+ * @param global_condition A simple formula part of the condition.
+ * @param pf An advanced formula part of the condition (bounded quantifiers, disjunction of other conditions...)
+ * @return An optimized APACondition.
+ */
+ def optimized(input_assignment: List[InputAssignment], global_condition: APAFormula, pf : APASplitCondition):APACondition = {
+ val final_input_variables = (global_condition.input_variables ++ pf.input_variables).distinct
+ val (useful_input_assignments, _) = input_assignment.foldRight((Nil:List[InputAssignment], final_input_variables:List[InputVar])) {
+ case (assignment@SingleInputAssignment(x, t), (useful_input_assignments, useful_input_variables)) =>
+ if(useful_input_variables contains x) { // Then it's useful
+ (assignment::useful_input_assignments, t.input_variables ++ useful_input_variables)
+ } else { // Then this variable is useless
+ (useful_input_assignments, useful_input_variables)
+ }
+ case (assignment@BezoutInputAssignment(xl, tl), (useful_input_assignments, useful_input_variables)) =>
+ if((xl.flatten : List[InputVar]) exists (useful_input_variables contains _)) { // Then it's useful
+ (assignment::useful_input_assignments, (tl flatMap (_.input_variables)) ++ useful_input_variables)
+ } else { // Then this variable is useless
+ (useful_input_assignments, useful_input_variables)
+ }
+ }
+ if(global_condition == APAFalse()) return APACondition.False
+ val result = if(pf.input_variables == Nil) {
+ pf.execute(Map()) match {
+ case false => APACondition.False
+ case true => APACondition(useful_input_assignments, global_condition.simplified, APAEmptySplitCondition())
+ }
+ } else {
+ global_condition.simplified match {
+ case t@APAFalse() => APACondition(useful_input_assignments, t, APAEmptySplitCondition())
+ case t => APACondition(useful_input_assignments, t, pf)
+ }
+ }
+ result
+ }
+}
+
+/** Class representing a program precondition.
+ *
+ * @param input_assignment The list of input assignments to change if necessary.
+ * @param global_condition A simple formula part of the condition.
+ * @param pf An advanced formula part of the condition (bounded quantifiers, disjunction of other conditions...)
+ * @author Mikaël Mayer
+ */
+case class APACondition(input_assignment: List[InputAssignment], global_condition: APAFormula, pf : APASplitCondition) extends APAAbstractCondition {
+
+ /** Adds an assumption after the existing assumptions and before the advanced formula. */
+ def &&(more_cond: APAFormula):APACondition = APACondition(input_assignment, global_condition && more_cond, pf)
+
+ /** Adds an assumption before the existing assumptions.
+ * Used e.g. in the case a condition a % b == 0 if b != 0 is checked before.
+ */
+ def assumeBefore(more_cond: APAFormula):APACondition = APACondition(input_assignment, more_cond && global_condition, pf)
+
+ /** Returns if the condition is trivially true. */
+ def isTrivial(): Boolean = global_condition == APATrue() && pf == APAEmptySplitCondition()
+
+ /** Returns the list of the input variables appearing anywhere in the precondition */
+ def input_variables = ((global_condition.input_variables ++ pf.input_variables) filterNot ((input_assignment flatMap (_.input_variables))).contains).distinct
+
+ /** Returns a parsable string representing the body of the condition, without variable assignment,
+ * under the current rendering mode. */
+ protected def conditionBodyToCommonString(rm: RenderingMode) = (global_condition, pf) match {
+ case (_, APAEmptySplitCondition()) => global_condition.toString
+ case (APATrue(), _) => pf.toString
+ case _ => "("+global_condition.toString+") "+rm.and_symbol+" ("+pf.toString+")"
+ }
+
+ /** Returns a parsable string representing the complete condition */
+ def conditionToCommonString = APASynthesis.rendering_mode match {
+ case RenderingScala => conditionToScalaString
+ case RenderingPython => conditionToPythonString
+ }
+
+ /** Returns a parsable scala string representing the complete condition */
+ def conditionToScalaString = input_assignment match {
+ case Nil => conditionBodyToCommonString(APASynthesis.rendering_mode)
+ case _ => "{"+(input_assignment map (_.toCommonString("")) reduceLeft (_+";"+_)) + ";"+conditionBodyToCommonString(APASynthesis.rendering_mode)+"}"
+ }
+
+ /** Returns a parsable python string representing the complete condition */
+ def conditionToPythonString = {
+ def conditionToPythonString_aux(input_assignment: List[InputAssignment]):String = input_assignment match {
+ case Nil => conditionBodyToCommonString(APASynthesis.rendering_mode)
+ case (assignment::q) =>
+ "(lambda "+assignment.varToPythonString+": "+conditionToPythonString_aux(q)+")("+assignment.valToPythonString+")"
+ }
+ conditionToPythonString_aux(input_assignment)
+ }
+
+ /** toString alias */
+ def toCommonString = conditionToCommonString
+
+ /** toString alias */
+ override def toString = toCommonString
+
+ def execute(l: Map[InputVar, Int]): Boolean = {
+ var input_value_map = l
+ input_assignment foreach {
+ case SingleInputAssignment(v, t) => val input_value_assignment = APAAbstractProgram.toAPAInputAssignment(input_value_map)
+ t.replaceList(input_value_assignment) match {
+ case APAInputCombination(i, Nil) => input_value_map += (v -> i)
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+input_value_map)
+ }
+ case BezoutInputAssignment(vl, tl) => val input_value_assignment = APAAbstractProgram.toAPAInputAssignment(input_value_map)
+ val bezout_coefs:List[Int] = tl map (_.replaceList(input_value_assignment)) map {
+ case APAInputCombination(i, Nil) => i
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+input_value_map)
+ }
+ // Double zip and add all assignments to variables
+ (vl zip Common.bezoutWithBase(1, bezout_coefs)) map { case (l1, l2) => l1 zip l2 } foreach { _ foreach { input_value_map += _ } }
+ }
+ global_condition.replaceListInput(APAAbstractProgram.toAPAInputAssignment(input_value_map)) match {
+ case APATrue() => pf.execute(input_value_map)
+ case APAFalse() => false
+ case t =>
+ throw new Exception ("Could not find the truth value of "+this+"\n under the mapping "+input_value_map+".\n Got the result: "+t)
+ }
+ }
+}
+
+/** Advanced conditions.
+ * @author Mikaël Mayer
+ */
+sealed abstract class APASplitCondition extends APAAbstractCondition {
+
+ /** Returns a string representing the condition. */
+ override def toString = toStringGeneral(APASynthesis.rendering_mode)
+
+ /** Method to override. Return astring representing the solution under the given RenderingMode */
+ protected def toStringGeneral(rm: RenderingMode):String
+
+ /** Alias for toString */
+ def toCommonString:String = toStringGeneral(APASynthesis.rendering_mode)
+}
+
+/** Disjunction of all conditions.
+ * c1 || c2 || c3 ...
+ * It is named CaseSplit because the condition is derived from a sequence of if-then-else statements/
+ * if(c1) ... else if(c2) ... else if(c3) ...
+ *
+ * @author Mikaël Mayer
+ */
+case class APACaseSplitCondition(csl: List[APAAbstractCondition]) extends APASplitCondition {
+
+ /** Returns the list of the input variables contained in this disjunction */
+ def input_variables = (csl flatMap (_.input_variables)).distinct
+
+ /** Returns a boolean indicating if the disjunction is true. */
+ def execute(l: Map[InputVar, Int]): Boolean = csl exists (_.execute(l))
+
+ /** Returns a string representing this disjunction. */
+ protected def toStringGeneral(rm: RenderingMode):String = csl map { t => ("("+(t.toCommonString)+")") } reduceLeft (_ + " "+rm.or_symbol+" " + _)
+
+ /** Returns a condition made from this disjunction. */
+ def toCondition: APACondition = APACondition(Nil, APATrue(), this)
+}
+
+/** Empty advanced condition
+ * Equivalent to a true precondition.
+ *
+ * @author Mikaël Mayer
+ */
+case class APAEmptySplitCondition() extends APASplitCondition {
+
+ /** Returns the empty set of input variables. */
+ def input_variables = Nil
+
+ /** Returns true, the truth value of this expression */
+ def execute(l: Map[InputVar, Int]): Boolean = true
+
+ /** Returns an empty string, which represents an empty condition. */
+ protected def toStringGeneral(rm: RenderingMode) = ""
+}
+
+/** Bounded quantifier representation.
+ * The variable vector will iterate over [lower_range, upper range]^n where n is the number of variables.
+ * The provided global condition is implicitly existentially quantified over this bounded variable vector.
+ * To sum up, the condition is true if global_condition holds for one tuple in the hypercube
+ *
+ * @param vl A list of input variables (v1...vn)
+ * @param lower_range The lower range for each variable.
+ * @param upper_range The upper range for each variable.
+ * @param global_condition The implicitly existentially quantified over the variables.
+ * @author Mikaël Mayer
+ */
+case class APAForCondition(vl: List[InputVar], lower_range: APAInputTerm, upper_range: APAInputTerm, global_condition: APACondition) extends APASplitCondition {
+
+ /** Returns the list of input variables in this condition, not part of the existentially quantified variables. */
+ def input_variables = (global_condition.input_variables) filterNot (vl.contains)
+
+ /** Returns a string representing the bounded quantified condition in a programming language. */
+ protected def toStringGeneral(rm: RenderingMode):String = {
+ rm match {
+ case RenderingScala => toScalaString
+ case RenderingPython => toPythonString
+ }
+ }
+
+ /** Returns a string containing the tuple of the existential variable's names */
+ def varsToString(vl : List[InputVar]) : String = vl match {
+ case Nil => ""
+ case (v::Nil) => v.name
+ case (v::q) => "("+v.name+","+varsToString(q)+")"
+ }
+
+ /** Returns a python string representing the condition */
+ def toPythonString:String = {
+ val basic_range = "xrange("+lower_range+", 1 + "+upper_range+")"
+ val list_ranges = "("+varsToString(vl)+" "+ (vl map { case i => "for "+i.name+" in "+basic_range}).reduceLeft(_ + " " + _) + ")"
+ val exists_construct = "lambda a, "+varsToString(vl)+": a or "+ global_condition.toCommonString
+ val condition = "reduce("+exists_construct+", "+list_ranges+", False)"
+ condition
+ }
+
+ /** Returns a scala string representing the condition */
+ def toScalaString:String = {
+ val basic_range = "("+lower_range+" to "+upper_range+")"
+ var ranges = basic_range
+ vl.tail foreach {k =>
+ ranges = ranges + " flatMap { t => "+basic_range+" map { i => (i, t) } } "
+ }
+
+ val expanded_vars = varsToString(vl)
+ val find_string = ranges + " exists { case "+expanded_vars+" => "
+ val cond_string = global_condition.toCommonString
+ val match_string = " }"
+ (find_string::cond_string::match_string::Nil).reduceLeft((_ + _))
+ }
+
+ /** Returns a boolean indicating if the condition is true under a given mapping */
+ def execute(l: Map[InputVar, Int]): Boolean = {
+ if(global_condition == APACondition.False) return false
+ val lr:Int = lower_range.replaceList(APAAbstractProgram.toAPAInputAssignment(l)) match {
+ case APAInputCombination(k, Nil) => k
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+l)
+ }
+ val ur:Int = upper_range.replaceList(APAAbstractProgram.toAPAInputAssignment(l)) match {
+ case APAInputCombination(k, Nil) => k
+ case t =>
+ throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+l)
+ }
+ val basic_range = (lr to ur)
+ def possible_assignments(vl: List[InputVar], i: Int, current_assignment: List[(InputVar, Int)]) : Stream[List[(InputVar, Int)]] = vl match {
+ case Nil => Stream(current_assignment)
+ case (v::q) if i > ur => Stream()
+ case (v::q) => possible_assignments(q, lr, (v, i)::current_assignment) append possible_assignments(vl, i+1, current_assignment)
+ }
+ val assignments = possible_assignments(vl, lr, Nil)
+
+ assignments exists { assignments =>
+ global_condition.execute(l ++ assignments)
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/comfusy/APAInputAssignments.scala b/src/main/scala/leon/synthesis/comfusy/APAInputAssignments.scala
new file mode 100644
index 000000000..c4a7e510e
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APAInputAssignments.scala
@@ -0,0 +1,197 @@
+package leon.synthesis.comfusy
+
+//dummy
+object APAInputAssignments
+
+/** This object offers global methods methods to deal with input assignments.
+ */
+object InputAssignment {
+ //Combines input sentences
+ def listToCommonString(input_assignment:List[InputAssignment], indent:String):String = {
+ val prog_input = input_assignment map (_.toCommonString(indent)) match {
+ case Nil => ""
+ case l => l reduceLeft {(t1, t2) => (t1 + "\n" + t2)}
+ }
+ prog_input
+ }
+}
+
+/** An input assignment is a way to assign some expressions to input variables
+ * like in "val a = b/2+c", where a, b and c are input variables.
+ */
+sealed abstract class InputAssignment {
+
+ /** Returns a list of input variables contained in the expression of this input assignment */
+ def input_variables: List[InputVar]
+
+ /** Extracts a non-exhaustive list of simple assignments of InputTerms to InputVars. */
+ def extract:List[(InputVar, APAInputTerm)]
+
+ /** Returns a string representing this assignment under the current rendering mode. */
+ def toCommonString(indent: String):String = APASynthesis.rendering_mode match {
+ case RenderingScala => toScalaString(indent)
+ case RenderingPython => toPythonString(indent)
+ }
+
+ /** Returns a scala string representing the variables on the left of val ... = ... */
+ def varToScalaString = this match {
+ case SingleInputAssignment(i, t) => i.name
+ case BezoutInputAssignment(vl, tl) => "List(" + (vl map { l => "List(" + (l map (_.name) reduceLeft (_+","+_)) + ")"} reduceLeft (_+","+_)) + ")"
+ }
+
+ /** Returns a scala string representing the value on the right of val ... = ... */
+ def valToScalaString = this match {
+ case SingleInputAssignment(i, t) => t
+ case BezoutInputAssignment(vl, tl) => "Common.bezoutWithBase(1, "+(tl map (_.toString) reduceLeft (_+", "+_))+")"
+ }
+
+ /** Returns a python string representing the variables on the left of val ... = ... */
+ def varToPythonString = this match {
+ case SingleInputAssignment(i, t) => i.name
+ case BezoutInputAssignment(vl, tl) => "(" + (vl map { l => "(" + (l map (_.name) reduceLeft (_+","+_)) + ")"} reduceLeft (_+","+_)) + ")"
+ }
+
+ /** Returns a python string representing the value on the right of val ... = ... */
+ def valToPythonString = this match {
+ case SingleInputAssignment(i, t) => t
+ case BezoutInputAssignment(vl, tl) => "bezoutWithBase(1, "+(tl map (_.toString) reduceLeft (_+", "+_))+")"
+ }
+
+ /** Returns the whole assignment as a scala string */
+ def toScalaString(indent: String): String = {
+ indent+"val "+ varToScalaString + " = " + valToScalaString
+ }
+
+ /** Returns the whole assignment as a python string */
+ def toPythonString(indent: String): String = {
+ indent+ varToPythonString + " = " + valToPythonString
+ }
+
+ /** Returns the assignment were all input variables have been replaced by corresponding input terms. */
+ def replaceList(l : List[(InputVar, APAInputTerm)]):List[InputAssignment]
+
+ /** Returns the assignment were the sign abstraction s is applied to each occurence of t1 */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):InputAssignment
+}
+
+// A simple assignment corresponding to val v = t
+case class SingleInputAssignment(v: InputVar, t: APAInputTerm) extends InputAssignment {
+ def input_variables = List(v)
+ def extract = List((v, t))
+ def replaceList(l : List[(InputVar, APAInputTerm)]) = List(SingleInputAssignment(v, t.replaceList(l)))
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction) = SingleInputAssignment(v, t.assumeSignInputTerm(t1, s))
+}
+// A complex Bézout assignemnt corresponding to val (v1::v2::Nil)::(v3::v4::Nil)::Nil = Common.bezoutWithBase(1, t1, t2)
+case class BezoutInputAssignment(v: List[List[InputVar]], t: List[APAInputTerm]) extends InputAssignment {
+ def input_variables = v.flatten : List[InputVar]
+ def extract = Nil
+ def replaceList(l: List[(InputVar, APAInputTerm)]) = BezoutInputAssignment(v, t map (_.replaceList(l))).simplified
+
+ /** Returns a simplified version of the assignment as a list of input assignments. */
+ /** Simplification occurs if some coefficients are equal to 1 or -1, or in other simple cases. */
+ def simplified: List[InputAssignment] = {
+ t map (_.simplified) match {
+ case t if t forall {
+ case APAInputCombination(i, Nil) => true
+ case _ => false
+ } =>
+ val bezout_coefs:List[Int] = t map {
+ case APAInputCombination(i, Nil) => i
+ case t => throw new Exception("Theoretically unreachable section : "+t+" should be an integer")
+ }
+ // Double zip and add all assignments to variables
+ val assignments: List[(InputVar, APAInputTerm)] = (
+ (v zip Common.bezoutWithBase(1, bezout_coefs)) map {
+ case (l1, l2) => l1 zip (
+ l2 map {
+ case i => APAInputCombination(i)
+ }
+ )
+ }
+ ).flatten
+ val assignment_converted = assignments.map({ case (v, t) => SingleInputAssignment(v, t)})
+ assignment_converted
+ case a::Nil => // This corresponds to equations of the type 1+a*v = 0. If there is a solution, it is exactly -a (a has to be equal to 1 or -1)
+ val List(List(iv)) = v
+ List(SingleInputAssignment(iv, -a))
+ case a::b::Nil => // This corresponds to equations of the type 1+a*u+b*v = 0
+ // There is an optimization if either a or b has an absolute value of 1.
+ (a, b) match {
+ case (APAInputCombination(i, Nil), b) if Math.abs(i) == 1 =>
+ // case 1 + i*u + a*v == 0
+ val index_b = 2
+ var map_index_term = Map[Int, APAInputTerm]() + (index_b -> b)
+ val new_ints = Common.bezoutWithBase(1, i, index_b)
+ val assignments = convertAssignments(v, new_ints, map_index_term)
+ val assignment_converted = assignments.map({ case (v, t) => SingleInputAssignment(v, t)})
+ assignment_converted
+ case (a, APAInputCombination(j, Nil)) if Math.abs(j) == 1 =>
+ val index_a = 2
+ var map_index_term = Map[Int, APAInputTerm]() + (index_a -> a)
+ val new_ints = Common.bezoutWithBase(1, index_a, j)
+ val assignments = convertAssignments(v, new_ints, map_index_term)
+ val assignment_converted = assignments.map({ case (v, t) => SingleInputAssignment(v, t)})
+ assignment_converted
+ case _ => List(BezoutInputAssignment(v, t))
+ }
+ case t =>
+ val t_indexed = t.zipWithIndex
+ t_indexed find {
+ case (APAInputCombination(i, Nil), index) if Math.abs(i) == 1 => true
+ case _ => false
+ } match {
+ case Some((APAInputCombination(one_coefficient, Nil), index)) =>
+ // Corresponds to something trivial like 1 + a*x + b*y + z + c*w = 0
+ // The corresponding assignment is x = y1, y = y2, z = -1-a*x-b*y-c*w and w = y3
+ // (1 )T (0, 0, -1, 0) (a)
+ // (ya) . (1, 0, -a, 0) . (b) + 1 == 0
+ // (yb) (0, 1, -b, 0) (1)
+ // (yc) (0, 0, -c, 1) (c)
+
+ // To find the solution, encode a = 10, b = 20, c=30, and in the found solution, replace -10 by -a, etc.
+ var map_index_term = Map[Int, APAInputTerm]()
+
+ val to_solve_bezout_on = t_indexed map { case (term, i) =>
+ if(i == index) {
+ one_coefficient
+ } else {
+ val final_index = 10*i+10
+ map_index_term += (final_index -> term)
+ final_index
+ }
+ }
+ val new_ints = Common.bezoutWithBase(1, to_solve_bezout_on)
+ val assignments = convertAssignments(v, new_ints, map_index_term)
+ val assignment_converted = assignments.map({ case (v, t) => SingleInputAssignment(v, t)})
+ assignment_converted
+
+ case _ => // Essentially None
+ List(BezoutInputAssignment(v, t))
+ }
+ }
+ }
+
+ /** Converts an integer Bézout solution to a InputTerm solution, where specific integers */
+ /** given in map_index_terms are replaced with some input terms. */
+ def convertAssignments(v: List[List[InputVar]],
+ solved_for_ints: List[List[Int]],
+ map_index_term: Map[Int, APAInputTerm]): List[(InputVar, APAInputTerm)] = {
+ (
+ (v zip solved_for_ints) map {
+ case (l1, l2) => l1 zip (
+ l2 map {
+ case index if map_index_term contains index =>
+ map_index_term(index)
+ case index if map_index_term contains (-index) =>
+ -map_index_term(index)
+ case i =>
+ APAInputCombination(i)
+ }
+ )
+ }
+ ).flatten
+ }
+
+ /** Propagate a sign assumption. Does nothing for Bézout assignment. */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction) = this
+}
diff --git a/src/main/scala/leon/synthesis/comfusy/APAInputSyntaxTree.scala b/src/main/scala/leon/synthesis/comfusy/APAInputSyntaxTree.scala
new file mode 100644
index 000000000..cfdea5f37
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APAInputSyntaxTree.scala
@@ -0,0 +1,721 @@
+package leon.synthesis.comfusy
+
+import scala.annotation.tailrec
+import scala.collection.mutable.ListBuffer
+
+// dummy
+object APAInputSyntaxTree
+
+/** Provides several methods to deal with input terms.
+ *
+ * @author Mikaël Mayer
+ */
+object APAInputTerm {
+ def partitionInteger(l: List[APAInputTerm]): (List[Int], List[APAInputTerm]) = l match {
+ case Nil => (Nil, Nil)
+ case (APAInputCombination(n, Nil)::q) =>
+ val (a, b) = partitionInteger(q)
+ (n::a, b)
+ case (p::q) =>
+ val (a, b) = partitionInteger(q)
+ (a, p::b)
+ }
+}
+
+/*****************
+ * Input terms *
+ *****************/
+
+/** Trait expressing that an expression can be converted to an InputTerm
+ * It is useful to deal with Input variables, which are not directly InputTerms
+ * in order not to overload the pattern matching.
+ *
+ * @author Mikaël Mayer
+ */
+trait ConvertibleToInputTerm {
+ implicit def toInputTerm():APAInputTerm
+}
+
+/** A class defining a general input term, that is, containing only input variables and integers.
+ * A sign abstraction is provided for each term.
+ *
+ * @author Mikaël Mayer
+ */
+sealed abstract class APAInputTerm extends SignAbstraction {
+
+ /** Returns the same expression, but simplified. */
+ def simplified:APAInputTerm // OptimizeMe : Store when it's already simplified in order not to compute two times the same thing
+
+ /** @return The list of Input variables that this expression contains. */
+ def input_variables: List[InputVar]
+
+ //@{ Operators
+ /** @param that A combination eventually containing output variables. */
+ /** @return The sum of this input term and the provided APACombination. */
+ def +(that : APACombination):APACombination = that + APACombination(this)
+
+ /** @return The difference of this input term and the provided APACombination. */
+ def -(that : APACombination):APACombination = -that + APACombination(this)
+
+ /** @return The product of this input term and the provided APACombination. */
+ def *(that : APACombination):APACombination = that * this
+
+ /** @return The sum of this input term and the provided input term. */
+ def +(that : APAInputTerm): APAInputTerm = APAInputAddition(this, that).simplified
+
+ /** @return The division of this input term by the provided input term. */
+ def /(that : APAInputTerm): APAInputTerm = APAInputDivision(this, that).simplified
+
+ /** @return The product of this input term by the provided input term. */
+ def *(that : APAInputTerm): APAInputTerm = APAInputMultiplication(this, that).simplified
+
+ /** @return The difference between this input term and the provided one. */
+ def -(that : APAInputTerm): APAInputTerm = (this, that) match {
+ case (t1: APAInputCombination, t2: APAInputCombination) => t1 - t2
+ case _ => this+(that*APAInputCombination(-1))
+ }
+
+ /** @return The opposite of this input term. */
+ def unary_-(): APAInputTerm = APAInputCombination(0, Nil) - this
+ //@}
+
+ /** @return This input term where all occurences of y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm
+
+ /** @return This input term where all occurences of y have been replaced by t. */
+ def replaceList(lxt : List[(InputVar, APAInputTerm)]): APAInputTerm = {
+ lxt.foldLeft(this){ case (result, (x, t)) => result.replace(x, t) }
+ }
+
+ /** @return This input term where the sign abstraction s is applied to all occurences of t1 */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAInputTerm = {
+ (this, t1, -t1) match {
+ case (t0:APAInputCombination, t1:APAInputCombination, _) if t0 == t1 =>
+ val result = t1.assumeSign(s).propagateSign(this)
+ result
+ case (t0:APAInputCombination, _, mt1:APAInputCombination) if t0 == mt1 =>
+ val result = (-t1.assumeSign(s)).propagateSign(this)
+ result
+ case (t0:APAInputCombination, t1:APAInputCombination, mt1:APAInputCombination) =>
+ this
+ case _ =>
+ this
+ }
+ }
+
+ /** @return The integer that this input term represents if it exists, else throws an exception. */
+ def toInt: Int = this match {
+ case APAInputCombination(i, Nil) => i
+ case _ =>
+ throw new Exception(this + " cannot be converted to an integer")
+ }
+
+ /** Converts this input term to a string */
+ override def toString = toGeneralString
+
+ /** Converts this input term to a string in the current rendering mode */
+ /** See APASynthesis.rendering_mode. */
+ def toGeneralString: String = APASynthesis.rendering_mode match {
+ case rm@RenderingPython => toPythonString(rm)
+ case rm@RenderingScala => toScalaString(rm)
+ }
+
+ /** Converts this input term to a Python string. */
+ /** @rm should be a RenderingPython() */
+ protected def toPythonString(rm: RenderingMode): String = this match {
+ case APAInputLCM(l) => rm.lcm_symbol+"(["+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"])"
+ case APAInputGCD(l) => rm.gcd_symbol+"(["+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"])"
+ case _ => toCommonString(rm)
+ }
+
+ /** Converts this input term to a Scala string. */
+ /** @rm should be a RenderingScala() */
+ protected def toScalaString(rm: RenderingMode): String = this match {
+ case APAInputLCM(l) => rm.lcm_symbol+"(List("+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"))"
+ case APAInputGCD(l) => rm.gcd_symbol+"(List("+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"))"
+ case _ => toCommonString(rm)
+ }
+
+ /** Converts this input term to a common string in the provided rendering mode. */
+ /** rm should be equal to APASynthesis.rendering_mode */
+ def toCommonString(rm:RenderingMode):String = this match {
+ case APAInputMultiplication(Nil) => "1"
+ case APAInputMultiplication(a::Nil) => a.toCommonString(rm)
+ case APAInputMultiplication(l) => l map {
+ case el =>
+ val s = el.toCommonString(rm)
+ if(((s indexOf '-') >= 0) || ((s indexOf '+') >= 0) || ((s indexOf '/') >= 0)) "("+s+")" else s
+ } reduceLeft (_ + "*" + _)
+ case APAInputDivision(Nil, ld) => "1/("+APAInputMultiplication(ld).toCommonString(rm)+")"
+ case APAInputDivision(ln, Nil) => APAInputMultiplication(ln).toCommonString(rm)
+ case APAInputDivision(ln, ld) =>
+ val num = APAInputMultiplication(ln).toCommonString(rm)
+ val den = APAInputMultiplication(ld).toCommonString(rm)
+ val num_string = (if((num indexOf '+') >= 0 || (num indexOf '-') >= 0 || (num indexOf '+') >= 0) "("+num+")" else num )
+ val den_string = (if((den indexOf '+') >= 0 || (den indexOf '-') >= 0 || (den indexOf '+') >= 0) "("+den+")" else den )
+ num_string +"/"+den_string
+ case APAInputAddition(l) => l map {
+ case el =>
+ val s = el.toCommonString(rm)
+ if((s indexOf '-') >= 0) "("+s+")" else s
+ } reduceLeft (_ + " + " + _)
+ case APAInputAbs(e) => rm.abs_symbol + "("+e.toCommonString(rm)+")"
+ case APAInputLCM(Nil) =>
+ throw new Exception("What is this lcm that has not been simplified ??")
+ case APAInputLCM(l) => rm.lcm_symbol+"(List("+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"))"
+ case APAInputGCD(l) => rm.gcd_symbol+"(List("+(l map (_.toCommonString(rm)) reduceLeft (_ + "," + _)) +"))"
+ case t:APAInputCombination => t.toNiceString
+ /*case APAInputMod(operand, divisor) =>
+ val num = operand.toCommonString(rm)
+ val den = operand.toCommonString(rm)
+ val num_string = (if((num indexOf '+') >= 0 || (num indexOf '-') >= 0 || (num indexOf '+') >= 0) "("+num+")" else num )
+ val den_string = (if((den indexOf '+') >= 0 || (den indexOf '-') >= 0 || (den indexOf '+') >= 0) "("+den+")" else den )
+ val final_den_string = if(divisor.isPositive) den_string else (rm.abs_symbol+"("+den_string+")")
+ rm.mod_function(num_string, final_den_string)*/
+ //case _ => super.toString
+ }
+}
+
+/** Definition of an input variable. */
+case class InputVar(name: String) extends SignAbstraction with ConvertibleToInputTerm with APAVariable {
+
+ /** Clones the variable without the sign abstraction */
+ def normalClone():this.type = InputVar(name).asInstanceOf[this.type]
+
+ /** Return an InputTerm containing the variable. */
+ def toInputTerm():APAInputCombination = {
+ if(isZero) return APAInputCombination(0)
+ APAInputCombination(this)
+ }
+ // Syntactic sugar
+ //def +(pac : APACombination) = pac+APACombination(this)
+ //def +(v : InputVar) = APACombination(v)+APACombination(this)
+ //def +(v : OutputVar) = APACombination(v)+APACombination(this)
+ //def *(i : Int) = APAInputCombination(0, (i, this)::Nil)
+ //def *(that: APAInputTerm) = APAInputMultiplication(APAInputCombination(this), that)
+}
+
+/** Object to provide more constructors for APAInputCombination.
+ */
+object APAInputCombination {
+ def apply(i: Int):APAInputCombination = APAInputCombination(i, Nil)
+ def apply(i: InputVar):APAInputCombination = APAInputCombination(0, (1, i)::Nil).propagateSign(i)
+}
+
+/** A linear combination of input variables, with a constant coefficient.
+ */
+case class APAInputCombination(coefficient: Int, input_linear: List[(Int, InputVar)]) extends APAInputTerm {
+ setSign(SignAbstraction.linearCombinationSign(coefficient, input_linear))
+
+ /** Clones the expression without the sign abstraction. */
+ def normalClone():this.type = APAInputCombination(coefficient, input_linear).asInstanceOf[this.type]
+
+ /** Returns the list of input variables that this expression contains. */
+ def input_variables: List[InputVar] = input_linear map (_._2)
+
+ /** Returns true if the variable i1 is has a name lexicographically less than the variable i2. */
+ def by_InputVar_name(i1:(Int, InputVar), i2:(Int, InputVar)) : Boolean = (i1, i2) match {
+ case ((_, InputVar(name1)), (_, InputVar(name2))) => name1 < name2
+ }
+
+ /** Adds the coefficiented variable i to the list of existing coefficiented regrouped_vars. */
+ /** Assumes that if the variable appears exist, it appears first. */
+ def fold_Inputvar_name(i:(Int, InputVar), regrouped_vars:List[(Int, InputVar)]):List[(Int, InputVar)] = (i, regrouped_vars) match {
+ case (i, Nil) => i::Nil
+ case ((coef1, InputVar(name1)), (coef2, InputVar(name2))::q) if name1 == name2 => (coef1 + coef2, InputVar(name1))::q
+ case (i, q) => i::q
+ }
+
+ /** Intercepts the sign propagation, and if there is a unique variable, propagates the sign abstraction to it. */
+ override def propagateSign(s: SignAbstraction):this.type = { //Intercepts the sign propagation
+ val result = (coefficient, input_linear) match {
+ case (0, (i, v)::Nil) =>
+ val new_v = v.assumeSign(SignAbstraction.multSign(SignAbstraction.mergeSign(this, s), SignAbstraction.number(i)))
+ APAInputCombination(0, (i, new_v)::Nil)
+ case _ => this
+ }
+ result.propagateSign_internal(s).asInstanceOf[this.type]
+ }
+
+ /** Returns a simplified version of this input combination.
+ * Guarantees that
+ * - The variables are alphabetically sorted,
+ * - There are no null coefficients
+ */
+ def simplified: APAInputCombination = {
+ if(isZero) return APAInputCombination(0)
+ val input_linear2 = (input_linear sortWith by_InputVar_name ).foldRight[List[(Int, InputVar)]](Nil){ case (a, b) => fold_Inputvar_name(a, b)}
+ val input_linear3: List[(Int, InputVar)] = input_linear2 match {
+ case (i, v)::Nil => (i, v.assumeSign(SignAbstraction.multSign(this, SignAbstraction.number(i))))::Nil
+ case _ => input_linear2
+ }
+ APAInputCombination(coefficient, input_linear3 filterNot { case (i, v) => i == 0 || v.isZero}).propagateSign(this)
+ }
+
+ /** Returns the list of the coefficients in front of the input variables + the constant coefficient. */
+ def coefficient_list = (coefficient :: ((input_linear map (_._1)) ))
+
+ /** Returns true if there is a non-null coefficient in the combination. */
+ def has_gcd_coefs: Boolean = coefficient_list exists (_ != 0)
+
+ /** Returns the gcd of all coefficients. has_gcd_coefs is assumed. */
+ def gcd_coefs = Common.gcdlist(coefficient_list)
+
+ /** Returns the first sign present.
+ * If this sign is negative in equations like -a+b == 0,
+ * it is used to gain a character and produce a-b == 0
+ */
+ def first_sign_present = coefficient_list find (_ != 0) match {
+ case Some(i) => if(i > 0) 1 else -1
+ case None => 1
+ }
+
+ /** Returns the division of this combination by an integer. */
+ /** Needs the coefficients to be divisible by i. */
+ def /(i : Int): APAInputCombination = {
+ APAInputCombination(coefficient / i, input_linear map {t => (t._1 / i, t._2)}).assumeSign(SignAbstraction.multSign(this, SignAbstraction.number(i)))
+ }
+
+ /** Returns true if this combination can be safely divisible by i. */
+ def safelyDivisibleBy(i : Int): Boolean = {
+ coefficient % i == 0 && (input_linear forall { case (k, v) => k % i == 0})
+ }
+
+ /** Returns the division of an input combination by another. */
+ /** The result is not necessarily a input combination */
+ def /(that : APAInputCombination): APAInputTerm = {
+ APAInputDivision(this, that).simplified
+ }
+
+ /** Returns the multiplication of this input combination by an integer. */
+ def *(i : Int): APAInputCombination = {
+ APAInputCombination(coefficient * i, input_linear map {t => (t._1 * i, t._2)}).assumeSign(SignAbstraction.multSign(this, SignAbstraction.number(i)))
+ }
+
+ /** Returns the multiplication of this input combination by another input combination. */
+ /** The result is not necessarily a input combination */
+ def *(that : APAInputCombination): APAInputTerm = {
+ APAInputMultiplication(this, that).simplified
+ }
+
+ /** Returns the sum of two input combinations. */
+ def +(pac : APAInputCombination): APAInputCombination = pac match {
+ case APAInputCombination(c, i) =>
+ APAInputCombination(coefficient + c, input_linear ++ i).simplified.assumeSign(SignAbstraction.addSign(this, pac))
+ }
+
+ /** Returns the difference between two input combinations. */
+ def -(that : APAInputCombination): APAInputCombination = this + (that * (-1))
+
+ /** Returns the sum of this input combination with a coefficiented variable. */
+ def +(kv : (Int, InputVar)): APAInputCombination = this + APAInputCombination(0, kv::Nil)
+
+ /** Returns the sum of this input combination with an integer. */
+ def +(k : Int): APAInputCombination = this + APAInputCombination(k, Nil)
+
+ /** Returns the difference of this input combination with a coefficiented variable. */
+ def -(kv : (Int, InputVar)): APAInputCombination = this - APAInputCombination(0, kv::Nil)
+
+ /** Returns the difference of this input combination with an integer. */
+ def -(k : Int): APAInputCombination = this + APAInputCombination(-k, Nil)
+
+ /** Returns the opposite of this input combination. */
+ override def unary_-(): APAInputCombination = (APAInputCombination(0, Nil) - this).propagateSign(SignAbstraction.oppSign(this))
+
+ /** Returns the linear expression where the input variable y has been replaced by the expression t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ val (input_linear_with_y, input_linear_without_y) = input_linear partition (_._2 == y)
+ val pac_without_y = APAInputCombination(coefficient, input_linear_without_y)
+ val total_y_coefficient = (input_linear_with_y map (_._1)).foldLeft(0)(_+_)
+ val result = t match {
+ case t:APAInputCombination =>
+ pac_without_y + (t*total_y_coefficient)
+ case _ =>
+ APAInputAddition(pac_without_y, APAInputMultiplication(APAInputCombination(total_y_coefficient), t))
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns this expression where the fact that t1 has sign s has been taken into account. */
+ override def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction) = {
+ t1 match {
+ case t@APAInputCombination(coefficient2, Nil) => this // Would be strange to arrive there.
+ case t@APAInputCombination(coefficient2, (i, v)::l) => // i is not null,
+ input_linear find (_._2 == v) match {
+ case Some((i2, v2)) =>
+ val t_assumed = t.assumeSign(s)
+ val resultWithoutT = (this*i-t_assumed*i2)
+ val resultAddingT =(t_assumed*i2)
+ val resultMultipliedByI = resultWithoutT+resultAddingT
+ val result = resultMultipliedByI/i
+ result
+ case None => this // This variable is not there, so we cannot conclude anything.
+ }
+ case _ => this
+
+ }
+ }
+
+ /** Returns a string representing this linear combination. */
+ override def toString = toNiceString // Comment this to keep the abstract syntax tree representation
+
+ /** Returns a nice string representing an usual linear combination, e.g. like 5+3a. */
+ def toNiceString:String = {
+ def inputElementToString(kv : (Int, InputVar)) = kv._1 match {
+ case 1 => kv._2.name
+ case -1 => "-" + kv._2.name
+ case k => k + "*" + kv._2.name
+ }
+ def makePlus(l: List[String]):String = l match {
+ case Nil => ""
+ case a::p => val s = makePlus(p)
+ if(s=="") a
+ else if(a=="") s
+ else if(s.charAt(0) == '-')
+ a + s
+ else
+ a + "+" + s
+ }
+ var c_string = if(coefficient == 0) "" else coefficient.toString
+ var i_string = input_linear match {
+ case Nil => ""
+ case a::l => l.foldLeft(inputElementToString(a)) { (s, t2) =>
+ val t2s = inputElementToString(t2)
+ s + (if(t2s.charAt(0) =='-') t2s else "+" + t2s)}
+ }
+ val s = makePlus(c_string::i_string::Nil)
+ if(s == "") "0" else s
+ }
+}
+
+/** Object providing methods to create a division of input terms, with some optimizations.
+ */
+object APAInputDivision {
+
+ /** Returns a simplified division of input terms. */
+ def apply(a: APAInputTerm, b: APAInputTerm): APAInputTerm = APAInputDivision(a::Nil, b::Nil).simplified
+
+ /** Returns a division where common occurrences between n and d have been removed (simplification). */
+ def simplifyNumDenom(n: List[APAInputTerm], d:List[APAInputTerm]):APAInputTerm = {
+ @tailrec def aux(n: List[APAInputTerm], d: List[APAInputTerm], collectedN: ListBuffer[APAInputTerm], collectedD: ListBuffer[APAInputTerm]): APAInputTerm = {
+ (n, d) match {
+ case (Nil, Nil) =>
+ (collectedN.toList, collectedD.toList) match {
+ case (Nil, Nil) => APAInputCombination(1, Nil)
+ case (n::Nil, Nil) => n
+ case (n, Nil) => APAInputMultiplication(n)
+ case (n, d) => APAInputDivision(n, d)
+ }
+ case (n1::np, d1::dp) =>
+ val i = d.indexOf(n1)
+ if (i > -1) {
+ aux(np, d.take(i) ++ d.drop(i+1), collectedN, collectedD)
+ } else {
+ val j = n.indexOf(d1)
+ if( j > -1) {
+ aux(n.take(j) ++ n.drop(j+1), dp, collectedN, collectedD)
+ } else {
+ aux(np, dp, collectedN += n1, collectedD += d1)
+ }
+ }
+ case (n, Nil) =>
+ aux(Nil, Nil, collectedN ++= n, collectedD)
+ case (Nil, d) =>
+ aux(Nil, Nil, collectedN, collectedD ++= d)
+ }
+ }
+ aux(n, d, ListBuffer(), ListBuffer())
+ }
+}
+
+/** Class representing a integer division between input terms.
+ * It should be guaranteed that the denominator divides the numerator.
+ */
+case class APAInputDivision(numerator: List[APAInputTerm], denominator : List[APAInputTerm]) extends APAInputTerm {
+ setSign(SignAbstraction.divSign(SignAbstraction.multSign(numerator), SignAbstraction.multSign(denominator)))
+
+ /** Returns a clone of this expression without the sign abstraction. */
+ def normalClone():this.type = APAInputDivision(numerator, denominator).asInstanceOf[this.type]
+
+ /** Returns a simplified version of this division. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val result = ((APAInputMultiplication(numerator).simplified, APAInputMultiplication(denominator).simplified) match {
+ case (n, APAInputCombination(1, Nil)) => n
+ case (n, d) if n == d => APAInputCombination(1, Nil)
+ case (nm@APAInputMultiplication(n), dm@APAInputMultiplication(d)) => APAInputDivision.simplifyNumDenom(n, d)
+ case (nm, dm@APAInputMultiplication(d)) => APAInputDivision.simplifyNumDenom(nm::Nil, d)
+ case (nm@APAInputMultiplication(n), dm) => APAInputDivision.simplifyNumDenom(n, dm::Nil)
+ case (nc@APAInputCombination(c, Nil), dc@APAInputCombination(i, Nil)) => APAInputCombination(c/i)
+ case (nc@APAInputCombination(c, l), dc@APAInputCombination(i, Nil)) if nc.safelyDivisibleBy(i) => nc/i
+ case (nc@APAInputCombination(c, l), dc@APAInputCombination(i, Nil)) => APAInputDivision(nc::Nil, dc::Nil)
+ case (n, d) => APAInputDivision(n::Nil, d::Nil)
+ })
+ result.propagateSign(this)
+ }
+
+ /** Returns the division where the variable y has been replaced by the input term t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputDivision(numerator map (_.replace(y, t)), denominator map (_.replace(y, t))).simplified.propagateSign(this)
+ }
+
+ /** Returns the list of input variables that this division contains. */
+ def input_variables: List[InputVar] = {
+ ((numerator flatMap (_.input_variables)) ++ (denominator flatMap (_.input_variables))).distinct
+ }
+}
+
+/** Object providing a method to create multiplications of input terms.
+ */
+object APAInputMultiplication {
+ def apply(a: APAInputTerm*):APAInputTerm = APAInputMultiplication(a.toList).simplified
+}
+
+/** Class representing a multiplication between input terms. */
+case class APAInputMultiplication(operands: List[APAInputTerm]) extends APAInputTerm {
+ //assert(operands.length > 1) // Else it does not make sense, it should have been simplified.
+ setSign(SignAbstraction.multSign(operands))
+
+ /** Returns a clone of this multiplication without the sign abstraction. */
+ def normalClone():this.type = APAInputMultiplication(operands).asInstanceOf[this.type]
+
+ /** Returns a simplified equal version of this multiplication. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val result = operands flatMap (_.simplified match {
+ case APAInputMultiplication(l) => l map (_.assumeNotzerobility(this))
+ case APAInputCombination(1, Nil) => Nil
+ case t => List(t.assumeNotzerobility(this))
+ }) match {
+ case Nil => APAInputCombination(1, Nil)
+ case a::Nil => a
+ case l =>
+ APAInputTerm.partitionInteger(l) match {
+ case (Nil, l) =>
+ APAInputMultiplication(l)
+ case (integers, not_input_combinations) =>
+ ((integers reduceLeft (_ * _)), not_input_combinations) match {
+ case (0, _) => APAInputCombination(0)
+ case (a, Nil) => APAInputCombination(a)
+ case (a, (t:APAInputCombination)::q) => APAInputMultiplication((t*a)::q)
+ case (a, _) => val s = APAInputCombination(a)::not_input_combinations
+ APAInputMultiplication(s)
+ }
+ }
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns the same multiplication where the non-zerobility of the applied sign abstraction. */
+ /** is propagated to all sub-children. */
+ override def propagateSign(s: SignAbstraction):this.type = { //Intercepts the sign propagation
+ if(s.isNotZero) {
+ val new_operands = operands map (_.assumeNotzerobility(s))
+ APAInputMultiplication(new_operands).propagateSign_internal(s).asInstanceOf[this.type]
+ } else {
+ APAInputMultiplication(operands).propagateSign_internal(s).asInstanceOf[this.type]
+ }
+ }
+
+ /** Returns an expression where all occurences of the variable y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputMultiplication(operands map (_.replace(y, t))).propagateSign(this).simplified
+ }
+
+ /** Returns the list of input variables contained in this multiplication. */
+ def input_variables: List[InputVar] = {
+ (operands flatMap (_.input_variables)).distinct
+ }
+}
+
+/** Object providing a method to create additions of input terms and others.
+ */
+object APAInputAddition {
+
+ /** Returns an addition of the given input terms. */
+ def apply(a: APAInputTerm*):APAInputTerm = APAInputAddition(a.toList).simplified
+
+ /** Separate the input terms in l between input combinations and general input terms. */
+ /** Used to group input combinations together */
+ def partitionInputCombination(l: List[APAInputTerm]): (List[APAInputCombination], List[APAInputTerm]) = l match {
+ case Nil => (Nil, Nil)
+ case ((t@APAInputCombination(_, _))::q) =>
+ val (a, b) = partitionInputCombination(q)
+ (t::a, b)
+ case (p::q) =>
+ val (a, b) = partitionInputCombination(q)
+ (a, p::b)
+ }
+}
+
+/** Class representing an addition of given input terms.
+ * Additions differs from linear combinations, because they can store general additions
+ * like a*b+c+b^2+1
+ */
+case class APAInputAddition(l: List[APAInputTerm]) extends APAInputTerm {
+ setSign(SignAbstraction.addSign(l))
+
+ /** Returns a clone of this addition without the top-level abstraction (strange ?). */
+ def normalClone():this.type = APAInputAddition(l).asInstanceOf[this.type]
+
+ /** Returns a simplified version of this addition. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val result = l flatMap (_.simplified match {
+ case APAInputAddition(l) => l
+ case APAInputCombination(0, Nil) => Nil
+ case t => List(t)
+ }) match {
+ case Nil => APAInputCombination(0, Nil)
+ case a::Nil => a
+ case l =>
+ APAInputAddition.partitionInputCombination(l) match {
+ case (Nil, l) =>
+ APAInputAddition(l)
+ case (input_combinations, not_input_combinations) =>
+ ((input_combinations reduceLeft (_ + _)), not_input_combinations) match {
+ case (a, Nil) => a
+ case (a, _) => val s = a::not_input_combinations
+ APAInputAddition(s)
+ }
+
+ }
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns an expression where all occurences of the variable y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputAddition(l map (_.replace(y, t))).propagateSign(this).simplified
+ }
+
+ /** Returns the list of input variables contained in this addition. */
+ def input_variables: List[InputVar] = {
+ (l flatMap (_.input_variables)).distinct
+ }
+}
+
+/** Class representing an absolute value of an input term.
+ */
+case class APAInputAbs(arg: APAInputTerm) extends APAInputTerm {
+ setSign(SignAbstraction.absSign(arg))
+
+ /** Returns a clone of this absolute value without the abstraction. */
+ def normalClone():this.type = APAInputAbs(arg).asInstanceOf[this.type]
+
+ /** Returns a simplified version of this absolute value. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val result = arg.simplified match {
+ case t if t.isPositiveZero => t
+ case APAInputCombination(i, Nil) => APAInputCombination(Math.abs(i), Nil)
+ case t =>
+ APAInputAbs(t)
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns an expression where all occurences of the variable y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ val result = APAInputAbs(arg.replace(y, t)).simplified
+ result.propagateSign(this)
+ }
+
+ /** Returns the list of input variables contained in this absolute value. */
+ def input_variables: List[InputVar] = {
+ arg.input_variables
+ }
+}
+
+/** Class representing the gcd of a list of input terms.
+ * The list of input terms should be guaranteed not to be all zero at the same time.
+ */
+case class APAInputGCD(l: List[APAInputTerm]) extends APAInputTerm {
+ setSign(1)
+
+ /** Returns a clone of this gcd without the abstraction. */
+ def normalClone():this.type = APAInputGCD(l).asInstanceOf[this.type]
+
+ /** Returns a simplified version of this gcd. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val (integers, non_integers) = APAInputTerm.partitionInteger(l map (_.simplified))
+ val result = (Common.gcdlistComplete(integers), non_integers) match {
+ case (Some(1), _) => APAInputCombination(1, Nil)
+ case (None, k::Nil) => APAInputAbs(k).simplified
+ case (None, Nil) =>
+ throw new Error("GCD is not defined on an empty set")
+ case (None, l) => APAInputGCD(l)
+ case (Some(n), Nil) => APAInputAbs(APAInputCombination(n, Nil)).simplified
+ case (Some(n), l) => APAInputGCD(APAInputCombination(n, Nil)::l)
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns an expression where all occurences of the variable y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputGCD(l map (_.replace(y, t))).simplified.propagateSign(this)
+ }
+
+ /** Returns the list of input variables contained in this gcd. */
+ def input_variables: List[InputVar] = {
+ (l flatMap (_.input_variables)).distinct
+ }
+}
+
+/** Class representing the lcm of a list of input terms.
+ */
+case class APAInputLCM(l: List[APAInputTerm]) extends APAInputTerm {
+ setSign(1)
+
+ /** Returns a clone of this lcm without the abstraction. */
+ def normalClone():this.type = APAInputLCM(l).asInstanceOf[this.type]
+
+ /** Returns a simplified version of this lcm. */
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val (integers, non_integers) = APAInputTerm.partitionInteger(l map (_.simplified))
+ val result = (Common.lcmlist(integers), non_integers) match {
+ case (1, Nil) => APAInputCombination(1)
+ case (1, k::Nil) => APAInputAbs(k).simplified
+ case (1, k1::k2::l) if k1 == k2 => APAInputLCM(k2::l).simplified
+ case (1, l) => APAInputLCM(l)
+ case (n, Nil) => APAInputAbs(APAInputCombination(n, Nil)).simplified
+ case (n, l) => APAInputLCM(APAInputCombination(n, Nil)::l)
+ }
+ result.propagateSign(this)
+ }
+
+ /** Returns an expression where all occurences of the variable y have been replaced by t. */
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputLCM(l map (_.replace(y, t))).simplified.propagateSign(this)
+ }
+
+ /** Returns the list of input variables contained in this lcm. */
+ def input_variables: List[InputVar] = {
+ (l flatMap (_.input_variables)).distinct
+ }
+}
+/*
+case class APAInputMod(operand: APAInputTerm, divisor: APAInputTerm) extends APAInputTerm {
+ setSign(true, true, false) // >= 0
+ if(divisor.can_be_zero) throw new Exception("Error : "+divisor+" can be zero in expression "+this)
+
+ def normalClone():this.type = APAInputMod(operand, divisor).asInstanceOf[this.type]
+ def simplified:APAInputTerm = {
+ if(isZero) return APAInputCombination(0)
+ val result = (operand.simplified, divisor.simplified) match {
+ case (APAInputCombination(0, Nil), _) => APAInputCombination(0, Nil)
+ case (_, APAInputCombination(1, Nil)) => APAInputCombination(0, Nil)
+ case (APAInputCombination(i, Nil), APAInputCombination(j, Nil)) if j != 0 => APAInputCombination(Common.smod(i, j), Nil)
+ case (o, d) => APAInputMod(o, d)
+ }
+ result.propagateSign(this)
+ }
+ def replace(y: InputVar, t: APAInputTerm):APAInputTerm = {
+ APAInputMod(operand.replace(y, t), divisor.replace(y, t)).simplified.propagateSign(this)
+ }
+ def input_variables: List[InputVar] = {
+ (operand.input_variables ++ divisor.input_variables).distinct
+ }
+}*/
diff --git a/src/main/scala/leon/synthesis/comfusy/APAProgram.scala b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala
new file mode 100644
index 000000000..05118df55
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala
@@ -0,0 +1,650 @@
+package leon.synthesis.comfusy
+
+
+/** Object providing methods to deal with generated programs.
+ *
+ * @author Mikaël Mayer
+ */
+object APAAbstractProgram {
+
+ /** Converts a map of (input variable, integer) to its corresponding input assignment list. */
+ def toAPAInputAssignment(imap : Map[InputVar, Int]):List[(InputVar, APAInputCombination)] =
+ imap.toList map {case (v, i) => (v, APAInputCombination(i, Nil))}
+
+ /** Converts a map of (output variable, integer) to its corresponding output assignment list. */
+ def toAPAOutputAssignment(imap : Map[OutputVar, Int]):List[(OutputVar, APACombination)] =
+ imap.toList map {case (v, i) => (v, APACombination(APAInputCombination(i, Nil), Nil))}
+
+ /** Returns the combination of the two sentences, adding a "\n" if needed */
+ def combineSentences(s1: String, s2: String):String = (if(s1.endsWith("\n") || s1 == "") s1 else s1 + "\n") + s2
+
+ /** Returns a list of useful consistent input and output assignments,
+ * given existing assignments and needs.
+ *
+ * @param input_assignments The input assignments of the program.
+ * @param output_assignment The output assignments of the program.
+ * @param assignments_to_propagate_input A list of simple input assignments which can be propagated at anytime.
+ * @param assignments_to_propagate_output A list of simple output assignments which can be propagated at anytime.
+ * @param interesting_input_variables A list of input variables that are needed for further computation.
+ * @param interesting_output_variables A list of output variables that are needed for the final program
+ */
+ def propagation_delete_temp(
+ input_assignments : List[InputAssignment],
+ output_assignments : List[(OutputVar, APATerm)],
+ assignments_to_propagate_input : List[(InputVar, APAInputCombination)],
+ assignments_to_propagate_output : List[(OutputVar, APACombination)],
+ interesting_input_variables : List[InputVar], //Variables appearing in a split for example.
+ interesting_output_variables : List[OutputVar])
+ : (List[InputAssignment], List[(OutputVar, APATerm)]) =
+ recursive_propagation_delete_temp(input_assignments,
+ output_assignments,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables, Nil, Nil)
+ /** Tail-recursive version of propagation_delete_temp
+ * Returns a list of useful consistent input and output assignments,
+ * given existing assignments and needs.
+ *
+ * @param input_assignments The input assignments of the program.
+ * @param output_assignment The output assignments of the program.
+ * @param assignments_to_propagate_input A list of simple input assignments which can be propagated at anytime.
+ * @param assignments_to_propagate_output A list of simple output assignments which can be propagated at anytime.
+ * @param interesting_input_variables A list of input variables that are needed for further computation.
+ * @param interesting_output_variables A list of output variables that are needed for the final program
+ * @param input_assignments_new The current list of final input assignments
+ * @param input_assignments_new The current list of final output assignments
+ */
+ def recursive_propagation_delete_temp(
+ input_assignments : List[InputAssignment],
+ output_assignments : List[(OutputVar, APATerm)],
+ assignments_to_propagate_input : List[(InputVar, APAInputCombination)],
+ assignments_to_propagate_output : List[(OutputVar, APACombination)],
+ interesting_input_variables : List[InputVar],
+ interesting_output_variables : List[OutputVar],
+ input_assignments_new : List[InputAssignment],
+ output_assignments_new : List[(OutputVar, APATerm)]
+ )
+ : (List[InputAssignment], List[(OutputVar, APATerm)]) = {
+ // First: input assignments and then output assignments
+ input_assignments match {
+ case Nil =>
+ output_assignments match {
+ case Nil => (input_assignments_new.reverse, output_assignments_new.reverse)
+ case (v, pac@APACombination(_, _))::q =>
+ pac.replaceListInput(assignments_to_propagate_input).replaceList(assignments_to_propagate_output) match {
+ case t@APACombination(_, _) =>
+ if(interesting_output_variables contains v) { // yes ! let's keep this variable
+ recursive_propagation_delete_temp(Nil, q,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output ++ ((v,t)::Nil),
+ interesting_input_variables,
+ interesting_output_variables,
+ input_assignments_new,
+ (v, t)::output_assignments_new)
+ } else { // Not interesting to keep this variable. Just replace its content.
+ recursive_propagation_delete_temp(Nil, q,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output ++ ((v,t)::Nil),
+ interesting_input_variables,
+ interesting_output_variables,
+ input_assignments_new, output_assignments_new)
+ }
+ // The term is not affine anymore, so we keep it without replacing.
+ case t => recursive_propagation_delete_temp(Nil, q,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables,
+ input_assignments_new,
+ (v, t)::output_assignments_new)
+ }
+ // The term is not affine, so we keep it without replacing.
+ case (v, t)::q =>
+ recursive_propagation_delete_temp(Nil, q,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables,
+ input_assignments_new,
+ (v, t)::output_assignments_new)
+ }
+ // On input_assignments : they can be useful if case disjunctions, so we always keep them.
+ // OptimizeMe : If not used in case disjunction, remove input variables.
+ case (ass@SingleInputAssignment(v, pac@APAInputCombination(_, _)))::q =>
+ val keep_assigment = interesting_input_variables contains v
+ pac.replaceList(assignments_to_propagate_input) match {
+ case t@APAInputCombination(_, _) => // We propagate everything.
+ recursive_propagation_delete_temp(q, output_assignments,
+ assignments_to_propagate_input ++ ((v,t)::Nil),
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables,
+ (if(keep_assigment) (ass::input_assignments_new) else input_assignments_new),
+ output_assignments_new)
+ // Should not happen
+ case t => throw new Error("Honestly, I don't see how an input combination" + pac + "could be reduced to something else like" + t + ", but it happened.")
+ }
+ case assignment::q =>
+ assignment.replaceList(assignments_to_propagate_input) match {
+ case Nil => throw new Error("In theory it cannot come up to this point")
+ case new_assignment::Nil =>
+ recursive_propagation_delete_temp(q, output_assignments,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables,
+ new_assignment::input_assignments_new,
+ output_assignments_new)
+ case l =>
+ recursive_propagation_delete_temp(l ++ q, output_assignments,
+ assignments_to_propagate_input,
+ assignments_to_propagate_output,
+ interesting_input_variables,
+ interesting_output_variables,
+ input_assignments_new,
+ output_assignments_new)
+ }
+ }
+
+ }
+}
+
+/** Abstract class representing program common properties.
+ */
+sealed abstract class APAAbstractProgram {
+
+ /** Converts this program to a string which can be visualized.*/
+ def toCommonString(indent: String): String
+
+ /** Executes the program under the provided environment.
+ * Returns a list of integer mappings. */
+ def execute(l: Map[InputVar, Int]): Map[OutputVar, Int]
+
+ /** Returns the list of input variables needed by the program. */
+ def input_variables: List[InputVar]
+}
+
+/** Abstract class representing a particular class of programs, the middle part.
+ * It helps to describe conjunction or disjunctions of programs.
+ * One difference with a APAProgram is that it does not store the needed output variables,
+ * and thus needs an enclosing APAProgram to work.
+ */
+abstract class APASplit extends APAAbstractProgram
+
+/** Program equivalent to assert(false)
+ * A program containing an APAFalseSplit has a false precondition. */
+case class APAFalseSplit() extends APASplit {
+ def toCommonString(indent: String) = ""
+ def execute(l: Map[InputVar, Int]) = Map[OutputVar, Int]()
+ def input_variables = Nil
+}
+
+/** Program equivalent to NOOP. */
+case class APAEmptySplit() extends APASplit {
+ def toCommonString(indent: String) = ""
+ def execute(l: Map[InputVar, Int]) = Map[OutputVar, Int]()
+ def input_variables = Nil
+}
+
+/** Object providing several methods used by the class APACaseSplit */
+object APACaseSplit {
+
+ /** Returns a string containing the variable definition.
+ * For Scala, it corresponds to "val (x, y, z) = " */
+ def variable_define(indent: String, tuple_variables: String):String = {
+ APASynthesis.rendering_mode match {
+ case RenderingPython =>
+ indent // All variables will be described inside the program.
+ case RenderingScala =>
+ indent + "val "+ tuple_variables +" = "
+ }
+ }
+
+ /** Returns an optimized version of a given case split. */
+ def optimized(programs: List[(APACondition, APAProgram)]): APACaseSplit = {
+ val new_programs = programs filterNot {
+ case (cond, prog) =>
+ cond.global_condition == APAFalse() || (cond.pf match {
+ case t:APAForCondition => t.global_condition == APAFalse()
+ case _ => false
+ })
+ }
+ val reduced_programs = new_programs find {
+ case (cond, prog) => cond.isTrivial()
+ } match {
+ case Some(a) => a::Nil // Returns some trivial solution if it exists.
+ case _ => new_programs
+ }
+ APACaseSplit(reduced_programs)
+ }
+}
+
+/** Program used to represent a disjunction of programs under their conditions.
+ *
+ * if(condition1) program1
+ * else if(condition2) program2
+ * else if...
+ * else throw new Exception("No solution")
+ */
+case class APACaseSplit(programs: List[(APACondition, APAProgram)]) extends APASplit {
+
+ /** Returns a list containing the input variables presents in all sub-programs. */
+ def input_variables = (programs flatMap (_._2.input_variables)).distinct
+
+ /** Returns an indented string describing the program. */
+ override def toString = toCommonString(" ")
+
+ /** Returns the program equivalent to this case split. */
+ def toProgram: APAProgram = programs match {
+ case Nil => APAProgram.empty
+ case (c, p)::Nil => p
+ case (c, p)::q =>
+ APAProgram(p.input_variables, Nil, this, Nil, p.output_variables)
+ }
+
+ /** Returns a string representing this case split in the language provided in APASynthesis.rendering_mode. */
+ def toCommonString(indent: String) = {
+ APASynthesis.rendering_mode match {
+ case RenderingScala => toScalaString(indent)
+ case RenderingPython => toPythonString(indent)
+ }
+ }
+
+ /** Returns a string representing this case split in python.
+ * APASynthesis.rendering_mode should have been set to RenderingPython. */
+ def toPythonString(indent: String) = {
+ val indent2 = indent + " "
+ (programs match {
+ case Nil => ""
+ case ((cond, pap)::Nil) =>
+ pap.innerCommonContent(indent)
+ case ((cond, pap)::_::q) =>
+ val error_result = pap.errorResultCommon(RenderingPython)
+ val prefix = APACaseSplit.variable_define(indent, pap.resultCommonContent(""))
+ prefix +
+ ((programs map {
+ case (cond, pap) =>
+ val prog_if = "if "+(cond.toCommonString)+":"
+ val prog_ifthen = pap.innerCommonContent(indent2)
+ //val prog_ifthenresult = pap.resultCommonContent(indent2)
+ val prog_ifend = indent
+ (prog_if::prog_ifthen::prog_ifend::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ })++(("se:\n"+indent2+error_result)::Nil)).reduceLeft( _ + "el" + _)
+ })
+ }
+
+ /** Returns a string representing this case split in Scala.
+ * APASynthesis.rendering_mode should have been set to RenderingScala. */
+ def toScalaString(indent: String) = {
+ val indent2 = indent + " "
+ (programs match {
+ case Nil => ""
+ case ((cond, pap)::Nil) =>
+ pap.innerCommonContent(indent)
+ case ((cond, pap)::_::q) =>
+ val error_result = pap.errorResultCommon(RenderingScala)
+ val prefix = APACaseSplit.variable_define(indent, pap.resultCommonContent(""))
+ prefix +
+ ((programs map {
+ case (cond, pap) =>
+ val prog_if = "if("+(cond.conditionToScalaString)+") {"
+ val prog_ifthen = pap.innerCommonContent(indent2)
+ val prog_ifthenresult = pap.resultCommonContent(indent2)
+ val prog_ifend = indent + "}"
+ (prog_if::prog_ifthen::prog_ifthenresult::prog_ifend::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ })++(("{ "+error_result+" }")::Nil)).reduceLeft( _ + " else " + _)
+ })
+ }
+
+ /** Executes this case split under the provided environment. */
+ def execute(l: Map[InputVar, Int]): Map[OutputVar, Int] = {
+ programs foreach {
+ case (cond, prog) =>
+ if(cond.execute(l)) return prog.execute(l)
+ }
+ Map[OutputVar, Int]()
+ }
+}
+
+/** Program used to represent a pair (condition, program) which should execute the program whose condition is true for
+ * a particular value of the input variables.
+ *
+ * for((v1, ..., vL) in [lower_range, upper_range]^L) {
+ * if(condition) {
+ * program
+ * exitloop
+ * }
+ * }
+ * @param vl The list of input variables which are bound by the for-loop (bound input variabless).
+ * @param lower_range The lower range for each of the variables in vl.
+ * @param upper_range The upper range for each of the variables in vl.
+ * @param condition The condition to test.
+ * @param program The program to execute if the condition is ok.
+ */
+case class APAForSplit(vl: List[InputVar], lower_range: APAInputTerm, upper_range: APAInputTerm, condition: APACondition, program: APAProgram) extends APASplit {
+
+ /** Converts this program to an indented string. */
+ override def toString = toCommonString(" ")
+
+ /** Returns a list of the input variables contained in the program, without the bound variables in the for loop. */
+ def input_variables = (program.input_variables) filterNot (vl.contains)
+
+ /** Returns an string containing the program, depending on the rendering mode APASynthesis.rendering_mode. */
+ def toCommonString(indent: String) = {
+ APASynthesis.rendering_mode match {
+ case RenderingScala => toScalaString(indent)
+ case RenderingPython => toPythonString(indent)
+ }
+ }
+
+ /** Converts the bound variables to a tuple string. */
+ def varsToString(vl : List[InputVar]) : String = vl match {
+ case Nil => ""
+ case (v::Nil) => v.name
+ case (v::q) => "("+v.name+","+varsToString(q)+")"
+ }
+
+ /** Returns a string containing the program in python.
+ * APASynthesis.rendering_mode should be set to RenderingPython. */
+ def toPythonString(indent: String) = {
+ val condition_variable = "_condition_"
+
+ val indent2 = indent + " "
+ val basic_range = "xrange("+lower_range+", 1 + "+upper_range+")"
+ val vs = vl match {
+ case v::Nil => "("+varsToString(vl)+",)"
+ case _ => varsToString(vl)
+ }
+ val list_ranges = "("+vs+" "+ (vl map { case i => "for "+i.name+" in "+basic_range}).reduceLeft(_ + " " + _) + ")"
+ val exists_construct = "lambda a, "+vs+": a or ("+ condition.toCommonString+" and "+vs+")"
+ val finding_term = "reduce("+exists_construct+", "+list_ranges+", False)"
+ val line_condition = indent + condition_variable+" = "+finding_term
+ val line_if = indent + "if "+condition_variable+":"
+ val line_assign = indent + " " + vs + " = "+condition_variable
+ val prog_string = program.innerCommonContent(indent2)
+ val line_else = indent + "else:"
+ val line_else_prog = indent2 + program.errorResultCommon(RenderingPython)
+ (line_condition::line_if::line_assign::prog_string::line_else::line_else_prog::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ }
+
+ /** Returns a string containing the program in Scala.
+ * APASynthesis.rendering_mode should be set to RenderingScala. */
+ def toScalaString(indent: String) = {
+ val indent2 = indent + " "
+ val basic_range = "(("+lower_range+") to ("+upper_range+"))"
+ var ranges = basic_range
+ vl.tail foreach {k =>
+ ranges = ranges + " flatMap { t => "+basic_range+" map { i => (i, t) } } "
+ }
+ val expanded_vars = varsToString(vl)
+ val find_string = indent + "val " + program.resultCommonContent("") + " = " + ranges + " find { case "+expanded_vars+" => "
+ val cond_string = indent2 + condition.toCommonString
+ val match_string = indent+"} match {"
+ val case_string = indent2+"case Some("+expanded_vars+") => "
+ val prog_string = program.innerCommonContent(indent2)
+ val result_string = program.resultCommonContent(indent2)
+ val error_result = program.errorResultCommon(RenderingScala)
+ val end_string = indent2+"case None => "+error_result+"\n"+indent+"}"
+ (find_string::cond_string::match_string::case_string::prog_string::result_string::end_string::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ }
+
+ /** Returns the result of this program under the provided environment. */
+ def execute(l: Map[InputVar, Int]): Map[OutputVar, Int] = {
+ val lr:Int = lower_range.replaceList(APAAbstractProgram.toAPAInputAssignment(l)) match {
+ case APAInputCombination(k, Nil) => k
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+l)
+ }
+ val ur:Int = upper_range.replaceList(APAAbstractProgram.toAPAInputAssignment(l)) match {
+ case APAInputCombination(k, Nil) => k
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+l)
+ }
+ val basic_range = (lr to ur)
+ def possible_assignments(vl: List[InputVar], i: Int, current_assignment: List[(InputVar, Int)]) : Stream[List[(InputVar, Int)]] = vl match {
+ case Nil => Stream(current_assignment)
+ case (v::q) if i > ur => Stream()
+ case (v::q) => possible_assignments(q, lr, (v, i)::current_assignment) append possible_assignments(vl, i+1, current_assignment)
+ }
+ val assignments = possible_assignments(vl, lr, Nil)
+
+ assignments find { assignments =>
+ condition.execute(l ++ assignments)
+ } match {
+ case Some(assignments) =>
+ program.execute(l ++ assignments)
+ case None => //throw new Error("Could not find a satisfying "+vl+" in ["+lower_range+","+upper_range+"] for "+condition.toScalaString)
+ program.execute(l ++ (vl map { case v => (v -> 0)}))
+ }
+ }
+}
+
+/** Object providing methods to deal with program optimizations. */
+object APAProgram {
+
+ /** The empty program. */
+ def empty:APAProgram = APAProgram(Nil, Nil, APAEmptySplit(), Nil, Nil)
+
+ /** Returns an optimized version of the program described by these arguments.
+ *
+ * @param input_variables The input variables this program needs to run.
+ * @param input_assignment The input assignments defining new input variables this program needs to run.
+ * @param case_splits An eventual split among conditions.
+ * @param output_assignment The output assignements defining the output variables this program needs to compute.
+ * @param output_variables The output variables this program needs to compute.
+ */
+ def optimized(input_variables: List[InputVar],
+ input_assignment: List[InputAssignment],
+ case_splits: APASplit,
+ output_assignment: List[(OutputVar, APATerm)],
+ output_variables: List[OutputVar]):APAProgram = {
+ val final_output_variables = output_variables
+ val interesting_input_variables = (case_splits.input_variables ++ (output_assignment map (_._2) flatMap (_.input_variables))).distinct
+ // Let's propagate assignments that are temporary
+ val (reduced_input_assignments, reduced_output_assignments) = APAAbstractProgram.propagation_delete_temp(input_assignment, output_assignment, Nil, Nil, interesting_input_variables, output_variables)
+ APAProgram(input_variables, reduced_input_assignments, case_splits, reduced_output_assignments, output_variables)
+ }
+
+ /** Merges several conditions/programs together, which the help of case splits if needed.
+ *
+ * @param input_variables The general list of input variables all these programs need.
+ * @param output_variables The general list of output variables all these programs need.
+ * @param programs_conditions A list of pairs (conditions, programs) which needs to be merged.
+ */
+ def merge_disjunction(input_variables : List[InputVar],
+ output_variables: List[OutputVar],
+ programs_conditions: List[(APACondition, APAProgram)]): (APACondition, APAProgram) = {
+ //Adds the global precondition the disjunction fo the case split conditions.
+ val programs_conditions_filtered = programs_conditions filterNot (_._1.global_condition == APAFalse())
+ programs_conditions_filtered find { case (c, p) => c.isTrivial() } match {
+ case Some(complete_program) => complete_program
+ case None =>
+ programs_conditions_filtered match {
+ case Nil => (APACondition.False, APAProgram.empty)
+ case a::Nil => a
+ case _ =>
+ val splitted_conditions:List[APACondition] = programs_conditions_filtered map (_._1)
+ val splitted_formulas:List[APAFormula] = splitted_conditions map (_.global_condition)
+ val final_precondition = APACaseSplitCondition(splitted_conditions).toCondition
+ val final_program = APACaseSplit(programs_conditions_filtered).toProgram
+ (final_precondition, final_program)
+ }
+ }
+ }
+
+ /** Returns a string representing the given output assignment. */
+ def outputAssignmentToString(variable: OutputVar, value: APATerm):String = {
+ APASynthesis.rendering_mode match {
+ case RenderingScala => "val "+ variable.name + " = " + value.toCommonString
+ case RenderingPython => variable.name + " = " + value.toCommonString
+ }
+ }
+}
+
+/** Class representing the top-level program
+ * Contains the a definition of the needed input variables and required output variables.
+ *
+ * def progname(A: Int, ... input variables) {
+ * input assignments val k = ...
+ * case splits if ... else ...
+ * output assignments val x = ... a ...
+ * (output variables) (x, ...)
+ * }
+ *
+ * @param input_variables The input variables this program needs to run.
+ * @param input_assignment The input assignments defining new input variables this program needs to run.
+ * @param case_splits An eventual split among conditions.
+ * @param output_assignment The output assignements defining the output variables this program needs to compute.
+ * @param output_variables The output variables this program needs to compute.
+ */
+case class APAProgram(input_variables: List[InputVar],
+ input_assignment: List[InputAssignment],
+ case_splits: APASplit,
+ output_assignment: List[(OutputVar, APATerm)],
+ output_variables: List[OutputVar]) extends APAAbstractProgram {
+ var name="result"
+
+ /** Changes the name of this program
+ * Used when the program is rendered as a named function. */
+ def setName(new_name: String) = name = new_name
+
+ /** Returns a string representing this program. */
+ override def toString = toCommonString(" ")
+
+ /** Returns a string representing this program, depending on the rendering mode APASynthesis.rendering_mode. */
+ def toCommonString(indent: String): String = APASynthesis.rendering_mode match {
+ case RenderingScala => toScalaString(indent)
+ case RenderingPython => toPythonString(indent)
+ }
+
+ /** Returns a string representing the content of the function described by this program.
+ * Namely, the input assignments, the case split and the output assignments. */
+ def innerCommonContent(indent: String): String = {
+ val prog_input = InputAssignment.listToCommonString(input_assignment, indent)
+ val prog_case_split = case_splits.toCommonString(indent)
+ val prog_output = output_assignment map {
+ case (i, t) => indent + APAProgram.outputAssignmentToString(i, t)
+ } match {
+ case Nil => ""
+ case l => l reduceLeft (APAAbstractProgram.combineSentences(_, _))
+ }
+ (prog_input::prog_case_split::prog_output::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ }
+
+ /** Returns a string representing the result of the function described by this program,
+ * like "(x, y, z)" where x, y, z are the output variables of this program. */
+ def resultCommonContent(indent:String):String = {
+ indent+(output_variables match {
+ case Nil => "()"
+ case (a::Nil) => a.name
+ case l => "(" + (l map (_.name) sortWith {_ < _} reduceLeft (_+", "+_)) + ")"
+ })
+ }
+
+ /** Returns a string containing a default value when there is an error,
+ * depending on the programming language used APASynthesis.rendering_mode. */
+ def errorResultCommon(rm: RenderingMode): String = {
+ APASynthesis.rendering_mode match {
+ case RenderingPython => errorResultPython(rm)
+ case RenderingScala => errorResultScala(rm)
+ }
+ }
+
+ /** Returns a string containing a default value when there is an error, in Scala. */
+ def errorResultScala(rm: RenderingMode): String = {
+ if(APASynthesis.run_time_checks) {
+ rm.error_string
+ } else {
+ output_variables match {
+ case Nil => "()"
+ case (a::Nil) => "0"
+ case l => "("+(l map { _ => "0"} reduceLeft(_ + ", " + _))+")"
+ }
+ }
+ }
+
+ /** Returns a string containing a default value when there is an error, in Python. */
+ def errorResultPython(rm: RenderingMode): String = {
+ if(APASynthesis.run_time_checks) {
+ rm.error_string
+ } else {
+ output_variables match {
+ case Nil => "()"
+ case (a::Nil) => a.name + " = 0"
+ case l => "("+(l map (_.name ) reduceLeft (_ + ", " + _)) + ") = (" + (l map { _ => "0"} reduceLeft (_ + ", " + _)) + ")"
+ }
+ }
+ }
+
+ /** Returns a string containing the input variables in argument of the function.
+ * depending on the programming language used APASynthesis.rendering_mode.*/
+ def inputCommonContent:String = APASynthesis.rendering_mode match {
+ case RenderingScala => inputScalaContent
+ case RenderingPython => inputPythonContent
+ }
+
+ /** Returns a string containing the input variables in argument of the function, in Scala. */
+ def inputScalaContent:String = input_variables match {
+ case Nil => ""
+ case l => (input_variables map (_.name + " : Int") reduceLeft (_+", "+_))
+ }
+
+ /** Returns a string containing the input variables in argument of the function, in Python. */
+ def inputPythonContent:String = input_variables match {
+ case Nil => ""
+ case l => (input_variables map (_.name) reduceLeft (_+", "+_))
+ }
+
+ /** Returns a string containing the whole program in Python. */
+ def toPythonString(indent: String):String = {
+ val function_definition = "def "+name+"("+inputCommonContent+"):"
+ val inner_content = innerCommonContent(indent)
+ val result = indent + "return " + resultCommonContent("")
+ (function_definition::inner_content::result::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ }
+
+ /** Returns a string containing the whole program in Scala. */
+ def toScalaString(indent: String):String = {
+ val return_type = output_variables match {
+ case Nil => "()"
+ case (a::Nil) => "Int"
+ case l => "("+(l map {_=>"Int"} reduceLeft (_ + ", " + _)) +")"
+ }
+ val function_definition = "def "+name+"("+inputCommonContent+"):" + return_type + " = {"
+ val inner_content= innerCommonContent(indent)
+ val result = resultCommonContent(indent)
+ var prog = function_definition
+ (function_definition::inner_content::result::"}"::Nil).reduceLeft(APAAbstractProgram.combineSentences(_, _))
+ }
+
+ /** Returns the values this program generates with the input l. */
+ def execute(l: Map[InputVar, Int]): Map[OutputVar, Int] = {
+ var input_value_map = l
+ input_assignment foreach {
+ case SingleInputAssignment(v, t) => val input_value_assignment = APAAbstractProgram.toAPAInputAssignment(input_value_map)
+ t.replaceList(input_value_assignment) match {
+ case APAInputCombination(i, Nil) => input_value_map += (v -> i)
+ case t =>
+ throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+input_value_map)
+ }
+ case BezoutInputAssignment(vl, tl) => val input_value_assignment = APAAbstractProgram.toAPAInputAssignment(input_value_map)
+ val bezout_coefs:List[Int] = tl map (_.replaceList(input_value_assignment)) map {
+ case APAInputCombination(i, Nil) => i
+ case t => throw new Exception("Was not able to reduce term "+t+" to integer under the mapping "+input_value_map)
+ }
+ // Double zip and add all assignments to variables
+ (vl zip Common.bezoutWithBase(1, bezout_coefs)) map { case (l1, l2) => l1 zip l2 } foreach { _ foreach { input_value_map += _ } }
+ }
+ var output_value_map = case_splits.execute(input_value_map)
+ val input_assignments_listed = APAAbstractProgram.toAPAInputAssignment(input_value_map)
+ output_assignment foreach {
+ case (v, t) =>
+ t.replaceListInput(input_assignments_listed).replaceList(APAAbstractProgram.toAPAOutputAssignment(output_value_map)) match {
+ case APACombination(APAInputCombination(i, Nil), Nil) => output_value_map += (v -> i)
+ case g =>
+ throw new Exception("Was not able to reduce term to integer : "+t+"\nunder the mappings "+input_value_map+" and "+output_value_map+"\nGot : "+g)
+ }
+ }
+ Map[OutputVar, Int]() ++ (output_variables map {case v => (v, (output_value_map(v)))})
+ }
+}
+
diff --git a/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala b/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala
new file mode 100644
index 000000000..ab146ebaf
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala
@@ -0,0 +1,678 @@
+package leon.synthesis.comfusy
+
+/*****************************
+ * Abstract syntax tree *
+ *****************************/
+
+// dummy
+object APASyntaxTree
+
+/** Describes the concept of a variable. */
+trait APAVariable
+
+/** A class which can be converted to a linear combination. */
+trait ConvertibleToCombination {
+
+ /** Returns the corresponding linear combination equivalent to this expression. */
+ implicit def toCombination():APACombination
+}
+
+/** Class representing an output variable, with some syntactic sugar. */
+case class OutputVar(name: String) extends APAVariable with ConvertibleToCombination {
+ def toCombination():APACombination = APACombination(this)
+
+ /** Syntactic sugar */
+ /** Returns the addition of this variable with a linear combination. */
+ def +(pac : APACombination) = pac+APACombination(this)
+
+ /** Returns the addition of this variable with an input variable. */
+ def +(v : InputVar) = APAInputCombination(v)+APACombination(this)
+
+ /** Returns the addition of this variable with another output variable. */
+ def +(v : OutputVar) = APACombination(v)+APACombination(this)
+
+ /** Returns the multiplication of this variable by an integer. */
+ def *(i : Int) = APACombination(i, this)
+
+ /** Returns the multiplication of this variable by an input variable. */
+ def *(i : InputVar):APACombination = APACombination(APAInputCombination(0, Nil), (APAInputCombination(0, (1, i)::Nil), this)::Nil)
+}
+
+/** Abstract class describing an expression. Almost everything is an expression, except variables.
+ * Methods to convert or extract are regrouped here.
+ */
+abstract sealed class APAExpression {
+
+ /** Returns the list of output variables this expression contains. */
+ def output_variables:List[OutputVar] = this match {
+ case APACombination(c, o) => o map (_._2)
+ case APADivides(c, pac) => pac.output_variables
+ case APAEqualZero(pac) => pac.output_variables
+ case APAGreaterZero(pac) => pac.output_variables
+ case APAGreaterEqZero(pac) => pac.output_variables
+ case APATrue() => Nil
+ case APAFalse() => Nil
+ case APADivision(pac, n) => pac.output_variables
+ case APADisjunction(l) => (l flatMap (_.output_variables)).distinct
+ case APAConjunction(l) => (l flatMap (_.output_variables)).distinct
+ case APAMinimum(l) => (l flatMap (_.output_variables)).distinct
+ case APAMaximum(l) => (l flatMap (_.output_variables)).distinct
+ case APANegation(e)=> e.output_variables
+ }
+
+ /** Returns the list of input variables this expression contains. */
+ def input_variables:List[InputVar] = this match {
+ case APACombination(c, o) => (c.input_variables ++ ((o map (_._1)) flatMap (_.input_variables))).distinct
+ case APADivides(c, pac) => (pac.input_variables ++ c.input_variables).distinct
+ case APAEqualZero(pac) => pac.input_variables
+ case APAGreaterZero(pac) => pac.input_variables
+ case APAGreaterEqZero(pac) => pac.input_variables
+ case APATrue() => Nil
+ case APAFalse() => Nil
+ case APADivision(pac, c) => (pac.input_variables ++ c.input_variables).distinct
+ case APADisjunction(l) => (l flatMap (_.input_variables)).distinct
+ case APAConjunction(l) => (l flatMap (_.input_variables)).distinct
+ case APAMinimum(l) => (l flatMap (_.input_variables)).distinct
+ case APAMaximum(l) => (l flatMap (_.input_variables)).distinct
+ case APANegation(e)=> e.input_variables
+ }
+
+ /** Returns a boolean indicating if the number of output variables is at least 1. */
+ def has_output_variables: Boolean = (output_variables != Nil) //OptimizeMe!
+
+ /** Returns a simplified version of this expression. */
+ def simplified: APAExpression
+
+ /** Returns a version of this expression where all occurences of y have been replaced by the linear combination t. */
+ def replace(y: OutputVar, t: APACombination): APAExpression
+
+ /** Returns a string representing this expression. */
+ override def toString = toCommonString
+
+ /** Returns a string representing this expression. Alias for toString. */
+ def toCommonString: String = toStringGeneral(APASynthesis.rendering_mode)
+
+ /** Returns a string representing this expression, depending on the rendering mode rm.*/
+ def toStringGeneral(rm: RenderingMode) = this match {
+ case APADivides(n, pac) =>
+ val pac_s = pac.toNiceString
+ if(APASynthesis.advanced_modulo && APASynthesis.rendering_mode != RenderingPython) {
+ val string_pac = (if(((pac_s indexOf '-') >= 0) || ((pac_s indexOf '+') >= 0))
+ "("+ pac_s + ")"
+ else
+ pac_s)
+ val advanced_divisibility = rm.mod_function(string_pac, n.toString) + " == 0"
+ advanced_divisibility
+ } else {
+ val basic_divisibility = (if(((pac_s indexOf '-') >= 0) || ((pac_s indexOf '+') >= 0))
+ ("("+ pac_s + ") % " + n + " == 0")
+ else
+ (pac_s + " % " + n + " == 0"))
+ val zero_divisibility = pac_s + " == 0"
+ n match {
+ case n if n.isZero =>
+ zero_divisibility
+ case n if n.isPositive =>
+ basic_divisibility
+ case _ =>
+ "(("+n+"==0 "+rm.and_symbol+" "+zero_divisibility+") "+rm.or_symbol+" ("+n+"!=0 "+rm.and_symbol+" "+basic_divisibility+"))"
+ }
+ }
+ case APAEqualZero(pac) => pac.toString + " == 0"
+ case APAGreaterZero(pac) => pac.toString + " > 0"
+ case APAGreaterEqZero(pac) => pac.toString + " >= 0"
+ case APADivision(numerator, denominator) =>
+ var string_numerator = numerator.toString
+ var string_denominator = denominator.toString
+ if((string_numerator indexOf '-') >=0 || (string_numerator indexOf '+') >=0)
+ string_numerator = "("+string_numerator+")"
+ if((string_denominator indexOf '-') >=0 || (string_denominator indexOf '+') >=0 || (string_denominator indexOf '*') >=0 || (string_denominator indexOf '/') >=0)
+ string_denominator = "("+string_denominator+")"
+ if(APASynthesis.rendering_mode == RenderingPython) // Python is cool : (-2)/3 = -1
+ string_numerator+"/" + string_denominator
+ else {
+ numerator match {
+ case APACombination(i, Nil) if i.isPositiveZero =>
+ string_numerator+"/" + string_denominator
+ case _ => "("+ string_numerator + " - " + rm.mod_function(string_numerator, string_denominator) +")/" + string_denominator
+ }
+ }
+ case APAMinimum(l) => rm.min_symbol + "(" + (l map (_.toString) reduceLeft(_ + ", " + _)) + ")"
+ case APAMaximum(l) => rm.max_symbol + "(" + (l map (_.toString) reduceLeft(_ + ", " + _)) + ")"
+ case pac@APACombination(_, _) => pac.toNiceString
+ case APATrue() => rm.true_symbol
+ case APAFalse() => rm.false_symbol
+ case APAConjunction(eqs) => eqs match {
+ case Nil => rm.true_symbol
+ case (a::Nil) => a.toString
+ case l => l map (_ match {
+ case t if t.isInstanceOf[APAEquation] => t.toString
+ case pac@APAConjunction(_) => pac.toString
+ case t => "("+t.toString+")"
+ }
+ ) reduceLeft (_+ " "+rm.and_symbol+" " + _)
+ }
+ case APADisjunction(eqs) => eqs match {
+ case Nil => rm.false_symbol
+ case (a::Nil) => a.toString
+ case l => l map (_ match {
+ case t if t.isInstanceOf[APAEquation] => t.toString
+ case pac@APADisjunction(_) => pac.toString
+ case t => "("+t.toString+")"
+ }
+ ) reduceLeft (_+ " "+rm.or_symbol+" " + _)
+ }
+ case APANegation(eq) => rm.not_symbol+"("+eq.toString+")"
+ }
+
+ /** Returns a string representing this expression, in Scala. */
+ def toScalaString = {
+ toStringGeneral(RenderingScala)
+ }
+
+ /** Returns a string representing this expression, in Python. */
+ def toPythonString = {
+ toStringGeneral(RenderingPython)
+ }
+
+ /** Method to assume signs of input terms.
+ *
+ * To assume all occurences of the variable b to be >= 0 in myterm, call :
+ * myterm.assumeSignInputTerm(InputVar("b").toInputTerm, ASign(1, 1, 0))
+ * To assume all occurences of the variable b to be <= 0 in myterm, call :
+ * myterm.assumeSignInputTerm(InputVar("b").toInputTerm, ASign(0, 1, 1))
+ */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAExpression
+}
+
+/** Class representing formulas.
+ * A formula is an expression, which when evaluated, gives a boolean indicating if the formula is true or false.
+ */
+abstract sealed class APAFormula extends APAExpression {
+
+ /** Returns a version of this formula where all occurences of the input variable y have been replaced by the input term t. */
+ def replace(y: InputVar, t: APAInputTerm): APAFormula
+
+ /** Returns a version of this formula where all occurences of the output variable y have been replaced by the linear combination t. */
+ def replace(y: OutputVar, t: APACombination): APAFormula
+
+ /** Processes multiple replacements of input variables. */
+ def replaceListInput(lxt : List[(InputVar, APAInputTerm)]): APAFormula = {
+ lxt.foldLeft(this){ case (result, (x, t)) => result.replace(x, t) }
+ }
+
+ /** Processes multiple replacements of output variables. */
+ def replaceList(lxt : List[(OutputVar, APACombination)]): APAFormula = {
+ lxt.foldLeft(this){ case (result, (x, t)) => result.replace(x, t) }
+ }
+
+ /** Returns a simplified version of this formula. */
+ def simplified: APAFormula = this match {
+ case APAConjunction(eqs) => val eqs_simplified = eqs map (_.simplified)
+ eqs_simplified match {
+ case Nil => APATrue()
+ case l if l contains APAFalse() => APAFalse()
+ case l => l filterNot (_ == APATrue()) match {
+ case Nil => APATrue()
+ case (a::Nil) => a
+ case l => APAConjunction(l)
+ }
+ }
+ case APADisjunction(eqs) => eqs map (_.simplified) match {
+ case Nil => APAFalse()
+ case l if l contains APATrue() => APATrue()
+ case l => l filterNot (_ == APAFalse()) match {
+ case Nil => APAFalse()
+ case (a::Nil) => a
+ case l => APADisjunction(l)
+ }
+ }
+ case APANegation(f) => f.simplified match {
+ case APATrue() => APAFalse()
+ case APAFalse() => APATrue()
+ case l => APANegation(l)
+ }
+ // This matching IS exhaustive since this method is overriden in other child classes.
+ case t:APAFormula => throw new Error("formulas should have been simplified : "+this)
+ }
+
+ /** Returns the conjunction of this and that formulas. */
+ def &&(that : APAFormula) = APAConjunction(this::that::Nil).simplified
+
+ /** Returns the disjunction of this and that formulas. */
+ def ||(that : APAFormula) = APADisjunction(this::that::Nil).simplified
+
+ /** Get a stream of the DNF form of the formula. */
+ def getEquations = getEquations_tailrec(Nil)
+
+ /** Get a stream of the DNF form of the formula. Recursive version. */
+ def getEquations_tailrec(currentList: List[APAEquation]) : Stream[List[APAEquation]] = this match {
+ case t@APADivides(_, _) => Stream(currentList++List(t))
+ case t@APAEqualZero(_) => Stream(currentList++List(t))
+ case t@APAGreaterZero(_) => Stream(currentList++List(t))
+ case t@APAGreaterEqZero(_) => Stream(currentList++List(t))
+ case APAConjunction(Nil) => Stream(currentList)
+ case APAConjunction(a::Nil) =>
+ a.getEquations_tailrec(currentList)
+ case APAConjunction(a::q) =>
+ val p1 = a.getEquations_tailrec(currentList)
+ val p2 = APAConjunction(q).getEquations_tailrec(Nil)
+ (p1, p2)
+ val pp = (p1 map { eqs1 => p2 map { eqs2 => eqs1 ++ eqs2} })
+ val result = pp.foldLeft(Stream.empty:Stream[List[APAEquation]])(_.append(_))
+ result
+ case APADisjunction(Nil) => Stream(List(APAFalse()))
+ case APADisjunction(a::Nil) => a.getEquations_tailrec(currentList)
+ case APADisjunction(a::q) => a.getEquations_tailrec(currentList) append APADisjunction(q).getEquations_tailrec(currentList)
+ case APATrue() => Stream(currentList)
+ case APAFalse() => Stream(List(APAFalse()))
+ case APANegation(f) => throw new Error("Negation is not supported yet")
+ }
+
+ /** Gets a stream of immediate equalities and inequalities if there are some + the rest as a stream. of possibilities. */
+ def getLazyEquations = getLazyEquations_tailrec
+
+ /** Gets a stream of immediate equalities and inequalities if there are some + the rest as a stream. of possibilities. Recursive version. */
+ def getLazyEquations_tailrec: FormulaSplit = this match {
+ case t@APADivides(_, _) => FormulaSplit(Nil, List(t), Stream.empty)
+ case t@APAEqualZero(_) => FormulaSplit(t::Nil, Nil, Stream.empty)
+ case t@APAGreaterZero(_) => FormulaSplit(Nil, List(t), Stream.empty)
+ case t@APAGreaterEqZero(_) => FormulaSplit(Nil, List(t), Stream.empty)
+ case APAConjunction(Nil) => APATrue().getLazyEquations_tailrec
+ case APAConjunction(a::Nil) => a.getLazyEquations_tailrec
+ case APAConjunction(l) => l map (_.getLazyEquations_tailrec) reduceLeft (FormulaSplit.conjunction(_,_))
+ case APADisjunction(Nil) => APAFalse().getLazyEquations_tailrec
+ case APADisjunction(a::Nil) => a.getLazyEquations_tailrec
+ case APADisjunction(l) => FormulaSplit(Nil, Nil, l.toStream map (_.getLazyEquations_tailrec))
+ case APATrue() => FormulaSplit(Nil, Nil, Stream.empty)
+ case APAFalse() => FormulaSplit(Nil, APAFalse()::Nil, Stream.empty)
+ case APANegation(f) => throw new Error("Negation is not supported yet")
+ }
+
+ /** Assumes the sign of the input term t1 throughout the formula. */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAFormula
+}
+
+/** Object providing methods for the class FormulaSplit.
+ */
+object FormulaSplit {
+
+ /** Returns the conjunction of two FormulaSplit. */
+ def conjunction(f1:FormulaSplit, f2:FormulaSplit):FormulaSplit = (f1, f2) match {
+ case (FormulaSplit(eqs1, ineqs1, rest1), FormulaSplit(eqs2, ineqs2, rest2)) =>
+ FormulaSplit(eqs1++eqs2, ineqs1++ineqs2, disjunction(rest1, rest2))
+ }
+
+ /** Returns the disjunction of two FormulaSplit. */
+ def disjunction(sf1:Stream[FormulaSplit], sf2:Stream[FormulaSplit]):Stream[FormulaSplit] = {
+ if(sf1.isEmpty) sf2
+ else if(sf2.isEmpty) sf1
+ else {
+ sf1 flatMap { f1 => sf2 map { f2 => conjunction(f1, f2)}}
+ }
+ }
+}
+
+/** A FormulaSplit is a formula representing a conjunction of known equalities and inequalities, and a disjunction of other formula splits.
+ * e.g. FormulaSplit(eqs, noneqs, remaining) === (eqs && noneqs && (remaining1 || remaining2 || ...))
+ */
+case class FormulaSplit(eqs: List[APAEqualZero], noneqs : List[APAEquation], remaining:Stream[FormulaSplit]) {
+
+ /** Replaces all output variables by corresponding value in this FormulaSplit. */
+ def replaceList(assignments: List[(OutputVar, APACombination)]): FormulaSplit = {
+ var new_equalities = eqs
+ var new_nonequalities = noneqs
+ assignments foreach {
+ case (v, pac) =>
+ val (new_eqs1, new_noneqs1) = APASynthesis.partitionPAEqualZero(new_equalities map (_.replace(v, pac)))
+ val (new_eqs2, new_noneqs2) = APASynthesis.partitionPAEqualZero(new_nonequalities map (_.replace(v, pac)))
+ new_equalities = new_eqs1 ++ new_eqs2
+ new_nonequalities = new_noneqs1 ++ new_noneqs2
+ }
+ var new_remaining_disjunctions = remaining map (_.replaceList(assignments))
+ FormulaSplit(new_equalities, new_nonequalities, new_remaining_disjunctions)
+ }
+}
+
+/** Abstract class describing atomic equations, or literals, like divide predicates, greater or equal to zero predicates, equal to zero, etc.
+ */
+abstract sealed class APAEquation extends APAFormula {
+
+ /** Returns a simplified version of this equation. */
+ override def simplified: APAEquation = this match {
+ case APADivides(_, APACombination(APAInputCombination(0, Nil), Nil)) => APATrue()
+ case APADivides(APAInputCombination(1, Nil), pac) => APATrue()
+ case APADivides(APAInputCombination(0, Nil), pac) => APAEqualZero(pac.simplified.normalizedForEquality)
+ case APADivides(APAInputCombination(n, Nil), APACombination(APAInputCombination(i, Nil), Nil)) => if((i % n) == 0) APATrue() else APAFalse()
+ case APADivides(n, pac) => APADivides(n, pac.simplified) // OptimizeMe ! divides by gcd of n and pac
+ case APAEqualZero(pac) => APAEqualZero(pac.simplified.normalizedForEquality) match {
+ case APAEqualZero(APACombination(n, Nil)) if n.isZero => APATrue()
+ case APAEqualZero(APACombination(n, Nil)) if n.isNotZero => APAFalse()
+ case t => t
+ }
+ case APAGreaterZero(pac) => APAGreaterZero(pac.simplified.normalized) match {
+ case APAGreaterZero(APACombination(n, Nil)) if n.isPositive => APATrue()
+ case APAGreaterZero(APACombination(n, Nil)) if n.isNotPositive => APAFalse()
+ case t => t
+ }
+ case APAGreaterEqZero(pac) => APAGreaterEqZero(pac.simplified.normalized) match {
+ case APAGreaterEqZero(APACombination(n, Nil)) if n.isPositiveZero =>
+ APATrue()
+ case APAGreaterEqZero(APACombination(n, Nil)) if n.isNotPositiveZero => APAFalse()
+ case APAGreaterEqZero(tn@APACombination(n, Nil)) if n.isNegativeZero => APAEqualZero(tn)
+ case t => t
+ }
+ case APATrue() => APATrue()
+ case APAFalse() => APAFalse()
+ }
+
+ /** Returns a version of this equation where all occurences of the output variable y have been replaced by the term t. */
+ def replace(y: OutputVar, t: APACombination): APAEquation
+
+ /** Returns a version of this equation where each occurence of the input term t1 is assumed to have the sign s. */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation
+}
+
+/** Class representing terms, i.e. expressions that would evaluate to integers when fully evaluated.
+ */
+sealed abstract class APATerm extends APAExpression {
+
+ /** Returns a version of this term where all occurences of the output variable y have been replaced by the term t. */
+ def replace(y: OutputVar, t: APACombination):APATerm
+
+ /** Returns a version of this term where all occurences of the input variable y have been replaced by the input term t. */
+ def replace(y: InputVar, t: APAInputTerm):APATerm
+
+ /** Returns a simplified version of this term. */
+ def simplified:APATerm
+
+ /** Processes multiple replacements of output variables. */
+ def replaceList(lxt : List[(OutputVar, APACombination)]): APATerm = {
+ lxt.foldLeft(this){ case (result, (x, t)) => result.replace(x, t) }
+ }
+
+ /** Processes multiple replacements of input variables. */
+ def replaceListInput(lxt : List[(InputVar, APAInputTerm)]): APATerm = {
+ lxt.foldLeft(this){ case (result, (x, t)) => result.replace(x, t) }
+ }
+
+ /** Returns a version of this term where each occurence of the input term t1 is assumed to have the sign s. */
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APATerm
+}
+
+/*******************
+ * General terms *
+ *******************/
+
+/** Class representing a division of a linear combination by an input term.
+ * It is not required for the denominator to divide the expression.
+ */ // TODO : comment from here.
+case class APADivision(numerator : APACombination, denominator : APAInputTerm) extends APATerm {
+
+ def replace(y: OutputVar, t: APACombination):APATerm = APADivision(numerator.replace(y, t), denominator).simplified
+
+ def replace(y: InputVar, t: APAInputTerm):APATerm = APADivision(numerator.replace(y, t), denominator.replace(y, t)).simplified
+
+ def simplified:APATerm = {
+ val result = (numerator.simplified, denominator) match {
+ case (n, APAInputCombination(1, Nil)) => n
+ case (n, d0@APAInputCombination(0, Nil)) => APADivision(n, d0)
+ case (APACombination(APAInputCombination(n, Nil), Nil), APAInputCombination(d, Nil)) =>
+ APACombination(APAInputCombination((n - (d + (n % d))%d)/d, Nil), Nil)
+ case (n, d) => APADivision(n, d)
+ }
+ result
+ }
+
+
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APATerm = {
+ val new_numerator = numerator.assumeSignInputTerm(t1, s)
+ val new_denominator = denominator.assumeSignInputTerm(t1, s)
+ APADivision(new_numerator, new_denominator).simplified
+ }
+}
+
+case class APAMinimum(expressions: List[APATerm]) extends APATerm {
+ def replace(y: OutputVar, t: APACombination):APATerm = APAMinimum(expressions map (_.replace(y, t))).simplified
+ def replace(y: InputVar, t: APAInputTerm):APATerm = APAMinimum(expressions map (_.replace(y, t))).simplified
+ def simplified:APATerm = expressions match {
+ case Nil => APACombination(0)
+ case a::Nil => a.simplified
+ case a::b::q =>
+ (a.simplified, b.simplified) match {
+ case (APACombination(APAInputCombination(i, Nil), Nil), APACombination(APAInputCombination(j, Nil), Nil)) => APAMinimum(APACombination(APAInputCombination(Math.min(i, j), Nil), Nil)::q).simplified //OptimizeMe
+ case (p@APACombination(APAInputCombination(0, Nil), Nil), APACombination(j, Nil)) if j.isPositiveZero => APAMinimum(p::q).simplified //OptimizeMe
+ case (APACombination(APAInputCombination(0, Nil), Nil), p@APACombination(j, Nil)) if j.isNegativeZero => APAMinimum(p::q).simplified //OptimizeMe
+ case (a, b) => APAMinimum(a::b::(q map (_.simplified)))
+ }
+ }
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APATerm = {
+ APAMinimum(expressions map (_.assumeSignInputTerm(t1, s))).simplified
+ }
+}
+case class APAMaximum(expressions: List[APATerm]) extends APATerm {
+ def replace(y: OutputVar, t: APACombination):APATerm = APAMaximum(expressions map (_.replace(y, t))).simplified
+ def replace(y: InputVar, t: APAInputTerm):APATerm = APAMaximum(expressions map (_.replace(y, t))).simplified
+ def simplified:APATerm = expressions match {
+ case Nil => APACombination(0)
+ case a::Nil => a.simplified
+ case a::b::q =>
+ (a.simplified, b.simplified) match {
+ case (APACombination(APAInputCombination(i, Nil), Nil), APACombination(APAInputCombination(j, Nil), Nil)) => APAMaximum(APACombination(APAInputCombination(Math.max(i, j), Nil), Nil)::q).simplified //OptimizeMe
+ case (APACombination(APAInputCombination(0, Nil), Nil), p@APACombination(j, Nil)) if j.isPositiveZero => APAMaximum(p::q).simplified //OptimizeMe
+ case (p@APACombination(APAInputCombination(0, Nil), Nil), APACombination(j, Nil)) if j.isNegativeZero => APAMaximum(p::q).simplified //OptimizeMe
+ case (a, b) => APAMaximum(a::b::(q map (_.simplified)))
+ }
+ }
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APATerm = {
+ APAMaximum(expressions map (_.assumeSignInputTerm(t1, s))).simplified
+ }
+}
+
+object APACombination {
+ def apply(v: APAVariable):APACombination = this(1, v)
+ def apply(k: Int, v: APAVariable):APACombination= v match {
+ case v@InputVar(n) => APACombination(APAInputCombination(0, (k, v)::Nil), Nil)
+ case v@OutputVar(n) => APACombination(APAInputCombination(0, Nil), (APAInputCombination(k, Nil), v)::Nil)
+ }
+ def apply(i: Int): APACombination = APACombination(APAInputCombination(i, Nil), Nil)
+ def apply(i: APAInputTerm): APACombination = APACombination(i, Nil)
+ def apply(c: Int, i: List[(Int, InputVar)], o: List[(Int, OutputVar)]): APACombination = {
+ APACombination(APAInputCombination(c, i), o map { case (i, v) => (APAInputCombination(i), v)})
+ }
+}
+
+// Const_part does not contain any output variables
+case class APACombination(const_part: APAInputTerm, output_linear: List[(APAInputTerm, OutputVar)]) extends APATerm with CoefficientAbstraction {
+ if(output_linear == Nil) {
+ setNoCoefficients()
+ } else if(output_linear exists { case (i, _) if i.isNotZero => true; case _ => false}) {
+ setNotAllCoefficientsAreZero()
+ }
+ def normalClone():this.type = APACombination(const_part, output_linear).asInstanceOf[this.type]
+ // Sorting functions
+ def by_OutputVar_name(i1:(APAInputTerm, OutputVar), i2:(APAInputTerm, OutputVar)) : Boolean = (i1, i2) match {
+ case ((_, OutputVar(name1)), (_, OutputVar(name2))) => name1 < name2
+ }
+ // Regrouping functions
+ def fold_Outputvar_name(i:(APAInputTerm, OutputVar), regrouped_vars:List[(APAInputTerm, OutputVar)]):List[(APAInputTerm, OutputVar)] = (i, regrouped_vars) match {
+ case (i, Nil) => i::Nil
+ case ((coef1, OutputVar(name1)), (coef2, OutputVar(name2))::q) if name1 == name2 => (coef1 + coef2, OutputVar(name1))::q
+ case (i, q) => i::q
+ }
+
+ /** Simplified means that the variables are alphabetically sorted, that there are no null coefficients, and the gcd of all coefficients is 1. */
+ def simplified: APACombination = {
+ val output_linear2 = (output_linear sortWith by_OutputVar_name).foldRight[List[(APAInputTerm, OutputVar)]](Nil){ case (a, b) => fold_Outputvar_name(a, b)}
+ APACombination(const_part.simplified, output_linear2 filterNot (_._1.isZero)).propagateCoefficientAbstraction(this)
+ }
+
+ // Normalized means that we are within an equality or inequality
+ // It should have been simplified before (without 0-coefs)
+ def normalized_aux(for_equality: Boolean): APACombination = {
+ const_part match {
+ case t:APAInputCombination if t.has_gcd_coefs =>
+ var coefs:List[Int] = Nil
+ ((output_linear forall {
+ case (t@APAInputCombination(i, Nil), _) =>
+ coefs = i::coefs
+ true
+ case _ => false
+ }), output_linear.isEmpty) match {
+ case (true, false) =>
+ val gcd = Common.gcd(t.gcd_coefs, Common.gcdlist(coefs))
+ (this/gcd).propagateCoefficientAbstraction(this)
+ case (true, true) =>
+ val gcd = t.gcd_coefs
+ val factor = (if(for_equality) t.first_sign_present*gcd else gcd)
+ (this/factor)
+ case (false, _) => this
+ }
+ case _=> this
+ }
+ }
+ def normalized = normalized_aux(false)
+ def normalizedForEquality = normalized_aux(true)
+
+ /** Division of this combination by an integer. Caution ! It should be divisible. */
+ def /(i : Int): APACombination = {
+ APACombination(const_part / APAInputCombination(i), output_linear map {t => (t._1 / APAInputCombination(i), t._2)})
+ }
+ /** Division of this combination by an integer. Caution ! It should be divisible. */
+ def /(i : APAInputTerm): APACombination = {
+ APACombination(const_part / i, output_linear map {t => (t._1 / i, t._2)})
+ }
+ /** Multiplication by an integer */
+ def *(i : Int): APACombination = {
+ val result = APACombination(const_part * APAInputCombination(i), output_linear map {t => (t._1 * APAInputCombination(i), t._2)})
+ result.assumeMultCoefficientAbstraction(this, i)
+ }
+ /** Multiplication by an APAInputTerm */
+ def *(i : APAInputTerm): APACombination = {
+ APACombination(const_part * i, output_linear map {t => (t._1 * i, t._2)})
+ }
+ /** Addition between two combinations */
+ def +(pac : APACombination): APACombination = pac match {
+ case APACombination(c, o) =>
+ val result = APACombination(const_part + c, output_linear ++ o).simplified
+ result.assumeSumCoefficientAbstraction(this, pac)
+ }
+ /** Substraction between two combinations */
+ def -(that : APACombination): APACombination = this + (that * (-1))
+ /** Addition with a new variable and its coefficient */
+ def +(kv : (APAInputTerm, OutputVar)): APACombination = this + APACombination(APAInputCombination(0, Nil), kv::Nil)
+ def +(k : APAInputTerm): APACombination = this + APACombination(k, Nil)
+ /** Substraction with a new variable and its coefficient */
+ def -(kv : (APAInputTerm, OutputVar)): APACombination = this - APACombination(APAInputCombination(0, Nil), kv::Nil)
+ def -(k : APAInputTerm): APACombination = this + APACombination(-k, Nil)
+ def unary_-(): APACombination = (APACombination(APAInputCombination(0, Nil), Nil) - this)
+ /** Comparison */
+ def ===(that: APACombination):APAEquation = APAEqualZero(this - that).simplified
+ def >= (that: APACombination):APAEquation = APAGreaterEqZero(this - that).simplified
+ def > (that: APACombination):APAEquation = APAGreaterZero(this - that).simplified
+ def <= (that: APACombination):APAEquation = APAGreaterEqZero((-this) + that).simplified
+ def < (that: APACombination):APAEquation = APAGreaterZero((-this) + that).simplified
+ def ===(that: APAInputTerm):APAEquation = this === APACombination(that)
+ def >= (that: APAInputTerm):APAEquation = this >= APACombination(that)
+ def > (that: APAInputTerm):APAEquation = this > APACombination(that)
+ def <= (that: APAInputTerm):APAEquation = this <= APACombination(that)
+ def < (that: APAInputTerm):APAEquation = this < APACombination(that)
+ def divisible_by(that: APAInputTerm): APAEquation = APADivides(that, this)
+
+ /** Replacement of a variable by another */
+ def replace(y: OutputVar, t: APACombination):APACombination = (y, t) match {
+ case (OutputVar(name), pac_for_y@APACombination(ci2, o2)) =>
+ val (output_linear_with_y, output_linear_without_y) = output_linear partition (_._2 == y)
+ val pac_without_y = APACombination(const_part, output_linear_without_y)
+ val total_y_coefficient = (output_linear_with_y map (_._1)).foldLeft(APAInputCombination(0, Nil):APAInputTerm)(_+_)
+ val result = pac_without_y + (pac_for_y*total_y_coefficient)
+ result.simplified
+ }
+ def replace(y: InputVar, t: APAInputTerm):APACombination = {
+ APACombination(const_part.replace(y, t), (output_linear map {case (k, v) => (k.replace(y, t), v)})).simplified
+ }
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APACombination = {
+ val new_const_part = const_part.assumeSignInputTerm(t1, s)
+ val new_output_linear = output_linear map {case (i, v) => (i.assumeSignInputTerm(t1, s).propagateSign(i), v)}
+ APACombination(new_const_part, new_output_linear).propagateCoefficientAbstraction(this)
+ }
+
+ def toNiceString:String = {
+ def outputElementToString(kv : (APAInputTerm, OutputVar)) = kv._1 match {
+ case APAInputCombination(1, Nil) => kv._2.name
+ case APAInputCombination(-1, Nil) => "-" + kv._2.name
+ case APAInputCombination(k, Nil) => k + "*" + kv._2.name
+ case k => "("+ k.toString + ")*" + kv._2.name
+ }
+ def makePlus(l: List[String]):String = l match {
+ case Nil => ""
+ case a::p => val s = makePlus(p)
+ if(s=="") a
+ else if(a=="") s
+ else if(s.charAt(0) == '-')
+ a + s
+ else
+ a + "+" + s
+ }
+ var c_string = const_part.toString
+ if(c_string == "0") c_string = ""
+ var o_string = output_linear match {
+ case Nil => ""
+ case a::l => l.foldLeft(outputElementToString(a)) { (s, t2) =>
+ val t2s = outputElementToString(t2)
+ s + (if(t2s.charAt(0) =='-') t2s else "+" + t2s)}
+ }
+ val s = makePlus(c_string::o_string::Nil)
+ if(s == "") "0" else s
+ }
+}
+
+case class APADivides (coefficient: APAInputTerm, pac: APACombination) extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APADivides(coefficient, pac.replace(y, t)).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APADivides(coefficient.replace(y, t), pac.replace(y, t)).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APADivides(coefficient.assumeSignInputTerm(t1, s), pac.assumeSignInputTerm(t1, s)).simplified
+}
+case class APAEqualZero (pac: APACombination) extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APAEqualZero(pac.replace(y, t)).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APAEqualZero(pac.replace(y, t)).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APAEqualZero(pac.assumeSignInputTerm(t1, s)).simplified
+}
+case class APAGreaterZero (pac: APACombination) extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APAGreaterZero(pac.replace(y, t)).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APAGreaterZero(pac.replace(y, t)).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APAGreaterZero(pac.assumeSignInputTerm(t1, s)).simplified
+}
+case class APAGreaterEqZero(pac: APACombination) extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APAGreaterEqZero(pac.replace(y, t)).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APAGreaterEqZero(pac.replace(y, t)).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APAGreaterEqZero(pac.assumeSignInputTerm(t1, s)).simplified
+}
+case class APATrue() extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APATrue()
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APATrue()
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APATrue()
+}
+case class APAFalse() extends APAEquation {
+ override def replace(y: OutputVar, t: APACombination): APAEquation = APAFalse()
+ override def replace(y: InputVar, t: APAInputTerm): APAEquation = APAFalse()
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAEquation = APAFalse()
+}
+
+case class APAConjunction(eqs : List[APAFormula]) extends APAFormula {
+ override def replace(y: OutputVar, t: APACombination): APAFormula = APAConjunction(eqs map (_.replace(y, t))).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAFormula = APAConjunction(eqs map (_.replace(y, t))).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAFormula =
+ APAConjunction(eqs map (_.assumeSignInputTerm(t1, s))).simplified
+}
+case class APADisjunction(eqs : List[APAFormula]) extends APAFormula {
+ override def replace(y: OutputVar, t: APACombination): APAFormula = APADisjunction(eqs map (_.replace(y, t))).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAFormula = APADisjunction(eqs map (_.replace(y, t))).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAFormula =
+ APADisjunction(eqs map (_.assumeSignInputTerm(t1, s))).simplified
+}
+case class APANegation(eq: APAFormula) extends APAFormula {
+ override def replace(y: OutputVar, t: APACombination): APAFormula = APANegation(eq.replace(y, t)).simplified
+ override def replace(y: InputVar, t: APAInputTerm): APAFormula = APANegation(eq.replace(y, t)).simplified
+ def assumeSignInputTerm(t1: APAInputTerm, s: SignAbstraction):APAFormula =
+ APANegation(eq.assumeSignInputTerm(t1, s)).simplified
+}
diff --git a/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala b/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala
new file mode 100644
index 000000000..124d9807f
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala
@@ -0,0 +1,806 @@
+package leon.synthesis.comfusy
+//import scala.annotation.tailrec
+
+//*********************************** Pressburger Synthesis ************************************************//
+
+sealed abstract class RenderingMode {
+ val true_symbol:String
+ val false_symbol:String
+ val and_symbol: String
+ val or_symbol:String
+ val not_symbol:String
+ val min_symbol: String
+ val max_symbol: String
+ val error_string: String
+ val abs_symbol: String
+ val gcd_symbol: String
+ val lcm_symbol: String
+ def mod_function(operand: String, divisor: String): String
+}
+
+case object RenderingScala extends RenderingMode {
+ val (true_symbol, false_symbol, and_symbol, or_symbol, not_symbol, min_symbol, max_symbol, error_string) =
+ ("true", "false", "&&", "||", "!", "Math.min", "Math.max", "throw new Error(\"No solution exists\")")
+ val (abs_symbol, gcd_symbol, lcm_symbol) = ("Math.abs", "Common.gcdlist", "Common.lcmlist")
+ def mod_function(string_numerator: String, denominator: String): String = {
+ if(APASynthesis.advanced_modulo)
+ string_numerator+"%%"+denominator
+ else
+ "("+denominator+" + "+string_numerator+"%"+denominator+")%"+denominator
+
+ }
+}
+
+case object RenderingPython extends RenderingMode {
+ val (true_symbol, false_symbol, and_symbol, or_symbol, not_symbol, min_symbol, max_symbol, error_string) =
+ ("True", "False", "and", "or", "not", "min", "max", "raise Exception(\"No solution exists\")")
+ val (abs_symbol, gcd_symbol, lcm_symbol) = ("abs", "gcd", "lcm")
+ def mod_function(operand: String, divisor: String): String = {
+ operand+"%" + divisor
+ }
+}
+
+object APASynthesis {
+ /* ************* Synthesis options *************** */
+ /** Rendering expressions of the form a %% b where a %% 0 == a, and else (k %% b) is always between 0 and b-1 and congruent to k modulo b. */
+ var advanced_modulo = false
+
+ /** To turn off run-time checks : if true, the "throw new Error" are replaced by tuples filled with zeros. */
+ var run_time_checks = false
+
+ /** top-level rendering mode for toString */
+ var rendering_mode:RenderingMode = RenderingScala
+
+ // ************* Different ways of specifying solving conditions ***************/** */
+
+ /** Returns all output variables in the given list of equations */
+ def getOutputVariables(eqs: List[APAEquation]):List[OutputVar] = {
+ (eqs flatMap (_.output_variables)).distinct
+ }
+
+ /** Solve the equations in a lazy way */
+ def solveLazyEquations(input_variables: List[InputVar], output_variables: List[OutputVar], eqslazy: FormulaSplit):(APACondition, APAProgram) = {
+ return (new APASynthesis(eqslazy, input_variables, output_variables)).solve()
+ }
+
+ def solveLazyEquations(name: String, output_variables: List[OutputVar], eqs: APAFormula):(APACondition, APAProgram) = {
+ val input_variables = eqs.input_variables
+ var (cond, prog) = (new APASynthesis(eqs.getLazyEquations, input_variables, output_variables)).solve()
+ prog.setName(name)
+ (cond, prog)
+ }
+
+ /*def solveEquations(name: String, variables: List[OutputVar], eqs: List[APAEquation]) = {
+ var (cond, prog) = (new APASynthesis(eqs, variables)).solve()
+ prog.setName(name)
+ (cond, prog)
+ }*/
+
+ def solve(name: String, output_variables: List[OutputVar], formula_sequence: APAFormula*):(APACondition, APAProgram) = {
+ val formula = APAConjunction(formula_sequence.toList).simplified
+ //val dnf:Stream[List[APAEquation]] = formula.getEquations
+ //val output_variables = variables
+ //val input_variables = formula.input_variables
+ //val programs_conditions = (dnf map {solveEquations("", output_variables, _)}).toList
+ solveLazyEquations(name, output_variables, formula)
+ }
+ def solve(name: String, formula_sequence: APAFormula*):(APACondition, APAProgram) = {
+ solve(name, formula_sequence.toList)
+ }
+ def solve(name: String, formula_sequence: List[APAFormula]):(APACondition, APAProgram) = {
+ val formula = APAConjunction(formula_sequence.toList).simplified
+ solve(name, formula.output_variables, formula)
+ }
+ def solve(variables:List[OutputVar], formula_sequence: APAFormula*):(APACondition, APAProgram) = {
+ solve(variables, formula_sequence.toList)
+ }
+ def solve(variables:List[OutputVar], formula_sequence: List[APAFormula]):(APACondition, APAProgram) = {
+ val formula = APAConjunction(formula_sequence.toList).simplified
+ solve("result", variables, formula)
+ }
+ def solve(formula_sequence: APAFormula*):(APACondition, APAProgram) = {
+ solve(formula_sequence.toList)
+ }
+ def solve(formula_sequence: List[APAFormula]):(APACondition, APAProgram) = {
+ val formula = APAConjunction(formula_sequence).simplified
+ solve("result", formula.output_variables, formula)
+ }
+
+
+ /** ************* Function used in the algorithm *************** */
+ val alphabet = "abcdefghijklmnopqrstuvwxyz"
+ def newOutputVariable(input_existing: List[InputVar], output_existing : List[OutputVar]): OutputVar = {
+ //var typical = "xyzmnpqrstuvw"
+ var i = 0
+ val names = (input_existing map (_.name)) ++ (output_existing map (_.name))
+ (0 to 25) foreach { i =>
+ val test = "y"+alphabet.substring(i, i+1)
+ if(!(names contains test))
+ return OutputVar(test)
+ }
+ while(names contains ("y"+i)) {
+ i+=1
+ }
+ OutputVar("y"+i)
+ }
+ def newInputVariable(input_existing: List[InputVar], output_existing : List[OutputVar]): InputVar = {
+ var i = 0
+ val names = (input_existing map (_.name)) ++ (output_existing map (_.name))
+ while(names contains ("k"+i)) {
+ i+=1
+ }
+ InputVar("k"+i)
+ }
+
+ // Split the list into APAEqualZero one left and not APAEqualZero on right
+ def partitionPAEqualZero(eqs : List[APAEquation]):(List[APAEqualZero], List[APAEquation]) = eqs match {
+ case Nil => (Nil, Nil)
+ case (p@APAEqualZero(pac)::q) =>
+ val (a, b) = partitionPAEqualZero(q)
+ (APAEqualZero(pac)::a, b)
+ case (p::q) =>
+ val (a, b) = partitionPAEqualZero(q)
+ (a, p::b)
+ }
+ // Splits the list into equalities, inequalities, and a boolean indicating if the system is consistent.
+ def partitionPAGreaterEqZero(eqs : List[APAEquation]):(List[APAEqualZero], List[APAGreaterEqZero], Boolean) = eqs match {
+ case Nil => (Nil, Nil, true)
+ case (p@APAEqualZero(pac)::q) =>
+ val (a, b, c) = partitionPAGreaterEqZero(q)
+ (APAEqualZero(pac)::a, b, c)
+ case (p@APAGreaterEqZero(pac)::q) =>
+ val (a, b, c) = partitionPAGreaterEqZero(q)
+ (a, APAGreaterEqZero(pac)::b, c)
+ case (p@APAGreaterZero(APACombination(coef, o))::q) =>
+ val (a, b, c) = partitionPAGreaterEqZero(q)
+ (a, APAGreaterEqZero(APACombination(coef+APAInputCombination(-1), o))::b, c)
+ case (APATrue()::q) =>
+ partitionPAGreaterEqZero(q)
+ case (APAFalse()::q) =>
+ (Nil, Nil, false)
+ case (APADivides(n, pac)::q) =>
+ throw new Error("Divides are not supported at this point")
+ }
+
+
+ def recursive_propagation(
+ output_assignments : List[(OutputVar, APATerm)],
+ assignments_to_propagate : List[(OutputVar, APACombination)],
+ interesting_variables : List[OutputVar])
+ : List[(OutputVar, APATerm)] =
+ output_assignments match {
+ case Nil => Nil
+ case (v, pac@APACombination(_, _))::q => pac.replaceList(assignments_to_propagate) match {
+ case pac@APACombination(APAInputCombination(_, Nil), Nil) => // We propagate constants
+ if(interesting_variables contains v) {
+ (v, pac)::recursive_propagation(q, (v,pac)::assignments_to_propagate, interesting_variables)
+ } else {
+ recursive_propagation(q, (v,pac)::assignments_to_propagate, interesting_variables)
+ }
+ case t => (v, t)::recursive_propagation(q, assignments_to_propagate, interesting_variables)
+ }
+ case (v, t)::q => (v, t.replaceList(assignments_to_propagate))::recursive_propagation(q, assignments_to_propagate, interesting_variables)
+ }
+
+ // Propagate simple assignments, by removing the introduced variables if possible.
+ def propagateAssignment(y: OutputVar, t: APACombination, output_assignments : List[(OutputVar, APATerm)], output_variables_initial : List[OutputVar]): List[(OutputVar, APATerm)] = {
+ recursive_propagation(output_assignments, (y,t)::Nil, output_variables_initial)
+ }
+
+ def needsLessOperations(coef1: APAInputTerm, coef2: APAInputTerm): Boolean = (coef1, coef2) match {
+ case (APAInputCombination(k1, Nil), APAInputCombination(k2, Nil)) => Math.abs(k1) < Math.abs(k2)
+ case (APAInputCombination(k1, Nil), _) => true
+ case (_, APAInputCombination(k2, Nil)) => false
+ case (_, _) => false
+ }
+
+ def minInputTerms(coef1: APAInputTerm, coef2:APAInputTerm) = if(needsLessOperations(coef1, coef2)) coef1 else coef2
+
+ /** Sorting function (OptimizeMe) */
+ /** Priority to constant terms */
+ def by_least_outputvar_coef(eq1: APAEqualZero, eq2: APAEqualZero): Boolean = (eq1, eq2) match {
+ case (APAEqualZero(pac1@APACombination(c1, o1)), APAEqualZero(pac2@APACombination(c2, o2))) =>
+ val min_coefs_o1 = o1 map (_._1) reduceLeft (minInputTerms(_, _))
+ val min_coefs_o2 = o2 map (_._1) reduceLeft (minInputTerms(_, _))
+ needsLessOperations(min_coefs_o1, min_coefs_o2)
+ }
+}
+
+class APASynthesis(equations: FormulaSplit, input_variables_initial:List[InputVar], output_variables_initial:List[OutputVar]) {
+ import APASynthesis._
+ var output_variables:List[OutputVar] = output_variables_initial
+ var output_variables_encountered:List[OutputVar] = output_variables_initial
+
+ var input_variables:List[InputVar] = input_variables_initial
+ var input_variables_encountered:List[InputVar] = input_variables_initial
+
+ // Global_precondition is a conjunction of disjunctions of conjunctions.
+ var global_precondition: List[APAFormula] = Nil
+ // equation should not have output variables
+ def addPrecondition (e: APAFormula):Unit = {
+ val f = e.simplified
+ if(f.output_variables != Nil) // Debug sentence
+ throw new Exception("Error: there should be no output variables in this precondition :"+f)
+ f match {
+ case APATrue() =>
+ case APAFalse() => setFalsePrecondition()
+ case APAConjunction(l) => l foreach (addPrecondition(_))
+ case APAGreaterEqZero(APACombination(i, Nil)) => // We forward the constraint.
+ input_assignments = input_assignments map { case assignment =>
+ assignment.assumeSignInputTerm(i, PositiveZeroSign())
+ }
+ output_assignments = output_assignments map {
+ case (v, t) =>
+ (v, t.assumeSignInputTerm(i, PositiveZeroSign()))
+ }
+ global_precondition = f :: global_precondition
+ case f =>
+ global_precondition = f :: global_precondition
+ }
+ }
+ def setFalsePrecondition() = global_precondition = APAFalse()::Nil
+ def addOutputVar(y: OutputVar) = {
+ output_variables = (y::output_variables)
+ output_variables_encountered = (y::output_variables_encountered). distinct
+ }
+ def delOutputVar(y: OutputVar) = output_variables = output_variables.filterNot(_ == y)
+ def addInputVar (y: InputVar) = {
+ input_variables = (y::input_variables)
+ input_variables_encountered = (y::input_variables_encountered)
+ }
+ def getNewOutputVarWithoutRegistering() = APASynthesis.newOutputVariable(input_variables_encountered, output_variables_encountered)
+ def getNewOutputVar() = {
+ val y = getNewOutputVarWithoutRegistering()
+ addOutputVar(y)
+ y
+ }
+ def getNewInputVar() = {
+ val x = APASynthesis.newInputVariable(input_variables_encountered, output_variables_encountered)
+ addInputVar(x)
+ x
+ }
+ // List of reversed assignments: At the end, leftmost assignments should be done at the end.
+ var input_assignments: List[InputAssignment] = Nil
+ var output_assignments: List[(OutputVar, APATerm)] = Nil
+ def addSingleInputAssignment (x: InputVar, t: APAInputTerm) = input_assignments = input_assignments ++ (SingleInputAssignment(x, t.simplified)::Nil)
+ def addBezoutInputAssignment (xl: List[List[InputVar]], tl: List[APAInputTerm]) = input_assignments = input_assignments ++ (BezoutInputAssignment(xl, tl).simplified)
+ def addOutputAssignment(y: OutputVar, t: APATerm) = output_assignments = (y, t.simplified)::output_assignments
+ def removeInputAssignment(y: InputVar) = input_assignments = input_assignments filterNot {case SingleInputAssignment(x, _) if x == y => true; case _ => false}
+ /************* Functions used in the algorithm *************** */
+ def simplifyEquations(equations: List[APAEquation]) : List[APAEquation] = {
+ equations flatMap {
+ case e@APADivides(k, APACombination(c, Nil)) =>
+ addPrecondition(e.simplified)
+ Nil
+ case APADivides(k, APACombination(c, o)) =>
+ val y = getNewOutputVar()
+ APAEqualZero(APACombination(c, (k, y)::o)).simplified::Nil
+ case APAGreaterZero(APACombination(c, o)) => APAGreaterEqZero(APACombination(c-APAInputCombination(1), o)).simplified::Nil
+ case e => e.simplified::Nil
+ }
+ }
+
+ /** Returns the remaining non_equalities (non_equalities should not contain equalities, nor will the returned term do) */
+ def solveEqualities(data: FormulaSplit): APASplit = {
+ val FormulaSplit(equalities, non_equalities, remaining_disjunctions) = data
+
+ /** Make sure all equalities have at least one output variable, else remove them. */
+ val (interesting_equalities, precondition_equalities) = equalities partition (_.has_output_variables)
+ addPrecondition(APAConjunction(precondition_equalities))
+
+ val sorted_equalities = interesting_equalities sortWith by_least_outputvar_coef
+
+ sorted_equalities match {
+ case Nil =>
+ val newfs = FormulaSplit(Nil, non_equalities, remaining_disjunctions)
+ solveEquations(newfs)
+ case (eq1@APAEqualZero(pac@APACombination(c1, o1)))::rest_equalities =>
+ var const_part:APAInputTerm = c1
+ var o1_coefs = o1 map (_._1)
+ var o1_vars = o1 map (_._2)
+ val gcd = APAInputGCD(o1_coefs).replaceList(input_assignments flatMap (_.extract)).simplified
+
+ gcd match {
+ case APAInputCombination(1, Nil) =>
+ // Perfect !! We know that there is a solution.
+ // Continue to CONTINUE_POINT
+ case n =>
+ val coefs_are_zero = APAConjunction(o1_coefs map (APACombination(_)===APAInputCombination(0))).simplified
+ if(coefs_are_zero == APATrue() || pac.allCoefficientsAreZero) {
+ // We add the precondition const_part == 0
+ addPrecondition(APACombination(const_part)===APAInputCombination(0))
+ return solveEqualities(FormulaSplit(rest_equalities, non_equalities, remaining_disjunctions))
+ } else if(coefs_are_zero == APAFalse() || pac.notAllCoefficientsAreZero) {
+ // Regular run. We know that the GCD of the numbers is positive.
+ addPrecondition(APADivides(n, APACombination(const_part, Nil)))
+ val x = getNewInputVar()
+ val n_positive = n.assumeSign(1)
+ val gcd_expr = n_positive match {
+ case APAInputCombination(i, Nil) =>
+ n_positive
+ case APAInputCombination(0, ((k, _)::Nil)) if Math.abs(k) == 1 =>
+ n_positive
+ case _ =>
+ val gcd_var = getNewInputVar().assumePositive()
+ val result = APAInputCombination(gcd_var).replaceList(input_assignments flatMap (_.extract))
+ assert(result.isPositiveZero)
+ addSingleInputAssignment(gcd_var, n_positive)
+ result
+ }
+ addSingleInputAssignment(x, APAInputDivision(const_part, gcd_expr).simplified)
+ const_part = APAInputCombination(0, (1, x)::Nil)
+ o1_coefs = o1_coefs map (APAInputDivision(_, gcd_expr).simplified)
+ } else {
+ var (cond1, prog1) = APASynthesis.solve(output_variables, APAEqualZero(pac.assumeAllCoefficientsAreZero) :: rest_equalities ++ non_equalities) // Case where the coefficients are null.
+ cond1 = cond1.assumeBefore(coefs_are_zero)
+ var (cond2, prog2) = APASynthesis.solve(output_variables, APAEqualZero(pac.assumeNotAllCoefficientsAreZero) :: rest_equalities ++ non_equalities) //solve with the knowledge that not all the coefficients are null.
+ cond2 = cond2.assumeBefore(APANegation(coefs_are_zero))
+ return APACaseSplit.optimized((cond1, prog1)::(cond2, prog2)::Nil)
+ }
+ }
+ // CONTINUE_POINT
+ // Now the gcd of the output variables is for sure 1.
+ // We find a solution to o1_coefs.o1_vars + 1 = 0
+ // Then we know that by multiplying the first line by const_part, we obtain the general solution
+ // Express the input variables by assignments
+
+ val new_input_variables: List[List[InputVar]]= o1_vars.indices.toList map { _ => o1_vars.indices.toList map { _ => getNewInputVar()}}
+ addBezoutInputAssignment(new_input_variables, o1_coefs)
+
+ val first_line:List[APACombination] = new_input_variables.head map {
+ case iv =>
+ val p = APAInputCombination(0, (1, iv)::Nil)
+ p.replaceList(input_assignments flatMap (_.extract)) match {
+ case t@APAInputCombination(i, Nil) =>
+ removeInputAssignment(iv)
+ APACombination(const_part * t)
+ case t@APAInputCombination(0, (i, v)::Nil) if Math.abs(i) == 1 => // Simple case 2
+ removeInputAssignment(iv)
+ APACombination(const_part * t)
+ case _ => // If it's not an integer, keep the variable name.
+ APACombination(const_part * p)
+ }
+ }
+ // From this solution, we introduce |o1| - 1 new variables to solve the equality and remove the equation.
+ val new_assignments:List[APACombination] = new_input_variables.tail.foldLeft(first_line:List[APACombination]) { case (assignments, line) =>
+ val y = getNewOutputVar()
+ (assignments zip line) map {
+ case (expr:APACombination, iv) =>
+ //expr + y*iv
+ val p = APAInputCombination(0, (1, iv)::Nil)
+ p.replaceList(input_assignments flatMap (_.extract)) match {
+ case t@APAInputCombination(i, Nil) => // Simple case 2
+ removeInputAssignment(iv)
+ expr + (APACombination(y)*t)
+ case t@APAInputCombination(0, (i, v)::Nil) if Math.abs(i) == 1 => // Simple case 2
+ removeInputAssignment(iv)
+ expr + (APACombination(y)*t)
+ case _ =>
+ expr + (APACombination(y)*p)
+ }
+ }
+ }
+ // We add the variables if they are needed.
+ //if(((new_assignments flatMap (_.input_variables)).distinct intersect new_input_variables) != Nil)
+
+
+ //var new_equalities = rest_equalities
+ //var new_nonequalities = non_equalities
+ val assignments = (o1_vars zip new_assignments)
+ assignments foreach {
+ case (v, pac) => addOutputAssignment(v, pac)
+ //val (new_eqs1, new_noneqs1) = partitionPAEqualZero(new_equalities map (_.replace(v, pac)))
+ //val (new_eqs2, new_noneqs2) = partitionPAEqualZero(new_nonequalities map (_.replace(v, pac)))
+ //new_equalities = new_eqs1 ++ new_eqs2
+ //new_nonequalities = new_noneqs1 ++ new_noneqs2
+ delOutputVar(v)
+ }
+ //var new_remaining_disjunctions = remaining_disjunctions map (_.replaceList(assignments))
+ val newfs = FormulaSplit(rest_equalities, non_equalities, remaining_disjunctions).replaceList(assignments)
+ solveEqualities(newfs)
+ }
+ }
+
+ def setRemainingVariablesToZero(output_variables : List[OutputVar]):Unit = output_variables match {
+ case Nil =>
+ case y::q =>
+ output_variables_initial contains y match {
+ case true => output_assignments = propagateAssignment(y, APACombination(APAInputCombination(0, Nil), Nil), output_assignments, output_variables_initial)
+ addOutputAssignment(y, APACombination(APAInputCombination(0, Nil), Nil))
+ delOutputVar(y)
+ setRemainingVariablesToZero(q)
+ case false => output_assignments = propagateAssignment(y, APACombination(APAInputCombination(0, Nil), Nil), output_assignments, output_variables_initial)
+ delOutputVar(y)
+ setRemainingVariablesToZero(q)
+ }
+ }
+
+ // Returns (cond, l_left, l_right, l_remaining) such that:
+ // l_left contains elements (A, a) such that A <= a*v
+ // l_right contains elements (b, B) such that b*v <= B
+ // l_remaining contains elements which do not contain v
+ // l_cond is a list of formulas
+ // Properties : The length of the stream is 3^l_formulas.size of the first element.
+ def getInequalitiesForVariable(v: OutputVar, inequalities:List[APAGreaterEqZero]): Stream[(List[APAFormula], List[(APACombination, APAInputTerm)], List[(APAInputTerm, APACombination)], List[APAEquation])] = {
+ def getInequalitiesForVariable_aux(v: OutputVar,
+ inequalities:List[APAEquation],
+ result: (List[APAFormula], List[(APACombination, APAInputTerm)], List[(APAInputTerm, APACombination)], List[APAEquation])
+ ) : Stream[(List[APAFormula], List[(APACombination, APAInputTerm)], List[(APAInputTerm, APACombination)], List[APAEquation])] =
+ inequalities match {
+ case Nil =>
+ // At this split point, we can solve.
+ Stream(result)
+ case ((p@APAGreaterEqZero(pac@APACombination(c, o)))::q) =>
+ val (l_formulas, l_left, l_right, l_remaining)=result
+ o find (_._2 == v) match {
+ case None =>
+ getInequalitiesForVariable_aux(v, q, (l_formulas, l_left, l_right, p::l_remaining))
+ case Some(found_element@(k, v)) =>
+ if(k.isPositive)
+ getInequalitiesForVariable_aux(v, q, (l_formulas, (APACombination(c, o.filterNot(_ == found_element)) * (-1), k)::l_left, l_right, l_remaining))
+ else if(k.isZero) // Should not happen, but this is just to keep a coherent skeleton.
+ getInequalitiesForVariable_aux(v, q, (l_formulas, l_left, l_right, APAGreaterEqZero(APACombination(c, o.filterNot(_ == found_element)))::l_remaining))
+ else if(k.isNegative)
+ getInequalitiesForVariable_aux(v, q, (l_formulas, l_left, (-k, APACombination(c, o.filterNot(_ == found_element)))::l_right, l_remaining))
+ else {
+ def replaceLeftBound(left: List[(APACombination, APAInputTerm)], t1: APAInputTerm, s: SignAbstraction): List[(APACombination, APAInputTerm)] = {
+ left map {
+ case (pac, i) =>
+ val result = (pac.assumeSignInputTerm(t1, s), i.assumeSignInputTerm(t1, s))
+ result
+ }
+ }
+ def replaceRightBound(right: List[(APAInputTerm, APACombination)], t1: APAInputTerm, s: SignAbstraction): List[(APAInputTerm, APACombination)] = {
+ right map {
+ case (i, pac) =>
+ val result = (i.assumeSignInputTerm(t1, s), pac.assumeSignInputTerm(t1, s))
+ result
+ }
+ }
+ def replaceRemaining(remaining: List[APAEquation], t1: APAInputTerm, s: SignAbstraction): List[APAEquation] = {
+ val result = remaining map (_.assumeSignInputTerm(t1, s))
+ result
+ }
+ (if(k.can_be_positive) { // k can be positive
+ val k_positive = k.assumeSign(1)
+ assert(k_positive.isPositive)
+ val new_l_formulas = (APACombination(k) > APAInputCombination(0))::l_formulas
+ val new_l_left = (APACombination(c, o.filterNot(_ == found_element))*(-1), k_positive)::replaceLeftBound(l_left, k, k_positive)
+ val new_l_right = replaceRightBound(l_right, k, k_positive)
+ val new_l_remaining = replaceRemaining(l_remaining, k, k_positive)
+ val new_q = replaceRemaining(q, k, k_positive)
+ getInequalitiesForVariable_aux(v, new_q, (new_l_formulas, new_l_left, new_l_right, new_l_remaining))
+ } else Stream()) append
+ (if(k.can_be_zero) { // k can be zero
+ val k_nul = APAInputCombination(0)
+ assert(k_nul.isZero)
+ val new_l_formulas = (APACombination(k) === APAInputCombination(0))::l_formulas
+ val new_l_left = replaceLeftBound(l_left, k, k_nul)
+ val new_l_right = replaceRightBound(l_right, k, k_nul)
+ val new_l_remaining = APAGreaterEqZero(APACombination(c, o.filterNot(_ == found_element)))::replaceRemaining(l_remaining, k, k_nul)
+ val new_q = replaceRemaining(q, k, k_nul)
+ getInequalitiesForVariable_aux(v, new_q, (new_l_formulas, new_l_left, new_l_right, new_l_remaining))
+ } else Stream()) append
+ (if(k.can_be_negative) { // k can be negative
+ val k_negative = k.assumeSign(-1)
+ val mk_negative = -k_negative
+ assert(mk_negative.isPositive)
+ val new_l_formulas = (APACombination(k) < APAInputCombination(0))::l_formulas
+ val new_l_left = replaceLeftBound(l_left, k, k_negative)
+ val new_l_right = (mk_negative, APACombination(c, o.filterNot(_ == found_element)))::replaceRightBound(l_right, k, k_negative)
+ val new_l_remaining = replaceRemaining(l_remaining, k, k_negative)
+ val new_q = replaceRemaining(q, k, k_negative)
+ getInequalitiesForVariable_aux(v, new_q, (new_l_formulas, new_l_left, new_l_right, new_l_remaining))
+ } else Stream())
+ }
+ }
+ case APATrue()::q =>
+ val (l_formulas, l_left, l_right, l_remaining)=result
+ getInequalitiesForVariable_aux(v, q, (l_formulas, l_left, l_right, l_remaining))
+ case APAFalse()::q =>
+ val (l_formulas, l_left, l_right, l_remaining)=result
+ getInequalitiesForVariable_aux(v, q, (l_formulas, l_left, l_right, APAFalse()::l_remaining))
+ case f::q =>
+ throw new Error("Could not handle "+f)
+ }
+ getInequalitiesForVariable_aux(v, inequalities, (Nil, Nil, Nil, Nil))
+ }
+
+ /** Solve them, so now we only have non-equalities */
+ /** The simplification of inequalities can generate new equalities, so we handle them. */
+ def solveEquations(data: FormulaSplit):APASplit = {
+ val FormulaSplit(equalities, non_equalities, remaining_disjunctions) = data
+ // Let's extract the divisibility predicates and converts them to equalities.
+ val (new_equalities, new_non_equalities) = partitionPAEqualZero(simplifyEquations(non_equalities))
+ val total_equalities = equalities ++ new_equalities
+ if(total_equalities != Nil) {
+ solveEqualities(FormulaSplit(total_equalities, new_non_equalities, remaining_disjunctions))
+ } else {
+ val filtered_non_equalities = non_equalities filterNot (_==APATrue())
+ if(filtered_non_equalities contains APAFalse()) return APAFalseSplit()
+ //TODO :Here, verify that we don't have remaining_disjunctions anymore before handling the rest.
+ if(!remaining_disjunctions.isEmpty) {
+ assert(equalities == Nil)
+ // We merge the current non equalities to the subproblems.
+ val problems:Stream[FormulaSplit] = remaining_disjunctions map (FormulaSplit.conjunction(FormulaSplit(Nil, filtered_non_equalities, Stream.empty), _))
+ // We recombine the subproblems together.
+ val solutions = (problems map (APASynthesis.solveLazyEquations(input_variables, output_variables, _))).toList
+ return APACaseSplit.optimized(solutions)
+ }
+ assert(remaining_disjunctions.isEmpty)
+
+ /** Get only inequalities, plus maybe with "False" in other */
+ val (equalities2, inequalities, is_consistent) = partitionPAGreaterEqZero(non_equalities)
+ // equalities2 should be empty given that new_non_equalities cannot contain equalities
+ assert(equalities2 == Nil)
+ if(!is_consistent) return APAFalseSplit()
+
+ /** Remove redundant inequalities, maybe generating equalities */
+ //val (inequalities3, equalities3, is_consistent3) = removeRedundancies(inequalities)
+ val (inequalities3, equalities3, is_consistent3) = (inequalities, Nil, true)
+
+ if(!is_consistent3) return APAFalseSplit()
+ if(equalities3 != Nil)
+ return solveEqualities(FormulaSplit(equalities3, inequalities3, Stream.empty))
+
+ var current_inequalities = inequalities3
+ var current_noninequalities = List[APAEquation]()
+ var is_consistent4 = true
+ /** Solves for unbounded variables, when there are no case splits. */
+ /** The value of output_variable is going to change, but we just need the initial one. */
+ var current_inequalities_saved = APATrue()::current_inequalities
+ while(current_inequalities != current_inequalities_saved) {
+ current_inequalities_saved = current_inequalities
+ output_variables foreach { y =>
+ getInequalitiesForVariable(y, current_inequalities) match {
+ case Stream((l_formula@Nil, l_left@Nil, l_right@Nil, l_remaining)) =>
+ setRemainingVariablesToZero(y::Nil)
+ case Stream((l_formula@Nil, l_left@Nil, l_right@l, l_remaining)) =>
+ // Only bounded on the right by equations of style b*y <= pac, so we know that the integer upper bounds are pac/b
+ val upper_bounds = l_right map { case (b , pac) => APADivision(pac, b).simplified }
+ addOutputAssignment(y, APAMinimum(upper_bounds))
+ delOutputVar(y)
+ val (eqs, ineqs, consistency) = partitionPAGreaterEqZero(l_remaining)
+ if(eqs != Nil) throw new Exception("Support for equalities appearing after split is not supported (yet)")
+ is_consistent4 &&= consistency
+ current_inequalities = ineqs
+ case Stream((l_formula@Nil, l_left@l, l_right@Nil, l_remaining)) =>
+ // Only bounded on the left by equations of style pac <= a*y, so we know that the integer upper bounds are (pac+a-1)/a
+ val lower_bounds = l_left map { case (pac, a) => APADivision(pac + APACombination(a-APAInputCombination(1)), a).simplified }
+ addOutputAssignment(y, APAMaximum(lower_bounds))
+ delOutputVar(y)
+ val (eqs, ineqs, consistency) = partitionPAGreaterEqZero(l_remaining)
+ if(eqs != Nil) throw new Exception("Support for equalities appearing after split is not supported (yet)")
+ current_inequalities = ineqs
+ is_consistent4 &&= consistency
+ case _ =>
+ }
+ }
+ }
+ if(!is_consistent4) return APAFalseSplit()
+ if(output_variables == Nil) {
+ addPrecondition(APAConjunction(current_inequalities))
+ return APAEmptySplit()
+ }
+
+ // Now at this point, all variables are bounded on both sides.
+ // Let's find the one for which the LCM of its coefficients is the smallest.
+ // (Number of splits, min_coef)
+ val output_variables_with_min_coefs:List[((Int, APAInputTerm), OutputVar)] = output_variables map {
+ case y =>
+ // Both l_left and r_right are not empty because of the previous computation
+ getInequalitiesForVariable(y, current_inequalities) match {
+ case Stream((l_formula, l_left, l_right, l_remaining)) =>
+ assert(l_formula == Nil) // l_left and l_right only contain integers for bounds.
+ val l_left_coefs:List[APAInputTerm] = l_left map (_._2)
+ val l_right_coefs:List[APAInputTerm] = l_right map (_._1)
+ val min_coef = APAInputLCM(l_left_coefs ++ l_right_coefs).simplified
+ ((l_formula.size, min_coef), y)
+ case Stream.cons((l_formula, l_left, l_right, l_remaining), _) =>
+ // We have to split everything for this variable, so we don't do anything yet
+ ((l_formula.size, APAInputCombination(0)), y)
+ }
+ }
+ def min_coef(i1:((Int, APAInputTerm), OutputVar), i2:((Int, APAInputTerm), OutputVar)) : ((Int, APAInputTerm), OutputVar) = (i1, i2) match {
+ case (t1@((split1, k1), v1), t2@((split2, k2), v2)) =>
+ if(split1 < split2) t1 else (if(split1==split2) (if(needsLessOperations(k1, k2)) t1 else t2) else t2)
+ }
+ val (_, y) = output_variables_with_min_coefs.reduceRight(min_coef(_, _))
+
+ getInequalitiesForVariable(y, current_inequalities) match {
+ case Stream((Nil, l_left, l_right, l_remaining)) => // The signs are fully determined !!
+ val (eqs, ineqs, consistency) = partitionPAGreaterEqZero(l_remaining)
+ if(eqs != Nil) throw new Exception("Support for equalities appearing after split is not supported (yet)")
+ current_inequalities = ineqs
+ is_consistent4 &&= consistency
+
+ if(l_right.size <= l_left.size) {
+ val upper_bounds = l_right map { case (b , pac) => APADivision(pac, b).simplified }
+ addOutputAssignment(y, APAMinimum(upper_bounds))
+ delOutputVar(y)
+ } else {
+ val lower_bounds = l_left map { case (pac, a) => APADivision(pac + APACombination(a-APAInputCombination(1)), a).simplified }
+ addOutputAssignment(y, APAMaximum(lower_bounds))
+ delOutputVar(y)
+ }
+ val prog_needed_afterwards = output_variables != Nil
+
+ // OptimizeMe : If a is smaller than b, use it instead of a.
+ var output_variables_used = (output_variables_encountered).distinct
+ var input_variables_used = (input_variables_encountered).distinct
+
+ // We don't care about pairs of equations that are trivial to reduce.
+ l_left foreach { case (eqA, a) =>
+ l_right foreach { case (b, eqB) =>
+ if(a==APAInputCombination(1, Nil)) current_inequalities = (APAGreaterEqZero(eqB-(eqA*b)))::current_inequalities
+ else if(b==APAInputCombination(1, Nil)) current_inequalities = (APAGreaterEqZero((eqB*a)-eqA))::current_inequalities
+ }
+ }
+ val l_left_filtered = l_left filterNot (_._2==APAInputCombination(1, Nil))
+ val l_right_filtered = l_right filterNot (_._1==APAInputCombination(1, Nil))
+
+ val lcm_value = APAInputLCM((l_left_filtered map (_._2)) ++ (l_right_filtered map (_._1))).simplified
+ val lcm_int:Option[Int] = lcm_value match {
+ case APAInputCombination(i, Nil) => Some(i)
+ case _=> None
+ }
+ var lcm_expr = lcm_int match {
+ case Some(i) => APAInputCombination(i)
+ case None =>
+ lcm_value match {
+ case t@APAInputCombination(0, (i, v)::Nil) => t // Simple enough to get propagated easily
+ case t => // "Too complicated"
+ val var_lcm = getNewInputVar()
+ addSingleInputAssignment(var_lcm, lcm_value)
+ APAInputCombination(var_lcm)
+ }
+ }
+
+ val l_left_normalized = l_left_filtered map {
+ case (eqA, a) =>
+ assert(a.isPositive)
+ eqA*(lcm_expr/a)
+ }
+ val l_right_normalized = l_right_filtered map {
+ case (b, eqB) =>
+ assert(b.isPositive)
+ eqB*(lcm_expr/b)
+ }
+
+ var collected_new_input_variables:List[InputVar] = Nil
+ val collected_new_equations:List[APAEquation] = l_right_normalized flatMap { case eqB =>
+ val new_mod_bounds = l_left_normalized map { case eqA => (eqB - eqA) } filterNot {
+ case APACombination(APAInputCombination(i, Nil), Nil) =>
+ lcm_int match {
+ case Some(lcm) => i >= lcm-1
+ case None => false
+ }
+ case _ => false
+ }
+ // OptimizeMe ! If eqB%L contains only input variables, assign a new input variable to it.
+ // OptimizeMe ! If eqB & eqA contain only input variables, add a precondition for it.
+ new_mod_bounds match {
+ case Nil => Nil // Ok, nothing to add
+ case _ => // We need decomposition
+ val k = getNewInputVar().assumePositiveZero()
+ val ov = getNewOutputVar()
+ collected_new_input_variables = k::collected_new_input_variables
+ val k_expr = APAInputCombination(0, (1, k)::Nil)
+ assert(k_expr.isPositiveZero)
+ val new_ineqs = new_mod_bounds map {
+ case mod_bound =>
+ val result = APACombination(k_expr, Nil) <= mod_bound
+ result
+ }
+ val new_eq = eqB === APACombination(k_expr, (lcm_value, ov)::Nil)
+ new_eq::new_ineqs
+ }
+ }
+ (collected_new_equations, collected_new_input_variables) match {
+ case (Nil, Nil) =>
+ if(current_inequalities == Nil) {
+ APAEmptySplit()
+ } else {
+ solveEquations(FormulaSplit(Nil, current_inequalities, Stream.empty))
+ }
+ case (Nil, t) => throw new Error("How could this happen ? Both variables should be Nil, but the second one is "+t)
+ case (t, Nil) => throw new Error("How could this happen ? Both variables should be Nil, but the first one is "+t)
+ case (_, _) =>
+ val (condition, program) = APASynthesis.solve(collected_new_equations ++ current_inequalities)
+ if(prog_needed_afterwards) {
+ APAForSplit(collected_new_input_variables, APAInputCombination(0), lcm_value-APAInputCombination(1), condition, program)
+ } else {
+ //We don't need the program. Just the precondition
+ APAForSplit(collected_new_input_variables, APAInputCombination(0), lcm_value-APAInputCombination(1), condition, APAProgram.empty)
+ }
+ }
+ case stream => // The signs are not fully determined.
+ // OptimizeMe ! Too bad, the split is already done, but we cannot continue that way
+ // because we cannot assign it in other cases. Something better ?
+ val possibilities = stream.toList
+ val solutions = possibilities.zipWithIndex map {
+ case (t@(l_formula, l_left, l_right, l_remaining), i) =>
+ //println(i + " on variable " + y + " with equations " + t)
+ val left_equations = l_left map {
+ case (p, k) =>
+ if(k.isNotDefined) {
+ APAFalse()
+ } else {
+ assert(k.isPositive)
+ val right_member = APACombination(y)*k
+ p <= right_member
+ }
+ }
+ val right_equations = l_right map {
+ case (k, p) =>
+ if(k.isNotDefined) {
+ APAFalse()
+ } else {
+ assert(k.isPositive)
+ val left_member = APACombination(y)*k
+ left_member <= p
+ }
+ }
+ val collected_new_equations = left_equations ++ right_equations ++ l_remaining
+ //println("Collected : " + collected_new_equations)
+ val (condition, program) = APASynthesis.solve(output_variables, collected_new_equations)
+ val result = (condition && APAConjunction(l_formula), program)
+ result
+ }
+ //println("Regrouping solutions")
+ APACaseSplit.optimized(solutions)
+ }
+ }
+ }
+
+
+ def solve():(APACondition, APAProgram) = {
+ /************* Main algorithm *************** */
+ //***** Step 1: There are no quantifiers by construction. Nothing to do
+ //***** Step 2: Remove divisibility constraints
+ // Convert "Greater" to "GreaterEq"
+ // Simplify everything
+ //val equations2 = equations.simplified //simplifyEquations(equations)
+
+ //***** Step 3 : converting to DNF : Nothing to do, the argument is a conjunction
+ //***** Step 4 : Case Splitting. Nothing to do.
+ //***** Step 5 : Removing equalities
+
+ // All equations without output vars go directly to the global precondition
+ //val (eq_with_outputvars, eq_without_outputvars) = equations2 partition (_.has_output_variables)
+ //addPrecondition(APAConjunction(eq_without_outputvars))
+ // Retrieve all equalities
+ //var (equalities, non_equalities) = partitionPAEqualZero(eq_with_outputvars)
+
+ val result = solveEquations(equations)
+
+ // Looking for variables bounded only on one side.
+ result match {
+ case APAFalseSplit() =>
+ setFalsePrecondition()
+ (APACondition.optimized(Nil, APAConjunction(global_precondition), APAEmptySplitCondition()), APAProgram.empty)
+ case (pa_split@APACaseSplit(list_cond_prog)) =>
+ val splitted_conditions:List[APACondition] = list_cond_prog map (_._1)
+ if(list_cond_prog == Nil) { // Nobody took care of the remaining output variables.
+ setRemainingVariablesToZero(output_variables)
+ }
+ (APACondition.optimized(input_assignments, APAConjunction(global_precondition), APACaseSplitCondition(splitted_conditions)),
+ APAProgram.optimized(input_variables_initial, input_assignments, pa_split, output_assignments, output_variables_initial))
+ case pa_split@APAForSplit(vars, l, u, cond, prog) =>
+ prog match {
+ case t if t == APAProgram.empty =>
+ (APACondition.optimized(input_assignments, APAConjunction(global_precondition), APAForCondition(vars, l, u, cond)),
+ APAProgram.optimized(input_variables_initial, input_assignments, APAEmptySplit(), output_assignments, output_variables_initial))
+ case _ =>
+ (APACondition.optimized(input_assignments, APAConjunction(global_precondition), APAForCondition(vars, l, u, cond)),
+ APAProgram.optimized(input_variables_initial, input_assignments, pa_split, output_assignments, output_variables_initial))
+ }
+ case pa_split@APAEmptySplit() =>
+ setRemainingVariablesToZero(output_variables)
+ (APACondition.optimized(input_assignments, APAConjunction(global_precondition), APAEmptySplitCondition()),
+ APAProgram.optimized(input_variables_initial, input_assignments, pa_split, output_assignments, output_variables_initial))
+ case t =>
+ throw new Error("handling of "+t+" not implemented yet")
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/comfusy/APASynthesisExamples.scala b/src/main/scala/leon/synthesis/comfusy/APASynthesisExamples.scala
new file mode 100644
index 000000000..bcf8bafa3
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/APASynthesisExamples.scala
@@ -0,0 +1,277 @@
+package leon.synthesis.comfusy
+import scala.language.implicitConversions
+
+object APASynthesisExamples {
+ import APASynthesis._
+ def O(name: String) = OutputVar(name)
+ def I(name: String) = InputVar(name)
+ implicit def OutputVarToPACombination(o: OutputVar):APACombination = APACombination(o)
+ implicit def InputVarToPACombination(i: InputVar):APACombination = APACombination(i)
+ implicit def IntegerToPACombination(k: Int):APAInputCombination = APAInputCombination(k)
+ implicit def InputToPACombination(k: APAInputCombination):APACombination = APACombination(k)
+
+ val x = O("x")
+ val x1 = O("x1")
+ val y = O("y")
+ val y1 = O("y1")
+ val z = O("z")
+
+ val a = I("a")
+ val b = I("b")
+ val c = I("c")
+ val d = I("d")
+
+ APASynthesis.advanced_modulo = false
+ APASynthesis.run_time_checks = true
+ //APASynthesis.rendering_mode = RenderingPython
+ APASynthesis.rendering_mode = RenderingScala
+ Common.computing_mode = Common.OTBezout()
+
+ def main(args : Array[String]) : Unit = {
+ /*completeExample()
+ hourMinutSecondExample()
+ balancedProblem()
+ dividesExample()
+ rhymesExample()*/
+ quotientExample()
+ //multiplicativeInverseExample()
+ //OptimizedExample()
+ //extract7and8()
+ //stepExample()
+ //extractRatio()
+ //multiArray()
+ //APAExample()
+ //paboucle()
+ }
+
+ def hourMinutSecondExample() {
+ val seconds = I("seconds")
+ val s = O("s")
+ val m = O("m")
+ val h = O("h")
+ val condition = (
+ seconds === s + (m * 60) + (h*3600)
+ && s >= 0 && s < 60
+ && m >= 0 && m < 60
+ )
+ val solution = APASynthesis.solve("getHourMinutSeconds", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+ def balancedProblem() {
+ val weight = I("weight")
+ val w1 = O("w1")
+ val w2 = O("w2")
+ val w3 = O("w3")
+ val c1 = APAEqualZero(APACombination(0, (-1, weight)::Nil, (1, w1)::(3, w2)::(9, w3)::Nil))
+ val c2 = APAGreaterEqZero(APACombination(1, Nil, (1, w1)::Nil))
+ val c3 = APAGreaterEqZero(APACombination(1, Nil, (-1, w1)::Nil))
+ val c4 = APAGreaterEqZero(APACombination(1, Nil, (1, w2)::Nil))
+ val c5 = APAGreaterEqZero(APACombination(1, Nil, (-1, w2)::Nil))
+ val c6 = APAGreaterEqZero(APACombination(1, Nil, (1, w3)::Nil))
+ val c7 = APAGreaterEqZero(APACombination(1, Nil, (-1, w3)::Nil))
+ val solution = APASynthesis.solve("getWeights", c1::c2::c3::c4::c5::c6::c7::Nil)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def dividesExample() {
+ val pac1 = APADivides(5, b+y)
+ val pac2 = APADivides(7, c+y*b)
+ val solution = APASynthesis.solve("divides5And7", pac1::pac2::Nil)
+ println(solution._1)
+ println(solution._2)
+ }
+ def completeExample() {
+ val condition = ( y*c === b || y*b === c)
+ val solution = APASynthesis.solve("solveEquation", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def stepExample() {
+ val Nsyls = I("\\Nsyls")
+ val Isyls = I("\\Isyls")
+ val Elines = I("\\Elines")
+ val Ilines = I("\\Ilines")
+ val Tlines = O("\\Tlines")
+ val Nlines = O("\\Nlines")
+ val lines8 = O("\\lineeight")
+ val lines7 = O("\\lineseven")
+ val NSlines = O("\\NSlines")
+
+ val condition = (
+ Nsyls + Isyls === lines8*8 + lines7*7
+ && lines8 >= 0
+ && lines7 >= 0
+ && lines8 < 4*7
+ && Tlines === Elines + Nlines
+ && Nlines === lines8 + lines7
+ && Nlines === Ilines + NSlines
+ && (Tlines divisible_by 4)
+ )
+
+ val solution = APASynthesis.solve("rhymes78", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def rhymesExample() {
+ /* Solves the following poem problem:
+ We want to arrange names in a poem such that :
+ -- Most verses are made of 8 syllables of names (ex: Denver Youcef Elisabeth)
+ -- Maybe some are made of 7 syllables of names + 1 conjunction syllabe. (ex: Viktor Ruzica _and_ Philip)
+ -- on verse rhymes with its predecessor or its successor.
+ Aside from the rhyming problem, there is the arrangement problem.
+ We have to know in advance how many lines of 7 and 8 syllables of names we will have, before filling them.
+
+ Furthermore, the user supplies existing lines (such as the examples given above)
+ *
+ */
+ val complete_lines = I("complete_lines")
+ val incomplete_syllables = I("incomplete_syllables")
+ val input_syllables = I("input_syllables") /* Number of syllables to place */
+ val incomplete_lines = I("incomplete_lines")
+ val new_lines = O("new_lines")
+ val new_empty_lines = O("new_empty_lines")
+ val total_lines = O("total_lines")
+ val lines_7_syllables = O("lines_7_syllables")
+ val lines_8_syllables = O("lines_8_syllables")
+ val condition = (
+ total_lines === complete_lines + new_lines
+ && new_lines === incomplete_lines + new_empty_lines
+ && new_lines === lines_7_syllables + lines_8_syllables
+ && incomplete_syllables + input_syllables === lines_7_syllables * 7 + lines_8_syllables * 8
+ && (total_lines divisible_by 4)
+
+ && lines_7_syllables >= 0
+ && lines_8_syllables >= 0
+ && total_lines >= 0
+ && lines_7_syllables < 8*4
+ )
+ val solution = APASynthesis.solve("rhymes78", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def quotientExample() {
+ //val b2 = b.assumeSign(1).toInputTerm
+ //val condition = (a === (z*b2)*b2 + x*b2 + y && y >= 0 && y < b2 && x >= 0 && x < b2)
+ //val condition = (a === x*b2 + y && y >= 0 && y < b2)
+ val j = O("j")
+ val k = O("k")
+ val i = I("i")
+ val x = I("x")
+ val y = I("y")
+ /*val condition = (i === k * x + j
+ && j >= 0 && j < x
+ && k >= 0&& k < y)*/
+ val condition = APAConjunction(List(APAEqualZero(APACombination(APAInputCombination(0,
+ List((1,InputVar("i")))),List((APAInputCombination(-1,List()),OutputVar("j")),
+ (APAInputCombination(0,List((-1,InputVar("x")))),OutputVar("k"))))),
+ APAGreaterEqZero(APACombination(APAInputCombination(0,List()),
+ List((APAInputCombination(1,List()),OutputVar("j"))))),
+ APAGreaterEqZero(APACombination(APAInputCombination(-1,List((1,InputVar("x")))),List((APAInputCombination(-1,List()),OutputVar("j"))))), APAGreaterEqZero(APACombination(APAInputCombination(0,List()),List((APAInputCombination(1,List()),OutputVar("k"))))), APAGreaterEqZero(APACombination(APAInputCombination(-1,List((1,InputVar("y")))),List((APAInputCombination(-1,List()),OutputVar("k")))))))
+
+ println(condition)
+ val solution = APASynthesis.solve("quotient", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def multiplicativeInverseExample() {
+ val M = InputVar("M")
+ val n = InputVar("n")
+ val x = OutputVar("x")
+ val condition = ((x*n - 1) divisible_by M.toInputTerm())
+ val solution = APASynthesis.solve("multiplicativeInverse", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ /*def ArmandoExample() {
+ return
+ val N = InputVar("N").assumeSign(1)
+ val P = InputVar("P").assumeSign(1)
+ val p1 = InputVar("p1")
+ val p2 = InputVar("p2")
+ val e1 = OutputVar("e1")
+ val s1 = OutputVar("s1")
+ val e2 = OutputVar("e2")
+ val s2 = OutputVar("s1")
+ val p1len = OutputVar("p1len")
+ val p2len = OutputVar("p2len")
+ val rstart_c1 = OutputVar("rstart_c1")
+ val rstart_c2 = OutputVar("rstart_c2")
+ val rstart_c3 = OutputVar("rstart_c3")
+ val rstart_c4 = OutputVar("rstart_c4")
+ val rstart_c5 = OutputVar("rstart_c5")
+ val rstart_c6 = OutputVar("rstart_c6")
+ val rstart_c7 = OutputVar("rstart_c7")
+ val rstart_c8 = OutputVar("rstart_c8")
+ val rstart_c9 = OutputVar("rstart_c9")
+ val condition = (
+ ({val (proc, totProc, N) = (p1, P, N)
+ val modNtoProc = APAInputMod(N.toInputTerm(), totProc.toInputTerm())
+ (proc+rstart_c1 > modNtoProc +rstart_c2 && (proc-1+rstart_c3)*((N-1+rstart_c4)/totProc+rstart_c5-1)+modNtoProc+rstart_c6) ||
+ (proc+rstart_c1 <= modNtoProc +rstart_c2 && (proc-1+rstart_c7)*((N-1+rstart_c8)/totProc+rstart_c9-1))
+ }) &&
+ p1len === e1-s1 &&
+ p2len === e2-s2 &&
+ (p1len === p2len || p1len === p2len.toCombination() + 1 || p1len === p2len -1) &&
+ (p2 > p1+1 || p2 < p1+1 || s2===e1) &&
+ (p2 > p1-1 || p2 < p1-1 || e2===N) &&
+ (p1 > 0 || p1 < 0 || s1 === 0)
+ )
+ val solution = APASynthesis.solve("Armando", condition)
+ println(solution._1)
+ println(solution._2)
+ }*/
+
+ def OptimizedExample() {
+ val condition = (x+y === a+b && (b < x && x < y || a < y && y < x))
+ val solution = APASynthesis.solve("testnotdnf", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def extract7and8() {
+ val condition = (x*7+y*8+z*3 === a && x*2 >= y && y*2 >= z && z*2 >= x)
+ val solution = APASynthesis.solve("extract7and8", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def extractRatio() {
+ val condition = (y*b === c || y*c === b)
+ val solution = APASynthesis.solve("extractRatio", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+ def APAExample() {
+ val condition = (x*(-2)+y*a+1 <= 0 && x*b+y*3 + (-1) >= 0)
+ val solution = APASynthesis.solve("APAExample", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def multiArray() {
+ val x = I("x")
+ val y = I("y")
+ val c = O("c")
+ val i = O("i")
+ val j = O("j")
+ val condition = ((c + (i + j*640)*3 === x + y*1024) && c >= 0 && c < 3 && i >= 0 && i < 640 && j >= 0 && j < 480 && x >= 0 && x < 1024)
+ val solution = APASynthesis.solve("multiArray", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+
+ def paboucle() {
+ val a = I("a")
+ val condition = c - y <= a - x*6 && a - x*6 <= b + x + y*7 && x > y + z && z*9 <= x+y && z*5 > b + x + 8
+ val solution = APASynthesis.solve("paboucle", condition)
+ println(solution._1)
+ println(solution._2)
+ }
+}
diff --git a/src/main/scala/leon/synthesis/comfusy/Common.scala b/src/main/scala/leon/synthesis/comfusy/Common.scala
new file mode 100644
index 000000000..174171919
--- /dev/null
+++ b/src/main/scala/leon/synthesis/comfusy/Common.scala
@@ -0,0 +1,390 @@
+package leon.synthesis.comfusy
+
+object Common {
+
+ sealed abstract class BezoutType
+ case class OTBezout() extends BezoutType // Home-made
+ case class MMBezout() extends BezoutType // Made manually.
+
+ var computing_mode:BezoutType = MMBezout()
+
+ def bezout(e: Int, a : List[Int]):List[Int] = {
+ computing_mode match {
+ case OTBezout() => bezoutOT(e, a)
+ case MMBezout() => bezoutMM(a, e / gcdlist(a))
+ }
+ }
+ def bezoutWithBase(e: Int, a: List[Int]): (List[List[Int]]) = {
+ computing_mode match {
+ case OTBezout() => bezoutWithBaseOT(e, a)
+ case MMBezout() => bezoutWithBaseMM(e, a)
+ }
+ }
+
+ /** Shortcuts */
+ def bezout(e: Int, a : Int*): List[Int] = bezout(e, a.toList)
+ def bezoutWithBase(e: Int, a : Int*): List[List[Int]] = bezoutWithBase(e, a.toList)
+
+ /*
+ * Algorithms derived from the Omega-tests
+ */
+
+ // Finds a vector x such that x.a + e is 0 if this is possible.
+ def bezoutOT(e: Int, a : List[Int]):List[Int] = {
+ a match {
+ case Nil => Nil
+ case 0::Nil => 0::Nil
+ case k::Nil => ((-e + smod(e, k))/k) :: Nil
+ case a =>
+ val a_indexed:List[(Int, Int)] = (a.indices zip a).toList
+ (a_indexed find (_._2 == 0)) match {
+ case Some((index, element)) =>
+ // Takes the result when removing the zeros, then inserts some zeros.
+ val a_filtered = a filterNot (_==0)
+ val a_filtered_solved = bezoutOT(e, a_filtered )
+ val (_, a_solved) = a.foldLeft((a_filtered_solved, Nil:List[Int]))((_,_) match {
+ case ((q, l), 0) => (q, 0::l)
+ case ((Nil, l), k) => (Nil, l) // This should not happen, as we have many zeroes.
+ case ((a::q, l), k) => (q, a::l)
+ })
+ a_solved.reverse
+ case None =>
+ (a_indexed find {case a => Math.abs(a._2) == 1}) match {
+ case Some((index, element)) => // This is easy, like solving 4x+y+45z=30, just say that y=30 and other are zero
+ val sign = if(element > 0) 1 else -1
+ (a_indexed map { case (i, c) => if(i==index) -e/sign else 0 })
+ case None =>
+ val (index, min_coef) = a_indexed reduceLeft {
+ (_, _) match {
+ case (t1@(i, ci), t2@(j, cj)) => if(Math.abs(ci) < Math.abs(cj)) t1 else t2
+ }}
+ val min_coef_sign = if(min_coef > 0) 1 else -1
+ val abs_min_coef_plus_1 = Math.abs(min_coef) + 1
+ val e_assign = smod(e, abs_min_coef_plus_1)
+ val a_assign = abs_min_coef_plus_1 :: (a map {case k => smod(k, abs_min_coef_plus_1)})
+ // the coefficient at index 'index+1' is now 1 or -1.
+
+ val new_e = (e + Math.abs(min_coef) * (smod(e, abs_min_coef_plus_1)))/abs_min_coef_plus_1
+ val new_a = Math.abs(min_coef)::(a map {
+ case k => (k + Math.abs(min_coef) * (smod(k, abs_min_coef_plus_1)))/abs_min_coef_plus_1
+ })
+ // the coefficient at index 'index+1' is now 0, so it will be removed.
+
+ // Now, there is at least one zero in new_a
+ bezoutOT(new_e, new_a) match {
+ case Nil => throw new Error("Should not happen, the size of the input and output are the same")
+ case q@(w::l) =>
+ l.splitAt(index) match {
+ // The coefficient at index 'index' of l should be zero, we replace it by its assignment
+ case (left, 0::right) =>
+ val solution_a = scalarProduct(a_assign, q)
+ val solution = (solution_a + e_assign)*(min_coef_sign)
+ val result = left++(solution::right)
+ result
+ case (l, m) => throw new Error("The list "+l+" should have 0 at index "+index+" but this is not the case")
+ }
+ }
+ }
+ }
+ }
+ }
+
+ def enumerate[A](a: List[A]):List[(Int, A)] = (a.indices zip a).toList
+
+ // a is an indexed list
+ def replaceElementAtIndexByCoef(a: List[(Int, Int)], index: Int, coef: Int) = a map { _ match {
+ case (i, c) => if(i == index) coef else c
+ } }
+
+ // a is an indexed list
+ def replaceEverythingByCoef1ExceptCoef2AtIndex(a: List[(Int, Int)], coef1:Int, coef2: Int,index: Int): List[Int] =
+ a map { _ match {
+ case (i, c) if i == index => coef2
+ case _ => coef1
+ }
+ }
+
+ // a is an indexed list
+ def replaceEverythingByZeroExcept1AtIndex(a: List[(Int, Int)], index: Int): List[Int] =
+ replaceEverythingByCoef1ExceptCoef2AtIndex(a, 0, 1, index)
+
+ // a is an indexed list
+ def putCoef1AtIndex1andCoef2AtIndex2(a: List[(Int, Int)], coef1: Int, index1: Int, coef2: Int, index2: Int ):List[Int] = {
+ a map { _ match {
+ case (i, c) =>
+ if(i == index1) coef1
+ else if(i==index2) coef2
+ else 0
+ }
+ }
+ }
+
+ //insertPreviousZeros([a, b, 0, c, 0, d], [x, y, z, w]) = [x, y, 0, z, 0, d]
+ def insertPreviousZeros(list_with_zeros: List[Int], list_to_complete: List[Int]) :List[Int] = {
+ val (_, result) = list_with_zeros.foldLeft((list_to_complete, Nil: List[Int]))( (_, _) match {
+ case ((l, result), 0) => (l, 0::result)
+ case ((a::q, result), _) => (q, a::result)
+ })
+ result.reverse
+ }
+
+ def scalarProduct(a: List[Int], b:List[Int]): Int = {
+ (a zip b).foldLeft(0){case (result, (e_a, e_b)) => result + e_a * e_b}
+ }
+
+
+ // If size(a) == n, finds a matrix x of size n x n
+ // such that (1, k1, k2, .. kn-1).x.a + e = 0 if this is possible,
+ // and x describes all integer solutions of this equation. Rank(x) = n-1
+ // Output representation : it's the list of rows.
+ // n n n
+ def bezoutWithBaseOT(e: Int, a: List[Int]): (List[List[Int]]) = {
+ a match {
+ case Nil => Nil
+ case 0::Nil => ((0::Nil)::Nil)
+ case k::Nil => (((-e + smod(e, k))/k) :: Nil) :: Nil
+ case a =>
+ val a_indexed:List[(Int, Int)] = enumerate(a)
+ (a_indexed find (_._2 == 0)) match {
+ case Some((index, element)) =>
+ // Takes the result when removing the zeros, then inserts some zeros.
+ val a_filtered = a filterNot ( _ == 0 )
+ val solution = bezoutWithBase(e, a_filtered)
+ val (_, solution_completed) = a_indexed.foldLeft((solution, Nil:List[List[Int]]))((_,_) match {
+ case ((q, l), (i, 0)) => (q, replaceEverythingByZeroExcept1AtIndex(a_indexed, i)::l)
+ case ((Nil, l), (i, k)) => (Nil, l) // This should not happen, as we have many zeroes.
+ case ((b::q, l), (i, k)) => (q, insertPreviousZeros(a, b)::l)
+ })
+ // For each zero in a_indexed, add a new vector where 1 is at this position and it's zero everywhere else.
+ val new_vectors = a_indexed flatMap {
+ case (index, 0) => List(replaceEverythingByZeroExcept1AtIndex(a_indexed, index))
+ case t => Nil
+ }
+ solution_completed.reverse
+ case None =>
+ (a_indexed find {case a => Math.abs(a._2) == 1}) match {
+ case Some((index, element)) =>
+ // This is easy, like solving 4x+y+45z=30, just say that y=30 and other are zero
+ // For the vectors, just take the other variables as themselves.
+ val neg_sign = if(element > 0) -1 else 1
+ replaceEverythingByCoef1ExceptCoef2AtIndex(a_indexed, 0, neg_sign*e, index) ::
+ (a_indexed flatMap ( _ match {
+ case (i, c) =>
+ if(i == index)
+ Nil
+ else
+ List(putCoef1AtIndex1andCoef2AtIndex2(a_indexed, 1, i, neg_sign*c, index))
+ }))
+ case None =>
+ val (index, min_coef) = a_indexed reduceLeft {
+ (_, _) match {
+ case (t1@(i, ci), t2@(j, cj)) => if(Math.abs(ci) < Math.abs(cj)) t1 else t2
+ }}
+ val min_coef_sign = if(min_coef > 0) 1 else -1
+ val min_coef_sign2 = if(min_coef > 0) -1 else 1
+ val abs_min_coef_plus_1 = Math.abs(min_coef) + 1
+ val e_assign = smod(e, abs_min_coef_plus_1)
+ val a_assign = abs_min_coef_plus_1 :: (a map {case k => smod(k, abs_min_coef_plus_1)})
+ // the coefficient at index 'index+1' is now 1 or -1.
+
+ val new_e = (e + Math.abs(min_coef) * (smod(e, abs_min_coef_plus_1)))/abs_min_coef_plus_1
+ val new_a = Math.abs(min_coef)::(a map {
+ case k => (k + Math.abs(min_coef) * (smod(k, abs_min_coef_plus_1)))/abs_min_coef_plus_1
+ })
+ // the coefficient at index 'index+1' is now 0, so it will be removed.
+
+ // Now, there is at least one zero in new_a
+ bezoutWithBase(new_e, new_a) match {
+ case Nil => throw new Error("Should not happen as the input was not empty")
+ case v =>
+ val v_reduced = enumerate(v) flatMap {
+ case (i, Nil) => throw new Error("Should not happen as the input was not empty")
+ case (i, vs@(a::q)) =>
+ if(i == index +1) // We drop the line indicated by index
+ Nil
+ else {
+ val vs_replaced = replaceElementAtIndexByCoef(enumerate(vs), index+1, 0)
+ if(i==0) {
+ val new_element = (e_assign+scalarProduct(a_assign, vs_replaced)) * min_coef_sign
+ List(replaceElementAtIndexByCoef(enumerate(q), index, new_element))
+ } else {
+ val new_element = (scalarProduct(a_assign, vs_replaced)) * min_coef_sign
+ List(replaceElementAtIndexByCoef(enumerate(q), index, new_element))
+ }
+ }
+ }
+ v_reduced
+ }
+ }
+ }
+ }
+ }
+
+ /*
+ * Hand-made algorithms.
+ */
+
+ // Finds (x1, x2, k) such that x1.a + x2.b + gcd(a,b) = 0 and k =
+ // gcd(a ,b)
+ def advancedEuclid(a_in: Int, b_in: Int):(Int, Int, Int) = {
+ var (x, lastx) = (0, 1)
+ var (y, lasty) = (1, 0)
+ var (a, b) = (a_in, b_in)
+ var (quotient, temp) = (0, 0)
+ while(b != 0) {
+ val amodb = (Math.abs(b) + a%b)%b
+ quotient = (a - amodb)/b
+ a = b
+ b = amodb
+ temp = x
+ x = lastx-quotient*x
+ lastx = temp
+ temp = y
+ y = lasty-quotient*y
+ lasty = temp
+ }
+ if(a < 0)
+ return (lastx, lasty, -a)
+ else
+ return (-lastx, -lasty, a)
+ }
+
+ // Finds coefficients x such that k*gcd(a_in) + x.a_in = 0
+ def bezoutMM(a_in: List[Int], k: Int):List[Int] = {
+ var a = a_in
+ var a_in_gcds = a_in.foldRight(Nil:List[Int]){
+ case (i, Nil) => List(i)
+ case (i, a::q) => gcd(a, i)::a::q
+ }
+ var result:List[Int] = Nil
+ var last_coef = -1
+ while(a != Nil) {
+ a match {
+ case Nil =>
+ case 0::Nil =>
+ result = 0::result
+ a = Nil
+ case el::Nil =>
+ // Solution is -el/abs(el)
+ result = (k*(-last_coef * (-el/Math.abs(el))))::result
+ a = Nil
+ case (el1::el2::Nil) =>
+ val (u, v, _) = advancedEuclid(el1, el2)
+ result = (-v*k*last_coef)::(-u*k*last_coef)::result
+ a = Nil
+ case (el1::q) =>
+ val el2 = a_in_gcds.tail.head
+ val (u, v, _) = advancedEuclid(el1, el2)
+ result = (-u*k*last_coef)::result
+ last_coef = -v*last_coef
+ a = q
+ a_in_gcds = a_in_gcds.tail
+ }
+ }
+ result.reverse
+ }
+
+ // Finds coefficients x such that gcd(a_in) + x.a_in = 0
+ def bezoutMM(a_in: List[Int]):List[Int] = bezoutMM(a_in, 1)
+
+
+ def bezoutWithBaseMM(e: Int, a: List[Int]): (List[List[Int]]) = {
+ var coefs = a
+ var coefs_gcd = coefs.foldRight(Nil:List[Int]){
+ case (i, Nil) => List(Math.abs(i))
+ case (i, a::q) => gcd(a, i)::a::q
+ }
+ var n = a.length
+ var result = List(bezoutMM(a, e/coefs_gcd.head)) // The gcd of all coefs divides e.
+ var i = 1
+ var zeros:List[Int] = Nil
+ while(i <= n-1) {
+ val kii = coefs_gcd.tail.head / coefs_gcd.head
+ val kijs = bezoutMM(coefs.tail, coefs.head/coefs_gcd.head)
+ result = (zeros ::: (kii :: kijs))::result
+ coefs = coefs.tail
+ coefs_gcd = coefs_gcd.tail
+ zeros = 0::zeros
+ i += 1
+ }
+ result.reverse
+ }
+
+ class MatrixIterator(val m: List[List[Int]]) {
+ private var l:List[Int] = m.flatten
+ def next: Int = {
+ val result = l.head
+ l = l.tail
+ result
+ }
+ }
+
+ def smod(x:Int, m_signed:Int) = {
+ val m = Math.abs(m_signed)
+ val c = x % m
+ if(c >= (m+1)/2)
+ c - m
+ else if(c < -m/2)
+ c + m
+ else c
+ }
+
+ // Computes the GCD between two numbers
+ // Unsafe if y = -2^31
+ def gcd(x:Int, y:Int): Int = {
+ if (x==0) Math.abs(y)
+ else if (x<0) gcd(-x, y)
+ else if (y<0) gcd(x, -y)
+ else gcd(y%x, x)
+ }
+
+ // Computes the GCD between two numbers. Binary speed-up.
+ def binaryGcd(a:Int, b:Int):Int = {
+ var g = 1
+ var (u, v) = (a, b)
+ while(u%2 == 0 && v%2 == 0) {
+ u = u/2
+ v = v/2
+ g = 2*g
+ }
+ while(u != 0) {
+ if(u % 2 == 0) u = u/2
+ else if(v % 2 == 0) v = v/2
+ else {
+ val t = Math.abs(u-v)/2
+ if(u >= v) u = t else v = t
+ }
+ }
+ return g*v;
+ }
+
+ // Computes the LCM between two numbers
+ def lcm(x: Int, y: Int): Int = {
+ if(x < 0) lcm(-x, y)
+ else if(y < 0) lcm(x, -y)
+ else x * y / gcd(x, y)
+ }
+ // Computes the LCM over a list of numbers
+ // Do not handle correctly zero numbers.
+ def lcmlist(l:List[Int]):Int = l match {
+ case Nil => 1
+ case 0::q => lcmlist(q)
+ case a::Nil => if(a < 0) -a else a
+ case (a::b::q) => lcmlist(lcm(a,b)::q)
+ }
+ // Computes the GCD over a list of numbers
+ // Do not handle zero numbers.
+ def gcdlist(l:List[Int]):Int = l match {
+ case Nil => throw new Exception("Cannot compute GCD of nothing")
+ case 0::Nil => throw new Exception("Cannot compute GCD of zero")
+ case a::Nil => if(a < 0) -a else a
+ case (a::b::q) => gcdlist(gcd(a,b)::q)
+ }
+ // None represents infinity
+ def gcdlistComplete(l:List[Int]):Option[Int] = l match {
+ case Nil => None
+ case 0::q => gcdlistComplete(q)
+ case a::Nil => if(a < 0) Some(-a) else Some(a)
+ case (a::b::q) => gcdlistComplete(gcd(a, b)::q)
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala
new file mode 100644
index 000000000..7b2dbf7ac
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala
@@ -0,0 +1,556 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+
+import scala.annotation.tailrec
+import scala.collection.mutable.ListBuffer
+import evaluators.AbstractEvaluator
+import purescala.Definitions._
+import purescala.Common._
+import purescala.Types._
+import purescala.Constructors._
+import purescala.Expressions._
+import purescala.Extractors._
+import purescala.TypeOps
+import purescala.DefOps
+import purescala.ExprOps
+import purescala.SelfPrettyPrinter
+import solvers.ModelBuilder
+import solvers.string.StringSolver
+import programsets.DirectProgramSet
+import programsets.JoinProgramSet
+import leon.synthesis.comfusy._
+import leon.utils.Bijection
+
+class VarContext(val inputVariables: Set[Identifier], val outputVariables: Set[Identifier], val sctx: SearchContext) {
+ private var idToInputVar = new Bijection[Identifier, InputVar]
+ private var idToOutputVar = new Bijection[Identifier, OutputVar]
+
+ def getInputVar(id: Identifier): InputVar = {
+ idToInputVar.cachedB(id){
+ var i = 0
+ while(idToInputVar.containsB(InputVar(id.name + i))) i+=1
+ InputVar(id.name + i)
+ }
+ }
+
+ def getOutputVar(id: Identifier): OutputVar = {
+ idToOutputVar.cachedB(id){
+ var i = 0
+ while(idToOutputVar.containsB(OutputVar(id.name + i))) i+=1
+ OutputVar(id.name + i)
+ }
+ }
+
+ def getIdentifier(iv: InputVar): Identifier= {
+ idToInputVar.cachedA(iv){
+ FreshIdentifier(iv.name, IntegerType, false)
+ }
+ }
+
+ def getIdentifier(ov: OutputVar): Identifier= {
+ idToOutputVar.cachedA(ov){
+ FreshIdentifier(ov.name, IntegerType, false)
+ }
+ }
+
+ def newIdentifierName(init: String = ""): String = {
+ for(i <- 0 until 26) {
+ val c = init + ('a'.toInt + i).toChar.toString
+ if(idToInputVar.iterator.forall(_._1.name != c) && idToOutputVar.iterator.forall(_._1.name != c)) {
+ return c
+ }
+ }
+ newIdentifierName(init + "a")
+ }
+}
+
+case class NotInputVarException(msg: String) extends Exception(msg)
+
+object ComfusyConverters {
+
+ def convertToAPAInputTerm(e: Expr)(implicit vc: VarContext): APAInputTerm = e match {
+ case Plus(a, b) => convertToAPAInputTerm(a) + convertToAPAInputTerm(b)
+ case Minus(a, b) => convertToAPAInputTerm(a) - convertToAPAInputTerm(b)
+ case UMinus(a) => -convertToAPAInputTerm(a)
+ case Times(a, b) => convertToAPAInputTerm(a) * convertToAPAInputTerm(b)
+ case Division(a, b) => convertToAPAInputTerm(a) / convertToAPAInputTerm(b).assumeNotZero()
+ case purescala.Expressions.Assert(_, Some("Division by zero"), a) => convertToAPAInputTerm(a)
+ case IfExpr(LessEquals(a1, InfiniteIntegerLiteral(zero)), UMinus(a2), a3) if a1 == a2 && a2 == a3 && zero == BigInt(0) => APAInputAbs(convertToAPAInputTerm(a1))
+ //APAInputMod is not supported in Comfusy
+ case Variable(i) if vc.inputVariables contains i => APAInputCombination(0, (1, vc.getInputVar(i))::Nil)
+ case InfiniteIntegerLiteral(k) => APAInputCombination(k.toInt, Nil)
+ case _ => throw NotInputVarException(s"$e is not an input variable. Only + / * - and ${vc.inputVariables.mkString(",")} are allowed")
+ }
+
+ def convertToAPACombination(e: Expr)(implicit vc: VarContext): APACombination = e match {
+ case Plus(a, b) => convertToAPACombination(a) + convertToAPACombination(b)
+ case Minus(a, b) => convertToAPACombination(a) - convertToAPACombination(b)
+ case UMinus(a) => -convertToAPACombination(a)
+ case Times(a, b) =>
+ if(isInputVarParsable(a)) {
+ convertToAPAInputTerm(a) * convertToAPACombination(b)
+ } else {
+ convertToAPAInputTerm(b) * convertToAPACombination(a)
+ }
+ case Division(a, b) =>
+ convertToAPACombination(a) / convertToAPAInputTerm(b)
+ case Variable(i) if vc.outputVariables contains i =>
+ APACombination(APAInputCombination(0), (APAInputCombination(1), vc.getOutputVar(i))::Nil)
+ case e => APACombination(convertToAPAInputTerm(e), Nil)
+ }
+ def convertToAPAEqualZero(e: Equals)(implicit vc: VarContext) = {
+ APAEqualZero(convertToAPACombination(e.lhs) - convertToAPACombination(e.rhs))
+ }
+
+ def isInputVarParsable(e: Expr)(implicit vc: VarContext): Boolean = {
+ def aux(e: Expr): Boolean = e match {
+ case Plus(a, b) => aux(a) && aux(b)
+ case Minus(a, b) => aux(a) && aux(b)
+ case UMinus(a) => aux(a)
+ case Times(a, b) => aux(a) && aux(b)
+ case Division(a, b) => aux(a) && aux(b)
+ case purescala.Expressions.Assert(_, Some("Division by zero"), a) => aux(a)
+ //case Remainder(a, b) => aux(a) && aux(b)
+ //case Modulo(a, b) => aux(a) && aux(b)
+ case Variable(i) => vc.inputVariables contains i
+ case InfiniteIntegerLiteral(k) => true
+ case _ => false
+ }
+ aux(e)
+ }
+
+ def isLinInOutputVariables(e: Expr)(implicit vc: VarContext): Boolean = {
+ def aux(e: Expr): Boolean = e match {
+ case Plus(a, b) => aux(a) && aux(b)
+ case Minus(a, b) => aux(a) && aux(b)
+ case UMinus(a) => aux(a)
+ case Times(a, b) => (isInputVarParsable(a) && isLinInOutputVariables(b)) ||
+ (isInputVarParsable(b) && isLinInOutputVariables(a))
+ case Division(a, b) => isInputVarParsable(b) && isLinInOutputVariables(a)
+ case Variable(i) => (vc.inputVariables contains i) || (vc.outputVariables contains i)
+ case InfiniteIntegerLiteral(k) => true
+ case _ => isInputVarParsable(e)
+ }
+ aux(e)
+ }
+
+ def isLinEqInOutputVariables(e: Expr)(implicit vc: VarContext): Boolean = {
+ e match {
+ case Equals(a, b) => isLinInOutputVariables(a) &&
+ isLinInOutputVariables(b)
+ }
+ }
+
+
+
+ def convertToSolution(cond: APACondition, prog: APAProgram)(implicit vc: VarContext): Solution = {
+ val precond: Expr = APAConditionToExpr(cond)
+ val term: Expr = APAProgramToExpr(prog, prog.output_variables)
+ Solution(precond, Set.empty, term)
+ }
+
+ def APACombinationToExpr(e: APACombination)(implicit vc: VarContext): Expr = e match {
+ case APACombination(coef, varsWithCoefs) => (APAInputTermToExpr(coef) /: varsWithCoefs) { (c: Expr, iv) =>
+ val (i, v) = iv
+ Plus(c, Times(APAInputTermToExpr(i), Variable(vc.getIdentifier(v))))
+ }
+ }
+
+ def APAFormulaToExpr(e: APAFormula)(implicit vc: VarContext): Expr = e match {
+ case e: APAEquation => APAEquationToExpr(e)
+ case APAConjunction(conjuncts) => And(conjuncts map APAFormulaToExpr)
+ case APADisjunction(conjuncts) => Or(conjuncts map APAFormulaToExpr)
+ case APANegation(formula) => Not(APAFormulaToExpr(formula))
+ }
+
+ def APAEquationToExpr(e: APAEquation)(implicit vc: VarContext): Expr = e match {
+ case APADivides(coefficient, pac) => Equals(Modulo(APACombinationToExpr(pac), APAInputTermToExpr(coefficient)), InfiniteIntegerLiteral(BigInt(0)))
+ case APAEqualZero(pac) => Equals(APACombinationToExpr(pac), InfiniteIntegerLiteral(BigInt(0)))
+ case APAGreaterZero(pac) => GreaterThan(APACombinationToExpr(pac), InfiniteIntegerLiteral(BigInt(0)))
+ case APAGreaterEqZero(pac) => GreaterEquals(APACombinationToExpr(pac), InfiniteIntegerLiteral(BigInt(0)))
+ case APATrue() => BooleanLiteral(true)
+ case APAFalse() => BooleanLiteral(false)
+ }
+
+ def InputAssignmentToExpr(input_assignment: InputAssignment)(implicit vc: VarContext): Expr => Expr = {
+ input_assignment match {
+ case SingleInputAssignment(iv, t) =>
+ (x: Expr) => Let(vc.getIdentifier(iv), APAInputTermToExpr(t), x)
+ case BezoutInputAssignment(vs, ts) =>
+ val tsConverted = ts map APAInputTermToExpr
+ import vc.sctx.program.library.{ List => LeonList, Cons => LeonCons, Nil => LeonNil }
+ val listType = LeonList.get
+ val applyfun = vc.sctx.program.library.lookupUnique[FunDef]("leon.collection.List.apply")
+ val bezoutWithBase = vc.sctx.program.library.bezoutWithBase.get
+ val b = FreshIdentifier(vc.newIdentifierName(), listType.typed(Seq(listType.typed(Seq(IntegerType)))), false)
+ val decomposed: List[Expr => Expr] = vs.zipWithIndex.map{ case (lv, i) =>
+ lv.zipWithIndex.map { case (v, j) =>
+ (w: Expr) =>
+ Let(vc.getIdentifier(v),
+ functionInvocation(applyfun, Seq(
+ functionInvocation(applyfun, Seq(Variable(b), InfiniteIntegerLiteral(BigInt(i)))),
+ InfiniteIntegerLiteral(BigInt(j)))), w)
+ }
+ }.flatten
+ val decomposed_recomposed = decomposed.reduce(_ compose _)
+ val tsConvertedToList = (tsConverted :\ (CaseClass(CaseClassType(LeonNil.get, Seq(IntegerType)), Seq()): Expr)) {
+ (v, l) =>
+ CaseClass(CaseClassType(LeonCons.get, Seq(IntegerType)), Seq(v, l))
+ }
+ val initial_fun = (x: Expr) => Let(b, functionInvocation(bezoutWithBase, Seq(InfiniteIntegerLiteral(BigInt(1)), tsConvertedToList)), x)
+ initial_fun compose decomposed_recomposed
+ }
+ }
+
+ def APASplitConditionToExpr(sc: APASplitCondition)(implicit vc: VarContext): Expr = sc match {
+ case APAEmptySplitCondition() => BooleanLiteral(true)
+ case APACaseSplitCondition(Nil) => BooleanLiteral(true)
+ case APACaseSplitCondition(a::Nil) => APAAbstractConditionToExpr(a)
+ case APACaseSplitCondition(csl) => Or(csl.map(e => APAAbstractConditionToExpr(e)))
+ case APAForCondition(vl, lower_range, upper_range, global_condition) =>
+ val range = vc.sctx.program.library.lookupUnique[FunDef]("leon.collection.List.range")
+ val flatMap = vc.sctx.program.library.lookupUnique[FunDef]("leon.collection.List.flatMap")
+ val map = vc.sctx.program.library.lookupUnique[FunDef]("leon.collection.List.map")
+ val exists = vc.sctx.program.library.lookupUnique[FunDef]("leon.collection.List.exists")
+ val basic_range = functionInvocation(range, Seq(APAInputTermToExpr(lower_range), APAInputTermToExpr(upper_range)))
+ var ranges = basic_range
+ var tupleType: TypeTree = IntegerType
+ vl.tail foreach { k =>
+ val t = FreshIdentifier("t", IntegerType)
+ val i = FreshIdentifier("i", IntegerType)
+ ranges = functionInvocation(flatMap, Seq(ranges, Lambda(Seq(ValDef(t)),
+ functionInvocation(map, Seq(basic_range, Lambda(Seq(ValDef(i)), tupleWrap(Seq(Variable(i), Variable(t)))))))))
+ tupleType = TupleType(Seq(IntegerType, tupleType))
+ }
+ def getPattern(i: InputVar): Pattern = WildcardPattern(Some(vc.getIdentifier(i)))
+ val tuplePattern = (vl.init :\ getPattern(vl.last)) {
+ case (v, p) => tuplePatternWrap(Seq(getPattern(v), p))
+ }
+
+ val evars = FreshIdentifier("evars", tupleType)
+ functionInvocation(exists, Seq(ranges,
+ Lambda(Seq(ValDef(evars)),
+ MatchExpr(Variable(evars),
+ Seq(MatchCase(tuplePattern, None, APAConditionToExpr(global_condition)))))
+ ))
+ }
+
+ def APAAbstractConditionToExpr(cond: APAAbstractCondition)(implicit vc: VarContext): Expr = {
+ cond match {
+ case c: APACondition => APAConditionToExpr(c)
+ case s: APASplitCondition => APASplitConditionToExpr(s)
+ }
+ }
+
+ def ListOutputAssignmentToExpr(l: List[(OutputVar, APATerm)])(implicit vc: VarContext): Expr => Expr = {
+ val outputAssignments = if(l.isEmpty) None
+ else Some((l map (e => (x: Expr) => Let(vc.getIdentifier(e._1), APATermToExpr(e._2), x))) reduce (_ compose _))
+ (e: Expr) => outputAssignments.map(f => f(e)).getOrElse(e)
+ }
+
+ def ListInputAssignmentToExpr(l: List[InputAssignment])(implicit vc: VarContext): Expr => Expr = {
+ val inputAssignments = if(l.isEmpty) None
+ else Some((l map (e => InputAssignmentToExpr(e))) reduce (_ compose _))
+ (e: Expr) => inputAssignments.map(f => f(e)).getOrElse(e)
+ }
+
+ def APAConditionToExpr(cond: APACondition)(implicit vc: VarContext): Expr = {
+ val assigns = ListInputAssignmentToExpr(cond.input_assignment)
+ val g = APAFormulaToExpr(cond.global_condition)
+ if(cond.isTrivial) {
+ BooleanLiteral(true)
+ } else {
+ cond.pf match {
+ case APAEmptySplitCondition() =>
+ assigns(g)
+ case _ => // There are some more splits.
+ if(g == BooleanLiteral(true)) {
+ assigns(APASplitConditionToExpr(cond.pf))
+ } else {
+ assigns(And(g, APASplitConditionToExpr(cond.pf)))
+ }
+ }
+ }
+ }
+
+ def APAProgramToExpr(prog: APAProgram, expected_output_vars: List[OutputVar])(implicit vc: VarContext): Expr = {
+ val assigns = ListInputAssignmentToExpr(prog.input_assignment)
+ val affectedOutputVariables = prog.output_assignment.map(_._1).toSet
+ val referedOutputVariables = (expected_output_vars ++ prog.output_assignment.flatMap(_._2.output_variables)) filterNot affectedOutputVariables
+ val assignMiddle = APASplitToExpr(prog.case_splits, referedOutputVariables)
+ val assigns2 = ListOutputAssignmentToExpr(prog.output_assignment)
+ val output_expr = tupleWrap(expected_output_vars.map(ov => Variable(vc.getIdentifier(ov))))
+ assigns(assignMiddle(assigns2(output_expr)))
+ }
+
+ def conditionProgramToIfExpr(p: (APACondition, APAProgram), expected_output: List[OutputVar])(implicit vc: VarContext): Expr => Expr = {
+ val subprogram = APAProgramToExpr(p._2, expected_output)
+ (els: Expr) => IfExpr(APAConditionToExpr(p._1), subprogram, els)
+ }
+
+ def APASplitToExpr(p: APASplit, expected_output: List[OutputVar])(implicit vc: VarContext): Expr => Expr = p match {
+ case APAFalseSplit() => Let(FreshIdentifier("wrong", UnitType), NoTree(tupleTypeWrap(expected_output.map(_ => IntegerType))), _)
+ case APAEmptySplit() => e => e
+ case APACaseSplit(conditionPrograms) =>
+ val cps = conditionPrograms map (cp => conditionProgramToIfExpr(cp, expected_output))
+ if(cps.isEmpty) e => e
+ else {
+ val composition = cps.reduce(_ compose _)
+ (x: Expr) => letTuple(expected_output.map(vc.getIdentifier),
+ composition(Error(tupleTypeWrap(expected_output.map((ov: OutputVar) => IntegerType)), "Unreachable case")), x)
+ }
+ case APAForSplit(vl: List[InputVar], lower_range: APAInputTerm, upper_range: APAInputTerm, condition: APACondition, program: APAProgram) =>
+ import vc.sctx.program.library.{None => LeonNone, Some => LeonSome, List => LeonList, Cons => LeonCons, Nil => LeonNil, _}
+ val range = lookupUnique[FunDef]("leon.collection.List.range")
+ val flatMap = lookupUnique[FunDef]("leon.collection.List.flatMap")
+ val map = lookupUnique[FunDef]("leon.collection.List.map")
+ val find = lookupUnique[FunDef]("leon.collection.List.find")
+ val get = lookupUnique[FunDef]("leon.collection.Option.get")
+ val basic_range = functionInvocation(range, Seq(APAInputTermToExpr(lower_range), APAInputTermToExpr(upper_range)))
+ var ranges = basic_range
+ var tupleType: TypeTree = IntegerType
+ vl.tail foreach { k =>
+ val t = FreshIdentifier("t", IntegerType)
+ val i = FreshIdentifier("i", IntegerType)
+ ranges = functionInvocation(flatMap, Seq(ranges, Lambda(Seq(ValDef(t)),
+ functionInvocation(map, Seq(basic_range, Lambda(Seq(ValDef(i)), tupleWrap(Seq(Variable(i), Variable(t)))))))))
+ tupleType = TupleType(Seq(IntegerType, tupleType))
+ }
+ def getPattern(i: InputVar): Pattern = WildcardPattern(scala.Some(vc.getIdentifier(i)))
+ val tuplePattern = (vl.init :\ getPattern(vl.last)) {
+ case (v, p) => tuplePatternWrap(Seq(getPattern(v), p))
+ }
+
+ val evars = FreshIdentifier("evars", tupleType)
+ val findExpr = functionInvocation(find, Seq(ranges,
+ Lambda(Seq(ValDef(evars)),
+ MatchExpr(Variable(evars),
+ Seq(MatchCase(tuplePattern, scala.None, APAConditionToExpr(condition)))))
+ ))
+ val finalExpr = functionInvocation(get, Seq(findExpr))
+ (x: Expr) => letTuple(expected_output.map(vc.getIdentifier), finalExpr, x)
+ }
+
+ def APATermToExpr(e: APATerm)(implicit vc: VarContext): Expr = e match {
+ case APADivision(n, d) => Division(APACombinationToExpr(n), APAInputTermToExpr(d))
+ case APAMinimum(l) => l match {
+ case Nil => throw new Exception("Minimum of nothing")
+ case a::Nil => APATermToExpr(a)
+ case l =>
+ val minDef = vc.sctx.program.library.lookup("leon.math.min").collect{
+ case fd: FunDef => fd
+ }.filter { fd => fd.paramIds.head.getType == IntegerType }.head
+
+ (l.init :\ APATermToExpr(l.last)) { (v, res) =>
+ functionInvocation(minDef, Seq(APATermToExpr(v), res))
+ }
+ }
+ case APAMaximum(l) => l match {
+ case Nil => throw new Exception("Maximum of nothing")
+ case a::Nil => APATermToExpr(a)
+ case l =>
+ val maxDef = vc.sctx.program.library.lookup("leon.math.max").collect{
+ case fd: FunDef => fd
+ }.filter { fd => fd.paramIds.head.getType == IntegerType }.head
+
+ (l.init :\ APATermToExpr(l.last)) { (v, res) =>
+ functionInvocation(maxDef, Seq(APATermToExpr(v), res))
+ }
+ }
+ case a: APACombination =>
+ APACombinationToExpr(a)
+ }
+ def APAInputTermToExpr(t: APAInputTerm)(implicit vc: VarContext): Expr = t match {
+ case APAInputCombination(coef, input_linear) =>
+ ((InfiniteIntegerLiteral(BigInt(coef)): Expr) /: input_linear) { (c: Expr, iv) =>
+ val (i, v) = iv
+ val newTerm = if( i == BigInt(1) )
+ Variable(vc.getIdentifier(v))
+ else
+ Times(InfiniteIntegerLiteral(i), Variable(vc.getIdentifier(v)))
+ if( c == InfiniteIntegerLiteral(BigInt(0)))
+ newTerm
+ else
+ Plus(c, newTerm)
+ }
+ case APAInputDivision(numerator, denominator) =>
+ Division(APAInputTermToExpr(APAInputMultiplication(numerator)), APAInputTermToExpr(APAInputMultiplication(denominator)))
+ case APAInputMultiplication(operands) =>
+ val v = (operands map APAInputTermToExpr)
+ v match {
+ case Nil => InfiniteIntegerLiteral(1)
+ case a::Nil => a
+ case l => l.reduce(Times)
+ }
+ case APAInputAddition(operands) =>
+ val v = (operands map APAInputTermToExpr)
+ v match {
+ case Nil => InfiniteIntegerLiteral(0)
+ case a::Nil => a
+ case l => l.reduce(Plus)
+ }
+ case APAInputAbs(a) =>
+ val absFun = vc.sctx.program.library.lookupUnique[FunDef]("leon.math.abs")
+ functionInvocation(absFun, Seq(APAInputTermToExpr(a)))
+
+ case APAInputGCD(List(a)) =>
+ APAInputTermToExpr(APAInputAbs(a))
+
+ case APAInputGCD(numbers@List(a, b)) =>
+ import vc.sctx.program.library._
+ val gcdFun = lookupUnique[FunDef]("leon.math.gcd")
+ val args = numbers map APAInputTermToExpr
+ functionInvocation(gcdFun, args)
+
+ case APAInputGCD(numbers) =>
+ import vc.sctx.program.library._
+ val gcdFun = lookupUnique[FunDef]("leon.math.gcdlist")
+ val args = numbers map APAInputTermToExpr
+ val l = (args :\ (CaseClass(CaseClassType(Nil.get, Seq(IntegerType)), Seq()): Expr)) { (v, l) =>
+ CaseClass(CaseClassType(Cons.get, Seq(IntegerType)), Seq(v, l))
+ }
+ functionInvocation(gcdFun, Seq(l))
+
+ case APAInputLCM(List(a)) =>
+ APAInputTermToExpr(APAInputAbs(a))
+
+ case APAInputLCM(numbers@List(a, b)) =>
+ import vc.sctx.program.library._
+ val lcmFun = lookupUnique[FunDef]("leon.math.lcm")
+ val args = numbers map APAInputTermToExpr
+ functionInvocation(lcmFun, args)
+
+ case APAInputLCM(numbers) =>
+ import vc.sctx.program.library._
+ val lcmFun = lookupUnique[FunDef]("leon.math.lcmlist")
+ val args = numbers map APAInputTermToExpr
+ val l = (args :\ (CaseClass(CaseClassType(Nil.get, Seq(IntegerType)), Seq()): Expr)) { (v, l) =>
+ CaseClass(CaseClassType(Cons.get, Seq(IntegerType)), Seq(v, l))
+ }
+ functionInvocation(lcmFun, Seq(l))
+ }
+}
+
+case object IntegerEquality extends Rule("Solve integer equality"){
+
+ import ComfusyConverters._
+
+ object Flatten {
+ def unapply(e: Expr): Option[Expr] = e match {
+ case v: Variable => Some(v)
+ case Tuple(vs) => Some(Tuple(vs.map(e => Flatten.unapply(e).getOrElse(return None))))
+ case TupleSelect(Flatten(e), n) => Some(TupleSelect(e, n))
+ case Let(i, Flatten(e), Variable(i2)) if i2 == i => Some(e)
+ case Let(i, Flatten(e), Tuple(seq))
+ if seq.zipWithIndex.forall{
+ case (TupleSelect(Flatten(Variable(i2)), n), nm1) if nm1 + 1 == n && i2 == i => true case _ => false } =>
+ Some(e)
+ case LetTuple(is, Flatten(e), Tuple(vs)) if vs.toList == is.map(Variable) => Some(e)
+ case _ => None
+ }
+
+ }
+
+ object GetOutputVariables {
+ def unapply(e: Expr)(implicit p: Problem): Option[(Seq[Expr], Seq[Identifier])] =
+ rec(e, p.xs.map(Variable))
+
+ def rec(e: Expr, originOutputVariables: Seq[Expr]): Option[(Seq[Expr], Seq[Identifier])] = {
+ //println(s"Reducing $e under $originOutputVariables")
+ e} match {
+ case Let(i, Flatten(j), b) =>
+ val k = originOutputVariables.indexOf(j)
+ if(k == -1) { // Maybe j is a TupleSelect, in which case we need to expand the corresponding originOutputVariable
+ val varsOfJ = ExprOps.variablesOf(j)
+ val newOutputvariables= originOutputVariables.flatMap(ov =>
+ ov.getType match {
+ case t: TupleType if ExprOps.exists{ case Variable(m) if varsOfJ(m) => true case _ => false }(ov) =>
+ t.bases.indices.map(i => TupleSelect(ov, i + 1))
+ case _ => List(ov)
+ }
+ )
+ if(originOutputVariables != newOutputvariables) {
+ rec(e, newOutputvariables)
+ } else {
+ // Maybe j is a tuple of variable, in which case we are going to replace i._m by the corresponding variable.
+ j match {
+ case Tuple(values) if values.forall(_.isInstanceOf[Variable])=>
+ val newB =
+ ExprOps.preMap{
+ case TupleSelect(Variable(ii), n) if ii == i => Some(values(n - 1))
+ case _ => None
+ }(b)
+ if( b != newB ) {
+ rec(newB, originOutputVariables)
+ } else {
+ //println(s"Was not able 2 reduce the expression $e with input variables $originOutputVariables")
+ None
+ }
+ case _ =>
+ //println(s"Was not able to reduce the expression $e with input variables $originOutputVariables")
+ None
+ }
+
+ }
+ } else {
+ rec(b, originOutputVariables.take(k) ++ Seq(Variable(i)) ++ originOutputVariables.drop(k+1))
+ }
+ case LetTuple(is, Flatten(res), b) =>
+ val k = originOutputVariables.indexOf(res)
+ if (k >= 0) {
+ val newOriginOutputVariables =
+ originOutputVariables.take(k) ++ is.map(Variable) ++ originOutputVariables.drop(k+1)
+ rec(b, newOriginOutputVariables)
+ } else {
+ //println(s"Was not able to reduce $e under input variables $originOutputVariables")
+ None
+ }
+ // Now it's possible that j is a tuple select so let's try this
+ case TopLevelAnds(conjuncts) =>
+ val finalReturnVariables = originOutputVariables.map{
+ case Variable(x) => x
+ case e =>
+ //println(s"This is not an output variable: $e")
+ return None
+ }
+ Some((conjuncts, finalReturnVariables))
+ case _ =>
+ //println("Was not able to simplify the expression " + e)
+ None
+ }
+ }
+
+ def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ p.phi match {
+ case GetOutputVariables(conjuncts, outputVars) =>
+ implicit lazy val vc = new VarContext(p.as.toSet, outputVars.toSet, hctx)
+ val candidates: List[Equals] = conjuncts.toList collect {
+ case e: Equals => e
+ } filter { e => isLinEqInOutputVariables(e) }
+ //println(s"Candidates $conjuncts for $outputVars")
+ if(candidates.isEmpty) {
+ //println("No candidates for integer equality. Got " + conjuncts)
+ Nil
+ } else {
+ val realCandidates = candidates map (e => convertToAPAEqualZero(e)) sortWith APASynthesis.by_least_outputvar_coef
+ val problem = new APASynthesis(FormulaSplit(realCandidates, Nil, Stream.empty),
+ p.as.toList.map(vc.getInputVar), outputVars.toList.map(vc.getOutputVar))
+ List(RuleInstantiation("Solve integer equalities") {
+ //println(s"Solve problem ${realCandidates}")
+ val (cond, prog) = problem.solve()
+ //println(s"Solution condition = $cond under program = $prog")
+ val solution = convertToSolution(cond, prog)
+ //println(s"Rendered to $solution")
+ RuleClosed(solution)
+ })
+ }
+ case _ =>
+ //println("Not parsable as equation with conjuncts")
+ Nil
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 3e9b99c88..fed2a6a48 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -31,6 +31,8 @@ case class Library(pgm: Program) {
lazy val setMkString = lookup("leon.lang.Set.mkString").collectFirst { case fd : FunDef => fd }
lazy val bagMkString = lookup("leon.lang.Bag.mkString").collectFirst { case fd : FunDef => fd }
+
+ lazy val bezoutWithBase = lookup("leon.math.bezoutWithBase").collectFirst { case fd : FunDef => fd }
def lookup(name: String): Seq[Definition] = {
pgm.lookupAll(name)