Skip to content

TritModel.cc uses abc kissat. Include the necessary header.#10610

Open
hzeller wants to merge 1 commit into
The-OpenROAD-Project:masterfrom
hzeller:feature-20260608-kissat-inc
Open

TritModel.cc uses abc kissat. Include the necessary header.#10610
hzeller wants to merge 1 commit into
The-OpenROAD-Project:masterfrom
hzeller:feature-20260608-kissat-inc

Conversation

@hzeller

@hzeller hzeller commented Jun 8, 2026

Copy link
Copy Markdown
Collaborator

No description provided.

Signed-off-by: Henner Zeller <h.zeller@acm.org>
@hzeller hzeller requested a review from a team as a code owner June 8, 2026 14:25
@hzeller hzeller requested a review from povik June 8, 2026 14:25

@gemini-code-assist gemini-code-assist Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code Review

This pull request adds the #include "sat/kissat/kissat.h" header to src/syn/src/ir/TritModel.cc. I have no feedback to provide as there are no review comments.

extern void kissat_set_terminate(kissat* solver,
void* state,
int (*terminate)(void* state));
} // namespace abc

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Strictly speaking it's not necessary as we declare what we use here, and it's unlikely kissat's interface will ever change. By going the include way we'll pick up abc's global header (abc_global.h) with certain pragmas and macro definitions which might cause conflict, though we are exposed to abc's header in other parts of openroad anyway.

@hzeller what's motivating the include?

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Include what you use, essentially (also commonly known as IWYU).

It is dangerous to assume (and forward declare) a particular prototype (as it can change any time, and then you get weird issues), the best is to actually include the header, so we always include the corresponding headers to symbols. If there are issues with pragmas and macros, then we undef them or fix things upstream.

I stumbled upon it, as I ran the bant build cleaner and it suggested to remove @abc, as there is no header from abc included in any of the sources of //src/syn/src/ir, thus concluded that the abc dependency must be accidental and can be removed.

$ bant dwyu //src/syn/src/ir
buildozer 'remove deps @abc' //src/syn/src/ir

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree in general but here I think it's more likely we will run into some kind of issue with the abc headers than the kissat interface changing.

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What issue do you expect ? Things seem to compile nicely.

@povik povik left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

to resolve bant false positive

@hzeller

hzeller commented Jun 8, 2026

Copy link
Copy Markdown
Collaborator Author

Note, it is not a false positive, it is an actual positive: no abc header is included anywhere, so no dependency is added.

(you can tell bant to ignore that and not issue a removal, but that is only really for messed up projects; I prefer to fix the project instead :) ).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants