# HG changeset patch # User blanchet # Date 1402585322 -7200 # Node ID 2eb14982cd291f194527ed5b6a323b048bc0d93c # Parent b0b9a10e4bf42c88150cf58dcf883cea4f8abf71 made CVC3 work with SMT2 stack diff -r b0b9a10e4bf4 -r 2eb14982cd29 src/HOL/Tools/SMT2/smt2_systems.ML --- a/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 15:47:36 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 17:02:02 2014 +0200 @@ -31,9 +31,9 @@ " failed -- enable tracing using the " ^ quote (Config.name_of SMT2_Config.trace) ^ " option for details")) -fun on_first_line test_outcome solver_name lines = +fun on_first_nontrivial_line test_outcome solver_name lines = let - val empty_line = (fn "" => true | _ => false) + val empty_line = (fn "" => true | s => String.isPrefix "***" s) val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) val (l, ls) = split_first (snd (take_prefix empty_line lines)) in (test_outcome solver_name l, ls) end @@ -44,7 +44,7 @@ local fun cvc3_options ctxt = [ "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed), - "-lang", "smtlib", "-output-lang", "presentation", + "-lang", "smt2", "-output-lang", "presentation", "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))] in @@ -55,7 +55,7 @@ command = make_command "CVC3", options = cvc3_options, default_max_relevant = 400 (* FUDGE *), - outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), + outcome = on_first_nontrivial_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), parse_proof = NONE, replay = NONE } @@ -75,7 +75,7 @@ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)), "--smtlib"]), default_max_relevant = 350 (* FUDGE *), - outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), + outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"), parse_proof = NONE, replay = NONE } @@ -141,7 +141,7 @@ command = z3_make_command "Z3_NEW", options = z3_options, default_max_relevant = 350 (* FUDGE *), - outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), + outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"), parse_proof = SOME Z3_New_Replay.parse_proof, replay = SOME Z3_New_Replay.replay } diff -r b0b9a10e4bf4 -r 2eb14982cd29 src/HOL/Tools/SMT2/z3_new_interface.ML --- a/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Jun 12 15:47:36 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Jun 12 17:02:02 2014 +0200 @@ -31,11 +31,8 @@ local fun translate_config ctxt = - let - val {serialize, ...} = SMTLIB2_Interface.translate_config ctxt - in - {header=K "", serialize=serialize, has_datatypes=true} - end + {header = K "", has_datatypes = true, + serialize = #serialize (SMTLIB2_Interface.translate_config ctxt)} fun is_div_mod @{const div (int)} = true | is_div_mod @{const mod (int)} = true