projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9784b39) | patch
Use witness terms to represent values for large strings in models (#8089)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 10 Feb 2022 19:43:09 +0000 (13:43 -0600)
committerGitHub <noreply@github.com>
Thu, 10 Feb 2022 19:43:09 +0000 (19:43 +0000)
commit21419712aaa764031ad8731e777117c258e49ce6
tree8aab0a062cbcff99223430f283eabdff19635fe9tree
parent9784b39d8815cdc1c884d6b365cd16d70f2657bfcommit | diff
Use witness terms to represent values for large strings in models (#8089)

This makes it so that we don't prematurely fail on some Facebook benchmarks.
src/options/strings_options.toml diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
src/theory/strings/theory_strings_utils.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/strings/large-model.smt2 diff | blob | history