projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec865a8) | patch
Add lemma for str.to.int/int.to.str (#3541)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 6 Dec 2019 19:33:51 +0000 (11:33 -0800)
committerGitHub <noreply@github.com>
Fri, 6 Dec 2019 19:33:51 +0000 (11:33 -0800)
commit61c78314a1519b5e7be1c45ef9f6cee25b3a10b4
tree94e1dc58f365d672ca0568082b2618ddc1964b65tree
parentec865a83596fd1285e033426b80ddfc1c35085cdcommit | diff
Add lemma for str.to.int/int.to.str (#3541)

This commit adds a lemma to our encoding of `str.to.int` and
`int.to.str` that relates the integer value in the encodings to the
value of partial results.
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history