| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
| 2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-09 | some debugging changes | Kshitij Bansal |
| 2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
| 2014-03-11 | Fix for rewriterules build breakage. | Morgan Deters |
| 2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
| 2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
| 2014-02-21 | disable test cvc3_main, attempt to fix dist_check | Kshitij Bansal |
| 2014-02-21 | add new theory (sets) | Kshitij Bansal |
