summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-21Fix/add missing makefiles.ajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-28Fix the merge of kbansal/card branch (2039eab).Kshitij Bansal
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-13refactored the code, added more benchmarks and minor fixesPaul Meng
2016-09-12fixed capitalized "kind"Paul Meng
2016-09-12Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry b...ajreynol
2016-09-09Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.ajreynol
2016-09-09Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a...ajreynol
2016-08-30added more benchmarksPaul Meng
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for bounde...ajreynol
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor fixes to model construction to take singleton equivalence classes into ...ajreynol
2016-08-10Improvements to strings: work on propagations for reverse normal form process...ajreynol
2016-08-09Fixes for sep star rewrite.ajreynol
2016-07-28Fix bug 749.ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr under...ajreynol
2016-07-20Infer conflicts in strings based on abstracting equality as contains. Minor c...ajreynol
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz...ajreynol
2016-07-08Minor fix to last commit.ajreynol
2016-07-07Simplifications for strings normal forms, fix case for concat reps in normal ...ajreynol
2016-07-07Ensure heap disjointness in sep refinements.ajreynol
2016-07-07Refactoring of strings preprocess module. When enabled, apply eager preproces...ajreynol
2016-07-05Refactor last call for theories, only create one model when quantifiers are e...ajreynol
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ...ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
2016-06-18Fix unit test.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-06-01Fix to ignore a case of triggers with no free variables.ajreynol
2016-06-01Initial infrastructure for bounded set quantification (disabled). Refactoring...ajreynol
2016-05-28Fix buildClark Barrett
2016-05-28Disabling failing unit test for nowClark Barrett
2016-05-26Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in...ajreynol
2016-05-25Fixed unit testLiana Hadarean
2016-05-23Fix related to parametric sorts whose interpretation is finite due to uninter...ajreynol
2016-05-21Minor fix for strings.ajreynol
2016-05-20Minor fix to strings, cleanup in datatypes.ajreynol
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino...ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-10Fix for --inst-max-levelajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback