Skip to content

Incremental smt2 backend documentation #7363

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 1 commit into from
Nov 30, 2022
Merged

Incremental smt2 backend documentation #7363

merged 1 commit into from
Nov 30, 2022

Conversation

esteffin
Copy link
Contributor

User documentation for the incremental smt2 backend.

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Nov 18, 2022 •
edited
Loading

Codecov Report

Base: 78.35% // Head: 78.35% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (ead3518) compared to base (28b76fa).
Patch coverage: 44.44% of modified lines in pull request are covered.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #7363      +/-   ##
===========================================
- Coverage    78.35%   78.35%   -0.01%     
===========================================
  Files         1645     1645              
  Lines       190190   190208      +18     
===========================================
+ Hits        149031   149040       +9     
- Misses       41159    41168       +9
Impacted Files Coverage Δ
unit/solvers/sat/external_sat.cpp 100.00% <ø> (ø)
src/solvers/sat/external_sat.cpp 81.81% <28.57%> (-6.42%) ⬇️
src/ansi-c/c_typecheck_expr.cpp 75.34% <100.00%> (-0.02%) ⬇️
src/pointer-analysis/value_set.cpp 82.46% <100.00%> (-0.05%) ⬇️
src/nonstd/optional.hpp 96.18% <0.00%> (-1.53%) ⬇️
src/goto-programs/goto_convert_class.h 88.15% <0.00%> (ø)
src/goto-programs/goto_convert_functions.cpp 100.00% <0.00%> (ø)
src/util/simplify_expr.cpp 85.29% <0.00%> (+<0.01%) ⬆️
src/goto-programs/builtin_functions.cpp 60.02% <0.00%> (+1.01%) ⬆️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

@tautschnig
Copy link
Collaborator

How about added the newly proposed contents to src/solvers/README.md instead of creating a new file?

@esteffin
Copy link
Contributor Author

README.md instead of creating a new

It can be done.
Personally I prefer not adding it there as the added documentation is user-facing and not implementation specific as the one in src/solvers/README.md.

@esteffin esteffin force-pushed the esteffin/incr-smt2-backend-documentation branch from d450346 to 4cdb871 Compare November 21, 2022 11:58
@tautschnig
Copy link
Collaborator

README.md instead of creating a new

It can be done. Personally I prefer not adding it there as the added documentation is user-facing and not implementation specific as the one in src/solvers/README.md.

Ok, thank you for the push-back. I don't really mind having it in that separate file, but then please do make sure your newly added documentation ends up being rendered as part of the doxygen-generated documentation. There is no point in having user-facing documentation stowed away in the source tree.

@esteffin esteffin force-pushed the esteffin/incr-smt2-backend-documentation branch from 4cdb871 to 330ea63 Compare November 21, 2022 17:55
@esteffin esteffin marked this pull request as ready for review November 22, 2022 15:55
TGWDB
TGWDB approved these changes Nov 23, 2022
View reviewed changes
Copy link
Contributor

@TGWDB TGWDB left a comment

Choose a reason for hiding this comment

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

Minor text fixes only, otherwise approved.

doc/cprover-manual/smt2-incr.md Outdated
smt2 solver. For other solver usages use `cbmc --help`.

The incremental smt2 solver backend of CBMC is a solver-agnostic smt backend that allows the user to
specify which smtlib 2.6 compliant solver CBMC should use. This choice increase the flexibility of
Copy link
Contributor

Choose a reason for hiding this comment

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

increase -> increases

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Changed

doc/cprover-manual/smt2-incr.md Outdated

The incremental smt2 solver backend of CBMC is a solver-agnostic smt backend that allows the user to
specify which smtlib 2.6 compliant solver CBMC should use. This choice increase the flexibility of
CBMC as the user can easily switch solver at runtime allowing also custom parametrization of the
Copy link
Contributor

Choose a reason for hiding this comment

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

allowing also -> also allowing

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Changed

doc/cprover-manual/smt2-incr.md Outdated
The incremental smt2 solver backend of CBMC is a solver-agnostic smt backend that allows the user to
specify which smtlib 2.6 compliant solver CBMC should use. This choice increase the flexibility of
CBMC as the user can easily switch solver at runtime allowing also custom parametrization of the
solver to be used. Also the backend exploits the incremental mode of the smt solver, so subsequent
Copy link
Contributor

Choose a reason for hiding this comment

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

Also the -> Further, the

Copy link
Contributor Author

Choose a reason for hiding this comment

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

changed

doc/cprover-manual/smt2-incr.md Outdated
* supports incremental mode.

Because of the way supported features are encoded the smt solver should be capable to handle arrays,
bit-vectors and uninterpreted functions and quantifiers. Also, the solver should work with the `ALL`
Copy link
Contributor

Choose a reason for hiding this comment

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

bit-vectors and uninterpreted -> bit-vectors, uninterpreted

Copy link
Contributor Author

Choose a reason for hiding this comment

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

changed

doc/cprover-manual/smt2-incr.md Outdated
cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula program.c
```

We will get the verification results as well as the trace as follows:
Copy link
Contributor

Choose a reason for hiding this comment

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

No trace in the command here, remove "as well as the trace"

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Right, fixed

tautschnig
tautschnig reviewed Nov 23, 2022
View reviewed changes
doc/cprover-manual/index.md
Comment on lines +35 to +37
10. Solvers

* [Incremental SMT solver](smt2-incr/)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Leaving it up to @kroening to make a call here, for he maintains the rendered version of this documentation. My own view is that we should not discuss a particular solver as part of this manual.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I consider the "official" documentation now to be automatically rendered here: https://diffblue.github.io/cbmc/ Is that not the case? Will that not be the case for this file?

Where would you propose we discuss things specific to a particular solver?

Copy link
Collaborator

Choose a reason for hiding this comment

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

I agree that this one (github.io) is the right place; it will also include the CPROVER manual (which is otherwise rendered on cprover.org), but isn't limited to that manual.

Copy link
Contributor

Choose a reason for hiding this comment

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

I consider the "official" documentation now to be automatically rendered here: https://diffblue.github.io/cbmc/ Is that not the case? Will that not be the case for this file?

I can confirm that if I checkout and build the documentation locally as will be done on the documentation publishing job, then this new documentation will be included. Therefore it should be uploaded to the github.io page by github actions after this PR is merged.

The links to follow to find it will be -

  1. User Guide in the side bar.
  2. The link to "A short manual" in that pages's content.
  3. The new page link will be under item 10.

Where would you propose we discuss things specific to a particular solver?

I think this is the right place to add this documentation. Most information about the SAT solvers for instance wouldn't belong here, because they are compile/link time swappable not run-time swappable. However I think this list started by Enrico could be the right place to add documentation of the the dimacs file and external sat solver support, when someone takes the time to write it.

@esteffin esteffin force-pushed the esteffin/incr-smt2-backend-documentation branch from 330ea63 to 5bde5d4 Compare November 23, 2022 11:58
jimgrundy
jimgrundy approved these changes Nov 23, 2022
View reviewed changes
doc/cprover-manual/index.md
Comment on lines +35 to +37
10. Solvers

* [Incremental SMT solver](smt2-incr/)
Copy link
Collaborator

Choose a reason for hiding this comment

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

I consider the "official" documentation now to be automatically rendered here: https://diffblue.github.io/cbmc/ Is that not the case? Will that not be the case for this file?

Where would you propose we discuss things specific to a particular solver?

@esteffin esteffin force-pushed the esteffin/incr-smt2-backend-documentation branch from 5bde5d4 to ead3518 Compare November 24, 2022 14:17
@thomasspriggs thomasspriggs merged commit a487df2 into diffblue:develop Nov 30, 2022
@thomasspriggs thomasspriggs mentioned this pull request Nov 30, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig left review comments

@thomasspriggs thomasspriggs thomasspriggs approved these changes

@TGWDB TGWDB TGWDB approved these changes

@jimgrundy jimgrundy jimgrundy approved these changes

@NlightNFotis NlightNFotis Awaiting requested review from NlightNFotis

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

Assignees

@kroening kroening

@esteffin esteffin

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@esteffin @tautschnig @thomasspriggs @TGWDB @jimgrundy @kroening