projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3902038) | patch
support for quantifiers macros, bug fix for bug 454 involving E-matching Array select...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 18 Nov 2012 17:34:00 +0000 (17:34 +0000)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 18 Nov 2012 17:34:00 +0000 (17:34 +0000)
commita441252481616ff4851f208caffce826a026ae30
tree67df7986753dfbea35cd0a5a3264e7be1378a1d2tree
parent39020386be1c6cb304a5bfd1eaca37af46bb0bfccommit | diff
support for quantifiers macros, bug fix for bug 454 involving E-matching Array select terms (thanks for the bug report Francois)
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/macros.h diff | blob | history