renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish

--- a/NEWS	Sun May 04 18:53:58 2014 +0200
+++ b/NEWS	Sun May 04 18:57:45 2014 +0200
@@ -349,10 +349,10 @@
 * Theory reorganizations:
   * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
 
-* New internal SAT solver "dpll_p" that produces models and proof traces.
+* New internal SAT solver "cdclite" 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. In addition, "dpll_p" is now the default SAT
+  use "cdclite" instead. In addition, "cdclite" 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.

--- a/src/HOL/Library/refute.ML	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/Library/refute.ML	Sun May 04 18:57:45 2014 +0200
@@ -1068,7 +1068,7 @@
             val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
             val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
             val _ =
-              (if member (op =) ["dpll_p"] satsolver then
+              (if member (op =) ["cdclite"] satsolver then
                 warning ("Using SAT solver " ^ quote satsolver ^
                          "; for better performance, consider installing an \
                          \external solver.")

--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sun May 04 18:57:45 2014 +0200
@@ -574,7 +574,7 @@
         (* use the first ML solver (to avoid startup overhead) *)
         val (ml_solvers, nonml_solvers) =
           SatSolver.get_solvers ()
-          |> List.partition (member (op =) ["dptsat", "dpll_p"] o fst)
+          |> List.partition (member (op =) ["dptsat", "cdclite"] o fst)
         val res =
           if null nonml_solvers then
             TimeLimit.timeLimit tac_timeout (snd (hd ml_solvers)) prop

--- a/src/HOL/Tools/SMT2/smt2_config.ML	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Sun May 04 18:57:45 2014 +0200
@@ -161,7 +161,7 @@
 val infer_triggers = Attrib.setup_config_bool @{binding smt2_infer_triggers} (K false)
 val filter_only_facts = Attrib.setup_config_bool @{binding smt2_filter_only_facts} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt2_debug_files} (K "")
-val sat_solver = Attrib.setup_config_string @{binding smt2_sat_solver} (K "dpll_p")
+val sat_solver = Attrib.setup_config_string @{binding smt2_sat_solver} (K "cdclite")
 
 
 (* diagnostics *)

--- a/src/HOL/Tools/sat.ML	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/Tools/sat.ML	Sun May 04 18:57:45 2014 +0200
@@ -65,7 +65,7 @@
 fun cond_tracing ctxt msg =
   if Config.get ctxt trace then tracing (msg ()) else ();
 
-val solver = Attrib.setup_config_string @{binding sat_solver} (K "dpll_p");
+val solver = Attrib.setup_config_string @{binding sat_solver} (K "cdclite");
   (*see HOL/Tools/sat_solver.ML for possible values*)
 
 val counter = Unsynchronized.ref 0;

--- a/src/HOL/Tools/sat_solver.ML	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sun May 04 18:57:45 2014 +0200
@@ -384,7 +384,7 @@
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
-(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' --   *)
+(* Internal SAT solver, available as 'SatSolver.invoke_solver "cdclite"' --  *)
 (* a simplified implementation of the conflict-driven clause-learning        *)
 (* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean       *)
 (* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models  *)
@@ -575,7 +575,7 @@
     let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm
     in solve (clauses_of fm') end
 in
-  SatSolver.add_solver ("dpll_p", dpll_solver)
+  SatSolver.add_solver ("cdclite", dpll_solver)
 end;
 
 (* ------------------------------------------------------------------------- *)

--- a/src/HOL/ex/Refute_Examples.thy	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Sun May 04 18:57:45 2014 +0200
@@ -11,7 +11,7 @@
 imports "~~/src/HOL/Library/Refute"
 begin
 
-refute_params [satsolver = "dpll_p"]
+refute_params [satsolver = "cdclite"]
 
 lemma "P \<and> Q"
 apply (rule conjI)
@@ -20,7 +20,7 @@
 refute [expect = genuine]    -- {* equivalent to 'refute 1' *}
   -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
 refute [maxsize = 5, expect = genuine]   -- {* we can override parameters ... *}
-refute [satsolver = "dpll_p", expect = genuine] 2
+refute [satsolver = "cdclite", expect = genuine] 2
   -- {* ... and specify a subgoal at the same time *}
 oops
 

--- a/src/HOL/ex/SAT_Examples.thy	Sun May 04 18:53:58 2014 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Sun May 04 18:57:45 2014 +0200
@@ -5,7 +5,8 @@
 
 header {* Examples for proof methods "sat" and "satx" *}
 
-theory SAT_Examples imports Main
+theory SAT_Examples
+imports Main
 begin
 
 (*
@@ -14,8 +15,6 @@
 declare [[sat_trace]]
 *)
 
-declare [[sat_solver = dpll_p]]
-
 lemma "True"
 by sat