Age | Commit message (Expand) | Author |
2015-09-16 | Add option --fmf-fun-rlv, remove deprecated option --axiom-inst. | ajreynol |
2015-09-10 | Fix bug 670. Minor. | ajreynol |
2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Clea... | ajreynol |
2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/... | ajreynol |
2015-07-01 | Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-qu... | ajreynol |
2015-06-22 | Add --user-pat=interleave. Remove unused lte inst strategy. | ajreynol |
2015-02-22 | New trigger options. --inst-no-entail on by default. Misc cleanup. | ajreynol |
2015-01-23 | CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly a... | ajreynol |
2014-11-21 | Change default option to --inst-when=full-last-call (interleave instantiation... | ajreynol |
2014-11-16 | Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e... | ajreynol |
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol |
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | 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-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | 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-01 | Update copyrights. | Morgan Deters |
2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-02-27 | Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the defa... | Andrew Reynolds |
2014-02-25 | Add options --full-saturate-quant and --mbqi=trust. Other minor changes. | Andrew Reynolds |
2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q... | Andrew Reynolds |
2014-02-14 | Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp... | Andrew Reynolds |
2014-02-04 | Add variable ordering for QCF to accelerate matching procedure. Preparing fo... | Andrew Reynolds |
2014-01-24 | Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ... | Andrew Reynolds |
2014-01-17 | More optimizations for quantifiers conflict find. Add trust user patterns mode. | Andrew Reynolds |
2014-01-10 | Add stats to quantifiers conflict find. Added option for qcf. Working on ha... | Andrew Reynolds |
2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-03-15 | changed default option for quantifier instantiation | Andrew Reynolds |
2012-10-17 | first working version of new inst-gen-style quantifier instantiation techniqu... | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-07-31 | Options merge. This commit: | Morgan Deters |