migrate from internal

.gitignore

@@ -2,3 +2,4 @@
 *.vo
 #*#
 *.glob
+*.DS_Store

rosette/cosette.rkt

@@ -0,0 +1,30 @@
+; The rosette interface for cosette
+
+#lang rosette
+
+(require "util.rkt" "table.rkt" "equal.rkt" "sql.rkt")
+(require racket/pretty)
+(require json)
+
+(provide cosette-sol->json 
+         cosette-solve)
+
+(define (cosette-sol->json solution)
+  (let ([status (car solution)]
+        [tables (cdr solution)])
+    (jsexpr->string 
+      (hasheq 'status status
+              'counter-example (map (lambda (t) (table->jsexpr t)) tables)))))
+
+(define (cosette-solve q1 q2 input-tables)
+  (let ([solution (verify (same q1 q2))])
+    (cond 
+      [(sat? solution) (cons "neq" (evaluate input-tables solution))]
+      [else (cons "eq"  (list))]))) 
+
+(define (table->jsexpr t) 
+  (hasheq 'table-name (get-table-name t) 
+          'table-content (list (get-schema t) 
+                         (map (lambda (r) (list (car r) (cdr r))) 
+                              (get-content t)))))
+

rosette/playground/eg-1.rkt

@@ -0,0 +1,22 @@
+#lang rosette
+
+(require "../cosette.rkt" "../util.rkt" "../table.rkt" "../sql.rkt" "../evaluator.rkt" "../equal.rkt")
+
+(define t1 (Table "t1" (list "id") (gen-sym-schema 1 3)))
+(define t2 (Table "t2" (list "id") (list)))
+
+;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0))))
+
+; SELECT * AS u FROM users WHERE id = 1
+
+(define q1
+  (SELECT (VALS "t1.id")
+   FROM   (NAMED t1)
+   WHERE  (BINOP "t1.id" = 1)))
+
+(define q2 (NAMED t2))
+
+(cosette-sol->json (cosette-solve q1 q2 (list t1 t2)))
+;(map (lambda (t) (table-to-json-obj t)) (cosette-verify q1 q2 (list t1 t2)))
+;(time (verify (same q1 q2)))
+;(time (verify (neq q1 q2)))

rosette/playground/eg-2.rkt

@@ -0,0 +1,57 @@
+#lang rosette
+
+(require "../test-util.rkt" "../../table.rkt" "../../sql.rkt" "../../evaluator.rkt" "../../equal.rkt")
+
+(define (aggr-sum l)
+  (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x)))
+       (get-content l))))
+
+(define t1 (Table "votes" (list "vote" "story_id") (gen-sym-schema 2 3)))
+(define t2 (Table "stories" (list "id") (gen-sym-schema 1 2)))
+
+(define ct1 
+	(Table "votes" (list "vote" "story_id") 
+		(list (cons (list 2 3) 2)
+				  (cons (list 1 3) 1)
+				  (cons (list 2 1) 3))))
+
+(define ct2 
+	(Table "stories" (list "id") 
+		(list (cons (list 2) 1)
+		      (cons (list 3) 1))))
+
+
+(define t3 (Table "t" (list "sum") (list (cons (list -1) 1))))
+(define t4 (Table "t" (list "sum") (list)))
+
+
+;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0))))
+
+; SELECT SUM(vote) AS sumv FROM votes AS v INNER JOIN stories AS s ON v.story_id = s.id;
+
+(define q1
+	(SELECT (VALS (AGGR aggr-sum (SELECT (VALS "v.vote")
+																FROM   (JOIN (AS (NAMED t1) ["v" (list "vote" "story_id")]) 
+							   											       (AS (NAMED t2) ["s" (list "id")]))
+																WHERE (BINOP "v.story_id" = "s.id"))))
+	 FROM (NAMED t3)
+	 WHERE (filter-empty)))
+
+(define q2 (NAMED t3))
+
+(define q3 
+	(SELECT (VALS "j.s1")
+     FROM (AS (JOIN q1 q2)
+   				 ["j" (list "s1" "s2")])
+    WHERE (BINOP "j.s1" > "j.s2")))
+
+(define q4 (NAMED t4))
+
+;(run q1)
+;(get-content (run q2))
+;(get-content (run q3))
+;(get-content (run q4))
+
+(time (verify (same q3 q4)))
+(time (verify (neq q3 q4)))
+

rosette/playground/eg-3.rkt

@@ -0,0 +1,54 @@
+#lang rosette
+
+(require "../test-util.rkt" "../../table.rkt" "../../sql.rkt" "../../evaluator.rkt" "../../equal.rkt")
+
+;(current-bitwidth 32)
+
+(define (aggr-count l)
+  (foldl + 0 (map cdr (get-content l))))
+
+(define t (Table "t" (list "v") (gen-sym-schema 1 8)))
+(define ct (Table "t" (list "v") (list (cons (list 1) 10) (cons (list 2) 12))))
+(define t3 (Table "t" (list "v") (list (cons (list 50) 1))))
+(define t4 (Table "t" (list "v") (list)))
+
+;(define t2 (Table "t1" (list "id") (list (cons (list 0) 0))))
+
+; SELECT SUM(vote) AS sumv FROM votes AS v INNER JOIN stories AS s ON v.story_id = s.id;
+
+(define q1
+	(SELECT-DISTINCT 
+      (VALS (AGGR aggr-count (SELECT-DISTINCT (VALS "t.v") FROM (NAMED t) WHERE (filter-empty))))
+	 FROM  (NAMED t3)
+	 WHERE (filter-empty)))
+
+(define cq1
+	(SELECT-DISTINCT (VALS (AGGR aggr-count (SELECT-DISTINCT (VALS "t.v") FROM (NAMED ct) WHERE (filter-empty))))
+	 FROM  (NAMED t3)
+	 WHERE (filter-empty)))
+
+(define q2
+	(SELECT (VALS "j.s1")
+     FROM (AS q1 ["j" (list "s1")])
+    WHERE (BINOP "j.s1" < 8)))
+
+(define cq2
+	(SELECT (VALS "j.s1")
+     FROM (AS cq1 ["j" (list "s1")])
+    WHERE (BINOP "j.s1" < 50)))
+
+(define q4 (NAMED t4))
+
+;(run cq1)
+;(run cq2)
+;(run q4)
+
+;(time (verify (same cq2 q4)))
+;(time (verify (neq q2 q4)))
+;(get-content (run q2))
+;(get-content (run q3))
+;(get-content (run q4))
+
+(time (verify (same q2 q4)))
+(time (verify (neq q2 q4)))
+

rosette/tests/aggr-join.rkt

@@ -9,8 +9,8 @@
 ; (define ta (Table "R" (list "A" "B") concrete-table-2-col))
 ; (define tb (Table "S" (list "C" "D") concrete-table-2-col))
 
-(define ta (Table "R" (list "A" "B") (gen-sym-schema 2 num-rows-in-sym-table)))
-(define tb (Table "S" (list "C" "D") (gen-sym-schema 2 num-rows-in-sym-table)))
+(define ta (Table "R" (list "A" "B") (gen-sym-schema 2 2)))
+(define tb (Table "S" (list "C" "D") (gen-sym-schema 2 2)))
 
 (define (aggr-sum l)
   (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x)))

rosette/tests/aggr-pull-up.rkt

@@ -5,9 +5,7 @@
 (define (same q1 q2)
     (assert (bag-equal (get-content (run q1)) (get-content (run q2)))))
 
-
-
-(define t1 (Table "t1" (list "c1" "c2" "c3") (gen-sym-schema 3 num-rows-in-sym-table)))
+(define t1 (Table "t1" (list "c1" "c2" "c3") (gen-sym-schema 3 3)))
 ; (define t1 (Table "t1" (list "c1" "c2" "c3") concrete-table-3-col))
 
 (define (aggr-sum l)
@@ -71,16 +69,15 @@
 (define model (time (verify (same subq-aggr-1 subq-aggr-2))))
 (define model2 (verify (same subq-aggr-1 subq-aggr-wrong-2)))
 
-model
-
+;model
 model2
 
-(evaluate t1 model2)
-(evaluate (run subq-aggr-1) model2)
+;(evaluate t1 model2)
+;(evaluate (run subq-aggr-1) model2)
 ;(evaluate (run subq-aggr-wrong-2) model2)
-(println "========")
-(println "========")
-(denote-sql subq-aggr-1 (make-hash))
+;(println "========")
+;(println "========")
+;(denote-sql subq-aggr-1 (make-hash))
 
 ;(evaluate (Table-content t1) model)
 ;(evaluate (run subq-aggr-1) model)

rosette/run-tests.sh → rosette/tests/run-tests.sh

@@ -7,9 +7,9 @@ if [[ "$UNAME" == "Darwin" ]]; then
 fi
 
 function run_test {
-    for i in `seq 1 $3`;
+    for i in `seq 1 $2`;
     do
-        $SED "s/[0-9]/$i/" $2;
+        $SED "s/[0-9]/$i/";
         for j in `seq 0 2`;
         do
             racket $1 | grep "cpu time" &
@@ -19,22 +19,21 @@ function run_test {
     done;
 }
 
-TEST_DIR=tests
-ARGS_FILE=args.rkt
+TEST_DIR=.
 
 EASY_TESTS="simpleRA.rkt push-projection.rkt subquery-exists.rkt magic-set.rkt"
 HARD_TESTS="aggr-pull-up.rkt subquery-test.rkt aggr-join.rkt"
 
 for test in $EASY_TESTS;
 do
     echo "============== $test ==============";
-    run_test $TEST_DIR/$test $TEST_DIR/$ARGS_FILE 4;
+    run_test $TEST_DIR/$test 4;
 done;
 wait
 
 for test in $HARD_TESTS;
 do
     echo "============== $test ==============";
-    run_test $TEST_DIR/$test $TEST_DIR/$ARGS_FILE 2;
+    run_test $TEST_DIR/$test 2;
 done;
 wait

rosette/util.rkt

@@ -0,0 +1,23 @@
+#lang rosette
+
+(require "table.rkt" "equal.rkt" "sql.rkt")
+(require json)
+
+(provide (all-defined-out))  
+
+;; assertions
+
+(define (same q1 q2)
+    (assert (bag-equal (get-content (run q1)) (get-content (run q2)))))
+
+(define (neq q1 q2)
+  (assert (not (bag-equal (get-content (run q1)) (get-content (run q2))))))
+
+;; aggregation functions
+
+(define (aggr-count l)
+  (foldl + 0 (map cdr (get-content l))))
+
+(define (aggr-sum l)
+  (foldl + 0 (map (lambda (x) (* (car (car x)) (cdr x)))
+       (get-content l))))