[WIP] experimental branch on synthesize preconditions

examples/conditional/join-elim-fk.cos

@@ -0,0 +1,16 @@
+schema s1(id:int, n:int);
+schema s2(id:int, t1_id:int, n:int);
+
+table t1(s1);
+table t2(s2);
+
+query q1 
+`select y.id as t2id, y.n as t2n
+ from t1 x, t2 y
+ where x.id = y.t1_id`;
+
+query q2 
+`select y.id as t2id
+ from t2 y`;
+
+ verify q1 q2;

rosette/evaluator.rkt

@@ -114,6 +114,7 @@
                   (dedup (filter (lambda (x)(not (equal? (car ele) (car x))))
                                  (cdr table))))]))]))
 
+; normalized table, merge the mutiplicity of the same tuples
 (define (dedup-accum table)
   (cond 
     [(equal? '() table) '()]
@@ -242,5 +243,6 @@
     [(eq? l '()) #t]
     [else (&& (distinct-to-all-list (car l) (cdr l)) (list-distinct? (cdr l)))]))
 
+;; here, we treat two empty list 'distinct' 
 (define (distinct-to-all-list x l)
   (foldl && #t (map (lambda (y) (not (eq? x y))) l)))

rosette/syn-preconditions/join-elim-fk.rkt

@@ -0,0 +1,70 @@
+#lang rosette 
+
+(require "../cosette.rkt" "../util.rkt" "../table.rkt" 
+         "../sql.rkt" "../evaluator.rkt" "../equal.rkt") 
+
+
+(current-bitwidth #f)
+
+(define t2-info (table-info "t2" (list "id" "t1_id" "n")))
+
+(define t1-info (table-info "t1" (list "id" "n")))
+
+(define t1 (Table "t1" (list "id" "n") (gen-sym-schema 2 2)))
+
+(define t2 (Table "t2" (list "id" "t1_id" "n") (gen-sym-schema 3 2)))
+
+(define q1 
+  (SELECT (VALS "y.id" "y.n") 
+  FROM (JOIN (NAMED (RENAME t1 "x")) (NAMED (RENAME t2 "y"))) 
+  WHERE (BINOP "x.id" = "y.t1_id")))
+
+(define q2 
+  (SELECT (VALS "y.id" "y.n") 
+  FROM (NAMED (RENAME t2 "y")) 
+  WHERE (F-EMPTY)))
+
+;(assert (foreign-key-constraint? t1 t2 (list 0) (list 1)))
+;(assert (table-cols-distinct? t2 (list 2)))
+
+(define (gen-t1-pk col)
+  (assert (table-cols-distinct? t1 (list col))))
+
+(define (gen-t2-pk col)
+  (assert (table-cols-distinct? t2 (list col))))
+
+(define (gen-fk col1 col2)
+  (assert (foreign-key-constraint? t1 t2 (list col1) (list col2))))
+
+(define t1pk 0)
+(define t2pk 0)
+(define t1-fk-pk 0)
+(define t2-fk 0)
+
+(define (stop-condition i j k n)
+  (let ([sol
+         (begin
+           (gen-t1-pk i)
+           (gen-t2-pk j)
+           (gen-fk k n)
+           (verify (same q1 q2)))])
+    (cond
+      [(sat? sol) #f]
+      [else (begin (println "find")
+                   (println (list i j k n))
+                   (set! t1pk i)
+                   (set! t2pk j)
+                   (set! t1-fk-pk k)
+                   (set! t2-fk n)
+                   #t)])))
+; do the search here
+(time
+(for* ([i (in-range 3)]
+       [j (in-range 2)]
+       [k (in-range 3)]
+       [n (in-range 2)])
+       #:break (stop-condition i j k n)
+       (clear-asserts!)
+       (println (list i j k n))
+ ))
+;(verify (same q1 q2))

rosette/syn-preconditions/missing-pred.rkt

@@ -0,0 +1,64 @@
+#lang rosette 
+
+(require "../cosette.rkt" "../util.rkt" "../table.rkt" 
+         "../sql.rkt" "../evaluator.rkt" "../equal.rkt")
+
+(current-bitwidth #f)
+
+(define r-info (table-info "r" (list "a" "b" "c")))
+
+(define r (Table "r" (list "a" "b" "c") (gen-sym-schema 3 2)))
+
+(define q1 
+  (SELECT (VALS "x.b") 
+  FROM (NAMED (RENAME r "x")) 
+  WHERE (BINOP "x.a" = 5)))
+
+(define q2 
+  (SELECT (VALS "x.b") 
+  FROM (NAMED (RENAME r "x")) 
+  WHERE (BINOP "x.a" < 10)))
+
+(struct table-col (x)
+  #:transparent
+  #:guard (lambda (x type-name)
+            (cond
+              [(integer? x) x]
+              [else (error "col must be an integer")])))
+
+(define (eval-pred-on-table? table lo op ro)
+  (let ([content (filter-zero (Table-content table))]
+        [eval-o (lambda (row o)
+                  (cond
+                    [(table-col? o) (list-ref (car row) (table-col-x o))]
+                    [(integer? o) o]
+                    [else (error "o can only be a table-col or integer")]))])
+    (foldl && #t (map (lambda (x) (op (eval-o x lo) (eval-o x ro))) content)))) 
+
+(define literals (list 1 5 10))
+
+(define operators (list = >))
+
+(define cols (list (table-col 0) (table-col 1) (table-col 2)))
+
+(define (stop-condition i j k lits ops cols)
+  (let ([sol
+         (begin
+           (assert (eval-pred-on-table? r (list-ref lits i) (list-ref ops j) (list-ref cols k)))
+           (verify (same q1 q2)))])
+    (cond
+      [(sat? sol) #f]
+      [else (begin (println "find")
+                   (println (list (list-ref lits i) (list-ref ops j) (list-ref cols k)))
+                   #t)])))
+
+
+; do the search here
+(time
+(for* ([i (in-range (length literals))]
+       [j (in-range (length operators))]
+       [k (in-range (length cols))])
+       #:break (stop-condition i j k literals operators cols)
+       (clear-asserts!)
+       (println (list i j k))
+ ))

rosette/syn-preconditions/synthesize-key.rkt

@@ -0,0 +1,110 @@
+#lang rosette 
+
+(require "../cosette.rkt" "../util.rkt" "../table.rkt" 
+         "../sql.rkt" "../evaluator.rkt" "../equal.rkt") 
+
+(current-bitwidth #f)
+
+(define dept-info (table-info "dept" (list "dept" "loc" "mgr")))
+
+(define emp-info (table-info "emp" (list "name" "dept" "emp")))
+
+(define s-dept (Table "dept" (list "dept" "loc" "mgr") (gen-sym-schema 3 2)))
+
+(define s-emp (Table "emp" (list "name" "dept" "emp") (gen-sym-schema 3 2)))
+
+(define c-dept (Table "dept" (list "dept" "loc" "mgr")
+                      (list (cons (list 0 3 0) 1)
+                            (cons (list 0 3 0) 1))))
+
+(define c-emp (Table "emp" (list "name" "dept" "emp")
+                     (list (cons (list 42 0 0) 1)
+                           (cons (list 43 1 0) 1))))
+
+(define emp s-emp)
+
+(define dept s-dept)
+
+(define q1 
+  (SELECT (VALS "x.name") 
+  FROM (NAMED (RENAME emp "x")) 
+  WHERE (EXISTS (AS (SELECT (VALS "y.dept" "y.loc" "y.mgr") 
+                            FROM (NAMED (RENAME dept "y")) 
+                            WHERE (AND (AND (BINOP "y.loc" = 3)
+                                            (BINOP "x.emp" = "y.mgr"))
+                                       (BINOP "x.dept" = "y.dept"))) ["anyname" (list "dept" "loc" "mgr")]))))
+
+(define q2 
+  (SELECT (VALS "x.name") 
+  FROM (JOIN (NAMED (RENAME emp "x")) (NAMED (RENAME dept "y"))) 
+  WHERE (AND (AND (BINOP "x.dept" = "y.dept") (BINOP "y.loc" = 3)) (BINOP "x.emp" = "y.mgr"))))
+
+; when 
+;(assert-table-col-distinct emp (list 2))
+;(assert-table-col-distinct dept (list 0))
+
+(define-symbolic* e1 e2 e3 integer?)
+
+(define-symbolic* d1 d2 d3 integer?)
+
+;(require rosette/lib/angelic)
+;(define ec (choose* (list) (list e1) (list e1 e2) (list e1 e2 e3)))
+;(define dc (choose* (list) (list d1) (list d1 d2) (list d1 d2 d3)))
+
+(define ec (list e1 e2 e3))
+(define dc (list d1 d2 d3))
+
+;(assert-table-cols-distinct emp ec)
+;(assert-table-cols-distinct dept dc)
+
+;(optimize #:minimize (list (+ (length ec) (length dc)))
+;          #:guarantee (assert (forall (list s-emp s-dept) (same q1 q2))))
+(define (init-key-size table-num)
+  (make-list table-num 0))
+
+(define (inc-key-size key-size)
+  (match key-size
+         [(list x) (list (+ x 1))]
+         [(cons x l)
+          (cond [(< x (car l)) (append (list (+ x 1)) l)]
+                [else (append (list x) (inc-key-size l))])]))
+
+;(optimize #:minimize (list (+ (length ec) (length dc)))
+;          #:guarantee (assert (forall (list s-emp s-dept) (same q1 q2))))
+
+#; (synthesize #:forall (list s-emp s-dept)
+            #:guarantee (assert (same q1 q2)))
+
+;incremental search with increasing key size, once found, return the result
+(define (search-key-constraints input-tables keys key-size)
+  ; assertion of key-sizes
+  (for ([i (in-range (length input-tables))])
+          (assert-table-cols-distinct
+           (list-ref input-tables i)
+           (take (list-ref keys i) (list-ref key-size i))))
+     (assert (and (>= e1 0) (< e1 3)))
+     (assert (and (>= e2 0) (< e2 3)))
+     (assert (and (>= e3 0) (< e3 3)))
+     (assert (and (>= d1 0) (< d1 3)))
+     (assert (and (>= d2 0) (< d2 3)))
+     (assert (and (>= d3 0) (< d3 3)))
+     (define sol (synthesize #:forall input-tables
+                             #:guarantee (assert (same q1 q2))))
+     (cond [(sat? sol) (list sol key-size)]
+           [(eq? (car key-size) (length input-tables)) '('UNSAT)]
+           [else (begin
+                   (clear-asserts!)
+                   (search-key-constraints input-tables keys (inc-key-size key-size)))]))
+
+(define input-tables (list s-emp s-dept))
+
+(define keys (list ec dc))
+
+(define sol (search-key-constraints input-tables (list ec dc) (list 0 0)))
+
+(time (search-key-constraints input-tables (list ec dc) (list 0 0)))
+
+(if (sat? (car sol)) 
+    (for/list ([i (in-range (length keys))])
+      (take (evaluate (list-ref keys i) (car sol)) (list-ref (cadr sol) i)))
+    "UNSAT")

rosette/tests/util-test.rkt

@@ -19,7 +19,7 @@
 (time (verify
         #:assume (begin
                    (assert-table-ordered st)
-                   (assert-table-col-distinct st 1))
+                   (assert-table-cols-distinct st 1))
         #:guarantee (same (test-q st) (test-q2 st))))
 
 
@@ -37,7 +37,7 @@
 (time (verify
         #:assume (begin
                    (assert-table-ordered st)
-                   (assert-table-col-distinct st 1))
+                   (assert-table-col-distinct st (list 1)))
         #:guarantee (same (test-2-q st) (test-2-q2 st))))
 
 ;(let* ([ct (evaluate st cex)]

rosette/util.rkt

@@ -7,7 +7,11 @@
          gen-pos-sym-schema ;; generate table that contains only positive symbolic values
          assert-table-non-empty ;; assert that a table is not empty
          assert-table-ordered ;; assert that the table is ordered
-         assert-table-col-distinct ;; assert that all values in a column is distinct from each other
+         assert-table-cols-distinct ;; assert that all values in a list of columns is distinct from each other
+         table-cols-distinct? ;; check the projection of certern cols of a table is distinct or not
+         list-subset? ;; check whether the set of elements of a list is a subset of the set of elements of another list
+         foreign-key-constraint? ;; check whether two tables and specified cols conform pk-fk constraint
+         filter-zero
          same ;; assert two queries are the same 
          neq) ;; assert two queries are not the same
 
@@ -53,11 +57,42 @@
 (define (assert-table-ordered table)
   (assert (table-content-ascending? (get-content table))))
 
-; assert that all element in a column is distinct, it enforces that all multiplicity set to 1
-(define (assert-table-col-distinct table col-num)
-  (assert 
-    (and (list-distinct? (map (lambda (r) (list-ref (car r) col-num)) (get-content table)))
-         (foldl && #t (map (lambda (r) (and (eq? (cdr r) 0) (eq? (cdr r) 1))) (get-content table))))))
+; list subset: whether all elements in list a are contained in b 
+(define (list-subset? a b)
+  (cond
+    [(empty? a) #t]
+    [else (if (not (member (car a) b)) #f (list-subset? (cdr a) b))]))
+
+; filter all zero mul. tuples. input type is table content.
+(define (filter-zero table)
+  (filter (lambda (r) (not (eq? (cdr r) 0))) table))
+
+; project table-content according to indices, only projecting tuple (no cardinality attached)
+(define (project-content table-content indices)
+  (map (lambda (r) (map (lambda (x) (list-ref (car r) x)) indices))
+                               table-content))
+
+; check that all element in a list of columns is distinct, it enforces that all multiplicity set to 1
+; col-nums: a list of column indices
+(define (assert-table-cols-distinct table col-nums)
+  (assert (table-cols-distinct? table col-nums)))
+
+(define (table-cols-distinct? table col-indices)
+  (let ([ftable (filter-zero (get-content table))])
+    (or
+     (empty? col-indices)
+     (and (list-distinct? (project-content ftable col-indices))
+          (foldl && #t (map (lambda (r) (eq? (cdr r) 1)) ftable))))))
+
+; primary key foreign key constraints
+(define (foreign-key-constraint? pk-table fk-table pk-indices fk-indices)
+  (let* ([pk-content (filter-zero (get-content pk-table))]
+         [fk-content (filter-zero (get-content fk-table))]
+         [pk-proj (project-content pk-content pk-indices)]
+         [fk-proj (project-content fk-content fk-indices)])
+  (and (table-cols-distinct? pk-table pk-indices) ; pk need to be a key first
+       (list-subset? fk-proj pk-proj) ; check containment
+       )))
 
 ;; assertions