src/HOL/Tools/refute.ML

 (* ------------------------------------------------------------------------- *)
 (* params: parameters that control the translation into a propositional      *)
 (*         formula/model generation                                          *)
 (*                                                                           *)
 (* The following parameters are supported (and required (!), except for      *)
-(* "sizes"):                                                                 *)
+(* "sizes" and "expect"):                                                    *)
 (*                                                                           *)
 (* Name          Type    Description                                         *)
 (*                                                                           *)
 (* "sizes"       (string * int) list                                         *)
 (*                       Size of ground types (e.g. 'a=2), or depth of IDTs. *)

 (* "maxvars"     int     If >0, use at most 'maxvars' Boolean variables      *)
 (*                       when transforming the term into a propositional     *)
 (*                       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 =
     {
       sizes    : (string * int) list,
       minsize  : int,
       maxsize  : int,
       maxvars  : int,
       maxtime  : int,
-      satsolver: string
+      satsolver: string,
+      expect   : string
     };
 
 (* ------------------------------------------------------------------------- *)
 (* interpretation: a term's interpretation is given by a variable of type    *)
 (*                 'interpretation'                                          *)

     val maxsize   = read_int (allparams, "maxsize")
     val maxvars   = read_int (allparams, "maxvars")
     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    *)
     (*       whose name is one of the other parameters (e.g. 'maxvars')   *)
     (* (string * int) list *)

       (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
         andalso name<>"maxvars" andalso name<>"maxtime"
         andalso name<>"satsolver") allparams)
   in
     {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
-      maxtime=maxtime, satsolver=satsolver}
+      maxtime=maxtime, satsolver=satsolver, expect=expect}
   end;
 
 
 (* ------------------------------------------------------------------------- *)
 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)

           (* 'rhs', we must not use this equation to unfold, because *)
           (* that would loop.  Here would be the right place to      *)
           (* 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
       | Var _            => t
       | Bound _          => t

   (* To avoid collecting the same axiom multiple times, we use an           *)
   (* accumulator 'axs' which contains all axioms collected so far.          *)
 
   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 *)
     fun collect_this_axiom (axname, ax) axs =
     let
       val ax' = unfold_defs thy ax
     in
       if member (op aconv) axs ax' then
         axs
       else (
-        Output.immediate_output (" " ^ axname);
+        Output.tracing axname;
         collect_term_axioms (ax' :: axs, ax')
       )
     end
     (* Term.term list * Term.typ -> Term.term list *)
     and collect_sort_axioms (axs, T) =

         (collect_type_axioms (axs, T), body)
       | t1 $ t2          => collect_term_axioms
         (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;
 
 (* ------------------------------------------------------------------------- *)

 (* negate    : if true, find a model that makes 't' false (rather than true) *)
 (* ------------------------------------------------------------------------- *)
 
   (* 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 *)
             let
               val index           = #index info

               (* recursive datatype? *)
               Library.exists (fn (_, ds) =>
                 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') =>
           let
             val (i, m', a') = interpret thy m a t'

         (* add the well-formedness side condition                       *)
         val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
         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 *)
       minsize>=1 orelse
         error ("\"minsize\" is " ^ string_of_int minsize ^ ", must be at least 1");

       maxvars>=0 orelse
         error ("\"maxvars\" is " ^ string_of_int maxvars ^ ", must be at least 0");
       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 ()
     end;