Add --timeout option.

bin/verify.ml

@@ -1,8 +1,28 @@
 open Birds
 
+type args = {
+  filename: string;
+  timeout: int;
+}
+
+let default_timeout = 180
+let default_args = {
+  filename = "";
+  timeout = default_timeout;
+}
+
+let rec parse_argv args = function
+  | [] -> args
+  | "--timeout" :: timeout :: tail ->
+    begin match int_of_string_opt timeout with
+    | Some timeout -> parse_options { args with timeout } tail
+    | None -> failwith @@ Printf.sprintf "Invalid timeout: %s" timeout
+    end
+  | filename :: tail -> parse_options { args with filename } tail
+
 let _ =
-  let filename = Sys.argv.(1) in
-  let chan = open_in filename in
+  let args = parse_argv default_args @@ List.tl @@ Array.to_list Sys.argv in
+  let chan = open_in args.filename in
   let lexbuf = Lexing.from_channel chan in
   let ast = Parser.main Lexer.token lexbuf in
-  Verify.verify true 600 ast
+  Verify.verify true args.timeout ast

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.