projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-04-22
Aina Niemetz
api docs: Remove file reintroduced in past merge. ...
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Fix models for sygus-inference, bv2int, real2int (...
commit
|
commitdiff
|
tree
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
commit
|
commitdiff
|
tree
2021-04-22
Andres Noetzli
Allow in-place construction of `CDList` items (#6409)
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Move expand definition from Theory to TheoryRewriter...
commit
|
commitdiff
|
tree
2021-04-21
Aina Niemetz
Arithmetic: Move implementation of type rules to cpp...
commit
|
commitdiff
|
tree
2021-04-21
Aina Niemetz
UF: Move implementation of type rules to cpp. (#6403)
commit
|
commitdiff
|
tree
2021-04-21
Gereon Kremer
Add explicit dependencies for base lib (#6410)
commit
|
commitdiff
|
tree
2021-04-21
Gereon Kremer
Pass GMP to libpoly (#6411)
commit
|
commitdiff
|
tree
2021-04-21
Aina Niemetz
Datatypes: Move implementation of type rules to cpp...
commit
|
commitdiff
|
tree
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
commit
|
commitdiff
|
tree
2021-04-21
Mathias Preiner
cmake: Add optional module name argument for check_pyth...
commit
|
commitdiff
|
tree
2021-04-21
Aina Niemetz
Sets: Move implementation of type rules to cpp. (#6401)
commit
|
commitdiff
|
tree
2021-04-21
Aina Niemetz
Arrays: Move implementation of type rules to cpp. ...
commit
|
commitdiff
|
tree
2021-04-21
Andrew Reynolds
Add unit test for abduction (#6400)
commit
|
commitdiff
|
tree
2021-04-21
Andrew Reynolds
Add basic utilities for new implementation of justifica...
commit
|
commitdiff
|
tree
2021-04-21
mudathirmahgoub
Add getNumIndices to Op (#6386)
commit
|
commitdiff
|
tree
2021-04-20
Andrew Reynolds
Split FP expand definitions to own module (#6392)
commit
|
commitdiff
|
tree
2021-04-20
Aina Niemetz
BV: Move implementation of type rules from header to...
commit
|
commitdiff
|
tree
2021-04-20
Aina Niemetz
Sep: Move implementation of type rules to cpp. (#6402)
commit
|
commitdiff
|
tree
2021-04-20
Aina Niemetz
Quantifiers: Move implementation of type rules to cpp...
commit
|
commitdiff
|
tree
2021-04-20
Gereon Kremer
Add InferenceId as resources (#6339)
commit
|
commitdiff
|
tree
2021-04-20
Andrew Reynolds
Add instantiation pool feature to the API (#6358)
commit
|
commitdiff
|
tree
2021-04-20
Gereon Kremer
Split C++ API docs from general docs (#6365)
commit
|
commitdiff
|
tree
2021-04-20
Aina Niemetz
Remove support for CVC3 language. (#6369)
commit
|
commitdiff
|
tree
2021-04-20
Gereon Kremer
Basic setup for examples in documentation (#6383)
commit
|
commitdiff
|
tree
2021-04-20
Aina Niemetz
Add guards to disable clang-format around placeholders...
commit
|
commitdiff
|
tree
2021-04-20
Andres Noetzli
Fix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)
commit
|
commitdiff
|
tree
2021-04-20
Gereon Kremer
Properly link Poly against GMP (#6398)
commit
|
commitdiff
|
tree
2021-04-20
yoni206
python API sorts: adding functions and tests (#6361)
commit
|
commitdiff
|
tree
2021-04-19
Andrew Reynolds
Fully incorporate quantifiers macros into ppAssert...
commit
|
commitdiff
|
tree
2021-04-19
Gereon Kremer
Remove linking against gmp and cln in tests and parser...
commit
|
commitdiff
|
tree
2021-04-16
Gereon Kremer
Fix dependencies for stats options (#6378)
commit
|
commitdiff
|
tree
2021-04-16
Andrew Reynolds
Fix ONCE for post-rewrite (#6372)
commit
|
commitdiff
|
tree
2021-04-16
Gereon Kremer
Refactor cmake: auto-download and default-on dependenci...
commit
|
commitdiff
|
tree
2021-04-16
Gereon Kremer
Replace SExpr class by simpler conversion routines...
commit
|
commitdiff
|
tree
2021-04-16
Mathias Preiner
cmake: Build object libraries for base and context...
commit
|
commitdiff
|
tree
2021-04-15
Aina Niemetz
preprocessing context: Add wrapper for model substituti...
commit
|
commitdiff
|
tree
2021-04-15
Mathias Preiner
Build support library from base and context. (#6368)
commit
|
commitdiff
|
tree
2021-04-15
Gereon Kremer
Avoid options listener for resource manager. (#6366)
commit
|
commitdiff
|
tree
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
commit
|
commitdiff
|
tree
2021-04-15
Gereon Kremer
Fix printing of stats when aborted. (#6362)
commit
|
commitdiff
|
tree
2021-04-15
Andrew Reynolds
Reenable regression for minimizing instantiations ...
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Fix type rule for relations join image (#6349)
commit
|
commitdiff
|
tree
2021-04-14
Gereon Kremer
Improve documentation for FP rounding mode, add bibliog...
commit
|
commitdiff
|
tree
2021-04-14
Gereon Kremer
Improve documentation of API kinds (#6341)
commit
|
commitdiff
|
tree
2021-04-14
Gereon Kremer
Improve documentation for API exceptions (#6340)
commit
|
commitdiff
|
tree
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
commit
|
commitdiff
|
tree
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
commit
|
commitdiff
|
tree
2021-04-14
Haniel Barbosa
[unsat-cores] Improving new unsat cores (#6356)
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Add internal API methods for pool-based instantiation...
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Add interface for getting relevant assertions (#5131)
commit
|
commitdiff
|
tree
2021-04-14
Abdalrhman...
Merge equivalent sub-obligations instead of discarding...
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Warn about infeasible SyGuS conjectures (#6345)
commit
|
commitdiff
|
tree
2021-04-14
Haniel Barbosa
[proof-new] Fix explanation of literals in SAT proof...
commit
|
commitdiff
|
tree
2021-04-14
Haniel Barbosa
[proof-new] Miscellaneous improvements to dot printer...
commit
|
commitdiff
|
tree
2021-04-14
Gereon Kremer
Fix libpoly build and use new release (#6354)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Add pool instantiation strategy (#6308)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Refactor quantifiers macros (#6348)
commit
|
commitdiff
|
tree
2021-04-13
Mathias Preiner
ci: Use CVC5_REGRESSION_ARGS. (#6347)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Formalize more skolems (#6307)
commit
|
commitdiff
|
tree
2021-04-13
Aina Niemetz
API docs: Add custom target to build for GH pages....
commit
|
commitdiff
|
tree
2021-04-13
Abdalrhman...
Avoid using substitute's input cache after the method...
commit
|
commitdiff
|
tree
2021-04-13
Abdalrhman...
Fix sexpr bug with AST output language. (#6329)
commit
|
commitdiff
|
tree
2021-04-13
Aina Niemetz
Bags: Move more implementation of type rule from header...
commit
|
commitdiff
|
tree
2021-04-12
Aina Niemetz
Strings: Move implementation of type rules from header...
commit
|
commitdiff
|
tree
2021-04-12
Andrew Reynolds
Fix computation of whether a type is finite (#6312)
commit
|
commitdiff
|
tree
2021-04-12
Gereon Kremer
Refactor resource manager (#6322)
commit
|
commitdiff
|
tree
2021-04-12
Gereon Kremer
Only require GMP 6.1 (#6332)
commit
|
commitdiff
|
tree
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
commit
|
commitdiff
|
tree
2021-04-12
Andrew Reynolds
Consolidate interface to prop engine (#6189)
commit
|
commitdiff
|
tree
2021-04-12
Andres Noetzli
Fix GitHub Actions macOS build (#6331)
commit
|
commitdiff
|
tree
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
commit
|
commitdiff
|
tree
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
commit
|
commitdiff
|
tree
2021-04-09
Aina Niemetz
New C++ Api: Initial layout of Api documentation. ...
commit
|
commitdiff
|
tree
2021-04-09
Haniel Barbosa
[proof-new] Optimizing sat proof (#6324)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Add identifiers for extended function reductions (...
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Add regressions for issue 6214 (#6305)
commit
|
commitdiff
|
tree
2021-04-09
Andres Noetzli
Learn equalities involving Boolean variables (#6323)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Avoid spurious runs in run_regression.py (#6318)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Use expr miner timeout (#6321)
commit
|
commitdiff
|
tree
2021-04-09
Gereon Kremer
Add missing InferenceIds to toString (#6320)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Fix run_regression for cvc expected outputs (#6317)
commit
|
commitdiff
|
tree
2021-04-08
Gereon Kremer
Use newer version of update-pr-branch action. (#6315)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Use exceptions when constructing malformed datatypes...
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add benchmark for issue 5101 (#6301)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add benchmark for issue 4400 (#6288)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Initial support for parametric datatypes in sygus ...
commit
|
commitdiff
|
tree
2021-04-07
Aina Niemetz
Remove old API header. (#6309)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add cardinality class definition (#6302)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add benchmark for 6270 (#6283)
commit
|
commitdiff
|
tree
2021-04-07
Haniel Barbosa
[proof-new] Fixing SMT post-processor's handling of...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add benchmark for issue 4420 (#6286)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Set incomplete if not applying ho extensionality (...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Fixes for abducts (#6279)
commit
|
commitdiff
|
tree
2021-04-07
Aina Niemetz
New C++ Api: Rename and move checks.h. (#6306)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
(proof-new) Proper implementation of proof node cloning...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add term pools utility (#6243)
commit
|
commitdiff
|
tree
2021-04-07
Aina Niemetz
New C++ Api: Initial setup of Api documentation. (...
commit
|
commitdiff
|
tree
next