Age | Commit message (Expand) | Author |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
2014-10-28 | Improve stats in conjecture generator, minor cleanup. | ajreynol |
2014-10-25 | Minor fix for --user-pat=resort | ajreynol |
2014-10-24 | Fix typo. | Morgan Deters |
2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | ajreynol |
2014-10-18 | Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi... | ajreynol |
2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by CE... | ajreynol |
2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, a... | Morgan Deters |
2014-10-13 | CEGQI uses model. Enforce fairness in CEGQI natively. | ajreynol |
2014-10-13 | Model building into quantifiers engine. Simplify axiom-inst mode. | ajreynol |
2014-10-13 | Refactor model builder from model engine to quant engine. Work on fairness s... | ajreynol |
2014-10-10 | Initial draft of CEGQI. | ajreynol |
2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
2014-10-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | ajreynol |
2014-10-08 | Cache for getInstance, thanks to Johannes Kanig for the report. Do not mkRep... | ajreynol |
2014-10-07 | Refactor quantifiers attributes. | 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-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
2014-09-23 | Support :no-pattern. | ajreynol |
2014-09-23 | Do not throw error when codatatype is not well-founded. Add option for disab... | ajreynol |
2014-09-17 | Fix soundness bug for quantifier macros involving Int/Real. | 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 | Fix bug for variable term triggers within multi-triggers. | ajreynol |
2014-09-09 | Accept user-provided triggers with variable terms. Flush lemmas before quant... | ajreynol |
2014-09-03 | Merge remote-tracking branch 'origin/master' | Kshitij Bansal |
2014-09-03 | check() optimization | Kshitij Bansal |
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-29 | Set instantiation level on skolemized bodies of quantifiers. Rename inst-lev... | ajreynol |
2014-08-29 | Do not use pure theory terms as single triggers. Minor cleanup. | ajreynol |
2014-08-27 | Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict. | ajreynol |
2014-08-26 | Bug fixes for --purify-triggers, --dt-force-assignment. | ajreynol |
2014-08-25 | New option --purify-triggers. Refactoring of InstMatchGenerator. | ajreynol |
2014-08-20 | Add option for inductive strengthening based on well-founded induction for in... | ajreynol |
2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | ajreynol |
2014-08-05 | Minor fix : do not drop instantiation patterns when merging quantifiers. | 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 |
2014-07-26 | Minor bug fix for exhaustive instantiation in model_engine. | ajreynol |
2014-07-21 | initialization in model_engine | Kshitij Bansal |
2014-07-19 | Minor fix for explanations for co-datatypes. Bug fix for explanations in FMF... | ajreynol |
2014-07-01 | Update copyrights. | Morgan Deters |
2014-06-30 | Merge pull request #47 from kbansal/sets | Kshitij Bansal |