From 42899658309448acd823c246586ca6340ebc13e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 20 Jul 2016 11:30:08 +0200 Subject: [PATCH 1/8] Added compilable sources of comfusy --- .../synthesis/comfusy/APAAbstractions.scala | 372 ++++++++ .../leon/synthesis/comfusy/APACondition.scala | 287 +++++++ .../comfusy/APAInputAssignments.scala | 197 +++++ .../comfusy/APAInputSyntaxTree.scala | 721 ++++++++++++++++ .../leon/synthesis/comfusy/APAProgram.scala | 650 ++++++++++++++ .../synthesis/comfusy/APASyntaxTree.scala | 674 +++++++++++++++ .../leon/synthesis/comfusy/APASynthesis.scala | 807 ++++++++++++++++++ .../comfusy/APASynthesisExamples.scala | 277 ++++++ .../scala/leon/synthesis/comfusy/Common.scala | 390 +++++++++ 9 files changed, 4375 insertions(+) create mode 100644 src/main/scala/leon/synthesis/comfusy/APAAbstractions.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APACondition.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APAInputAssignments.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APAInputSyntaxTree.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APAProgram.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APASynthesis.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/APASynthesisExamples.scala create mode 100644 src/main/scala/leon/synthesis/comfusy/Common.scala 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..0b72115ea --- /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..2f1324c57 --- /dev/null +++ b/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala @@ -0,0 +1,674 @@ +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)}) + } + /** 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..5866bc0df --- /dev/null +++ b/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala @@ -0,0 +1,807 @@ +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) + } +} + +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 + } + } + + 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 + } + + /** 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)) + + + 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) + } + + 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) + } +} From 5fabaedac1c89116c28d5cc773a8baecf6a4bfad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 20 Jul 2016 18:54:06 +0200 Subject: [PATCH 2/8] Added comfusy for equalities. Not yet for abstract PA, but concrete is ok ! --- library/leon/math/package.scala | 239 +++++++++- .../scala/leon/purescala/Constructors.scala | 4 +- src/main/scala/leon/synthesis/Rules.scala | 1 + .../leon/synthesis/comfusy/APAProgram.scala | 4 +- .../synthesis/comfusy/APASyntaxTree.scala | 4 + .../leon/synthesis/comfusy/APASynthesis.scala | 39 +- .../synthesis/rules/IntegerEquality.scala | 421 ++++++++++++++++++ src/main/scala/leon/utils/Library.scala | 2 + 8 files changed, 689 insertions(+), 25 deletions(-) create mode 100644 src/main/scala/leon/synthesis/rules/IntegerEquality.scala diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala index 036d35771..e3a35a0da 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,243 @@ 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 + def isGCDable(l: List[BigInt]): Boolean = l match { + case Cons(x, b) if x == BigInt(0) => false + case Cons(a, b) => isGCDable(b) + case Nil() => true + } + + /** Computes the GCD between numbers */ + @library + 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(a, Cons(b, q)) => gcdlist(gcd(a,b)::q) + } + } + + /** Computes the LCM between numbers */ + @library + 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(a, Cons(b, q)) => lcmlist(lcm(a,b)::q) + } + } + + /** Computes the GCD between two numbers */ + @library + def gcd(x:BigInt, y:BigInt): BigInt = { + 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) + } + + /** Computes the LCM between two numbers */ + @library + def lcm(x: BigInt, y: BigInt): BigInt = { + x * y / gcd(x, y) + } + + /** 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 + def bezoutWithBase(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = { + 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 + def extendedEuclidFunc(a_in: BigInt, b_in: BigInt):(BigInt, BigInt, BigInt) = { + 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) + } + @library - def abs(n: BigInt) = if(n < 0) -n else n + def bezoutMMFunc(a_in: List[BigInt], k: BigInt):List[BigInt] = { + val a = a_in + val a_in_gcds = a_in.foldRight(List[BigInt]()){ (e: BigInt, v: List[BigInt]) => (e, v) match { + case (i, Nil()) => List(i) + case (i, a::q) => gcd(a, i)::a::q + } } + 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] = { + 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) + } + } + } + aux(a_in, a_in_gcds, result, last_coef) + } + + @library + def bezoutWithBaseMMFunc(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = { + val coefs = a + val coefs_gcd = coefs.foldRight(List[BigInt]()){ + case (i, Nil()) => List(abs(i)) + case (i, Cons(a, q)) => gcd(a, i)::a::q + } + 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]] = { + 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/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/APAProgram.scala b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala index 0b72115ea..9b624b0da 100644 --- a/src/main/scala/leon/synthesis/comfusy/APAProgram.scala +++ b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala @@ -511,14 +511,14 @@ case class APAProgram(input_variables: List[InputVar], 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 { + 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 = { + 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 { diff --git a/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala b/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala index 2f1324c57..ab146ebaf 100644 --- a/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala +++ b/src/main/scala/leon/synthesis/comfusy/APASyntaxTree.scala @@ -538,6 +538,10 @@ case class APACombination(const_part: APAInputTerm, output_linear: List[(APAInpu 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)}) diff --git a/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala b/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala index 5866bc0df..124d9807f 100644 --- a/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala +++ b/src/main/scala/leon/synthesis/comfusy/APASynthesis.scala @@ -186,6 +186,24 @@ object APASynthesis { 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]) { @@ -261,14 +279,7 @@ class APASynthesis(equations: FormulaSplit, input_variables_initial:List[InputVa case e => e.simplified::Nil } } - - 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 - } - + /** 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 @@ -277,18 +288,6 @@ class APASynthesis(equations: FormulaSplit, input_variables_initial:List[InputVa val (interesting_equalities, precondition_equalities) = equalities partition (_.has_output_variables) addPrecondition(APAConjunction(precondition_equalities)) - - 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) - } - val sorted_equalities = interesting_equalities sortWith by_least_outputvar_coef sorted_equalities match { 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..8752be48e --- /dev/null +++ b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala @@ -0,0 +1,421 @@ +/* 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) + } + } +} + +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) + 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 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("b", 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) + decomposed_recomposed compose initial_fun + } + } + + def APASplitConditionToExpr(sc: APASplitCondition)(implicit vc: VarContext): Expr = sc match { + case APAEmptySplitCondition() => BooleanLiteral(true) + 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 = 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 + Plus(c, Times(InfiniteIntegerLiteral(i), Variable(vc.getIdentifier(v)))) + } + 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(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(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._ + + + def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = { + implicit lazy val vc = new VarContext(p.as.toSet, p.xs.toSet, hctx) + p.phi match { + case TopLevelAnds(conjuncts) => + val candidates: List[Equals] = conjuncts.toList collect { case e: Equals => e } filter { e => isLinEqInOutputVariables(e) } + if(candidates.isEmpty) { + 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), p.xs.toList.map(vc.getOutputVar)) + List(RuleInstantiation("Solve integer equalities") { + val (cond, prog) = problem.solve() + val solution = convertToSolution(cond, prog) + RuleClosed(solution) + }) + } + case _ => 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) From 0f40a5ec477d8b79bef1e7d222d5f0a53a036b30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Wed, 20 Jul 2016 21:35:04 +0200 Subject: [PATCH 3/8] Fixed missing variable bug. APA synthesis works for equalities. --- src/main/scala/leon/synthesis/rules/IntegerEquality.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala index 8752be48e..ca1a1ddec 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala @@ -190,7 +190,7 @@ object ComfusyConverters { CaseClass(CaseClassType(LeonCons.get, Seq(IntegerType)), Seq(v, l)) } val initial_fun = (x: Expr) => Let(b, functionInvocation(bezoutWithBase, Seq(InfiniteIntegerLiteral(BigInt(1)), tsConvertedToList)), x) - decomposed_recomposed compose initial_fun + initial_fun compose decomposed_recomposed } } From a8fb211f2f0d141f4b9298228d8dfea6fdd6dbab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 21 Jul 2016 13:24:25 +0200 Subject: [PATCH 4/8] Corrected isGCDable More let-tuple extraction in postcondition f.apply(a) is now written with .apply --- library/leon/math/package.scala | 6 +- .../scala/leon/purescala/Extractors.scala | 1 + .../scala/leon/purescala/PrettyPrinter.scala | 7 +- .../synthesis/rules/IntegerEquality.scala | 123 +++++++++++++++++- 4 files changed, 127 insertions(+), 10 deletions(-) diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala index e3a35a0da..e98201ceb 100644 --- a/library/leon/math/package.scala +++ b/library/leon/math/package.scala @@ -23,9 +23,9 @@ package object math { @library def isGCDable(l: List[BigInt]): Boolean = l match { - case Cons(x, b) if x == BigInt(0) => false - case Cons(a, b) => isGCDable(b) - case Nil() => true + case Cons(x, b) if x == BigInt(0) => isGCDable(b) + case Cons(x, b) => true + case Nil() => false } /** Computes the GCD between numbers */ 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/IntegerEquality.scala b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala index ca1a1ddec..fff0471c5 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala @@ -375,6 +375,16 @@ object ComfusyConverters { 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") @@ -383,6 +393,16 @@ object ComfusyConverters { 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") @@ -398,24 +418,117 @@ 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] = { - implicit lazy val vc = new VarContext(p.as.toSet, p.xs.toSet, hctx) p.phi match { - case TopLevelAnds(conjuncts) => - val candidates: List[Equals] = conjuncts.toList collect { case e: Equals => e } filter { e => isLinEqInOutputVariables(e) } + 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), p.xs.toList.map(vc.getOutputVar)) + 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) RuleClosed(solution) }) } - case _ => Nil + case _ => + //println("Not parsable as equation with conjuncts") + Nil } } } \ No newline at end of file From c02284d9a1fa5d758a1930e54eaa7850bb957323 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 21 Jul 2016 13:29:10 +0200 Subject: [PATCH 5/8] Adding isabelle noBody annotation --- library/leon/math/package.scala | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala index e98201ceb..75a2a2afe 100644 --- a/library/leon/math/package.scala +++ b/library/leon/math/package.scala @@ -22,6 +22,7 @@ package object math { def abs(i: BigInt) = if(i < BigInt(0)) -i else i @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 @@ -30,6 +31,7 @@ package object math { /** Computes the GCD between numbers */ @library + @annotation.isabelle.noBody() def gcdlist(l:List[BigInt]):BigInt = { require(l.length > 0 && isGCDable(l)) l match { @@ -40,6 +42,7 @@ package object math { /** Computes the LCM between numbers */ @library + @annotation.isabelle.noBody() def lcmlist(l:List[BigInt]):BigInt = { require(l.length > 0 && isGCDable(l)) l match { @@ -50,6 +53,7 @@ package object math { /** Computes the GCD between two numbers */ @library + @annotation.isabelle.noBody() def gcd(x:BigInt, y:BigInt): BigInt = { if (x==BigInt(0)) abs(y) else if (x<0) gcd(-x, y) @@ -59,6 +63,7 @@ package object math { /** Computes the LCM between two numbers */ @library + @annotation.isabelle.noBody() def lcm(x: BigInt, y: BigInt): BigInt = { x * y / gcd(x, y) } @@ -91,6 +96,7 @@ package object math { }*/ @library + @annotation.isabelle.noBody() def bezoutWithBase(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = { bezoutWithBaseMMFunc(e, a) } @@ -183,6 +189,7 @@ package object math { }*/ @library + @annotation.isabelle.noBody() def extendedEuclidFunc(a_in: BigInt, b_in: BigInt):(BigInt, BigInt, BigInt) = { val (x, lastx) = (BigInt(0), BigInt(1)) val (y, lasty) = (BigInt(1), BigInt(0)) @@ -203,6 +210,7 @@ package object math { } @library + @annotation.isabelle.noBody() def bezoutMMFunc(a_in: List[BigInt], k: BigInt):List[BigInt] = { val a = a_in val a_in_gcds = a_in.foldRight(List[BigInt]()){ (e: BigInt, v: List[BigInt]) => (e, v) match { @@ -234,6 +242,7 @@ package object math { } @library + @annotation.isabelle.noBody() def bezoutWithBaseMMFunc(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = { val coefs = a val coefs_gcd = coefs.foldRight(List[BigInt]()){ From 0016a389a78dfa59deccca05d16362f28d2c7cb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Thu, 21 Jul 2016 17:29:16 +0200 Subject: [PATCH 6/8] Updated corner cases and added some proofs. --- library/leon/math/package.scala | 55 +++++++++++++++++++++++++++------ 1 file changed, 45 insertions(+), 10 deletions(-) diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala index 75a2a2afe..0329a1cd6 100644 --- a/library/leon/math/package.scala +++ b/library/leon/math/package.scala @@ -36,6 +36,7 @@ package object math { 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) } } @@ -47,6 +48,7 @@ package object math { 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) } } @@ -55,17 +57,23 @@ package object math { @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 = { - x * y / gcd(x, y) + 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.*/ @@ -98,6 +106,7 @@ package object math { @library @annotation.isabelle.noBody() def bezoutWithBase(e: BigInt, a: List[BigInt]): (List[List[BigInt]]) = { + require(isNonZero(a) && a.nonEmpty) bezoutWithBaseMMFunc(e, a) } @@ -209,14 +218,40 @@ package object math { aux(a, b, x, y, lastx, lasty) } + @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 + @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)) val a = a_in - val a_in_gcds = a_in.foldRight(List[BigInt]()){ (e: BigInt, v: List[BigInt]) => (e, v) match { - case (i, Nil()) => List(i) - case (i, a::q) => gcd(a, i)::a::q - } } + + 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] = { @@ -244,16 +279,16 @@ package object math { @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 = coefs.foldRight(List[BigInt]()){ - case (i, Nil()) => List(abs(i)) - case (i, Cons(a, q)) => gcd(a, i)::a::q - } + 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]] = { + def aux(i: BigInt, result: List[List[BigInt]], coefs: List[BigInt], coefs_gcd: List[BigInt], zeros: List[BigInt]) + : List[List[BigInt]] = { + require(i <= n && isPositive(coefs_gcd) && isNonZero(coefs) && coefs_gcd.length >= 2 && coefs.length >= 1) if (i > n-BigInt(1)) { result.reverse } else { From 77b8c706d3b726d5d7563b53f38a6bad7a5a3cf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 22 Jul 2016 10:15:44 +0200 Subject: [PATCH 7/8] Added more proofs for comfusy's math. --- library/leon/math/package.scala | 33 +++++++++++++++++++++++++++------ 1 file changed, 27 insertions(+), 6 deletions(-) diff --git a/library/leon/math/package.scala b/library/leon/math/package.scala index 0329a1cd6..213dcd278 100644 --- a/library/leon/math/package.scala +++ b/library/leon/math/package.scala @@ -21,6 +21,17 @@ package object math { @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 { @@ -200,6 +211,7 @@ package object math { @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) @@ -216,7 +228,10 @@ package object math { } } 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() @@ -248,18 +263,19 @@ package object math { @library @annotation.isabelle.noBody() def bezoutMMFunc(a_in: List[BigInt], k: BigInt):List[BigInt] = { - require(isNonZero(a_in)) + 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(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) @@ -272,9 +288,14 @@ package object math { 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() @@ -288,7 +309,7 @@ package object math { 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 && isPositive(coefs_gcd) && isNonZero(coefs) && coefs_gcd.length >= 2 && coefs.length >= 1) + 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 { From f30debb8af2fe2abbf19f96a0deabf12db19c807 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 5 Aug 2016 15:49:57 +0200 Subject: [PATCH 8/8] Comfusy: Fixed output variable bug Fixed names. --- .../leon/synthesis/comfusy/APAProgram.scala | 2 +- .../synthesis/rules/IntegerEquality.scala | 30 ++++++++++++++++--- 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/src/main/scala/leon/synthesis/comfusy/APAProgram.scala b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala index 9b624b0da..05118df55 100644 --- a/src/main/scala/leon/synthesis/comfusy/APAProgram.scala +++ b/src/main/scala/leon/synthesis/comfusy/APAProgram.scala @@ -522,7 +522,7 @@ case class APAProgram(input_variables: List[InputVar], 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) + case (i, t) => indent + APAProgram.outputAssignmentToString(i, t) } match { case Nil => "" case l => l reduceLeft (APAAbstractProgram.combineSentences(_, _)) diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala index fff0471c5..7b2dbf7ac 100644 --- a/src/main/scala/leon/synthesis/rules/IntegerEquality.scala +++ b/src/main/scala/leon/synthesis/rules/IntegerEquality.scala @@ -56,6 +56,16 @@ class VarContext(val inputVariables: Set[Identifier], val outputVariables: Set[I 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) @@ -67,7 +77,8 @@ object ComfusyConverters { 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) + 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) @@ -102,6 +113,7 @@ object ComfusyConverters { 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 @@ -174,7 +186,7 @@ object ComfusyConverters { 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("b", listType.typed(Seq(listType.typed(Seq(IntegerType)))), false) + 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) => @@ -196,6 +208,8 @@ object ComfusyConverters { 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") @@ -266,7 +280,7 @@ object ComfusyConverters { 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 = prog.output_assignment.flatMap(_._2.output_variables) filterNot affectedOutputVariables + 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)))) @@ -354,7 +368,14 @@ object ComfusyConverters { case APAInputCombination(coef, input_linear) => ((InfiniteIntegerLiteral(BigInt(coef)): Expr) /: input_linear) { (c: Expr, iv) => val (i, v) = iv - Plus(c, Times(InfiniteIntegerLiteral(i), Variable(vc.getIdentifier(v)))) + 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))) @@ -523,6 +544,7 @@ case object IntegerEquality extends Rule("Solve integer equality"){ 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) }) }