summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_match_generator.h
AgeCommit message (Expand)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2017-12-02Minor improvements to inst match generator (#1415)Andrew Reynolds
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-18Ho instantiation (#1204)Andrew Reynolds
2017-07-07Update copyright headers.Mathias Preiner
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul...ajreynol
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ...ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-03Simple memory fixes, minor cleanup in quantifiers.ajreynol
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-31Improvements to trigger selection, min triggers by default. Optimizations for...ajreynol
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor updates...ajreynol
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-05-15Fixes related to cbqi + E-matching.ajreynol
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ho...ajreynol
2014-11-07Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr...ajreynol
2014-08-25New option --purify-triggers. Refactoring of InstMatchGenerator.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-01-28More optimizations of quantifier instantiation data structures.Andrew Reynolds
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option fo...Andrew Reynolds
2013-06-17Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod...Andrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-02-05More improvements for E-matchingAndrew Reynolds
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback