From 488cea0f18f4172e67fb4d0d91daf7717015a5b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 5 Feb 2015 16:11:57 +1100
Subject: [PATCH] Implement queue printing
---
src/debugger/debugger.ml | 1 -
src/lib/CoAlgMisc.ml | 27 ++++++++++++++++++++-------
2 files changed, 20 insertions(+), 8 deletions(-)
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index 93962b9..05f8ce5 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 54ed51e..e1cf97d 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"
+
--
GitLab