diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index f24844e9fec7a23036dd9d8e22da51c2a2997282..42f2685af16a267b1cdab7b6983f20fe8a5c1a54 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -146,7 +146,6 @@ let propagateSatMu () = setAddState setStates state; if bsetCompare (stateGetDeferral state) emptySet == 0 then begin - print_endline (stateToString state); setAddState setFinishingStates state end else () @@ -166,7 +165,6 @@ let propagateSatMu () = setAddCore setCores core; if bsetCompare (coreGetDeferral core) emptySet == 0 then begin - print_endline (coreToString core); setAddCore setFinishingCores core end else () @@ -190,11 +188,9 @@ let propagateSatMu () = let allowedCores = setEmptyCore () in let rec visitParentStates (core : core) : unit = - print_endline ("Looking at Core " ^ (string_of_int (coreGetIdx core))); if not (setMemCore allowedCores core) then begin setAddCore allowedCores core; - print_endline ("Adding Core " ^ (string_of_int (coreGetIdx core))); let verifyParent (state,_) = let rules = stateGetRules state in let ruleiter (dependencies, corelist) = @@ -203,17 +199,14 @@ let propagateSatMu () = in if List.for_all ruleiter rules then visitParentCores state - else print_endline ("Not considering state "^(string_of_int (stateGetIdx state))) in List.iter verifyParent (coreGetParents core) end and visitParentCores (state : state) : unit = - print_endline ("Looking at State " ^ (string_of_int (stateGetIdx state))); if not (setMemState allowedStates state) then begin setAddState allowedStates state; - print_endline ("Adding State " ^ (string_of_int (stateGetIdx state))); let verifyParent core = let acceptable = List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat) @@ -221,7 +214,6 @@ let propagateSatMu () = in if acceptable then visitParentStates core - else print_endline ("Not considering state "^(string_of_int (coreGetIdx core))) in List.iter verifyParent (stateGetParents state) end @@ -235,7 +227,6 @@ let propagateSatMu () = List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist in if not (List.exists ruleiter (stateGetRules state)) then begin - print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as proper starting node"); visitParentCores state end @@ -246,7 +237,6 @@ let propagateSatMu () = if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state)) (coreGetChildren core)) then begin - print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as proper starting node"); visitParentStates core end in