summaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2017-01-04Merge pull request #122 from 4tXJ7f/fix_lfsc_strAndrew Reynolds
2016-12-28[LFSC] Minor fixes/improvementsAndres Notzli
2016-12-28[LFSC] Fix memory leaks when creating CExprsfix_lfsc_mem_leaksAndres Notzli
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-25Adding virtual destructors to several classes in expr.h .Tim King
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-15Expression sharing on demand in LFSC (replace definitionally equivalent child...ajreynol
2016-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-06-08Support for printing a global let map in LFSC proofs.Guy
2016-06-03Better infrastructure for proving constant disequality.Guy
2016-06-03A better mechanism for handling BV terms with aliases: inject the alias at th...Guy
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
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-03-23squash-merge from proof branchGuy
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig...ajreynol
2014-08-20Update bv proof signature and example, after discussions with Liana.ajreynol
2014-08-08Add draft of BV proof signature (incomplete) and example proof.ajreynol
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-16lfsc_checker: fix some warnings reported by _both_ gcc and clangKshitij Bansal
2014-03-19Fix proof signatures makefileMorgan Deters
2014-03-19Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (pr...Andrew Reynolds
2014-03-14dos2unix on the proof signatures, and fix the makefile.Morgan Deters
2014-03-13Add working example of LFSC proof with quantifiers. Update quantifiers signa...Andrew Reynolds
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-18Reduce autoconf version for dependence (should fix 32-bit builds).Morgan Deters
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-10-03Adding example proof signatures for LFSC.Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback