author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64304  96bc94c87a81 
permissions  rwrr 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

1 
(* Title: HOL/Library/Old_SMT/old_smt_solver.ML 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
SMT solvers registry and SMT tactic. 

5 
*) 

6 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

7 
signature OLD_SMT_SOLVER = 
36898  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, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

13 
class: Proof.context > Old_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, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

20 
cex_parser: (Proof.context > Old_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, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

22 
reconstruct: (Proof.context > Old_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 > 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

39 
{outcome: Old_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 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

46 
structure Old_SMT_Solver: OLD_SMT_SOLVER = 
36898  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 

62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
61268
diff
changeset

54 
fun make_cmd command options problem_path proof_path = 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
61268
diff
changeset

55 
space_implode " " 
64304  56 
("(exec 2>&1;" :: map Bash.string (command () @ options) @ 
62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
61268
diff
changeset

57 
[File.bash_path problem_path, ")", ">", File.bash_path proof_path]) 
36898  58 

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

59 
fun trace_and ctxt msg f x = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

62 

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

63 
fun run ctxt name mk_cmd input = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

64 
(case Old_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

65 
NONE => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

66 
if not (Old_SMT_Config.is_available ctxt name) then 
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

67 
error ("The SMT solver " ^ quote name ^ " is not installed.") 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

68 
else if Config.get ctxt Old_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

69 
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

70 
(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

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

72 
let 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

73 
val base_path = Path.explode (Config.get ctxt Old_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

74 
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

75 
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

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

79 
(NONE, key) => 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

81 
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

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

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

85 
trace_and ctxt ("Using cached certificate from " ^ 
62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
61268
diff
changeset

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

87 
I output)) 
36898  88 

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

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

92 
(map Pretty.str ls)) 

93 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

96 
val {redirected_output=res, output=err, return_code} = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

97 
Old_SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

98 
val _ = Old_SMT_Config.trace_msg ctxt (pretty "Solver:") err 
36898  99 

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

100 
val ls = fst (take_suffix (equal "") res) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

101 
val _ = Old_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

102 

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

103 
val _ = return_code <> 0 andalso 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

104 
raise Old_SMT_Failure.SMT (Old_SMT_Failure.Abnormal_Termination return_code) 
36898  105 
in ls end 
106 

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

107 
fun trace_assms ctxt = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

110 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

111 
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) = 
36898  112 
let 
113 
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

114 
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

115 
fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) 
36898  116 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

117 
Old_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

118 
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

119 
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

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

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

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

124 

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

125 
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

126 
let 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

127 
val options = Old_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

128 
val comments = ("solver: " ^ name) :: 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

130 
("random seed: " ^ 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

132 
"arguments:" :: options 
36898  133 

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

134 
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

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

136 
> tap (trace_assms ctxt) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

138 
> tap trace_recon_data 
41601  139 
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

140 

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

141 
end 
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 

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

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

145 

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

146 
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

147 

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

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

149 
name: string, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

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

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

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

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

156 
outcome: string > string list > outcome * string list, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

157 
cex_parser: (Proof.context > Old_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

158 
term list * term list) option, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

159 
reconstruct: (Proof.context > Old_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

160 
int list * thm) option } 
41041  161 

162 

163 
(* registry *) 

164 

165 
type solver_info = { 

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

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

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

168 
supports_filter: bool, 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

170 
int list * thm } 
36898  171 

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

172 
structure Solvers = Generic_Data 
36898  173 
( 
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

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

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

178 
) 

179 

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

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

181 
fun finish outcome cex_parser reconstruct ocl outer_ctxt 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

182 
(output, (recon as {context=ctxt, ...} : Old_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

183 
(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

184 
(Unsat, ls) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

185 
if not (Config.get ctxt Old_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

186 
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

187 
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

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

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

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

191 
(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

192 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

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

196 
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

197 
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

198 

59634  199 
val cfalse = Thm.cterm_of @{context} (@{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

200 
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

201 

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 
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

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

204 
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

205 
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

206 

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

207 
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

208 

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

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

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

211 
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

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

213 
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

214 

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

215 
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

216 
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

217 
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

218 
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

219 
Context.theory_map (Old_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

220 
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

221 

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 
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

223 

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

224 
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

225 
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

226 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

228 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

230 

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

231 
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

232 
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

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

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

236 

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

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

238 
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

239 
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

240 
(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

241 
> 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

242 
> 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

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

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

245 

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

246 
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

247 

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

248 
val default_max_relevant = #default_max_relevant oo get_info 
36898  249 

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

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

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

252 

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

253 
(* 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

254 

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 
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

256 
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

257 
 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

258 
 _ => 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

259 

41239  260 
(* 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

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

262 
if has_topsort (Thm.prop_of thm) then 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

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

266 

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

267 
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

268 

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

269 

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

270 
(* 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

271 

59634  272 
val cnot = Thm.cterm_of @{context} @{const Not} 
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

273 

41239  274 
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

275 

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

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

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

278 
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

279 
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

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

281 
ctxt 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

282 
> Config.put Old_SMT_Config.oracle false 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

283 
> Config.put Old_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

284 

60695
757549b4bbe6
Variable.focus etc.: optional bindings provided by user;
wenzelm
parents:
59634
diff
changeset

285 
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE 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

286 
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

287 
val cprop = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

289 
SOME ct => ct 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

291 
"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

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

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

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

295 
> 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

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

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

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

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

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

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

304 
ctxt 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

306 

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

307 
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

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

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

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

312 
> 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

313 
> 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

314 
end 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

315 
handle Old_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

316 

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

317 

36898  318 
(* SMT tactic *) 
319 

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

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

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

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

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

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

326 
> map_filter (AList.lookup (op =) iwthms) 
40165  327 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

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

330 
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" 
61268  331 
(map (Thm.pretty_thm ctxt o snd) wthms))) 
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41328
diff
changeset

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

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

334 

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

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

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

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

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

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

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

341 

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

342 
fun str_of ctxt fail = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

343 
Old_SMT_Failure.string_of_failure ctxt fail 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

344 
> prefix ("Solver " ^ Old_SMT_Config.solver_of ctxt ^ ": ") 
36898  345 

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

346 
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

347 
handle 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

348 
Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Counterexample _) => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

349 
(Old_SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

350 
 Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Time_Out) => 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

351 
error ("SMT: Solver " ^ quote (Old_SMT_Config.solver_of ctxt) ^ ": " ^ 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

352 
Old_SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^ 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

353 
"configuration option " ^ quote (Config.name_of Old_SMT_Config.timeout) ^ " might help)") 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

354 
 Old_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

355 

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

356 
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

357 
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

358 

60752  359 
fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 
360 
 resolve _ NONE = no_tac 

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

361 

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

362 
fun tac prove ctxt rules = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

363 
CONVERSION (Old_SMT_Normalize.atomize_conv ctxt) 
60752  364 
THEN' resolve_tac ctxt @{thms ccontr} 
365 
THEN' SUBPROOF (fn {context = ctxt', prems, ...} => 

366 
resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt 

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

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

368 

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

369 
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

370 
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

371 

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

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

373 

36898  374 
end 