Age | Commit message (Expand) | Author |
2021-05-24 | Fix LFSC for nested skolems in purification | ajreynol |
2021-05-21 | Refactor regular expression unfolding, formalize skolems, working LFSC transl... | ajreynol |
2021-05-21 | Support shared selectors in LFSC proof output | ajreynol |
2021-05-19 | Use skolem function for shared selectors | ajreynol |
2021-05-19 | Update LFSC commit | ajreynol |
2021-05-19 | Minor, update LFSC signature | ajreynol |
2021-05-17 | Update LFSC signature | ajreynol |
2021-05-17 | Minor fixes for LFSC conversion | ajreynol |
2021-05-17 | Constant sequences, more fixes, exclude bad regressions | ajreynol |
2021-05-17 | LFSC commit | ajreynol |
2021-05-17 | Simplify indexof reduction, update LFSC sig commit | ajreynol |
2021-05-14 | More additions for LFSC, ho congruence, missing operators | ajreynol |
2021-05-14 | Increment lfsc commit | ajreynol |
2021-05-13 | Increment LFSC commit | ajreynol |
2021-05-13 | Fixes to LFSC printer | ajreynol |
2021-05-13 | Fix congruence over quantifiers in LFSC | ajreynol |
2021-05-13 | Properly print sorts using user names in LFSC, fix pow. | ajreynol |
2021-05-12 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol |
2021-05-12 | Preliminary draft of changes for SMT comp 2021 (#6522) | Andrew Reynolds |
2021-05-05 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol |
2021-04-28 | Allow Int/Real subtyping in LFSC proofs | ajreynol |
2021-04-27 | LFSC commit | ajreynol |
2021-04-27 | Minor fixes, additions to LFSC | ajreynol |
2021-04-27 | Work on indexed operators in LFSC | ajreynol |
2021-04-21 | Update scripts | ajreynol |
2021-04-21 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol |
2021-04-21 | Goodbye CVC4, hello cvc5! (#6371) | Mathias Preiner |
2021-04-20 | More LFSC signature | ajreynol |
2021-04-20 | Add proofs for sets purification | ajreynol |
2021-04-20 | Minor to LFSC | ajreynol |
2021-04-20 | Minor for LFSC term conversion, increase commit | ajreynol |
2021-04-19 | Fixes for printing types | ajreynol |
2021-04-19 | Work on real and bv constants in LFSC term process | ajreynol |
2021-04-15 | Increase LFSC signature commit | ajreynol |
2021-04-13 | Update commit | ajreynol |
2021-04-13 | Fixes for term processor for LFSC, update commit | ajreynol |
2021-04-13 | Updates to scripts | ajreynol |
2021-04-12 | Merge branch 'master' into proof-new | Haniel Barbosa |
2021-04-12 | Refactor and update copyright headers. (#6316) | Aina Niemetz |
2021-04-09 | Basic work on printing other LFSC term types | ajreynol |
2021-04-09 | Revert | ajreynol |
2021-04-09 | Automating set up of latest LFSC | ajreynol |
2021-04-09 | Fix | ajreynol |
2021-04-09 | Hack to extract regression calls | ajreynol |
2021-04-09 | Basic scripts for summarizing status of regressions for LFSC | ajreynol |
2021-03-31 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol |
2021-03-31 | Refactor GMP and Poly dependencies (#6245) | Gereon Kremer |
2021-03-31 | Refactor dependencies for external SAT solvers (#6215) | Gereon Kremer |
2021-03-31 | Refactor SymFPU dependency (#6218) | Gereon Kremer |
2021-03-29 | Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new | ajreynol |