| Age | Commit message (Expand) | Author |
|---|
| 2016-09-20 | Refactor, separate theory-specific counterexample-guided instantiation. | ajreynol |
| 2016-06-23 | Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures. | Clark Barrett |
| 2016-06-17 | Support for separation logic. Enable cbqi by default for pure BV. | ajreynol |
| 2016-06-01 | Merge from proof branch | Guy |
| 2016-06-01 | Revert "Merging proof branch" | Guy |
| 2016-06-01 | Merging proof branch | Guy |
| 2016-05-24 | Merged cryptominisat from experimental branch. | Liana Hadarean |
| 2016-04-09 | Minor refactoring of entailment tests and quantifiers util. Initial draft of ... | ajreynol |
| 2016-03-28 | Implement equality inference module for arithmetic terms. Optimization for e... | ajreynol |
| 2016-03-24 | Refactored the equality engine in order to remove theory-specific logic from ... | Guy |
| 2016-03-23 | squash-merge from proof branch | Guy |
| 2016-03-01 | Shorter explanations for strings based on tracking which parts of normal form... | ajreynol |
| 2016-02-24 | Unifying the definitions of ClauseId to a single source of truth. | Tim King |
| 2016-02-18 | Implement dynamic splitting for quantified formulas. Minor refactoring of re... | ajreynol |
| 2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
| 2016-02-01 | Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build p... | Tim King |
| 2016-01-28 | Adding listeners to Options. | Tim King |
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
| 2016-01-08 | Removing StatisticsRegistry's static functions current() and registerStat(). | Tim King |
| 2016-01-05 | Removing dead code. StackingMap only appeared in unit tests. | Tim King |
| 2016-01-05 | Add SmtGlobals Class | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-12-01 | More work on --cegqi-si-partial, incomplete. | ajreynol |
| 2015-11-03 | Adding a test to ensure the <build>/src/theory directory is available to the ... | Tim King |
| 2015-10-27 | Adding the new mkdirs script to EXTRA_DIST. This should fix the failing night... | Tim King |
| 2015-10-26 | This commit removes using absolute paths in the generation of the .subdirs fi... | Tim King |
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
| 2015-09-09 | Working towards a fair enumerator for codatatypes. | ajreynol |
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
| 2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
| 2015-02-11 | Move si solution reconstruction to own file, make more robust. Other refactor... | ajreynol |
| 2015-02-02 | Single invocation module for counterexample guided quantifier instantiation -... | ajreynol |
| 2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
| 2015-01-21 | Initial work on sygusNormalForm. | ajreynol |
| 2014-12-03 | Floating point infrastructure. | Martin Brain |
| 2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
| 2014-11-07 | Remove some dead code. | Morgan Deters |
| 2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
| 2014-10-19 | Finish sets type enumerator implementation. | Kshitij Bansal |
| 2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
| 2014-07-31 | New module for generating candidate equality conjectures used in inductive pr... | ajreynol |
| 2014-06-21 | fixed build failure | lianah |
| 2014-06-19 | get-glpk-cut-log script, and configure code. | Morgan Deters |
| 2014-06-14 | Evil bitvector preprocessing pass for simplifying powers of two. | lianah |
| 2014-06-11 | Fix an omission in bv sources. | Morgan Deters |
| 2014-06-11 | Some clean-up, post bv-merge. | Morgan Deters |
| 2014-06-10 | Merging Tim's pseudoboolean work from his fmcad14 branch. | Tim King |
| 2014-06-10 | Merging CAV14 paper bit-vector work. | lianah |
| 2014-05-26 | Separating an implicit inclusion of smt_engine.h from theory.h. | Tim King |
