Skip to content

Conversation

daniel-larraz
Copy link
Contributor

cvc5 recently stopped using a singleton TermManager (see cvc5/cvc5#11816). As a consequence, the Pythonic API broke, since it relied on this behavior. This PR fixes the issue by establishing a one-to-one association between a Context and a TermManager, ensuring that each Context has its own TermManager and that every object uses the correct Context.

Copy link
Member

@alex-ozdemir alex-ozdemir left a comment

Choose a reason for hiding this comment

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

LGTM. Thanks for fixing this!

@daniel-larraz daniel-larraz merged commit bdab0ff into cvc5:main May 1, 2025
1 check passed
@caioraposo
Copy link

Hi @daniel-larraz, with these changes the PR #106 became obsolete due to it relying on the Context having a solver. I think the only way to go would be to keep both TermManager and Solver within Context, but I don't know if this is desirable. What do you think?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants