Skip to content
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

SAWScript.Prover.Rewrite.rewriteEqs is very slow #590

Closed
brianhuffman opened this issue Nov 16, 2019 · 1 comment
Closed

SAWScript.Prover.Rewrite.rewriteEqs is very slow #590

brianhuffman opened this issue Nov 16, 2019 · 1 comment
Labels
performance Issues that involve or include performance problems

Comments

@brianhuffman
Copy link
Contributor

The problem is that it rebuilds the simpset from scratch (using function basic_ss) every time it is called, which is quite expensive.

rewriteEqs :: SharedContext -> Term -> IO Term
rewriteEqs sc t =
do let eqs = map (mkIdent preludeName)
[ "eq_Bool", "eq_Nat", "eq_bitvector", "eq_VecBool"
, "eq_VecVec" ]
rs <- scEqsRewriteRules sc eqs
ss <- addRules rs <$> basic_ss sc
t' <- rewriteSharedTerm sc ss t
return t'

Profiling on my use-case shows that basic_ss makes up around 30% of both the total runtime and total allocation.
Interestingly, one of the most expensive parts of building the simpset is scTypeOfGlobal, so we should probably optimize that one too.

@brianhuffman brianhuffman added the performance Issues that involve or include performance problems label Nov 16, 2019
@brianhuffman
Copy link
Contributor Author

Function basic_ss is also called from function resolveSAWTerm, which I think is actually the source of the performance issue I'm seeing.

We should cache the simpset somewhere, instead of recomputing it every single time.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
performance Issues that involve or include performance problems
Projects
None yet
Development

No branches or pull requests

1 participant