14350

1 
(* Title: HOL/Refute.thy


2 
ID: $Id$


3 
Author: Tjark Weber


4 
Copyright 20032004


5 


6 
Basic setup and documentation for the 'refute' (and 'refute_params') command.


7 
*)


8 


9 
(*  *)


10 
(* REFUTE *)


11 
(* *)


12 
(* We use a SAT solver to search for a (finite) model that refutes a given *)


13 
(* HOL formula. *)


14 
(*  *)


15 


16 
(*  *)


17 
(* INSTALLATION *)


18 
(* *)


19 
(* 1. Install a standalone SAT solver. The default parameters in *)


20 
(* 'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/ *)


21 
(* Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is *)


22 
(* installed as '$HOME/bin/zchaff'. If you want to use a different SAT *)


23 
(* solver (or install ZChaff to a different location), you will need to *)


24 
(* modify at least the values for 'command' and (probably) 'success'. *)


25 
(* *)


26 
(* 2. That's it. You can now use the 'refute' command in your own theories. *)


27 
(*  *)


28 


29 
(*  *)


30 
(* USAGE *)


31 
(* *)


32 
(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *)


33 
(* parameters are explained below. *)


34 
(*  *)


35 


36 
(*  *)


37 
(* CURRENT LIMITATIONS *)


38 
(* *)


39 
(* 'refute' currently accepts formulas of higherorder predicate logic (with *)


40 
(* equality), including free/bound/schematic variables, lambda abstractions, *)


41 
(* sets and set membership. *)


42 
(* *)


43 
(* NOT (YET) SUPPORTED ARE *)


44 
(* *)


45 
(*  schematic type variables *)


46 
(*  type constructors other than =>, set, unit, and inductive datatypes *)


47 
(*  constants, including constructors of inductive datatypes and recursive *)


48 
(* functions on inductive datatypes *)


49 
(* *)


50 
(* Unfolding of constants currently needs to be done manually, e.g. using *)


51 
(* 'apply (unfold xxx_def)'. *)


52 
(* *)


53 
(* For formulas that contain (variables of) an inductive datatype, a *)


54 
(* spurious countermodel may be returned. Currently no warning is issued in *)


55 
(* this case. *)


56 
(*  *)


57 


58 
(*  *)


59 
(* PARAMETERS *)


60 
(* *)


61 
(* The following global parameters are currently supported (and required): *)


62 
(* *)


63 
(* Name Type Description *)


64 
(* *)


65 
(* "minsize" int Only search for models with size at least *)


66 
(* 'minsize'. *)


67 
(* "maxsize" int If >0, only search for models with size at most *)


68 
(* 'maxsize'. *)


69 
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)


70 
(* when transforming the term into a propositional *)


71 
(* formula. *)


72 
(* "satfile" string Name of the file used to store the propositional *)


73 
(* formula, i.e. the input to the SAT solver. *)


74 
(* "satformat" string Format of the SAT solver's input file. Must be *)


75 
(* either "cnf", "defcnf", or "sat". Since "sat" is *)


76 
(* not supported by most SAT solvers, and "cnf" can *)


77 
(* cause exponential blowup of the formula, "defcnf" *)


78 
(* is recommended. *)


79 
(* "resultfile" string Name of the file containing the SAT solver's *)


80 
(* output. *)


81 
(* "success" string Part of the line in the SAT solver's output that *)


82 
(* precedes a list of integers representing the *)


83 
(* satisfying assignment. *)


84 
(* "command" string System command used to execute the SAT solver. *)


85 
(* Note that you if you change 'satfile' or *)


86 
(* 'resultfile', you will also need to change *)


87 
(* 'command'. *)


88 
(*  *)


89 


90 
(*  *)


91 
(* FILES *)


92 
(* *)


93 
(* HOL/Tools/refute.ML Implementation of the algorithm. *)


94 
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)


95 
(* syntax. *)


96 
(* HOL/Refute.thy This file. Loads the ML files, basic setup, *)


97 
(* documentation. *)


98 
(* HOL/Main.thy Sets default parameters. *)


99 
(* HOL/ex/RefuteExamples.thy Examples. *)


100 
(*  *)


101 


102 
header {* Refute *}


103 


104 
theory Refute = Map


105 


106 
files "Tools/refute.ML"


107 
"Tools/refute_isar.ML":


108 


109 
(* Setting up the 'refute' and 'refute\_params' commands *)


110 


111 
use "Tools/refute.ML"


112 
use "Tools/refute_isar.ML"


113 


114 
setup Refute.setup


115 


116 
end
