projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 576d50a) | patch
Refactor trigger selection, revisions to --relational-trigger. Properly process non...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 7 Apr 2016 14:38:41 +0000 (09:38 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 7 Apr 2016 14:38:41 +0000 (09:38 -0500)
commit59b935c1af18ec51efacf87b0e45d9134d3aaa1e
tree57cee5cddf68999e20553ee9746f4a83183e8b99tree
parent576d50ac7c13233a589771401537b587eb36361ecommit | diff
Refactor trigger selection, revisions to --relational-trigger. Properly process non-standard user-provided triggers. Avoid entailed instantiations based on equality earlier. Refactor core addInstantiation method, add notification mechanism. Add optional argument to entailment checks. Fix bug for duplicate triggers.
14 files changed:
src/theory/quantifiers/inst_match_generator.cpp 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/macros.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h 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
src/theory/quantifiers_engine.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/double-pattern.smt2 [new file with mode: 0644] blob