From bc27ddbbf659f6622de37fd7b5fcc0e27c7ac22e Mon Sep 17 00:00:00 2001 From: stechu Date: Mon, 5 Jun 2017 18:32:06 -0700 Subject: [PATCH 1/6] generalize table-col-distinct to mul. cols --- rosette/evaluator.rkt | 1 + rosette/tests/util-test.rkt | 2 +- rosette/util.rkt | 15 +++++++++++---- 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/rosette/evaluator.rkt b/rosette/evaluator.rkt index 60caf13..b930dd2 100644 --- a/rosette/evaluator.rkt +++ b/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) '()] diff --git a/rosette/tests/util-test.rkt b/rosette/tests/util-test.rkt index bb229f1..d2e5627 100644 --- a/rosette/tests/util-test.rkt +++ b/rosette/tests/util-test.rkt @@ -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)] diff --git a/rosette/util.rkt b/rosette/util.rkt index 8675272..d30503d 100644 --- a/rosette/util.rkt +++ b/rosette/util.rkt @@ -53,11 +53,18 @@ (define (assert-table-ordered table) (assert (table-content-ascending? (get-content table)))) +; filter all zero mul. tuples. input type is table content. +(define (filter-zero table) + (filter (lambda (r) (not (eq? (cdr r) 0))) 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)))))) +; col-nums: a list of column indices +(define (assert-table-col-distinct table col-nums) + (let ([ftable (filter-zero (get-content table))]) + (assert + (and (list-distinct? (map (lambda (r) (map (lambda (x) (list-ref (car r) x)) col-nums)) + ftable)) + (foldl && #t (map (lambda (r) (and (eq? (cdr r) 0) (eq? (cdr r) 1))) ftable)))))) ;; assertions From 9d26952c34c46c0ac22435e2fab9286abbdddc89 Mon Sep 17 00:00:00 2001 From: stechu Date: Tue, 6 Jun 2017 12:34:31 -0700 Subject: [PATCH 2/6] synthesize key constraints --- rosette/evaluator.rkt | 1 + rosette/tests/inline-exists.rkt | 115 ++++++++++++++++++++++++++++++++ rosette/tests/util-test.rkt | 2 +- rosette/util.rkt | 17 +++-- 4 files changed, 128 insertions(+), 7 deletions(-) create mode 100644 rosette/tests/inline-exists.rkt diff --git a/rosette/evaluator.rkt b/rosette/evaluator.rkt index b930dd2..1202c13 100644 --- a/rosette/evaluator.rkt +++ b/rosette/evaluator.rkt @@ -243,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))) diff --git a/rosette/tests/inline-exists.rkt b/rosette/tests/inline-exists.rkt new file mode 100644 index 0000000..3ae2210 --- /dev/null +++ b/rosette/tests/inline-exists.rkt @@ -0,0 +1,115 @@ +#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?) + +(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))) + +;(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))) + +(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") diff --git a/rosette/tests/util-test.rkt b/rosette/tests/util-test.rkt index d2e5627..3e549bc 100644 --- a/rosette/tests/util-test.rkt +++ b/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)))) diff --git a/rosette/util.rkt b/rosette/util.rkt index d30503d..8f45934 100644 --- a/rosette/util.rkt +++ b/rosette/util.rkt @@ -7,7 +7,8 @@ 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? same ;; assert two queries are the same neq) ;; assert two queries are not the same @@ -57,14 +58,18 @@ (define (filter-zero table) (filter (lambda (r) (not (eq? (cdr r) 0))) table)) -; assert that all element in a column is distinct, it enforces that all multiplicity set to 1 +; 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-col-distinct table col-nums) +(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))]) - (assert - (and (list-distinct? (map (lambda (r) (map (lambda (x) (list-ref (car r) x)) col-nums)) + (or + (empty? col-indices) + (and (list-distinct? (map (lambda (r) (map (lambda (x) (list-ref (car r) x)) col-indices)) ftable)) - (foldl && #t (map (lambda (r) (and (eq? (cdr r) 0) (eq? (cdr r) 1))) ftable)))))) + (foldl && #t (map (lambda (r) (eq? (cdr r) 1)) ftable)))))) ;; assertions From 726ff92229600a0e50e41a81a303fad035865f33 Mon Sep 17 00:00:00 2001 From: stechu Date: Tue, 6 Jun 2017 14:50:32 -0700 Subject: [PATCH 3/6] rename --- rosette/tests/synthesize-key.rkt | 110 +++++++++++++++++++++++++++++++ 1 file changed, 110 insertions(+) create mode 100644 rosette/tests/synthesize-key.rkt diff --git a/rosette/tests/synthesize-key.rkt b/rosette/tests/synthesize-key.rkt new file mode 100644 index 0000000..fd6ef8f --- /dev/null +++ b/rosette/tests/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") From 4203d5d73abeb7e7723ca4b10cacf520b4a7797c Mon Sep 17 00:00:00 2001 From: stechu Date: Tue, 6 Jun 2017 14:57:42 -0700 Subject: [PATCH 4/6] add foreign key example --- examples/conditional/join-elim-fk.cos | 16 ++++ rosette/tests/inline-exists.rkt | 115 -------------------------- 2 files changed, 16 insertions(+), 115 deletions(-) create mode 100644 examples/conditional/join-elim-fk.cos delete mode 100644 rosette/tests/inline-exists.rkt diff --git a/examples/conditional/join-elim-fk.cos b/examples/conditional/join-elim-fk.cos new file mode 100644 index 0000000..1f22028 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/rosette/tests/inline-exists.rkt b/rosette/tests/inline-exists.rkt deleted file mode 100644 index 3ae2210..0000000 --- a/rosette/tests/inline-exists.rkt +++ /dev/null @@ -1,115 +0,0 @@ -#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?) - -(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))) - -;(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))) - -(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") From 27d2e35519a7fa57b78cd1cb3cfb8e097adb9d9c Mon Sep 17 00:00:00 2001 From: stechu Date: Wed, 7 Jun 2017 00:50:50 -0700 Subject: [PATCH 5/6] synthesize pk-fk --- rosette/tests/join-elim-fk.rkt | 68 ++++++++++++++++++++++++++++++++++ rosette/util.rkt | 28 ++++++++++++-- 2 files changed, 93 insertions(+), 3 deletions(-) create mode 100644 rosette/tests/join-elim-fk.rkt diff --git a/rosette/tests/join-elim-fk.rkt b/rosette/tests/join-elim-fk.rkt new file mode 100644 index 0000000..b91e573 --- /dev/null +++ b/rosette/tests/join-elim-fk.rkt @@ -0,0 +1,68 @@ +#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)]))) +(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) + (println (list i j k n)) + )) +;(verify (same q1 q2)) diff --git a/rosette/util.rkt b/rosette/util.rkt index 8f45934..4d0d718 100644 --- a/rosette/util.rkt +++ b/rosette/util.rkt @@ -8,7 +8,9 @@ assert-table-non-empty ;; assert that a table is not empty assert-table-ordered ;; assert that the table is ordered assert-table-cols-distinct ;; assert that all values in a list of columns is distinct from each other - table-cols-distinct? + 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 same ;; assert two queries are the same neq) ;; assert two queries are not the same @@ -54,10 +56,21 @@ (define (assert-table-ordered table) (assert (table-content-ascending? (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) @@ -67,10 +80,19 @@ (let ([ftable (filter-zero (get-content table))]) (or (empty? col-indices) - (and (list-distinct? (map (lambda (r) (map (lambda (x) (list-ref (car r) x)) col-indices)) - ftable)) + (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 (define (same q1 q2) From 866ca6f8d7f6b6f176d79445b06eaacab2307aa4 Mon Sep 17 00:00:00 2001 From: stechu Date: Thu, 8 Jun 2017 16:49:30 -0700 Subject: [PATCH 6/6] refactor --- .../join-elim-fk.rkt | 2 + rosette/syn-preconditions/missing-pred.rkt | 64 +++++++++++++++++++ .../synthesize-key.rkt | 0 rosette/util.rkt | 1 + 4 files changed, 67 insertions(+) rename rosette/{tests => syn-preconditions}/join-elim-fk.rkt (97%) create mode 100644 rosette/syn-preconditions/missing-pred.rkt rename rosette/{tests => syn-preconditions}/synthesize-key.rkt (100%) diff --git a/rosette/tests/join-elim-fk.rkt b/rosette/syn-preconditions/join-elim-fk.rkt similarity index 97% rename from rosette/tests/join-elim-fk.rkt rename to rosette/syn-preconditions/join-elim-fk.rkt index b91e573..cfdb88c 100644 --- a/rosette/tests/join-elim-fk.rkt +++ b/rosette/syn-preconditions/join-elim-fk.rkt @@ -57,12 +57,14 @@ (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)) diff --git a/rosette/syn-preconditions/missing-pred.rkt b/rosette/syn-preconditions/missing-pred.rkt new file mode 100644 index 0000000..87005eb --- /dev/null +++ b/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)) + )) diff --git a/rosette/tests/synthesize-key.rkt b/rosette/syn-preconditions/synthesize-key.rkt similarity index 100% rename from rosette/tests/synthesize-key.rkt rename to rosette/syn-preconditions/synthesize-key.rkt diff --git a/rosette/util.rkt b/rosette/util.rkt index 4d0d718..62a5b39 100644 --- a/rosette/util.rkt +++ b/rosette/util.rkt @@ -11,6 +11,7 @@ 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