Skip to content

Maintain ID_C_expr_simplified #37

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

Closed
wants to merge 2 commits into from

Conversation

tautschnig
Copy link
Collaborator

The aim is to avoid redundant invocations of the simplifier by storing is_simplified with each expression. This patch is the first part of this, then second half will be added once #25 is merged as there would be conflicting code changes.

#else
if(!local_replace_map.empty() &&
}
#if 0
Copy link
Member

Choose a reason for hiding this comment

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

@tautschnig, can you explain why this code is commented out?
Otherwise, this looks mergeable.

@tautschnig
Copy link
Collaborator Author

I have cleaned up the code that really was for debugging purposes only.

@forejtv forejtv assigned tautschnig and unassigned kroening Feb 21, 2017
@forejtv
Copy link
Contributor

forejtv commented Feb 21, 2017

@tautschnig can you please rebase to fix the conflict and also see if all tests pass?

@tautschnig
Copy link
Collaborator Author

Rebased, all checks passing. As with #35, there is another question about performance, however.

@forejtv forejtv assigned kroening and unassigned tautschnig Feb 22, 2017
@forejtv
Copy link
Contributor

forejtv commented Feb 22, 2017

@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance?

@tautschnig
Copy link
Collaborator Author

It would be nice to have some continuous performance evaluations set up. As a first step, the scripting outlined in https://github.com/diffblue/cprover-sv-comp/blob/master/README.md could be picked up. That is, one would likely want a two-fold evaluation: monitor SV-COMP overall results, but also build and run with profiling data as 1) not every change results in immediate overall verification improvements and 2) overall improvement on any specific set of benchmarks (such as SV-COMP) is not necessarily representative.

danpoe added a commit to danpoe/cbmc that referenced this pull request Feb 24, 2017
…vity-const-domain

Variable Sensitivity Domain
@tautschnig tautschnig force-pushed the store-is_simplified branch from 4a018c6 to 88e52cf Compare June 8, 2017 08:56
@tautschnig tautschnig assigned tautschnig and unassigned kroening Jul 3, 2017
smowton added a commit to smowton/cbmc that referenced this pull request May 9, 2018
…_make

Only build CBMC directories we need
@hannes-steffenhagen-diffblue
Copy link
Contributor

@tautschnig This has been stale for a while. I'm not sure if this still makes sense to do now 5 years later, if you want to revive this feel free to rebase and reopen, but closing for now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants