--- a/Admin/isatest/settings/mac-poly-M4 Fri Oct 30 14:00:43 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M4 Fri Oct 30 14:02:42 2009 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/Admin/isatest/settings/mac-poly-M8 Fri Oct 30 14:00:43 2009 +0100
+++ b/Admin/isatest/settings/mac-poly-M8 Fri Oct 30 14:02:42 2009 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="--mutable 800 --immutable 2000"
--- a/src/HOL/SMT/Examples/cert/z3_arith_quant_18 Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_18 Fri Oct 30 14:02:42 2009 +0100
@@ -2,6 +2,6 @@
:extrafuns (
(uf_1 Int)
)
-:assumption (not (forall (?x1 Int) (implies (< ?x1 uf_1) (< (* 2 ?x1) (* 2 uf_1))) :pat{ ?x1 }))
+:assumption (not (forall (?x1 Int) (implies (< ?x1 uf_1) (< (* 2 ?x1) (* 2 uf_1))) :pat { ?x1 }))
:formula true
)
--- a/src/HOL/SMT/Tools/cvc3_solver.ML Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML Fri Oct 30 14:02:42 2009 +0100
@@ -15,8 +15,7 @@
val solver_name = "cvc3"
val env_var = "CVC3_SOLVER"
-val options =
- ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"]
+val options = ["-lang", "smtlib", "-output-lang", "presentation"]
val is_sat = String.isPrefix "Satisfiable."
val is_unsat = String.isPrefix "Unsatisfiable."
@@ -25,11 +24,7 @@
fun cex_kind true = "Counterexample"
| cex_kind false = "Possible counterexample"
-fun raise_cex real ctxt recon ls =
- let
- val ls' = filter_out (String.isPrefix "%") ls
- val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls')
- in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
let
@@ -38,8 +33,8 @@
val (l, ls) = split_first (dropwhile empty_line output)
in
if is_unsat l then @{cprop False}
- else if is_sat l then raise_cex true context recon ls
- else if is_unknown l then raise_cex false context recon ls
+ else if is_sat l then raise_cex true
+ else if is_unknown l then raise_cex false
else error (solver_name ^ " failed")
end
--- a/src/HOL/SMT/Tools/smt_normalize.ML Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Fri Oct 30 14:02:42 2009 +0100
@@ -318,7 +318,7 @@
fun replace ctxt cvs ct (cx as (nctxt, defs)) =
let
val cvs' = used_vars cvs ct
- val ct' = fold Thm.cabs cvs' ct
+ val ct' = fold_rev Thm.cabs cvs' ct
val mk_repl = fold (fn ct => fn cu => Thm.capply cu ct) cvs'
in
(case Termtab.lookup defs (Thm.term_of ct') of
--- a/src/HOL/SMT/Tools/smtlib_interface.ML Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML Fri Oct 30 14:02:42 2009 +0100
@@ -69,7 +69,6 @@
fun wr1 s = sep (wr s)
fun wrn f n = (fn [] => wr1 n | ts => par (wr n #> fold f ts))
-fun ins s f = (fn [] => I | x::xs => f x #> fold (fn x => wr1 s #> f x) xs)
val term_marker = "__term"
val formula_marker = "__form"
@@ -104,7 +103,7 @@
val wre = wr_expr loc (map (tvar o fst) (rev vs) @ env)
- fun wrp s ts = wr1 (":" ^ s ^ "{") #> ins "," wre ts #> wr1 "}"
+ fun wrp s ts = wr1 (":" ^ s ^ " {") #> fold wre ts #> wr1 "}"
fun wr_pat (T.SPat ts) = wrp "pat" ts
| wr_pat (T.SNoPat ts) = wrp "nopat" ts
in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
--- a/src/HOL/SMT/Tools/yices_solver.ML Fri Oct 30 14:00:43 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML Fri Oct 30 14:02:42 2009 +0100
@@ -15,14 +15,12 @@
val solver_name = "yices"
val env_var = "YICES_SOLVER"
-val options = ["--evidence", "--smtlib"]
+val options = ["--smtlib"]
fun cex_kind true = "Counterexample"
| cex_kind false = "Possible counterexample"
-fun raise_cex real ctxt rtab ls =
- let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
- in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
structure S = SMT_Solver
@@ -33,8 +31,8 @@
val (l, ls) = split_first (dropwhile empty_line output)
in
if String.isPrefix "unsat" l then @{cprop False}
- else if String.isPrefix "sat" l then raise_cex true context recon ls
- else if String.isPrefix "unknown" l then raise_cex false context recon ls
+ else if String.isPrefix "sat" l then raise_cex true
+ else if String.isPrefix "unknown" l then raise_cex false
else error (solver_name ^ " failed")
end