1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/refute.ML Sat Jan 10 13:35:10 2004 +0100
1.3 @@ -0,0 +1,1648 @@
1.4 +(* Title: HOL/Tools/refute.ML
1.5 + ID: $Id$
1.6 + Author: Tjark Weber
1.7 + Copyright 2003-2004
1.8 +
1.9 +Finite model generation for HOL formulae, using an external SAT solver.
1.10 +*)
1.11 +
1.12 +(* ------------------------------------------------------------------------- *)
1.13 +(* Declares the 'REFUTE' signature as well as a structure 'Refute'. See *)
1.14 +(* 'find_model' below for a description of the implemented algorithm, and *)
1.15 +(* the Isabelle/Isar theories 'HOL/Refute.thy' and 'HOL/Main.thy' on how to *)
1.16 +(* set things up. *)
1.17 +(* ------------------------------------------------------------------------- *)
1.18 +
1.19 +signature REFUTE =
1.20 +sig
1.21 +
1.22 + (* We use 'REFUTE' only for internal error conditions that should *)
1.23 + (* never occur in the first place (i.e. errors caused by bugs in our *)
1.24 + (* code). Otherwise (e.g. to indicate invalid input data) we use *)
1.25 + (* 'error'. *)
1.26 +
1.27 + exception REFUTE of string * string; (* ("in function", "cause") *)
1.28 +
1.29 + val setup : (theory -> theory) list
1.30 +
1.31 + val set_default_param : (string * string) -> theory -> theory
1.32 + val get_default_param : theory -> string -> string option
1.33 + val get_default_params : theory -> (string * string) list
1.34 +
1.35 + val find_model : theory -> (string * string) list -> Term.term -> unit
1.36 +
1.37 + val refute_term : theory -> (string * string) list -> Term.term -> unit
1.38 + val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
1.39 +end;
1.40 +
1.41 +
1.42 +structure Refute : REFUTE =
1.43 +struct
1.44 + exception REFUTE of string * string;
1.45 +
1.46 + exception EMPTY_DATATYPE;
1.47 +
1.48 + structure RefuteDataArgs =
1.49 + struct
1.50 + val name = "Refute/refute";
1.51 + type T = string Symtab.table;
1.52 + val empty = Symtab.empty;
1.53 + val copy = I;
1.54 + val prep_ext = I;
1.55 + val merge =
1.56 + fn (symTable1, symTable2) =>
1.57 + (Symtab.merge (op =) (symTable1, symTable2));
1.58 + fun print sg symTable =
1.59 + writeln
1.60 + ("'refute', default parameters:\n" ^
1.61 + (space_implode "\n" (map (fn (name,value) => name ^ " = " ^ value) (Symtab.dest symTable))))
1.62 + end;
1.63 +
1.64 + structure RefuteData = TheoryDataFun(RefuteDataArgs);
1.65 +
1.66 +
1.67 +(* ------------------------------------------------------------------------- *)
1.68 +(* INTERFACE, PART 1: INITIALIZATION, PARAMETER MANAGEMENT *)
1.69 +(* ------------------------------------------------------------------------- *)
1.70 +
1.71 +(* ------------------------------------------------------------------------- *)
1.72 +(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
1.73 +(* structure *)
1.74 +(* ------------------------------------------------------------------------- *)
1.75 +
1.76 + val setup = [RefuteData.init];
1.77 +
1.78 +(* ------------------------------------------------------------------------- *)
1.79 +(* set_default_param: stores the '(name, value)' pair in RefuteData's symbol *)
1.80 +(* table *)
1.81 +(* ------------------------------------------------------------------------- *)
1.82 +
1.83 + fun set_default_param (name, value) thy =
1.84 + let
1.85 + val symTable = RefuteData.get thy
1.86 + in
1.87 + case Symtab.lookup (symTable, name) of
1.88 + None => RefuteData.put (Symtab.extend (symTable, [(name, value)])) thy
1.89 + | Some _ => RefuteData.put (Symtab.update ((name, value), symTable)) thy
1.90 + end;
1.91 +
1.92 +(* ------------------------------------------------------------------------- *)
1.93 +(* get_default_param: retrieves the value associated with 'name' from *)
1.94 +(* RefuteData's symbol table *)
1.95 +(* ------------------------------------------------------------------------- *)
1.96 +
1.97 + fun get_default_param thy name = Symtab.lookup (RefuteData.get thy, name);
1.98 +
1.99 +(* ------------------------------------------------------------------------- *)
1.100 +(* get_default_params: returns a list of all '(name, value)' pairs that are *)
1.101 +(* stored in RefuteData's symbol table *)
1.102 +(* ------------------------------------------------------------------------- *)
1.103 +
1.104 + fun get_default_params thy = Symtab.dest (RefuteData.get thy);
1.105 +
1.106 +
1.107 +(* ------------------------------------------------------------------------- *)
1.108 +(* PROPOSITIONAL FORMULAS *)
1.109 +(* ------------------------------------------------------------------------- *)
1.110 +
1.111 +(* ------------------------------------------------------------------------- *)
1.112 +(* prop_formula: formulas of propositional logic, built from boolean *)
1.113 +(* variables (referred to by index) and True/False using *)
1.114 +(* not/or/and *)
1.115 +(* ------------------------------------------------------------------------- *)
1.116 +
1.117 + datatype prop_formula =
1.118 + True
1.119 + | False
1.120 + | BoolVar of int
1.121 + | Not of prop_formula
1.122 + | Or of prop_formula * prop_formula
1.123 + | And of prop_formula * prop_formula;
1.124 +
1.125 + (* the following constructor functions make sure that True and False do *)
1.126 + (* not occur within any of the other connectives (i.e. Not, Or, And) *)
1.127 +
1.128 + (* prop_formula -> prop_formula *)
1.129 +
1.130 + fun SNot True = False
1.131 + | SNot False = True
1.132 + | SNot fm = Not fm;
1.133 +
1.134 + (* prop_formula * prop_formula -> prop_formula *)
1.135 +
1.136 + fun SOr (True, _) = True
1.137 + | SOr (_, True) = True
1.138 + | SOr (False, fm) = fm
1.139 + | SOr (fm, False) = fm
1.140 + | SOr (fm1, fm2) = Or (fm1, fm2);
1.141 +
1.142 + (* prop_formula * prop_formula -> prop_formula *)
1.143 +
1.144 + fun SAnd (True, fm) = fm
1.145 + | SAnd (fm, True) = fm
1.146 + | SAnd (False, _) = False
1.147 + | SAnd (_, False) = False
1.148 + | SAnd (fm1, fm2) = And (fm1, fm2);
1.149 +
1.150 +(* ------------------------------------------------------------------------- *)
1.151 +(* list_disjunction: computes the disjunction of a list of propositional *)
1.152 +(* formulas *)
1.153 +(* ------------------------------------------------------------------------- *)
1.154 +
1.155 + (* prop_formula list -> prop_formula *)
1.156 +
1.157 + fun list_disjunction [] = False
1.158 + | list_disjunction (x::xs) = SOr (x, list_disjunction xs);
1.159 +
1.160 +(* ------------------------------------------------------------------------- *)
1.161 +(* list_conjunction: computes the conjunction of a list of propositional *)
1.162 +(* formulas *)
1.163 +(* ------------------------------------------------------------------------- *)
1.164 +
1.165 + (* prop_formula list -> prop_formula *)
1.166 +
1.167 + fun list_conjunction [] = True
1.168 + | list_conjunction (x::xs) = SAnd (x, list_conjunction xs);
1.169 +
1.170 +(* ------------------------------------------------------------------------- *)
1.171 +(* prop_formula_dot_product: [x1,...,xn] * [y1,...,yn] -> x1*y1+...+xn*yn *)
1.172 +(* ------------------------------------------------------------------------- *)
1.173 +
1.174 + (* prop_formula list * prop_formula list -> prop_formula *)
1.175 +
1.176 + fun prop_formula_dot_product ([],[]) = False
1.177 + | prop_formula_dot_product (x::xs,y::ys) = SOr (SAnd (x,y), prop_formula_dot_product (xs,ys))
1.178 + | prop_formula_dot_product (_,_) = raise REFUTE ("prop_formula_dot_product", "lists are of different length");
1.179 +
1.180 +(* ------------------------------------------------------------------------- *)
1.181 +(* prop_formula_to_nnf: computes the negation normal form of a formula 'fm' *)
1.182 +(* of propositional logic (i.e. only variables may be *)
1.183 +(* negated, but not subformulas) *)
1.184 +(* ------------------------------------------------------------------------- *)
1.185 +
1.186 + (* prop_formula -> prop_formula *)
1.187 +
1.188 + fun prop_formula_to_nnf fm =
1.189 + case fm of
1.190 + (* constants *)
1.191 + True => True
1.192 + | False => False
1.193 + (* literals *)
1.194 + | BoolVar i => BoolVar i
1.195 + | Not (BoolVar i) => Not (BoolVar i)
1.196 + (* double-negation elimination *)
1.197 + | Not (Not fm) => prop_formula_to_nnf fm
1.198 + (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
1.199 + | Not (Or (fm1,fm2)) => SAnd (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
1.200 + | Not (And (fm1,fm2)) => SOr (prop_formula_to_nnf (SNot fm1),prop_formula_to_nnf (SNot fm2))
1.201 + (* 'or' and 'and' as outermost connectives are left untouched *)
1.202 + | Or (fm1,fm2) => SOr (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
1.203 + | And (fm1,fm2) => SAnd (prop_formula_to_nnf fm1,prop_formula_to_nnf fm2)
1.204 + (* 'not' + constant *)
1.205 + | Not _ => raise REFUTE ("prop_formula_to_nnf", "'True'/'False' not allowed inside of 'Not'");
1.206 +
1.207 +(* ------------------------------------------------------------------------- *)
1.208 +(* prop_formula_nnf_to_cnf: computes the conjunctive normal form of a *)
1.209 +(* formula 'fm' of propositional logic that is given in negation normal *)
1.210 +(* form. Note that there may occur an exponential blowup of the *)
1.211 +(* formula. *)
1.212 +(* ------------------------------------------------------------------------- *)
1.213 +
1.214 + (* prop_formula -> prop_formula *)
1.215 +
1.216 + fun prop_formula_nnf_to_cnf fm =
1.217 + case fm of
1.218 + (* constants *)
1.219 + True => True
1.220 + | False => False
1.221 + (* literals *)
1.222 + | BoolVar i => BoolVar i
1.223 + | Not (BoolVar i) => Not (BoolVar i)
1.224 + (* pushing 'or' inside of 'and' using distributive laws *)
1.225 + | Or (fm1,fm2) =>
1.226 + let
1.227 + val fm1' = prop_formula_nnf_to_cnf fm1
1.228 + val fm2' = prop_formula_nnf_to_cnf fm2
1.229 + in
1.230 + case fm1' of
1.231 + And (fm11,fm12) => prop_formula_nnf_to_cnf (SAnd (SOr(fm11,fm2'),SOr(fm12,fm2')))
1.232 + | _ =>
1.233 + (case fm2' of
1.234 + And (fm21,fm22) => prop_formula_nnf_to_cnf (SAnd (SOr(fm1',fm21),SOr(fm1',fm22)))
1.235 + (* neither subformula contains 'and' *)
1.236 + | _ => fm)
1.237 + end
1.238 + (* 'and' as outermost connective is left untouched *)
1.239 + | And (fm1,fm2) => SAnd (prop_formula_nnf_to_cnf fm1, prop_formula_nnf_to_cnf fm2)
1.240 + (* error *)
1.241 + | _ => raise REFUTE ("prop_formula_nnf_to_cnf", "formula is not in negation normal form");
1.242 +
1.243 +(* ------------------------------------------------------------------------- *)
1.244 +(* max: computes the maximum of two integer values 'i' and 'j' *)
1.245 +(* ------------------------------------------------------------------------- *)
1.246 +
1.247 + (* int * int -> int *)
1.248 +
1.249 + fun max (i,j) =
1.250 + if (i>j) then i else j;
1.251 +
1.252 +(* ------------------------------------------------------------------------- *)
1.253 +(* max_var_index: computes the maximal variable index occuring in 'fm', *)
1.254 +(* where 'fm' is a formula of propositional logic *)
1.255 +(* ------------------------------------------------------------------------- *)
1.256 +
1.257 + (* prop_formula -> int *)
1.258 +
1.259 + fun max_var_index fm =
1.260 + case fm of
1.261 + True => 0
1.262 + | False => 0
1.263 + | BoolVar i => i
1.264 + | Not fm1 => max_var_index fm1
1.265 + | And (fm1,fm2) => max (max_var_index fm1, max_var_index fm2)
1.266 + | Or (fm1,fm2) => max (max_var_index fm1, max_var_index fm2);
1.267 +
1.268 +(* ------------------------------------------------------------------------- *)
1.269 +(* prop_formula_nnf_to_def_cnf: computes the definitional conjunctive normal *)
1.270 +(* form of a formula 'fm' of propositional logic that is given in *)
1.271 +(* negation normal form. To avoid an exponential blowup of the *)
1.272 +(* formula, auxiliary variables may be introduced. The result formula *)
1.273 +(* is SAT-equivalent to 'fm' (i.e. it is satisfiable if and only if *)
1.274 +(* 'fm' is satisfiable). *)
1.275 +(* ------------------------------------------------------------------------- *)
1.276 +
1.277 + (* prop_formula -> prop_formula *)
1.278 +
1.279 + fun prop_formula_nnf_to_def_cnf fm =
1.280 + let
1.281 + (* prop_formula * int -> prop_formula * int *)
1.282 + fun prop_formula_nnf_to_def_cnf_new (fm,new) =
1.283 + (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
1.284 + case fm of
1.285 + (* constants *)
1.286 + True => (True, new)
1.287 + | False => (False, new)
1.288 + (* literals *)
1.289 + | BoolVar i => (BoolVar i, new)
1.290 + | Not (BoolVar i) => (Not (BoolVar i), new)
1.291 + (* pushing 'or' inside of 'and' using distributive laws *)
1.292 + | Or (fm1,fm2) =>
1.293 + let
1.294 + val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
1.295 + val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
1.296 + in
1.297 + case fst fm1' of
1.298 + And (fm11,fm12) =>
1.299 + let
1.300 + val aux = BoolVar (snd fm2')
1.301 + in
1.302 + (* '(fm11 AND fm12) OR fm2' is SAT-equivalent to '(fm11 OR aux) AND (fm12 OR aux) AND (fm2 OR NOT aux)' *)
1.303 + prop_formula_nnf_to_def_cnf_new (SAnd (SAnd (SOr (fm11,aux), SOr (fm12,aux)), SOr(fst fm2', Not aux)), (snd fm2')+1)
1.304 + end
1.305 + | _ =>
1.306 + (case fst fm2' of
1.307 + And (fm21,fm22) =>
1.308 + let
1.309 + val aux = BoolVar (snd fm2')
1.310 + in
1.311 + (* 'fm1 OR (fm21 AND fm22)' is SAT-equivalent to '(fm1 OR NOT aux) AND (fm21 OR aux) AND (fm22 OR NOT aux)' *)
1.312 + prop_formula_nnf_to_def_cnf_new (SAnd (SOr (fst fm1', Not aux), SAnd (SOr (fm21,aux), SOr (fm22,aux))), (snd fm2')+1)
1.313 + end
1.314 + (* neither subformula contains 'and' *)
1.315 + | _ => (fm, new))
1.316 + end
1.317 + (* 'and' as outermost connective is left untouched *)
1.318 + | And (fm1,fm2) =>
1.319 + let
1.320 + val fm1' = prop_formula_nnf_to_def_cnf_new (fm1, new)
1.321 + val fm2' = prop_formula_nnf_to_def_cnf_new (fm2, snd fm1')
1.322 + in
1.323 + (SAnd (fst fm1', fst fm2'), snd fm2')
1.324 + end
1.325 + (* error *)
1.326 + | _ => raise REFUTE ("prop_formula_nnf_to_def_cnf", "formula is not in negation normal form")
1.327 + in
1.328 + fst (prop_formula_nnf_to_def_cnf_new (fm, (max_var_index fm)+1))
1.329 + end;
1.330 +
1.331 +(* ------------------------------------------------------------------------- *)
1.332 +(* prop_formula_to_cnf: computes the conjunctive normal form of a formula *)
1.333 +(* 'fm' of propositional logic *)
1.334 +(* ------------------------------------------------------------------------- *)
1.335 +
1.336 + (* prop_formula -> prop_formula *)
1.337 +
1.338 + fun prop_formula_to_cnf fm =
1.339 + prop_formula_nnf_to_cnf (prop_formula_to_nnf fm);
1.340 +
1.341 +(* ------------------------------------------------------------------------- *)
1.342 +(* prop_formula_to_def_cnf: computes the definitional conjunctive normal *)
1.343 +(* form of a formula 'fm' of propositional logic, introducing auxiliary *)
1.344 +(* variables if necessary to avoid an exponential blowup of the formula *)
1.345 +(* ------------------------------------------------------------------------- *)
1.346 +
1.347 + (* prop_formula -> prop_formula *)
1.348 +
1.349 + fun prop_formula_to_def_cnf fm =
1.350 + prop_formula_nnf_to_def_cnf (prop_formula_to_nnf fm);
1.351 +
1.352 +(* ------------------------------------------------------------------------- *)
1.353 +(* prop_formula_to_dimacs_cnf_format: serializes a formula of propositional *)
1.354 +(* logic to a file in DIMACS CNF format (see "Satisfiability Suggested *)
1.355 +(* Format", May 8 1993, Section 2.1) *)
1.356 +(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
1.357 +(* index less than 1. *)
1.358 +(* def : If true, translate 'fm' into definitional CNF. Otherwise translate *)
1.359 +(* 'fm' into CNF. *)
1.360 +(* path: path of the file to be created *)
1.361 +(* ------------------------------------------------------------------------- *)
1.362 +
1.363 + (* prop_formula -> bool -> Path.T -> unit *)
1.364 +
1.365 + fun prop_formula_to_dimacs_cnf_format fm def path =
1.366 + let
1.367 + (* prop_formula *)
1.368 + val cnf =
1.369 + if def then
1.370 + prop_formula_to_def_cnf fm
1.371 + else
1.372 + prop_formula_to_cnf fm
1.373 + val fm' =
1.374 + case cnf of
1.375 + True => Or (BoolVar 1, Not (BoolVar 1))
1.376 + | False => And (BoolVar 1, Not (BoolVar 1))
1.377 + | _ => cnf (* either 'cnf'=True/False, or 'cnf' does not contain True/False at all *)
1.378 + (* prop_formula -> int *)
1.379 + fun cnf_number_of_clauses (And (fm1,fm2)) =
1.380 + (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
1.381 + | cnf_number_of_clauses _ =
1.382 + 1
1.383 + (* prop_formula -> string *)
1.384 + fun cnf_prop_formula_to_string (BoolVar i) =
1.385 + if (i<1) then
1.386 + raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains a variable index less than 1")
1.387 + else
1.388 + (string_of_int i)
1.389 + | cnf_prop_formula_to_string (Not fm1) =
1.390 + "-" ^ (cnf_prop_formula_to_string fm1)
1.391 + | cnf_prop_formula_to_string (Or (fm1,fm2)) =
1.392 + (cnf_prop_formula_to_string fm1) ^ " " ^ (cnf_prop_formula_to_string fm2)
1.393 + | cnf_prop_formula_to_string (And (fm1,fm2)) =
1.394 + (cnf_prop_formula_to_string fm1) ^ " 0\n" ^ (cnf_prop_formula_to_string fm2)
1.395 + | cnf_prop_formula_to_string _ =
1.396 + raise REFUTE ("prop_formula_to_dimacs_cnf_format", "formula contains True/False")
1.397 + in
1.398 + File.write path ("c This file was generated by prop_formula_to_dimacs_cnf_format\n"
1.399 + ^ "c (c) Tjark Weber\n"
1.400 + ^ "p cnf " ^ (string_of_int (max_var_index fm')) ^ " " ^ (string_of_int (cnf_number_of_clauses fm')) ^ "\n"
1.401 + ^ (cnf_prop_formula_to_string fm') ^ "\n")
1.402 + end;
1.403 +
1.404 +(* ------------------------------------------------------------------------- *)
1.405 +(* prop_formula_to_dimacs_sat_format: serializes a formula of propositional *)
1.406 +(* logic to a file in DIMACS SAT format (see "Satisfiability Suggested *)
1.407 +(* Format", May 8 1993, Section 2.2) *)
1.408 +(* fm : formula to be serialized. Note: 'fm' must not contain a variable *)
1.409 +(* index less than 1. *)
1.410 +(* path: path of the file to be created *)
1.411 +(* ------------------------------------------------------------------------- *)
1.412 +
1.413 + (* prop_formula -> Path.T -> unit *)
1.414 +
1.415 + fun prop_formula_to_dimacs_sat_format fm path =
1.416 + let
1.417 + fun prop_formula_to_string True =
1.418 + "*()"
1.419 + | prop_formula_to_string False =
1.420 + "+()"
1.421 + | prop_formula_to_string (BoolVar i) =
1.422 + if (i<1) then
1.423 + raise REFUTE ("prop_formula_to_dimacs_sat_format", "formula contains a variable index less than 1")
1.424 + else
1.425 + (string_of_int i)
1.426 + | prop_formula_to_string (Not fm1) =
1.427 + "-(" ^ (prop_formula_to_string fm1) ^ ")"
1.428 + | prop_formula_to_string (Or (fm1,fm2)) =
1.429 + "+(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
1.430 + | prop_formula_to_string (And (fm1,fm2)) =
1.431 + "*(" ^ (prop_formula_to_string fm1) ^ " " ^ (prop_formula_to_string fm2) ^ ")"
1.432 + in
1.433 + File.write path ("c This file was generated by prop_formula_to_dimacs_sat_format\n"
1.434 + ^ "c (c) Tjark Weber\n"
1.435 + ^ "p sat " ^ (string_of_int (max (max_var_index fm, 1))) ^ "\n"
1.436 + ^ "(" ^ (prop_formula_to_string fm) ^ ")\n")
1.437 + end;
1.438 +
1.439 +(* ------------------------------------------------------------------------- *)
1.440 +(* prop_formula_sat_solver: try to find a satisfying assignment for the *)
1.441 +(* boolean variables in a propositional formula, using an external SAT *)
1.442 +(* solver. If the SAT solver did not find an assignment, 'None' is *)
1.443 +(* returned. Otherwise 'Some (list of integers)' is returned, where *)
1.444 +(* i>0 means that the boolean variable i is set to TRUE, and i<0 means *)
1.445 +(* that the boolean variable i is set to FALSE. Note that if *)
1.446 +(* 'satformat' is 'defcnf', then the assignment returned may contain *)
1.447 +(* auxiliary variables that were not present in the original formula *)
1.448 +(* 'fm'. *)
1.449 +(* fm : formula that is passed to the SAT solver *)
1.450 +(* satpath : path of the file used to store the propositional formula, *)
1.451 +(* i.e. the input to the SAT solver *)
1.452 +(* satformat : format of the SAT solver's input file. Must be either "cnf", *)
1.453 +(* "defcnf", or "sat". *)
1.454 +(* resultpath: path of the file containing the SAT solver's output *)
1.455 +(* success : part of the line in the SAT solver's output that is followed *)
1.456 +(* by a line consisting of a list of integers representing the *)
1.457 +(* satisfying assignment *)
1.458 +(* command : system command used to execute the SAT solver *)
1.459 +(* ------------------------------------------------------------------------- *)
1.460 +
1.461 + (* prop_formula -> Path.T -> string -> Path.T -> string -> string -> int list option *)
1.462 +
1.463 + fun prop_formula_sat_solver fm satpath satformat resultpath success command =
1.464 + if File.exists satpath then
1.465 + error ("file '" ^ (Path.pack satpath) ^ "' exists, please delete (will not overwrite)")
1.466 + else if File.exists resultpath then
1.467 + error ("file '" ^ (Path.pack resultpath) ^ "' exists, please delete (will not overwrite)")
1.468 + else
1.469 + (
1.470 + (* serialize the formula 'fm' to a file *)
1.471 + if satformat="cnf" then
1.472 + prop_formula_to_dimacs_cnf_format fm false satpath
1.473 + else if satformat="defcnf" then
1.474 + prop_formula_to_dimacs_cnf_format fm true satpath
1.475 + else if satformat="sat" then
1.476 + prop_formula_to_dimacs_sat_format fm satpath
1.477 + else
1.478 + error ("invalid argument: satformat='" ^ satformat ^ "' (must be either 'cnf', 'defcnf', or 'sat')");
1.479 + (* execute SAT solver *)
1.480 + if (system command)<>0 then
1.481 + (
1.482 + (* error executing SAT solver *)
1.483 + File.rm satpath;
1.484 + File.rm resultpath;
1.485 + error ("system command '" ^ command ^ "' failed (make sure a SAT solver is installed)")
1.486 + )
1.487 + else
1.488 + (
1.489 + (* read assignment from the result file *)
1.490 + File.rm satpath;
1.491 + let
1.492 + (* 'a option -> 'a Library.option *)
1.493 + fun option (SOME a) =
1.494 + Some a
1.495 + | option NONE =
1.496 + None
1.497 + (* string -> int list *)
1.498 + fun string_to_int_list s =
1.499 + mapfilter (option o LargeInt.fromString) (space_explode " " s)
1.500 + (* string -> string -> bool *)
1.501 + fun is_substring s1 s2 =
1.502 + let
1.503 + val length1 = String.size s1
1.504 + val length2 = String.size s2
1.505 + in
1.506 + if length2 < length1 then
1.507 + false
1.508 + else if s1 = String.substring (s2, 0, length1) then
1.509 + true
1.510 + else is_substring s1 (String.substring (s2, 1, length2-1))
1.511 + end
1.512 + (* string list -> int list option *)
1.513 + fun extract_solution [] =
1.514 + None
1.515 + | extract_solution (line::lines) =
1.516 + if is_substring success line then
1.517 + (* the next line must be a list of integers *)
1.518 + Some (string_to_int_list (hd lines))
1.519 + else
1.520 + extract_solution lines
1.521 + val sat_result = File.read resultpath
1.522 + in
1.523 + File.rm resultpath;
1.524 + extract_solution (split_lines sat_result)
1.525 + end
1.526 + )
1.527 + );
1.528 +
1.529 +
1.530 +(* ------------------------------------------------------------------------- *)
1.531 +(* TREES *)
1.532 +(* ------------------------------------------------------------------------- *)
1.533 +
1.534 +(* ------------------------------------------------------------------------- *)
1.535 +(* tree: implements an arbitrarily (but finitely) branching tree as a list *)
1.536 +(* of (lists of ...) elements *)
1.537 +(* ------------------------------------------------------------------------- *)
1.538 +
1.539 + datatype 'a tree =
1.540 + Leaf of 'a
1.541 + | Node of ('a tree) list;
1.542 +
1.543 + type prop_tree =
1.544 + prop_formula list tree;
1.545 +
1.546 + (* ('a -> 'b) -> 'a tree -> 'b tree *)
1.547 +
1.548 + fun tree_map f tr =
1.549 + case tr of
1.550 + Leaf x => Leaf (f x)
1.551 + | Node xs => Node (map (tree_map f) xs);
1.552 +
1.553 + (* ('a * 'b -> 'a) -> 'a * ('b tree) -> 'a *)
1.554 +
1.555 + fun tree_foldl f =
1.556 + let
1.557 + fun itl (e, Leaf x) = f(e,x)
1.558 + | itl (e, Node xs) = foldl (tree_foldl f) (e,xs)
1.559 + in
1.560 + itl
1.561 + end;
1.562 +
1.563 + (* 'a tree * 'b tree -> ('a * 'b) tree *)
1.564 +
1.565 + fun tree_pair (t1,t2) =
1.566 + case t1 of
1.567 + Leaf x =>
1.568 + (case t2 of
1.569 + Leaf y => Leaf (x,y)
1.570 + | Node _ => raise REFUTE ("tree_pair", "trees are of different height (second tree is higher)"))
1.571 + | Node xs =>
1.572 + (case t2 of
1.573 + (* '~~' will raise an exception if the number of branches in both trees is different at the current node *)
1.574 + Node ys => Node (map tree_pair (xs ~~ ys))
1.575 + | Leaf _ => raise REFUTE ("tree_pair", "trees are of different height (first tree is higher)"));
1.576 +
1.577 +(* ------------------------------------------------------------------------- *)
1.578 +(* prop_tree_to_true: returns a propositional formula that is true iff the *)
1.579 +(* tree denotes the boolean value TRUE *)
1.580 +(* ------------------------------------------------------------------------- *)
1.581 +
1.582 + (* prop_tree -> prop_formula *)
1.583 +
1.584 + (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.585 + (* the term is true iff the leaf's first element is true *)
1.586 +
1.587 + fun prop_tree_to_true (Leaf [fm,_]) =
1.588 + fm
1.589 + | prop_tree_to_true _ =
1.590 + raise REFUTE ("prop_tree_to_true", "tree is not a 2-element leaf");
1.591 +
1.592 +(* ------------------------------------------------------------------------- *)
1.593 +(* prop_tree_to_false: returns a propositional formula that is true iff the *)
1.594 +(* tree denotes the boolean value FALSE *)
1.595 +(* ------------------------------------------------------------------------- *)
1.596 +
1.597 + (* prop_tree -> prop_formula *)
1.598 +
1.599 + (* a term of type 'bool' is represented as a 2-element leaf, where *)
1.600 + (* the term is false iff the leaf's second element is true *)
1.601 +
1.602 + fun prop_tree_to_false (Leaf [_,fm]) =
1.603 + fm
1.604 + | prop_tree_to_false _ =
1.605 + raise REFUTE ("prop_tree_to_false", "tree is not a 2-element leaf");
1.606 +
1.607 +(* ------------------------------------------------------------------------- *)
1.608 +(* restrict_to_single_element: returns a propositional formula which is true *)
1.609 +(* iff the tree 'tr' describes a single element of its corresponding *)
1.610 +(* type, i.e. iff at each leaf, one and only one formula is true *)
1.611 +(* ------------------------------------------------------------------------- *)
1.612 +
1.613 + (* prop_tree -> prop_formula *)
1.614 +
1.615 + fun restrict_to_single_element tr =
1.616 + let
1.617 + (* prop_formula list -> prop_formula *)
1.618 + fun allfalse [] = True
1.619 + | allfalse (x::xs) = SAnd (SNot x, allfalse xs)
1.620 + (* prop_formula list -> prop_formula *)
1.621 + fun exactly1true [] = False
1.622 + | exactly1true (x::xs) = SOr (SAnd (x, allfalse xs), SAnd (SNot x, exactly1true xs))
1.623 + in
1.624 + case tr of
1.625 + Leaf [BoolVar _, Not (BoolVar _)] => True (* optimization for boolean variables *)
1.626 + | Leaf xs => exactly1true xs
1.627 + | Node trees => list_conjunction (map restrict_to_single_element trees)
1.628 + end;
1.629 +
1.630 +(* ------------------------------------------------------------------------- *)
1.631 +(* HOL FORMULAS *)
1.632 +(* ------------------------------------------------------------------------- *)
1.633 +
1.634 +(* ------------------------------------------------------------------------- *)
1.635 +(* absvar: form an abstraction over a schematic variable *)
1.636 +(* ------------------------------------------------------------------------- *)
1.637 +
1.638 + (* Term.indexname * Term.typ * Term.term -> Term.term *)
1.639 +
1.640 + (* this function is similar to Term.absfree, but for schematic *)
1.641 + (* variables (rather than free variables) *)
1.642 + fun absvar ((x,i),T,body) =
1.643 + Abs(x, T, abstract_over (Var((x,i),T), body));
1.644 +
1.645 +(* ------------------------------------------------------------------------- *)
1.646 +(* list_all_var: quantification over a list of schematic variables *)
1.647 +(* ------------------------------------------------------------------------- *)
1.648 +
1.649 + (* (Term.indexname * Term.typ) list * Term.term -> Term.term *)
1.650 +
1.651 + (* this function is similar to Term.list_all_free, but for schematic *)
1.652 + (* variables (rather than free variables) *)
1.653 + fun list_all_var ([], t) =
1.654 + t
1.655 + | list_all_var ((idx,T)::vars, t) =
1.656 + (all T) $ (absvar(idx, T, list_all_var(vars,t)));
1.657 +
1.658 +(* ------------------------------------------------------------------------- *)
1.659 +(* close_vars: close up a formula over all schematic variables by *)
1.660 +(* quantification (note that the result term may still contain *)
1.661 +(* (non-schematic) free variables) *)
1.662 +(* ------------------------------------------------------------------------- *)
1.663 +
1.664 + (* Term.term -> Term.term *)
1.665 +
1.666 + (* this function is similar to Logic.close_form, but for schematic *)
1.667 + (* variables (rather than free variables) *)
1.668 + fun close_vars A =
1.669 + list_all_var (sort_wrt (fst o fst) (map dest_Var (term_vars A)), A);
1.670 +
1.671 +(* ------------------------------------------------------------------------- *)
1.672 +(* make_universes: given a list 'xs' of "types" and a universe size 'size', *)
1.673 +(* this function returns all possible partitions of the universe into *)
1.674 +(* the "types" in 'xs' such that no "type" is empty. If 'size' is less *)
1.675 +(* than 'length xs', the returned list of partitions is empty. *)
1.676 +(* Otherwise, if the list 'xs' is empty, then the returned list of *)
1.677 +(* partitions contains only the empty list, regardless of 'size'. *)
1.678 +(* ------------------------------------------------------------------------- *)
1.679 +
1.680 + (* 'a list -> int -> ('a * int) list list *)
1.681 +
1.682 + fun make_universes xs size =
1.683 + let
1.684 + (* 'a list -> int -> int -> ('a * int) list list *)
1.685 + fun make_partitions_loop (x::xs) 0 total =
1.686 + map (fn us => ((x,0)::us)) (make_partitions xs total)
1.687 + | make_partitions_loop (x::xs) first total =
1.688 + (map (fn us => ((x,first)::us)) (make_partitions xs (total-first))) @ (make_partitions_loop (x::xs) (first-1) total)
1.689 + | make_partitions_loop _ _ _ =
1.690 + raise REFUTE ("make_universes::make_partitions_loop", "empty list")
1.691 + and
1.692 + (* 'a list -> int -> ('a * int) list list *)
1.693 + make_partitions [x] size =
1.694 + (* we must use all remaining elements on the type 'x', so there is only one partition *)
1.695 + [[(x,size)]]
1.696 + | make_partitions (x::xs) 0 =
1.697 + (* there are no elements left in the universe, so there is only one partition *)
1.698 + [map (fn t => (t,0)) (x::xs)]
1.699 + | make_partitions (x::xs) size =
1.700 + (* we assign either size, size-1, ..., 1 or 0 elements to 'x'; the remaining elements are partitioned recursively *)
1.701 + make_partitions_loop (x::xs) size size
1.702 + | make_partitions _ _ =
1.703 + raise REFUTE ("make_universes::make_partitions", "empty list")
1.704 + val len = length xs
1.705 + in
1.706 + if size<len then
1.707 + (* the universe isn't big enough to make every type non-empty *)
1.708 + []
1.709 + else if xs=[] then
1.710 + (* no types: return one universe, regardless of the size *)
1.711 + [[]]
1.712 + else
1.713 + (* partition into possibly empty types, then add 1 element to each type *)
1.714 + map (fn us => map (fn (x,i) => (x,i+1)) us) (make_partitions xs (size-len))
1.715 + end;
1.716 +
1.717 +(* ------------------------------------------------------------------------- *)
1.718 +(* sum: computes the sum of a list of integers; sum [] = 0 *)
1.719 +(* ------------------------------------------------------------------------- *)
1.720 +
1.721 + (* int list -> int *)
1.722 +
1.723 + fun sum xs = foldl (op +) (0, xs);
1.724 +
1.725 +(* ------------------------------------------------------------------------- *)
1.726 +(* product: computes the product of a list of integers; product [] = 1 *)
1.727 +(* ------------------------------------------------------------------------- *)
1.728 +
1.729 + (* int list -> int *)
1.730 +
1.731 + fun product xs = foldl (op *) (1, xs);
1.732 +
1.733 +(* ------------------------------------------------------------------------- *)
1.734 +(* power: power(a,b) computes a^b, for a>=0, b>=0 *)
1.735 +(* ------------------------------------------------------------------------- *)
1.736 +
1.737 + (* int * int -> int *)
1.738 +
1.739 + fun power (a,0) = 1
1.740 + | power (a,1) = a
1.741 + | power (a,b) = let val ab = power(a,b div 2) in ab * ab * power(a,b mod 2) end;
1.742 +
1.743 +(* ------------------------------------------------------------------------- *)
1.744 +(* size_of_type: returns the size of a type, where 'us' specifies the size *)
1.745 +(* of each basic type (i.e. each type variable), and 'cdepth' specifies *)
1.746 +(* the maximal constructor depth for inductive datatypes *)
1.747 +(* ------------------------------------------------------------------------- *)
1.748 +
1.749 + (* Term.typ -> (Term.typ * int) list -> theory -> int -> int *)
1.750 +
1.751 + fun size_of_type T us thy cdepth =
1.752 + let
1.753 + (* Term.typ -> (Term.typ * int) -> int *)
1.754 + fun lookup_size T [] =
1.755 + raise REFUTE ("size_of_type", "no size specified for type variable '" ^ (Sign.string_of_typ (sign_of thy) T) ^ "'")
1.756 + | lookup_size T ((typ,size)::pairs) =
1.757 + if T=typ then size else lookup_size T pairs
1.758 + in
1.759 + case T of
1.760 + Type ("prop", []) => 2
1.761 + | Type ("bool", []) => 2
1.762 + | Type ("Product_Type.unit", []) => 1
1.763 + | Type ("+", [T1,T2]) => (size_of_type T1 us thy cdepth) + (size_of_type T2 us thy cdepth)
1.764 + | Type ("*", [T1,T2]) => (size_of_type T1 us thy cdepth) * (size_of_type T2 us thy cdepth)
1.765 + | Type ("fun", [T1,T2]) => power (size_of_type T2 us thy cdepth, size_of_type T1 us thy cdepth)
1.766 + | Type ("set", [T1]) => size_of_type (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
1.767 + | Type (s, Ts) =>
1.768 + (case DatatypePackage.datatype_info thy s of
1.769 + Some info => (* inductive datatype *)
1.770 + if cdepth>0 then
1.771 + let
1.772 + val index = #index info
1.773 + val descr = #descr info
1.774 + val (_, dtyps, constrs) = the (assoc (descr, index))
1.775 + val Typs = dtyps ~~ Ts
1.776 + (* DatatypeAux.dtyp -> Term.typ *)
1.777 + fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.778 + the (assoc (Typs, DatatypeAux.DtTFree a))
1.779 + | typ_of_dtyp (DatatypeAux.DtRec i) =
1.780 + let
1.781 + val (s, ds, _) = the (assoc (descr, i))
1.782 + in
1.783 + Type (s, map typ_of_dtyp ds)
1.784 + end
1.785 + | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.786 + Type (s, map typ_of_dtyp ds)
1.787 + in
1.788 + sum (map (fn (_,ds) => product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)) constrs)
1.789 + end
1.790 + else 0
1.791 + | None => error ("size_of_type: type contains an unknown type constructor: '" ^ s ^ "'"))
1.792 + | TFree _ => lookup_size T us
1.793 + | TVar _ => lookup_size T us
1.794 + end;
1.795 +
1.796 +(* ------------------------------------------------------------------------- *)
1.797 +(* type_to_prop_tree: creates a tree of boolean variables that denotes an *)
1.798 +(* element of the type 'T'. The height and branching factor of the *)
1.799 +(* tree depend on the size and "structure" of 'T'. *)
1.800 +(* 'us' : a "universe" specifying the number of elements for each basic type *)
1.801 +(* (i.e. each type variable) in 'T' *)
1.802 +(* 'cdepth': maximum constructor depth to be used for inductive datatypes *)
1.803 +(* 'idx': the next index to be used for a boolean variable *)
1.804 +(* ------------------------------------------------------------------------- *)
1.805 +
1.806 + (* Term.typ -> (Term.typ * int) list -> theory -> int -> int -> prop_tree * int *)
1.807 +
1.808 + fun type_to_prop_tree T us thy cdepth idx =
1.809 + let
1.810 + (* int -> Term.typ -> int -> prop_tree list * int *)
1.811 + fun type_to_prop_tree_list 1 T' idx' =
1.812 + let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
1.813 + ([tr], newidx)
1.814 + end
1.815 + | type_to_prop_tree_list n T' idx' =
1.816 + let val (tr, newidx) = type_to_prop_tree T' us thy cdepth idx' in
1.817 + let val (trees, lastidx) = type_to_prop_tree_list (n-1) T' newidx in
1.818 + (tr::trees, lastidx)
1.819 + end
1.820 + end
1.821 + in
1.822 + case T of
1.823 + Type ("prop", []) =>
1.824 + (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
1.825 + | Type ("bool", []) =>
1.826 + (Leaf [BoolVar idx, Not (BoolVar idx)], idx+1)
1.827 + | Type ("Product_Type.unit", []) =>
1.828 + (Leaf [True], idx)
1.829 + | Type ("+", [T1,T2]) =>
1.830 + let
1.831 + val s1 = size_of_type T1 us thy cdepth
1.832 + val s2 = size_of_type T2 us thy cdepth
1.833 + val s = s1 + s2
1.834 + in
1.835 + if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
1.836 + raise EMPTY_DATATYPE
1.837 + else
1.838 + error "sum types (+) not implemented yet (TODO)"
1.839 + end
1.840 + | Type ("*", [T1,T2]) =>
1.841 + let
1.842 + val s1 = size_of_type T1 us thy cdepth
1.843 + val s2 = size_of_type T2 us thy cdepth
1.844 + val s = s1 * s2
1.845 + in
1.846 + if s1=0 orelse s2=0 then
1.847 + raise EMPTY_DATATYPE
1.848 + else
1.849 + error "product types (*) not implemented yet (TODO)"
1.850 + end
1.851 + | Type ("fun", [T1,T2]) =>
1.852 + (* we create 'size_of_type T1' different copies of the tree for 'T2', *)
1.853 + (* which are then combined into a single new tree *)
1.854 + let
1.855 + val s = size_of_type T1 us thy cdepth
1.856 + in
1.857 + if s=0 then
1.858 + raise EMPTY_DATATYPE
1.859 + else
1.860 + let val (trees, newidx) = type_to_prop_tree_list s T2 idx in
1.861 + (Node trees, newidx)
1.862 + end
1.863 + end
1.864 + | Type ("set", [T1]) =>
1.865 + type_to_prop_tree (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth idx
1.866 + | Type (s, _) =>
1.867 + (case DatatypePackage.constrs_of thy s of
1.868 + Some _ => (* inductive datatype *)
1.869 + let
1.870 + val s = size_of_type T us thy cdepth
1.871 + in
1.872 + if s=0 then
1.873 + raise EMPTY_DATATYPE
1.874 + else
1.875 + (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.876 + end
1.877 + | None => error ("type_to_prop_tree: type contains an unknown type constructor: '" ^ s ^ "'"))
1.878 + | TFree _ =>
1.879 + let val s = size_of_type T us thy cdepth in
1.880 + (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.881 + end
1.882 + | TVar _ =>
1.883 + let val s = size_of_type T us thy cdepth in
1.884 + (Leaf (map (fn i => BoolVar i) (idx upto (idx+s-1))), idx+s)
1.885 + end
1.886 + end;
1.887 +
1.888 +(* ------------------------------------------------------------------------- *)
1.889 +(* type_to_constants: creates a list of prop_trees with constants (True, *)
1.890 +(* False) rather than boolean variables, one for every element in the *)
1.891 +(* type 'T'; c.f. type_to_prop_tree *)
1.892 +(* ------------------------------------------------------------------------- *)
1.893 +
1.894 + (* Term.typ -> (Term.typ * int) list -> theory -> int -> prop_tree list *)
1.895 +
1.896 + fun type_to_constants T us thy cdepth =
1.897 + let
1.898 + (* returns a list with all unit vectors of length n *)
1.899 + (* int -> prop_tree list *)
1.900 + fun unit_vectors n =
1.901 + let
1.902 + (* returns the k-th unit vector of length n *)
1.903 + (* int * int -> prop_tree *)
1.904 + fun unit_vector (k,n) =
1.905 + Leaf ((replicate (k-1) False) @ (True :: (replicate (n-k) False)))
1.906 + (* int -> prop_tree list -> prop_tree list *)
1.907 + fun unit_vectors_acc k vs =
1.908 + if k>n then [] else (unit_vector (k,n))::(unit_vectors_acc (k+1) vs)
1.909 + in
1.910 + unit_vectors_acc 1 []
1.911 + end
1.912 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.913 + (* 'a -> 'a list list -> 'a list list *)
1.914 + fun cons_list x xss =
1.915 + map (fn xs => x::xs) xss
1.916 + (* returns a list of lists, each one consisting of n (possibly identical) elements from 'xs' *)
1.917 + (* int -> 'a list -> 'a list list *)
1.918 + fun pick_all 1 xs =
1.919 + map (fn x => [x]) xs
1.920 + | pick_all n xs =
1.921 + let val rec_pick = pick_all (n-1) xs in
1.922 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.923 + end
1.924 + in
1.925 + case T of
1.926 + Type ("prop", []) => unit_vectors 2
1.927 + | Type ("bool", []) => unit_vectors 2
1.928 + | Type ("Product_Type.unit", []) => unit_vectors 1
1.929 + | Type ("+", [T1,T2]) =>
1.930 + let
1.931 + val s1 = size_of_type T1 us thy cdepth
1.932 + val s2 = size_of_type T2 us thy cdepth
1.933 + in
1.934 + if s1=0 orelse s2=0 then (* could use 'andalso' instead? *)
1.935 + raise EMPTY_DATATYPE
1.936 + else
1.937 + error "sum types (+) not implemented yet (TODO)"
1.938 + end
1.939 + | Type ("*", [T1,T2]) =>
1.940 + let
1.941 + val s1 = size_of_type T1 us thy cdepth
1.942 + val s2 = size_of_type T2 us thy cdepth
1.943 + in
1.944 + if s1=0 orelse s2=0 then
1.945 + raise EMPTY_DATATYPE
1.946 + else
1.947 + error "product types (*) not implemented yet (TODO)"
1.948 + end
1.949 + | Type ("fun", [T1,T2]) =>
1.950 + let
1.951 + val s = size_of_type T1 us thy cdepth
1.952 + in
1.953 + if s=0 then
1.954 + raise EMPTY_DATATYPE
1.955 + else
1.956 + map (fn xs => Node xs) (pick_all s (type_to_constants T2 us thy cdepth))
1.957 + end
1.958 + | Type ("set", [T1]) => type_to_constants (Type ("fun", [T1, HOLogic.boolT])) us thy cdepth
1.959 + | Type (s, _) =>
1.960 + (case DatatypePackage.constrs_of thy s of
1.961 + Some _ => (* inductive datatype *)
1.962 + let
1.963 + val s = size_of_type T us thy cdepth
1.964 + in
1.965 + if s=0 then
1.966 + raise EMPTY_DATATYPE
1.967 + else
1.968 + unit_vectors s
1.969 + end
1.970 + | None => error ("type_to_constants: type contains an unknown type constructor: '" ^ s ^ "'"))
1.971 + | TFree _ => unit_vectors (size_of_type T us thy cdepth)
1.972 + | TVar _ => unit_vectors (size_of_type T us thy cdepth)
1.973 + end;
1.974 +
1.975 +(* ------------------------------------------------------------------------- *)
1.976 +(* prop_tree_equal: returns a propositional formula that is true iff 'tr1' *)
1.977 +(* and 'tr2' both denote the same element *)
1.978 +(* ------------------------------------------------------------------------- *)
1.979 +
1.980 + (* prop_tree * prop_tree -> prop_formula *)
1.981 +
1.982 + fun prop_tree_equal (tr1,tr2) =
1.983 + case tr1 of
1.984 + Leaf x =>
1.985 + (case tr2 of
1.986 + Leaf y => prop_formula_dot_product (x,y)
1.987 + | _ => raise REFUTE ("prop_tree_equal", "second tree is higher"))
1.988 + | Node xs =>
1.989 + (case tr2 of
1.990 + Leaf _ => raise REFUTE ("prop_tree_equal", "first tree is higher")
1.991 + (* extensionality: two functions are equal iff they are equal for every element *)
1.992 + | Node ys => list_conjunction (map prop_tree_equal (xs ~~ ys)));
1.993 +
1.994 +(* ------------------------------------------------------------------------- *)
1.995 +(* prop_tree_apply: returns a tree that denotes the element obtained by *)
1.996 +(* applying the function which is denoted by the tree 't1' to the *)
1.997 +(* element which is denoted by the tree 't2' *)
1.998 +(* ------------------------------------------------------------------------- *)
1.999 +
1.1000 + (* prop_tree * prop_tree -> prop_tree *)
1.1001 +
1.1002 + fun prop_tree_apply (tr1,tr2) =
1.1003 + let
1.1004 + (* prop_tree * prop_tree -> prop_tree *)
1.1005 + fun prop_tree_disjunction (tr1,tr2) =
1.1006 + tree_map (fn (xs,ys) => map (fn (x,y) => SOr(x,y)) (xs ~~ ys)) (tree_pair (tr1,tr2))
1.1007 + (* prop_formula * prop_tree -> prop_tree *)
1.1008 + fun prop_formula_times_prop_tree (fm,tr) =
1.1009 + tree_map (map (fn x => SAnd (fm,x))) tr
1.1010 + (* prop_formula list * prop_tree list -> prop_tree *)
1.1011 + fun prop_formula_list_dot_product_prop_tree_list ([fm],[tr]) =
1.1012 + prop_formula_times_prop_tree (fm,tr)
1.1013 + | prop_formula_list_dot_product_prop_tree_list (fm::fms,tr::trees) =
1.1014 + prop_tree_disjunction (prop_formula_times_prop_tree (fm,tr), prop_formula_list_dot_product_prop_tree_list (fms,trees))
1.1015 + | prop_formula_list_dot_product_prop_tree_list (_,_) =
1.1016 + raise REFUTE ("prop_tree_apply::prop_formula_list_dot_product_prop_tree_list", "empty list")
1.1017 + (* concatenates 'x' with every list in 'xss', returning a new list of lists *)
1.1018 + (* 'a -> 'a list list -> 'a list list *)
1.1019 + fun cons_list x xss =
1.1020 + map (fn xs => x::xs) xss
1.1021 + (* returns a list of lists, each one consisting of one element from each element of 'xss' *)
1.1022 + (* 'a list list -> 'a list list *)
1.1023 + fun pick_all [xs] =
1.1024 + map (fn x => [x]) xs
1.1025 + | pick_all (xs::xss) =
1.1026 + let val rec_pick = pick_all xss in
1.1027 + foldl (fn (acc,x) => (cons_list x rec_pick) @ acc) ([],xs)
1.1028 + end
1.1029 + | pick_all _ =
1.1030 + raise REFUTE ("prop_tree_apply::pick_all", "empty list")
1.1031 + (* prop_tree -> prop_formula list *)
1.1032 + fun prop_tree_to_prop_formula_list (Leaf xs) =
1.1033 + xs
1.1034 + | prop_tree_to_prop_formula_list (Node trees) =
1.1035 + map list_conjunction (pick_all (map prop_tree_to_prop_formula_list trees))
1.1036 + in
1.1037 + case tr1 of
1.1038 + Leaf _ =>
1.1039 + raise REFUTE ("prop_tree_apply", "first tree is a leaf")
1.1040 + | Node xs =>
1.1041 + prop_formula_list_dot_product_prop_tree_list (prop_tree_to_prop_formula_list tr2, xs)
1.1042 + end
1.1043 +
1.1044 +(* ------------------------------------------------------------------------- *)
1.1045 +(* term_to_prop_tree: translates a HOL term 't' into a tree of propositional *)
1.1046 +(* formulas; 'us' specifies the number of elements for each type *)
1.1047 +(* variable in 't'; 'cdepth' specifies the maximal constructor depth *)
1.1048 +(* for inductive datatypes. Also returns the lowest index that was not *)
1.1049 +(* used for a boolean variable, and a substitution of terms (free/ *)
1.1050 +(* schematic variables) by prop_trees. *)
1.1051 +(* ------------------------------------------------------------------------- *)
1.1052 +
1.1053 + (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.1054 +
1.1055 + fun term_to_prop_tree t us thy cdepth =
1.1056 + let
1.1057 + (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.1058 + fun variable_to_prop_tree_subst t' (idx,subs) =
1.1059 + case assoc (subs,t') of
1.1060 + Some tr =>
1.1061 + (* return the previously associated tree; the substitution remains unchanged *)
1.1062 + (tr, (idx,subs))
1.1063 + | None =>
1.1064 + (* generate a new tree; update the index; extend the substitution *)
1.1065 + let
1.1066 + val T = case t' of
1.1067 + Free (_,T) => T
1.1068 + | Var (_,T) => T
1.1069 + | _ => raise REFUTE ("variable_to_prop_tree_subst", "term is not a (free or schematic) variable")
1.1070 + val (tr,newidx) = type_to_prop_tree T us thy cdepth idx
1.1071 + in
1.1072 + (tr, (newidx, (t',tr)::subs))
1.1073 + end
1.1074 + (* Term.term -> int * (Term.term * prop_tree) list -> prop_tree list -> prop_tree * (int * (Term.term * prop_tree) list) *)
1.1075 + fun term_to_prop_tree_subst t' (idx,subs) bsubs =
1.1076 + case t' of
1.1077 + (* meta-logical constants *)
1.1078 + Const ("Goal", _) $ t1 =>
1.1079 + term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1080 + | Const ("all", _) $ t1 =>
1.1081 + let
1.1082 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1083 + in
1.1084 + case tree1 of
1.1085 + Node xs =>
1.1086 + let
1.1087 + val fmTrue = list_conjunction (map prop_tree_to_true xs)
1.1088 + val fmFalse = list_disjunction (map prop_tree_to_false xs)
1.1089 + in
1.1090 + (Leaf [fmTrue, fmFalse], (i1,s1))
1.1091 + end
1.1092 + | _ =>
1.1093 + raise REFUTE ("term_to_prop_tree_subst", "'all' is not followed by a function")
1.1094 + end
1.1095 + | Const ("==", _) $ t1 $ t2 =>
1.1096 + let
1.1097 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1098 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1099 + val fmTrue = prop_tree_equal (tree1,tree2)
1.1100 + val fmFalse = SNot fmTrue
1.1101 + in
1.1102 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1103 + end
1.1104 + | Const ("==>", _) $ t1 $ t2 =>
1.1105 + let
1.1106 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1107 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1108 + val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
1.1109 + val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
1.1110 + in
1.1111 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1112 + end
1.1113 + (* HOL constants *)
1.1114 + | Const ("Trueprop", _) $ t1 =>
1.1115 + term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1116 + | Const ("Not", _) $ t1 =>
1.1117 + let
1.1118 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1119 + val fmTrue = prop_tree_to_false tree1
1.1120 + val fmFalse = prop_tree_to_true tree1
1.1121 + in
1.1122 + (Leaf [fmTrue, fmFalse], (i1,s1))
1.1123 + end
1.1124 + | Const ("True", _) =>
1.1125 + (Leaf [True, False], (idx,subs))
1.1126 + | Const ("False", _) =>
1.1127 + (Leaf [False, True], (idx,subs))
1.1128 + | Const ("All", _) $ t1 =>
1.1129 + let
1.1130 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1131 + in
1.1132 + case tree1 of
1.1133 + Node xs =>
1.1134 + let
1.1135 + val fmTrue = list_conjunction (map prop_tree_to_true xs)
1.1136 + val fmFalse = list_disjunction (map prop_tree_to_false xs)
1.1137 + in
1.1138 + (Leaf [fmTrue, fmFalse], (i1,s1))
1.1139 + end
1.1140 + | _ =>
1.1141 + raise REFUTE ("term_to_prop_tree_subst", "'All' is not followed by a function")
1.1142 + end
1.1143 + | Const ("Ex", _) $ t1 =>
1.1144 + let
1.1145 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1146 + in
1.1147 + case tree1 of
1.1148 + Node xs =>
1.1149 + let
1.1150 + val fmTrue = list_disjunction (map prop_tree_to_true xs)
1.1151 + val fmFalse = list_conjunction (map prop_tree_to_false xs)
1.1152 + in
1.1153 + (Leaf [fmTrue, fmFalse], (i1,s1))
1.1154 + end
1.1155 + | _ =>
1.1156 + raise REFUTE ("term_to_prop_tree_subst", "'Ex' is not followed by a function")
1.1157 + end
1.1158 + | Const ("Ex1", Type ("fun", [Type ("fun", [T, Type ("bool",[])]), Type ("bool",[])])) $ t1 =>
1.1159 + (* 'Ex1 t1' is equivalent to 'Ex Abs(x,T,t1' x & All Abs(y,T,t1'' y --> x=y))' *)
1.1160 + let
1.1161 + val t1' = Term.incr_bv (1, 0, t1)
1.1162 + val t1'' = Term.incr_bv (2, 0, t1)
1.1163 + val t_equal = (HOLogic.eq_const T) $ (Bound 1) $ (Bound 0)
1.1164 + val t_unique = (HOLogic.all_const T) $ Abs("y",T,HOLogic.mk_imp (t1'' $ (Bound 0),t_equal))
1.1165 + val t_ex1 = (HOLogic.exists_const T) $ Abs("x",T,HOLogic.mk_conj (t1' $ (Bound 0),t_unique))
1.1166 + in
1.1167 + term_to_prop_tree_subst t_ex1 (idx,subs) bsubs
1.1168 + end
1.1169 + | Const ("op =", _) $ t1 $ t2 =>
1.1170 + let
1.1171 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1172 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1173 + val fmTrue = prop_tree_equal (tree1,tree2)
1.1174 + val fmFalse = SNot fmTrue
1.1175 + in
1.1176 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1177 + end
1.1178 + | Const ("op &", _) $ t1 $ t2 =>
1.1179 + let
1.1180 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1181 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1182 + val fmTrue = SAnd (prop_tree_to_true tree1, prop_tree_to_true tree2)
1.1183 + val fmFalse = SOr (prop_tree_to_false tree1, prop_tree_to_false tree2)
1.1184 + in
1.1185 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1186 + end
1.1187 + | Const ("op |", _) $ t1 $ t2 =>
1.1188 + let
1.1189 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1190 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1191 + val fmTrue = SOr (prop_tree_to_true tree1, prop_tree_to_true tree2)
1.1192 + val fmFalse = SAnd (prop_tree_to_false tree1, prop_tree_to_false tree2)
1.1193 + in
1.1194 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1195 + end
1.1196 + | Const ("op -->", _) $ t1 $ t2 =>
1.1197 + let
1.1198 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1199 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1200 + val fmTrue = SOr (prop_tree_to_false tree1, prop_tree_to_true tree2)
1.1201 + val fmFalse = SAnd (prop_tree_to_true tree1, prop_tree_to_false tree2)
1.1202 + in
1.1203 + (Leaf [fmTrue, fmFalse], (i2,s2))
1.1204 + end
1.1205 + (* set constants *)
1.1206 + | Const ("Collect", _) $ t1 =>
1.1207 + term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1208 + | Const ("op :", _) $ t1 $ t2 =>
1.1209 + term_to_prop_tree_subst (t2 $ t1) (idx,subs) bsubs
1.1210 + (* datatype constants *)
1.1211 + | Const ("Product_Type.Unity", _) =>
1.1212 + (Leaf [True], (idx,subs))
1.1213 + (* unknown constants *)
1.1214 + | Const (c, _) =>
1.1215 + error ("term contains an unknown constant: '" ^ c ^ "'")
1.1216 + (* abstractions *)
1.1217 + | Abs (_,T,body) =>
1.1218 + let
1.1219 + val constants = type_to_constants T us thy cdepth
1.1220 + val (trees, substs) = split_list (map (fn c => term_to_prop_tree_subst body (idx,subs) (c::bsubs)) constants)
1.1221 + in
1.1222 + (* the substitutions in 'substs' are all identical *)
1.1223 + (Node trees, hd substs)
1.1224 + end
1.1225 + (* (free/schematic) variables *)
1.1226 + | Free _ =>
1.1227 + variable_to_prop_tree_subst t' (idx,subs)
1.1228 + | Var _ =>
1.1229 + variable_to_prop_tree_subst t' (idx,subs)
1.1230 + (* bound variables *)
1.1231 + | Bound i =>
1.1232 + if (length bsubs) <= i then
1.1233 + raise REFUTE ("term_to_prop_tree_subst", "term contains a loose bound variable (with index " ^ (string_of_int i) ^ ")")
1.1234 + else
1.1235 + (nth_elem (i,bsubs), (idx,subs))
1.1236 + (* application *)
1.1237 + | t1 $ t2 =>
1.1238 + let
1.1239 + val (tree1,(i1,s1)) = term_to_prop_tree_subst t1 (idx,subs) bsubs
1.1240 + val (tree2,(i2,s2)) = term_to_prop_tree_subst t2 (i1,s1) bsubs
1.1241 + in
1.1242 + (prop_tree_apply (tree1,tree2), (i2,s2))
1.1243 + end
1.1244 + in
1.1245 + term_to_prop_tree_subst t (1,[]) []
1.1246 + end;
1.1247 +
1.1248 +(* ------------------------------------------------------------------------- *)
1.1249 +(* term_to_prop_formula: translates a HOL formula 't' into a propositional *)
1.1250 +(* formula that is satisfiable if and only if 't' has a model of "size" *)
1.1251 +(* 'us' (where 'us' specifies the number of elements for each free type *)
1.1252 +(* variable in 't') and maximal constructor depth 'cdepth'. *)
1.1253 +(* ------------------------------------------------------------------------- *)
1.1254 +
1.1255 + (* TODO: shouldn't 'us' also specify the number of elements for schematic type variables? (if so, modify the comment above) *)
1.1256 +
1.1257 + (* Term.term -> (Term.typ * int) list -> theory -> int -> prop_formula * (int * (Term.term * prop_tree) list) *)
1.1258 +
1.1259 + fun term_to_prop_formula t us thy cdepth =
1.1260 + let
1.1261 + val (tr, (idx,subs)) = term_to_prop_tree t us thy cdepth
1.1262 + val fm = prop_tree_to_true tr
1.1263 + in
1.1264 + if subs=[] then
1.1265 + (fm, (idx,subs))
1.1266 + else
1.1267 + (* make sure every tree that is substituted for a term describes a single element *)
1.1268 + (SAnd (list_conjunction (map (fn (_,tr) => restrict_to_single_element tr) subs), fm), (idx,subs))
1.1269 + end;
1.1270 +
1.1271 +
1.1272 +(* ------------------------------------------------------------------------- *)
1.1273 +(* INTERFACE, PART 2: FINDING A MODEL *)
1.1274 +(* ------------------------------------------------------------------------- *)
1.1275 +
1.1276 +(* ------------------------------------------------------------------------- *)
1.1277 +(* string_of_universe: prints a universe, i.e. an assignment of sizes for *)
1.1278 +(* types *)
1.1279 +(* thy: the current theory *)
1.1280 +(* us : a list containing types together with their size *)
1.1281 +(* ------------------------------------------------------------------------- *)
1.1282 +
1.1283 + (* theory -> (Term.typ * int) list -> string *)
1.1284 +
1.1285 + fun string_of_universe thy [] =
1.1286 + "empty universe (no type variables in term)"
1.1287 + | string_of_universe thy us =
1.1288 + space_implode ", " (map (fn (T,i) => (Sign.string_of_typ (sign_of thy) T) ^ ": " ^ (string_of_int i)) us);
1.1289 +
1.1290 +(* ------------------------------------------------------------------------- *)
1.1291 +(* string_of_model: prints a model, given by a substitution 'subs' of trees *)
1.1292 +(* of propositional variables and an assignment 'ass' of truth values *)
1.1293 +(* for these variables. *)
1.1294 +(* thy : the current theory *)
1.1295 +(* us : universe, specifies the "size" of each type (i.e. type variable) *)
1.1296 +(* cdepth: maximal constructor depth for inductive datatypes *)
1.1297 +(* subs : substitution of trees of propositional formulas (for variables) *)
1.1298 +(* ass : assignment of truth values for boolean variables; see function *)
1.1299 +(* 'truth_value' below for its meaning *)
1.1300 +(* ------------------------------------------------------------------------- *)
1.1301 +
1.1302 + (* theory -> (Term.typ * int) list -> int -> (Term.term * prop_formula tree) list -> int list -> string *)
1.1303 +
1.1304 + fun string_of_model thy us cdepth [] ass =
1.1305 + "empty interpretation (no free variables in term)"
1.1306 + | string_of_model thy us cdepth subs ass =
1.1307 + let
1.1308 + (* Sign.sg *)
1.1309 + val sg = sign_of thy
1.1310 + (* int -> bool *)
1.1311 + fun truth_value i =
1.1312 + if i mem ass then true
1.1313 + else if ~i mem ass then false
1.1314 + else error ("SAT solver assignment does not specify a value for variable " ^ (string_of_int i))
1.1315 + (* string -> string *)
1.1316 + fun strip_leading_quote str =
1.1317 + if nth_elem_string(0,str)="'" then
1.1318 + String.substring (str, 1, size str - 1)
1.1319 + else
1.1320 + str;
1.1321 + (* prop_formula list -> int *)
1.1322 + fun true_index xs =
1.1323 + (* returns the (0-based) index of the first true formula in xs *)
1.1324 + let fun true_index_acc [] _ =
1.1325 + raise REFUTE ("string_of_model::true_index", "no variable was set to true")
1.1326 + | true_index_acc (x::xs) n =
1.1327 + case x of
1.1328 + BoolVar i =>
1.1329 + if truth_value i then n else true_index_acc xs (n+1)
1.1330 + | True =>
1.1331 + n
1.1332 + | False =>
1.1333 + true_index_acc xs (n+1)
1.1334 + | _ =>
1.1335 + raise REFUTE ("string_of_model::true_index", "formula is not a boolean variable/true/false")
1.1336 + in
1.1337 + true_index_acc xs 0
1.1338 + end
1.1339 + (* Term.typ -> int -> prop_tree -> string *)
1.1340 + (* prop *)
1.1341 + fun string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
1.1342 + if truth_value i then "true" else "false"
1.1343 + | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [True, False]) =
1.1344 + "true"
1.1345 + | string_of_prop_tree (Type ("prop",[])) cdepth (Leaf [False, True]) =
1.1346 + "false"
1.1347 + (* bool *)
1.1348 + | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [BoolVar i, Not (BoolVar _)]) =
1.1349 + if truth_value i then "true" else "false"
1.1350 + | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [True, False]) =
1.1351 + "true"
1.1352 + | string_of_prop_tree (Type ("bool",[])) cdepth (Leaf [False, True]) =
1.1353 + "false"
1.1354 + (* unit *)
1.1355 + | string_of_prop_tree (Type ("Product_Type.unit",[])) cdepth (Leaf [True]) =
1.1356 + "()"
1.1357 + | string_of_prop_tree (Type (s,Ts)) cdepth (Leaf xs) =
1.1358 + (case DatatypePackage.datatype_info thy s of
1.1359 + Some info => (* inductive datatype *)
1.1360 + let
1.1361 + val index = #index info
1.1362 + val descr = #descr info
1.1363 + val (_, dtyps, constrs) = the (assoc (descr, index))
1.1364 + val Typs = dtyps ~~ Ts
1.1365 + (* string -> string *)
1.1366 + fun unqualify s =
1.1367 + implode (snd (take_suffix (fn c => c <> ".") (explode s)))
1.1368 + (* DatatypeAux.dtyp -> Term.typ *)
1.1369 + fun typ_of_dtyp (DatatypeAux.DtTFree a) =
1.1370 + the (assoc (Typs, DatatypeAux.DtTFree a))
1.1371 + | typ_of_dtyp (DatatypeAux.DtRec i) =
1.1372 + let
1.1373 + val (s, ds, _) = the (assoc (descr, i))
1.1374 + in
1.1375 + Type (s, map typ_of_dtyp ds)
1.1376 + end
1.1377 + | typ_of_dtyp (DatatypeAux.DtType (s, ds)) =
1.1378 + Type (s, map typ_of_dtyp ds)
1.1379 + (* DatatypeAux.dtyp list -> int -> string *)
1.1380 + fun string_of_inductive_type_cargs [] n =
1.1381 + if n<>0 then
1.1382 + raise REFUTE ("string_of_model", "internal error computing the element index for an inductive type")
1.1383 + else
1.1384 + ""
1.1385 + | string_of_inductive_type_cargs (d::ds) n =
1.1386 + let
1.1387 + val size_ds = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
1.1388 + in
1.1389 + " " ^ (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))
1.1390 + end
1.1391 + (* (string * DatatypeAux.dtyp list) list -> int -> string *)
1.1392 + fun string_of_inductive_type_constrs [] n =
1.1393 + raise REFUTE ("string_of_model", "inductive type has fewer elements than needed")
1.1394 + | string_of_inductive_type_constrs ((s,ds)::cs) n =
1.1395 + let
1.1396 + val size = product (map (fn d => size_of_type (typ_of_dtyp d) us thy (cdepth-1)) ds)
1.1397 + in
1.1398 + if n < size then
1.1399 + (unqualify s) ^ (string_of_inductive_type_cargs ds n)
1.1400 + else
1.1401 + string_of_inductive_type_constrs cs (n - size)
1.1402 + end
1.1403 + in
1.1404 + string_of_inductive_type_constrs constrs (true_index xs)
1.1405 + end
1.1406 + | None =>
1.1407 + raise REFUTE ("string_of_model", "type contains an unknown type constructor: '" ^ s ^ "'"))
1.1408 + (* type variable *)
1.1409 + | string_of_prop_tree (TFree (s,_)) cdepth (Leaf xs) =
1.1410 + (strip_leading_quote s) ^ (string_of_int (true_index xs))
1.1411 + | string_of_prop_tree (TVar ((s,_),_)) cdepth (Leaf xs) =
1.1412 + (strip_leading_quote s) ^ (string_of_int (true_index xs))
1.1413 + (* function or set type *)
1.1414 + | string_of_prop_tree T cdepth (Node xs) =
1.1415 + case T of
1.1416 + Type ("fun", [T1,T2]) =>
1.1417 + let
1.1418 + 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)
1.1419 + in
1.1420 + "(" ^ (space_implode ", " strings) ^ ")"
1.1421 + end
1.1422 + | Type ("set", [T1]) =>
1.1423 + let
1.1424 + 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)
1.1425 + in
1.1426 + "{" ^ (space_implode ", " strings) ^ "}"
1.1427 + end
1.1428 + | _ => raise REFUTE ("string_of_model::string_of_prop_tree", "not a function/set type")
1.1429 + (* Term.term * prop_formula tree -> string *)
1.1430 + fun string_of_term_assignment (t,tr) =
1.1431 + let
1.1432 + val T = case t of
1.1433 + Free (_,T) => T
1.1434 + | Var (_,T) => T
1.1435 + | _ => raise REFUTE ("string_of_model::string_of_term_assignment", "term is not a (free or schematic) variable")
1.1436 + in
1.1437 + (Sign.string_of_term sg t) ^ " = " ^ (string_of_prop_tree T cdepth tr)
1.1438 + end
1.1439 + in
1.1440 + space_implode "\n" (map string_of_term_assignment subs)
1.1441 + end;
1.1442 +
1.1443 +(* ------------------------------------------------------------------------- *)
1.1444 +(* find_model: repeatedly calls 'prop_formula_sat_solver' with appropriate *)
1.1445 +(* parameters, and displays the results to the user *)
1.1446 +(* params : list of '(name, value)' pairs used to override default *)
1.1447 +(* parameters *)
1.1448 +(* *)
1.1449 +(* This is a brief description of the algorithm implemented: *)
1.1450 +(* *)
1.1451 +(* 1. Let k = max ('minsize',1). *)
1.1452 +(* 2. Let the universe have k elements. Find all possible partitions of *)
1.1453 +(* these elements into the basic types occuring in 't' such that no basic *)
1.1454 +(* type is empty. *)
1.1455 +(* 3. Translate 't' into a propositional formula p s.t. 't' has a model wrt. *)
1.1456 +(* the partition chosen in step (2.) if (actually, if and only if) p is *)
1.1457 +(* satisfiable. To do this, replace quantification by conjunction/ *)
1.1458 +(* disjunction over all elements of the type being quantified over. (If *)
1.1459 +(* p contains more than 'maxvars' boolean variables, terminate.) *)
1.1460 +(* 4. Serialize p to a file, and try to find a satisfying assignment for p *)
1.1461 +(* by invoking an external SAT solver. *)
1.1462 +(* 5. If the SAT solver finds a satisfying assignment for p, translate this *)
1.1463 +(* assignment back into a model for 't'. Present this model to the user, *)
1.1464 +(* then terminate. *)
1.1465 +(* 6. As long as there is another partition left, pick it and go back to *)
1.1466 +(* step (3.). *)
1.1467 +(* 7. Increase k by 1. As long as k does not exceed 'maxsize', go back to *)
1.1468 +(* step (2.). *)
1.1469 +(* *)
1.1470 +(* The following parameters are currently supported (and required!): *)
1.1471 +(* *)
1.1472 +(* Name Type Description *)
1.1473 +(* *)
1.1474 +(* "minsize" int Only search for models with size at least *)
1.1475 +(* 'minsize'. *)
1.1476 +(* "maxsize" int If >0, only search for models with size at most *)
1.1477 +(* 'maxsize'. *)
1.1478 +(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
1.1479 +(* when transforming the term into a propositional *)
1.1480 +(* formula. *)
1.1481 +(* "satfile" string Name of the file used to store the propositional *)
1.1482 +(* formula, i.e. the input to the SAT solver. *)
1.1483 +(* "satformat" string Format of the SAT solver's input file. Must be *)
1.1484 +(* either "cnf", "defcnf", or "sat". Since "sat" is *)
1.1485 +(* not supported by most SAT solvers, and "cnf" can *)
1.1486 +(* cause exponential blowup of the formula, "defcnf" *)
1.1487 +(* is recommended. *)
1.1488 +(* "resultfile" string Name of the file containing the SAT solver's *)
1.1489 +(* output. *)
1.1490 +(* "success" string Part of the line in the SAT solver's output that *)
1.1491 +(* precedes a list of integers representing the *)
1.1492 +(* satisfying assignment. *)
1.1493 +(* "command" string System command used to execute the SAT solver. *)
1.1494 +(* Note that you if you change 'satfile' or *)
1.1495 +(* 'resultfile', you will also need to change *)
1.1496 +(* 'command'. *)
1.1497 +(* *)
1.1498 +(* See the Isabelle/Isar theory 'Refute.thy' for reasonable default values. *)
1.1499 +(* ------------------------------------------------------------------------- *)
1.1500 +
1.1501 + (* theory -> (string * string) list -> Term.term -> unit *)
1.1502 +
1.1503 + fun find_model thy params t =
1.1504 + let
1.1505 + (* (string * string) list * (string * string) list -> (string * string) list *)
1.1506 + fun add_params (parms, []) =
1.1507 + parms
1.1508 + | add_params (parms, defparm::defparms) =
1.1509 + add_params (gen_ins (fn (a, b) => (fst a) = (fst b)) (defparm, parms), defparms)
1.1510 + (* (string * string) list * string -> int *)
1.1511 + fun read_int (parms, name) =
1.1512 + case assoc_string (parms, name) of
1.1513 + Some s => (case LargeInt.fromString s of
1.1514 + SOME i => i
1.1515 + | NONE => error ("parameter '" ^ name ^ "' (value is '" ^ s ^ "') must be an integer value"))
1.1516 + | None => error ("parameter '" ^ name ^ "' must be assigned a value")
1.1517 + (* (string * string) list * string -> string *)
1.1518 + fun read_string (parms, name) =
1.1519 + case assoc_string (parms, name) of
1.1520 + Some s => s
1.1521 + | None => error ("parameter '" ^ name ^ "' must be assigned a value")
1.1522 + (* (string * string) list *)
1.1523 + val allparams = add_params (params, get_default_params thy)
1.1524 + (* int *)
1.1525 + val minsize = read_int (allparams, "minsize")
1.1526 + val maxsize = read_int (allparams, "maxsize")
1.1527 + val maxvars = read_int (allparams, "maxvars")
1.1528 + (* string *)
1.1529 + val satfile = read_string (allparams, "satfile")
1.1530 + val satformat = read_string (allparams, "satformat")
1.1531 + val resultfile = read_string (allparams, "resultfile")
1.1532 + val success = read_string (allparams, "success")
1.1533 + val command = read_string (allparams, "command")
1.1534 + (* misc *)
1.1535 + val satpath = Path.unpack satfile
1.1536 + val resultpath = Path.unpack resultfile
1.1537 + val sg = sign_of thy
1.1538 + (* Term.typ list *)
1.1539 + val tvars = map (fn (i,s) => TVar(i,s)) (term_tvars t)
1.1540 + val tfrees = map (fn (x,s) => TFree(x,s)) (term_tfrees t)
1.1541 + (* universe -> int -> bool *)
1.1542 + fun find_model_universe u cdepth =
1.1543 + let
1.1544 + (* given the universe 'u' and constructor depth 'cdepth', translate *)
1.1545 + (* the term 't' into a propositional formula 'fm' *)
1.1546 + val (fm,(idx,subs)) = term_to_prop_formula t u thy cdepth
1.1547 + val usedvars = idx-1
1.1548 + in
1.1549 + (* 'maxvars=0' means "use as many variables as necessary" *)
1.1550 + if usedvars>maxvars andalso maxvars<>0 then
1.1551 + (
1.1552 + (* too many variables used: terminate *)
1.1553 + writeln ("\nSearch terminated: " ^ (string_of_int usedvars) ^ " boolean variables used (only " ^ (string_of_int maxvars) ^ " allowed).");
1.1554 + true
1.1555 + )
1.1556 + else
1.1557 + (* pass the formula 'fm' to an external SAT solver *)
1.1558 + case prop_formula_sat_solver fm satpath satformat resultpath success command of
1.1559 + None =>
1.1560 + (* no model found *)
1.1561 + false
1.1562 + | Some assignment =>
1.1563 + (* model found: terminate *)
1.1564 + (
1.1565 + writeln ("\nModel found:\n" ^ (string_of_universe thy u) ^ "\n" ^ (string_of_model thy u cdepth subs assignment));
1.1566 + true
1.1567 + )
1.1568 + end
1.1569 + (* universe list -> int -> bool *)
1.1570 + fun find_model_universes [] cdepth =
1.1571 + (
1.1572 + std_output "\n";
1.1573 + false
1.1574 + )
1.1575 + | find_model_universes (u::us) cdepth =
1.1576 + (
1.1577 + std_output ".";
1.1578 + ((if find_model_universe u cdepth then
1.1579 + (* terminate *)
1.1580 + true
1.1581 + else
1.1582 + (* continue search with the next universe *)
1.1583 + find_model_universes us cdepth)
1.1584 + handle EMPTY_DATATYPE => (std_output "[empty inductive type (constructor depth too small)]\n"; false))
1.1585 + )
1.1586 + (* int * int -> unit *)
1.1587 + fun find_model_from_to (min,max) =
1.1588 + (* 'max=0' means "search for arbitrary large models" *)
1.1589 + if min>max andalso max<>0 then
1.1590 + writeln ("Search terminated: no model found.")
1.1591 + else
1.1592 + (
1.1593 + std_output ("Searching for a model of size " ^ (string_of_int min));
1.1594 + if find_model_universes (make_universes tfrees min) min then
1.1595 + (* terminate *)
1.1596 + ()
1.1597 + else
1.1598 + (* continue search with increased size *)
1.1599 + find_model_from_to (min+1, max)
1.1600 + )
1.1601 + in
1.1602 + writeln ("Trying to find a model of: " ^ (Sign.string_of_term sg t));
1.1603 + if tvars<>[] then
1.1604 + (* TODO: deal with schematic type variables in a better way, if possible *)
1.1605 + error "term contains schematic type variables"
1.1606 + else
1.1607 + (
1.1608 + if minsize<1 then
1.1609 + writeln ("'minsize' is less than 1; starting search with size 1.")
1.1610 + else
1.1611 + ();
1.1612 + if maxsize<max (minsize,1) andalso maxsize<>0 then
1.1613 + writeln ("'maxsize' is less than 'minsize': no model found.")
1.1614 + else
1.1615 + find_model_from_to (max (minsize,1), maxsize)
1.1616 + )
1.1617 + end;
1.1618 +
1.1619 +(* ------------------------------------------------------------------------- *)
1.1620 +(* refute_term: calls 'find_model' on the negation of a term *)
1.1621 +(* params : list of '(name, value)' pairs used to override default *)
1.1622 +(* parameters *)
1.1623 +(* ------------------------------------------------------------------------- *)
1.1624 +
1.1625 + (* theory -> (string * string) list -> Term.term -> unit *)
1.1626 +
1.1627 + fun refute_term thy params t =
1.1628 + let
1.1629 + (* TODO: schematic type variables? *)
1.1630 + val negation = close_vars (HOLogic.Not $ t)
1.1631 + (* If 't' is of type 'propT' (rather than 'boolT'), applying *)
1.1632 + (* 'HOLogic.Not' is not type-correct. However, this isn't *)
1.1633 + (* really a problem as long as 'find_model' still interprets *)
1.1634 + (* the resulting term correctly, without checking its type. *)
1.1635 + in
1.1636 + find_model thy params negation
1.1637 + end;
1.1638 +
1.1639 +(* ------------------------------------------------------------------------- *)
1.1640 +(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
1.1641 +(* params : list of '(name, value)' pairs used to override default *)
1.1642 +(* parameters *)
1.1643 +(* subgoal : 0-based index specifying the subgoal number *)
1.1644 +(* ------------------------------------------------------------------------- *)
1.1645 +
1.1646 + (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
1.1647 +
1.1648 + fun refute_subgoal thy params thm subgoal =
1.1649 + refute_term thy params (nth_elem (subgoal, prems_of thm));
1.1650 +
1.1651 +end