projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f6a2704) | patch
Strings: More aggressive skolem normalization (#2761)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 18 Jun 2019 17:04:08 +0000 (10:04 -0700)
committerGitHub <noreply@github.com>
Tue, 18 Jun 2019 17:04:08 +0000 (10:04 -0700)
commit073335156ff7644364d12a91d4d41af776cfb91b
tree3c541683c11b132f168198b0f5c95ccd52df74datree
parentf6a2704f9e35f72c7e682fa71a3f64e79dd4e9e3commit | diff
 Strings: More aggressive skolem normalization (#2761)

This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.
src/theory/strings/skolem_cache.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history