projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8b57c18) | patch
Improvements to theory combination + strings: do not return trivial care graph, split...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 20 May 2016 18:59:13 +0000 (13:59 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 20 May 2016 18:59:20 +0000 (13:59 -0500)
commitd5d05e4723581c86808a866af1a9f20343ed36dc
treeb8b6985db8c361f4ad8a0a004ebb4596fca32824tree
parent8b57c18d24caced0744d8624b3e0208aeba923efcommit | diff
Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history