src/HOL/Tools/refute.ML
author webertj
Mon Jan 12 14:35:07 2004 +0100 (2004-01-12)
changeset 14351 cd3ef10d02be
parent 14350 41b32020d0b3
child 14456 cca28ec5f9a6
permissions -rw-r--r--
Fixed compatibility issues with SML/NJ:
- replaced '(op *)' by 'op*'
- replaced 'LargeInt' by 'Int'
     1 (*  Title:      HOL/Tools/refute.ML
     2     ID:         $Id$
     3     Author:     Tjark Weber
     4     Copyright   2003-2004
     5 
     6 Finite model generation for HOL formulae, using an external SAT solver.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------- *)
    10 (* Declares the 'REFUTE' signature as well as a structure 'Refute'.  See     *)
    11 (* 'find_model' below for a description of the implemented algorithm, and    *)
    12 (* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to  *)
    13 (* set things up.                                                            *)
    14 (* ------------------------------------------------------------------------- *)
    15 
    16 signature REFUTE =
    17 sig
    18 
    19 	(* We use 'REFUTE' only for internal error conditions that should    *)
    20 	(* never occur in the first place (i.e. errors caused by bugs in our *)
    21 	(* code).  Otherwise (e.g. to indicate invalid input data) we use    *)
    22 	(* 'error'.                                                          *)
    23 
    24 	exception REFUTE of string * string;	(* ("in function", "cause") *)
    25 
    26 	val setup : (theory -> theory) list
    27 
    28 	val set_default_param : (string * string) -> theory -> theory
    29 	val get_default_param : theory -> string -> string option
    30 	val get_default_params : theory -> (string * string) list
    31 
    32 	val find_model : theory -> (string * string) list -> Term.term -> unit
    33 
    34 	val refute_term : theory -> (string * string) list -> Term.term -> unit
    35 	val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
    36 end;
    37 
    38 
    39 structure Refute : REFUTE =
    40 struct
    41 	exception REFUTE of string * string;
    42 
    43 	exception EMPTY_DATATYPE;
    44 
    45 	structure RefuteDataArgs =
    46 	struct
    47 		val name = "Refute/refute";
    48 		type T = string Symtab.table;
    49 		val empty = Symtab.empty;
    50 		val copy = I;
    51 		val prep_ext = I;
    52 		val merge =
    53 			fn (symTable1, symTable2) =>
    54 				(Symtab.merge (op=) (symTable1, symTable2));
    55 		fun print sg symTable =
    56 			writeln
    57 				("'refute', default parameters:\n" ^
    58 				(space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
    59 	end;
    60 
    61 	structure RefuteData = TheoryDataFun(RefuteDataArgs);
    62 
    63 
    64 (* ------------------------------------------------------------------------- *)
    65 (* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT                   *)
    66 (* ------------------------------------------------------------------------- *)
    67 
    68 (* ------------------------------------------------------------------------- *)
    69 (* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
    70 (* structure                                                                 *)
    71 (* ------------------------------------------------------------------------- *)
    72 
    73 	val setup = [RefuteData.init];
    74 
    75 (* ------------------------------------------------------------------------- *)
    76 (* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
    77 (*                    table                                                  *)
    78 (* ------------------------------------------------------------------------- *)
    79 
    80 	fun set_default_param (name, value) thy =
    81 	let
    82 		val symTable = RefuteData.get thy
    83 	in
    84 		case Symtab.lookup (symTable, name) of
    85 			None   => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
    86 		|	Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
    87 	end;
    88 
    89 (* ------------------------------------------------------------------------- *)
    90 (* get_default_param: retrieves the value associated with 'name' from        *)
    91 (*                    RefuteData's symbol table                              *)
    92 (* ------------------------------------------------------------------------- *)
    93 
    94 	fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
    95 
    96 (* ------------------------------------------------------------------------- *)
    97 (* get_default_params: returns a list of all '(name, value)' pairs that are  *)
    98 (*                     stored in RefuteData's symbol table                   *)
    99 (* ------------------------------------------------------------------------- *)
   100 
   101 	fun get_default_params thy = Symtab.dest (RefuteData.get thy);
   102 
   103 
   104 (* ------------------------------------------------------------------------- *)
   105 (* PROPOSITIONAL FORMULAS                                                    *)
   106 (* ------------------------------------------------------------------------- *)
   107 
   108 (* ------------------------------------------------------------------------- *)
   109 (* prop_formula: formulas of propositional logic, built from boolean         *)
   110 (*               variables (referred to by index) and True/False using       *)
   111 (*               not/or/and                                                  *)
   112 (* ------------------------------------------------------------------------- *)
   113 
   114 	datatype prop_formula =
   115 		  True
   116 		| False
   117 		| BoolVar of int
   118 		| Not of prop_formula
   119 		| Or of prop_formula * prop_formula
   120 		| And of prop_formula * prop_formula;
   121 
   122 	(* the following constructor functions make sure that True and False do *)
   123 	(* not occur within any of the other connectives (i.e. Not, Or, And)    *)
   124 
   125 	(* prop_formula -> prop_formula *)
   126 
   127 	fun SNot True  = False
   128 	  | SNot False = True
   129 	  | SNot fm    = Not fm;
   130 
   131 	(* prop_formula * prop_formula -> prop_formula *)
   132 
   133 	fun SOr (True, _)   = True
   134 	  | SOr (_, True)   = True
   135 	  | SOr (False, fm) = fm
   136 	  | SOr (fm, False) = fm
   137 	  | SOr (fm1, fm2)  = Or (fm1, fm2);
   138 
   139 	(* prop_formula * prop_formula -> prop_formula *)
   140 
   141 	fun SAnd (True, fm) = fm
   142 	  | SAnd (fm, True) = fm
   143 	  | SAnd (False, _) = False
   144 	  | SAnd (_, False) = False
   145 	  | SAnd (fm1, fm2) = And (fm1, fm2);
   146 
   147 (* ------------------------------------------------------------------------- *)
   148 (* list_disjunction: computes the disjunction of a list of propositional     *)
   149 (*                   formulas                                                *)
   150 (* ------------------------------------------------------------------------- *)
   151 
   152 	(* prop_formula list -> prop_formula *)
   153 
   154 	fun list_disjunction []      = False
   155 	  | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
   156 
   157 (* ------------------------------------------------------------------------- *)
   158 (* list_conjunction: computes the conjunction of a list of propositional     *)
   159 (*                   formulas                                                *)
   160 (* ------------------------------------------------------------------------- *)
   161 
   162 	(* prop_formula list -> prop_formula *)
   163 
   164 	fun list_conjunction []      = True
   165 	  | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
   166 
   167 (* ------------------------------------------------------------------------- *)
   168 (* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn    *)
   169 (* ------------------------------------------------------------------------- *)
   170 
   171 	(* prop_formula list * prop_formula list -> prop_formula *)
   172 
   173 	fun prop_formula_dot_product ([],[])       = False
   174 	  | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
   175 	  | prop_formula_dot_product (_,_)         = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
   176 
   177 (* ------------------------------------------------------------------------- *)
   178 (* prop_formula_to_nnf: computes the negation normal form of a formula 'fm'  *)
   179 (*                      of propositional logic (i.e. only variables may be   *)
   180 (*                      negated, but not subformulas)                        *)
   181 (* ------------------------------------------------------------------------- *)
   182 
   183 	(* prop_formula -> prop_formula *)
   184 
   185 	fun prop_formula_to_nnf fm =
   186 		case fm of
   187 		(* constants *)
   188 		  True                => True
   189 		| False               => False
   190 		(* literals *)
   191 		| BoolVar i           => BoolVar i
   192 		| Not (BoolVar i)     => Not (BoolVar i)
   193 		(* double-negation elimination *)
   194 		| Not (Not fm)        => prop_formula_to_nnf fm
   195 		(* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
   196 		| Not (Or  (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   197 		| Not (And (fm1,fm2)) => SOr  (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
   198 		(* 'or' and 'and' as outermost connectives are left untouched *)
   199 		| Or  (fm1,fm2)       => SOr  (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   200 		| And (fm1,fm2)       => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
   201 		(* 'not' + constant *)
   202 		| Not _               => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
   203 
   204 (* ------------------------------------------------------------------------- *)
   205 (* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a        *)
   206 (*      formula 'fm' of propositional logic that is given in negation normal *)
   207 (*      form.  Note that there may occur an exponential blowup of the        *)
   208 (*      formula.                                                             *)
   209 (* ------------------------------------------------------------------------- *)
   210 
   211 	(* prop_formula -> prop_formula *)
   212 
   213 	fun prop_formula_nnf_to_cnf fm =
   214 		case fm of
   215 		(* constants *)
   216 		  True            => True
   217 		| False           => False
   218 		(* literals *)
   219 		| BoolVar i       => BoolVar i
   220 		| Not (BoolVar i) => Not (BoolVar i)
   221 		(* pushing 'or' inside of 'and' using distributive laws *)
   222 		| Or (fm1,fm2)    =>
   223 			let
   224 				val fm1' = prop_formula_nnf_to_cnf fm1
   225 				val fm2' = prop_formula_nnf_to_cnf fm2
   226 			in
   227 				case fm1' of
   228 				  And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
   229 				| _               =>
   230 					(case fm2' of
   231 					  And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
   232 					(* neither subformula contains 'and' *)
   233 					| _               => fm)
   234 			end
   235 		(* 'and' as outermost connective is left untouched *)
   236 		| And (fm1,fm2)   => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
   237 		(* error *)
   238 		| _               => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
   239 
   240 (* ------------------------------------------------------------------------- *)
   241 (* max: computes the maximum of two integer values 'i' and 'j'               *)
   242 (* ------------------------------------------------------------------------- *)
   243 
   244 	(* int * int -> int *)
   245 
   246 	fun max (i,j) =
   247 		if (i>j) then i else j;
   248 
   249 (* ------------------------------------------------------------------------- *)
   250 (* max_var_index: computes the maximal variable index occuring in 'fm',      *)
   251 (*      where 'fm' is a formula of propositional logic                       *)
   252 (* ------------------------------------------------------------------------- *)
   253 
   254 	(* prop_formula -> int *)
   255 
   256 	fun max_var_index fm =
   257 		case fm of
   258 		  True          => 0
   259 		| False         => 0
   260 		| BoolVar i     => i
   261 		| Not fm1       => max_var_index fm1
   262 		| And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
   263 		| Or (fm1,fm2)  => max (max_var_index fm1, max_var_index fm2);
   264 
   265 (* ------------------------------------------------------------------------- *)
   266 (* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
   267 (*      form of a formula 'fm' of propositional logic that is given in       *)
   268 (*      negation normal form.  To avoid an exponential blowup of the         *)
   269 (*      formula, auxiliary variables may be introduced.  The result formula  *)
   270 (*      is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if     *)
   271 (*      'fm' is satisfiable).                                                *)
   272 (* ------------------------------------------------------------------------- *)
   273 
   274 	(* prop_formula -> prop_formula *)
   275 
   276 	fun prop_formula_nnf_to_def_cnf fm =
   277 	let
   278 		(* prop_formula * int -> prop_formula * int *)
   279 		fun prop_formula_nnf_to_def_cnf_new (fm,new) =
   280 		(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
   281 			case fm of
   282 			(* constants *)
   283 			  True            => (True, new)
   284 			| False           => (False, new)
   285 			(* literals *)
   286 			| BoolVar i       => (BoolVar i, new)
   287 			| Not (BoolVar i) => (Not (BoolVar i), new)
   288 			(* pushing 'or' inside of 'and' using distributive laws *)
   289 			| Or (fm1,fm2)    =>
   290 				let
   291 					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   292 					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   293 				in
   294 					case fst fm1' of
   295 					  And (fm11,fm12) =>
   296 						let
   297 							val aux = BoolVar (snd fm2')
   298 						in
   299 							(* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
   300 							prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
   301 						end
   302 					| _               =>
   303 						(case fst fm2' of
   304 						  And (fm21,fm22) =>
   305 							let
   306 								val aux = BoolVar (snd fm2')
   307 							in
   308 								(* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
   309 								prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
   310 							end
   311 						(* neither subformula contains 'and' *)
   312 						| _               => (fm, new))
   313 				end
   314 			(* 'and' as outermost connective is left untouched *)
   315 			| And (fm1,fm2)   =>
   316 				let
   317 					val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
   318 					val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
   319 				in
   320 					(SAnd (fst fm1', fst fm2'), snd fm2')
   321 				end
   322 			(* error *)
   323 			| _               => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
   324 	in
   325 		fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
   326 	end;
   327 
   328 (* ------------------------------------------------------------------------- *)
   329 (* prop_formula_to_cnf: computes the conjunctive normal form of a formula    *)
   330 (*                      'fm' of propositional logic                          *)
   331 (* ------------------------------------------------------------------------- *)
   332 
   333 	(* prop_formula -> prop_formula *)
   334 
   335 	fun prop_formula_to_cnf fm =
   336 		prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
   337 
   338 (* ------------------------------------------------------------------------- *)
   339 (* prop_formula_to_def_cnf: computes the definitional conjunctive normal     *)
   340 (*      form of a formula 'fm' of propositional logic, introducing auxiliary *)
   341 (*      variables if necessary to avoid an exponential blowup of the formula *)
   342 (* ------------------------------------------------------------------------- *)
   343 
   344 	(* prop_formula -> prop_formula *)
   345 
   346 	fun prop_formula_to_def_cnf fm =
   347 		prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
   348 
   349 (* ------------------------------------------------------------------------- *)
   350 (* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional  *)
   351 (*      logic to a file in DIMACS CNF format (see "Satisfiability Suggested  *)
   352 (*      Format", May 8 1993, Section 2.1)                                    *)
   353 (* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   354 (*       index less than 1.                                                  *)
   355 (* def : If true, translate 'fm' into definitional CNF.  Otherwise translate *)
   356 (*       'fm' into CNF.                                                      *)
   357 (* path: path of the file to be created                                      *)
   358 (* ------------------------------------------------------------------------- *)
   359 
   360 	(* prop_formula -> bool -> Path.T -> unit *)
   361 
   362 	fun prop_formula_to_dimacs_cnf_format fm def path =
   363 	let
   364 		(* prop_formula *)
   365 		val cnf =
   366 			if def then
   367 				prop_formula_to_def_cnf fm
   368 			else
   369 				prop_formula_to_cnf fm
   370 		val fm' =
   371 			case cnf of
   372 			  True  => Or (BoolVar 1, Not (BoolVar 1))
   373 			| False => And (BoolVar 1, Not (BoolVar 1))
   374 			| _     => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
   375 		(* prop_formula -> int *)
   376 		fun cnf_number_of_clauses (And (fm1,fm2)) =
   377 			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   378 		  | cnf_number_of_clauses _ =
   379 			1
   380 		(* prop_formula -> string *)
   381 		fun cnf_prop_formula_to_string (BoolVar i) =
   382 			if (i<1) then
   383 				raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
   384 			else
   385 				(string_of_int i)
   386 		  | cnf_prop_formula_to_string (Not fm1) =
   387 			"-" ^ (cnf_prop_formula_to_string fm1)
   388 		  | cnf_prop_formula_to_string (Or (fm1,fm2)) =
   389 			(cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
   390 		  | cnf_prop_formula_to_string (And (fm1,fm2)) =
   391 			(cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
   392 		  | cnf_prop_formula_to_string _ =
   393 			raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
   394 	in
   395 		File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
   396 			^ "c (c) Tjark Weber\n"
   397 			^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
   398 			^ (cnf_prop_formula_to_string fm') ^ "\n")
   399 	end;
   400 
   401 (* ------------------------------------------------------------------------- *)
   402 (* prop_formula_to_dimacs_sat_format: serializes a formula of propositional  *)
   403 (*      logic to a file in DIMACS SAT format (see "Satisfiability Suggested  *)
   404 (*      Format", May 8 1993, Section 2.2)                                    *)
   405 (* fm  : formula to be serialized.  Note: 'fm' must not contain a variable   *)
   406 (*       index less than 1.                                                  *)
   407 (* path: path of the file to be created                                      *)
   408 (* ------------------------------------------------------------------------- *)
   409 
   410 	(* prop_formula -> Path.T -> unit *)
   411 
   412 	fun prop_formula_to_dimacs_sat_format fm path =
   413 	let
   414 		fun prop_formula_to_string True =
   415 			"*()"
   416 		  | prop_formula_to_string False =
   417 			"+()"
   418 		  | prop_formula_to_string (BoolVar i) =
   419 			if (i<1) then
   420 				raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
   421 			else
   422 				(string_of_int i)
   423 		  | prop_formula_to_string (Not fm1) =
   424 			"-(" ^ (prop_formula_to_string fm1) ^ ")"
   425 		  | prop_formula_to_string (Or (fm1,fm2)) =
   426 			"+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   427 		  | prop_formula_to_string (And (fm1,fm2)) =
   428 			"*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
   429 	in
   430 		File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
   431 			^ "c (c) Tjark Weber\n"
   432 			^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
   433 			^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
   434 	end;
   435 
   436 (* ------------------------------------------------------------------------- *)
   437 (* prop_formula_sat_solver: try to find a satisfying assignment for the      *)
   438 (*      boolean variables in a propositional formula, using an external SAT  *)
   439 (*      solver.  If the SAT solver did not find an assignment, 'None' is     *)
   440 (*      returned.  Otherwise 'Some (list of integers)' is returned, where    *)
   441 (*      i>0 means that the boolean variable i is set to TRUE, and i<0 means  *)
   442 (*      that the boolean variable i is set to FALSE.  Note that if           *)
   443 (*      'satformat' is 'defcnf', then the assignment returned may contain    *)
   444 (*      auxiliary variables that were not present in the original formula    *)
   445 (*      'fm'.                                                                *)
   446 (* fm        : formula that is passed to the SAT solver                      *) 
   447 (* satpath   : path of the file used to store the propositional formula,     *)
   448 (*             i.e. the input to the SAT solver                              *)
   449 (* satformat : format of the SAT solver's input file.  Must be either "cnf", *)
   450 (*             "defcnf", or "sat".                                           *)
   451 (* resultpath: path of the file containing the SAT solver's output           *)
   452 (* success   : part of the line in the SAT solver's output that is followed  *)
   453 (*             by a line consisting of a list of integers representing the   *)
   454 (*             satisfying assignment                                         *)
   455 (* command   : system command used to execute the SAT solver                 *)
   456 (* ------------------------------------------------------------------------- *)
   457 
   458 	(* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
   459 
   460 	fun prop_formula_sat_solver fm satpath satformat resultpath success command =
   461 		if File.exists satpath then
   462 			error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
   463 		else if File.exists resultpath then
   464 			error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
   465 		else
   466 		(
   467 			(* serialize the formula 'fm' to a file *)
   468 			if satformat="cnf" then
   469 				prop_formula_to_dimacs_cnf_format fm false satpath
   470 			else if satformat="defcnf" then
   471 				prop_formula_to_dimacs_cnf_format fm true satpath
   472 			else if satformat="sat" then
   473 				prop_formula_to_dimacs_sat_format fm satpath
   474 			else
   475 				error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
   476 			(* execute SAT solver *)
   477 			if (system command)<>0 then
   478 			(
   479 				(* error executing SAT solver *)
   480 				File.rm satpath;
   481 				File.rm resultpath;
   482 				error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
   483 			)
   484 			else
   485 			(
   486 				(* read assignment from the result file *)
   487 				File.rm satpath;
   488 				let
   489 					(* 'a option -> 'a Library.option *)
   490 					fun option (SOME a) =
   491 						Some a
   492 					  | option NONE =
   493 						None
   494 					(* string -> int list *)
   495 					fun string_to_int_list s =
   496 						mapfilter (option o Int.fromString) (space_explode " " s)
   497 					(* string -> string -> bool *)
   498 					fun is_substring s1 s2 =
   499 					let
   500 						val length1 = String.size s1
   501 						val length2 = String.size s2
   502 					in
   503 						if length2 < length1 then
   504 							false
   505 						else if s1 = String.substring (s2, 0, length1) then
   506 							true
   507 						else is_substring s1 (String.substring (s2, 1, length2-1))
   508 					end
   509 					(* string list -> int list option *)
   510 					fun extract_solution [] =
   511 						None
   512 					  | extract_solution (line::lines) =
   513 						if is_substring success line then
   514 							(* the next line must be a list of integers *)
   515 							Some (string_to_int_list (hd lines))
   516 						else
   517 							extract_solution lines
   518 					val sat_result = File.read resultpath
   519 				in
   520 					File.rm resultpath;
   521 					extract_solution (split_lines sat_result)
   522 				end
   523 			)
   524 		);
   525 
   526 
   527 (* ------------------------------------------------------------------------- *)
   528 (* TREES                                                                     *)
   529 (* ------------------------------------------------------------------------- *)
   530 
   531 (* ------------------------------------------------------------------------- *)
   532 (* tree: implements an arbitrarily (but finitely) branching tree as a list   *)
   533 (*       of (lists of ...) elements                                          *)
   534 (* ------------------------------------------------------------------------- *)
   535 
   536 	datatype 'a tree =
   537 		  Leaf of 'a
   538 		| Node of ('a tree) list;
   539 
   540 	type prop_tree =
   541 		prop_formula list tree;
   542 
   543 	(* ('a -> 'b) -> 'a tree -> 'b tree *)
   544 
   545 	fun tree_map f tr =
   546 		case tr of
   547 		  Leaf x  => Leaf (f x)
   548 		| Node xs => Node (map (tree_map f) xs);
   549 
   550 	(* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
   551 
   552 	fun tree_foldl f =
   553 	let
   554 		fun itl (e, Leaf x)  = f(e,x)
   555 		  | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
   556 	in
   557 		itl
   558 	end;
   559 
   560 	(* 'a tree * 'b tree -> ('a * 'b) tree *)
   561 
   562 	fun tree_pair (t1,t2) =
   563 		case t1 of
   564 		  Leaf x =>
   565 			(case t2 of
   566 				  Leaf y => Leaf (x,y)
   567 				| Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
   568 		| Node xs =>
   569 			(case t2 of
   570 				  (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
   571 				  Node ys => Node (map tree_pair (xs ~~ ys))
   572 				| Leaf _  => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
   573 
   574 (* ------------------------------------------------------------------------- *)
   575 (* prop_tree_to_true: returns a propositional formula that is true iff the   *)
   576 (*      tree denotes the boolean value TRUE                                  *)
   577 (* ------------------------------------------------------------------------- *)
   578 
   579 	(* prop_tree -> prop_formula *)
   580 
   581 	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   582 	(* the term is true iff the leaf's first element is true           *)
   583 
   584 	fun prop_tree_to_true (Leaf [fm,_]) =
   585 		fm
   586 	  | prop_tree_to_true _ =
   587 		raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
   588 
   589 (* ------------------------------------------------------------------------- *)
   590 (* prop_tree_to_false: returns a propositional formula that is true iff the  *)
   591 (*      tree denotes the boolean value FALSE                                 *)
   592 (* ------------------------------------------------------------------------- *)
   593 
   594 	(* prop_tree -> prop_formula *)
   595 
   596 	(* a term of type 'bool' is represented as a 2-element leaf, where *)
   597 	(* the term is false iff the leaf's second element is true         *)
   598 
   599 	fun prop_tree_to_false (Leaf [_,fm]) =
   600 		fm
   601 	  | prop_tree_to_false _ =
   602 		raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
   603 
   604 (* ------------------------------------------------------------------------- *)
   605 (* restrict_to_single_element: returns a propositional formula which is true *)
   606 (*      iff the tree 'tr' describes a single element of its corresponding    *)
   607 (*      type, i.e. iff at each leaf, one and only one formula is true        *)
   608 (* ------------------------------------------------------------------------- *)
   609 
   610 	(* prop_tree -> prop_formula *)
   611 
   612 	fun restrict_to_single_element tr =
   613 	let
   614 		(* prop_formula list -> prop_formula *)
   615 		fun allfalse []      = True
   616 		  | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
   617 		(* prop_formula list -> prop_formula *)
   618 		fun exactly1true []      = False
   619 		  | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
   620 	in
   621 		case tr of
   622 		  Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
   623 		| Leaf xs                           => exactly1true xs
   624 		| Node trees                        => list_conjunction (map restrict_to_single_element trees)
   625 	end;
   626 
   627 (* ------------------------------------------------------------------------- *)
   628 (* HOL FORMULAS                                                              *)
   629 (* ------------------------------------------------------------------------- *)
   630 
   631 (* ------------------------------------------------------------------------- *)
   632 (* absvar: form an abstraction over a schematic variable                     *)
   633 (* ------------------------------------------------------------------------- *)
   634 
   635 	(* Term.indexname * Term.typ * Term.term -> Term.term *)
   636 
   637 	(* this function is similar to Term.absfree, but for schematic       *)
   638 	(* variables (rather than free variables)                            *)
   639 	fun absvar ((x,i),T,body) =
   640 		Abs(x, T, abstract_over (Var((x,i),T), body));
   641 
   642 (* ------------------------------------------------------------------------- *)
   643 (* list_all_var: quantification over a list of schematic variables           *)
   644 (* ------------------------------------------------------------------------- *)
   645 
   646 	(* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
   647 
   648 	(* this function is similar to Term.list_all_free, but for schematic *)
   649 	(* variables (rather than free variables)                            *)
   650 	fun list_all_var ([], t) =
   651 		t
   652 	  | list_all_var ((idx,T)::vars, t) =
   653 		(all T) $ (absvar(idx, T, list_all_var(vars,t)));
   654 
   655 (* ------------------------------------------------------------------------- *)
   656 (* close_vars: close up a formula over all schematic variables by            *)
   657 (*             quantification (note that the result term may still contain   *)
   658 (*             (non-schematic) free variables)                               *)
   659 (* ------------------------------------------------------------------------- *)
   660 
   661 	(* Term.term -> Term.term *)
   662 
   663 	(* this function is similar to Logic.close_form, but for schematic   *)
   664 	(* variables (rather than free variables)                            *)
   665 	fun close_vars A =
   666 		list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
   667 
   668 (* ------------------------------------------------------------------------- *)
   669 (* make_universes: given a list 'xs' of "types" and a universe size 'size',  *)
   670 (*      this function returns all possible partitions of the universe into   *)
   671 (*      the "types" in 'xs' such that no "type" is empty.  If 'size' is less *)
   672 (*      than 'length xs', the returned list of partitions is empty.          *)
   673 (*      Otherwise, if the list 'xs' is empty, then the returned list of      *)
   674 (*      partitions contains only the empty list, regardless of 'size'.       *)
   675 (* ------------------------------------------------------------------------- *)
   676 
   677 	(* 'a list -> int -> ('a * int) list list *)
   678 
   679 	fun make_universes xs size =
   680 	let
   681 		(* 'a list -> int -> int -> ('a * int) list list *)
   682 		fun make_partitions_loop (x::xs) 0 total =
   683 			map (fn us => ((x,0)::us)) (make_partitions xs total)
   684 		  | make_partitions_loop (x::xs) first total =
   685 			(map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
   686 		  | make_partitions_loop _ _ _ =
   687 			raise REFUTE ("make_universes::make_partitions_loop", "empty list")
   688 		and
   689 		(* 'a list -> int -> ('a * int) list list *)
   690 		make_partitions [x] size =
   691 			(* we must use all remaining elements on the type 'x', so there is only one partition *)
   692 			[[(x,size)]]
   693 		  | make_partitions (x::xs) 0 =
   694 			(* there are no elements left in the universe, so there is only one partition *)
   695 			[map (fn t => (t,0)) (x::xs)]
   696 		  | make_partitions (x::xs) size =
   697 			(* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
   698 			make_partitions_loop (x::xs) size size
   699 		  | make_partitions _ _ =
   700 			raise REFUTE ("make_universes::make_partitions", "empty list")
   701 		val len = length xs
   702 	in
   703 		if size<len then
   704 			(* the universe isn't big enough to make every type non-empty *)
   705 			[]
   706 		else if xs=[] then
   707 			(* no types: return one universe, regardless of the size *)
   708 			[[]]
   709 		else
   710 			(* partition into possibly empty types, then add 1 element to each type *)
   711 			map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
   712 	end;
   713 
   714 (* ------------------------------------------------------------------------- *)
   715 (* sum: computes the sum of a list of integers; sum [] = 0                   *)
   716 (* ------------------------------------------------------------------------- *)
   717 
   718 	(* int list -> int *)
   719 
   720 	fun sum xs = foldl op+ (0, xs);
   721 
   722 (* ------------------------------------------------------------------------- *)
   723 (* product: computes the product of a list of integers; product [] = 1       *)
   724 (* ------------------------------------------------------------------------- *)
   725 
   726 	(* int list -> int *)
   727 
   728 	fun product xs = foldl op* (1, xs);
   729 
   730 (* ------------------------------------------------------------------------- *)
   731 (* power: power(a,b) computes a^b, for a>=0, b>=0                            *)
   732 (* ------------------------------------------------------------------------- *)
   733 
   734 	(* int * int -> int *)
   735 
   736 	fun power (a,0) = 1
   737 	  | power (a,1) = a
   738 	  | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
   739 
   740 (* ------------------------------------------------------------------------- *)
   741 (* size_of_type: returns the size of a type, where 'us' specifies the size   *)
   742 (*      of each basic type (i.e. each type variable), and 'cdepth' specifies *)
   743 (*      the maximal constructor depth for inductive datatypes                *)
   744 (* ------------------------------------------------------------------------- *)
   745 
   746 	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
   747 
   748 	fun size_of_type T us thy cdepth =
   749 	let
   750 		(* Term.typ -> (Term.typ * int) -> int *)
   751 		fun lookup_size T [] =
   752 			raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
   753 		  | lookup_size T ((typ,size)::pairs) =
   754 			if T=typ then size else lookup_size T pairs
   755 	in
   756 		case T of
   757 		  Type ("prop", [])     => 2
   758 		| Type ("bool", [])     => 2
   759 		| Type ("Product_Type.unit", []) => 1
   760 		| Type ("+", [T1,T2])   => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
   761 		| Type ("*", [T1,T2])   => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
   762 		| Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
   763 		| Type ("set", [T1])    => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   764 		| Type (s, Ts)          =>
   765 			(case DatatypePackage.datatype_info thy s of
   766 			  Some info => (* inductive datatype *)
   767 				if cdepth>0 then
   768 					let
   769 						val index               = #index info
   770 						val descr               = #descr info
   771 						val (_, dtyps, constrs) = the (assoc (descr, index))
   772 						val Typs                = dtyps ~~ Ts
   773 						(* DatatypeAux.dtyp -> Term.typ *)
   774 						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
   775 							the (assoc (Typs, DatatypeAux.DtTFree a))
   776 						  | typ_of_dtyp (DatatypeAux.DtRec i) =
   777 							let
   778 								val (s, ds, _) = the (assoc (descr, i))
   779 							in
   780 								Type (s, map typ_of_dtyp ds)
   781 							end
   782 						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
   783 							Type (s, map typ_of_dtyp ds)
   784 					in
   785 						sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
   786 					end
   787 				else 0
   788 			| None      => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
   789 		| TFree _               => lookup_size T us
   790 		| TVar _                => lookup_size T us
   791 	end;
   792 
   793 (* ------------------------------------------------------------------------- *)
   794 (* type_to_prop_tree: creates a tree of boolean variables that denotes an    *)
   795 (*      element of the type 'T'.  The height and branching factor of the     *)
   796 (*      tree depend on the size and "structure" of 'T'.                      *)
   797 (* 'us' : a "universe" specifying the number of elements for each basic type *)
   798 (*        (i.e. each type variable) in 'T'                                   *)
   799 (* 'cdepth': maximum constructor depth to be used for inductive datatypes    *)
   800 (* 'idx': the next index to be used for a boolean variable                   *)
   801 (* ------------------------------------------------------------------------- *)
   802 
   803 	(* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
   804 
   805 	fun type_to_prop_tree T us thy cdepth idx =
   806 	let
   807 		(* int -> Term.typ -> int -> prop_tree list * int *)
   808 		fun type_to_prop_tree_list 1 T' idx' =
   809 			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   810 				([tr], newidx)
   811 			end
   812 		  | type_to_prop_tree_list n T' idx' =
   813 			let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
   814 				let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
   815 					(tr::trees, lastidx)
   816 				end
   817 			end
   818 	in
   819 		case T of
   820 		  Type ("prop", []) =>
   821 			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   822 		| Type ("bool", []) =>
   823 			(Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
   824 		| Type ("Product_Type.unit", []) =>
   825 			(Leaf [True], idx)
   826 		| Type ("+", [T1,T2]) =>
   827 			let
   828 				val s1 = size_of_type T1 us thy cdepth
   829 				val s2 = size_of_type T2 us thy cdepth
   830 				val s  = s1 + s2
   831 			in
   832 				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   833 					raise EMPTY_DATATYPE
   834 				else
   835 					error "sum types (+) not implemented yet (TODO)"
   836 			end
   837 		| Type ("*", [T1,T2]) =>
   838 			let
   839 				val s1 = size_of_type T1 us thy cdepth
   840 				val s2 = size_of_type T2 us thy cdepth
   841 				val s  = s1 * s2
   842 			in
   843 				if s1=0 orelse s2=0 then
   844 					raise EMPTY_DATATYPE
   845 				else
   846 					error "product types (*) not implemented yet (TODO)"
   847 			end
   848 		| Type ("fun", [T1,T2]) =>
   849 			(* we create 'size_of_type T1' different copies of the tree for 'T2', *)
   850 			(* which are then combined into a single new tree                     *)
   851 			let
   852 				val s = size_of_type T1 us thy cdepth
   853 			in
   854 				if s=0 then
   855 					raise EMPTY_DATATYPE
   856 				else
   857 					let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
   858 						(Node trees, newidx)
   859 					end
   860 			end
   861 		| Type ("set", [T1]) =>
   862 			type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
   863 		| Type (s, _) =>
   864 			(case DatatypePackage.constrs_of thy s of
   865 			   Some _ => (* inductive datatype *)
   866 					let
   867 						val s = size_of_type T us thy cdepth
   868 					in
   869 						if s=0 then
   870 							raise EMPTY_DATATYPE
   871 						else
   872 							(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   873 					end
   874 			 | None   => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
   875 		| TFree _ =>
   876 			let val s = size_of_type T us thy cdepth in
   877 				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   878 			end
   879 		| TVar _  =>
   880 			let val s = size_of_type T us thy cdepth in
   881 				(Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
   882 			end
   883 	end;
   884 
   885 (* ------------------------------------------------------------------------- *)
   886 (* type_to_constants: creates a list of prop_trees with constants (True,     *)
   887 (*      False) rather than boolean variables, one for every element in the   *)
   888 (*      type 'T'; c.f. type_to_prop_tree                                     *)
   889 (* ------------------------------------------------------------------------- *)
   890 
   891 	(* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
   892 
   893 	fun type_to_constants T us thy cdepth =
   894 	let
   895 		(* returns a list with all unit vectors of length n *)
   896 		(* int -> prop_tree list *)
   897 		fun unit_vectors n =
   898 		let
   899 			(* returns the k-th unit vector of length n *)
   900 			(* int * int -> prop_tree *)
   901 			fun unit_vector (k,n) =
   902 				Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
   903 			(* int -> prop_tree list -> prop_tree list *)
   904 			fun unit_vectors_acc k vs =
   905 				if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
   906 		in
   907 			unit_vectors_acc 1 []
   908 		end
   909 		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
   910 		(* 'a -> 'a list list -> 'a list list *)
   911 		fun cons_list x xss =
   912 			map (fn xs => x::xs) xss
   913 		(* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
   914 		(* int -> 'a list -> 'a list list *)
   915 		fun pick_all 1 xs =
   916 			map (fn x => [x]) xs
   917 		  | pick_all n xs =
   918 			let val rec_pick = pick_all (n-1) xs in
   919 				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
   920 			end
   921 	in
   922 		case T of
   923 		  Type ("prop", [])     => unit_vectors 2
   924 		| Type ("bool", [])     => unit_vectors 2
   925 		| Type ("Product_Type.unit", []) => unit_vectors 1
   926                 | Type ("+", [T1,T2])   =>
   927 			let
   928 				val s1 = size_of_type T1 us thy cdepth
   929 				val s2 = size_of_type T2 us thy cdepth
   930 			in
   931 				if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
   932 					raise EMPTY_DATATYPE
   933 				else
   934 					error "sum types (+) not implemented yet (TODO)"
   935 			end
   936                 | Type ("*", [T1,T2])   =>
   937 			let
   938 				val s1 = size_of_type T1 us thy cdepth
   939 				val s2 = size_of_type T2 us thy cdepth
   940 			in
   941 				if s1=0 orelse s2=0 then
   942 					raise EMPTY_DATATYPE
   943 				else
   944 					error "product types (*) not implemented yet (TODO)"
   945 			end
   946 		| Type ("fun", [T1,T2]) =>
   947 			let
   948 				val s = size_of_type T1 us thy cdepth
   949 			in
   950 				if s=0 then
   951 					raise EMPTY_DATATYPE
   952 				else
   953 					map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
   954 			end
   955 		| Type ("set", [T1])    => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
   956 		| Type (s, _)           =>
   957 			(case DatatypePackage.constrs_of thy s of
   958 			   Some _ => (* inductive datatype *)
   959 					let
   960 						val s = size_of_type T us thy cdepth
   961 					in
   962 						if s=0 then
   963 							raise EMPTY_DATATYPE
   964 						else
   965 							unit_vectors s
   966 					end
   967 			 | None   => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
   968 		| TFree _               => unit_vectors (size_of_type T us thy cdepth)
   969 		| TVar _                => unit_vectors (size_of_type T us thy cdepth)
   970 	end;
   971 
   972 (* ------------------------------------------------------------------------- *)
   973 (* prop_tree_equal: returns a propositional formula that is true iff 'tr1'   *)
   974 (*      and 'tr2' both denote the same element                               *)
   975 (* ------------------------------------------------------------------------- *)
   976 
   977 	(* prop_tree * prop_tree -> prop_formula *)
   978 
   979 	fun prop_tree_equal (tr1,tr2) =
   980 		case tr1 of
   981 		  Leaf x =>
   982 			(case tr2 of
   983 			  Leaf y => prop_formula_dot_product (x,y)
   984 			| _      => raise REFUTE ("prop_tree_equal", "second tree is higher"))
   985 		| Node xs =>
   986 			(case tr2 of
   987 			  Leaf _  => raise REFUTE ("prop_tree_equal", "first tree is higher")
   988 			(* extensionality: two functions are equal iff they are equal for every element *)
   989 			| Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
   990 
   991 (* ------------------------------------------------------------------------- *)
   992 (* prop_tree_apply: returns a tree that denotes the element obtained by      *)
   993 (*      applying the function which is denoted by the tree 't1' to the       *)
   994 (*      element which is denoted by the tree 't2'                            *)
   995 (* ------------------------------------------------------------------------- *)
   996 
   997 	(* prop_tree * prop_tree -> prop_tree *)
   998 
   999 	fun prop_tree_apply (tr1,tr2) =
  1000 	let
  1001 		(* prop_tree * prop_tree -> prop_tree *)
  1002 		fun prop_tree_disjunction (tr1,tr2) =
  1003 			tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
  1004 		(* prop_formula * prop_tree -> prop_tree *)
  1005 		fun prop_formula_times_prop_tree (fm,tr) =
  1006 			tree_map (map (fn x => SAnd (fm,x))) tr
  1007 		(* prop_formula list * prop_tree list -> prop_tree *)
  1008 		fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
  1009 			prop_formula_times_prop_tree (fm,tr)
  1010 		  | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
  1011 			prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
  1012 		  | prop_formula_list_dot_product_prop_tree_list (_,_) =
  1013 			raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
  1014 		(* concatenates 'x' with every list in 'xss', returning a new list of lists *)
  1015 		(* 'a -> 'a list list -> 'a list list *)
  1016 		fun cons_list x xss =
  1017 			map (fn xs => x::xs) xss
  1018 		(* returns a list of lists, each one consisting of one element from each element of 'xss' *)
  1019 		(* 'a list list -> 'a list list *)
  1020 		fun pick_all [xs] =
  1021 			map (fn x => [x]) xs
  1022 		  | pick_all (xs::xss) =
  1023 			let val rec_pick = pick_all xss in
  1024 				foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
  1025 			end
  1026 		  | pick_all _ =
  1027 			raise REFUTE ("prop_tree_apply::pick_all", "empty list")
  1028 		(* prop_tree -> prop_formula list *)
  1029 		fun prop_tree_to_prop_formula_list (Leaf xs) =
  1030 			xs
  1031 		  | prop_tree_to_prop_formula_list (Node trees) =
  1032 			map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
  1033 	in
  1034 		case tr1 of
  1035 		  Leaf _ =>
  1036 			raise REFUTE ("prop_tree_apply", "first tree is a leaf")
  1037 		| Node xs =>
  1038 			prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
  1039 	end
  1040 
  1041 (* ------------------------------------------------------------------------- *)
  1042 (* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
  1043 (*      formulas; 'us' specifies the number of elements for each type        *)
  1044 (*      variable in 't'; 'cdepth' specifies the maximal constructor depth    *)
  1045 (*      for inductive datatypes.  Also returns the lowest index that was not *)
  1046 (*      used for a boolean variable, and a substitution of terms (free/      *)
  1047 (*      schematic variables) by prop_trees.                                  *)
  1048 (* ------------------------------------------------------------------------- *)
  1049 
  1050 	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1051 
  1052 	fun term_to_prop_tree t us thy cdepth =
  1053 	let
  1054 		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1055 		fun variable_to_prop_tree_subst t' (idx,subs) =
  1056 			case assoc (subs,t') of
  1057 			  Some tr =>
  1058 				(* return the previously associated tree; the substitution remains unchanged *)
  1059 				(tr, (idx,subs))
  1060 			| None =>
  1061 				(* generate a new tree; update the index; extend the substitution *)
  1062 				let
  1063 					val T = case t' of
  1064 						  Free (_,T) => T
  1065 						| Var (_,T)  => T
  1066 						| _          => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
  1067 					val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
  1068 				in
  1069 					(tr, (newidx, (t',tr)::subs))
  1070 				end
  1071 		(* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
  1072 		fun term_to_prop_tree_subst t' (idx,subs) bsubs =
  1073 			case t' of
  1074 			(* meta-logical constants *)
  1075 			  Const ("Goal", _) $ t1 =>
  1076 				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1077 			| Const ("all", _) $ t1 =>
  1078 				let
  1079 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1080 				in
  1081 					case tree1 of
  1082 					  Node xs =>
  1083 						let
  1084 							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1085 							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1086 						in
  1087 							(Leaf [fmTrue, fmFalse], (i1,s1))
  1088 						end
  1089 					| _ =>
  1090 						raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
  1091 				end
  1092 			| Const ("==", _) $ t1 $ t2 =>
  1093 				let
  1094 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1095 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1096 					val fmTrue          = prop_tree_equal (tree1,tree2)
  1097 					val fmFalse         = SNot fmTrue
  1098 				in
  1099 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1100 				end
  1101 			| Const ("==>", _) $ t1 $ t2 =>
  1102 				let
  1103 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1104 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1105 					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1106 					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1107 				in
  1108 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1109 				end
  1110 			(* HOL constants *)
  1111 			| Const ("Trueprop", _) $ t1 =>
  1112 				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1113 			| Const ("Not", _) $ t1 =>
  1114 				let
  1115 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1116 					val fmTrue          = prop_tree_to_false tree1
  1117 					val fmFalse         = prop_tree_to_true tree1
  1118 				in
  1119 					(Leaf [fmTrue, fmFalse], (i1,s1))
  1120 				end
  1121 			| Const ("True", _) =>
  1122 				(Leaf [True, False], (idx,subs))
  1123 			| Const ("False", _) =>
  1124 				(Leaf [False, True], (idx,subs))
  1125 			| Const ("All", _) $ t1 =>
  1126 				let
  1127 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1128 				in
  1129 					case tree1 of
  1130 					  Node xs =>
  1131 						let
  1132 							val fmTrue  = list_conjunction (map prop_tree_to_true xs)
  1133 							val fmFalse = list_disjunction (map prop_tree_to_false xs)
  1134 						in
  1135 							(Leaf [fmTrue, fmFalse], (i1,s1))
  1136 						end
  1137 					| _ =>
  1138 						raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
  1139 				end
  1140 			| Const ("Ex", _) $ t1 =>
  1141 				let
  1142 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1143 				in
  1144 					case tree1 of
  1145 					  Node xs =>
  1146 						let
  1147 							val fmTrue  = list_disjunction (map prop_tree_to_true xs)
  1148 							val fmFalse = list_conjunction (map prop_tree_to_false xs)
  1149 						in
  1150 							(Leaf [fmTrue, fmFalse], (i1,s1))
  1151 						end
  1152 					| _ =>
  1153 						raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
  1154 				end
  1155 			| Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
  1156 				(* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
  1157 				let
  1158 					val t1'      = Term.incr_bv (1, 0, t1)
  1159 					val t1''     = Term.incr_bv (2, 0, t1)
  1160 					val t_equal  = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
  1161 					val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
  1162 					val t_ex1    = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
  1163 				in
  1164 					term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
  1165 				end
  1166 			| Const ("op =", _) $ t1 $ t2 =>
  1167 				let
  1168 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1169 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1170 					val fmTrue          = prop_tree_equal (tree1,tree2)
  1171 					val fmFalse         = SNot fmTrue
  1172 				in
  1173 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1174 				end
  1175 			| Const ("op &", _) $ t1 $ t2 =>
  1176 				let
  1177 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1178 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1179 					val fmTrue          = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1180 					val fmFalse         = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1181 				in
  1182 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1183 				end
  1184 			| Const ("op |", _) $ t1 $ t2 =>
  1185 				let
  1186 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1187 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1188 					val fmTrue          = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
  1189 					val fmFalse         = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
  1190 				in
  1191 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1192 				end
  1193 			| Const ("op -->", _) $ t1 $ t2 =>
  1194 				let
  1195 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1196 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1197 					val fmTrue          = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
  1198 					val fmFalse         = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
  1199 				in
  1200 					(Leaf [fmTrue, fmFalse], (i2,s2))
  1201 				end
  1202 			(* set constants *)
  1203 			| Const ("Collect", _) $ t1 =>
  1204 				term_to_prop_tree_subst t1 (idx,subs) bsubs
  1205 			| Const ("op :", _) $ t1 $ t2 =>
  1206 				term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
  1207 			(* datatype constants *)
  1208 			| Const ("Product_Type.Unity", _) =>
  1209 				(Leaf [True], (idx,subs))
  1210 			(* unknown constants *)
  1211 			| Const (c, _) =>
  1212 				error ("term contains an unknown constant: '" ^ c ^ "'")
  1213 			(* abstractions *)
  1214 			| Abs (_,T,body) =>
  1215 				let
  1216 					val constants       = type_to_constants T us thy cdepth
  1217 					val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
  1218 				in
  1219 					(* the substitutions in 'substs' are all identical *)
  1220 					(Node trees, hd substs)
  1221 				end
  1222 			(* (free/schematic) variables *)
  1223 			| Free _ =>
  1224 				variable_to_prop_tree_subst t' (idx,subs)
  1225 			| Var _ =>
  1226 				variable_to_prop_tree_subst t' (idx,subs)
  1227 			(* bound variables *)
  1228 			| Bound i =>
  1229 				if (length bsubs) <= i then
  1230 					raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
  1231 				else
  1232 					(nth_elem (i,bsubs), (idx,subs))
  1233 			(* application *)
  1234 			| t1 $ t2 =>
  1235 				let
  1236 					val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
  1237 					val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
  1238 				in
  1239 					(prop_tree_apply (tree1,tree2), (i2,s2))
  1240 				end
  1241 	in
  1242 		term_to_prop_tree_subst t (1,[]) []
  1243 	end;
  1244 
  1245 (* ------------------------------------------------------------------------- *)
  1246 (* term_to_prop_formula: translates a HOL formula 't' into a propositional   *)
  1247 (*      formula that is satisfiable if and only if 't' has a model of "size" *)
  1248 (*      'us' (where 'us' specifies the number of elements for each free type *)
  1249 (*      variable in 't') and maximal constructor depth 'cdepth'.             *)
  1250 (* ------------------------------------------------------------------------- *)
  1251 
  1252 	(* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
  1253 
  1254 	(* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
  1255 
  1256 	fun term_to_prop_formula t us thy cdepth =
  1257 	let
  1258 		val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
  1259 		val fm               = prop_tree_to_true tr
  1260 	in
  1261 		if subs=[] then
  1262 			(fm, (idx,subs))
  1263 		else
  1264 			(* make sure every tree that is substituted for a term describes a single element *)
  1265 			(SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
  1266 	end;
  1267 
  1268 
  1269 (* ------------------------------------------------------------------------- *)
  1270 (* INTERFACE, PART 2: FINDING A MODEL                                        *)
  1271 (* ------------------------------------------------------------------------- *)
  1272 
  1273 (* ------------------------------------------------------------------------- *)
  1274 (* string_of_universe: prints a universe, i.e. an assignment of sizes for    *)
  1275 (*                     types                                                 *)
  1276 (* thy: the current theory                                                   *)
  1277 (* us : a list containing types together with their size                     *)
  1278 (* ------------------------------------------------------------------------- *)
  1279 
  1280 	(* theory -> (Term.typ * int) list -> string *)
  1281 
  1282 	fun string_of_universe thy [] =
  1283 		"empty universe (no type variables in term)"
  1284 	  | string_of_universe thy us =
  1285 		space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
  1286 
  1287 (* ------------------------------------------------------------------------- *)
  1288 (* string_of_model: prints a model, given by a substitution 'subs' of trees  *)
  1289 (*      of propositional variables and an assignment 'ass' of truth values   *)
  1290 (*      for these variables.                                                 *)
  1291 (* thy   : the current theory                                                *)
  1292 (* us    : universe, specifies the "size" of each type (i.e. type variable)  *)
  1293 (* cdepth: maximal constructor depth for inductive datatypes                 *)
  1294 (* subs  : substitution of trees of propositional formulas (for variables)   *)
  1295 (* ass   : assignment of truth values for boolean variables; see function    *)
  1296 (*         'truth_value' below for its meaning                               *)
  1297 (* ------------------------------------------------------------------------- *)
  1298 
  1299 	(* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
  1300 
  1301 	fun string_of_model thy us cdepth [] ass =
  1302 		"empty interpretation (no free variables in term)"
  1303 	  | string_of_model thy us cdepth subs ass =
  1304 		let
  1305 			(* Sign.sg *)
  1306 			val sg = sign_of thy
  1307 			(* int -> bool *)
  1308 			fun truth_value i =
  1309 				if i mem ass then true
  1310 				else if ~i mem ass then false
  1311 				else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
  1312 			(* string -> string *)
  1313 			fun strip_leading_quote str =
  1314 				if nth_elem_string(0,str)="'" then
  1315 					String.substring (str, 1, size str - 1)
  1316 				else
  1317 					str;
  1318 			(* prop_formula list -> int *)
  1319 			fun true_index xs =
  1320 				(* returns the (0-based) index of the first true formula in xs *)
  1321 				let fun true_index_acc [] _ =
  1322 					raise REFUTE ("string_of_model::true_index", "no variable was set to true")
  1323 				      | true_index_acc (x::xs) n =
  1324 					case x of
  1325 					  BoolVar i =>
  1326 						if truth_value i then n else true_index_acc xs (n+1)
  1327 					| True =>
  1328 						n
  1329 					| False =>
  1330 						true_index_acc xs (n+1)
  1331 					| _ =>
  1332 						raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
  1333 				in
  1334 					true_index_acc xs 0
  1335 				end
  1336 			(* Term.typ -> int -> prop_tree -> string *)
  1337 			(* prop *)
  1338 			fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1339 				if truth_value i then "true" else "false"
  1340 			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
  1341 				"true"
  1342 			  | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
  1343 				"false"
  1344 			(* bool *)
  1345 			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
  1346 				if truth_value i then "true" else "false"
  1347 			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
  1348 				"true"
  1349 			  | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
  1350 				"false"
  1351 			(* unit *)
  1352 			  | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
  1353 				"()"
  1354 			  | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
  1355 				(case DatatypePackage.datatype_info thy s of
  1356 				   Some info => (* inductive datatype *)
  1357 					let
  1358 						val index               = #index info
  1359 						val descr               = #descr info
  1360 						val (_, dtyps, constrs) = the (assoc (descr, index))
  1361 						val Typs                = dtyps ~~ Ts
  1362 						(* string -> string *)
  1363 						fun unqualify s =
  1364 							implode (snd (take_suffix (fn c => c <> ".") (explode s)))
  1365 						(* DatatypeAux.dtyp -> Term.typ *)
  1366 						fun typ_of_dtyp (DatatypeAux.DtTFree a) =
  1367 							the (assoc (Typs, DatatypeAux.DtTFree a))
  1368 						  | typ_of_dtyp (DatatypeAux.DtRec i) =
  1369 							let
  1370 								val (s, ds, _) = the (assoc (descr, i))
  1371 							in
  1372 								Type (s, map typ_of_dtyp ds)
  1373 							end
  1374 						  | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
  1375 							Type (s, map typ_of_dtyp ds)
  1376 						(* DatatypeAux.dtyp list -> int -> string *)
  1377 						fun string_of_inductive_type_cargs [] n =
  1378 							if n<>0 then
  1379 								raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
  1380 							else
  1381 								""
  1382 						  | string_of_inductive_type_cargs (d::ds) n =
  1383 							let
  1384 								val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1385 							in
  1386 								" " ^ (string_of_prop_tree (typ_of_dtyp d) (cdepth-1) (nth_elem (n div size_ds, type_to_constants (typ_of_dtyp d) us thy (cdepth-1)))) ^ (string_of_inductive_type_cargs ds (n mod size_ds))
  1387 							end
  1388 						(* (string * DatatypeAux.dtyp list) list -> int -> string *)
  1389 						fun string_of_inductive_type_constrs [] n =
  1390 							raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
  1391 						  | string_of_inductive_type_constrs ((s,ds)::cs) n =
  1392 							let
  1393 								val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
  1394 							in
  1395 								if n < size then
  1396 									(unqualify s) ^ (string_of_inductive_type_cargs ds n)
  1397 								else
  1398 									string_of_inductive_type_constrs cs (n - size)
  1399 							end
  1400 					in
  1401 						string_of_inductive_type_constrs constrs (true_index xs)
  1402 					end
  1403 				 | None =>
  1404 					raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
  1405 			(* type variable *)
  1406 			  | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
  1407 					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1408 			  | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
  1409 					(strip_leading_quote s) ^ (string_of_int (true_index xs))
  1410 			(* function or set type *)
  1411 			  | string_of_prop_tree T cdepth (Node xs) =
  1412 				case T of
  1413 				  Type ("fun", [T1,T2]) =>
  1414 					let
  1415 						val strings = foldl (fn (ss,(c,x)) => ss @ [(string_of_prop_tree T1 cdepth c) ^ "\\<mapsto>" ^ (string_of_prop_tree T2 cdepth x)]) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
  1416 					in
  1417 						"(" ^ (space_implode ", " strings) ^ ")"
  1418 					end
  1419 				| Type ("set", [T1]) =>
  1420 					let
  1421 						val strings = foldl (fn (ss,(c,x)) => if (string_of_prop_tree (Type ("bool",[])) cdepth x)="true" then ss @ [string_of_prop_tree T1 cdepth c] else ss) ([], (type_to_constants T1 us thy cdepth) ~~ xs)
  1422 					in
  1423 						"{" ^ (space_implode ", " strings) ^ "}"
  1424 					end
  1425 				| _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
  1426 			(* Term.term * prop_formula tree -> string *)
  1427 			fun string_of_term_assignment (t,tr) =
  1428 			let
  1429 				val T = case t of
  1430 					  Free (_,T) => T
  1431 					| Var (_,T)  => T
  1432 					| _          => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
  1433 			in
  1434 				(Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
  1435 			end
  1436 		in
  1437 			space_implode "\n" (map string_of_term_assignment subs)
  1438 		end;
  1439 
  1440 (* ------------------------------------------------------------------------- *)
  1441 (* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate   *)
  1442 (*             parameters, and displays the results to the user              *)
  1443 (* params    : list of '(name, value)' pairs used to override default        *)
  1444 (*             parameters                                                    *)
  1445 (*                                                                           *)
  1446 (* This is a brief description of the algorithm implemented:                 *)
  1447 (*                                                                           *)
  1448 (* 1. Let k = max ('minsize',1).                                             *)
  1449 (* 2. Let the universe have k elements.  Find all possible partitions of     *)
  1450 (*    these elements into the basic types occuring in 't' such that no basic *)
  1451 (*    type is empty.                                                         *)
  1452 (* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
  1453 (*    the partition chosen in step (2.) if (actually, if and only if) p is   *)
  1454 (*    satisfiable.  To do this, replace quantification by conjunction/       *)
  1455 (*    disjunction over all elements of the type being quantified over.  (If  *)
  1456 (*    p contains more than 'maxvars' boolean variables, terminate.)          *)
  1457 (* 4. Serialize p to a file, and try to find a satisfying assignment for p   *)
  1458 (*    by invoking an external SAT solver.                                    *)
  1459 (* 5. If the SAT solver finds a satisfying assignment for p, translate this  *)
  1460 (*    assignment back into a model for 't'.  Present this model to the user, *)
  1461 (*    then terminate.                                                        *)
  1462 (* 6. As long as there is another partition left, pick it and go back to     *)
  1463 (*    step (3.).                                                             *)
  1464 (* 7. Increase k by 1.  As long as k does not exceed 'maxsize', go back to   *)
  1465 (*    step (2.).                                                             *)
  1466 (*                                                                           *)
  1467 (* The following parameters are currently supported (and required!):         *)
  1468 (*                                                                           *)
  1469 (* Name          Type    Description                                         *)
  1470 (*                                                                           *)
  1471 (* "minsize"     int     Only search for models with size at least           *)
  1472 (*                       'minsize'.                                          *)
  1473 (* "maxsize"     int     If >0, only search for models with size at most     *)
  1474 (*                       'maxsize'.                                          *)
  1475 (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
  1476 (*                       when transforming the term into a propositional     *)
  1477 (*                       formula.                                            *)
  1478 (* "satfile"     string  Name of the file used to store the propositional    *)
  1479 (*                       formula, i.e. the input to the SAT solver.          *)
  1480 (* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
  1481 (*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
  1482 (*                       not supported by most SAT solvers, and "cnf" can    *)
  1483 (*                       cause exponential blowup of the formula, "defcnf"   *)
  1484 (*                       is recommended.                                     *)
  1485 (* "resultfile"  string  Name of the file containing the SAT solver's        *)
  1486 (*                       output.                                             *)
  1487 (* "success"     string  Part of the line in the SAT solver's output that    *)
  1488 (*                       precedes a list of integers representing the        *)
  1489 (*                       satisfying assignment.                              *)
  1490 (* "command"     string  System command used to execute the SAT solver.      *)
  1491 (*                       Note that you if you change 'satfile' or            *)
  1492 (*                       'resultfile', you will also need to change          *)
  1493 (*                       'command'.                                          *)
  1494 (*                                                                           *)
  1495 (* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values.  *)
  1496 (* ------------------------------------------------------------------------- *)
  1497 
  1498 	(* theory -> (string * string) list -> Term.term -> unit *)
  1499 
  1500 	fun find_model thy params t =
  1501 	let
  1502 		(* (string * string) list * (string * string) list -> (string * string) list *)
  1503 		fun add_params (parms, []) =
  1504 			parms
  1505 		  | add_params (parms, defparm::defparms) =
  1506 			add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
  1507 		(* (string * string) list * string -> int *)
  1508 		fun read_int (parms, name) =
  1509 			case assoc_string (parms, name) of
  1510 			  Some s => (case Int.fromString s of
  1511 				  SOME i => i
  1512 				| NONE   => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
  1513 			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1514 		(* (string * string) list * string -> string *)
  1515 		fun read_string (parms, name) =
  1516 			case assoc_string (parms, name) of
  1517 			  Some s => s
  1518 			| None   => error ("parameter '" ^ name ^ "' must be assigned a value")
  1519 		(* (string * string) list *)
  1520 		val allparams  = add_params (params, get_default_params thy)
  1521 		(* int *)
  1522 		val minsize    = read_int (allparams, "minsize")
  1523 		val maxsize    = read_int (allparams, "maxsize")
  1524 		val maxvars    = read_int (allparams, "maxvars")
  1525 		(* string *)
  1526 		val satfile    = read_string (allparams, "satfile")
  1527 		val satformat  = read_string (allparams, "satformat")
  1528 		val resultfile = read_string (allparams, "resultfile")
  1529 		val success    = read_string (allparams, "success")
  1530 		val command    = read_string (allparams, "command")
  1531 		(* misc *)
  1532 		val satpath    = Path.unpack satfile
  1533 		val resultpath = Path.unpack resultfile
  1534 		val sg         = sign_of thy
  1535 		(* Term.typ list *)
  1536 		val tvars      = map (fn (i,s) => TVar(i,s)) (term_tvars t)
  1537 		val tfrees     = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
  1538 		(* universe -> int -> bool *)
  1539 		fun find_model_universe u cdepth =
  1540 			let
  1541 				(* given the universe 'u' and constructor depth 'cdepth', translate *)
  1542         	                (* the term 't' into a propositional formula 'fm'                   *)
  1543 				val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
  1544 				val usedvars        = idx-1
  1545 			in
  1546 				(* 'maxvars=0' means "use as many variables as necessary" *)
  1547 				if usedvars>maxvars andalso maxvars<>0 then
  1548 					(
  1549 						(* too many variables used: terminate *)
  1550 						writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
  1551 						true
  1552 					)
  1553 				else
  1554 					(* pass the formula 'fm' to an external SAT solver *)
  1555 					case prop_formula_sat_solver fm satpath satformat resultpath success command of
  1556 					  None =>
  1557 						(* no model found *)
  1558 						false
  1559 					| Some assignment =>
  1560 						(* model found: terminate *)
  1561 						(
  1562 							writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
  1563 							true
  1564 						)
  1565 			end
  1566 		(* universe list -> int -> bool *)
  1567 		fun find_model_universes [] cdepth =
  1568 			(
  1569 				std_output "\n";
  1570 				false
  1571 			)
  1572 		  | find_model_universes (u::us) cdepth =
  1573 			(
  1574 				std_output ".";
  1575 				((if find_model_universe u cdepth then
  1576 					(* terminate *)
  1577 					true
  1578 				else
  1579 					(* continue search with the next universe *)
  1580 					find_model_universes us cdepth)
  1581 				handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
  1582 			)
  1583 		(* int * int -> unit *)
  1584 		fun find_model_from_to (min,max) =
  1585 			(* 'max=0' means "search for arbitrary large models" *)
  1586 			if min>max andalso max<>0 then
  1587 				writeln ("Search terminated: no model found.")
  1588 			else
  1589 			(
  1590 				std_output ("Searching for a model of size " ^ (string_of_int min));
  1591 				if find_model_universes (make_universes tfrees min) min then
  1592 					(* terminate *)
  1593 					()
  1594 				else
  1595 					(* continue search with increased size *)
  1596 					find_model_from_to (min+1, max)
  1597 			)
  1598 	in
  1599 		writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
  1600 		if tvars<>[] then
  1601 			(* TODO: deal with schematic type variables in a better way, if possible *)
  1602 			error "term contains schematic type variables"
  1603 		else
  1604 		(
  1605 			if minsize<1 then
  1606 				writeln ("'minsize' is less than 1; starting search with size 1.")
  1607 			else
  1608 				();
  1609 			if maxsize<max (minsize,1) andalso maxsize<>0 then
  1610 				writeln ("'maxsize' is less than 'minsize': no model found.")
  1611 			else
  1612 				find_model_from_to (max (minsize,1), maxsize)
  1613 		)
  1614 	end;
  1615 
  1616 (* ------------------------------------------------------------------------- *)
  1617 (* refute_term: calls 'find_model' on the negation of a term                 *)
  1618 (* params     : list of '(name, value)' pairs used to override default       *)
  1619 (*              parameters                                                   *)
  1620 (* ------------------------------------------------------------------------- *)
  1621 
  1622 	(* theory -> (string * string) list -> Term.term -> unit *)
  1623 
  1624 	fun refute_term thy params t =
  1625 	let
  1626 		(* TODO: schematic type variables? *)
  1627 		val negation = close_vars (HOLogic.Not $ t)
  1628 		(* If 't' is of type 'propT' (rather than 'boolT'), applying *)
  1629 		(* 'HOLogic.Not' is not type-correct.  However, this isn't   *)
  1630 		(* really a problem as long as 'find_model' still interprets *)
  1631 		(* the resulting term correctly, without checking its type.  *)
  1632 	in
  1633 		find_model thy params negation
  1634 	end;
  1635 
  1636 (* ------------------------------------------------------------------------- *)
  1637 (* refute_subgoal: calls 'refute_term' on a specific subgoal                 *)
  1638 (* params        : list of '(name, value)' pairs used to override default    *)
  1639 (*                 parameters                                                *)
  1640 (* subgoal       : 0-based index specifying the subgoal number               *)
  1641 (* ------------------------------------------------------------------------- *)
  1642 
  1643 	(* theory -> (string * string) list -> Thm.thm -> int -> unit *)
  1644 
  1645 	fun refute_subgoal thy params thm subgoal =
  1646 		refute_term thy params (nth_elem (subgoal, prems_of thm));
  1647 
  1648 end