diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml index 93962b98b7719075cdee6ef62388b7455b1b1578..05f8ce5c293961d7f36235d7115edb881ec31665 100644 --- a/src/debugger/debugger.ml +++ b/src/debugger/debugger.ml @@ -41,7 +41,6 @@ let printStatus () = print_endline ""; print_endline "Queue content:"; print_endline (CM.queuePrettyStatus ()); - print_endline ""; printResult () let rec repeat (n:int) (action: unit -> unit) = diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml index 54ed51e78c5833a63b2c745d97e46f9f54631e4e..e1cf97dfb1a824b0e2860f10f7ef5a1aa9ea4c1a 100644 --- a/src/lib/CoAlgMisc.ml +++ b/src/lib/CoAlgMisc.ml @@ -362,12 +362,6 @@ let doSatPropagation () = doPropagation := false; res -let queuePrettyStatus () = - (Printf.sprintf "Constraints: %d\n" (List.length !queueCnstrs)) - ^(Printf.sprintf "States: %d\n" (List.length !queueStates)) - ^(Printf.sprintf "Cores1: %d\n" (List.length !queueCores1)) - ^(Printf.sprintf "Cores2: %d\n" (List.length !queueCores2)) - (*****************************************************************************) (* "Module type" and a specific implementation of the graph *) (*****************************************************************************) @@ -475,7 +469,6 @@ let nextNodeIdx () : int = nodeCounter := oldVal + 1; oldVal - let stateMake sort bs exp = { sortS = sort; bsS = bs; statusS = Expandable; parentsS = []; childrenS = []; constraintsS = cssEmpty; expandFkt = exp; @@ -687,11 +680,16 @@ let coreToString core = (csetToString core.sortC cset):: lst in let constraints = cssFold helper core.constraintsC [] in + let children = + List.map (fun (st:state) -> string_of_int st.idx) core.childrenC + in "Core "^(string_of_int core.idx)^" {\n"^ " Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^ " " ^ bsetToString core.sortC core.bsC ^ "\n" ^ " Constraints: { "^(String.concat "\n " constraints)^" }\n"^ + " Children: { "^(String.concat + ", " children)^" }\n"^ "}" let stateToString (state:state): string = @@ -718,6 +716,21 @@ let stateToString (state:state): string = "\n " conclusionList)^" }\n"^ "}" +let queuePrettyStatus () = + let printList (sl : int list) : string = + String.concat ", " (List.map string_of_int sl) + in + (* TODO: are atFormulas always look-up-able for sort 0? *) + (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs)) + ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs)) + ^(Printf.sprintf "\n%d States: " (List.length !queueStates)) + ^(printList (List.map (fun (st:state) -> st.idx) !queueStates)) + ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1)) + ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1)) + ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2)) + ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2)) + ^"\n" +