From 4c297b5701075ea6854e1398d3f5d7974d36327a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Tue, 13 Sep 2011 18:23:17 +0000
Subject: [PATCH] Our CEGIS loop used for the alternative way of integer
 squaring

---
 cp-demo/CEGISsqr.scala | 48 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 cp-demo/CEGISsqr.scala

diff --git a/cp-demo/CEGISsqr.scala b/cp-demo/CEGISsqr.scala
new file mode 100644
index 000000000..766c2aad8
--- /dev/null
+++ b/cp-demo/CEGISsqr.scala
@@ -0,0 +1,48 @@
+import cp.Definitions._
+import cp.Terms._
+
+object CEGISsqr {
+  @spec def sqr(x: Int, y: Int): Boolean = {
+    x*x <= y && (x+1)*(x+1) > y
+  }
+
+  @spec def sqr_sk(x: Int, q1: Int, q2: Int, q3: Int): Int = {
+    if (x <= 1) x + q1
+    else q2*x + sqr_sk(x - 2, q1, q2, q3) + q3
+  }
+
+  def main(args: Array[String]): Unit = {
+    var continue = true
+
+    val initialX = ((x: Int) => x >= 0).solve
+    println("Initial x: " + initialX)
+
+    // constraint is sqr(x, sqr_sk(x, q1, q2, q3))
+    def cnstrGivenX(x0: Int): Constraint3[Int,Int,Int] = 
+      ((q1: Int, q2: Int, q3: Int) => sqr(x0, sqr_sk(x0, q1, q2, q3)))
+
+    def cnstrGivenParams(q1: Int, q2: Int, q3: Int): Constraint1[Int] =
+      ((x: Int) => sqr(x, sqr_sk(x, q1, q2, q3)))
+
+    var currentCnstr = cnstrGivenX(initialX)
+
+    while (continue) {
+      currentCnstr.find match {
+        case Some((q1, q2, q3)) => {
+          println("found candidate parameters q1 = " + q1 + ", q2 = " + q2 + ", q3 = " + q3)
+          (((x: Int) => x >= 0) && (! cnstrGivenParams(q1, q2, q3))).find match {
+            case None =>
+              println("proved!")
+              continue = false
+            case Some(counterex) =>
+              println("found a counterexample for x: " + counterex)
+              currentCnstr = currentCnstr && cnstrGivenX(counterex)
+          }
+        }
+        case None =>
+          println("cannot prove property!")
+          continue = false
+      }
+    }
+  }
+}
-- 
GitLab