Refactored to singleton logger by KlevisImeri · Pull Request #483 · ftsrg/theta

KlevisImeri · 2026-03-03T01:39:20Z

PR: Logger singleton

Read Logging.md

leventeBajczi

Thanks for the changes, I think these really help clear up the logging infrastructure of Theta!
I've skimmed through the changes, and these were my initial impressions. Please take a look -- but overall, I'm really happy with this PR.

leventeBajczi · 2026-03-04T08:11:24Z

+
+    @Parameter(
+            names = {"--grep", "-grep"},
+            description = "Log type pattern for the new logger API")


Saying "new" won't age well, just say "Log type pattern" -- also, add a line of documentation on its use with an example (either here as a comment, or in one of the doc markdown files)

Also, explicitly say that either this pattern, or -- if not given -- the loglevel takes effect, but never their conjunction.

leventeBajczi · 2026-03-04T08:19:03Z

I will need to take a closer look at this file. However, what I can already say, is that I don't like to see "yices" here -- that is very specific to one half-supported SMT solver. Can you give a reason why that is here, but no other solver is?

That is just me trying to use the logger and giving an example how I accept it to be used in the future. Yices is not special at all its just where I spend more time trying to find a workaround to the SSL expired certificate problem, and therefore I used the logger their more extensively so I can also use it as a concreate example. The main idea is that eventually every class will have a type. (and also subtypes with in the that class type, is a tree of types with "grep" used to query it).

Lets suppose that I want to get the logs inside the CegarChecker. I would put as type:

INFO_CEGARCHECKER -> create a func infoCegarChecker

MAINSTEP_CEGARCHECKER -> create a func mainstepCegarChecker

SUBSTEP_CEGARCHECKER -> create a func substepCegarChecker
when I initialize with Logger.init("MAINSTEP|SUBSTEP") I would have both the MAINSTEP_CEGARCHECKER, SUBSTEP_CEGARCHECKER (and all the other types that have a substring of MAINSTEP and SUBSTEP). But if I want only CEGARCHECKER then Logger.init("CEGARCHECKER") and it will show SUBSTEP_CEGARCHECKER, MAINSTEP_CEGARCHECKER and INFO_CEGARCHECKER.

Sorry I didn't do it justice explaining how it works. I will have to write better docs.

So, familiarizing myself with the logger, the main idea is that you have a more complex filtering than just a few levels of increasing verbosity. I think the filtering side (how you use --grep) is mostly clear to me.

My question is rather about how and where the possible values that are filtered are defined.

Here is what I understand about that:
I see the logTypes in the logger. I see that level is passed as a string to the log method and I see the enabled set. I can see that enabled just contains all matches of logTypes to the regex from --grep.

I think what Levi did not like (or will not like? :D ) is that someone implementing something new - let's say a new checker - will have to think about adding stuff in the logger. So the logger becomes cluttered with information from literally everywhere in Theta, and logTypes becomes huge.

I did not fully think the solution through, but I think there are roughly two directions:

the central logTypes collection of all the log types is avoided and these values should be distributed, e.g., per class/per file. Something like STMT_LABELs and things like that - an extra "utility" constant. Pro: if I develop a new checker, I just add a constant or two and I instantly have a working, customized logger; (BIG) Con: extra constant value in practically every file

I think the other solution is to just keep logTypes, expect it to be huge and try to make that usable and maintainable - put it in it's own file and somehow make it foolproof in a way so that I don't forget to add my new log values to the new log checker

Also, the question is: how much do we plan to fill up logTypes right now? Do we want to 1) go through a lot of places and add a lot of custom log types OR 2) do we do it gradually - e.g., you add what you needed (yices, cegar, whatever) and the next person who needs it elsewhere, say IC3, can add it there. I would prefer the latter - just with some really well shown / highlighted doc, so that people know that they can do this?

(I'm curious about everyone's and anyone's input on this.)

I prefer having one file witch contains all the logTypes (option 2). I like it more for maintainability. Why?

You can simply answer the question without searching the codebase: What logger types can I use?

How can i use a logger type in many places in the codebase, in other words how do I pass the logger type around?

the central logTypes collection of all the log types is avoided and these values should be distributed, e.g., per class/per file. Something like STMT_LABELs and things like that - an extra "utility" constant. Pro: if I develop a new checker, I just add a constant or two and I instantly have a working, customized logger; (BIG) Con: extra constant value in practically every file

Not flexible enough. With other central types you can make whatever type you like it does not depend on the class or file, IT DEPENDS ON THE CONTEXT.

I think the other solution is to just keep logTypes, expect it to be huge and try to make that usable and maintainable - put it in it's own file and somehow make it foolproof in a way so that I don't forget to add my new log values to the new log checker

I think adding a new logger type is very simple. One constant + 1 boilerplate func.

Also, the question is: how much do we plan to fill up logTypes right now? Do we want to 1) go through a lot of places and add a lot of custom log types OR 2) do we do it gradually - e.g., you add what you needed (yices, cegar, whatever) and the next person who needs it elsewhere, say IC3, can add it there. I would prefer the latter - just with some really well shown / highlighted doc, so that people know that they can do this?

Doing it gradually is better cause the log types depend on the contex not the class so its not very simple to add, you have to understand that part of code. Therefore, refactoring all of it right now is like an "impossible" task.
Adding better docs is better.

KlevisImeri · 2026-03-04T09:26:10Z

Thanks for the changes, I think these really help clear up the logging infrastructure of Theta! I've skimmed through the changes, and these were my initial impressions. Please take a look -- but overall, I'm really happy with this PR.

This PR is barely finished I just wanted a review if the API is nice and fits theta's ecosystem and mindset.
If happy with the idea then I will fix every detail and have a complete nice PR, cause this one has a lot of "leftovers" which have to be cleaned up.
And also thank you for the review!

mondokm · 2026-03-04T15:55:17Z

Thank you for the PR, this is something that was needed for a while now:D

Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum
"LegacyLevel"
"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

mondokm · 2026-03-04T15:59:53Z

Thank you for the PR, this is something that was needed for a while now:D

Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum

"LegacyLevel"

"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

Also I think it would be better to arrive on one option instead of having "grep", "log" and "loglevel" on the CLI interfaces. We have proper versioning, so we don't necessarily have to stick to older CLI parameters.

AdamZsofi · 2026-03-04T20:36:17Z

Thank you for the PR, this is something that was needed for a while now:D
Levi commented above that he would like to see "new" gone from the CLI parameter descriptions. I think this is something that we should go even further with and completely avoid maintaining both a "new" and "old/legacy" logging system, and instead remove the legacy logging completely, including:

the deprecated "Level" enum

"LegacyLevel"

"initOld"

If we reach a stable new logging system that can provide everything the legacy logging did, I think there is no need to maintain the legacy parts, they would only lead to confusion.

Also I think it would be better to arrive on one option instead of having "grep", "log" and "loglevel" on the CLI interfaces. We have proper versioning, so we don't necessarily have to stick to older CLI parameters.

Maybe it's just nostalgia, but I would vouch to keep the current loglevel flag. :D But I agree that we should only have one flag. If it can do complex regex expressions then it can do simple ones as well, so maybe with a different syntax, but it can still express what the old levels expressed.

And I agree about being able to change the flag syntax due to versioning.

KlevisImeri · 2026-03-05T09:16:22Z

@AdamZsofi To implement the Legacy (old flags) I just translated them to the appropriate regex expressions for the "grep" API.

…disable support - Replace multiple Logger classes (BaseLogger, ConsoleLogger, FileLogger, NullLogger, UniqueWarningLogger) with a single Kotlin object Logger - Add Logger.enabled.kt / Logger.disabled.kt templates for compile-time logging toggle via -PnoLogging - Make Level enum public, remove isEnabled(String) overload - Update all call sites across analysis algorithms, CLI tools, tests, and solver installers to use the new Logger API - Fix corrupted StsMddCheckerTest.java (missing block comment opener) - Remove stale bin/.gitignore files - Add Logging.md documentation

KlevisImeri · 2026-04-07T01:50:00Z

I finished refactoring all the logger to a singleton:

Removed the legacy API completely
Wrote the Logging.md documentation
Refactored parts that the logger was beings passed as function parameter
Clean any bad leftovers from debugging.
Reviewed the whole pull request one more time.
Added the -PnoLogging build time flag so we can build with 0 logging overhead.

Another important thing is that I could see .gitignore files inside the **/bin/ i removed them from there and adde bin in the root .gitignore.

AdamZsofi · 2026-06-08T13:10:48Z

@KlevisImeri
Can you please

fix the conflicts
check and "resolve conversation" in the above reviews if they are not relevant anymore?

I'll do a second review on this in the meantime sometime.

AdamZsofi · 2026-06-08T13:38:45Z

Just to make it clear: log levels are still built upon each other, i.e., init to BENCHMARK will still log error, warn, etc., right?

I removed that, but I can add it back. I just left it as a regex string. More simple.

AdamZsofi · 2026-06-08T13:46:22Z

@@ -0,0 +1,277 @@
+/*


This is what I was looking for to understand the logger, great! Can you maybe reference these tests as examples in the doc?

That is a great idea.

AdamZsofi · 2026-06-08T13:51:14Z


-        @Parameter(names = "--loglevel", description = "Detailedness of logging")
-        Logger.Level logLevel = Logger.Level.MAINSTEP;
+        @Parameter(names = "--loglevel", description = "Regex pattern for log levels (e.g. ERROR|WARN|INFO)")


Okay, so, connecting to my first comment, I think I understand the logger itself now.
AFAIK if you say "INFO", it will ONLY display the info level logs, nothing else above/below - that is of course necessary to be able to set the granularity, regex, etc.

But maybe we misunderstood each other: on the clis, if I say "INFO" in --loglevel, I think I still actually want "INFO|everything below INFO", as it was before the refactor. I don't want to list all the levels. This is still the most common use case, so I don't think it can change.

(Am I correct with above or did I manage to misunderstand the whole thing?)

(This goes for all the other CLIs as well. I think some earlier reviews addressed this as well.)

I can design such that if it says INFO i get only the "INFO|+everything below" but that means you have two user interfaces.
I mean how do you design the cli interface such that the user can ask both "INFO|+everything below" and just "INFO"?

The way maybe that it woudl be nicer is instead of calling --loglevel I woudl just call it --log. So for:

"INFO|+everything below": ./theta --log -level INFO

"INFO": ./theta --log "INFO"

…arams

…ing and copyright

Refactored to the singleton logger but still some solver issues in tests

db5f0c3

AdamZsofi self-assigned this Mar 3, 2026

KlevisImeri marked this pull request as draft March 3, 2026 14:25

leventeBajczi reviewed Mar 4, 2026

View reviewed changes

KlevisImeri added 2 commits April 6, 2026 19:25

Merge master into refactor/singleton-logger

8e349ae

KlevisImeri marked this pull request as ready for review April 7, 2026 01:56

Fix typo

5ded3f5

AdamZsofi requested changes Jun 8, 2026

View reviewed changes

KlevisImeri and others added 2 commits June 8, 2026 20:36

Merge branch 'master' into refactor/singleton-logger

d1ad666

Fix singleton Logger: safe close, reset on reinit, remove redundant p…

5058547

…arams

KlevisImeri marked this pull request as draft June 8, 2026 20:48

Fix typo, add LoggerTest reference to docs, bump version, fix formatt…

a87e6d9

…ing and copyright

Conversation

KlevisImeri commented Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR: Logger singleton

Uh oh!

leventeBajczi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AdamZsofi Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

KlevisImeri commented Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mondokm commented Mar 4, 2026

Uh oh!

mondokm commented Mar 4, 2026

Uh oh!

AdamZsofi commented Mar 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

KlevisImeri commented Mar 5, 2026

Uh oh!

KlevisImeri commented Apr 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

AdamZsofi commented Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

KlevisImeri Jun 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

KlevisImeri commented Mar 3, 2026 •

edited

Loading

KlevisImeri Mar 4, 2026 •

edited

Loading

AdamZsofi Mar 4, 2026 •

edited

Loading

KlevisImeri Jun 8, 2026 •

edited

Loading

KlevisImeri commented Mar 4, 2026 •

edited

Loading

AdamZsofi commented Mar 4, 2026 •

edited

Loading

KlevisImeri commented Apr 7, 2026 •

edited

Loading

AdamZsofi commented Jun 8, 2026 •

edited

Loading

KlevisImeri Jun 8, 2026 •

edited

Loading

KlevisImeri Jun 8, 2026 •

edited

Loading