Skip to content

Make IPASIR configuration build after solver hardness changes #5710

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
Jan 21, 2021
Merged

Make IPASIR configuration build after solver hardness changes #5710

merged 1 commit into from
Jan 21, 2021
+57 −47

Conversation

tautschnig
Copy link
Collaborator

In #5480 the solver hardness interface was updated, but changes were
only implemented in the Minisat2 interface. Update the IPASIR interface
to match these changes.

To avoid future regressions, make the check-macos-10_15-make-clang
GitHub action use IPASIR with Riss as the back-end solver.

  • 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.
  • n/a 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).
  • n/a 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.

@codecov
Copy link

codecov bot commented Jan 1, 2021 •
edited
Loading

Codecov Report

Merging #5710 (2a544f7) into develop (ec21533) will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5710   +/-   ##
========================================
  Coverage    69.68%   69.68%           
========================================
  Files         1248     1248           
  Lines       100855   100855           
========================================
  Hits         70278    70278           
  Misses       30577    30577
Flag Coverage Δ
cproversmt2 43.43% <ø> (ø)
regression 66.66% <ø> (ø)
unit 32.20% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out 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 ec21533...2a544f7. Read the comment docs.

@tautschnig tautschnig force-pushed the fix-ipasir branch 5 times, most recently from b38ed96 to db97449 Compare January 2, 2021 22:35
@tautschnig tautschnig self-assigned this Jan 3, 2021
martin-cs
martin-cs approved these changes Jan 12, 2021
View reviewed changes
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Again, good to have this in CI.

peterschrammel
peterschrammel approved these changes Jan 14, 2021
View reviewed changes
src/solvers/refinement/bv_refinement_loop.cpp Outdated
@@ -123,6 +123,10 @@ void bv_refinementt::check_SAT()

arrays_overapproximated();

// get values before modifying the formula
Copy link
Member

Choose a reason for hiding this comment

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

How did you notice this? Is there a test for that or does it fail quite broadly?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I actually noticed this while working on #4758, because Cadical complained. For the IPASIR interface this commit was just an attempt to make things work, but we still have failing regression tests, so I need to dig deeper.

@tautschnig
Make IPASIR configuration build after solver hardness changes
2a544f7 
In diffblue#5480 the solver hardness interface was updated, but changes were
only implemented in the Minisat2 interface. Update the IPASIR interface
to match these changes.

Also fix the status tracking in do_prop_solve as the previous
implementation would keep the solver in an UNSAT state, even when
assumptions had been modified. This issue was surfaced by the
cbmc-incr-oneloop suite of regression tests.

To avoid future regressions, make the check-ubuntu-20_04-make-gcc GitHub
action use IPASIR with Riss as the back-end solver.
@tautschnig tautschnig merged commit 37d6328 into diffblue:develop Jan 21, 2021
@tautschnig tautschnig deleted the fix-ipasir branch January 21, 2021 22:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

@martin-cs martin-cs martin-cs approved these changes

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

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

Assignees

@tautschnig tautschnig

Labels
bugfix
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tautschnig @peterschrammel @martin-cs