summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-03-06Use TMPDIR environment variable for temp filesup-fix-fixAndres Noetzli
2019-03-06Update drat2er interfaceAlex Ozdemir
2019-03-03Another DRAT/LRAT compatibility bugAlex Ozdemir
2019-03-03Always assert that drat-trim exits successfully.Alex Ozdemir
2019-03-03Treat tautologies as "sat" during unit propegation.Alex Ozdemir
2019-03-03Bugfix: `clear` does not empty ostream.Alex Ozdemir
2019-03-03Enable DRAT optimization for all pipelines.Alex Ozdemir
2019-03-03Responded to Andres' reviewAlex Ozdemir
2019-03-02Enable CryptoMiniSat-backed BV proofsAlex Ozdemir
2019-02-28ErProof class with LFSC output (#2812)Alex Ozdemir
2019-02-27Use string stream for proofs instead of tmp files (#2841)Andres Noetzli
2019-02-26ClangFormat: Disable DerivePointerAlignment (#2842)Andres Noetzli
2019-02-13New C++ API: Remove redundant declareFun function. (#2837)Aina Niemetz
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-12New C++ API: Remove redundant mkTerm function. (#2836)Aina Niemetz
2019-02-12Delete temporary proof files when aborting CVC4 (#2834)Andres Noetzli
2019-02-11New C++ API: Unit tests for declare* functions. (#2831)Aina Niemetz
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
2019-01-29Fix warning due to catching polymorphic exceptions (#2821)Andres Noetzli
2019-01-29New C++ API: Fix checks for mkTerm. (#2820)Aina Niemetz
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
2019-01-24Extended DRAT signature to operational DRAT (#2815)Alex Ozdemir
2019-01-23Avoid using ProofManager in non-proof CMS build (#2814)Andres Noetzli
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-22 Fix parsing of overloaded parametric datatype selectors (#2819)Andrew Reynolds
2019-01-22New README (markdown). (#2797)Aina Niemetz
2019-01-19Fix missing-override warning (#2811)Andres Noetzli
2019-01-18Extract DIMACS Printing (#2800)Alex Ozdemir
2019-01-18Strings: Introduce checkEntailContains() (#2809)Andres Noetzli
2019-01-18 Fix ABC build (#2808)Andres Noetzli
2019-01-16Add option to print BV constants in binary (#2805)Andres Noetzli
2019-01-16Update NEWS file (#2804)Andres Noetzli
2019-01-16Bugfix: LFSC clause equality (#2801)Alex Ozdemir
2019-01-15Extended Resolution Signature (#2788)Alex Ozdemir
2019-01-15Fix constant contains ITOS rewrite (#2799)Andrew Reynolds
2019-01-15CMake: Fix search for static libraries (#2798)Andres Noetzli
2019-01-15Strings: Add option to change loop process mode (#2794)Andres Noetzli
2019-01-15 Fix unsound double abs rewrite rule for FP (#2792)Andrew Reynolds
2019-01-14 Only check disequal terms with sygus-rr-verify (#2793)Andrew Reynolds
2019-01-14ClausalBitvectorProof (#2786)Alex Ozdemir
2019-01-13LFSC LRAT Output (#2787)Alex Ozdemir
2019-01-11LratInstruction inheritance (#2784)Alex Ozdemir
2019-01-11Fixed linking against drat2er, and use drat2er (#2785)Alex Ozdemir
2019-01-11New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)Aina Niemetz
2019-01-10New C++ API: Get rid of mkConst functions (simplify API). (#2783)Aina Niemetz
2019-01-09Do not rewrite 1-constructor sygus testers to true (#2780)Andrew Reynolds
2019-01-09[BV Proofs] Option for proof format (#2777)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback