author  blanchet 
Wed, 02 Mar 2011 15:51:22 +0100  
changeset 41872  10fd9e5d58ba 
parent 41871  394eef237bd1 
child 41875  e3cd0dce9b1a 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Finite model generation for HOL formulas using Kodkod. 

6 
*) 

7 

8 
signature NITPICK = 

9 
sig 

33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33580
diff
changeset

10 
type styp = Nitpick_Util.styp 
35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

11 
type term_postprocessor = Nitpick_Model.term_postprocessor 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

12 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

13 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

14 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

15 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

16 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

17 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

18 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

19 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

20 
monos: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

21 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

22 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

23 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

24 
blocking: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

25 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

26 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

27 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

28 
overlord: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

29 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

30 
assms: bool, 
38209  31 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

32 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

33 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

34 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

35 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

36 
star_linear_preds: bool, 
41856  37 
total_consts: bool option, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

38 
preconstrs: (term option * bool option) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

39 
peephole_optim: bool, 
38124  40 
datatype_sym_break: int, 
41 
kodkod_sym_break: int, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

42 
timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

43 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

44 
max_threads: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

45 
show_datatypes: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

46 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

47 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

48 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

49 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

50 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

51 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

52 
check_potential: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

53 
check_genuine: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

54 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

55 
expect: string} 
33192  56 

57 
val register_frac_type : string > (string * string) list > theory > theory 

58 
val unregister_frac_type : string > theory > theory 

59 
val register_codatatype : typ > string > styp list > theory > theory 

60 
val unregister_codatatype : typ > theory > theory 

35711
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

61 
val register_term_postprocessor : 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

62 
typ > term_postprocessor > theory > theory 
548d3f16404b
added term postprocessor to Nitpick, to provide custom syntax for typedefs
blanchet
parents:
35696
diff
changeset

63 
val unregister_term_postprocessor : typ > theory > theory 
33192  64 
val pick_nits_in_term : 
35335  65 
Proof.state > params > bool > int > int > int > (term * term) list 
66 
> term list > term > string * Proof.state 

33192  67 
val pick_nits_in_subgoal : 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

68 
Proof.state > params > bool > int > int > string * Proof.state 
33192  69 
end; 
70 

71 
structure Nitpick : NITPICK = 

72 
struct 

73 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

74 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

75 
open Nitpick_HOL 
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset

76 
open Nitpick_Preproc 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

77 
open Nitpick_Mono 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

78 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

79 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

80 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

81 
open Nitpick_Nut 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

82 
open Nitpick_Kodkod 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

83 
open Nitpick_Model 
33192  84 

34126  85 
structure KK = Kodkod 
86 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

87 
type params = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

88 
{cards_assigns: (typ option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

89 
maxes_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

90 
iters_assigns: (styp option * int list) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

91 
bitss: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

92 
bisim_depths: int list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

93 
boxes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

94 
finitizes: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

95 
monos: (typ option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

96 
stds: (typ option * bool) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

97 
wfs: (styp option * bool option) list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

98 
sat_solver: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

99 
blocking: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

100 
falsify: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

101 
debug: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

102 
verbose: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

103 
overlord: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

104 
user_axioms: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

105 
assms: bool, 
38209  106 
whacks: term list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

107 
merge_type_vars: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

108 
binary_ints: bool option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

109 
destroy_constrs: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

110 
specialize: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

111 
star_linear_preds: bool, 
41856  112 
total_consts: bool option, 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

113 
preconstrs: (term option * bool option) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

114 
peephole_optim: bool, 
38124  115 
datatype_sym_break: int, 
116 
kodkod_sym_break: int, 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

117 
timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

118 
tac_timeout: Time.time option, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

119 
max_threads: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

120 
show_datatypes: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

121 
show_consts: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

122 
evals: term list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

123 
formats: (term option * int list) list, 
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37257
diff
changeset

124 
atomss: (typ option * string list) list, 
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

125 
max_potential: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

126 
max_genuine: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

127 
check_potential: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

128 
check_genuine: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

129 
batch_size: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

130 
expect: string} 
33192  131 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

132 
(* TODO: eliminate these historical aliases *) 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

133 
val register_frac_type = Nitpick_HOL.register_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

134 
val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

135 
val register_codatatype = Nitpick_HOL.register_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

136 
val unregister_codatatype = Nitpick_HOL.unregister_codatatype_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

137 
val register_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

138 
Nitpick_Model.register_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

139 
val unregister_term_postprocessor = 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

140 
Nitpick_Model.unregister_term_postprocessor_global 
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

141 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

142 
type problem_extension = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

143 
{free_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

144 
sel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

145 
nonsel_names: nut list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

146 
rel_table: nut NameTable.table, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

147 
unsound: bool, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

148 
scope: scope} 
39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
38857
diff
changeset

149 

34126  150 
type rich_problem = KK.problem * problem_extension 
33192  151 

152 
fun pretties_for_formulas _ _ [] = [] 

153 
 pretties_for_formulas ctxt s ts = 

154 
[Pretty.str (s ^ plural_s_for_list ts ^ ":"), 

155 
Pretty.indent indent_size (Pretty.chunks 

156 
(map2 (fn j => fn t => 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

157 
Pretty.block [t > shorten_names_in_term 
33192  158 
> Syntax.pretty_term ctxt, 
159 
Pretty.str (if j = 1 then "." else ";")]) 

160 
(length ts downto 1) ts))] 

161 

35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

162 
fun install_java_message () = 
38517  163 
"Nitpick requires a Java 1.5 virtual machine called \"java\"." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

164 
fun install_kodkodi_message () = 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

165 
"Nitpick requires the external Java program Kodkodi. To install it, download \ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

166 
\the package from Isabelle's web page and add the \"kodkodix.y.z\" \ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

167 
\directory's full path to \"" ^ 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

168 
Path.implode (Path.expand (Path.appends 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

169 
(Path.variable "ISABELLE_HOME_USER" :: 
36266  170 
map Path.basic ["etc", "components"]))) ^ "\" on a line of its own." 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

171 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

172 
val max_unsound_delay_ms = 200 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

173 
val max_unsound_delay_percent = 2 
33192  174 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

175 
fun unsound_delay_for_timeout NONE = max_unsound_delay_ms 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

176 
 unsound_delay_for_timeout (SOME timeout) = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

177 
Int.max (0, Int.min (max_unsound_delay_ms, 
33192  178 
Time.toMilliseconds timeout 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

179 
* max_unsound_delay_percent div 100)) 
33192  180 

181 
fun passed_deadline NONE = false 

182 
 passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS 

183 

34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset

184 
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns 
33192  185 

41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

186 
fun has_lonely_bool_var (@{const Pure.conjunction} 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

187 
$ (@{const Trueprop} $ Free _) $ _) = true 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

188 
 has_lonely_bool_var _ = false 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

189 

34038
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

190 
val syntactic_sorts = 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38517
diff
changeset

191 
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @ 
34038
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

192 
@{sort number} 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

193 
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) = 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

194 
subset (op =) (S, syntactic_sorts) 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

195 
 has_tfree_syntactic_sort _ = false 
a2736debeabd
make Nitpick output the message "Hint: Maybe you forgot a type constraint?" only for syntactic classes
blanchet
parents:
33982
diff
changeset

196 
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort) 
33192  197 

33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

198 
fun plazy f = Pretty.blk (0, pstrs (f ())) 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

199 

41868
a4fb98eb0edf
make "preconstr" option more robust  shouldn't throw exceptions
blanchet
parents:
41858
diff
changeset

200 
fun check_constr_nut (Construct (_, _, _, us)) = List.app check_constr_nut us 
a4fb98eb0edf
make "preconstr" option more robust  shouldn't throw exceptions
blanchet
parents:
41858
diff
changeset

201 
 check_constr_nut _ = 
a4fb98eb0edf
make "preconstr" option more robust  shouldn't throw exceptions
blanchet
parents:
41858
diff
changeset

202 
error "The \"preconstr\" option requires a constructor term." 
a4fb98eb0edf
make "preconstr" option more robust  shouldn't throw exceptions
blanchet
parents:
41858
diff
changeset

203 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

204 
fun pick_them_nits_in_term deadline state (params : params) auto i n step 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

205 
subst assm_ts orig_t = 
33192  206 
let 
207 
val timer = Timer.startRealTimer () 

34935
cb011ba38950
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents:
34126
diff
changeset

208 
val thy = Proof.theory_of state 
cb011ba38950
removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
blanchet
parents:
34126
diff
changeset

209 
val ctxt = Proof.context_of state 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

210 
(* FIXME: reintroduce code before new release: 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

211 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37213
diff
changeset

212 
val nitpick_thy = Thy_Info.get_theory "Nitpick" 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

213 
val _ = Theory.subthy (nitpick_thy, thy) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

214 
error "You must import the theory \"Nitpick\" to use Nitpick" 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

215 
*) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

216 
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

217 
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug, 
38209  218 
verbose, overlord, user_axioms, assms, whacks, merge_type_vars, 
219 
binary_ints, destroy_constrs, specialize, star_linear_preds, 

41856  220 
total_consts, preconstrs, peephole_optim, datatype_sym_break, 
221 
kodkod_sym_break, tac_timeout, max_threads, show_datatypes, 

222 
show_consts, evals, formats, atomss, max_potential, max_genuine, 

223 
check_potential, check_genuine, batch_size, ...} = params 

33192  224 
val state_ref = Unsynchronized.ref state 
225 
val pprint = 

226 
if auto then 

227 
Unsynchronized.change state_ref o Proof.goal_message o K 

33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
33558
diff
changeset

228 
o Pretty.chunks o cons (Pretty.str "") o single 
33192  229 
o Pretty.mark Markup.hilite 
230 
else 

40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39361
diff
changeset

231 
(fn s => (Output.urgent_message s; if debug then tracing s else ())) 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

232 
o Pretty.string_of 
33192  233 
fun pprint_m f = () > not auto ? pprint o f 
234 
fun pprint_v f = () > verbose ? pprint o f 

235 
fun pprint_d f = () > debug ? pprint o f 

236 
val print = pprint o curry Pretty.blk 0 o pstrs 

39345  237 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

238 
val print_g = pprint o Pretty.str 
39345  239 
*) 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

240 
val print_m = pprint_m o K o plazy 
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

241 
val print_v = pprint_v o K o plazy 
33192  242 

243 
fun check_deadline () = 

41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

244 
if passed_deadline deadline then raise TimeLimit.TimeOut else () 
33192  245 

38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

246 
val assm_ts = if assms orelse auto then assm_ts else [] 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

247 
val _ = 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

248 
if step = 0 then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

249 
print_m (fn () => "Nitpicking formula...") 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

250 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

251 
pprint_m (fn () => Pretty.chunks ( 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

252 
pretties_for_formulas ctxt ("Nitpicking " ^ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

253 
(if i <> 1 orelse n <> 1 then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

254 
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

255 
else 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

256 
"goal")) [Logic.list_implies (assm_ts, orig_t)])) 
41278
8e1cde88aae6
added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents:
41052
diff
changeset

257 
val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S" 
8e1cde88aae6
added a timestamp to Nitpick in verbose mode for debugging purposes;
blanchet
parents:
41052
diff
changeset

258 
o Date.fromTimeLocal o Time.now) 
33192  259 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) 
260 
else orig_t 

41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

261 
val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

262 
val tfree_table = 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

263 
if merge_type_vars then merged_type_var_table_for_terms thy conj_ts 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

264 
else [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

265 
val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

266 
val neg_t = neg_t > merge_tfrees 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

267 
val assm_ts = assm_ts > map merge_tfrees 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

268 
val evals = evals > map merge_tfrees 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

269 
val preconstrs = preconstrs > map (apfst (Option.map merge_tfrees)) 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

270 
val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs 
33192  271 
val original_max_potential = max_potential 
272 
val original_max_genuine = max_genuine 

273 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

274 
val case_names = case_const_names ctxt stds 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

275 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of ctxt subst 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

276 
val def_tables = const_def_tables ctxt subst defs 
33192  277 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 
35335  278 
val simp_table = Unsynchronized.ref (const_simp_table ctxt subst) 
279 
val psimp_table = const_psimp_table ctxt subst 

35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

280 
val choice_spec_table = const_choice_spec_table ctxt subst 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

281 
val user_nondefs = 
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35711
diff
changeset

282 
user_nondefs > filter_out (is_choice_spec_axiom thy choice_spec_table) 
41791
01d722707a36
always unfold constant defitions marked with "nitpick_def"  to prevent unfolding, there's already "nitpick_simp"
blanchet
parents:
41789
diff
changeset

283 
val intro_table = inductive_intro_table ctxt subst def_tables 
33192  284 
val ground_thm_table = ground_theorem_table thy 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

285 
val ersatz_table = ersatz_table ctxt 
41007
75275c796b46
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout  this becomes necessary with the new, more powerful monotonicity calculus
blanchet
parents:
41001
diff
changeset

286 
val hol_ctxt as {wf_cache, ...} = 
33192  287 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

288 
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug, 
38209  289 
whacks = whacks, binary_ints = binary_ints, 
290 
destroy_constrs = destroy_constrs, specialize = specialize, 

41871
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

291 
star_linear_preds = star_linear_preds, total_consts = total_consts, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

292 
preconstrs = preconstrs, tac_timeout = tac_timeout, evals = evals, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

293 
case_names = case_names, def_tables = def_tables, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

294 
nondef_table = nondef_table, user_nondefs = user_nondefs, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

295 
simp_table = simp_table, psimp_table = psimp_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

296 
choice_spec_table = choice_spec_table, intro_table = intro_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

297 
ground_thm_table = ground_thm_table, ersatz_table = ersatz_table, 
394eef237bd1
lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
blanchet
parents:
41869
diff
changeset

298 
skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [], 
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

299 
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], 
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33568
diff
changeset

300 
constr_cache = Unsynchronized.ref []} 
41789
7c7b68b06c1a
don't distinguish between "fixes" and other free variables  this confuses users
blanchet
parents:
41772
diff
changeset

301 
val pseudo_frees = [] 
41869
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

302 
val real_frees = fold Term.add_frees conj_ts [] 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

303 
val _ = null (fold Term.add_tvars conj_ts []) orelse 
9e367f1c9570
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
blanchet
parents:
41868
diff
changeset

304 
error "Nitpick cannot handle goals with schematic type variables." 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

305 
val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms, 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

306 
no_poly_user_axioms, binarize) = 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

307 
preprocess_formulas hol_ctxt assm_ts neg_t 
33192  308 
val got_all_user_axioms = 
309 
got_all_mono_user_axioms andalso no_poly_user_axioms 

310 

311 
fun print_wf (x, (gfp, wf)) = 

312 
pprint (Pretty.blk (0, 

313 
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"") 

314 
@ Syntax.pretty_term ctxt (Const x) :: 

315 
pstrs (if wf then 

316 
"\" was proved wellfounded. Nitpick can compute it \ 

317 
\efficiently." 

318 
else 

319 
"\" could not be proved wellfounded. Nitpick might need to \ 

320 
\unroll it."))) 

321 
val _ = if verbose then List.app print_wf (!wf_cache) else () 

38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

322 
val das_wort_formula = if falsify then "Negated conjecture" else "Formula" 
33192  323 
val _ = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

324 
pprint_d (fn () => Pretty.chunks 
38171
5f2ea92319e0
fix soundness bug w.r.t. "Suc" with "binary_ints"
blanchet
parents:
38170
diff
changeset

325 
(pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

326 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

327 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

328 
(tl nondef_ts))) 
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

329 
val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts) 
33192  330 
handle TYPE (_, Ts, ts) => 
331 
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) 

332 

41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

333 
val nondef_us = nondef_ts > map (nut_from_term hol_ctxt Eq) 
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

334 
val def_us = def_ts > map (nut_from_term hol_ctxt DefEq) 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

335 
val preconstr_us = preconstr_ts > map (nut_from_term hol_ctxt Eq) 
41868
a4fb98eb0edf
make "preconstr" option more robust  shouldn't throw exceptions
blanchet
parents:
41858
diff
changeset

336 
val _ = List.app check_constr_nut preconstr_us 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

337 
val (free_names, const_names) = 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

338 
fold add_free_and_const_names (nondef_us @ def_us) ([], []) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

339 
val (sel_names, nonsel_names) = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

340 
List.partition (is_sel o nickname_of) const_names 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

341 
val sound_finitizes = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

342 
none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

343 
 _ => false) finitizes) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

344 
val standard = forall snd stds 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

345 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

346 
val _ = List.app (print_g o string_for_nut ctxt) (nondef_us @ def_us) 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

347 
*) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

348 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
34039
diff
changeset

349 
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

350 
fun monotonicity_message Ts extra = 
38188  351 
let val pretties = map (pretty_maybe_quote o pretty_for_type ctxt) Ts in 
352 
Pretty.blk (0, 

353 
pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @ 

354 
pretty_serial_commas "and" pretties @ 

355 
pstrs (" " ^ 

356 
(if none_true monos then 

357 
"passed the monotonicity test" 

358 
else 

359 
(if length pretties = 1 then "is" else "are") ^ " considered monotonic") ^ 

360 
". " ^ extra)) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

361 
end 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

362 
fun is_type_fundamentally_monotonic T = 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

363 
(is_datatype ctxt stds T andalso not (is_quot_type ctxt T) andalso 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

364 
(not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse 
38240
a44d108a8d39
local versions of Nitpick.register_xxx functions
blanchet
parents:
38214
diff
changeset

365 
is_number_type ctxt T orelse is_bit_type T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

366 
fun is_type_actually_monotonic T = 
41001
11715564e2ad
removed old baggage from monotonicity calculus  the "calculus" option didn't really work anyway because of onthefly simplifications
blanchet
parents:
40993
diff
changeset

367 
formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

368 
fun is_type_kind_of_monotonic T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

369 
case triple_lookup (type_match thy) monos T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

370 
SOME (SOME false) => false 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

371 
 _ => is_type_actually_monotonic T 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

372 
fun is_type_monotonic T = 
33192  373 
unique_scope orelse 
374 
case triple_lookup (type_match thy) monos T of 

375 
SOME (SOME b) => b 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

376 
 _ => is_type_fundamentally_monotonic T orelse 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

377 
is_type_actually_monotonic T 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

378 
fun is_deep_datatype_finitizable T = 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

379 
triple_lookup (type_match thy) finitizes T = SOME (SOME true) 
41052
3db267a01c1d
remove the "fin_fun" optimization in Nitpick  it was always a hack and didn't help much
blanchet
parents:
41051
diff
changeset

380 
fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) = 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

381 
is_type_kind_of_monotonic T 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

382 
 is_shallow_datatype_finitizable T = 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

383 
case triple_lookup (type_match thy) finitizes T of 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

384 
SOME (SOME b) => b 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

385 
 _ => is_type_kind_of_monotonic T 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

386 
fun is_datatype_deep T = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

387 
not standard orelse T = nat_T orelse is_word_type T orelse 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

388 
exists (curry (op =) T o domain_type o type_of) sel_names 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

389 
val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) 
35408  390 
> sort Term_Ord.typ_ord 
38214  391 
val _ = 
392 
if verbose andalso binary_ints = SOME true andalso 

393 
exists (member (op =) [nat_T, int_T]) all_Ts then 

394 
print_v (K "The option \"binary_ints\" will be ignored because of the \ 

395 
\presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \ 

396 
\in the problem or because of the \"non_std\" option.") 

397 
else 

398 
() 

399 
val _ = 

400 
if not auto andalso 

401 
exists (fn Type (@{type_name Datatype.node}, _) => true  _ => false) 

402 
all_Ts then 

403 
print_m (K ("Warning: The problem involves directly or indirectly the \ 

404 
\internal type " ^ quote @{type_name Datatype.node} ^ 

405 
". This type is very Nitpickunfriendly, and its presence \ 

39361  406 
\usually indicates either a failure of abstraction or a \ 
407 
\quirk in Nitpick.")) 

38214  408 
else 
409 
() 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

410 
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts 
33192  411 
val _ = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

412 
if verbose andalso not unique_scope then 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset

413 
case filter_out is_type_fundamentally_monotonic mono_Ts of 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

414 
[] => () 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

415 
 interesting_mono_Ts => 
38188  416 
pprint_v (K (monotonicity_message interesting_mono_Ts 
417 
"Nitpick might be able to skip some scopes.")) 

33192  418 
else 
419 
() 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

420 
val (deep_dataTs, shallow_dataTs) = 
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

421 
all_Ts > filter (is_datatype ctxt stds) 
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37213
diff
changeset

422 
> List.partition is_datatype_deep 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

423 
val finitizable_dataTs = 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

424 
(deep_dataTs > filter_out (is_finite_type hol_ctxt) 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

425 
> filter is_deep_datatype_finitizable) @ 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

426 
(shallow_dataTs > filter_out (is_finite_type hol_ctxt) 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

427 
> filter is_shallow_datatype_finitizable) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

428 
val _ = 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

429 
if verbose andalso not (null finitizable_dataTs) then 
38188  430 
pprint_v (K (monotonicity_message finitizable_dataTs 
431 
"Nitpick can use a more precise finite encoding.")) 

35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

432 
else 
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset

433 
() 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

434 
(* This detection code is an ugly hack. Fortunately, it is used only to 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

435 
provide a hint to the user. *) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

436 
fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) = 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

437 
not (null fixes) andalso 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

438 
exists (String.isSuffix ".hyps" o fst) assumes andalso 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

439 
exists (exists (curry (op =) name o shortest_name o fst) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

440 
o datatype_constrs hol_ctxt) deep_dataTs 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

441 
val likely_in_struct_induct_step = 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

442 
exists is_struct_induct_step (ProofContext.cases_of ctxt) 
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

443 
val _ = if standard andalso likely_in_struct_induct_step then 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

444 
pprint_m (fn () => Pretty.blk (0, 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

445 
pstrs "Hint: To check that the induction hypothesis is \ 
35177  446 
\general enough, try this command: " @ 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

447 
[Pretty.mark Markup.sendback (Pretty.blk (0, 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

448 
pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

449 
else 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

450 
() 
33192  451 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

452 
val _ = print_g "Monotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

453 
val _ = List.app (print_g o string_for_type ctxt) mono_Ts 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

454 
val _ = print_g "Nonmonotonic types:" 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

455 
val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts 
33192  456 
*) 
457 

36384  458 
val incremental = Int.max (max_potential, max_genuine) >= 2 
459 
val actual_sat_solver = 

33192  460 
if sat_solver <> "smart" then 
36384  461 
if incremental andalso 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

462 
not (member (op =) (Kodkod_SAT.configured_sat_solvers true) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

463 
sat_solver) then 
33192  464 
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ 
465 
\be used instead of " ^ quote sat_solver ^ ".")); 

466 
"SAT4J") 

467 
else 

468 
sat_solver 

469 
else 

36384  470 
Kodkod_SAT.smart_sat_solver_name incremental 
33192  471 
val _ = 
472 
if sat_solver = "smart" then 

36384  473 
print_v (fn () => 
474 
"Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^ 

475 
(if incremental then " incremental " else " ") ^ 

476 
"solvers are configured: " ^ 

477 
commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".") 

33192  478 
else 
479 
() 

480 

481 
val too_big_scopes = Unsynchronized.ref [] 

482 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

483 
fun problem_for_scope unsound 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

484 
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) = 
33192  485 
let 
486 
val _ = not (exists (fn other => scope_less_eq other scope) 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

487 
(!too_big_scopes)) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

488 
raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\ 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

489 
\problem_for_scope", "too large scope") 
33192  490 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

491 
val _ = print_g "Offsets:" 
33192  492 
val _ = List.app (fn (T, j0) => 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

493 
print_g (string_for_type ctxt T ^ " = " ^ 
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

494 
string_of_int j0)) 
33192  495 
(Typtab.dest ofs) 
496 
*) 

41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

497 
val effective_total_consts = 
41856  498 
case total_consts of 
499 
SOME b => b 

500 
 NONE => forall (is_exact_type datatypes true) all_Ts 

33192  501 
val main_j0 = offset_of_type ofs bool_T 
502 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

503 
val (int_card, int_j0) = spec_of_type scope int_T 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

504 
val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

505 
raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope", 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

506 
"bad offsets") 
33192  507 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 
508 
val (free_names, rep_table) = 

38170  509 
choose_reps_for_free_vars scope pseudo_frees free_names 
510 
NameTable.empty 

33192  511 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 
38170  512 
val (nonsel_names, rep_table) = 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

513 
choose_reps_for_consts scope effective_total_consts nonsel_names 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

514 
rep_table 
38182  515 
val (guiltiest_party, min_highest_arity) = 
516 
NameTable.fold (fn (name, R) => fn (s, n) => 

517 
let val n' = arity_of_rep R in 

518 
if n' > n then (nickname_of name, n') else (s, n) 

519 
end) rep_table ("", 1) 

33192  520 
val min_univ_card = 
36384  521 
NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table 
34126  522 
(univ_card nat_card int_card main_j0 [] KK.True) 
38182  523 
val _ = check_arity guiltiest_party min_univ_card min_highest_arity 
33192  524 

41802  525 
val def_us = 
526 
def_us > map (choose_reps_in_nut scope unsound rep_table true) 

527 
val nondef_us = 

528 
nondef_us > map (choose_reps_in_nut scope unsound rep_table false) 

41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

529 
val preconstr_us = 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

530 
preconstr_us > map (choose_reps_in_nut scope unsound rep_table false) 
33745  531 
(* 
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
36126
diff
changeset

532 
val _ = List.app (print_g o string_for_nut ctxt) 
33192  533 
(free_names @ sel_names @ nonsel_names @ 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

534 
nondef_us @ def_us) 
33745  535 
*) 
33192  536 
val (free_rels, pool, rel_table) = 
537 
rename_free_vars free_names initial_pool NameTable.empty 

538 
val (sel_rels, pool, rel_table) = 

539 
rename_free_vars sel_names pool rel_table 

540 
val (other_rels, pool, rel_table) = 

541 
rename_free_vars nonsel_names pool rel_table 

41802  542 
val nondef_us = nondef_us > map (rename_vars_in_nut pool rel_table) 
543 
val def_us = def_us > map (rename_vars_in_nut pool rel_table) 

41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

544 
val preconstr_us = 
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

545 
preconstr_us > map (rename_vars_in_nut pool rel_table) 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

546 
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

547 
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

548 
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

549 
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ 
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
36913
diff
changeset

550 
Print_Mode.setmp [] multiline_string_for_scope scope 
34998  551 
val kodkod_sat_solver = 
36384  552 
Kodkod_SAT.sat_solver_spec actual_sat_solver > snd 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

553 
val bit_width = if bits = 0 then 16 else bits + 1 
36384  554 
val delay = 
555 
if unsound then 

556 
Option.map (fn time => Time. (time, Time.now ())) deadline 

557 
> unsound_delay_for_timeout 

558 
else 

559 
0 

560 
val settings = [("solver", commas_quote kodkod_sat_solver), 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

561 
("bit_width", string_of_int bit_width), 
38124  562 
("symmetry_breaking", string_of_int kodkod_sym_break), 
36386
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

563 
("sharing", "3"), 
2132f15b366f
Fruhjahrsputz: remove three mostly useless Nitpick options
blanchet
parents:
36385
diff
changeset

564 
("flatten", "false"), 
33192  565 
("delay", signed_string_of_int delay)] 
566 
val plain_rels = free_rels @ other_rels 

567 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

568 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

569 
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

570 
val dtype_axioms = 
41803
ef13e3b7cbaf
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
blanchet
parents:
41802
diff
changeset

571 
declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us 
41801
ed77524f3429
first steps in implementing "fix_datatype_vals" optimization
blanchet
parents:
41793
diff
changeset

572 
datatype_sym_break bits ofs kk rel_table datatypes 
33192  573 
val declarative_axioms = plain_axioms @ dtype_axioms 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

574 
val univ_card = Int.max (univ_card nat_card int_card main_j0 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

575 
(plain_bounds @ sel_bounds) formula, 
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

576 
main_j0 > bits > 0 ? Integer.add (bits + 1)) 
38126  577 
val (built_in_bounds, built_in_axioms) = 
39345  578 
bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card 
579 
nat_card int_card main_j0 (formula :: declarative_axioms) 

33192  580 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 
581 
> not debug ? merge_bounds 

38126  582 
val axioms = built_in_axioms @ declarative_axioms 
33192  583 
val highest_arity = 
584 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

38126  585 
val formula = fold_rev s_and axioms formula 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

586 
val _ = if bits = 0 then () else check_bits bits formula 
34126  587 
val _ = if formula = KK.False then () 
38182  588 
else check_arity "" univ_card highest_arity 
33192  589 
in 
590 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

591 
tuple_assigns = [], bounds = bounds, 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

592 
int_bounds = if bits = 0 then sequential_int_bounds univ_card 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

593 
else pow_of_two_int_bounds bits main_j0, 
33192  594 
expr_assigns = [], formula = formula}, 
595 
{free_names = free_names, sel_names = sel_names, 

596 
nonsel_names = nonsel_names, rel_table = rel_table, 

35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

597 
unsound = unsound, scope = scope}) 
33192  598 
end 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

599 
handle TOO_LARGE (loc, msg) => 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

600 
if loc = "Nitpick_Kodkod.check_arity" andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34935
diff
changeset

601 
not (Typtab.is_empty ofs) then 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

602 
problem_for_scope unsound 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

603 
{hol_ctxt = hol_ctxt, binarize = binarize, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

604 
card_assigns = card_assigns, bits = bits, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

605 
bisim_depth = bisim_depth, datatypes = datatypes, 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

606 
ofs = Typtab.empty} 
33192  607 
else if loc = "Nitpick.pick_them_nits_in_term.\ 
608 
\problem_for_scope" then 

609 
NONE 

610 
else 

611 
(Unsynchronized.change too_big_scopes (cons scope); 

612 
print_v (fn () => ("Limit reached: " ^ msg ^ 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

613 
". Skipping " ^ (if unsound then "potential" 
33192  614 
else "genuine") ^ 
615 
" component of scope.")); 

616 
NONE) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

617 
 TOO_SMALL (_, msg) => 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

618 
(print_v (fn () => ("Limit reached: " ^ msg ^ 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

619 
". Skipping " ^ (if unsound then "potential" 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

620 
else "genuine") ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

621 
" component of scope.")); 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34123
diff
changeset

622 
NONE) 
33192  623 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

624 
val das_wort_model = 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

625 
(if falsify then "counterexample" else "model") 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

626 
> not standard ? prefix "nonstandard " 
33192  627 

628 
val scopes = Unsynchronized.ref [] 

629 
val generated_scopes = Unsynchronized.ref [] 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

630 
val generated_problems = Unsynchronized.ref ([] : rich_problem list) 
33192  631 
val checked_problems = Unsynchronized.ref (SOME []) 
632 
val met_potential = Unsynchronized.ref 0 

633 

634 
fun update_checked_problems problems = 

635 
List.app (Unsynchronized.change checked_problems o Option.map o cons 

636 
o nth problems) 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

637 
fun show_kodkod_warning "" = () 
35334
b83b9f2a4b92
show Kodkod warning message even in nonverbose mode
blanchet
parents:
35333
diff
changeset

638 
 show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".") 
33192  639 

640 
fun print_and_check_model genuine bounds 

641 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

642 
: problem_extension) = 

643 
let 

644 
val (reconstructed_model, codatatypes_ok) = 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36389
diff
changeset

645 
reconstruct_hol_model {show_datatypes = show_datatypes, 
33192  646 
show_consts = show_consts} 
38170  647 
scope formats atomss real_frees pseudo_frees free_names sel_names 
648 
nonsel_names rel_table bounds 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

649 
val genuine_means_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

650 
got_all_user_axioms andalso none_true wfs andalso 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

651 
sound_finitizes andalso total_consts <> SOME true andalso 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

652 
codatatypes_ok 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

653 
fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) 
33192  654 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

655 
(pprint (Pretty.chunks 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

656 
[Pretty.blk (0, 
40223  657 
(pstrs ((if auto then "Auto " else "") ^ "Nitpick found a" ^ 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

658 
(if not genuine then " potential " 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

659 
else if genuine_means_genuine then " " 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

660 
else " quasi genuine ") ^ das_wort_model) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

661 
(case pretties_for_scope scope verbose of 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

662 
[] => [] 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

663 
 pretties => pstrs " for " @ pretties) @ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

664 
[Pretty.str ":\n"])), 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

665 
Pretty.indent indent_size reconstructed_model]); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

666 
if genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

667 
(if check_genuine andalso standard then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

668 
case prove_hol_model scope tac_timeout free_names sel_names 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

669 
rel_table bounds (assms_prop ()) of 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

670 
SOME true => 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

671 
print ("Confirmation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

672 
das_wort_model ^ " is really genuine.") 
33192  673 
 SOME false => 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

674 
if genuine_means_genuine then 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

675 
error ("A supposedly genuine " ^ das_wort_model ^ " was \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

676 
\shown to be spurious by \"auto\".\nThis should never \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

677 
\happen.\nPlease send a bug report to blanchet\ 
33192  678 
\te@in.tum.de.") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

679 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

680 
print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

681 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

682 
 NONE => print "No confirmation by \"auto\"." 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

683 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

684 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

685 
if not standard andalso likely_in_struct_induct_step then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

686 
print "The existence of a nonstandard model suggests that the \ 
36126  687 
\induction hypothesis is not general enough or may even be \ 
688 
\wrong. See the Nitpick manual's \"Inductive Properties\" \ 

689 
\section for details (\"isabelle doc nitpick\")." 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

690 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

691 
(); 
41048
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

692 
if has_lonely_bool_var orig_t then 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

693 
print "Hint: Maybe you forgot a colon after the lemma's name?" 
d5ebe94248ad
added a hint when the user obviously just forgot a colon after the lemma's name
blanchet
parents:
41007
diff
changeset

694 
else if has_syntactic_sorts orig_t then 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

695 
print "Hint: Maybe you forgot a type constraint?" 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

696 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

697 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

698 
if not genuine_means_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

699 
if no_poly_user_axioms then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

700 
let 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

701 
val options = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

702 
[] > not got_all_mono_user_axioms 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

703 
? cons ("user_axioms", "\"true\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

704 
> not (none_true wfs) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

705 
? cons ("wf", "\"smart\" or \"false\"") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

706 
> not sound_finitizes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

707 
? cons ("finitize", "\"smart\" or \"false\"") 
41858
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

708 
> total_consts = SOME true 
37ce158d6266
if "total_consts" is set, report cex's as quasigenuine
blanchet
parents:
41856
diff
changeset

709 
? cons ("total_consts", "\"smart\" or \"false\"") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

710 
> not codatatypes_ok 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

711 
? cons ("bisim_depth", "a nonnegative value") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

712 
val ss = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

713 
map (fn (name, value) => quote name ^ " set to " ^ value) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

714 
options 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

715 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

716 
print ("Try again with " ^ 
41872  717 
space_implode " " (serial_commas "and" ss) ^ 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

718 
" to confirm that the " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

719 
" is genuine.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

720 
end 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

721 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

722 
print ("Nitpick is unable to guarantee the authenticity of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

723 
\the " ^ das_wort_model ^ " in the presence of \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

724 
\polymorphic axioms.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

725 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

726 
(); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

727 
NONE) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

728 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

729 
if not genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

730 
(Unsynchronized.inc met_potential; 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

731 
if check_potential then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

732 
let 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

733 
val status = prove_hol_model scope tac_timeout free_names 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

734 
sel_names rel_table bounds 
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

735 
(assms_prop ()) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

736 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

737 
(case status of 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

738 
SOME true => print ("Confirmation by \"auto\": The \ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

739 
\above " ^ das_wort_model ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

740 
" is genuine.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

741 
 SOME false => print ("Refutation by \"auto\": The above " ^ 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

742 
das_wort_model ^ " is spurious.") 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

743 
 NONE => print "No confirmation by \"auto\"."); 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

744 
status 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

745 
end 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

746 
else 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

747 
NONE) 
33192  748 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

749 
NONE) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

750 
> pair genuine_means_genuine 
33192  751 
end 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

752 
fun solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

753 
donno) first_time problems = 
33192  754 
let 
755 
val max_potential = Int.max (0, max_potential) 

756 
val max_genuine = Int.max (0, max_genuine) 

757 
fun print_and_check genuine (j, bounds) = 

758 
print_and_check_model genuine bounds (snd (nth problems j)) 

759 
val max_solutions = max_potential + max_genuine 

36384  760 
> not incremental ? Integer.min 1 
33192  761 
in 
762 
if max_solutions <= 0 then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

763 
(found_really_genuine, 0, 0, donno) 
33192  764 
else 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

765 
case KK.solve_any_problem debug overlord deadline max_threads 
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
41791
diff
changeset

766 
max_solutions (map fst problems) of 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

767 
KK.JavaNotInstalled => 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

768 
(print_m install_java_message; 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

769 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

770 
 KK.JavaTooOld => 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

771 
(print_m install_java_message; 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38240
diff
changeset

772 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

773 
 KK.KodkodiNotInstalled => 
33568
532b915afa14
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet
parents:
33566
diff
changeset

774 
(print_m install_kodkodi_message; 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

775 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

776 
 KK.Normal ([], unsat_js, s) => 
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

777 
(update_checked_problems problems unsat_js; show_kodkod_warning s; 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

778 
(found_really_genuine, max_potential, max_genuine, donno)) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

779 
 KK.Normal (sat_ps, unsat_js, s) => 
33192  780 
let 
781 
val (lib_ps, con_ps) = 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

782 
List.partition (#unsound o snd o nth problems o fst) sat_ps 
33192  783 
in 
784 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35280
diff
changeset

785 
show_kodkod_warning s; 
33192  786 
if null con_ps then 
787 
let 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

788 
val genuine_codes = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

789 
lib_ps > take max_potential 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

790 
> map (print_and_check false) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

791 
> filter (curry (op =) (SOME true) o snd) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

792 
val found_really_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

793 
found_really_genuine orelse exists fst genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

794 
val num_genuine = length genuine_codes 
33192  795 
val max_genuine = max_genuine  num_genuine 
796 
val max_potential = max_potential 

797 
 (length lib_ps  num_genuine) 

798 
in 

799 
if max_genuine <= 0 then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

800 
(found_really_genuine, 0, 0, donno) 
33192  801 
else 
802 
let 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

803 
(* "co_js" is the list of sound problems whose unsound 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

804 
pendants couldn't be satisfied and hence that most 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

805 
probably can't be satisfied themselves. *) 
33192  806 
val co_js = 
807 
map (fn j => j  1) unsat_js 

808 
> filter (fn j => 

809 
j >= 0 andalso 

810 
scopes_equivalent 

35814  811 
(#scope (snd (nth problems j)), 
812 
#scope (snd (nth problems (j + 1))))) 

33192  813 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 
814 
unsat_js @ co_js) 

815 
val problems = 

816 
problems > filter_out_indices bye_js 

817 
> max_potential <= 0 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

818 
? filter_out (#unsound o snd) 
33192  819 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

820 
solve_any_problem (found_really_genuine, max_potential, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

821 
max_genuine, donno) false problems 
33192  822 
end 
823 
end 

824 
else 

825 
let 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

826 
val genuine_codes = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

827 
con_ps > take max_genuine 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

828 
> map (print_and_check true) 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

829 
val max_genuine = max_genuine  length genuine_codes 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

830 
val found_really_genuine = 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

831 
found_really_genuine orelse exists fst genuine_codes 
33192  832 
in 
833 
if max_genuine <= 0 orelse not first_time then 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

834 
(found_really_genuine, 0, max_genuine, donno) 
33192  835 
else 
836 
let 

837 
val bye_js = sort_distinct int_ord 

838 
(map fst sat_ps @ unsat_js) 

839 
val problems = 

840 
problems > filter_out_indices bye_js 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

841 
> filter_out (#unsound o snd) 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

842 
in 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

843 
solve_any_problem (found_really_genuine, 0, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

844 
donno) false problems 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

845 
end 
33192  846 
end 
847 
end 

34126  848 
 KK.TimedOut unsat_js => 
33192  849 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 
34126  850 
 KK.Error (s, unsat_js) => 
33192  851 
(update_checked_problems problems unsat_js; 
852 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

853 
(found_really_genuine, max_potential, max_genuine, donno + 1)) 
33192  854 
end 
855 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

856 
fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

857 
donno) = 
33192  858 
let 
859 
val _ = 

860 
if null scopes then 

861 
print_m (K "The scope specification is inconsistent.") 

862 
else if verbose then 

863 
pprint (Pretty.chunks 

864 
[Pretty.blk (0, 

865 
pstrs ((if n > 1 then 

866 
"Batch " ^ string_of_int (j + 1) ^ " of " ^ 

867 
signed_string_of_int n ^ ": " 

868 
else 

869 
"") ^ 

870 
"Trying " ^ string_of_int (length scopes) ^ 

871 
" scope" ^ plural_s_for_list scopes ^ ":")), 

872 
Pretty.indent indent_size 

873 
(Pretty.chunks (map2 

874 
(fn j => fn scope => 

875 
Pretty.block ( 

876 
(case pretties_for_scope scope true of 

877 
[] => [Pretty.str "Empty"] 

878 
 pretties => pretties) @ 

879 
[Pretty.str (if j = 1 then "." else ";")])) 

880 
(length scopes downto 1) scopes))]) 

881 
else 

882 
() 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

883 
fun add_problem_for_scope (scope, unsound) (problems, donno) = 
33192  884 
(check_deadline (); 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

885 
case problem_for_scope unsound scope of 
33192  886 
SOME problem => 
887 
(problems 

888 
> (null problems orelse 

35814  889 
not (KK.problems_equivalent (fst problem, fst (hd problems)))) 
33192  890 
? cons problem, donno) 
891 
 NONE => (problems, donno + 1)) 

892 
val (problems, donno) = 

893 
fold add_problem_for_scope 

894 
(map_product pair scopes 

895 
((if max_genuine > 0 then [false] else []) @ 

896 
(if max_potential > 0 then [true] else []))) 

897 
([], donno) 

898 
val _ = Unsynchronized.change generated_problems (append problems) 

899 
val _ = Unsynchronized.change generated_scopes (append scopes) 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

900 
val _ = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

901 
if j + 1 = n then 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

902 
let 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

903 
val (unsound_problems, sound_problems) = 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

904 
List.partition (#unsound o snd) (!generated_problems) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

905 
in 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

906 
if not (null sound_problems) andalso 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

907 
forall (KK.is_problem_trivially_false o fst) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

908 
sound_problems then 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

909 
print_m (fn () => 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

910 
"Warning: The conjecture either trivially holds for the \ 
35384  911 
\given scopes or lies outside Nitpick's supported \ 
912 
\fragment." ^ 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

913 
(if exists (not o KK.is_problem_trivially_false o fst) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

914 
unsound_problems then 
36913  915 
" Only potential " ^ das_wort_model ^ "s may be found." 
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

916 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

917 
"")) 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

918 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

919 
() 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

920 
end 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

921 
else 
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

922 
() 
33192  923 
in 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

924 
solve_any_problem (found_really_genuine, max_potential, max_genuine, 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

925 
donno) true (rev problems) 
33192  926 
end 
927 

928 
fun scope_count (problems : rich_problem list) scope = 

35814  929 
length (filter (curry scopes_equivalent scope o #scope o snd) problems) 
33192  930 
fun excipit did_so_and_so = 
931 
let 

932 
val do_filter = 

35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35183
diff
changeset

933 
if !met_potential = max_potential then filter_out (#unsound o snd) 
33192  934 
else I 
935 
val total = length (!scopes) 

936 
val unsat = 

937 
fold (fn scope => 

938 
case scope_count (do_filter (!generated_problems)) scope of 

939 
0 => I 

940 
 n => 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

941 
scope_count (do_filter (these (!checked_problems))) 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

942 
scope = n 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

943 
? Integer.add 1) (!generated_scopes) 0 
33192  944 
in 
945 
"Nitpick " ^ did_so_and_so ^ 

946 
(if is_some (!checked_problems) andalso total > 0 then 

39361  947 
" " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope" 
948 
^ plural_s total 

33192  949 
else 
950 
"") ^ "." 

951 
end 

952 

37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

953 
val (skipped, the_scopes) = 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

954 
all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

955 
bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

956 
finitizable_dataTs 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

957 
val _ = if skipped > 0 then 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

958 
print_m (fn () => "Too many scopes. Skipping " ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

959 
string_of_int skipped ^ " scope" ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

960 
plural_s skipped ^ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

961 
". (Consider using \"mono\" or \ 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

962 
\\"merge_type_vars\" to prevent this.)") 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

963 
else 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

964 
() 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

965 
val _ = scopes := the_scopes 
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

966 

35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

967 
fun run_batches _ _ [] 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

968 
(found_really_genuine, max_potential, max_genuine, donno) = 
33192  969 
if donno > 0 andalso max_genuine > 0 then 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

970 
(print_m (fn () => excipit "checked"); "unknown") 
33192  971 
else if max_genuine = original_max_genuine then 
972 
if max_potential = original_max_potential then 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

973 
(print_m (fn () => 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

974 
"Nitpick found no " ^ das_wort_model ^ "." ^ 
35183
8580ba651489
reintroduce structural induction hint in Nitpick
blanchet
parents:
35181
diff
changeset

975 
(if not standard andalso likely_in_struct_induct_step then 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

976 
" This suggests that the induction hypothesis might be \ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

977 
\general enough to prove this subgoal." 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

978 
else 
37704
c6161bee8486
adapt Nitpick to "prod_case" and "*" > "sum" renaming;
blanchet
parents:
37497
diff
changeset

979 
"")); if skipped > 0 then "unknown" else "none") 
33192  980 
else 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

981 
(print_m (fn () => 
38123
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

982 
excipit ("could not find a" ^ 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

983 
(if max_genuine = 1 then 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

984 
" better " ^ das_wort_model ^ "." 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

985 
else 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

986 
"ny better " ^ das_wort_model ^ "s.") ^ 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

987 
" It checked")); 
36f649db4a6c
clarify Nitpick's output in case of a potential counterexample
blanchet
parents:
37928
diff
changeset

988 
"potential") 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

989 
else if found_really_genuine then 
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

990 
"genuine" 
33192  991 
else 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

992 
"quasi_genuine" 
33192  993 
 run_batches j n (batch :: batches) z = 
35671
ed2c3830d881
improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = 1"
blanchet
parents:
35665
diff
changeset

994 
let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in 
33192  995 
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z 
996 
end 

997 

998 
val batches = batch_list batch_size (!scopes) 

999 
val outcome_code = 

40411
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

1000 
run_batches 0 (length batches) batches 
36b7ed41ca9f
removed explicit "Interrupt" handling for conformity with async model  unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet
parents:
40381
diff
changeset

1001 
(false, max_potential, max_genuine, 0) 
33192  1002 
handle TimeLimit.TimeOut => 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35671
diff
changeset

1003 
(print_m (fn () => excipit "ran out of time after checking"); 
33192  1004 
if !met_potential > 0 then "potential" else "unknown") 
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1005 
val _ = print_v (fn () => 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1006 
"Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ 
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40223
diff
changeset

1007 
".") 
33192  1008 
in (outcome_code, !state_ref) end 
1009 

41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1010 
(* Give the inner timeout a chance. *) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1011 
val timeout_bonus = seconds 1.0 
41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1012 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1013 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

1014 
step subst assm_ts orig_t = 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1015 
let val print_m = if auto then K () else Output.urgent_message in 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1016 
if getenv "KODKODI" = "" then 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1017 
(* The "expect" argument is deliberately ignored if Kodkodi is missing so 
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1018 
that the "Nitpick_Examples" can be processed on any machine. *) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1019 
(print_m (Pretty.string_of (plazy install_kodkodi_message)); 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1020 
("no_kodkodi", state)) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1021 
else 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1022 
let 
37497
71fdbffe3275
distinguish between "unknown" and "no Kodkodi installed" errors
blanchet
parents:
37273
diff
changeset

1023 
val unknown_outcome = ("unknown", state) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1024 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1025 
val outcome as (outcome_code, _) = 
41051
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1026 
time_limit (if debug orelse is_none timeout then NONE 
2ed1b971fc20
give the inner timeout mechanism a chance, since it gives more precise information to the user
blanchet
parents:
41048
diff
changeset

1027 
else SOME (Time.+ (the timeout, timeout_bonus))) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1028 
(pick_them_nits_in_term deadline state params auto i n step subst 
38169
b51784515471
optimize local "def"s by treating them as definitions
blanchet
parents:
38126
diff
changeset

1029 
assm_ts) orig_t 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1030 
handle TOO_LARGE (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1031 
(print_m ("Limit reached: " ^ details ^ "."); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1032 
 TOO_SMALL (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1033 
(print_m ("Limit reached: " ^ details ^ "."); unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1034 
 Kodkod.SYNTAX (_, details) => 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1035 
(print_m ("Malformed Kodkodi output: " ^ details ^ "."); 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1036 
unknown_outcome) 
41772
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1037 
 TimeLimit.TimeOut => 
27d4c768cf20
make Nitpick's timeout mechanism somewhat more reliable/friendly;
blanchet
parents:
41278
diff
changeset

1038 
(print_m "Nitpick ran out of time."; unknown_outcome) 
37213
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1039 
in 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1040 
if expect = "" orelse outcome_code = expect then outcome 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1041 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1042 
end 
efcad7594872
fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
blanchet
parents:
37146
diff
changeset

1043 
end 
33192  1044 

35335  1045 
fun is_fixed_equation fixes 
1046 
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) = 

1047 
member (op =) fixes s 

1048 
 is_fixed_equation _ _ = false 

1049 
fun extract_fixed_frees ctxt (assms, t) = 

1050 
let 

1051 
val fixes = Variable.fixes_of ctxt > map snd 

1052 
val (subst, other_assms) = 

1053 
List.partition (is_fixed_equation fixes) assms 

1054 
>> map Logic.dest_equals 

1055 
in (subst, other_assms, subst_atomic subst t) end 

1056 

34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1057 
fun pick_nits_in_subgoal state params auto i step = 
33192  1058 
let 
1059 
val ctxt = Proof.context_of state 

33292  1060 
val t = state > Proof.raw_goal > #goal > prop_of 
33192  1061 
in 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1062 
case Logic.count_prems t of 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39361
diff
changeset

1063 
0 => (Output.urgent_message "No subgoal!"; ("none", state)) 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34938
diff
changeset

1064 
 n => 
33192  1065 
let 
36406  1066 
val t = Logic.goal_params t i > fst 
33192  1067 
val assms = map term_of (Assumption.all_assms_of ctxt) 
35335  1068 
val (subst, assms, t) = extract_fixed_frees ctxt (assms, t) 
1069 
in pick_nits_in_term state params auto i n step subst assms t end 

33192  1070 
end 
1071 

1072 
end; 