Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Instantiating a universal whose variable does not appear in the formula results in an error #69

Open
connorjayr opened this issue Mar 24, 2022 · 1 comment
Labels
bug Something isn't working

Comments

@connorjayr
Copy link
Collaborator

The following decomposition in a truth tree results in an error:

forall x forall y P(y)
forall y P(y)

This is because the code does not know to what constant the user is trying to assign x. If the variable does not appear in the formula, the assignment code should assume an arbitrary value (which will necessarily be valid since the constant will not appear in the resulting formula).

@connorjayr connorjayr added the bug Something isn't working label Mar 24, 2022
@jputlock
Copy link
Collaborator

This fix does not introduce that new constant to the universe, but prevents crashing when running into this scenario.

@jputlock jputlock reopened this Mar 26, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants