projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a626d85) | patch
Move cardinality inference scheme to base solver in strings (#3792)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 22 Feb 2020 07:05:43 +0000 (01:05 -0600)
committerGitHub <noreply@github.com>
Sat, 22 Feb 2020 07:05:43 +0000 (23:05 -0800)
commit9b20af281db3e77a25540305dfb73cbe56519f75
tree2122c9f51c7d536621a3e3d32da66216d3cde1e8tree
parenta626d85e490256a5d872fec49910cdb43e85c16dcommit | diff
Move cardinality inference scheme to base solver in strings (#3792)

Moves handling of cardinality to the base solver, refactors how cardinality is accessed.

No intended behavior change in this commit.
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/base_solver.h diff | blob | history
src/theory/strings/regexp_operation.cpp diff | blob | history
src/theory/strings/regexp_operation.h 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_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h 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/strings/type_enumerator.h diff | blob | history