summaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2020-01-25Axioms for affine function bounds. Tests. (#3632)Alex Ozdemir
2020-01-21Types and side conditions for affine bounds (#3631)Alex Ozdemir
2020-01-21Affine Axioms (#3630)Alex Ozdemir
2020-01-21Types & side-conditions for linear and affine fns (#3627)Alex Ozdemir
2020-01-21Axioms (and side conditions) for tightening bounds (#3613)Alex Ozdemir
2020-01-17LIRA proof: Arithmetic predicates & reification thereof (#3612)Alex Ozdemir
2020-01-17LIRA sig: int, real terms, and conversions (#3610)Alex Ozdemir
2019-12-06[proof] Eliminate side-condition from ER signature (#3230)Alex Ozdemir
2019-11-18Signature documentation update (#3476)Alex Ozdemir
2019-08-05Fix drat signature wrt side condition return types. (#3160)Andrew Reynolds
2019-06-05DRAT-Optimization (#2971)Alex Ozdemir
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-03-29removing deprecated rewriting signature / example (#2906)Haniel Barbosa
2019-03-28fix ex_bv.plf (#2905)Haniel Barbosa
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
2019-01-24Extended DRAT signature to operational DRAT (#2815)Alex Ozdemir
2019-01-16Bugfix: LFSC clause equality (#2801)Alex Ozdemir
2019-01-15Extended Resolution Signature (#2788)Alex Ozdemir
2018-12-16DRAT Signature (#2757)Alex Ozdemir
2018-12-11[LRA proof] More complete LRA example proofs. (#2722)Alex Ozdemir
2018-12-11[LRAT] signature robust against duplicate literals (#2743)Alex Ozdemir
2018-12-11LRAT signature (#2731)Alex Ozdemir
2018-11-27LRA proof signature fixes and a first proof for linear polynomials (#2713)Alex Ozdemir
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-09-22cmake: Add make install rule.Mathias Preiner
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
2018-09-22cmake: Add libsignatures for proofs.Mathias Preiner
2018-09-22cmake: .cpp generation done, .h generation not yet completeAina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-04-02a formula should be an instance of itself (#1668)yoni206
2018-03-20correct instruction for running example (#1669)yoni206
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
2017-07-29Change remaining hash_set -> unordered_set (#208)Andres Noetzli
2017-04-05Merge pull request #143 from FabianWolff/masterClark Barrett
2017-04-05[LFSC] Fix segfaultAndres Notzli
2017-04-05Fix several spelling errorsFabian Wolff
2017-03-17better support for proof production when encountering bool terms: handle the ...guykatzz
2017-03-09bug fixguykatzz
2017-03-09better proof support for bools and formulasguykatzz
2017-03-06Adding support for bool-to-bvClark Barrett
2017-01-16[LFSC] Fix performance issues, more determinismAndres Notzli
2017-01-04Marking the proof signature files as non-executable.Tim King
2017-01-04Reverting two files encoding with DOS linebreaks back into using unix linebre...Tim King
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback