Refactoring command line interface of MOLOSS

Author: jogiet

src/ast_modal.ml

@@ -18,6 +18,13 @@ type formula =
 	| Boxe of formula
 	| Diamond of formula
 
+type axiom = 
+  | AxS
+  | AxB
+  | Ax4
+  | Ax5
+  | AxCD
+
   (** This function propagate a negation in a modal formula.
      Helps to compute the NNF of the formula *)
 let rec prop_neg = function

src/decide.ml

@@ -522,37 +522,20 @@ end
 let axiom_to_dec_proc axiom =
   let rec aux = function
     | [] -> []
-    | "-S"::q | "-M"::q | "-boxeM"::q ->
-      if L.mem "-5" axiom then
+    | M.AxS::q ->
+      if L.mem M.Ax5 axiom then
         reflexiv::(aux q)
       else
         reflexiv::(aux q)
-    | "-K"::q -> aux q
-    | "-4"::q -> transitivity::(aux q)
-    | "-B"::q -> symmetric::(aux q)
-    | "-5"::q -> euclidean::(aux q)
-    | "-CD"::q -> functionnal::(aux q)
-    | t::q ->
-    begin
-      if String.length t <= 1
-      then begin
-        Printf.printf "argument inconnu : %s\n" t;
-        exit 0
-      end
-      else if String.get t 0 = '-' && String.get t 1 != '-'
-      then
-      begin
-        fpf "Axiome inconne : %s \n" t;
-        exit 1
-      end
-      else
-        aux q
-    end
+    | M.Ax4::q -> transitivity::(aux q)
+    | M.AxB::q -> symmetric::(aux q)
+    | M.Ax5::q -> euclidean::(aux q)
+    | M.AxCD::q -> functionnal::(aux q)
   in let res = aux axiom in
-  if L.mem  "-CD" axiom  || L.mem "-boxeM" axiom then
+  if L.mem  M.AxCD axiom then
     res@[forall]
-  else if (L.mem "-4" axiom || L.mem "-5" axiom || L.mem "--soft" axiom)
-    && not (L.mem "--soft-ignore" axiom) then
+  else if (L.mem M.Ax4 axiom || L.mem M.Ax5 axiom || Cmdline.(!optSoft))
+    && not (Cmdline.(!optSoftIgnore)) then
     res@[forall;softexist]
   else
     res@[forall;exist]

src/direct.ml

@@ -78,19 +78,19 @@ let getUniqueId () =
 
 (** An association list between the axioms and their FO translation *)
 let assoc =
-[("-M",";axiome de réfléxivité \n\
+[(Ast_modal.AxS,";axiome de réfléxivité \n\
 	(assert (forall ((w0 W)) (r w0 w0)))");
- ("-4",";axiome de trasitivité \n\
+ (Ast_modal.Ax4,";axiome de trasitivité \n\
  	(assert (forall ((w0 W) (w1 W) (w2 W)) \
 			(=> (and (r w0 w1) (r w1 w2)) (r w0 w2))))\n");
- ("-B",";axiome de symétrie \n\
+ (Ast_modal.AxB,";axiome de symétrie \n\
  	(assert (forall ((w1 W)(w2 W)) \
  			(=> (r w1 w2) (r w2 w1))))\n");
- ("-5",":axiome de euclidienne \n\
+ (Ast_modal.Ax5,":axiome de euclidienne \n\
  	(assert (forall ((w0 W) (w1 W) (w2 W)) \
  			(=> (and (r w0 w1) (r w0 w2)) \
 				(and (r w1 w2) (r w2 w1)))))\n");
- ("-CD",";axiome de fonctionelle \n\
+ (Ast_modal.AxCD,";axiome de fonctionelle \n\
  	(assert (forall ((w0 W) (w1 W) (w2 W)) \
  			(=> (and (r w0 w1) (r w0 w2)) \
 				(= w1 w2))))\n")]
@@ -105,24 +105,10 @@ begin
 		in begin
 			output_string oc ax;
 			p_out ax out;
+	    p_axiom oc out q;
 		end
 	else
-	begin
-    if String.length t <= 1
-    then begin
-      Printf.printf "argument inconnu : %s\n" t;
-      exit 1
-    end
-    else if String.get t 0 = '-' && String.get t 1 != '-'
-    then
-    begin
-      fpf "Axiome inconne : %s \n" t;
-      exit 1
-    end
-    else
-      p_axiom oc out q
-	 end;
-	p_axiom oc out q;
+    assert false
 end
 
 

src/moloss.ml

@@ -4,14 +4,13 @@ open Lexing
 
 module Dummy  = struct let truc = 0 end
 
+
 module DecisionArg : Sign.DecideArg =
 struct
-  let argument = match (Array.to_list (Sys.argv)) with
-    | _ :: _ :: q ->
-      q
-    | _  ->
-      Printf.printf "Give a formula to solve\n";
-      exit 1
+
+  let argument = 
+    let _ = Cmdline.init () in
+      Cmdline.(!axs)
 end
 
 module Decision = Decide.GetDecide(DecisionArg)
@@ -39,7 +38,7 @@ let argv = Array.to_list (Sys.argv) in
 	if List.mem "--out" argv then
 		Printf.printf "pas encore implem'\n"
 	else
-		if List.mem "--all" argv then
+		if Cmdline.(!optAll) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify) in
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify) in
     let module MiniSAT = Solv(Smtminisat.Smtmini)(Decision)(Simplify)
@@ -51,13 +50,13 @@ let argv = Array.to_list (Sys.argv) in
 				Printf.printf "c oracle minisat\n";
 				MiniSAT.solve f |> ignore;
 			end
-		else if List.mem "--z3" argv then
+		else if Cmdline.(!optZ3) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify)
 			in begin
 				Printf.printf "c oracle z3\n";
 				Z3.solve f |> ignore;
 			end
-		else if List.mem "--mSAT" argv then
+		else if Cmdline.(!optmSAT) then
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify)
 			in begin
 				Printf.printf "c oracle mSAT\n";
@@ -77,7 +76,7 @@ let argv = Array.to_list (Sys.argv) in
 	if List.mem "--out" argv then
 		Printf.printf "pas encore implem'\n"
 	else
-		if List.mem "--all" argv then
+		if Cmdline.(!optAll) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify) in
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify) in
     let module MiniSAT = Solv(Smtminisat.Smtmini)(Decision)(Simplify)
@@ -90,14 +89,14 @@ let argv = Array.to_list (Sys.argv) in
 				Printf.printf "c oracle minisat\n";
 				MiniSAT.solve f |> ignore;
 			end
-		else if List.mem "--z3" argv then
+		else if Cmdline.(!optZ3) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify)
 			in begin
         Printf.printf "c "; Pprinter.print_m f;
 				Printf.printf "c oracle z3\n";
 				Z3.solve f |> ignore;
 			end
-		else if List.mem "--mSAT" argv then
+		else if Cmdline.(!optmSAT) then
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify)
 			in begin
         Printf.printf "c "; Pprinter.print_m f;
@@ -119,7 +118,7 @@ let solve_assert f =
   if List.mem "--out" argv then
     Printf.printf "pas encore implem'\n"
   else
-  if List.mem "--all" argv then
+	if Cmdline.(!optAll) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify) in
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify) in
     let module MiniSAT = Solv(Smtminisat.Smtmini)(Decision)(Simplify)
@@ -132,14 +131,14 @@ let solve_assert f =
       Printf.printf "c oracle minisat\n";
       MiniSAT.solve f |> ignore;
     end
-  else if List.mem "--z3" argv then
+	else if Cmdline.(!optZ3) then
     let module Z3 = Solv(Smtz3.SMTz3)(Decision)(Simplify)
     in begin
       Printf.printf "c "; Pprinter.print_m f;
       Printf.printf "c oracle z3\n";
       Z3.solve f |> ignore;
     end
-  else if List.mem "--mSAT" argv then
+	else if Cmdline.(!optmSAT) then
     let module MSAT = Solv(Smtmsat.SMTmsat(Dummy))(Decision)(Simplify)
     in begin
       Printf.printf "c "; Pprinter.print_m f;
@@ -156,23 +155,23 @@ let solve_assert f =
 
 
 let _ =
-	let argv = Array.to_list (Sys.argv)
-	and t0 = Unix.gettimeofday ()
+  let _ = Cmdline.init () in
+  let t0 = Unix.gettimeofday ()
 	in begin
 	begin
-		match argv with
-  	| _ :: filename :: _  ->
+		match Cmdline.(!file) with
+  	| Some filename ->
     begin
       let file = open_in filename in
       let lb = Lexing.from_channel file in
       try
         let f = InToHyLoParser.file InToHyLoLexer.next_token lb in
-        if List.mem "--direct" argv then
+        if Cmdline.(!optDirect) then
           begin
             Printf.printf "c oracle direct\n";
-            (Direct.solve (Convertisseur.st 0 f) argv) |> ignore;
+            (Direct.solve (Convertisseur.st 0 f) Cmdline.(!axs)) |> ignore;
           end
-        else if List.mem "--get-simplify" argv then
+        else if Cmdline.(!optGetSimplify) then
           let fs = Simplify.simplify f in
           let l = Ast_modal.formLength f
           and d = Ast_modal.modDegree f
@@ -186,9 +185,9 @@ let _ =
 						else "\027[31m"
           in
             Printf.printf "%d,%d,%s%d\027[0m,%s%d\027[0m\n" l d cls ls cds ds
-        else if List.mem "--get-assert" argv then
+        else if Cmdline.(!optGetAssert) then
           solve_assert f
-        else if List.mem "--get-model" argv then
+        else if Cmdline.(!optGetAssert) then
           solve_model f
         else
           solve_vanilla f
@@ -206,12 +205,11 @@ let _ =
     end
 		| _ ->
 		begin
-			Printf.printf
-			"Give a filename of a InToHyLo formula to solve.\n";
+      Cmdline.print_usage ();
 			exit 1;
 		end;
 	end;
 		flush_all ();
-		if List.mem "--time" argv then
+		if Cmdline.(!optTime) then
     Printf.printf "c Done in %f s \n" (Unix.gettimeofday () -.t0);
 	end

src/sign.ml

@@ -104,7 +104,7 @@ module type DecideArg =
 sig
   (** Basically : this argument is the argument in the command line. it contains :
     - the axioms : -S, -K, -4, -5 *)
-		val argument : string list
+		val argument : Ast_modal.axiom list
 end
 
 

src/simplify.ml

@@ -124,9 +124,9 @@ let rec simplifyS = function
     end
 
 let getSimplify arg =
-  if L.mem "--no-simplify" arg then
+  if Cmdline.(!optNoSimplify) then
     (fun x -> x)
-  else if L.mem "-S" arg  || L.mem "--S4" arg || L.mem "--S5" arg
+  else if L.mem M.AxS arg
     then simplifyS
     else simplifyK
 

src/solve.ml

@@ -43,7 +43,15 @@ let add_model model new_bf =
     ISet.fold
       (fun ax model -> (ax, true)::model)
 			axs model
-  | _ -> assert false
+  | BFO.Conj _ ->
+    let _ = Printf.printf "C'est Conj"
+    in assert false
+  | BFO.Atom _ ->
+    let _ = Printf.printf "C'est Atom"
+    in assert false
+  | BFO.Not _ ->
+    let _ = Printf.printf "C'est Not"
+    in assert false
 
 
 module Solve
@@ -115,9 +123,11 @@ let solve f =
 				begin
 					List.iter (fun v -> SMT.dec_const v) new_var;
 					SMT.dec_assert new_bf ;
+          (*
           let new_m = add_model m new_bf in
           multi_decide config new_m
-				end;
+				  *)
+        end;
 				| D.SoftFound (new_var1,new_bf,new_var2,bf_soft,wght) ->
 				begin
 					List.iter (fun v -> SMT.dec_const v ) new_var1;

test.sh

@@ -1,4 +1,4 @@
-for filename in ./data/InToHyLo/test*; do
+for filename in ./data/InToHyLo/test-basic*; do
 	echo " "
 	echo "$filename"
 	./moloss.native "$filename" --time $*