Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

counterexampleコマンドの追加 #53

Merged
merged 3 commits into from
Jan 8, 2025
Merged

counterexampleコマンドの追加 #53

merged 3 commits into from
Jan 8, 2025

Conversation

hiroshi-cl
Copy link

@hiroshi-cl hiroshi-cl commented Nov 2, 2024 •
edited
Loading

概要

https://hackmd.io/J2B9Co2sTtKE5NI7KomV7g

https://github.com/dangtv/BIRDS/blob/c3cb32c4fed9dd38c0b3483349714c1f3123bbd3/src/debugger.ml からcounterexample 機能を移植してduneのコマンドとして追加しました

使い方

実行にはRacketとRosetteが必要です
https://github.com/proof-ninja/docker-verify-BIRDS をご利用ください

counterexampleを生成したいpropertyを getput, putget, disdelta (delta disjointness) から選んでください

$ dune exec counterexample [getput|putget|disdelta] [filename]

未実装機能

元のコードの中にあった以下のオプションは未実装です -> 実装しました

  • log: 詳細ログ出力するか。現在false(出さない)固定
  • cex_max: 出力するcounterexampleの最大。現在は5個固定
  • timeout: racketを呼び出すときのタイムアウト。現在は180秒固定

実行例

https://github.com/proof-ninja/docker-verify-BIRDS のコンテナ内で実行しました

verify_invalid_getput1.dl

root@b274eb993e3f:/birds# dune exec counterexample getput examples/verify_invalid_getput1.dl 
% Invalidity: The following counterexample shows that getput is not satisfied:
tracks2('..aa..', 0, '..aa..', 2).

log=true のとき

______string-mapped program______      
String active domain in the program is: '..aa..', '..bb..', '..cc..', '..dd..', '..ee..', '..ff..', '..gg..', '..hh..', '..ii..', '..jj..', '..kk..', '..ll..', '..mm..', '..nn..', '..oo..', '..pp..', '..qq..', '..rr..', '..ss..', '..tt..', '..uu..', '..vv..', '..ww..', '..xx..', '..yy..', '..zz..'
source tracks2('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
view tracks3('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
⊥() :- tracks3(T, R, A, Q) , Q <= 2.
⊥() :- tracks3(T, R, A, Q) , Q <= 2.
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
tracks3(T, R, A, Q) :- tracks2(T, R, A, Q) , Q > 2.

__________________________________
==> generating a counterexample for getput
_____preprocessed datalog rules_______
tracks3(T, R, A, Q) :- tracks2(T, R, A, Q) , Q > 2.
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
+__dummy__tracks2(COL0, COL1, COL2, COL3) :- +tracks2(COL0, COL1, COL2, COL3) , not tracks2(COL0, COL1, COL2, COL3).
⊥() :- tracks3(T, R, A, Q) , Q <= 2.
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
-__dummy__tracks2(COL0, COL1, COL2, COL3) :- -tracks2(COL0, COL1, COL2, COL3) , tracks2(COL0, COL1, COL2, COL3).
______________

==> generating constraint not involving view
_____constraints not involing view_______
source tracks2('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
view tracks3('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
tracks3(T, R, A, Q) :- tracks2(T, R, A, Q) , Q > 2.
______________

==> generating a counterexample by Rosette
--------------
Racket code:

#lang rosette/safe

(define curry
    (lambda (f . c) (lambda x (apply f (append c x)))))

(define stitch
    (lambda (tuples element)
        (map (curry cons element) tuples)))

(define flatten
    (curry apply append))

(define cartesian
    (lambda (l1 l2)
        (flatten (map (curry stitch l2) l1))))

(define cartesian-lists
    (lambda (lists)
        (foldr cartesian '(()) lists)))

(define cartesian-map
    (lambda (f . lists)
        (map (curry apply f) (cartesian-lists lists))))



(define-symbolic tracks2$TRACK$1 integer?)
 (assert (and (< -1  tracks2$TRACK$1) (< tracks2$TRACK$1 26)))
(define-symbolic tracks2$RATING$1 integer?)
(define-symbolic tracks2$ALBUM$1 integer?)
 (assert (and (< -1  tracks2$ALBUM$1) (< tracks2$ALBUM$1 26)))
(define-symbolic tracks2$QUANTITY$1 integer?)

(define tracks2_tuple_1 (list tracks2$TRACK$1 tracks2$RATING$1 tracks2$ALBUM$1 tracks2$QUANTITY$1))

(define tracks2 (list  tracks2_tuple_1))



(define delta_del___dummy__tracks2 (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1) (list-ref tuplelst 2) (list-ref tuplelst 3))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 1) 2) (list-ref (list-ref tuplelst 1) 3))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 0)) (and (equal? (list-ref (list-ref tuplelst 1) 3) (list-ref (list-ref tuplelst 0) 3)) true))))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (> (list-ref (list-ref tuplelst 0) 3) 2)) (cartesian-map list tracks2))))))) (cartesian-map list tracks2))) tracks2)))))))

(define delta_ins___dummy__tracks2 (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1) (list-ref tuplelst 2) (list-ref tuplelst 3))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks2)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks2)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (> (list-ref (list-ref tuplelst 0) 3) 2)) (cartesian-map list tracks2)))))))))))))

(define emptiness (append delta_del___dummy__tracks2 delta_ins___dummy__tracks2))

(solve (assert (< 0 (length emptiness))))
--------------
>>> Checked by Rosette
________Model from rosette______
(model
 [tracks2$TRACK$1 0]
 [tracks2$ALBUM$1 0]
 [tracks2$QUANTITY$1 2])
_____________________
>>> parsing model from rosette
(tracks2, TRACK, 1) = 0
(tracks2, ALBUM, 1) = 0
(tracks2, QUANTITY, 1) = 2

________getput counterexample________ 
tracks2('..aa..', 0, '..aa..', 2).

________________
% Invalidity: The following counterexample shows that getput is not satisfied:
tracks2('..aa..', 0, '..aa..', 2).

verify_invalid_getput2.dl

root@b274eb993e3f:/birds# dune exec counterexample getput examples/verify_invalid_getput2.dl 
% Invalidity: The following counterexample shows that getput is not satisfied:
b(0, 0).
a(0, 1).

log=true のとき

______string-mapped program______      
String active domain in the program is: '..aa..', '..bb..', '..cc..', '..dd..', '..ee..', '..ff..', '..gg..', '..hh..', '..ii..', '..jj..', '..kk..', '..ll..', '..mm..', '..nn..', '..oo..', '..pp..', '..qq..', '..rr..', '..ss..', '..tt..', '..uu..', '..vv..', '..ww..', '..xx..', '..yy..', '..zz..'
source b('B':int, 'C':int).
source a('A':int, 'B':int).
view s('A':int, 'B':int, 'C':int).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
+b(B, C) :- s(_, B, C) , not b(B, C).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
+a(A, B) :- s(A, B, _) , not a(A, B).
-a(A, B) :- a(A, B) , not s(A, B, _).
s(A, B, C) :- a(A, B) , b(B, C).

__________________________________
==> generating a counterexample for getput
_____preprocessed datalog rules_______
s(A, B, C) :- a(A, B) , b(B, C).
+b(B, C) :- s(_, B, C) , not b(B, C).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
+a(A, B) :- s(A, B, _) , not a(A, B).
+__dummy__a(COL0, COL1) :- +a(COL0, COL1) , not a(COL0, COL1).
+__dummy__b(COL0, COL1) :- +b(COL0, COL1) , not b(COL0, COL1).
-a(A, B) :- a(A, B) , not s(A, B, _).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
-__dummy__b(COL0, COL1) :- -b(COL0, COL1) , b(COL0, COL1).
-__dummy__a(COL0, COL1) :- -a(COL0, COL1) , a(COL0, COL1).
______________

==> generating constraint not involving view
_____constraints not involing view_______
source b('B':int, 'C':int).
source a('A':int, 'B':int).
view s('A':int, 'B':int, 'C':int).
+a(A, B) :- s(A, B, _) , not a(A, B).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
-a(A, B) :- a(A, B) , not s(A, B, _).
+b(B, C) :- s(_, B, C) , not b(B, C).
s(A, B, C) :- a(A, B) , b(B, C).
______________

==> generating a counterexample by Rosette
--------------
Racket code:

#lang rosette/safe

(define curry
    (lambda (f . c) (lambda x (apply f (append c x)))))

(define stitch
    (lambda (tuples element)
        (map (curry cons element) tuples)))

(define flatten
    (curry apply append))

(define cartesian
    (lambda (l1 l2)
        (flatten (map (curry stitch l2) l1))))

(define cartesian-lists
    (lambda (lists)
        (foldr cartesian '(()) lists)))

(define cartesian-map
    (lambda (f . lists)
        (map (curry apply f) (cartesian-lists lists))))



(define-symbolic a$A$1 integer?)
(define-symbolic a$B$1 integer?)

(define a_tuple_1 (list a$A$1 a$B$1))

(define a (list  a_tuple_1))


(define-symbolic b$B$1 integer?)
(define-symbolic b$C$1 integer?)

(define b_tuple_1 (list b$B$1 b$C$1))

(define b (list  b_tuple_1))



(define delta_del___dummy__a (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 0)) true))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a b))))))) (cartesian-map list a))) a)))))))

(define delta_del___dummy__b (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 0)) true))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 0)) (and (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 1) 1)) true))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a b)))))) true))) (cartesian-map list b (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a b)))))) b)))))))

(define delta_ins___dummy__a (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) a)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) a)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a b)))))))))))))

(define delta_ins___dummy__b (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) b)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 1)) true))) b)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a b)))))))))))))

(define emptiness (append delta_del___dummy__a delta_del___dummy__b delta_ins___dummy__a delta_ins___dummy__b))

(solve (assert (< 0 (length emptiness))))
--------------
>>> Checked by Rosette
________Model from rosette______
(model
 [a$B$1 1]
 [b$B$1 0])
_____________________
>>> parsing model from rosette
(a, B, 1) = 1
(b, B, 1) = 0

________getput counterexample________ 
b(0, 0).
a(0, 1).

________________
% Invalidity: The following counterexample shows that getput is not satisfied:
b(0, 0).
a(0, 1).

verify_invalid_putget1.dl

root@b274eb993e3f:/birds# dune exec counterexample putget examples/verify_invalid_putget1.dl 
% Invalidity: The following counterexample shows that putget is not satisfied:
tracks3('..aa..', 0, '..aa..', 0).
tracks2('..aa..', 0, '..aa..', -1).

log=true のとき

______string-mapped program______      
String active domain in the program is: '..aa..', '..bb..', '..cc..', '..dd..', '..ee..', '..ff..', '..gg..', '..hh..', '..ii..', '..jj..', '..kk..', '..ll..', '..mm..', '..nn..', '..oo..', '..pp..', '..qq..', '..rr..', '..ss..', '..tt..', '..uu..', '..vv..', '..ww..', '..xx..', '..yy..', '..zz..'
source tracks2('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
view tracks3('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
tracks3(T, R, A, Q) :- tracks2(T, R, A, Q) , Q > 2.

__________________________________
==> generating a counterexample for putget
_____putget datalog program_______
source tracks2('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
view tracks3('TRACK':string, 'RATING':int, 'ALBUM':string, 'QUANTITY':int).
__dummy_new_tracks3(T, R, A, Q) :- __dummy_new_tracks2(T, R, A, Q) , Q > 2.
__dummy_new_tracks2(COL0, COL1, COL2, COL3) :- tracks2(COL0, COL1, COL2, COL3) , not -tracks2(COL0, COL1, COL2, COL3).
__dummy_new_tracks2(COL0, COL1, COL2, COL3) :- +tracks2(COL0, COL1, COL2, COL3).
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
______________

_____preprocessed datalog rules_______
__emptinesstracks3(TRACK, RATING, ALBUM, QUANTITY) :- __dummy_new_tracks3(TRACK, RATING, ALBUM, QUANTITY) , not tracks3(TRACK, RATING, ALBUM, QUANTITY).
__emptinesstracks3(TRACK, RATING, ALBUM, QUANTITY) :- tracks3(TRACK, RATING, ALBUM, QUANTITY) , not __dummy_new_tracks3(TRACK, RATING, ALBUM, QUANTITY).
-tracks2(T, R, A, Q) :- tracks2(T, R, A, Q) , not tracks3(T, R, A, Q).
__dummy_new_tracks3(T, R, A, Q) :- __dummy_new_tracks2(T, R, A, Q) , Q > 2.
+tracks2(T, R, A, Q) :- tracks3(T, R, A, Q) , not tracks2(T, R, A, Q).
__dummy_new_tracks2(COL0, COL1, COL2, COL3) :- tracks2(COL0, COL1, COL2, COL3) , not -tracks2(COL0, COL1, COL2, COL3).
__dummy_new_tracks2(COL0, COL1, COL2, COL3) :- +tracks2(COL0, COL1, COL2, COL3).
______________

==> generating racket code for all constraints
==> generating a counterexample by Rosette
--------------
Racket code:

#lang rosette/safe

(define curry
    (lambda (f . c) (lambda x (apply f (append c x)))))

(define stitch
    (lambda (tuples element)
        (map (curry cons element) tuples)))

(define flatten
    (curry apply append))

(define cartesian
    (lambda (l1 l2)
        (flatten (map (curry stitch l2) l1))))

(define cartesian-lists
    (lambda (lists)
        (foldr cartesian '(()) lists)))

(define cartesian-map
    (lambda (f . lists)
        (map (curry apply f) (cartesian-lists lists))))



(define-symbolic tracks2$TRACK$1 integer?)
 (assert (and (< -1  tracks2$TRACK$1) (< tracks2$TRACK$1 26)))
(define-symbolic tracks2$RATING$1 integer?)
(define-symbolic tracks2$ALBUM$1 integer?)
 (assert (and (< -1  tracks2$ALBUM$1) (< tracks2$ALBUM$1 26)))
(define-symbolic tracks2$QUANTITY$1 integer?)

(define tracks2_tuple_1 (list tracks2$TRACK$1 tracks2$RATING$1 tracks2$ALBUM$1 tracks2$QUANTITY$1))

(define tracks2 (list  tracks2_tuple_1))


(define-symbolic tracks3$TRACK$1 integer?)
 (assert (and (< -1  tracks3$TRACK$1) (< tracks3$TRACK$1 26)))
(define-symbolic tracks3$RATING$1 integer?)
(define-symbolic tracks3$ALBUM$1 integer?)
 (assert (and (< -1  tracks3$ALBUM$1) (< tracks3$ALBUM$1 26)))
(define-symbolic tracks3$QUANTITY$1 integer?)

(define tracks3_tuple_1 (list tracks3$TRACK$1 tracks3$RATING$1 tracks3$ALBUM$1 tracks3$QUANTITY$1))

(define tracks3 (list  tracks3_tuple_1))



(define putget_emptiness (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1) (list-ref tuplelst 2) (list-ref tuplelst 3))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks3)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (> (list-ref (list-ref tuplelst 0) 3) 2)) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks3)))) (cartesian-map list tracks2))))))) (cartesian-map list tracks2))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks2)))) (cartesian-map list tracks3)))))))))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (> (list-ref (list-ref tuplelst 0) 3) 2)) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks3)))) (cartesian-map list tracks2))))))) (cartesian-map list tracks2))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 0) 3))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 3) (list-ref (list-ref tuplelst 0) 3)) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))))) tracks2)))) (cartesian-map list tracks3))))))))))))) (cartesian-map list tracks3))))))))

(solve (assert (< 0 (length putget_emptiness))))
--------------
>>> Checked by Rosette
________Model from rosette______
(model
 [tracks2$TRACK$1 0]
 [tracks2$RATING$1 0]
 [tracks2$ALBUM$1 0]
 [tracks2$QUANTITY$1 -1]
 [tracks3$TRACK$1 0]
 [tracks3$RATING$1 0]
 [tracks3$ALBUM$1 0]
 [tracks3$QUANTITY$1 0])
_____________________
>>> parsing model from rosette
(tracks2, TRACK, 1) = 0
(tracks2, RATING, 1) = 0
(tracks2, ALBUM, 1) = 0
(tracks2, QUANTITY, 1) = -1
(tracks3, TRACK, 1) = 0
(tracks3, RATING, 1) = 0
(tracks3, ALBUM, 1) = 0
(tracks3, QUANTITY, 1) = 0

________putget counterexample________ 
tracks3('..aa..', 0, '..aa..', 0).
tracks2('..aa..', 0, '..aa..', -1).

________________
% Invalidity: The following counterexample shows that putget is not satisfied:
tracks3('..aa..', 0, '..aa..', 0).
tracks2('..aa..', 0, '..aa..', -1).

verify_invalid_putget2.dl

root@b274eb993e3f:/birds# dune exec counterexample putget examples/verify_invalid_putget2.dl 
% Invalidity: The following counterexample shows that putget is not satisfied:
s(0, 0, 0).
b(1, 0).
a(0, 1).

log=true のとき

______string-mapped program______      
String active domain in the program is: '..aa..', '..bb..', '..cc..', '..dd..', '..ee..', '..ff..', '..gg..', '..hh..', '..ii..', '..jj..', '..kk..', '..ll..', '..mm..', '..nn..', '..oo..', '..pp..', '..qq..', '..rr..', '..ss..', '..tt..', '..uu..', '..vv..', '..ww..', '..xx..', '..yy..', '..zz..'
source b('B':int, 'C':int).
source a('A':int, 'B':int).
view s('A':int, 'B':int, 'C':int).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
+b(B, C) :- s(_, B, C) , not b(B, C).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
+a(A, B) :- s(A, B, _) , not a(A, B).
s(A, B, C) :- a(A, B) , b(B, C).

__________________________________
==> generating a counterexample for putget
_____putget datalog program_______
source b('B':int, 'C':int).
source a('A':int, 'B':int).
view s('A':int, 'B':int, 'C':int).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
__dummy_new_s(A, B, C) :- __dummy_new_a(A, B) , __dummy_new_b(B, C).
__dummy_new_b(COL0, COL1) :- b(COL0, COL1) , not -b(COL0, COL1).
__dummy_new_b(COL0, COL1) :- +b(COL0, COL1).
__dummy_new_a(COL0, COL1) :- a(COL0, COL1).
__dummy_new_a(COL0, COL1) :- +a(COL0, COL1).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
+b(B, C) :- s(_, B, C) , not b(B, C).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
+a(A, B) :- s(A, B, _) , not a(A, B).
______________

_____preprocessed datalog rules_______
+b(B, C) :- s(_, B, C) , not b(B, C).
__dummy_new_a(COL0, COL1) :- a(COL0, COL1).
__dummy_new_a(COL0, COL1) :- +a(COL0, COL1).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
+a(A, B) :- s(A, B, _) , not a(A, B).
__dummy_new_s(A, B, C) :- __dummy_new_a(A, B) , __dummy_new_b(B, C).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
__dummy_new_b(COL0, COL1) :- b(COL0, COL1) , not -b(COL0, COL1).
__dummy_new_b(COL0, COL1) :- +b(COL0, COL1).
__emptinesss(A, B, C) :- __dummy_new_s(A, B, C) , not s(A, B, C).
__emptinesss(A, B, C) :- s(A, B, C) , not __dummy_new_s(A, B, C).
______________

==> generating racket code for all constraints
_____preprocessed datalog rules_______
+b(B, C) :- s(_, B, C) , not b(B, C).
-b(B, C) :- b(B, C) , s(_, B, _) , not s(_, B, C).
⊥() :- s(_, B, C1) , s(_, B, C2) , C1 <> C2.
⊥() :- a(_, B) , not b(B, _).
+a(A, B) :- s(A, B, _) , not a(A, B).
______________

==> generating a counterexample by Rosette
--------------
Racket code:

#lang rosette/safe

(define curry
    (lambda (f . c) (lambda x (apply f (append c x)))))

(define stitch
    (lambda (tuples element)
        (map (curry cons element) tuples)))

(define flatten
    (curry apply append))

(define cartesian
    (lambda (l1 l2)
        (flatten (map (curry stitch l2) l1))))

(define cartesian-lists
    (lambda (lists)
        (foldr cartesian '(()) lists)))

(define cartesian-map
    (lambda (f . lists)
        (map (curry apply f) (cartesian-lists lists))))



(define-symbolic a$A$1 integer?)
(define-symbolic a$B$1 integer?)

(define a_tuple_1 (list a$A$1 a$B$1))

(define a (list  a_tuple_1))


(define-symbolic b$B$1 integer?)
(define-symbolic b$C$1 integer?)

(define b_tuple_1 (list b$B$1 b$C$1))

(define b (list  b_tuple_1))


(define-symbolic s$A$1 integer?)
(define-symbolic s$B$1 integer?)
(define-symbolic s$C$1 integer?)

(define s_tuple_1 (list s$A$1 s$B$1 s$C$1))

(define s (list  s_tuple_1))

(define constr_emptiness (map (lambda (tuplelst) (list )) (map (lambda (tuplelst) '()) (cartesian-map list (append (map (lambda (tuplelst) '()) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1)) (and (not (equal? (list-ref (list-ref tuplelst 0) 2) (list-ref (list-ref tuplelst 1) 2))) true))) (cartesian-map list s s))) (map (lambda (tuplelst) '()) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 1))) b)))) (cartesian-map list a))))))))

(assert (= 0 (length constr_emptiness)))

(define putget_emptiness (map (lambda (tuplelst) (list (list-ref tuplelst 0) (list-ref tuplelst 1) (list-ref tuplelst 2))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true)))) s)))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a)) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) a)))) (cartesian-map list s)))))) (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 0)) (and (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 1) 1)) true))) s))) true))) (cartesian-map list b s))))))) (cartesian-map list b))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 1)) true))) b)))) (cartesian-map list s)))))))))))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true)))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 1) 1))) (filter (lambda (tuplelst) (equal? (list-ref (list-ref tuplelst 1) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list a)) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) a)))) (cartesian-map list s)))))) (append (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 0)) true))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 1))) (filter (lambda (tuplelst) (and (equal? (list-ref (list-ref tuplelst 1) 1) (list-ref (list-ref tuplelst 0) 0)) (and (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 2) (list-ref (list-ref tuplelst 0) 1)) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 1) 1)) true))) s))) true))) (cartesian-map list b s))))))) (cartesian-map list b))) (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 0) (list-ref (list-ref tuplelst 0) 1))) (cartesian-map list (map (lambda (tuplelst) (list (list-ref (list-ref tuplelst 0) 1) (list-ref (list-ref tuplelst 0) 2))) (filter (lambda (tuplelst) (= 0 (length (filter (lambda (negtuple) (and (equal? (list-ref negtuple 1) (list-ref (list-ref tuplelst 0) 2)) (and (equal? (list-ref negtuple 0) (list-ref (list-ref tuplelst 0) 1)) true))) b)))) (cartesian-map list s))))))))))))) (cartesian-map list s))))))))

(solve (assert (< 0 (length putget_emptiness))))
--------------
>>> Checked by Rosette
________Model from rosette______
(model
 [a$A$1 0]
 [a$B$1 1]
 [b$B$1 1]
 [b$C$1 0]
 [s$A$1 0]
 [s$B$1 0]
 [s$C$1 0])
_____________________
>>> parsing model from rosette
(a, A, 1) = 0
(a, B, 1) = 1
(b, B, 1) = 1
(b, C, 1) = 0
(s, A, 1) = 0
(s, B, 1) = 0
(s, C, 1) = 0

________putget counterexample________ 
s(0, 0, 0).
b(1, 0).
a(0, 1).

________________
% Invalidity: The following counterexample shows that putget is not satisfied:
s(0, 0, 0).
b(1, 0).
a(0, 1).

verify_valid1.dl

root@4a3db892195f:/birds# dune exec counterexample getput examples/verify_valid1.dl 
% Fail to generate a counterexample of getput: Stop generating a counterexample of getput: Timeout
root@4a3db892195f:/birds# dune exec counterexample putget examples/verify_valid1.dl 
% Fail to generate a counterexample of putget: Stop generating a counterexample of putget: Timeout

@hiroshi-cl hiroshi-cl marked this pull request as ready for review November 5, 2024 14:22
@yoshihiro503
Copy link
Member

--timeout オプションでtimeout時間を指定できるようにしてほしいです。

hiroshi-cl
hiroshi-cl commented Nov 20, 2024
View reviewed changes
src/run_counterexample.ml Outdated Show resolved Hide resolved
@hiroshi-cl
Copy link
Author

動作確認はまだですがとりいそぎ元のBIRDSにあった --log, -x, --counterexample, -t の4つのoptionが使えるようにしておきました
--timeout は -t のエイリアスということにしました

例

dune exec counterexample putget examples/verify_invalid_getput1.dl -- --timeout 180

@hiroshi-cl
Copy link
Author

動作確認も行いました

@hiroshi-cl
Copy link
Author

hiroshi-cl#2

@hiroyukikato
Copy link
Collaborator

Thanks, LGTM

@hiroshi-cl
Copy link
Author

見ていただいてありがとうございます 🙇

@hiroshi-cl hiroshi-cl merged commit 20d9abd into proof-ninja:master Jan 8, 2025
2 checks passed
@hiroshi-cl hiroshi-cl deleted the feat/counterexample branch January 8, 2025 11:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hiroyukikato hiroyukikato Awaiting requested review from hiroyukikato

@cedretaber cedretaber Awaiting requested review from cedretaber

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@hiroshi-cl @yoshihiro503 @hiroyukikato