--- a/NEWS Sun May 04 18:50:42 2014 +0200
+++ b/NEWS Sun May 04 18:53:58 2014 +0200
@@ -352,7 +352,10 @@
* New internal SAT solver "dpll_p" that produces models and proof traces.
This solver replaces the internal SAT solvers "enumerate" and "dpll".
Applications that explicitly used one of these two SAT solvers should
- use "dpll_p" instead. Minor INCOMPATIBILITY.
+ use "dpll_p" instead. In addition, "dpll_p" is now the default SAT
+ solver for the "sat" and "satx" proof methods and corresponding tactics;
+ the old default can be restored using
+ "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
* SMT module:
* A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
--- a/src/HOL/Groebner_Basis.thy Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy Sun May 04 18:53:58 2014 +0200
@@ -86,9 +86,4 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
-
-subsection {* Try0 *}
-
-ML_file "Tools/try0.ML"
-
end
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Sun May 04 18:53:58 2014 +0200
@@ -23,7 +23,7 @@
quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
(*
-nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
+nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
--- a/src/HOL/Presburger.thy Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Presburger.thy Sun May 04 18:53:58 2014 +0200
@@ -434,5 +434,9 @@
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+
+subsection {* Try0 *}
+
+ML_file "Tools/try0.ML"
+
end
-
--- a/src/HOL/Tools/sat_solver.ML Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sun May 04 18:53:58 2014 +0200
@@ -1032,4 +1032,3 @@
in
SatSolver.add_solver ("jerusat", jerusat)
end;
-
--- a/src/HOL/Tools/try0.ML Sun May 04 18:50:42 2014 +0200
+++ b/src/HOL/Tools/try0.ML Sun May 04 18:53:58 2014 +0200
@@ -100,7 +100,8 @@
("fast", ((false, false), clas_attrs)),
("fastforce", ((false, false), full_attrs)),
("force", ((false, false), full_attrs)),
- ("meson", ((false, false), metis_attrs))]
+ ("meson", ((false, false), metis_attrs)),
+ ("satx", ((false, false), no_attrs))];
val apply_methods = map apply_named_method named_methods;