1(* Title: HOL/SMT.thy 2 Author: Sascha Boehme, TU Muenchen 3 Author: Jasmin Blanchette, VU Amsterdam 4*) 5 6section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close> 7 8theory SMT 9 imports Divides 10 keywords "smt_status" :: diag 11begin 12 13subsection \<open>A skolemization tactic and proof method\<close> 14 15lemma choices: 16 "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)" 17 "\<And>Q. \<forall>x. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x. Q x (f x) (fa x) (fb x)" 18 "\<And>Q. \<forall>x. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x. Q x (f x) (fa x) (fb x) (fc x)" 19 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 20 \<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 21 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 22 \<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" 23 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 24 \<exists>f fa fb fc fd fe ff. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" 25 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> 26 \<exists>f fa fb fc fd fe ff fg. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" 27 by metis+ 28 29lemma bchoices: 30 "\<And>Q. \<forall>x \<in> S. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x \<in> S. Q x (f x) (fa x)" 31 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x \<in> S. Q x (f x) (fa x) (fb x)" 32 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x)" 33 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 34 \<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 35 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 36 \<exists>f fa fb fc fd fe. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" 37 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 38 \<exists>f fa fb fc fd fe ff. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" 39 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> 40 \<exists>f fa fb fc fd fe ff fg. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" 41 by metis+ 42 43ML \<open> 44fun moura_tac ctxt = 45 Atomize_Elim.atomize_elim_tac ctxt THEN' 46 SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN 47 ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) 48 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' 49 blast_tac ctxt)) 50\<close> 51 52method_setup moura = \<open> 53 Scan.succeed (SIMPLE_METHOD' o moura_tac) 54\<close> "solve skolemization goals, especially those arising from Z3 proofs" 55 56hide_fact (open) choices bchoices 57 58 59subsection \<open>Triggers for quantifier instantiation\<close> 60 61text \<open> 62Some SMT solvers support patterns as a quantifier instantiation 63heuristics. Patterns may either be positive terms (tagged by "pat") 64triggering quantifier instantiations -- when the solver finds a 65term matching a positive pattern, it instantiates the corresponding 66quantifier accordingly -- or negative terms (tagged by "nopat") 67inhibiting quantifier instantiations. A list of patterns 68of the same kind is called a multipattern, and all patterns in a 69multipattern are considered conjunctively for quantifier instantiation. 70A list of multipatterns is called a trigger, and their multipatterns 71act disjunctively during quantifier instantiation. Each multipattern 72should mention at least all quantified variables of the preceding 73quantifier block. 74\<close> 75 76typedecl 'a symb_list 77 78consts 79 Symb_Nil :: "'a symb_list" 80 Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list" 81 82typedecl pattern 83 84consts 85 pat :: "'a \<Rightarrow> pattern" 86 nopat :: "'a \<Rightarrow> pattern" 87 88definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where 89 "trigger _ P = P" 90 91 92subsection \<open>Higher-order encoding\<close> 93 94text \<open> 95Application is made explicit for constants occurring with varying 96numbers of arguments. This is achieved by the introduction of the 97following constant. 98\<close> 99 100definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f" 101 102text \<open> 103Some solvers support a theory of arrays which can be used to encode 104higher-order functions. The following set of lemmas specifies the 105properties of such (extensional) arrays. 106\<close> 107 108lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def 109 110 111subsection \<open>Normalization\<close> 112 113lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" 114 by simp 115 116lemmas Ex1_def_raw = Ex1_def[abs_def] 117lemmas Ball_def_raw = Ball_def[abs_def] 118lemmas Bex_def_raw = Bex_def[abs_def] 119lemmas abs_if_raw = abs_if[abs_def] 120lemmas min_def_raw = min_def[abs_def] 121lemmas max_def_raw = max_def[abs_def] 122 123lemma nat_zero_as_int: 124 "0 = nat 0" 125 by simp 126 127lemma nat_one_as_int: 128 "1 = nat 1" 129 by simp 130 131lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp 132lemma nat_less_as_int: "(<) = (\<lambda>a b. int a < int b)" by simp 133lemma nat_leq_as_int: "(\<le>) = (\<lambda>a b. int a \<le> int b)" by simp 134lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp 135lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp 136lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp 137lemma nat_times_as_int: "( * ) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) 138lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) 139lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) 140 141lemma int_Suc: "int (Suc n) = int n + 1" by simp 142lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) 143lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto 144 145lemma nat_int_comparison: 146 fixes a b :: nat 147 shows "(a = b) = (int a = int b)" 148 and "(a < b) = (int a < int b)" 149 and "(a \<le> b) = (int a \<le> int b)" 150 by simp_all 151 152lemma int_ops: 153 fixes a b :: nat 154 shows "int 0 = 0" 155 and "int 1 = 1" 156 and "int (numeral n) = numeral n" 157 and "int (Suc a) = int a + 1" 158 and "int (a + b) = int a + int b" 159 and "int (a - b) = (if int a < int b then 0 else int a - int b)" 160 and "int (a * b) = int a * int b" 161 and "int (a div b) = int a div int b" 162 and "int (a mod b) = int a mod int b" 163 by (auto intro: zdiv_int zmod_int) 164 165lemma int_if: 166 fixes a b :: nat 167 shows "int (if P then a else b) = (if P then int a else int b)" 168 by simp 169 170 171subsection \<open>Integer division and modulo for Z3\<close> 172 173text \<open> 174The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This 175Sch��nheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems. 176\<close> 177 178definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 179 "z3div k l = (if l \<ge> 0 then k div l else - (k div - l))" 180 181definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 182 "z3mod k l = k mod (if l \<ge> 0 then l else - l)" 183 184lemma div_as_z3div: 185 "\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" 186 by (simp add: z3div_def) 187 188lemma mod_as_z3mod: 189 "\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" 190 by (simp add: z3mod_def) 191 192 193subsection \<open>Setup\<close> 194 195ML_file "Tools/SMT/smt_util.ML" 196ML_file "Tools/SMT/smt_failure.ML" 197ML_file "Tools/SMT/smt_config.ML" 198ML_file "Tools/SMT/smt_builtin.ML" 199ML_file "Tools/SMT/smt_datatypes.ML" 200ML_file "Tools/SMT/smt_normalize.ML" 201ML_file "Tools/SMT/smt_translate.ML" 202ML_file "Tools/SMT/smtlib.ML" 203ML_file "Tools/SMT/smtlib_interface.ML" 204ML_file "Tools/SMT/smtlib_proof.ML" 205ML_file "Tools/SMT/smtlib_isar.ML" 206ML_file "Tools/SMT/z3_proof.ML" 207ML_file "Tools/SMT/z3_isar.ML" 208ML_file "Tools/SMT/smt_solver.ML" 209ML_file "Tools/SMT/cvc4_interface.ML" 210ML_file "Tools/SMT/cvc4_proof_parse.ML" 211ML_file "Tools/SMT/verit_proof.ML" 212ML_file "Tools/SMT/verit_isar.ML" 213ML_file "Tools/SMT/verit_proof_parse.ML" 214ML_file "Tools/SMT/conj_disj_perm.ML" 215ML_file "Tools/SMT/z3_interface.ML" 216ML_file "Tools/SMT/z3_replay_util.ML" 217ML_file "Tools/SMT/z3_replay_rules.ML" 218ML_file "Tools/SMT/z3_replay_methods.ML" 219ML_file "Tools/SMT/z3_replay.ML" 220ML_file "Tools/SMT/smt_systems.ML" 221 222method_setup smt = \<open> 223 Scan.optional Attrib.thms [] >> 224 (fn thms => fn ctxt => 225 METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) 226\<close> "apply an SMT solver to the current goal" 227 228 229subsection \<open>Configuration\<close> 230 231text \<open> 232The current configuration can be printed by the command 233\<open>smt_status\<close>, which shows the values of most options. 234\<close> 235 236 237subsection \<open>General configuration options\<close> 238 239text \<open> 240The option \<open>smt_solver\<close> can be used to change the target SMT 241solver. The possible values can be obtained from the \<open>smt_status\<close> 242command. 243\<close> 244 245declare [[smt_solver = z3]] 246 247text \<open> 248Since SMT solvers are potentially nonterminating, there is a timeout 249(given in seconds) to restrict their runtime. 250\<close> 251 252declare [[smt_timeout = 20]] 253 254text \<open> 255SMT solvers apply randomized heuristics. In case a problem is not 256solvable by an SMT solver, changing the following option might help. 257\<close> 258 259declare [[smt_random_seed = 1]] 260 261text \<open> 262In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 263solvers are fully trusted without additional checks. The following 264option can cause the SMT solver to run in proof-producing mode, giving 265a checkable certificate. This is currently only implemented for Z3. 266\<close> 267 268declare [[smt_oracle = false]] 269 270text \<open> 271Each SMT solver provides several commandline options to tweak its 272behaviour. They can be passed to the solver by setting the following 273options. 274\<close> 275 276declare [[cvc3_options = ""]] 277declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] 278declare [[verit_options = "--index-sorts --index-fresh-sorts"]] 279declare [[z3_options = ""]] 280 281text \<open> 282The SMT method provides an inference mechanism to detect simple triggers 283in quantified formulas, which might increase the number of problems 284solvable by SMT solvers (note: triggers guide quantifier instantiations 285in the SMT solver). To turn it on, set the following option. 286\<close> 287 288declare [[smt_infer_triggers = false]] 289 290text \<open> 291Enable the following option to use built-in support for datatypes, 292codatatypes, and records in CVC4. Currently, this is implemented only 293in oracle mode. 294\<close> 295 296declare [[cvc4_extensions = false]] 297 298text \<open> 299Enable the following option to use built-in support for div/mod, datatypes, 300and records in Z3. Currently, this is implemented only in oracle mode. 301\<close> 302 303declare [[z3_extensions = false]] 304 305 306subsection \<open>Certificates\<close> 307 308text \<open> 309By setting the option \<open>smt_certificates\<close> to the name of a file, 310all following applications of an SMT solver a cached in that file. 311Any further application of the same SMT solver (using the very same 312configuration) re-uses the cached certificate instead of invoking the 313solver. An empty string disables caching certificates. 314 315The filename should be given as an explicit path. It is good 316practice to use the name of the current theory (with ending 317\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file. 318Certificate files should be used at most once in a certain theory context, 319to avoid race conditions with other concurrent accesses. 320\<close> 321 322declare [[smt_certificates = ""]] 323 324text \<open> 325The option \<open>smt_read_only_certificates\<close> controls whether only 326stored certificates are should be used or invocation of an SMT solver 327is allowed. When set to \<open>true\<close>, no SMT solver will ever be 328invoked and only the existing certificates found in the configured 329cache are used; when set to \<open>false\<close> and there is no cached 330certificate for some proposition, then the configured SMT solver is 331invoked. 332\<close> 333 334declare [[smt_read_only_certificates = false]] 335 336 337subsection \<open>Tracing\<close> 338 339text \<open> 340The SMT method, when applied, traces important information. To 341make it entirely silent, set the following option to \<open>false\<close>. 342\<close> 343 344declare [[smt_verbose = true]] 345 346text \<open> 347For tracing the generated problem file given to the SMT solver as 348well as the returned result of the solver, the option 349\<open>smt_trace\<close> should be set to \<open>true\<close>. 350\<close> 351 352declare [[smt_trace = false]] 353 354 355subsection \<open>Schematic rules for Z3 proof reconstruction\<close> 356 357text \<open> 358Several prof rules of Z3 are not very well documented. There are two 359lemma groups which can turn failing Z3 proof reconstruction attempts 360into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to 361any implemented reconstruction procedure for all uncertain Z3 proof 362rules; the facts in \<open>z3_simp\<close> are only fed to invocations of 363the simplifier when reconstructing theory-specific proof steps. 364\<close> 365 366lemmas [z3_rule] = 367 refl eq_commute conj_commute disj_commute simp_thms nnf_simps 368 ring_distribs field_simps times_divide_eq_right times_divide_eq_left 369 if_True if_False not_not 370 NO_MATCH_def 371 372lemma [z3_rule]: 373 "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 374 "(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 375 "(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" 376 "(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))" 377 "(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))" 378 "(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))" 379 "(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))" 380 "(\<not> P \<and> \<not> Q) = (\<not> (Q \<or> P))" 381 by auto 382 383lemma [z3_rule]: 384 "(P \<longrightarrow> Q) = (Q \<or> \<not> P)" 385 "(\<not> P \<longrightarrow> Q) = (P \<or> Q)" 386 "(\<not> P \<longrightarrow> Q) = (Q \<or> P)" 387 "(True \<longrightarrow> P) = P" 388 "(P \<longrightarrow> True) = True" 389 "(False \<longrightarrow> P) = True" 390 "(P \<longrightarrow> P) = True" 391 "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" 392 by auto 393 394lemma [z3_rule]: 395 "((P = Q) \<longrightarrow> R) = (R \<or> (Q = (\<not> P)))" 396 by auto 397 398lemma [z3_rule]: 399 "(\<not> True) = False" 400 "(\<not> False) = True" 401 "(x = x) = True" 402 "(P = True) = P" 403 "(True = P) = P" 404 "(P = False) = (\<not> P)" 405 "(False = P) = (\<not> P)" 406 "((\<not> P) = P) = False" 407 "(P = (\<not> P)) = False" 408 "((\<not> P) = (\<not> Q)) = (P = Q)" 409 "\<not> (P = (\<not> Q)) = (P = Q)" 410 "\<not> ((\<not> P) = Q) = (P = Q)" 411 "(P \<noteq> Q) = (Q = (\<not> P))" 412 "(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))" 413 "(P \<noteq> Q) = ((\<not> P \<or> \<not> Q) \<and> (P \<or> Q))" 414 by auto 415 416lemma [z3_rule]: 417 "(if P then P else \<not> P) = True" 418 "(if \<not> P then \<not> P else P) = True" 419 "(if P then True else False) = P" 420 "(if P then False else True) = (\<not> P)" 421 "(if P then Q else True) = ((\<not> P) \<or> Q)" 422 "(if P then Q else True) = (Q \<or> (\<not> P))" 423 "(if P then Q else \<not> Q) = (P = Q)" 424 "(if P then Q else \<not> Q) = (Q = P)" 425 "(if P then \<not> Q else Q) = (P = (\<not> Q))" 426 "(if P then \<not> Q else Q) = ((\<not> Q) = P)" 427 "(if \<not> P then x else y) = (if P then y else x)" 428 "(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)" 429 "(if P then (if Q then x else y) else x) = (if (\<not> Q) \<and> P then y else x)" 430 "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" 431 "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" 432 "(if P then x else if P then y else z) = (if P then x else z)" 433 "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" 434 "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" 435 "(if P then x = y else x = z) = (x = (if P then y else z))" 436 "(if P then x = y else y = z) = (y = (if P then x else z))" 437 "(if P then x = y else z = y) = (y = (if P then x else z))" 438 by auto 439 440lemma [z3_rule]: 441 "0 + (x::int) = x" 442 "x + 0 = x" 443 "x + x = 2 * x" 444 "0 * x = 0" 445 "1 * x = x" 446 "x + y = y + x" 447 by (auto simp add: mult_2) 448 449lemma [z3_rule]: (* for def-axiom *) 450 "P = Q \<or> P \<or> Q" 451 "P = Q \<or> \<not> P \<or> \<not> Q" 452 "(\<not> P) = Q \<or> \<not> P \<or> Q" 453 "(\<not> P) = Q \<or> P \<or> \<not> Q" 454 "P = (\<not> Q) \<or> \<not> P \<or> Q" 455 "P = (\<not> Q) \<or> P \<or> \<not> Q" 456 "P \<noteq> Q \<or> P \<or> \<not> Q" 457 "P \<noteq> Q \<or> \<not> P \<or> Q" 458 "P \<noteq> (\<not> Q) \<or> P \<or> Q" 459 "(\<not> P) \<noteq> Q \<or> P \<or> Q" 460 "P \<or> Q \<or> P \<noteq> (\<not> Q)" 461 "P \<or> Q \<or> (\<not> P) \<noteq> Q" 462 "P \<or> \<not> Q \<or> P \<noteq> Q" 463 "\<not> P \<or> Q \<or> P \<noteq> Q" 464 "P \<or> y = (if P then x else y)" 465 "P \<or> (if P then x else y) = y" 466 "\<not> P \<or> x = (if P then x else y)" 467 "\<not> P \<or> (if P then x else y) = x" 468 "P \<or> R \<or> \<not> (if P then Q else R)" 469 "\<not> P \<or> Q \<or> \<not> (if P then Q else R)" 470 "\<not> (if P then Q else R) \<or> \<not> P \<or> Q" 471 "\<not> (if P then Q else R) \<or> P \<or> R" 472 "(if P then Q else R) \<or> \<not> P \<or> \<not> Q" 473 "(if P then Q else R) \<or> P \<or> \<not> R" 474 "(if P then \<not> Q else R) \<or> \<not> P \<or> Q" 475 "(if P then Q else \<not> R) \<or> P \<or> R" 476 by auto 477 478hide_type (open) symb_list pattern 479hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod 480 481end 482