src/HOL/Tools/sat_solver.ML
changeset 14999 2c39efba8f67
parent 14965 7155b319eafa
child 15040 ed574b4f7e70
equal deleted inserted replaced
14998:9606c6224933 14999:2c39efba8f67
    86 		fun cnf_number_of_clauses (And (fm1,fm2)) =
    86 		fun cnf_number_of_clauses (And (fm1,fm2)) =
    87 			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
    87 			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
    88 		  | cnf_number_of_clauses _ =
    88 		  | cnf_number_of_clauses _ =
    89 			1
    89 			1
    90 		(* prop_formula -> string *)
    90 		(* prop_formula -> string *)
    91 		fun cnf_string True =
    91 		fun cnf_string fm =
    92 			error "formula is not in CNF"
    92 		let
    93 		  | cnf_string False =
    93 			(* prop_formula -> string list -> string list *)
    94 			error "formula is not in CNF"
    94 			fun cnf_string_acc True acc =
    95 		  | cnf_string (BoolVar i) =
    95 				error "formula is not in CNF"
    96 			(assert (i>=1) "formula contains a variable index less than 1";
    96 			  | cnf_string_acc False acc =
    97 			string_of_int i)
    97 				error "formula is not in CNF"
    98 		  | cnf_string (Not fm) =
    98 			  | cnf_string_acc (BoolVar i) acc =
    99 			"-" ^ cnf_string fm
    99 				(assert (i>=1) "formula contains a variable index less than 1";
   100 		  | cnf_string (Or (fm1,fm2)) =
   100 				string_of_int i :: acc)
   101 			cnf_string fm1 ^ " " ^ cnf_string fm2
   101 			  | cnf_string_acc (Not (BoolVar i)) acc =
   102 		  | cnf_string (And (fm1,fm2)) =
   102 				"-" :: cnf_string_acc (BoolVar i) acc
   103 			cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
   103 			  | cnf_string_acc (Not _) acc =
       
   104 				error "formula is not in CNF"
       
   105 			  | cnf_string_acc (Or (fm1,fm2)) acc =
       
   106 				cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
       
   107 			  | cnf_string_acc (And (fm1,fm2)) acc =
       
   108 				cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
       
   109 		in
       
   110 			concat (cnf_string_acc fm [])
       
   111 		end
   104 	in
   112 	in
   105 		File.write path
   113 		File.write path
   106 			(let
   114 			(let
   107 				val fm'               = cnf_True_False_elim fm
   115 				val fm'               = cnf_True_False_elim fm
   108 				val number_of_vars    = maxidx fm'
   116 				val number_of_vars    = maxidx fm'
   109 				val number_of_clauses = cnf_number_of_clauses fm'
   117 				val number_of_clauses = cnf_number_of_clauses fm'
   110 				val cnfstring         = cnf_string fm'
       
   111 			in
   118 			in
   112 				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
   119 				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
   113 				"c (c) Tjark Weber\n" ^
   120 				"c (c) Tjark Weber\n" ^
   114 				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
   121 				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
   115 				cnfstring ^ " 0\n"
   122 				cnf_string fm' ^ " 0\n"
   116 			end)
   123 			end)
   117 	end;
   124 	end;
   118 
   125 
   119 (* ------------------------------------------------------------------------- *)
   126 (* ------------------------------------------------------------------------- *)
   120 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
   127 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
   126 	(* Path.T -> prop_formula -> unit *)
   133 	(* Path.T -> prop_formula -> unit *)
   127 
   134 
   128 	fun write_dimacs_sat_file path fm =
   135 	fun write_dimacs_sat_file path fm =
   129 	let
   136 	let
   130 		(* prop_formula -> string *)
   137 		(* prop_formula -> string *)
   131 		fun sat_string True =
   138 		fun sat_string fm =
   132 			"*()"
   139 		let
   133 		  | sat_string False =
   140 			(* prop_formula -> string list -> string list *)
   134 			"+()"
   141 			fun sat_string_acc True acc =
   135 		  | sat_string (BoolVar i) =
   142 				"*()" :: acc
   136 			(assert (i>=1) "formula contains a variable index less than 1";
   143 			  | sat_string_acc False acc =
   137 			string_of_int i)
   144 				"+()" :: acc
   138 		  | sat_string (Not fm) =
   145 			  | sat_string_acc (BoolVar i) acc =
   139 			"-(" ^ sat_string fm ^ ")"
   146 				(assert (i>=1) "formula contains a variable index less than 1";
   140 		  | sat_string (Or (fm1,fm2)) =
   147 				string_of_int i :: acc)
   141 			"+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
   148 			  | sat_string_acc (Not fm) acc =
   142 		  | sat_string (And (fm1,fm2)) =
   149 				"-(" :: sat_string_acc fm (")" :: acc)
   143 			"*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
   150 			  | sat_string_acc (Or (fm1,fm2)) acc =
       
   151 				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
       
   152 			  | sat_string_acc (And (fm1,fm2)) acc =
       
   153 				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
       
   154 		in
       
   155 			concat (sat_string_acc fm [])
       
   156 		end
   144 	in
   157 	in
   145 		File.write path
   158 		File.write path
   146 			(let
   159 			(let
   147 				val number_of_vars = Int.max (maxidx fm, 1)
   160 				val number_of_vars = Int.max (maxidx fm, 1)
   148 			in
   161 			in