Age | Commit message (Expand) | Author |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
2016-09-29 | Address some coverity warnings, add another stat. | ajreynol |
2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
2016-05-05 | Compute term indices lazily in TermDb. Optimization for qcf to recognize irre... | ajreynol |
2016-05-02 | Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ... | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-13 | Handle parametric datatypes with --quant-ind. Minor updates. | ajreynol |
2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ... | ajreynol |
2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ... | ajreynol |
2015-09-11 | Minor cleanup related to codatatypes. | ajreynol |
2015-07-02 | On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force n... | ajreynol |
2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett |
2015-04-21 | Fix file permissions | Clark Barrett |
2015-04-09 | Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, an... | ajreynol |
2015-04-08 | Make fun-def quantifiers carry the function app they define, make fun-def uti... | ajreynol |
2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
2014-11-28 | Synchronize conjecture generation with E-matching. Minor fix to --full-satur... | ajreynol |
2014-11-13 | More preparation for filtering relevant terms in TermDb. | ajreynol |
2014-10-28 | Improve stats in conjecture generator, minor cleanup. | ajreynol |
2014-10-10 | Initial draft of CEGQI. | ajreynol |
2014-10-01 | Option for more aggressive merging in UEE. | ajreynol |
2014-09-29 | Add option for aggressive model filtering in conjecture generator (enumerate ... | ajreynol |
2014-09-24 | Fix infinite loop in datatypes enumerator. Minor work on conjecture generator. | ajreynol |
2014-09-17 | Refactor entailment filtering for conjecture generator. Other minor cleanup. | ajreynol |
2014-09-17 | More refactoring of conjecture generation. Term generation into own class. | ajreynol |
2014-09-16 | Bug fix variable triggers with --inst-max-level : use term in EQC with minima... | ajreynol |
2014-09-16 | Refactoring of conjecture generator. Determine subgoals are non-canonical ba... | ajreynol |
2014-09-09 | Accept user-provided triggers with variable terms. Flush lemmas before quant... | ajreynol |
2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change... | ajreynol |
2014-09-03 | Work on conjecture generator : do not generalize subterms with concrete value... | ajreynol |
2014-08-01 | Minor cleanup from previous commit. Better organization for how quantifiers ... | ajreynol |
2014-07-31 | New module for generating candidate equality conjectures used in inductive pr... | ajreynol |