# HG changeset patch # User boehmes # Date 1288086312 -7200 # Node ID 7f58a9a843c2bf638e2104f60f553dc5e830d30a # Parent 539d07b00e5f04835e0715b1ef0ac5991be83d5c joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface diff -r 539d07b00e5f -r 7f58a9a843c2 NEWS --- a/NEWS Tue Oct 26 11:39:26 2010 +0200 +++ b/NEWS Tue Oct 26 11:45:12 2010 +0200 @@ -306,6 +306,15 @@ sledgehammer [atp = ...] ~> sledgehammer [prover = ...] INCOMPATIBILITY. +* Changed SMT configuration options: + - Renamed: + z3_proofs ~> smt_oracle (with swapped semantics) + z3_trace_assms ~> smt_trace_used_facts + INCOMPATIBILITY. + - Added: + cvc3_options + yices_options + smt_datatypes *** FOL *** diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/IsaMakefile Tue Oct 26 11:45:12 2010 +0200 @@ -336,20 +336,18 @@ Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ Tools/Sledgehammer/sledgehammer_atp_translate.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ - Tools/SMT/cvc3_solver.ML \ Tools/SMT/smtlib_interface.ML \ Tools/SMT/smt_monomorph.ML \ Tools/SMT/smt_normalize.ML \ + Tools/SMT/smt_setup_solvers.ML \ Tools/SMT/smt_solver.ML \ Tools/SMT/smt_translate.ML \ - Tools/SMT/yices_solver.ML \ Tools/SMT/z3_interface.ML \ Tools/SMT/z3_model.ML \ Tools/SMT/z3_proof_literals.ML \ Tools/SMT/z3_proof_parser.ML \ Tools/SMT/z3_proof_reconstruction.ML \ Tools/SMT/z3_proof_tools.ML \ - Tools/SMT/z3_solver.ML \ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/SMT.thy Tue Oct 26 11:45:12 2010 +0200 @@ -19,9 +19,7 @@ ("Tools/SMT/z3_proof_reconstruction.ML") ("Tools/SMT/z3_model.ML") ("Tools/SMT/z3_interface.ML") - ("Tools/SMT/z3_solver.ML") - ("Tools/SMT/cvc3_solver.ML") - ("Tools/SMT/yices_solver.ML") + ("Tools/SMT/smt_setup_solvers.ML") begin @@ -124,16 +122,12 @@ use "Tools/SMT/z3_proof_literals.ML" use "Tools/SMT/z3_proof_reconstruction.ML" use "Tools/SMT/z3_model.ML" -use "Tools/SMT/z3_solver.ML" -use "Tools/SMT/cvc3_solver.ML" -use "Tools/SMT/yices_solver.ML" +use "Tools/SMT/smt_setup_solvers.ML" setup {* SMT_Solver.setup #> Z3_Proof_Reconstruction.setup #> - Z3_Solver.setup #> - CVC3_Solver.setup #> - Yices_Solver.setup + SMT_Setup_Solvers.setup *} @@ -171,6 +165,31 @@ declare [[ smt_timeout = 20 ]] +text {* +In general, the binding to SMT solvers runs as an oracle, i.e, the SMT +solvers are fully trusted without additional checks. The following +option can cause the SMT solver to run in proof-producing mode, giving +a checkable certificate. This is currently only implemented for Z3. +*} + +declare [[ smt_oracle = false ]] + +text {* +Each SMT solver provides several commandline options to tweak its +behaviour. They can be passed to the solver by setting the following +options. +*} + +declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]] + +text {* +Enable the following option to use built-in support for datatypes and +records. Currently, this is only implemented for Z3 running in oracle +mode. +*} + +declare [[ smt_datatypes = false ]] + subsection {* Certificates *} @@ -213,41 +232,14 @@ declare [[ smt_trace = false ]] - - -subsection {* Z3-specific options *} - text {* -Z3 is the only SMT solver whose proofs are checked (or reconstructed) -in Isabelle (all other solvers are implemented as oracles). Enabling -or disabling proof reconstruction for Z3 is controlled by the option -@{text z3_proofs}. +From the set of assumptions given to the SMT solver, those assumptions +used in the proof are traced when the following option is set to +@{term true}. This only works for Z3 when it runs in non-oracle mode +(see options @{text smt_solver} and @{text smt_oracle} above). *} -declare [[ z3_proofs = true ]] - -text {* -From the set of assumptions given to Z3, those assumptions used in -the proof are traced when the option @{text z3_trace_assms} is set to -@{term true}. -*} - -declare [[ z3_trace_assms = false ]] - -text {* -Z3 provides several commandline options to tweak its behaviour. They -can be configured by writing them literally as value for the option -@{text z3_options}. -*} - -declare [[ z3_options = "" ]] - -text {* -The following configuration option may be used to enable mapping of -HOL datatypes and records to native datatypes provided by Z3. -*} - -declare [[ z3_datatypes = false ]] +declare [[ smt_trace_used_facts = false ]] diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/cvc3_solver.ML --- a/src/HOL/Tools/SMT/cvc3_solver.ML Tue Oct 26 11:39:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* Title: HOL/Tools/SMT/cvc3_solver.ML - Author: Sascha Boehme, TU Muenchen - -Interface of the SMT solver CVC3. -*) - -signature CVC3_SOLVER = -sig - val setup: theory -> theory -end - -structure CVC3_Solver: CVC3_SOLVER = -struct - -val solver_name = "cvc3" -val env_var = "CVC3_SOLVER" - -val options = ["-lang", "smtlib", "-output-lang", "presentation"] - -val is_sat = String.isPrefix "Satisfiable." -val is_unsat = String.isPrefix "Unsatisfiable." -val is_unknown = String.isPrefix "Unknown." - -fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, []) - -fun core_oracle (output, _) = - let - val empty_line = (fn "" => true | _ => false) - val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) - val (l, _) = split_first (snd (chop_while empty_line output)) - in - if is_unsat l then @{cprop False} - else if is_sat l then raise_cex true - else if is_unknown l then raise_cex false - else raise SMT_Solver.SMT (solver_name ^ " failed") - end - -fun solver oracle _ = { - command = {env_var=env_var, remote_name=SOME solver_name}, - arguments = options, - interface = SMTLIB_Interface.interface, - reconstruct = pair o pair [] o oracle } - -val setup = - Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => - Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) - -end diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Oct 26 11:45:12 2010 +0200 @@ -17,7 +17,7 @@ signature SMT_NORMALIZE = sig - type extra_norm = (int * thm) list -> Proof.context -> + type extra_norm = bool -> (int * thm) list -> Proof.context -> (int * thm) list * Proof.context val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context -> (int * thm) list * Proof.context @@ -480,7 +480,7 @@ (* combined normalization *) -type extra_norm = (int * thm) list -> Proof.context -> +type extra_norm = bool -> (int * thm) list -> Proof.context -> (int * thm) list * Proof.context fun with_context f irules ctxt = (f ctxt irules, ctxt) @@ -492,7 +492,7 @@ |> normalize_numerals ctxt |> nat_as_int ctxt |> rpair ctxt - |-> extra_norm + |-> extra_norm with_datatypes |-> with_context (fn cx => map (apsnd (normalize_rule cx))) |-> SMT_Monomorph.monomorph |-> lift_lambdas diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/smt_setup_solvers.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Oct 26 11:45:12 2010 +0200 @@ -0,0 +1,93 @@ +(* Title: HOL/Tools/SMT/smt_setup_solvers.ML + Author: Sascha Boehme, TU Muenchen + +Setup SMT solvers. +*) + +signature SMT_SETUP_SOLVERS = +sig + val setup: theory -> theory +end + +structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS = +struct + +fun outcome_of unsat sat unknown solver_name line = + if String.isPrefix unsat line then SMT_Solver.Unsat + else if String.isPrefix sat line then SMT_Solver.Sat + else if String.isPrefix unknown line then SMT_Solver.Unknown + else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^ + quote solver_name ^ " failed, " ^ "see trace for details.")) + +fun on_first_line test_outcome solver_name lines = + let + val empty_line = (fn "" => true | _ => false) + val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) + val (l, ls) = split_first (snd (chop_while empty_line lines)) + in (test_outcome solver_name l, ls) end + + +(* CVC3 *) + +val cvc3 = { + name = "cvc3", + env_var = "CVC3_SOLVER", + is_remote = true, + options = K ["-lang", "smtlib", "-output-lang", "presentation"], + interface = SMTLIB_Interface.interface, + outcome = + on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), + cex_parser = NONE, + reconstruct = NONE } + + +(* Yices *) + +val yices = { + name = "yices", + env_var = "YICES_SOLVER", + is_remote = false, + options = K ["--smtlib"], + interface = SMTLIB_Interface.interface, + outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), + cex_parser = NONE, + reconstruct = NONE } + + +(* Z3 *) + +fun z3_options ctxt = + ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"] + |> not (Config.get ctxt SMT_Solver.oracle) ? + append ["DISPLAY_PROOF=true","PROOF_MODE=2"] + +fun z3_on_last_line solver_name lines = + let + fun junk l = + String.isPrefix "WARNING" l orelse + String.isPrefix "ERROR" l orelse + forall Symbol.is_ascii_blank (Symbol.explode l) + in + the_default ("", []) (try (swap o split_last) (filter_out junk lines)) + |>> outcome_of "unsat" "sat" "unknown" solver_name + end + +val z3 = { + name = "z3", + env_var = "Z3_SOLVER", + is_remote = true, + options = z3_options, + interface = Z3_Interface.interface, + outcome = z3_on_last_line, + cex_parser = SOME Z3_Model.parse_counterex, + reconstruct = SOME Z3_Proof_Reconstruction.reconstruct } + + +(* overall setup *) + +val setup = + SMT_Solver.add_solver cvc3 #> + SMT_Solver.add_solver yices #> + SMT_Solver.add_solver z3 + +end diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:45:12 2010 +0200 @@ -6,24 +6,37 @@ signature SMT_SOLVER = sig - exception SMT of string - exception SMT_COUNTEREXAMPLE of bool * term list + datatype failure = + Counterexample of bool * term list | + Time_Out | + Other_Failure of string + val string_of_failure: Proof.context -> failure -> string + exception SMT of failure type interface = { extra_norm: SMT_Normalize.extra_norm, translate: SMT_Translate.config } + datatype outcome = Unsat | Sat | Unknown type solver_config = { - command: {env_var: string, remote_name: string option}, - arguments: string list, + name: string, + env_var: string, + is_remote: bool, + options: Proof.context -> string list, interface: interface, - reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> - (int list * thm) * Proof.context } + outcome: string -> string list -> outcome * string list, + cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> + term list) option, + reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> + (int list * thm) * Proof.context) option } (*options*) + val oracle: bool Config.T + val datatypes: bool Config.T val timeout: int Config.T val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b val trace: bool Config.T val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit + val trace_used_facts: bool Config.T (*certificates*) val fixed_certificates: bool Config.T @@ -31,19 +44,17 @@ (*solvers*) type solver = Proof.context -> (int * thm) list -> int list * thm - type solver_info = Context.generic -> Pretty.T list - val add_solver: string * (Proof.context -> solver_config) -> - Context.generic -> Context.generic + val add_solver: solver_config -> theory -> theory + val set_solver_options: string -> string -> Context.generic -> + Context.generic val all_solver_names_of: Context.generic -> string list - val add_solver_info: string * solver_info -> Context.generic -> - Context.generic val solver_name_of: Context.generic -> string val select_solver: string -> Context.generic -> Context.generic val solver_of: Context.generic -> solver - (*solver*) - val smt_solver: Proof.context -> ('a * thm) list -> 'a list * thm - val smt_filter: Proof.context -> ('a * thm) list -> 'a list * string + (*filter*) + val smt_filter: Proof.state -> int -> ('a * thm) list -> + 'a list * failure option (*tactic*) val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic @@ -57,36 +68,64 @@ structure SMT_Solver: SMT_SOLVER = struct -exception SMT of string -exception SMT_COUNTEREXAMPLE of bool * term list +datatype failure = + Counterexample of bool * term list | + Time_Out | + Other_Failure of string +fun string_of_failure ctxt (Counterexample (real, ex)) = + let + val msg = if real then "Counterexample found" + else "Potential counterexample found" + in + if null ex then msg ^ "." + else Pretty.string_of (Pretty.big_list (msg ^ ":") + (map (Syntax.pretty_term ctxt) ex)) + end + | string_of_failure _ Time_Out = "Time out." + | string_of_failure _ (Other_Failure msg) = msg + +exception SMT of failure type interface = { extra_norm: SMT_Normalize.extra_norm, translate: SMT_Translate.config } +datatype outcome = Unsat | Sat | Unknown + type solver_config = { - command: {env_var: string, remote_name: string option}, - arguments: string list, + name: string, + env_var: string, + is_remote: bool, + options: Proof.context -> string list, interface: interface, - reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> - (int list * thm) * Proof.context } + outcome: string -> string list -> outcome * string list, + cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> + term list) option, + reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> + (int list * thm) * Proof.context) option } (* SMT options *) +val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true) + +val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false) + val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30) fun with_timeout ctxt f x = TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x - handle TimeLimit.TimeOut => raise SMT "timeout" + handle TimeLimit.TimeOut => raise SMT Time_Out val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false) fun trace_msg ctxt f x = if Config.get ctxt trace then tracing (f x) else () +val (trace_used_facts, setup_trace_used_facts) = + Attrib.config_bool "smt_trace_used_facts" (K false) (* SMT certificates *) @@ -115,21 +154,20 @@ local -fun choose {env_var, remote_name} = +fun choose (env_var, is_remote, remote_name) = let val local_solver = getenv env_var - val remote_solver = the_default "" remote_name val remote_url = getenv "REMOTE_SMT_URL" in if local_solver <> "" then (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ..."); [local_solver]) - else if remote_solver <> "" + else if is_remote then - (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^ + (tracing ("Invoking remote SMT solver " ^ quote remote_name ^ " at " ^ quote remote_url ^ " ..."); - [getenv "REMOTE_SMT", remote_solver]) + [getenv "REMOTE_SMT", remote_name]) else error ("Undefined Isabelle environment variable: " ^ quote env_var) end @@ -181,30 +219,46 @@ Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () end -fun invoke translate_config comments command arguments irules ctxt = - irules - |> SMT_Translate.translate translate_config ctxt comments - ||> tap (trace_recon_data ctxt) - |>> run_solver ctxt command arguments - |> rpair ctxt +fun invoke translate_config name cmd more_opts options irules ctxt = + let + val args = more_opts @ options ctxt + val comments = ("solver: " ^ name) :: + ("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: + "arguments:" :: args + in + irules + |> SMT_Translate.translate translate_config ctxt comments + ||> tap (trace_recon_data ctxt) + |>> run_solver ctxt cmd args + |> rpair ctxt + end fun discharge_definitions thm = if Thm.nprems_of thm = 0 then thm else discharge_definitions (@{thm reflexive} RS thm) -fun gen_solver name solver ctxt prems = +fun set_has_datatypes with_datatypes translate = let - val {command, arguments, interface, reconstruct} = solver ctxt - val comments = ("solver: " ^ name) :: - ("timeout: " ^ string_of_int (Config.get ctxt timeout)) :: - "arguments:" :: arguments + val {prefixes, header, strict, builtins, serialize} = translate + val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins + val with_datatypes' = has_datatypes andalso with_datatypes + val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num, + builtin_fun=builtin_fun, has_datatypes=with_datatypes} + val translate' = {prefixes=prefixes, header=header, strict=strict, + builtins=builtins', serialize=serialize} + in (with_datatypes', translate') end + +fun gen_solver name info ctxt irules = + let + val {env_var, is_remote, options, more_options, interface, reconstruct} = + info val {extra_norm, translate} = interface - val {builtins, ...} = translate - val {has_datatypes, ...} = builtins + val (with_datatypes, translate') = + set_has_datatypes (Config.get ctxt datatypes) translate in - (prems, ctxt) - |-> SMT_Normalize.normalize extra_norm has_datatypes - |-> invoke translate comments command arguments + (irules, ctxt) + |-> SMT_Normalize.normalize extra_norm with_datatypes + |-> invoke translate' name (env_var, is_remote, name) more_options options |-> reconstruct |-> (fn (idxs, thm) => fn ctxt' => thm |> singleton (ProofContext.export ctxt' ctxt) @@ -217,11 +271,19 @@ (* solver store *) type solver = Proof.context -> (int * thm) list -> int list * thm -type solver_info = Context.generic -> Pretty.T list + +type solver_info = { + env_var: string, + is_remote: bool, + options: Proof.context -> string list, + more_options: string list, + interface: interface, + reconstruct: string list * SMT_Translate.recon -> Proof.context -> + (int list * thm) * Proof.context } structure Solvers = Generic_Data ( - type T = ((Proof.context -> solver_config) * solver_info) Symtab.table + type T = solver_info Symtab.table val empty = Symtab.empty val extend = I fun merge data = Symtab.merge (K true) data @@ -229,10 +291,48 @@ ) val no_solver = "(none)" -val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K [])) + +fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn + {env_var, is_remote, options, interface, reconstruct, ...} => + {env_var=env_var, is_remote=is_remote, options=options, + more_options=String.tokens (Symbol.is_ascii_blank o str) opts, + interface=interface, reconstruct=reconstruct})) + +local + fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt = + (case outcome output of + (Unsat, ls) => + if not (Config.get ctxt oracle) andalso is_some reconstruct + then the reconstruct ctxt recon ls + else (([], ocl ()), ctxt) + | (result, ls) => + let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => []) + in raise SMT (Counterexample (result = Sat, ts)) end) +in + +fun add_solver cfg = + let + val {name, env_var, is_remote, options, interface, outcome, cex_parser, + reconstruct} = cfg + + fun core_oracle () = @{cprop False} + + fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, + more_options=[], interface=interface, + reconstruct=finish (outcome name) cex_parser reconstruct ocl } + in + Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => + Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> + Attrib.setup (Binding.name (name ^ "_options")) + (Scan.lift (Parse.$$$ "=" |-- Args.name) >> + (Thm.declaration_attribute o K o set_solver_options name)) + ("Additional command line options for SMT solver " ^ quote name) + end + +end + val all_solver_names_of = Symtab.keys o Solvers.get val lookup_solver = Symtab.lookup o Solvers.get -fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i))) @@ -256,7 +356,7 @@ fun raw_solver_of context name = (case lookup_solver context name of NONE => error "No SMT solver selected" - | SOME (s, _) => s) + | SOME s => s) fun solver_of context = let val name = solver_name_of context @@ -264,58 +364,57 @@ -(* SMT solver *) +(* SMT filter *) val has_topsort = Term.exists_type (Term.exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)) -fun smt_solver ctxt xrules = +fun smt_solver ctxt irules = (* without this test, we would run into problems when atomizing the rules: *) - if exists (has_topsort o Thm.prop_of o snd) xrules - then raise SMT "proof state contains the universal sort {}" - else + if exists (has_topsort o Thm.prop_of o snd) irules + then raise SMT (Other_Failure "proof state contains the universal sort {}") + else solver_of (Context.Proof ctxt) ctxt irules + +fun smt_filter st i xrules = + let + val {context, facts, goal} = Proof.goal st + val cprop = + Thm.cprem_of goal i + |> Thm.rhs_of o SMT_Normalize.atomize_conv context + |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg + val irs = map (pair ~1) (Thm.assume cprop :: facts) + in split_list xrules - ||>> solver_of (Context.Proof ctxt) ctxt o map_index I + ||>> solver_of (Context.Proof context) context o append irs o map_index I |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =)) - -fun smt_filter ctxt xrules = - (fst (smt_solver ctxt xrules), "") - handle SMT msg => ([], "SMT: " ^ msg) - | SMT_COUNTEREXAMPLE _ => ([], "SMT: potential counterexample") + |> rpair NONE o fst + end + handle SMT fail => ([], SOME fail) (* SMT tactic *) local - fun pretty_cex ctxt (real, ex) = - let - val msg = if real then "SMT: counterexample found" - else "SMT: potential counterexample found" - in - if null ex then msg ^ "." - else Pretty.string_of (Pretty.big_list (msg ^ ":") - (map (Syntax.pretty_term ctxt) ex)) - end - fun fail_tac f msg st = (f msg; Tactical.no_tac st) fun SAFE pass_exns tac ctxt i st = if pass_exns then tac ctxt i st - else (tac ctxt i st - handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st - | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st) + else (tac ctxt i st handle SMT fail => fail_tac + (trace_msg ctxt (prefix "SMT: ") o string_of_failure ctxt) fail st) in + fun smt_tac' pass_exns ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' Tactic.rtac @{thm ccontr} THEN' SUBPROOF (fn {context, prems, ...} => - let fun solve cx = snd (smt_solver cx (map (pair ()) (rules @ prems))) + let fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems))) in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt val smt_tac = smt_tac' false + end val smt_method = @@ -332,8 +431,11 @@ (Scan.lift (Parse.$$$ "=" |-- Args.name) >> (Thm.declaration_attribute o K o select_solver)) "SMT solver configuration" #> + setup_oracle #> + setup_datatypes #> setup_timeout #> setup_trace #> + setup_trace_used_facts #> setup_fixed_certificates #> Attrib.setup @{binding smt_certificates} (Scan.lift (Parse.$$$ "=" |-- Args.name) >> @@ -348,13 +450,12 @@ val t = string_of_int (Config.get_generic context timeout) val names = sort_strings (all_solver_names_of context) val ns = if null names then [no_solver] else names - val take_info = (fn (_, []) => NONE | info => SOME info) - val infos = - Solvers.get context - |> Symtab.dest - |> map_filter (fn (n, (_, info)) => take_info (n, info context)) - |> sort (prod_ord string_ord (K EQUAL)) - |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps) + val n = solver_name_of context + val opts = + (case Symtab.lookup (Solvers.get context) n of + NONE => [] + | SOME {more_options, options, ...} => + more_options @ options (Context.proof_of context)) val certs_filename = (case get_certificates_path context of SOME path => Path.implode path @@ -363,12 +464,14 @@ else "false" in Pretty.writeln (Pretty.big_list "SMT setup:" [ - Pretty.str ("Current SMT solver: " ^ solver_name_of context), + Pretty.str ("Current SMT solver: " ^ n), + Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), Pretty.str_list "Available SMT solvers: " "" ns, Pretty.str ("Current timeout: " ^ t ^ " seconds"), + Pretty.str ("With proofs: " ^ + (if Config.get_generic context oracle then "false" else "true")), Pretty.str ("Certificates cache: " ^ certs_filename), - Pretty.str ("Fixed certificates: " ^ fixed), - Pretty.big_list "Solver-specific settings:" infos]) + Pretty.str ("Fixed certificates: " ^ fixed)]) end val _ = diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Oct 26 11:45:12 2010 +0200 @@ -15,7 +15,7 @@ val add_builtins: builtins -> Context.generic -> Context.generic val add_logic: (term list -> string option) -> Context.generic -> Context.generic - val extra_norm: bool -> SMT_Normalize.extra_norm + val extra_norm: SMT_Normalize.extra_norm val interface: SMT_Solver.interface end @@ -283,7 +283,7 @@ (** interfaces **) val interface = { - extra_norm = extra_norm false, + extra_norm = extra_norm, translate = { prefixes = { sort_prefix = "S", diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/yices_solver.ML --- a/src/HOL/Tools/SMT/yices_solver.ML Tue Oct 26 11:39:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -(* Title: HOL/Tools/SMT/yices_solver.ML - Author: Sascha Boehme, TU Muenchen - -Interface of the SMT solver Yices. -*) - -signature YICES_SOLVER = -sig - val setup: theory -> theory -end - -structure Yices_Solver: YICES_SOLVER = -struct - -val solver_name = "yices" -val env_var = "YICES_SOLVER" - -val options = ["--smtlib"] - -fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, []) - -fun core_oracle (output, _) = - let - val empty_line = (fn "" => true | _ => false) - val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) - val (l, _) = split_first (snd (chop_while empty_line output)) - in - if String.isPrefix "unsat" l then @{cprop False} - else if String.isPrefix "sat" l then raise_cex true - else if String.isPrefix "unknown" l then raise_cex false - else raise SMT_Solver.SMT (solver_name ^ " failed") - end - -fun solver oracle _ = { - command = {env_var=env_var, remote_name=NONE}, - arguments = options, - interface = SMTLIB_Interface.interface, - reconstruct = pair o pair [] o oracle } - -val setup = - Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => - Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) - -end diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Oct 26 11:45:12 2010 +0200 @@ -8,7 +8,7 @@ sig type builtin_fun = string * typ -> term list -> (string * term list) option val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic - val interface: bool -> SMT_Solver.interface + val interface: SMT_Solver.interface datatype sym = Sym of string * sym list type mk_builtins = { @@ -95,8 +95,8 @@ is_some (z3_builtin_fun' ctxt c ts) orelse is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->)) -fun interface has_datatypes = { - extra_norm = extra_norm' has_datatypes, +val interface = { + extra_norm = extra_norm', translate = { prefixes = prefixes, strict = strict, @@ -105,7 +105,7 @@ builtin_typ = builtin_typ, builtin_num = builtin_num, builtin_fun = z3_builtin_fun', - has_datatypes = has_datatypes}, + has_datatypes = true}, serialize = serialize}} end diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/z3_proof_parser.ML --- a/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Oct 26 11:45:12 2010 +0200 @@ -240,8 +240,8 @@ (* core parser *) -fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^ - string_of_int line_no ^ "): " ^ msg) +fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure + ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg)) fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Oct 26 11:39:26 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Oct 26 11:45:12 2010 +0200 @@ -8,7 +8,7 @@ sig val add_z3_rule: thm -> Context.generic -> Context.generic val trace_assms: bool Config.T - val reconstruct: string list * SMT_Translate.recon -> Proof.context -> + val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> (int list * thm) * Proof.context val setup: theory -> theory end @@ -20,7 +20,8 @@ structure T = Z3_Proof_Tools structure L = Z3_Proof_Literals -fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg) +fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure + ("Z3 proof reconstruction: " ^ msg)) @@ -826,7 +827,7 @@ (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab))) end -fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt = +fun reconstruct ctxt {typs, terms, unfolds, assms} output = P.parse ctxt typs terms output |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab)) diff -r 539d07b00e5f -r 7f58a9a843c2 src/HOL/Tools/SMT/z3_solver.ML --- a/src/HOL/Tools/SMT/z3_solver.ML Tue Oct 26 11:39:26 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,87 +0,0 @@ -(* Title: HOL/Tools/SMT/z3_solver.ML - Author: Sascha Boehme, TU Muenchen - -Interface of the SMT solver Z3. -*) - -signature Z3_SOLVER = -sig - val proofs: bool Config.T - val options: string Config.T - val datatypes: bool Config.T - val setup: theory -> theory -end - -structure Z3_Solver: Z3_SOLVER = -struct - -val solver_name = "z3" -val env_var = "Z3_SOLVER" - -val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false) -val (options, options_setup) = Attrib.config_string "z3_options" (K "") -val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false) - -fun add xs ys = ys @ xs - -fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s - -fun get_options ctxt = - ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"] - |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"] - |> add (explode_options (Config.get ctxt options)) - -fun pretty_config context = [ - Pretty.str ("With proofs: " ^ - (if Config.get_generic context proofs then "true" else "false")), - Pretty.str ("Options: " ^ - space_implode " " (get_options (Context.proof_of context))) ] - -fun cmdline_options ctxt = - get_options ctxt - |> add ["-smt"] - -fun raise_cex ctxt real recon ls = - let val cex = Z3_Model.parse_counterex ctxt recon ls - in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end - -fun if_unsat f (output, recon) ctxt = - let - fun jnk l = - String.isPrefix "WARNING" l orelse - String.isPrefix "ERROR" l orelse - forall Symbol.is_ascii_blank (Symbol.explode l) - val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output)) - in - if String.isPrefix "unsat" l then f (ls, recon) ctxt - else if String.isPrefix "sat" l then raise_cex ctxt true recon ls - else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls - else raise SMT_Solver.SMT (solver_name ^ " failed") - end - -val core_oracle = uncurry (if_unsat (K (K @{cprop False}))) - -val prover = if_unsat Z3_Proof_Reconstruction.reconstruct - -fun solver oracle ctxt = - let - val with_datatypes = Config.get ctxt datatypes - val with_proof = not with_datatypes andalso Config.get ctxt proofs - (* FIXME: implement proof reconstruction for datatypes *) - in - {command = {env_var=env_var, remote_name=SOME solver_name}, - arguments = cmdline_options ctxt, - interface = Z3_Interface.interface with_datatypes, - reconstruct = - if with_proof then prover else (fn r => `(pair [] o oracle o pair r))} - end - -val setup = - proofs_setup #> - options_setup #> - datatypes_setup #> - Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => - Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #> - Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config)) - -end