projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2fda1f5) | patch
Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain instant...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 3 Feb 2014 16:23:28 +0000 (10:23 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 3 Feb 2014 16:23:39 +0000 (10:23 -0600)
commit7b50c3f698cd2abdc4f3c2d57e63996419423938
treeafc11a370f9386c70550b20aea7d8c64cf6c4d4ctree
parent2fda1f59b3f5c5d0d6d9b36ae206b8984fb6064ccommit | diff
Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instantiation breadth-first.
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history