projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 29718a8) | patch
Add entailment checks between length terms to reduce splitting in strings solver...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 24 Feb 2016 18:19:09 +0000 (12:19 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 24 Feb 2016 20:52:15 +0000 (14:52 -0600)
commitbab37658aa27ee455e3928c66db49c1bb3224e3b
tree0f472eb5364572a3e505e0ad4d577e7f688205b6tree
parent29718a8926b15287c211a437c3a4947d919f31b1commit | diff
Add entailment checks between length terms to reduce splitting in strings solver.  Minor additions to datatypes and qcf.
src/options/strings_options diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history