# HG changeset patch # User blanchet # Date 1236364651 -3600 # Node ID 853778f6ef7d83e004445464a585e6d0b26e87e0 # Parent 0e0cb7ac02813a949826acceeceaf4c66781f99b Added "expect" option to Refute, like in Nitpick, that allows to write regression tests. Also replaced calls to "Output.immediate_output" with "priority" or "tracing", because "immediate_output" causes some problems (as explained by Makarius to Sascha). diff -r 0e0cb7ac0281 -r 853778f6ef7d src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Mar 06 17:21:17 2009 +0100 +++ b/src/HOL/Tools/refute.ML Fri Mar 06 19:37:31 2009 +0100 @@ -144,7 +144,7 @@ (* formula/model generation *) (* *) (* The following parameters are supported (and required (!), except for *) -(* "sizes"): *) +(* "sizes" and "expect"): *) (* *) (* Name Type Description *) (* *) @@ -157,6 +157,8 @@ (* formula. *) (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) (* "satsolver" string SAT solver to be used. *) +(* "expect" string Expected result ("genuine", "potential", "none", or *) +(* "unknown") *) (* ------------------------------------------------------------------------- *) type params = @@ -166,7 +168,8 @@ maxsize : int, maxvars : int, maxtime : int, - satsolver: string + satsolver: string, + expect : string }; (* ------------------------------------------------------------------------- *) @@ -387,6 +390,7 @@ val maxtime = read_int (allparams, "maxtime") (* string *) val satsolver = read_string (allparams, "satsolver") + val expect = the_default "" (AList.lookup (op =) allparams "expect") (* all remaining parameters of the form "string=int" are collected in *) (* 'sizes' *) (* TODO: it is currently not possible to specify a size for a type *) @@ -399,7 +403,7 @@ andalso name<>"satsolver") allparams) in {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars, - maxtime=maxtime, satsolver=satsolver} + maxtime=maxtime, satsolver=satsolver, expect=expect} end; @@ -731,7 +735,7 @@ (* check this. However, getting this really right seems *) (* difficult because the user may state arbitrary axioms, *) (* which could interact with overloading to create loops. *) - ((*Output.immediate_output (" unfolding: " ^ axname);*) + ((*Output.tracing (" unfolding: " ^ axname);*) unfold_loop rhs) | NONE => t) | Free _ => t @@ -771,7 +775,7 @@ fun collect_axioms thy t = let - val _ = Output.immediate_output "Adding axioms..." + val _ = Output.tracing "Adding axioms..." (* (string * Term.term) list *) val axioms = Theory.all_axioms_of thy (* string * Term.term -> Term.term list -> Term.term list *) @@ -782,7 +786,7 @@ if member (op aconv) axs ax' then axs else ( - Output.immediate_output (" " ^ axname); + Output.tracing axname; collect_term_axioms (ax' :: axs, ax') ) end @@ -945,7 +949,7 @@ (collect_term_axioms (axs, t1), t2) (* Term.term list *) val result = map close_form (collect_term_axioms ([], t)) - val _ = writeln " ...done." + val _ = Output.tracing " ...done." in result end; @@ -1155,25 +1159,26 @@ (* theory -> params -> Term.term -> bool -> unit *) - fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver} t - negate = + fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver, + expect} t negate = let (* unit -> unit *) fun wrapper () = let val u = unfold_defs thy t - val _ = writeln ("Unfolded term: " ^ Syntax.string_of_term_global thy u) + val _ = Output.tracing ("Unfolded term: " ^ + Syntax.string_of_term_global thy u) val axioms = collect_axioms thy u (* Term.typ list *) val types = Library.foldl (fn (acc, t') => acc union (ground_types thy t')) ([], u :: axioms) - val _ = writeln ("Ground types: " + val _ = Output.tracing ("Ground types: " ^ (if null types then "none." else commas (map (Syntax.string_of_typ_global thy) types))) (* we can only consider fragments of recursive IDTs, so we issue a *) (* warning if the formula contains a recursive IDT *) (* TODO: no warning needed for /positive/ occurrences of IDTs *) - val _ = if Library.exists (fn + val maybe_spurious = Library.exists (fn Type (s, _) => (case DatatypePackage.get_datatype thy s of SOME info => (* inductive datatype *) @@ -1187,18 +1192,19 @@ Library.exists DatatypeAux.is_rec_type ds) constrs end | NONE => false) - | _ => false) types then + | _ => false) types + val _ = if maybe_spurious then warning ("Term contains a recursive datatype; " ^ "countermodel(s) may be spurious!") else () - (* (Term.typ * int) list -> unit *) + (* (Term.typ * int) list -> string *) fun find_model_loop universe = let val init_model = (universe, []) val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, bounds = [], wellformed = True} - val _ = Output.immediate_output ("Translating term (sizes: " + val _ = Output.tracing ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") (* translate 'u' and all axioms *) val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') => @@ -1216,31 +1222,37 @@ val fm_ax = PropLogic.all (map toTrue (tl intrs)) val fm = PropLogic.all [#wellformed args, fm_ax, fm_u] in - Output.immediate_output " invoking SAT solver..."; + Output.priority "Invoking SAT solver..."; (case SatSolver.invoke_solver satsolver fm of SatSolver.SATISFIABLE assignment => - (writeln " model found!"; - writeln ("*** Model found: ***\n" ^ print_model thy model - (fn i => case assignment i of SOME b => b | NONE => true))) + (Output.priority ("*** Model found: ***\n" ^ print_model thy model + (fn i => case assignment i of SOME b => b | NONE => true)); + "genuine") | SatSolver.UNSATISFIABLE _ => - (Output.immediate_output " no model exists.\n"; + (Output.priority "No model exists."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' - | NONE => writeln - "Search terminated, no larger universe within the given limits.") + | NONE => (Output.priority + "Search terminated, no larger universe within the given limits."; + "none")) | SatSolver.UNKNOWN => - (Output.immediate_output " no model found.\n"; + (Output.priority "No model found."; case next_universe universe sizes minsize maxsize of SOME universe' => find_model_loop universe' - | NONE => writeln - "Search terminated, no larger universe within the given limits.") + | NONE => (Output.priority + "Search terminated, no larger universe within the given limits."; + "unknown")) ) handle SatSolver.NOT_CONFIGURED => - error ("SAT solver " ^ quote satsolver ^ " is not configured.") + (error ("SAT solver " ^ quote satsolver ^ " is not configured."); + "unknown") end handle MAXVARS_EXCEEDED => - writeln ("\nSearch terminated, number of Boolean variables (" - ^ string_of_int maxvars ^ " allowed) exceeded.") + (Output.priority ("Search terminated, number of Boolean variables (" + ^ string_of_int maxvars ^ " allowed) exceeded."); + "unknown") + val outcome_code = find_model_loop (first_universe types sizes minsize) in - find_model_loop (first_universe types sizes minsize) + if expect = "" orelse outcome_code = expect then () + else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") end in (* some parameter sanity checks *) @@ -1256,14 +1268,15 @@ maxtime>=0 orelse error ("\"maxtime\" is " ^ string_of_int maxtime ^ ", must be at least 0"); (* enter loop with or without time limit *) - writeln ("Trying to find a model that " + Output.priority ("Trying to find a model that " ^ (if negate then "refutes" else "satisfies") ^ ": " ^ Syntax.string_of_term_global thy t); if maxtime>0 then ( TimeLimit.timeLimit (Time.fromSeconds maxtime) wrapper () handle TimeLimit.TimeOut => - writeln ("\nSearch terminated, time limit (" ^ string_of_int maxtime + Output.priority ("Search terminated, time limit (" ^ + string_of_int maxtime ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.") ) else wrapper ()