summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2016-09-13refactored the code, added more benchmarks and minor fixesPaul Meng
2016-09-12fixed capitalized "kind"Paul Meng
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
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-13Update native language support for strings.ajreynol
2016-04-12Bug fixes related to parametric datatypes + theory combination + quantifiers....ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-12added more benchmarksPaulMeng
2016-04-11Minor fixes for inst match generators. Updates to qip.googleajreynol
2016-04-10More work on instantiation propagation. Enable external filtering of instanti...ajreynol
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-07Refactor trigger selection, revisions to --relational-trigger. Properly proce...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback