Age | Commit message (Expand) | Author |
2016-10-11 | - fixed a memory leak issue with context dependent data structure | Paul Meng |
2016-09-23 | fixed a few bugs | Paul Meng |
2016-09-13 | fixed type checking and computing for PRODUCT and JOIN | Paul Meng |
2016-09-13 | refactored the code, added more benchmarks and minor fixes | Paul Meng |
2016-09-12 | fixed capitalized "kind" | Paul Meng |
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 |
2016-08-30 | fixed TC inference from graph constructed from a relation and the null | Paul Meng |
2016-08-26 | minor fix | PaulMeng |
2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng |
2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in Th... | ajreynol |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ... | ajreynol |
2016-08-11 | Minor change to strings, introduce proxy vars only when necessary. | ajreynol |
2016-08-10 | Improvements to strings: work on propagations for reverse normal form process... | ajreynol |
2016-08-09 | Fixes for sep star rewrite. | ajreynol |
2016-07-30 | Prioritize inferences when processing normal forms in strings. | ajreynol |
2016-07-28 | fixed construction of TC graph | Paul Meng |
2016-07-28 | fixed construction of TC graph | PaulMeng |
2016-07-28 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-28 | Bug fix involving negated lemmas | Guy |
2016-07-28 | Fix bug 749. | ajreynol |
2016-07-28 | Add the negative conjunction case | Guy |
2016-07-27 | Proper instrumentation of the preprocessing phase | Guy |
2016-07-27 | proper handling of ITEs | Guy |
2016-07-27 | Proper handling of IFF lemmas in the unsat core. | Guy |
2016-07-26 | Add option to minimize sygus solutions based on using weakest implicants of i... | ajreynol |
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ... | ajreynol |
2016-07-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-24 | cleanup | Guy |
2016-07-24 | Proper handling for lemmas that are conjuncts: | Guy |
2016-07-24 | more code refactor | PaulMeng |
2016-07-24 | more code refactor | Paul Meng |
2016-07-23 | refactored code | Paul Meng |
2016-07-22 | Minor, error handling for polymorphism + sep logic. | ajreynol |
2016-07-21 | Fixes for strings, explanations for constant split propagations, substr under... | ajreynol |
2016-07-20 | bug fixes for reachablity check | PaulMeng |
2016-07-20 | Infrastructure for storing and printing heap models for separation logic. Ens... | ajreynol |
2016-07-20 | Print only instantiations that are in the unsat core when --proof is enabled.... | ajreynol |
2016-07-20 | Infer conflicts in strings based on abstracting equality as contains. Minor c... | ajreynol |
2016-07-19 | Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz... | ajreynol |
2016-07-16 | Refactor strings extf evaluation info. Ensure strings eager preprocess elimin... | ajreynol |
2016-07-15 | The ProofManager now allows theory solvers to get their lemmas that participa... | Guy |
2016-07-15 | Minor simplification to normal form explanations. | ajreynol |
2016-07-11 | added support for expansion of transitive closure | Paul Meng |
2016-07-08 | Minor fix to last commit. | ajreynol |
2016-07-07 | Simplifications for strings normal forms, fix case for concat reps in normal ... | ajreynol |
2016-07-07 | Ensure heap disjointness in sep refinements. | ajreynol |
2016-07-07 | Refactoring of strings preprocess module. When enabled, apply eager preproces... | ajreynol |