src/HOL/Tools/sat_solver.ML
changeset 15531 08c8dad8e399
parent 15332 0dc05858a862
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  	exception NOT_CONFIGURED;
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* type of partial (satisfying) assignments: 'a i = None' means that 'a' is  *)
     1.8 +(* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is  *)
     1.9  (*      a satisfying assigment regardless of the value of variable 'i'       *)
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  
    1.12 @@ -186,20 +186,20 @@
    1.13  
    1.14  	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
    1.15  	let
    1.16 -		(* 'a option -> 'a Library.option *)
    1.17 +		(* 'a option -> 'a option *)
    1.18  		fun option (SOME a) =
    1.19 -			Some a
    1.20 +			SOME a
    1.21  		  | option NONE =
    1.22 -			None
    1.23 +			NONE
    1.24  		(* string -> int list *)
    1.25  		fun int_list_from_string s =
    1.26  			mapfilter (option o Int.fromString) (space_explode " " s)
    1.27  		(* int list -> assignment *)
    1.28  		fun assignment_from_list [] i =
    1.29 -			None  (* the SAT solver didn't provide a value for this variable *)
    1.30 +			NONE  (* the SAT solver didn't provide a value for this variable *)
    1.31  		  | assignment_from_list (x::xs) i =
    1.32 -			if x=i then (Some true)
    1.33 -			else if x=(~i) then (Some false)
    1.34 +			if x=i then (SOME true)
    1.35 +			else if x=(~i) then (SOME false)
    1.36  			else assignment_from_list xs i
    1.37  		(* int list -> string list -> assignment *)
    1.38  		fun parse_assignment xs [] =
    1.39 @@ -365,27 +365,27 @@
    1.40  		(* int list -> int list -> int list option *)
    1.41  		(* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
    1.42  		fun next_list _ ([]:int list) =
    1.43 -			None
    1.44 +			NONE
    1.45  		  | next_list [] (y::ys) =
    1.46 -			Some [y]
    1.47 +			SOME [y]
    1.48  		  | next_list (x::xs) (y::ys) =
    1.49  			if x=y then
    1.50  				(* reset the bit, continue *)
    1.51  				next_list xs ys
    1.52  			else
    1.53  				(* set the lowest bit that wasn't set before, keep the higher bits *)
    1.54 -				Some (y::x::xs)
    1.55 +				SOME (y::x::xs)
    1.56  		(* int list -> int -> bool *)
    1.57  		fun assignment_from_list xs i =
    1.58  			i mem xs
    1.59  		(* int list -> SatSolver.result *)
    1.60  		fun solver_loop xs =
    1.61  			if PropLogic.eval (assignment_from_list xs) fm then
    1.62 -				SatSolver.SATISFIABLE (Some o (assignment_from_list xs))
    1.63 +				SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
    1.64  			else
    1.65  				(case next_list xs indices of
    1.66 -				  Some xs' => solver_loop xs'
    1.67 -				| None     => SatSolver.UNSATISFIABLE)
    1.68 +				  SOME xs' => solver_loop xs'
    1.69 +				| NONE     => SatSolver.UNSATISFIABLE)
    1.70  	in
    1.71  		(* start with the "first" assignment (all variables are interpreted as 'false') *)
    1.72  		solver_loop []
    1.73 @@ -454,29 +454,29 @@
    1.74  				val (xs', fm') = eval_and_force xs fm
    1.75  			in
    1.76  				case fm' of
    1.77 -				  True  => Some xs'
    1.78 -				| False => None
    1.79 +				  True  => SOME xs'
    1.80 +				| False => NONE
    1.81  				| _     =>
    1.82  					let
    1.83  						val x = the (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
    1.84  					in
    1.85  						case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
    1.86 -						  Some xs'' => Some xs''
    1.87 -						| None      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
    1.88 +						  SOME xs'' => SOME xs''
    1.89 +						| NONE      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
    1.90  					end
    1.91  			end
    1.92  			(* int list -> assignment *)
    1.93  			fun assignment_from_list [] i =
    1.94 -				None  (* the DPLL procedure didn't provide a value for this variable *)
    1.95 +				NONE  (* the DPLL procedure didn't provide a value for this variable *)
    1.96  			  | assignment_from_list (x::xs) i =
    1.97 -				if x=i then (Some true)
    1.98 -				else if x=(~i) then (Some false)
    1.99 +				if x=i then (SOME true)
   1.100 +				else if x=(~i) then (SOME false)
   1.101  				else assignment_from_list xs i
   1.102  		in
   1.103  			(* initially, no variable is interpreted yet *)
   1.104  			case dpll [] fm' of
   1.105 -			  Some assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   1.106 -			| None            => SatSolver.UNSATISFIABLE
   1.107 +			  SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   1.108 +			| NONE            => SatSolver.UNSATISFIABLE
   1.109  		end
   1.110  	end  (* local *)
   1.111  in