Age | Commit message (Expand) | Author |
2016-10-08 | Adding initializers for structs internal to ite_utilities. | Tim King |
2016-10-02 | Removing the throw specifiers from theory_uf_type_rules.h. | Tim King |
2016-10-02 | Removing the throw specifiers from theory_fp_type_rules.h. | Tim King |
2016-10-02 | Removing the throw specifiers from theory_datatypes_type_rules.h. | Tim King |
2016-10-02 | Removing an unused member from TreeLog. | Tim King |
2016-10-02 | Removing the throw specifiers from theory_bv_type_rules.h. | Tim King |
2016-10-01 | Incorporate non-bv parts of ajr/bvExt branch | ajreynol |
2016-09-29 | Address some coverity warnings, add another stat. | ajreynol |
2016-09-29 | Minor cleanup and additions to quantifiers statistics. | ajreynol |
2016-09-28 | Fix the merge of kbansal/card branch (2039eab). | Kshitij Bansal |
2016-09-27 | Reverting part of the previous changes to unconstrained simplifier. | Tim King |
2016-09-26 | Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp. | Tim King |
2016-09-25 | Deleting the eager bitblasting solver if present in TheoryBV. | Tim King |
2016-09-25 | Adding a destructor to QuantAntiSkolem. | Tim King |
2016-09-25 | Adding a destructor to TermDb. | Tim King |
2016-09-25 | Adding a destructor to CegqiOutputSingleInv. | Tim King |
2016-09-25 | Deleting optional members of StrongSolverTheoryUF. | Tim King |
2016-09-25 | Disambiguating a vector insert warning coming from coverity scan. | Tim King |
2016-09-25 | Deleting a temporary in theory sets enumerator. | Tim King |
2016-09-25 | Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here. | Tim King |
2016-09-25 | Removing an unused iterator. | Tim King |
2016-09-25 | Fixing a potential use after free coming from a pop_back() call invalidating ... | Tim King |
2016-09-23 | fixed a few bugs | Paul Meng |
2016-09-21 | Remove duplicate code from my last commit | ajreynol |
2016-09-20 | Refactor, separate theory-specific counterexample-guided instantiation. | ajreynol |
2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol |
2016-09-18 | Minor fix for strings | ajreynol |
2016-09-16 | In a ROW guard proof, if the transitivity proof does not have a disequality, ... | guykatzz |
2016-09-16 | Merge branch 'master' of https://github.com/CVC4/CVC4 | guykatzz |
2016-09-16 | Use matching heuristics for EPR instantiation. | ajreynol |
2016-09-16 | Handling a corner case where a ROW's guard is a constant disequality. | Guy |
2016-09-16 | More refactoring of cbqi, start developing new interface. | ajreynol |
2016-09-15 | Further refactor cbqi. | ajreynol |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul... | ajreynol |
2016-09-15 | Make sep pto a trigger kind, track in equality engines and term database. | ajreynol |
2016-09-15 | Refactor setIncomplete in quantifiers. | ajreynol |
2016-09-14 | Support for unique variable generation in node manager. | ajreynol |
2016-09-14 | Lemma cache in theory sep. Minor optimization for sets. Minor improvements to... | ajreynol |
2016-09-13 | fixed type checking and computing for PRODUCT and JOIN | Paul Meng |
2016-09-13 | Minor changes to sep logic, epr, quantifier splitting. | ajreynol |
2016-09-13 | refactored the code, added more benchmarks and minor fixes | Paul Meng |
2016-09-12 | fixed capitalized "kind" | Paul Meng |
2016-09-12 | Refactor prenex modes. | ajreynol |
2016-09-12 | Remove old implementation of cbqi | ajreynol |
2016-09-12 | Prefer non-cardinality constants in term models for sep logic. | ajreynol |
2016-09-12 | Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry b... | ajreynol |
2016-09-09 | Fix bug in unconstrained simplifier related to sep.nil/distinguished variables. | ajreynol |
2016-09-09 | Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a... | ajreynol |
2016-09-08 | Refactor seplog preprocess. Handle case where sep data type cannot be inferred. | ajreynol |
2016-09-03 | Miniscope top level conjunctions for prenex normal form, allow one level mini... | ajreynol |