projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6ae3e71) | patch
Add proof skolem cache (#4485)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 May 2020 14:14:54 +0000 (09:14 -0500)
committerGitHub <noreply@github.com>
Wed, 20 May 2020 14:14:54 +0000 (09:14 -0500)
commitc010efcdea8e96f3d423d8cebdfd0f3c19a379c7
treed67331c190a3c304a9c3f4a390dc82278817454btree
parent6ae3e7167132e9060257d4f3d876f4e49e67b2a8commit | diff
Add proof skolem cache (#4485)

This adds the general utility for maintaining mappings from Skolems to their witness form via attributes.

I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs.
src/expr/CMakeLists.txt diff | blob | history
src/expr/proof_skolem_cache.cpp [new file with mode: 0644] blob
src/expr/proof_skolem_cache.h [new file with mode: 0644] blob