author  blanchet 
Wed, 02 Oct 2013 22:54:42 +0200  
changeset 54041  227908156cd2 
parent 52732  b4da1f2ec73f 
permissions  rwrr 
36898  1 
(* Title: HOL/Tools/SMT/smt_solver.ML 
2 
Author: Sascha Boehme, TU Muenchen 

3 

4 
SMT solvers registry and SMT tactic. 

5 
*) 

6 

7 
signature SMT_SOLVER = 

8 
sig 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

9 
(*configuration*) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

10 
datatype outcome = Unsat  Sat  Unknown 
36898  11 
type solver_config = { 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

12 
name: string, 
48043
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47701
diff
changeset

13 
class: Proof.context > SMT_Utils.class, 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

14 
avail: unit > bool, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

15 
command: unit > string list, 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

16 
options: Proof.context > string list, 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

17 
default_max_relevant: int, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

18 
supports_filter: bool, 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

19 
outcome: string > string list > outcome * string list, 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

20 
cex_parser: (Proof.context > SMT_Translate.recon > string list > 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

21 
term list * term list) option, 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

22 
reconstruct: (Proof.context > SMT_Translate.recon > string list > 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

23 
int list * thm) option } 
36898  24 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

25 
(*registry*) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

26 
val add_solver: solver_config > theory > theory 
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset

27 
val solver_name_of: Proof.context > string 
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset

28 
val available_solvers_of: Proof.context > string list 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

29 
val apply_solver: Proof.context > (int * (int option * thm)) list > 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

30 
int list * thm 
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

31 
val default_max_relevant: Proof.context > string > int 
36898  32 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

33 
(*filter*) 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

34 
type 'a smt_filter_data = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

35 
('a * thm) list * ((int * thm) list * Proof.context) 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset

36 
val smt_filter_preprocess: Proof.context > thm list > thm > 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

37 
('a * (int option * thm)) list > int > 'a smt_filter_data 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

38 
val smt_filter_apply: Time.time > 'a smt_filter_data > 
41239  39 
{outcome: SMT_Failure.failure option, used_facts: ('a * thm) list} 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

40 

36898  41 
(*tactic*) 
46464  42 
val smt_tac: Proof.context > thm list > int > tactic 
43 
val smt_tac': Proof.context > thm list > int > tactic 

36898  44 
end 
45 

46 
structure SMT_Solver: SMT_SOLVER = 

47 
struct 

48 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

49 

36898  50 
(* interface to external solvers *) 
51 

52 
local 

53 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

54 
fun make_cmd command options problem_path proof_path = space_implode " " ( 
48532
c0f44941e674
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers  no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents:
48043
diff
changeset

55 
"(exec 2>&1;" :: map File.shell_quote (command () @ options) @ 
c0f44941e674
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers  no need to additionally print scores of warnings (cf. 4b0daca2bf88)
blanchet
parents:
48043
diff
changeset

56 
[File.shell_path problem_path, ")", ">", File.shell_path proof_path]) 
36898  57 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

58 
fun trace_and ctxt msg f x = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

59 
let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

60 
in f x end 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

61 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

62 
fun run ctxt name mk_cmd input = 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

63 
(case SMT_Config.certificates_of ctxt of 
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset

64 
NONE => 
46743
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

65 
if not (SMT_Config.is_available ctxt name) then 
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

66 
error ("The SMT solver " ^ quote name ^ " is not installed.") 
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

67 
else if Config.get ctxt SMT_Config.debug_files = "" then 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

68 
trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

69 
(Cache_IO.run mk_cmd) input 
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset

70 
else 
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset

71 
let 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

72 
val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) 
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset

73 
val in_path = Path.ext "smt_in" base_path 
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40561
diff
changeset

74 
val out_path = Path.ext "smt_out" base_path 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

75 
in Cache_IO.raw_run mk_cmd input in_path out_path end 
36898  76 
 SOME certs => 
77 
(case Cache_IO.lookup certs input of 

78 
(NONE, key) => 

47152
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46743
diff
changeset

79 
if Config.get ctxt SMT_Config.read_only_certificates then 
446cfc760ccf
renamed "smt_fixed" to "smt_read_only_certificates"
blanchet
parents:
46743
diff
changeset

80 
error ("Bad certificate cache: missing certificate") 
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset

81 
else 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

82 
Cache_IO.run_and_cache certs key mk_cmd input 
36898  83 
 (SOME output, _) => 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

84 
trace_and ctxt ("Using cached certificate from " ^ 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

85 
File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

86 
I output)) 
36898  87 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

88 
fun run_solver ctxt name mk_cmd input = 
36898  89 
let 
90 
fun pretty tag ls = Pretty.string_of (Pretty.big_list tag 

91 
(map Pretty.str ls)) 

92 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

93 
val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input 
36898  94 

40550
f84c664ece8e
trace more solver output before raising an exception due to a nonzero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset

95 
val {redirected_output=res, output=err, return_code} = 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

96 
SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

97 
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err 
36898  98 

48902
44a6967240b7
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
wenzelm
parents:
48534
diff
changeset

99 
val ls = fst (take_suffix (equal "") res) 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

100 
val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls 
40550
f84c664ece8e
trace more solver output before raising an exception due to a nonzero return code (avoids truncating potential counterexamples produced by Z3)
boehmes
parents:
40538
diff
changeset

101 

48534
2307efbfc554
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised  better be more aggressive here
blanchet
parents:
48532
diff
changeset

102 
val _ = return_code <> 0 andalso 
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40560
diff
changeset

103 
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) 
36898  104 
in ls end 
105 

41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

106 
fun trace_assms ctxt = 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

107 
SMT_Config.trace_msg ctxt (Pretty.string_of o 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

108 
Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) 
40198
8d470bbaafd7
trace assumptions before giving them to the SMT solver
boehmes
parents:
40197
diff
changeset

109 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

110 
fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) = 
36898  111 
let 
112 
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] 

40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

113 
fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

114 
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) 
36898  115 
in 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

116 
SMT_Config.trace_msg ctxt (fn () => 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

117 
Pretty.string_of (Pretty.big_list "Names:" [ 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

118 
Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), 
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

119 
Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () 
36898  120 
end 
121 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

122 
in 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

123 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

124 
fun invoke name command ithms ctxt = 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

125 
let 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

126 
val options = SMT_Config.solver_options_of ctxt 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

127 
val comments = ("solver: " ^ name) :: 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

128 
("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) :: 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

129 
("random seed: " ^ 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

130 
string_of_int (Config.get ctxt SMT_Config.random_seed)) :: 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

131 
"arguments:" :: options 
36898  132 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

133 
val (str, recon as {context=ctxt', ...}) = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

134 
ithms 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

135 
> tap (trace_assms ctxt) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

136 
> SMT_Translate.translate ctxt comments 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

137 
> tap trace_recon_data 
41601  138 
in (run_solver ctxt' name (make_cmd command options) str, recon) end 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

139 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

140 
end 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

141 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

142 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

143 
(* configuration *) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

144 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

145 
datatype outcome = Unsat  Sat  Unknown 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

146 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

147 
type solver_config = { 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

148 
name: string, 
48043
3ff2c76c9f64
introduced option "z3_with_extensions" to control whether Z3's support for nonlinear arithmetic and datatypes should be enabled (including potential proof reconstruction failures)
boehmes
parents:
47701
diff
changeset

149 
class: Proof.context > SMT_Utils.class, 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

150 
avail: unit > bool, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

151 
command: unit > string list, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

152 
options: Proof.context > string list, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

153 
default_max_relevant: int, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

154 
supports_filter: bool, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

155 
outcome: string > string list > outcome * string list, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

156 
cex_parser: (Proof.context > SMT_Translate.recon > string list > 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

157 
term list * term list) option, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

158 
reconstruct: (Proof.context > SMT_Translate.recon > string list > 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

159 
int list * thm) option } 
41041  160 

161 

162 
(* registry *) 

163 

164 
type solver_info = { 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

165 
command: unit > string list, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

166 
default_max_relevant: int, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

167 
supports_filter: bool, 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

168 
reconstruct: Proof.context > string list * SMT_Translate.recon > 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

169 
int list * thm } 
36898  170 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

171 
structure Solvers = Generic_Data 
36898  172 
( 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

173 
type T = solver_info Symtab.table 
36898  174 
val empty = Symtab.empty 
175 
val extend = I 

176 
fun merge data = Symtab.merge (K true) data 

177 
) 

178 

40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

179 
local 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

180 
fun finish outcome cex_parser reconstruct ocl outer_ctxt 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

181 
(output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) = 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

182 
(case outcome output of 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

183 
(Unsat, ls) => 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

184 
if not (Config.get ctxt SMT_Config.oracle) andalso is_some reconstruct 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

185 
then the reconstruct outer_ctxt recon ls 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

186 
else ([], ocl ()) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

187 
 (result, ls) => 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

188 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

189 
val (ts, us) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

190 
(case cex_parser of SOME f => f ctxt recon ls  _ => ([], [])) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

191 
in 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

192 
raise SMT_Failure.SMT (SMT_Failure.Counterexample { 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

193 
is_real_cex = (result = Sat), 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

194 
free_constraints = ts, 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40666
diff
changeset

195 
const_defs = us}) 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40357
diff
changeset

196 
end) 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset

197 

98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset

198 
val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False}) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

199 
in 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

200 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

201 
fun add_solver cfg = 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

202 
let 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

203 
val {name, class, avail, command, options, default_max_relevant, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

204 
supports_filter, outcome, cex_parser, reconstruct} = cfg 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

205 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset

206 
fun core_oracle () = cfalse 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

207 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

208 
fun solver ocl = { 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

209 
command = command, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

210 
default_max_relevant = default_max_relevant, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

211 
supports_filter = supports_filter, 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

212 
reconstruct = finish (outcome name) cex_parser reconstruct ocl } 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

213 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

214 
val info = {name=name, class=class, avail=avail, options=options} 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

215 
in 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

216 
Thm.add_oracle (Binding.name name, core_oracle) #> (fn (_, ocl) => 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

217 
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

218 
Context.theory_map (SMT_Config.add_solver info) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

219 
end 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

220 

7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

221 
end 
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

222 

40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

223 
fun get_info ctxt name = 
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

224 
the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) 
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

225 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

226 
val solver_name_of = SMT_Config.solver_of 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

227 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

228 
val available_solvers_of = SMT_Config.available_solvers_of 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

229 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

230 
fun name_and_info_of ctxt = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

231 
let val name = solver_name_of ctxt 
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

232 
in (name, get_info ctxt name) end 
36898  233 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

234 
fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt 
40940
ff805bb109d8
export more information about available SMT solvers
blanchet
parents:
40828
diff
changeset

235 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

236 
fun gen_apply (ithms, ctxt) = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

237 
let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

238 
in 
46743
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

239 
(ithms, ctxt) 
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

240 
> invoke name command 
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

241 
> reconstruct ctxt 
8e365bc843e9
finetune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates
boehmes
parents:
46736
diff
changeset

242 
>> distinct (op =) 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

243 
end 
40166
d3bc972b7d9d
optionally force the remote version of an SMT solver to be executed
boehmes
parents:
40165
diff
changeset

244 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

245 
fun apply_solver ctxt = gen_apply o gen_preprocess ctxt 
40981
67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

246 

67f436af0638
have SMT solvers report the number of facts that they should have by default in Sledgehammer  the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
blanchet
parents:
40980
diff
changeset

247 
val default_max_relevant = #default_max_relevant oo get_info 
36898  248 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

249 
val supports_filter = #supports_filter o snd o name_and_info_of 
36898  250 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

251 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

252 
(* check wellsortedness *) 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

253 

539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

254 
val has_topsort = Term.exists_type (Term.exists_subtype (fn 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

255 
TFree (_, []) => true 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

256 
 TVar (_, []) => true 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

257 
 _ => false)) 
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

258 

41239  259 
(* without this test, we would run into problems when atomizing the rules: *) 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

260 
fun check_topsort ctxt thm = 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

261 
if has_topsort (Thm.prop_of thm) then 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

262 
(SMT_Normalize.drop_fact_warning ctxt thm; TrueI) 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

263 
else 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

264 
thm 
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

265 

227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

266 
fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

267 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

268 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

269 
(* filter *) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

270 

40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset

271 
val cnot = Thm.cterm_of @{theory} @{const Not} 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40578
diff
changeset

272 

41239  273 
fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

274 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

275 
type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) 
41239  276 

50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset

277 
fun smt_filter_preprocess ctxt facts goal xwthms i = 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

278 
let 
40164
57f5db2a48a3
added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents:
40162
diff
changeset

279 
val ctxt = 
50486
d5dc28fafd9d
made MaSh evaluation driver work with SMT solvers
blanchet
parents:
48902
diff
changeset

280 
ctxt 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

281 
> Config.put SMT_Config.oracle false 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41300
diff
changeset

282 
> Config.put SMT_Config.filter_only_facts true 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

283 

40357
82ebdd19c4a4
simulate more closely the behaviour of the tactic
boehmes
parents:
40332
diff
changeset

284 
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46464
diff
changeset

285 
fun negate ct = Thm.dest_comb ct > Thm.apply cnot > Thm.apply 
42320
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset

286 
val cprop = 
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset

287 
(case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) of 
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset

288 
SOME ct => ct 
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset

289 
 NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure ( 
1f09e4c680fc
check if negating the goal is possible (avoids CTERM exception for Pure propositions)
boehmes
parents:
41761
diff
changeset

290 
"goal is not a HOL term"))) 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

291 
in 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

292 
map snd xwthms 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

293 
> map_index I 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

294 
> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

295 
> check_topsorts ctxt' 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

296 
> gen_preprocess ctxt' 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

297 
> pair (map (apsnd snd) xwthms) 
41239  298 
end 
299 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

300 
fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = 
41241  301 
let 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

302 
val ctxt' = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

303 
ctxt 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

304 
> Config.put SMT_Config.timeout (Time.toReal time_limit) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

305 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

306 
fun filter_thms false = K xthms 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

307 
 filter_thms true = map_filter (try (nth xthms)) o fst 
41241  308 
in 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

309 
(ithms, ctxt') 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

310 
> gen_apply 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

311 
> filter_thms (supports_filter ctxt') 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

312 
> mk_result NONE 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40161
diff
changeset

313 
end 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

314 
handle SMT_Failure.SMT fail => mk_result (SOME fail) [] 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

315 

539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39811
diff
changeset

316 

36898  317 
(* SMT tactic *) 
318 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

319 
local 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

320 
fun trace_assumptions ctxt iwthms idxs = 
40165  321 
let 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

322 
val wthms = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

323 
idxs 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

324 
> filter (fn i => i >= 0) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

325 
> map_filter (AList.lookup (op =) iwthms) 
40165  326 
in 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

327 
if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

328 
then 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

329 
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

330 
(map (Display.pretty_thm ctxt o snd) wthms))) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

331 
else () 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

332 
end 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

333 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

334 
fun solve ctxt iwthms = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

335 
iwthms 
54041
227908156cd2
make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents:
52732
diff
changeset

336 
> check_topsorts ctxt 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

337 
> apply_solver ctxt 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

338 
>> trace_assumptions ctxt iwthms 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

339 
> snd 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

340 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

341 
fun str_of ctxt fail = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

342 
SMT_Failure.string_of_failure ctxt fail 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

343 
> prefix ("Solver " ^ SMT_Config.solver_of ctxt ^ ": ") 
36898  344 

41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

345 
fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

346 
handle 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

347 
SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

348 
(SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) 
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset

349 
 SMT_Failure.SMT (fail as SMT_Failure.Time_Out) => 
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset

350 
error ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^ 
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset

351 
SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^ 
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42320
diff
changeset

352 
"configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)") 
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41601
diff
changeset

353 
 SMT_Failure.SMT fail => error (str_of ctxt fail) 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

354 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

355 
fun tag_rules thms = map_index (apsnd (pair NONE)) thms 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

356 
fun tag_prems thms = map (pair ~1 o pair NONE) thms 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

357 

52732  358 
fun resolve (SOME thm) = rtac thm 1 
46464  359 
 resolve NONE = no_tac 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

360 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

361 
fun tac prove ctxt rules = 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

362 
CONVERSION (SMT_Normalize.atomize_conv ctxt) 
52732  363 
THEN' rtac @{thm ccontr} 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

364 
THEN' SUBPROOF (fn {context, prems, ...} => 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

365 
resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

366 
in 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

367 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

368 
val smt_tac = tac safe_solve 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

369 
val smt_tac' = tac (SOME oo solve) 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

370 

3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

371 
end 
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

372 

36898  373 
end 