Skip to content

prop_conv_solvert: introduce scopes #4510

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
Merged
merged 4 commits into from
Jun 15, 2021
Merged

prop_conv_solvert: introduce scopes #4510

merged 4 commits into from
Jun 15, 2021

Conversation

kroening
Copy link
Member

This is the biggest change to the solver interface since it got added to the codebase.

Currently, bound identifiers (exists, forall, let) must be unique; the solver looses soundness if that assumption is violated.

This change introduces scopes, i.e., the uniqueness requirement is dropped. Nested scoping works as expected. This matches what SMT-LIB does, i.e., the renaming done in the SMT-LIB front-end can be dropped.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

peterschrammel
peterschrammel reviewed Apr 15, 2019
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

Looks OK. CI is failing, though.

@peterschrammel
Copy link
Member

Tests for prop_conv and smt2 would be required.

tautschnig
tautschnig requested changes Apr 15, 2019
View reviewed changes
@kroening kroening force-pushed the solver-scopes branch 4 times, most recently from e670983 to 412d755 Compare April 16, 2019 15:14
@kroening kroening force-pushed the solver-scopes branch 2 times, most recently from 3a8968d to 7503418 Compare April 16, 2019 18:13
@kroening
Copy link
Member Author

This will need #4931 to work.

@tautschnig tautschnig changed the title prop_conv_solvert: introduce scopes prop_conv_solvert: introduce scopes [depends-on: #4931] Aug 5, 2019
kroening pushed a commit that referenced this pull request Aug 6, 2019
Merge pull request #4931 from diffblue/binding
9a3ffde 
introduce binding_exprt [blocks: #4510]
@tautschnig tautschnig changed the title prop_conv_solvert: introduce scopes [depends-on: #4931] prop_conv_solvert: introduce scopes Aug 7, 2019
@kroening
Copy link
Member Author

This needs #4992.

Daniel Kroening added 2 commits June 15, 2021 10:56
@kroening
consolidate let-related tests for smt2_solver
58df539 
Now all in one directory.
@kroening
prop_conv_solvert: remove let conversion
028ac2c 
This removes the handling of let expressions from prop_conv_solvert to
prevent duplicating this functionality in boolbvt.
@kroening kroening assigned tautschnig and unassigned kroening Jun 15, 2021
tautschnig
tautschnig reviewed Jun 15, 2021
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

  1. See admin comments about what's being promised vs what is delivered below.
  2. Could array_comprehension_exprt please also make use of scopes?

Daniel Kroening added 2 commits June 15, 2021 11:58
@kroening
boolbvt: introduce scopes
4da9fad 
This is the biggest change to the solver interface since it got added to the
codebase.

Currently, bound identifiers (exists, forall, let, lambda,
array_comprehension_exprt) must be unique; the solver loses soundness if
that assumption is violated.

This change introduces scopes for let, i.e., the uniqueness requirement is
dropped.  Nested scoping works as expected.  This matches what SMT-LIB does,
i.e., the renaming done in the SMT-LIB front-end can be dropped.
@kroening
smt2_solver: add another test for bit-vector let
de99e34
@kroening
Copy link
Member Author

  1. Could array_comprehension_exprt please also make use of scopes?

There are many more expressions with scope (forall and exists in particular). Will deliver!

@kroening kroening merged commit 22b7a89 into develop Jun 15, 2021
@kroening kroening deleted the solver-scopes branch June 15, 2021 11:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel left review comments

@tautschnig tautschnig tautschnig approved these changes

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@allredj allredj Awaiting requested review from allredj

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@tautschnig tautschnig

Labels
RFC Request for comment Solvers
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kroening @peterschrammel @tautschnig