projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 363b838) | patch
Improve quantifier instantiation: always use original terms when matching (was missin...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 25 May 2014 14:18:42 +0000 (09:18 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 25 May 2014 14:18:55 +0000 (09:18 -0500)
commit9d3f97ea91ffbf9ceea5814281a4d434d8e09a53
treef1f9fccd3eb09b3d9333506b85ab09587e985b05tree
parent363b838e4a0b799da537d60632fe844c5c5e4686commit | diff
Improve quantifier instantiation: always use original terms when matching (was missing for simple triggers).   Minor updates to scripts.
contrib/run-script-cascj7-fnt diff | blob | history
contrib/run-script-cascj7-fof diff | blob | history
contrib/run-script-cascj7-tff diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/rewrite_engine.cpp diff | blob | history
test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 diff | blob | history