projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a026f19) | patch
Adding str.len to triggers (#5746)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 5 Jan 2021 19:19:34 +0000 (11:19 -0800)
committerGitHub <noreply@github.com>
Tue, 5 Jan 2021 19:19:34 +0000 (11:19 -0800)
commit2d2ee68b75d1fd3ea0d523b44815d2dc63529e54
tree4bf0a6aee2eb88d1358b77c3454ebce92c0d8595tree
parenta026f19e6472a252286f2c5cde9e9d71b835fc95commit | diff
Adding str.len to triggers (#5746)

This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/quant_len_trigger.smt2 [new file with mode: 0644] blob