This is an old revision of the document!
COMFUSY: COMplete FUnctional SYnthesis - Examples
ScaleWeights
import synthesis.Definitions._ object ScaleWeights { def main(args: Array[String]): Unit = { println("Give me a weight: ") val weight: Int = Console.readInt try { val (w1,w2,w3,w4) = choose((w1:Int,w2:Int,w3:Int,w4:Int) => ( w1 + 3 * w2 + 9 * w3 + 27 * w4 == weight && -1 <= w1 && w1 <= 1 && -1 <= w2 && w2 <= 1 && -1 <= w3 && w3 <= 1 && -1 <= w4 && w4 <= 1 )) println("Put what you think weights " + weight + " to the left, then") println("Put 1 : " + numToPlace(w1)) println("Put 3 : " + numToPlace(w2)) println("Put 9 : " + numToPlace(w3)) println("Put 27 : " + numToPlace(w4)) } catch { case UnsatisfiableConstraint() => println("Sorry, cannot measure " + weight + " with weights 1,3,9 and 27.") } } def numToPlace(i: Int): String = i match { case -1 => "to the left" case 0 => "nowhere" case 1 => "to the right" case _ => "??? " + i } }
SecondsToTime
import synthesis.Definitions._ object SecondsToTime { def main(args: Array[String]): Unit = { println("Please enter a number of seconds: ") val secnum: Int = Console.readInt val (hours, minutes, seconds) = choose((h: Int, m: Int, s: Int) => ( h * 3600 + m * 60 + s == secnum && 0 <= m && m < 60 && 0 <= s && s < 60 ) ) println(secnum + "s = " + hours + "h, " + minutes + "m and " + seconds + "s.") } }
SetConstraints
import synthesis.Definitions._ import scala.collection.immutable.Set object SetConstraints { def main(args : Array[String]) : Unit = { val bigSet = Set("AA", "BB", "CC", "DD", "EE") val setZ = Set.empty[String] val maxDiff = 1 val (setA, setB) = choose((A: Set[String], B: Set[String]) => ( A ++ B == bigSet && A ** B == Set.empty && A.size > 0 && B.size > 0 )) println("We can split:") println(bigSet) println("...into:") println(setA) println("...and:") println(setB) } }
SplitSetsInABalancedWay
import synthesis.Definitions._ import scala.collection.immutable.Set object SplitSetsInABalancedWay { def main(args : Array[String]) : Unit = { val bigSet = Set("Ladybugs", "must", "render", "you", "catatonic", ".") val maxDiff = 1 val (setA, setB) = choose((A: Set[String], B: Set[String]) => ( -maxDiff <= A.size - B.size && A.size - B.size <= maxDiff && A ++ B == bigSet && A ** B == Set.empty )) println("We can split:") println(bigSet) println("...into:") println(setA) println("...and:") println(setB) } }
FastExponentiation
import synthesis.Definitions._ object FastExponentiation { def pow(base: Int, p: Int) = { def fp(m : Int, b : Int, i : Int) : Int = i match { case 0 => m case 2 * j => fp(m, b*b, j) case 2 * j + 1 => fp(m*b, b*b, j) } fp(1, base, p) } def main(args : Array[String]) : Unit = { println("Base ?") val bse = Console.readInt println("Exponent ?") val exp = Console.readInt println(bse + "^" + exp + " = " + pow(bse,exp)) } }
PrimeHeuristic
import synthesis.Definitions._ object PrimeHeuristic { def maybePrime(n: Int): Boolean = n match { case 2 * k => false case 3 * k => false case 6 * k - 1 => true case 6 * k + 1 => true } def main(args : Array[String]) : Unit = { println("Number !") val x = Console.readInt println("Any chance that " + x + " is prime ? " + maybePrime(x)) } }
NewYearSong
(similar code with fewer variables was used to compute the distribution of names in this song)
import synthesis.Definitions._ object NewYearSong { def main(args : Array[String]) : Unit = { println("eLines (6) ?") val eLines: Int = Console.readInt println("iLines (2) ?") val iLines: Int = Console.readInt println("iSyls (5) ?") val iSyls: Int = Console.readInt println("nSyls (952) ?") val nSyls: Int = Console.readInt val (line7, line8, nsLines, nLines, tLines, _) = choose((line7: Int, line8: Int, nsLines: Int, nLines: Int, tLines: Int, tLinesFact: Int) => ( tLines == eLines + nLines && nLines == iLines + nsLines && nLines == line7 + line8 && nSyls + iSyls == 7 * line7 + 8 * line8 && tLines == 4 * tLinesFact // expresses (4 | tLines) && line8 >= 0 && line7 >= 0 && tLines >= 0 )) println("line7 : " + line7) println("line8 : " + line8) println("nsLines : " + nsLines) println("nLines : " + nLines) println("tLines : " + tLines) } }