projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 304f3d6) | patch
Improve relevant domain computation for arithmetic, full saturation strategy. Simply...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 17 Nov 2015 15:41:56 +0000 (16:41 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 17 Nov 2015 15:42:10 +0000 (16:42 +0100)
commit6c49fe8691cf011237be30f4062affc79d8a5314
tree43de311707603716902815226840083ee26e1749tree
parent304f3d632766a445b9e2fb9dd617b2c2cfd50fb2commit | diff
Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/strings/options diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history