added 'satx' proof method to Try0
authorblanchet
Sun May 04 18:53:58 2014 +0200 (2014-05-04)
changeset 5685013a7bca533a3
parent 56849 474767f0173e
child 56851 35ff4ede3409
added 'satx' proof method to Try0
NEWS
src/HOL/Groebner_Basis.thy
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/Presburger.thy
src/HOL/Tools/sat_solver.ML
src/HOL/Tools/try0.ML
     1.1 --- a/NEWS	Sun May 04 18:50:42 2014 +0200
     1.2 +++ b/NEWS	Sun May 04 18:53:58 2014 +0200
     1.3 @@ -352,7 +352,10 @@
     1.4  * New internal SAT solver "dpll_p" that produces models and proof traces.
     1.5    This solver replaces the internal SAT solvers "enumerate" and "dpll".
     1.6    Applications that explicitly used one of these two SAT solvers should
     1.7 -  use "dpll_p" instead. Minor INCOMPATIBILITY.
     1.8 +  use "dpll_p" instead. In addition, "dpll_p" is now the default SAT
     1.9 +  solver for the "sat" and "satx" proof methods and corresponding tactics;
    1.10 +  the old default can be restored using
    1.11 +  "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
    1.12  
    1.13  * SMT module:
    1.14    * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
     2.1 --- a/src/HOL/Groebner_Basis.thy	Sun May 04 18:50:42 2014 +0200
     2.2 +++ b/src/HOL/Groebner_Basis.thy	Sun May 04 18:53:58 2014 +0200
     2.3 @@ -86,9 +86,4 @@
     2.4  declare zmod_eq_dvd_iff[algebra]
     2.5  declare nat_mod_eq_iff[algebra]
     2.6  
     2.7 -
     2.8 -subsection {* Try0 *}
     2.9 -
    2.10 -ML_file "Tools/try0.ML"
    2.11 -
    2.12  end
     3.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sun May 04 18:50:42 2014 +0200
     3.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sun May 04 18:53:58 2014 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4  quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
     3.5  
     3.6  (*
     3.7 -nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
     3.8 +nitpick_params [timeout = 5, sat_solver = MiniSat_JNI, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
     3.9  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
    3.10  *)
    3.11  
     4.1 --- a/src/HOL/Presburger.thy	Sun May 04 18:50:42 2014 +0200
     4.2 +++ b/src/HOL/Presburger.thy	Sun May 04 18:53:58 2014 +0200
     4.3 @@ -434,5 +434,9 @@
     4.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     4.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     4.6  
     4.7 +
     4.8 +subsection {* Try0 *}
     4.9 +
    4.10 +ML_file "Tools/try0.ML"
    4.11 +
    4.12  end
    4.13 -
     5.1 --- a/src/HOL/Tools/sat_solver.ML	Sun May 04 18:50:42 2014 +0200
     5.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun May 04 18:53:58 2014 +0200
     5.3 @@ -1032,4 +1032,3 @@
     5.4  in
     5.5    SatSolver.add_solver ("jerusat", jerusat)
     5.6  end;
     5.7 -
     6.1 --- a/src/HOL/Tools/try0.ML	Sun May 04 18:50:42 2014 +0200
     6.2 +++ b/src/HOL/Tools/try0.ML	Sun May 04 18:53:58 2014 +0200
     6.3 @@ -100,7 +100,8 @@
     6.4     ("fast", ((false, false), clas_attrs)),
     6.5     ("fastforce", ((false, false), full_attrs)),
     6.6     ("force", ((false, false), full_attrs)),
     6.7 -   ("meson", ((false, false), metis_attrs))]
     6.8 +   ("meson", ((false, false), metis_attrs)),
     6.9 +   ("satx", ((false, false), no_attrs))];
    6.10  
    6.11  val apply_methods = map apply_named_method named_methods;
    6.12