projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[proof-new] Connecting new unsat cores (#5834)
[cvc5.git] / proofs /
2020-10-02 Alex OzdemirRemove duplicate declarations in th_bv.plf (#5183) tree | commitdiff
2020-09-01 FabianWolffFix spelling errors (#4977) tree | commitdiff
2020-07-01 Andres NoetzliAdd testing infrastructure for LFSC signatures (#4678) tree | commitdiff
2020-02-22 Alex OzdemirRIP th_lra.plf (#3796) tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-21 Alex OzdemirRemove IntReal tightening axioms from th_lira.plf ... tree | commitdiff
2020-02-10 Alex OzdemirAdd more IntReal predicates (#3731) tree | commitdiff
2020-01-26 Alex OzdemirAxioms for affine function bounds. Tests. (#3632) tree | commitdiff
2020-01-21 Alex OzdemirTypes and side conditions for affine bounds (#3631) tree | commitdiff
2020-01-21 Alex OzdemirAffine Axioms (#3630) tree | commitdiff
2020-01-21 Alex OzdemirTypes & side-conditions for linear and affine fns ... tree | commitdiff
2020-01-21 Alex OzdemirAxioms (and side conditions) for tightening bounds... tree | commitdiff
2020-01-18 Alex OzdemirLIRA proof: Arithmetic predicates & reification thereof... tree | commitdiff
2020-01-17 Alex OzdemirLIRA sig: int, real terms, and conversions (#3610) tree | commitdiff
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... tree | commitdiff
2019-11-19 Alex OzdemirSignature documentation update (#3476) tree | commitdiff
2019-08-06 Andrew ReynoldsFix drat signature wrt side condition return types... tree | commitdiff
2019-06-05 Alex OzdemirDRAT-Optimization (#2971) tree | commitdiff
2019-06-04 Andres NoetzliEnable proof checking for QF_LRA benchmarks (#2928) tree | commitdiff
2019-03-29 Haniel Barbosaremoving deprecated rewriting signature / example ... tree | commitdiff
2019-03-28 Haniel Barbosafix ex_bv.plf (#2905) tree | commitdiff
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847) tree | commitdiff
2019-01-24 Alex OzdemirExtended DRAT signature to operational DRAT (#2815) tree | commitdiff
2019-01-16 Alex OzdemirBugfix: LFSC clause equality (#2801) tree | commitdiff
2019-01-16 Alex OzdemirExtended Resolution Signature (#2788) tree | commitdiff
2018-12-17 Alex OzdemirDRAT Signature (#2757) tree | commitdiff
2018-12-12 Alex Ozdemir[LRA proof] More complete LRA example proofs. (#2722) tree | commitdiff
2018-12-12 Alex Ozdemir[LRAT] signature robust against duplicate literals... tree | commitdiff
2018-12-11 Alex OzdemirLRAT signature (#2731) tree | commitdiff
2018-11-27 Alex OzdemirLRA proof signature fixes and a first proof for linear... tree | commitdiff
2018-10-19 Mathias PreinerRemove autotools build system. (#2639) tree | commitdiff
2018-09-22 Mathias Preinercmake: Add make install rule. tree | commitdiff
2018-09-22 Mathias Preinercmake: Only build libcvc4 and libcvc4parser as libraries. tree | commitdiff
2018-09-22 Mathias Preinercmake: Add libsignatures for proofs. tree | commitdiff
2018-09-22 Aina Niemetzcmake: .cpp generation done, .h generation not yet... tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-04-02 yoni206a formula should be an instance of itself (#1668) tree | commitdiff
2018-03-20 yoni206correct instruction for running example (#1669) tree | commitdiff
2017-08-25 Aina NiemetzMove LFSC checker out of the CVC repository. (#222) tree | commitdiff
2017-08-24 Andrew ReynoldsMerge pull request #191 from timothy-king/cleanup-regexp tree | commitdiff
2017-07-30 Andres NoetzliChange remaining hash_set -> unordered_set (#208) tree | commitdiff
2017-04-06 Clark BarrettMerge pull request #143 from FabianWolff/master tree | commitdiff
2017-04-05 Andrew ReynoldsMerge pull request #145 from 4tXJ7f/fix_lfsc_args tree | commitdiff
2017-04-05 Andres Notzli[LFSC] Fix segfault tree | commitdiff
2017-04-04 Fabian WolffFix several spelling errors tree | commitdiff
2017-03-17 guykatzzbetter support for proof production when encountering... tree | commitdiff
2017-03-14 Clark BarrettMerge pull request #132 from 4tXJ7f/fix_mingw64 tree | commitdiff
2017-03-09 guykatzzbug fix tree | commitdiff
2017-03-09 guykatzzbetter proof support for bools and formulas tree | commitdiff
2017-03-06 Clark BarrettAdding support for bool-to-bv tree | commitdiff
2017-01-18 Andrew ReynoldsMerge pull request #128 from 4tXJ7f/fix_lfsc_perf tree | commitdiff
2017-01-16 Andres Notzli[LFSC] Fix performance issues, more determinism tree | commitdiff
2017-01-04 Tim KingMarking the proof signature files as non-executable. tree | commitdiff
2017-01-04 Tim KingReverting two files encoding with DOS linebreaks back... tree | commitdiff
2017-01-04 Andrew ReynoldsMerge pull request #122 from 4tXJ7f/fix_lfsc_str tree | commitdiff
2017-01-04 guykatzzMerge pull request #120 from 4tXJ7f/fix_f_pp_holes tree | commitdiff
2017-01-04 Andrew ReynoldsMerge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks tree | commitdiff
2016-12-28 Andres Notzli[LFSC] Minor fixes/improvements tree | commitdiff
2016-12-28 Andres Notzli[LFSC] Fix memory leaks when creating CExprs tree | commitdiff
2016-10-13 Tim KingRevert "Merge branch 'origin' of https://github.com... tree | commitdiff
2016-10-11 Paul MengMerge branch 'origin' of https://github.com/CVC4/CVC4.git tree | commitdiff
2016-10-01 Tim KingMerge pull request #93 from timothy-king/clang-format tree | commitdiff
2016-09-25 Tim KingAdding virtual destructors to several classes in expr.h . tree | commitdiff
2016-08-24 PaulMengMerge remote-tracking branch 'origin/master' tree | commitdiff
2016-08-15 ajreynolExpression sharing on demand in LFSC (replace definitio... tree | commitdiff
2016-08-06 guykatzzMerge pull request #88 from 4tXJ7f/fix_comments tree | commitdiff
2016-08-05 Andres NotzliMinor: add/fix comments, remove redundant includes tree | commitdiff
2016-07-05 PaulMengMerge branch 'master' of https://github.com/CVC4/CVC4.git tree | commitdiff
2016-06-08 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 tree | commitdiff
2016-06-08 GuySupport for printing a global let map in LFSC proofs. tree | commitdiff
2016-06-06 guykatzzMerge pull request #85 from CVC4/master_for_proof_merge tree | commitdiff
2016-06-03 GuyBetter infrastructure for proving constant disequality. tree | commitdiff
2016-06-03 GuyA better mechanism for handling BV terms with aliases... tree | commitdiff
2016-06-02 GuyMerge from proof branch tree | commitdiff
2016-06-02 GuyRevert "Merging proof branch" tree | commitdiff
2016-06-02 GuyMerging proof branch tree | commitdiff
2016-05-05 ajreynolCompute term indices lazily in TermDb. Optimization... tree | commitdiff
2016-05-02 ajreynolClean up issues related to compiled scc in LFSC. Refact... tree | commitdiff
2016-04-20 PaulMengupdate from the master tree | commitdiff
2016-03-23 guykatzzMerge pull request #82 from CVC4/master_for_merge tree | commitdiff
2016-03-23 Guysquash-merge from proof branch tree | commitdiff
2016-01-27 Liana HadareanMerged bit-vector and uf proof branch. tree | commitdiff
2015-05-12 barrettcwMerge pull request #74 from finnhaedicke/namespace_minisat tree | commitdiff
2015-04-23 Clark BarrettMerge branch 'master' into google tree | commitdiff
2015-04-23 Clark BarrettA few more minor updates to match google repository... tree | commitdiff
2015-04-21 Clark BarrettChanges needed to compile at Google, plus some bug... tree | commitdiff
2015-03-10 ajreynolCNF proofs. Infrastructure for preprocessing proofs... tree | commitdiff
2014-11-10 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-11-05 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-17 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-16 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-11 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-10 Kshitij BansalMerge remote-tracking branch 'origin/1.4.x' tree | commitdiff
2014-10-09 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-07 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-06 Morgan DetersMerge branch '1.4.x' tree | commitdiff
2014-10-06 Morgan DetersMerge branch '1.4.x' tree | commitdiff
next