projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fc573f3) | patch
Accept user-provided triggers with variable terms. Flush lemmas before quantifiers...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 8 Sep 2014 22:51:34 +0000 (00:51 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 8 Sep 2014 22:51:34 +0000 (00:51 +0200)
commit433401b05664d9c8827b19455ef7b93fd27efd9d
tree9be15c6804521434d4116b05eb571ecd78ac2767tree
parentfc573f3512b5345763755c9d7a061d430c46ae5fcommit | diff
Accept user-provided triggers with variable terms.  Flush lemmas before quantifiers check.  Minor fix for conjecture generation.
src/theory/quantifiers/conjecture_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history