Skip to content

Add implementation of smt2_incremental_decision_proceduret::get #6573

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

Merged

Conversation

thomasspriggs
Copy link
Contributor

@thomasspriggs thomasspriggs commented Jan 12, 2022

This PR adds the implementation of smt2_incremental_decision_proceduret::get. This adds enough functionality to allow printing of traces and performing incremental solving.

  • 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 Jan 12, 2022

Codecov Report

Merging #6573 (8348994) into develop (bd1401f) will increase coverage by 0.02%.
The diff coverage is 91.35%.

❗ Current head 8348994 differs from pull request most recent head a3f6bd4. Consider uploading reports for the commit a3f6bd4 to get more accurate results
Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6573      +/-   ##
===========================================
+ Coverage    75.99%   76.01%   +0.02%     
===========================================
  Files         1579     1579              
  Lines       181124   181368     +244     
===========================================
+ Hits        137643   137875     +232     
- Misses       43481    43493      +12     
Impacted Files Coverage Δ
...ncremental/smt2_incremental_decision_procedure.cpp 88.88% <79.41%> (-1.04%) ⬇️
...ncremental/smt2_incremental_decision_procedure.cpp 96.47% <100.00%> (+0.92%) ⬆️
src/solvers/sat/satcheck_minisat2.h 75.00% <0.00%> (-9.22%) ⬇️
src/util/symbol_table_builder.h 56.66% <0.00%> (-6.67%) ⬇️
src/util/std_types.cpp 85.71% <0.00%> (-1.65%) ⬇️
jbmc/src/java_bytecode/java_pointer_casts.cpp 92.50% <0.00%> (-0.84%) ⬇️
src/solvers/flattening/boolbv_get.cpp 82.03% <0.00%> (-0.72%) ⬇️
src/util/std_types.h 95.01% <0.00%> (-0.57%) ⬇️
src/ansi-c/expr2c.cpp 65.94% <0.00%> (-0.46%) ⬇️
...trument/contracts/havoc_assigns_clause_targets.cpp 97.72% <0.00%> (-0.35%) ⬇️
... and 44 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b79bd51...a3f6bd4. Read the comment docs.

@thomasspriggs thomasspriggs force-pushed the tas/smt2_incremental_solving branch from 8348994 to ac7667b Compare January 13, 2022 19:43
This commit includes updates existing tests for added solving support
these tests need to be updates, because they no longer cause cbmc to
reach an invariant violation. This means that their exit codes need to
be updated accordingly.
In order to make it easier to reuse when writing new tests.
@thomasspriggs thomasspriggs force-pushed the tas/smt2_incremental_solving branch from ac7667b to a3f6bd4 Compare January 14, 2022 15:31
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.

LGTM

Copy link
Contributor

@NlightNFotis NlightNFotis left a comment

Choose a reason for hiding this comment

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

LGTM.

@thomasspriggs thomasspriggs merged commit 208ca7a into diffblue:develop Jan 17, 2022
@thomasspriggs thomasspriggs deleted the tas/smt2_incremental_solving branch January 17, 2022 10:48
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

Successfully merging this pull request may close these issues.

3 participants