verify コマンドを追加

bin/dune

@@ -51,3 +51,10 @@
   (name counterexample)
   (modules counterexample)
   (libraries birds))
+
+(executable
+  (public_name verify)
+  (name verify)
+  (modules verify)
+  (libraries birds))
+

bin/verify.ml

@@ -0,0 +1,16 @@
+open Birds
+
+let usage_message = "Usage: verify [--timeout <timeout>] <filename>"
+let filename = ref ""
+let timeout = ref 180
+let parse_rest filename' = filename := filename'
+let speclist = [
+  ("--timeout", Arg.Set_int timeout, "Set the timeout in seconds");
+]
+
+let _ =
+  Arg.parse speclist parse_rest usage_message;
+  let chan = open_in !filename in
+  let lexbuf = Lexing.from_channel chan in
+  let ast = Parser.main Lexer.token lexbuf in
+  Verify.verify true !timeout ast

examples/verify_comp.dl

@@ -0,0 +1,24 @@
+source classes('CLASS_ID':int, 'CLASS_NAME':string, 'FACULTY_ID':int).
+source faculty('FACULTY_ID':int, 'FACULTY_NAME':string, 'OFFICE':string).
+view v('CLASS_ID':int, 'CLASS_NAME':string, 'FACULTY_NAME':string).
+v(C,CN,FN) :- classes(C,CN,F), faculty(F,FN,O).
+all_classes(C,CN,F,FN,O) :- classes(C,CN,F), faculty(F,FN,O).
+mac(C,CN,F,FN,O) :- all_classes(C,CN,F,FN,O), not v(C,CN,FN).
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), not mac(_,_,_,_,_), faculty(F,FN,O).
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), not mac(_,_,_,_,_), not faculty(_,FN,_), F=-100, O='New'.
+pac(C,CN,F,FN,O) :- v(C,CN,FN), not all_classes(C,CN,_,FN,_), mac(_,_,F,_,O).
+uac(C,CN,F,FN,O) :- pac(C,CN,F,FN,O).
+uac(C,CN,F,FN,O) :- all_classes(C,CN,F,FN,O), not mac(C,CN,F,FN,O).
+% foreign key on base tables
+_|_ :- classes(_,_,F), not faculty(F,_,_).
+% constraints on views
+_|_ :- uac(_,_,F,FN1,_), uac(_,_,F,FN2,_), FN1<>FN2.
+_|_ :- uac(_,_,F,_,O1), uac(_,_,F,_,O2), O1<>O2.
+% faculty_name -> faculty_id on faculty
+_|_ :- faculty(F1, FN, _), faculty(F2, FN, _), F1<>F2.
+-classes(C,CN,F) :- classes(C,CN,F), not uac(C,CN,F,_,_).
++classes(C,CN,F) :- uac(C,CN,F,_,_), not classes(C,CN,F).
+-faculty(F,FN,O) :- faculty(F,FN,O), uac(_,_,F,_,_), not uac(_,_,F,FN,O).
+% The following rule is for strategy 2
+-faculty(F,FN,O) :- faculty(F,FN,O), uac(_,_,_,FN,_), not uac(_,_,F,FN,_).
++faculty(F,FN,O) :- uac(_,_,F,FN,O), not faculty(F,FN,O).

examples/verify_test1.dl

@@ -0,0 +1,24 @@
+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) :- tracks2(T,R,A,Q),Q > 2.
+⊥ :- tracks3(T,R,A,Q), NOT Q>2.
+
+% Album -> Quantity
+⊥ :- tracks2(_,_,A,Q1), tracks2(_,_,A,Q2), not Q1=Q2.
+⊥ :- tracks3(_,_,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2.
+% Track -> Rating
+⊥ :- tracks2(T,R1,_,_), tracks2(T,R2,_,_), not R1=R2.
+⊥ :- tracks3(T,R1,_,_), tracks3(T,R2,_,_), not R1=R2.
+
+% put
+-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q), Q > 2.
++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
+
+% relational revision for Track -> Rating
+_|_ :- tracks2(T,R1,A,Q), tracks3(T,R2,_,_), not R1=R2.
+_|_ :- tracks2(T,R1,A,Q), tracks3(T,R2,_,_), not R1=R2.
+
+% relational revision for Album -> Quantity
+-tracks2(T,R,A,Q1) :- tracks2(T,R,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2. 
++tracks2(T,R,A,Q2) :- tracks2(T,R,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2.

examples/verify_test2.dl

@@ -0,0 +1,24 @@
+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) :- tracks2(T,R,A,Q),Q > 2.
+⊥ :- tracks3(T,R,A,Q), NOT Q>2.
+
+% Album -> Quantity
+⊥ :- tracks2(_,_,A,Q1), tracks2(_,_,A,Q2), not Q1=Q2.
+⊥ :- tracks3(_,_,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2.
+% Track -> Rating
+⊥ :- tracks2(T,R1,_,_), tracks2(T,R2,_,_), not R1=R2.
+⊥ :- tracks3(T,R1,_,_), tracks3(T,R2,_,_), not R1=R2.
+
+% put
+-tracks2(T,R,A,Q) :- tracks2(T,R,A,Q), not tracks3(T,R,A,Q), Q > 2.
++tracks2(T,R,A,Q) :- tracks3(T,R,A,Q), not tracks2(T,R,A,Q).
+
+% relational revision for Track -> Rating
+%_|_ :- tracks2(T,R1,A,Q), tracks3(T,R2,_,_), not R1=R2.
+_|_ :- tracks2(T,R1,A,Q), tracks3(T,R2,_,_), not R1=R2.
+
+% relational revision for Album -> Quantity
+-tracks2(T,R,A,Q1) :- tracks2(T,R,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2. 
++tracks2(T,R,A,Q2) :- tracks2(T,R,A,Q1), tracks3(_,_,A,Q2), not Q1=Q2.