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

Support for the check_sat statement in Dolmen frontend #594

Closed
wants to merge 4 commits into from

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Apr 24, 2023

The model PR add a new statement in the native language that is not present in Dolmen.

Do not merge before the PR Gbury/dolmen#140 is released.

@Halbaroth Halbaroth added this to the 2.5.0 milestone Apr 24, 2023
@bclement-ocp
Copy link
Collaborator

This doesn't seem to work?

6 | check_sat g :
                ^
Error Syntax error (state 336) while reading the reserved word ':'.

@Halbaroth
Copy link
Collaborator Author

You have to use my PR on dolmen also.

@bclement-ocp
Copy link
Collaborator

Ah, would have been good to mention. Gbury/dolmen#140

Looking at the code for the Solve case smtlib (below in solving_loop) it looks like we maybe should merge back the two cases if we have support for Solve in D_cnf?

@Halbaroth
Copy link
Collaborator Author

I applied the modifications :)

@bclement-ocp
Copy link
Collaborator

Is this compatible with the last changes to Gbury/dolmen#140? If so, please resolve the conflicts and I will take a look.

@bclement-ocp
Copy link
Collaborator

@Halbaroth Can you please resolve the conflicts with the next branch so that I can take a look? Thanks.

@Halbaroth Halbaroth marked this pull request as draft June 13, 2023 15:21
@Halbaroth Halbaroth marked this pull request as ready for review June 13, 2023 16:50
@Halbaroth
Copy link
Collaborator Author

It's ready :)

@bclement-ocp bclement-ocp self-requested a review June 14, 2023 04:57
@bclement-ocp bclement-ocp mentioned this pull request Jun 14, 2023
Copy link
Collaborator

@bclement-ocp bclement-ocp left a comment

Choose a reason for hiding this comment

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

Looks good to me with some minor changes, I'd say let's wait on #630 to make them and merge however.

@@ -50,10 +50,6 @@ In other word, `cut` and `check` allow to test if intermediate goals can be prov
<cut_declaration> ::= 'cut' <expr>
```

## `check_valid`

This keyword is an alias for `goal`.
Copy link
Collaborator

Choose a reason for hiding this comment

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

RIP

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We remove check_valid right?

Copy link
Collaborator

@bclement-ocp bclement-ocp Jun 15, 2023

Choose a reason for hiding this comment

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

Yes! RIP = Requiescat In Pace, I was semi-humorously paying respect to its short life :)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

:D very short! I know what RIP means by the way XD

loc;
}
| `Solve _ -> failwith "not yet supported"
| _ -> assert false
Copy link
Collaborator

Choose a reason for hiding this comment

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

I don't think this case is needed, OCaml should be able to infer that contents has type [ `Solve of _ list * _ list ] (there is no "this match case is unused" because with the match it gets inferred as [> `Solve of _list * _list] instead, it is a known limitation of polymorphic variants).

contents;
loc;
}
| `Solve _ -> failwith "not yet supported"
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
| `Solve _ -> failwith "not yet supported"
| `Solve _ -> failwith "Only `(check-sat)` with no arguments is supported."

match contents with
| `Solve ([], []) ->
let contents =
`Solve ([], [DStd.Expr.Term.(of_cst Const._false)])
Copy link
Collaborator

Choose a reason for hiding this comment

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

I am not a very big fan of passing the general form of `Solve to D_cnf.make, and then have D_cnf.make ignore some of the solves.

I think it would be better to keep `Goal` in `D_cnf.make` (see what I did in #630 ) and have a new constructor (maybe `Check``?) for the check-sat case.

@bclement-ocp
Copy link
Collaborator

These changes are included in #652 so closing in favor of #652

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Jun 19, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Jun 21, 2023
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Jun 23, 2023
bclement-ocp added a commit that referenced this pull request Jun 26, 2023
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