# HG changeset patch
# User blanchet
# Date 1504821735 -7200
# Node ID 556e19e43e4d412f5a0ac95ef95dbb279b33f235
# Parent  048524a4f537b9f3a95055a7ea74c0babf8e104d
added singular 'solver' option to Nunchaku

diff -r 048524a4f537 -r 556e19e43e4d src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:14 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Sep 08 00:02:15 2017 +0200
@@ -34,7 +34,10 @@
    ("verbose", "false"),
    ("wf_timeout", "0.5")];
 
-val negated_params =
+val alias_params =
+  [("solver", "solvers")];
+
+val negated_alias_params =
   [("dont_whack", "whack"),
    ("dont_specialize", "specialize"),
    ("dont_spy", "spy"),
@@ -48,7 +51,8 @@
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
-  AList.defined (op =) negated_params s orelse
+  AList.defined (op =) alias_params s orelse
+  AList.defined (op =) negated_alias_params s orelse
   member (op =) ["atoms", "card", "eval", "expect"] s orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
     ["atoms", "card", "dont_whack", "mono", "non_mono", "non_wf", "wf", "whack"];
@@ -57,7 +61,7 @@
   if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s);
 
 fun unnegate_param_name name =
-  (case AList.lookup (op =) negated_params name of
+  (case AList.lookup (op =) negated_alias_params name of
     NONE =>
     if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
     else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
@@ -65,15 +69,18 @@
   | some_name => some_name);
 
 fun normalize_raw_param (name, value) =
-  (case unnegate_param_name name of
-    SOME name' =>
-    [(name',
-      (case value of
-        ["false"] => ["true"]
-      | ["true"] => ["false"]
-      | [] => ["false"]
-      | _ => value))]
-  | NONE => [(name, value)]);
+  (case AList.lookup (op =) alias_params name of
+    SOME alias => [(alias, value)]
+  | NONE =>
+    (case unnegate_param_name name of
+      SOME name' =>
+      [(name',
+        (case value of
+          ["false"] => ["true"]
+        | ["true"] => ["false"]
+        | [] => ["false"]
+        | _ => value))]
+    | NONE => [(name, value)]));
 
 structure Data = Theory_Data
 (