projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 346c85d) | patch
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 10 Mar 2016 23:49:13 +0000 (17:49 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 10 Mar 2016 23:49:13 +0000 (17:49 -0600)
commitd0df704a60696d7f824eb01781b413d91a0e4202
tree501058c359ff029cad024a3a715efdf33968c426tree
parent346c85d145f6938ce7dce74e7e7cb855d5a6025acommit | diff
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.
17 files changed:
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/quant_conflict_find.h diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.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_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/sort_inference.cpp diff | blob | history
src/theory/sort_inference.h diff | blob | history