src/HOL/Tools/sat_solver.ML
changeset 14703 837d7180c39a
parent 14514 15abb7d42e2e
child 14753 f40b45db8cf0
equal deleted inserted replaced
14702:64844b4cc107 14703:837d7180c39a
   297 			  | partial_eval xs False            = False
   297 			  | partial_eval xs False            = False
   298 			  | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   298 			  | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   299 			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   299 			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   300 			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   300 			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   301 			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   301 			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   302 			  | partial_eval xs _                = raise ERROR  (* formula is not in negation normal form *)
       
   303 			(* prop_formula -> int list *)
   302 			(* prop_formula -> int list *)
   304 			fun forced_vars True              = []
   303 			fun forced_vars True              = []
   305 			  | forced_vars False             = []
   304 			  | forced_vars False             = []
   306 			  | forced_vars (BoolVar i)       = [i]
   305 			  | forced_vars (BoolVar i)       = [i]
   307 			  | forced_vars (Not (BoolVar i)) = [~i]
   306 			  | forced_vars (Not (BoolVar i)) = [~i]