From a748f4ec7c67e38cefeef8b6fc95f43d7c9afdb8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 23 Jul 2015 17:33:56 +0200
Subject: [PATCH] Added more comments for some synthesis functions.
---
src/main/scala/leon/purescala/Common.scala | 8 ++++++++
src/main/scala/leon/synthesis/Algebra.scala | 18 ++++++++++++++++--
.../scala/leon/synthesis/ExampleBank.scala | 2 +-
src/main/scala/leon/synthesis/Problem.scala | 11 +++++++++--
src/main/scala/leon/synthesis/Rules.scala | 7 ++++++-
.../leon/synthesis/rules/DetupleInput.scala | 11 +++++++++++
6 files changed, 51 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 2d592e006..27818fd39 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -76,9 +76,17 @@ object Common {
}
object FreshIdentifier {
+ /** Builds a fresh identifier
+ * @param name The name of the identifier
+ * @param tpe The type of the identifier
+ * @param alwaysShowUniqueID If the unique ID should always be shown */
def apply(name: String, tpe: TypeTree = Untyped, alwaysShowUniqueID: Boolean = false) : Identifier =
new Identifier(name, UniqueCounter.nextGlobal, UniqueCounter.next(name), tpe: TypeTree, alwaysShowUniqueID)
+ /** Builds a fresh identifier, whose ID is always shown
+ * @param name The name of the identifier
+ * @param forceId The forced ID of the identifier
+ * @param tpe The type of the identifier */
def apply(name: String, forceId: Int, tpe: TypeTree): Identifier =
new Identifier(name, UniqueCounter.nextGlobal, forceId, tpe, true)
diff --git a/src/main/scala/leon/synthesis/Algebra.scala b/src/main/scala/leon/synthesis/Algebra.scala
index 6730cabb2..92ee346e0 100644
--- a/src/main/scala/leon/synthesis/Algebra.scala
+++ b/src/main/scala/leon/synthesis/Algebra.scala
@@ -11,20 +11,23 @@ package leon.synthesis
*/
object Algebra {
-
+ /** Returns the remainder of the euclidian division between x an y (always positive) */
def remainder(x: Int, y: Int) = ((x % y) + y.abs) % y.abs
+ /** Returns the quotient of the euclidian division between a and b.*/
def divide(a: Int, b: Int): (Int, Int) = {
val r = remainder(a, b)
((a - r)/b, r)
}
+ /** Returns the remainder of the euclidian division between the big integers x an y (always positive) */
def remainder(x: BigInt, y: BigInt) = ((x % y) + y.abs) % y.abs
+ /** Returns the quotient of the euclidian division between the big integers x an y */
def divide(a: BigInt, b: BigInt): (BigInt, BigInt) = {
val r = remainder(a, b)
((a - r)/b, r)
}
-
+ /** Returns the gcd of two integers */
def gcd(a: Int, b: Int): Int = {
val (na, nb) = (a.abs, b.abs)
def gcd0(a: Int, b: Int): Int = {
@@ -34,6 +37,7 @@ object Algebra {
if(na > nb) gcd0(na, nb) else gcd0(nb, na)
}
+ /** Returns the gcd of three or more integers */
def gcd(a1: Int, a2: Int, a3: Int, as: Int*): Int = {
var tmp = gcd(a1, a2)
tmp = gcd(tmp, a3)
@@ -45,6 +49,7 @@ object Algebra {
tmp
}
+ /** Returns the gcd of a non-empty sequence of integers */
def gcd(as: Seq[Int]): Int = {
require(as.length >= 1)
if(as.length == 1)
@@ -60,6 +65,7 @@ object Algebra {
}
}
+ /** Returns the gcd of two big integers */
def gcd(a: BigInt, b: BigInt): BigInt = {
val (na, nb) = (a.abs, b.abs)
def gcd0(a: BigInt, b: BigInt): BigInt = {
@@ -69,6 +75,7 @@ object Algebra {
if(na > nb) gcd0(na, nb) else gcd0(nb, na)
}
+ /** Returns the gcd of three or more big integers */
def gcd(a1: BigInt, a2: BigInt, a3: BigInt, as: BigInt*): BigInt = {
var tmp = gcd(a1, a2)
tmp = gcd(tmp, a3)
@@ -80,6 +87,7 @@ object Algebra {
tmp
}
+ /** Returns the gcd of a non-empty sequence of big integers */
def gcd(as: Seq[BigInt]): BigInt = {
require(as.length >= 1)
if(as.length == 1)
@@ -95,11 +103,13 @@ object Algebra {
}
}
+ /** Returns the lcm of two integers */
def lcm(a: Int, b: Int): Int = {
val (na, nb) = (a.abs, b.abs)
na*nb/gcd(a, b)
}
+ /** Returns the lcm of three or more integers */
def lcm(a1: Int, a2: Int, a3: Int, as: Int*): Int = {
var tmp = lcm(a1, a2)
tmp = lcm(tmp, a3)
@@ -111,6 +121,7 @@ object Algebra {
tmp
}
+ /** Returns the lcm of a sequence of integers */
def lcm(as: Seq[Int]): Int = {
require(as.length >= 1)
if(as.length == 1)
@@ -126,11 +137,13 @@ object Algebra {
}
}
+ /** Returns the lcm of two big integers */
def lcm(a: BigInt, b: BigInt): BigInt = {
val (na, nb) = (a.abs, b.abs)
na*nb/gcd(a, b)
}
+ /** Returns the lcm of three or more big integers */
def lcm(a1: BigInt, a2: BigInt, a3: BigInt, as: BigInt*): BigInt = {
var tmp = lcm(a1, a2)
tmp = lcm(tmp, a3)
@@ -142,6 +155,7 @@ object Algebra {
tmp
}
+ /** Returns the lcm of a sequence of big integers */
def lcm(as: Seq[BigInt]): BigInt = {
require(as.length >= 1)
if(as.length == 1)
diff --git a/src/main/scala/leon/synthesis/ExampleBank.scala b/src/main/scala/leon/synthesis/ExampleBank.scala
index 29c82015b..23fa9039e 100644
--- a/src/main/scala/leon/synthesis/ExampleBank.scala
+++ b/src/main/scala/leon/synthesis/ExampleBank.scala
@@ -9,7 +9,7 @@ import purescala.Common._
import repair._
import leon.utils.ASCIIHelpers._
-
+/** Sets of valid and invalid examples */
case class ExampleBank(valids: Seq[Example], invalids: Seq[Example]) {
def examples = valids ++ invalids
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 99b1d699d..4ae607f81 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -11,8 +11,15 @@ import leon.purescala.Constructors._
import leon.purescala.Extractors._
import Witnesses._
-// Defines a synthesis triple of the form:
-// ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
+/** Defines a synthesis triple of the form:
+ * ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
+ *
+ * @param as The list of input identifiers so far
+ * @param ws The axioms and other already proven theorems
+ * @param pc The path condition so far
+ * @param phi The formula on `as` and `xs` to satisfy
+ * @param xs The list of output identifiers for which we want to compute a function
+ */
case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExampleBank = ExampleBank.empty) {
def inType = tupleTypeWrap(as.map(_.getType))
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 2195cb126..908b753d9 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -10,6 +10,7 @@ import purescala.ExprOps._
import purescala.Constructors.and
import rules._
+/** A Rule can be applied on a synthesis problem */
abstract class Rule(val name: String) extends RuleDSL {
def instantiateOn(implicit hctx: SearchContext, problem: Problem): Traversable[RuleInstantiation]
@@ -30,7 +31,9 @@ abstract class PreprocessingRule(name: String) extends Rule(name) {
override val priority = RulePriorityPreprocessing
}
+/** Contains the list of all available rules for synthesis */
object Rules {
+ /** Returns the list of all available rules for synthesis */
def all = List[Rule](
Unification.DecompTrivialClash,
Unification.OccursCheck, // probably useless
@@ -142,12 +145,14 @@ case object RulePriorityDefault extends RulePriority(20)
*/
trait RuleDSL {
this: Rule =>
-
+ /** Replaces all first elements of `what` by their second element in the expression `ìn`*/
def subst(what: (Identifier, Expr), in: Expr): Expr = replaceFromIDs(Map(what), in)
+ /** Replaces all keys of `what` by their key in the expression `ìn`*/
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replaceFromIDs(what, in)
val forward: List[Solution] => Option[Solution] = { ss => ss.headOption }
+ /** Returns a function that transforms the precondition and term of the first Solution of a list using `f`. */
def forwardMap(f : Expr => Expr) : List[Solution] => Option[Solution] = {
_.headOption map { s =>
Solution(f(s.pre), s.defs, f(s.term), s.isTrusted)
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index ed25fc4b3..bb0f1b4ba 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -10,15 +10,26 @@ import purescala.Types._
import purescala.ExprOps._
import purescala.Constructors._
+/** Rule for detupling input variables, to be able to use their sub-expressions. For example, the input variable:
+ * {{{d: Cons(head: Int, tail: List)}}}
+ * will create the following input variables
+ * {{{head42: Int, tail57: List}}}
+ * Recomposition is available.
+ */
case object DetupleInput extends NormalizingRule("Detuple In") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
+ /** Returns true if this identifier is a tuple or a case class */
def isDecomposable(id: Identifier) = id.getType match {
case CaseClassType(t, _) if !t.isAbstract => true
case TupleType(ts) => true
case _ => false
}
+ /* Decomposes a decomposable input identifier (eg of type Tuple or case class)
+ * into a list of fresh typed identifiers, the tuple of these new identifiers,
+ * and the mapping of those identifiers to their respective expressions.
+ */
def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr]) = id.getType match {
case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
--
GitLab