summaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2021-05-24Fix LFSC for nested skolems in purificationajreynol
2021-05-21Refactor regular expression unfolding, formalize skolems, working LFSC transl...ajreynol
2021-05-21Support shared selectors in LFSC proof outputajreynol
2021-05-19Use skolem function for shared selectorsajreynol
2021-05-19Update LFSC commitajreynol
2021-05-19Minor, update LFSC signatureajreynol
2021-05-17Update LFSC signatureajreynol
2021-05-17Minor fixes for LFSC conversionajreynol
2021-05-17Constant sequences, more fixes, exclude bad regressionsajreynol
2021-05-17LFSC commitajreynol
2021-05-17Simplify indexof reduction, update LFSC sig commitajreynol
2021-05-14More additions for LFSC, ho congruence, missing operatorsajreynol
2021-05-14Increment lfsc commitajreynol
2021-05-13Increment LFSC commitajreynol
2021-05-13Fixes to LFSC printerajreynol
2021-05-13Fix congruence over quantifiers in LFSCajreynol
2021-05-13Properly print sorts using user names in LFSC, fix pow.ajreynol
2021-05-12Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-05-12Preliminary draft of changes for SMT comp 2021 (#6522)Andrew Reynolds
2021-05-05Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-04-28Allow Int/Real subtyping in LFSC proofsajreynol
2021-04-27LFSC commitajreynol
2021-04-27Minor fixes, additions to LFSCajreynol
2021-04-27Work on indexed operators in LFSCajreynol
2021-04-21Update scriptsajreynol
2021-04-21Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-20More LFSC signatureajreynol
2021-04-20Add proofs for sets purificationajreynol
2021-04-20Minor to LFSCajreynol
2021-04-20Minor for LFSC term conversion, increase commitajreynol
2021-04-19Fixes for printing typesajreynol
2021-04-19Work on real and bv constants in LFSC term processajreynol
2021-04-15Increase LFSC signature commitajreynol
2021-04-13Update commitajreynol
2021-04-13Fixes for term processor for LFSC, update commitajreynol
2021-04-13Updates to scriptsajreynol
2021-04-12Merge branch 'master' into proof-newHaniel Barbosa
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Basic work on printing other LFSC term typesajreynol
2021-04-09Revertajreynol
2021-04-09Automating set up of latest LFSCajreynol
2021-04-09Fixajreynol
2021-04-09Hack to extract regression callsajreynol
2021-04-09Basic scripts for summarizing status of regressions for LFSCajreynol
2021-03-31Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-03-31Refactor GMP and Poly dependencies (#6245)Gereon Kremer
2021-03-31Refactor dependencies for external SAT solvers (#6215)Gereon Kremer
2021-03-31Refactor SymFPU dependency (#6218)Gereon Kremer
2021-03-29Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback