| Age | Commit message (Expand) | Author |
|---|
| 2017-11-21 | Cegqi bv remove extract terms preprocess pass (#1376) | Andrew Reynolds |
| 2017-11-15 | Reenable some regressions, minor. (#1369) | Andrew Reynolds |
| 2017-11-14 | Clean Ceg Instantiators (#1365) | Andrew Reynolds |
| 2017-11-01 | CBQI BV choice expressions (#1296) | Andrew Reynolds |
| 2017-10-25 | CBQI BV: Add handling for missing operators. (#1274) | Aina Niemetz |
| 2017-10-23 | CBQI BV: Add ULT/SLT inverse handling. (#1268) | Aina Niemetz |
| 2017-10-13 | CBQI BV: Added EXTRACT handling. (#1240) | Aina Niemetz |
| 2017-10-12 | CBQI BV quick heuristics (#1239) | Andrew Reynolds |
| 2017-10-12 | Initial support for solving bit-vector inequalities (#1229) | Andrew Reynolds |
| 2017-10-11 | Enable regressions for CBQI BV and fix inverse for LSHR. (#1234) | Aina Niemetz |
| 2017-10-11 | Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224) | Mathias Preiner |
| 2017-10-11 | Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ... | Andrew Reynolds |
| 2017-10-09 | CBQI BV: Add inverse for more operators. (#1213) | Aina Niemetz |
| 2017-09-29 | Simplify representation of inversion Skolems for bv cegqi (#1164) | Andrew Reynolds |
| 2017-09-29 | Initial working version of BV word-level instantiation (#1158) | Andrew Reynolds |
| 2017-09-14 | Remove unhandled subtypes (#1098) | Andrew Reynolds |
| 2017-08-04 | Set default language to smt lib 2.6 (including as a base language for sygus),... | ajreynol |
| 2017-06-30 | Minor change to trigger selection, fixes related to subtypes (in macros, cbqi... | ajreynol |
| 2017-06-15 | Add regression. | ajreynol |
| 2017-05-31 | Fix model construction for BV with cbqi. Minor change to defaults. | ajreynol |
| 2017-05-31 | Minor change to defaults, update smt comp script, minor changes to options in... | ajreynol |
| 2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol |
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
| 2017-01-04 | Marking regression test files as non-executable. | Tim King |
| 2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix linebre... | Tim King |
| 2016-11-17 | Fix Makefiles in test | Andres Notzli |
| 2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol |
| 2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
| 2016-07-28 | Fix bug 749. | ajreynol |
| 2016-07-19 | Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz... | ajreynol |
| 2016-07-05 | Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ... | ajreynol |
| 2016-06-01 | Fix to ignore a case of triggers with no free variables. | ajreynol |
| 2016-05-26 | Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in... | ajreynol |
| 2016-05-10 | Fix for --inst-max-level | ajreynol |
| 2016-05-02 | Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ... | ajreynol |
| 2016-04-12 | Bug fixes related to parametric datatypes + theory combination + quantifiers.... | ajreynol |
| 2016-04-12 | Optimizations for QCF to check relevant domain of variable argument positions... | ajreynol |
| 2016-04-07 | Refactor trigger selection, revisions to --relational-trigger. Properly proce... | ajreynol |
| 2016-03-18 | Limit duplicate propagating instances to avoid exponential behavior in QuantC... | ajreynol |
| 2016-03-12 | Add options related to interleaving quantifiers and theory combination, chang... | ajreynol |
| 2016-03-02 | Work towards complete instantiation for datatypes. | ajreynol |
| 2016-03-01 | Shorter explanations for strings based on tracking which parts of normal form... | ajreynol |
| 2016-02-18 | Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug ... | ajreynol |
| 2016-02-11 | More aggressive conditional rewriting for quantified formulas. Bug fix set in... | ajreynol |
| 2016-02-08 | Updates related to finite model finding and (co)datatypes. Bug fix enumerator... | ajreynol |
| 2015-11-11 | Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation. | ajreynol |
| 2015-11-10 | Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq... | ajreynol |
| 2015-11-06 | Changing file permissions to add or remove executable tag as appropriate. | Tim King |
| 2015-11-05 | Merging the google branch back into master. | Tim King |
| 2015-11-05 | Fixes some initialization and desctruction problems in quantifiers. Also rest... | Tim King |
