projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[Docs] Update `EnumDocumenter` for newer Sphinx (#8914)
[cvc5.git]
/
proofs
/
2022-06-23
mudathirmahgoub
Add set.fold operator (#8867)
tree
|
commitdiff
2022-06-07
mudathirmahgoub
Add set.filter operator and its inference rules (#8856)
tree
|
commitdiff
2022-06-07
Andrew Reynolds
Add str.unit to LFSC signature (#8862)
tree
|
commitdiff
2022-06-07
mudathirmahgoub
Add set.map signature to lfsc (#8860)
tree
|
commitdiff
2022-05-06
Andrew Reynolds
Fix LFSC side condition for matching premise of concat_...
tree
|
commitdiff
2022-05-03
Andrew Reynolds
Use (non-recursive) unpurified form instead of original...
tree
|
commitdiff
2022-04-19
Andrew Reynolds
Generalize concat conflict for sequences in LFSC (...
tree
|
commitdiff
2022-04-18
Andrew Reynolds
Add some missing FP symbols to LFSC (#8629)
tree
|
commitdiff
2022-04-06
Andrew Reynolds
Fixes for LFSC printing and signatures (#8579)
tree
|
commitdiff
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
tree
|
commitdiff
2022-03-22
Andrew Reynolds
Change null terminator for regular expression intersect...
tree
|
commitdiff
2022-03-13
Andrew Reynolds
Minor sync from proof-new (#8293)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Fixes and additions to LFSC signature (#8205)
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Generalize LFSC string signature to sequences (#8220)
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Syntax fixes for LFSC signature (#8172)
tree
|
commitdiff
2022-02-21
Andrew Reynolds
Fixes and additions for LFSC signatures (#8120)
tree
|
commitdiff
2022-02-07
Andrew Reynolds
Generalize LFSC concat unify for splitting constants...
tree
|
commitdiff
2022-02-03
Andrew Reynolds
Add miscellaneous missing theory definitions for LFSC...
tree
|
commitdiff
2022-02-02
Andrew Reynolds
Make LFSC side condition for concat unify robust to...
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Updates to LFSC signatures (#7840)
tree
|
commitdiff
2021-11-09
Andrew Reynolds
Add LFSC signature for strings (#7523)
tree
|
commitdiff
2021-11-02
Andrew Reynolds
Add LFSC signature for quantifiers (#7540)
tree
|
commitdiff
2021-10-28
Andrew Reynolds
LFSC signature for linear arithmetic (#7445)
tree
|
commitdiff
2021-10-28
Andrew Reynolds
LFSC signature for CNF (#7444)
tree
|
commitdiff
2021-10-28
Andrew Reynolds
LFSC signature for Booleans (#7443)
tree
|
commitdiff
2021-10-28
Andrew Reynolds
LFSC signature for equality (#7442)
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Add LFSC signature for n-ary programs (#7360)
tree
|
commitdiff
2021-10-14
Andrew Reynolds
Add core LFSC signatures (#7289)
tree
|
commitdiff
2021-03-25
Haniel Barbosa
Deleting old LFSC signatures (#6194)
tree
|
commitdiff
2020-10-02
Alex Ozdemir
Remove duplicate declarations in th_bv.plf (#5183)
tree
|
commitdiff
2020-09-01
FabianWolff
Fix spelling errors (#4977)
tree
|
commitdiff
2020-07-01
Andres Noetzli
Add testing infrastructure for LFSC signatures (#4678)
tree
|
commitdiff
2020-02-22
Alex Ozdemir
RIP th_lra.plf (#3796)
tree
|
commitdiff
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
tree
|
commitdiff
2020-02-21
Alex Ozdemir
Remove IntReal tightening axioms from th_lira.plf ...
tree
|
commitdiff
2020-02-10
Alex Ozdemir
Add more IntReal predicates (#3731)
tree
|
commitdiff
2020-01-26
Alex Ozdemir
Axioms for affine function bounds. Tests. (#3632)
tree
|
commitdiff
2020-01-21
Alex Ozdemir
Types and side conditions for affine bounds (#3631)
tree
|
commitdiff
2020-01-21
Alex Ozdemir
Affine Axioms (#3630)
tree
|
commitdiff
2020-01-21
Alex Ozdemir
Types & side-conditions for linear and affine fns ...
tree
|
commitdiff
2020-01-21
Alex Ozdemir
Axioms (and side conditions) for tightening bounds...
tree
|
commitdiff
2020-01-18
Alex Ozdemir
LIRA proof: Arithmetic predicates & reification thereof...
tree
|
commitdiff
2020-01-17
Alex Ozdemir
LIRA 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 Ozdemir
Signature documentation update (#3476)
tree
|
commitdiff
2019-08-06
Andrew Reynolds
Fix drat signature wrt side condition return types...
tree
|
commitdiff
2019-06-05
Alex Ozdemir
DRAT-Optimization (#2971)
tree
|
commitdiff
2019-06-04
Andres Noetzli
Enable proof checking for QF_LRA benchmarks (#2928)
tree
|
commitdiff
2019-03-29
Haniel Barbosa
removing deprecated rewriting signature / example ...
tree
|
commitdiff
2019-03-28
Haniel Barbosa
fix ex_bv.plf (#2905)
tree
|
commitdiff
2019-03-16
Alex Ozdemir
Enable CryptoMiniSat-backed BV proofs (#2847)
tree
|
commitdiff
2019-01-24
Alex Ozdemir
Extended DRAT signature to operational DRAT (#2815)
tree
|
commitdiff
2019-01-16
Alex Ozdemir
Bugfix: LFSC clause equality (#2801)
tree
|
commitdiff
2019-01-16
Alex Ozdemir
Extended Resolution Signature (#2788)
tree
|
commitdiff
2018-12-17
Alex Ozdemir
DRAT 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 Ozdemir
LRAT signature (#2731)
tree
|
commitdiff
2018-11-27
Alex Ozdemir
LRA proof signature fixes and a first proof for linear...
tree
|
commitdiff
2018-10-19
Mathias Preiner
Remove autotools build system. (#2639)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Add make install rule.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Only build libcvc4 and libcvc4parser as libraries.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Add libsignatures for proofs.
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: .cpp generation done, .h generation not yet...
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-04-02
yoni206
a formula should be an instance of itself (#1668)
tree
|
commitdiff
2018-03-20
yoni206
correct instruction for running example (#1669)
tree
|
commitdiff
2017-08-25
Aina Niemetz
Move LFSC checker out of the CVC repository. (#222)
tree
|
commitdiff
2017-08-24
Andrew Reynolds
Merge pull request #191 from timothy-king/cleanup-regexp
tree
|
commitdiff
2017-07-30
Andres Noetzli
Change remaining hash_set -> unordered_set (#208)
tree
|
commitdiff
2017-04-06
Clark Barrett
Merge pull request #143 from FabianWolff/master
tree
|
commitdiff
2017-04-05
Andrew Reynolds
Merge pull request #145 from 4tXJ7f/fix_lfsc_args
tree
|
commitdiff
2017-04-05
Andres Notzli
[LFSC] Fix segfault
tree
|
commitdiff
2017-04-04
Fabian Wolff
Fix several spelling errors
tree
|
commitdiff
2017-03-17
guykatzz
better support for proof production when encountering...
tree
|
commitdiff
2017-03-14
Clark Barrett
Merge pull request #132 from 4tXJ7f/fix_mingw64
tree
|
commitdiff
2017-03-09
guykatzz
bug fix
tree
|
commitdiff
2017-03-09
guykatzz
better proof support for bools and formulas
tree
|
commitdiff
2017-03-06
Clark Barrett
Adding support for bool-to-bv
tree
|
commitdiff
2017-01-18
Andrew Reynolds
Merge 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 King
Marking the proof signature files as non-executable.
tree
|
commitdiff
2017-01-04
Tim King
Reverting two files encoding with DOS linebreaks back...
tree
|
commitdiff
2017-01-04
Andrew Reynolds
Merge pull request #122 from 4tXJ7f/fix_lfsc_str
tree
|
commitdiff
2017-01-04
guykatzz
Merge pull request #120 from 4tXJ7f/fix_f_pp_holes
tree
|
commitdiff
2017-01-04
Andrew Reynolds
Merge 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 King
Revert "Merge branch 'origin' of https://github.com...
tree
|
commitdiff
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-10-01
Tim King
Merge pull request #93 from timothy-king/clang-format
tree
|
commitdiff
2016-09-25
Tim King
Adding virtual destructors to several classes in expr.h .
tree
|
commitdiff
2016-08-24
PaulMeng
Merge remote-tracking branch 'origin/master'
tree
|
commitdiff
2016-08-15
ajreynol
Expression sharing on demand in LFSC (replace definitio...
tree
|
commitdiff
2016-08-06
guykatzz
Merge pull request #88 from 4tXJ7f/fix_comments
tree
|
commitdiff
2016-08-05
Andres Notzli
Minor: add/fix comments, remove redundant includes
tree
|
commitdiff
2016-07-05
PaulMeng
Merge branch 'master' of https://github.com/CVC4/CVC4.git
tree
|
commitdiff
2016-06-08
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
tree
|
commitdiff
2016-06-08
Guy
Support for printing a global let map in LFSC proofs.
tree
|
commitdiff
2016-06-06
guykatzz
Merge pull request #85 from CVC4/master_for_proof_merge
tree
|
commitdiff
next