projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4f3416b) | patch
Support for str.<= and str.< (#1882)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 May 2018 19:50:47 +0000 (14:50 -0500)
committerGitHub <noreply@github.com>
Tue, 8 May 2018 19:50:47 +0000 (14:50 -0500)
commitf5e3739358b98d9a6ebc16fbc5aed9edee1483dc
tree6659d344360af9964266614f33dd16f24ed39923tree
parent4f3416bf998cdf3fc8b6adf6debb7e65d663bd7ccommit | diff
Support for str.<= and str.< (#1882)
17 files changed:
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/strings/kinds diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.h diff | blob | history
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h diff | blob | history
src/theory/strings/theory_strings_type_rules.h diff | blob | history
src/util/regexp.cpp diff | blob | history
src/util/regexp.h diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress0/strings/code-sat-neg-one.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/strings-leq-trans-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/strings-lt-len5.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/strings-lt-simple.smt2 [new file with mode: 0644] blob