projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5938faa) | patch
Theory strings preprocess (#4534)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 4 Jun 2020 14:52:55 +0000 (09:52 -0500)
committerGitHub <noreply@github.com>
Thu, 4 Jun 2020 14:52:55 +0000 (09:52 -0500)
commita3670b55e0ef3d4c8e31800aa943688065ca029c
tree8142dc5cff62cad0ab61cc730c777204298b39eetree
parent5938faaf034a761f3462d8e03b86b1726a332f68commit | diff
Theory strings preprocess (#4534)

This makes it so that the main reduce function in TheoryStringsPreprocess is static, so that it can be used both by the solver and the proof checker.

It also updates the functions to make use of IndexVar for constructing canonical universal variables.
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.h diff | blob | history