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.

Sign up for GitHub

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

Jump to bottom

Change satisfiable to valid in implication endpoint response #3601

Closed
goodlyrottenapple opened this issue Jun 9, 2023 · 1 comment
Closed

Change satisfiable to valid in implication endpoint response #3601

goodlyrottenapple opened this issue Jun 9, 2023 · 1 comment
Assignees
@goodlyrottenapple

Comments

@goodlyrottenapple
Copy link
Contributor

Technically we should return valid rather than satisfiable here:

haskell-backend/kore-rpc-types/src/Kore/JsonRpc/Types.hs

Line 142 in 740a60e

, satisfiable :: Bool

@nwatson22 nwatson22 mentioned this issue Jun 15, 2023
Open
@jberthold jberthold mentioned this issue Jun 19, 2023
Open
@jberthold jberthold mentioned this issue May 1, 2024
Merged
@goodlyrottenapple goodlyrottenapple mentioned this issue May 7, 2024
Merged
rv-jenkins pushed a commit that referenced this issue May 8, 2024
@goodlyrottenapple
Implies endpoint in booster (#3846)
a0ca443 
Closes #3778 #3601

This PR introduces a simple check implication implementation, which uses
the matching algorithm to try to find a substitution or fail to unify
the given configurations.

If matching the RHS configuration to the LHS succeeds and produces a
substitution σ, we filter out any predicates in the consequent which
appear in the antecedent and then check if all predicates in
σ(filtered_preds) evaluate to true/#top. (Question: do we want to apply
σ to the RHS preds before filtering?). With this simple algorithm, we
can successfully discharge almost 85% of implication checks in KEVM and
88% in Kontrol.

---------

Co-authored-by: github-actions <github-actions@github.com>
@geo2a
Copy link
Collaborator

geo2a commented May 10, 2024

Closed by #3846

@geo2a geo2a closed this as completed May 10, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@goodlyrottenapple goodlyrottenapple

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@geo2a @goodlyrottenapple