Age | Commit message (Expand) | Author |
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 | Adding a clang format file for the project. | Tim King |
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 | Let arith_proof print its own terms | 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 |
2016-09-03 | Option for prenex normal form | ajreynol |
2016-09-01 | Merge pull request #91 from timothy-king/no-throw | Tim King |
2016-09-01 | Fix boolean term issue in invariants from sygus. Minor default options change... | ajreynol |
2016-09-01 | Cleanup quantifier elimination in smt engine. | ajreynol |
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
2016-09-01 | Relaxing the throw specifiers for the destructors for Node, TypeNode, the con... | Tim King |
2016-08-31 | Removing the forward declaration of QuantInfo from rewrite_engine.h. | Tim King |
2016-08-31 | Cleaning up the dead FORIT macros. | Tim King |
2016-08-31 | Removing the usage of typeof from theory_sets_private. | Tim King |
2016-08-31 | Beautifying theory_model.h. | Tim King |
2016-08-31 | Removing BOOST_FOREACH from theory/sets/scrutinize.h. | Tim King |
2016-08-31 | Removing typeof from sets normal form and beautifying the file. | Tim King |
2016-08-31 | Removing typeof from command_executor_portfolio.cpp. | Tim King |
2016-08-31 | Removing typeof from didyoumean.cpp. | Tim King |
2016-08-30 | Computed members for tp and product rels even they are not used in | Paul Meng |
2016-08-30 | also computed members for relations that do not have explicit membership | Paul Meng |
2016-08-30 | more fix for TC inference | Paul Meng |