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

Unsat core not working #311

Open
dkasak opened this issue Feb 5, 2025 · 2 comments
Open

Unsat core not working #311

dkasak opened this issue Feb 5, 2025 · 2 comments

Comments

@dkasak
Copy link
Contributor

dkasak commented Feb 5, 2025

How is unsat core supposed to work? Judging from http://alloytools.org/quickguide/unsat.html, it's supposed to highlight the core in red, but this is not happening for me.

One thing that's confusing me is that there's no MiniSat with Unsat Core solver in the latest release. However there is a minisat.solver which (is the only one that) enables the core minimization and granularity options, so I'm assuming this is what MiniSat with Unsat Core used to be and the documentation is just outdated.

However, running the following model highlights nothing (obtained as an example from here):

sig Node {
    edge: some Node
}

fact {some Node}

run {no edge}

Additionally, the right pane output doesn't contain any message like "Core reduced from ..." which is visible in the linked docs.

I'm beginning to suspect it's somehow broken, but maybe I'm just not holding it right.

@grayswandyr
Copy link
Contributor

Confirmed, there is an issue indeed, I stumbled upon it last week-end too. Thanks for reporting the issue.

@dkasak
Copy link
Contributor Author

dkasak commented Feb 10, 2025

I think when this is fixed, it would also be prudent to re-add the string "Unsat Core" to that solver's menu item. This will reduce confusion for people coming to Alloy from old articles that mention it by that name.

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

No branches or pull requests

2 participants