From 9c009929ddfa061934533a384f02afd4604e79d7 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 15 Jun 2023 10:53:29 +0200
Subject: [PATCH] [interpretation] Log the resulting interpreted formula for
 debugging.

---
 src/interpretation.ml |  3 +++
 src/logging.ml        | 12 +++++++++++-
 src/logging.mli       |  1 +
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/interpretation.ml b/src/interpretation.ml
index 4d5af8b..7e0bddf 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -373,6 +373,9 @@ let interpret_task ~cwd env task =
   in
   let g, f = (Task.task_goal task, Task.task_goal_fmla task) in
   let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
+  Logs.debug ~src:Logging.src_interpret_goal (fun m ->
+    m "Interpreted formula for goal '%a':@.%a@.%a" Pretty.print_pr g
+      Pretty.print_term f print_caisar_op_of_ls caisar_env);
   let _, task = Task.task_separate_goal task in
   let task = declare_language_lsymbols caisar_env task in
   let task = Task.(add_prop_decl task Pgoal g f) in
diff --git a/src/logging.ml b/src/logging.ml
index f15df62..049a3d7 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -26,10 +26,20 @@ let src_prover_spec =
   Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"
 
 let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"
+
+let src_interpret_goal =
+  Logs.Src.create "InterpretGoal" ~doc:"Goal interpretation"
+
 let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
 
 let all_srcs () =
-  [ src_autodetect; src_prover_spec; src_prover_call; src_stack_trace ]
+  [
+    src_autodetect;
+    src_prover_spec;
+    src_prover_call;
+    src_interpret_goal;
+    src_stack_trace;
+  ]
 
 let is_debug_level src =
   match Logs.Src.level src with Some Debug -> true | _ -> false
diff --git a/src/logging.mli b/src/logging.mli
index 48e43c3..315bbc7 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -25,6 +25,7 @@
 val src_autodetect : Logs.src
 val src_prover_spec : Logs.src
 val src_prover_call : Logs.src
+val src_interpret_goal : Logs.src
 val src_stack_trace : Logs.src
 
 val all_srcs : unit -> Logs.src list
-- 
GitLab