projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-03-18
Gereon Kremer
Move stats registry to env. (#6173)
commit
|
commitdiff
|
tree
2021-03-18
Andrew Reynolds
Eliminate dependency on quantifiers engine in quantifie...
commit
|
commitdiff
|
tree
2021-03-18
Abdalrhman...
Eliminate more uses of SExpr. (#6149)
commit
|
commitdiff
|
tree
2021-03-18
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-17
Andrew Reynolds
(proof-new) Fixes to set defaults (#6163)
commit
|
commitdiff
|
tree
2021-03-17
Andrew Reynolds
Move utilities for inferred bounds on quantifers to...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename test/unit/expr to test/unit/node. (#6156)
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename fixtures in test/unit/context to conform to...
commit
|
commitdiff
|
tree
2021-03-17
Aina Niemetz
Rename fixtures in test/unit/base to conform to naming...
commit
|
commitdiff
|
tree
2021-03-16
Mathias Preiner
ci: Enable checking of proofs + unsat cores. (#6088)
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Activating proofs when dumping proofs ...
commit
|
commitdiff
|
tree
2021-03-16
Andrew Reynolds
Further standardization of strings statistics (#6128)
commit
|
commitdiff
|
tree
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
commit
|
commitdiff
|
tree
2021-03-16
Haniel Barbosa
[proof-new] Disabling proofs on regressions with known...
commit
|
commitdiff
|
tree
2021-03-16
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Fix rewrite for double replace (#6152)
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Gereon Kremer
Replace HistogramStat by IntegralHistogramStat (#6126)
commit
|
commitdiff
|
tree
2021-03-15
Gereon Kremer
Disable sqlite (#6145)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Make nonlinear extension account for relevant term...
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Split inst match generator class to own file (#6125)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Letify quantifier bodies independently (#6112)
commit
|
commitdiff
|
tree
2021-03-15
Andrew Reynolds
Reorganizing initialization of term registry in quantif...
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-15
Aina Niemetz
New C++ Api: Comprehensive guards for member functions...
commit
|
commitdiff
|
tree
2021-03-14
Diego Della...
[proof-new] Adding a dot printer for proof nodes (...
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
New C++ Api: Move checks to separate file. (#6138)
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
New C++ API: Rename TRY CATCH macros. (#6135)
commit
|
commitdiff
|
tree
2021-03-12
Andres Noetzli
Schedule preregistration lemmas to be satisfied after...
commit
|
commitdiff
|
tree
2021-03-12
Mathias Preiner
cmake: Remove install rules for old API headers. (...
commit
|
commitdiff
|
tree
2021-03-12
Andrew Reynolds
(proof-new) Miscellaneous sync to master (#6129)
commit
|
commitdiff
|
tree
2021-03-12
Haniel Barbosa
[proof-new] Fix arity check when building equality...
commit
|
commitdiff
|
tree
2021-03-12
Gereon Kremer
Add missing includes for statistics (#6124)
commit
|
commitdiff
|
tree
2021-03-12
Andrew Reynolds
Simplify instantiation match generator interface (...
commit
|
commitdiff
|
tree
2021-03-12
Aina Niemetz
Add more unit tests for api::Sort. (#6122)
commit
|
commitdiff
|
tree
2021-03-12
Mathias Preiner
ci: Replace debug builds with assertion enabled product...
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
Make linear arithmetic use its inference manager (...
commit
|
commitdiff
|
tree
2021-03-11
Alex Ozdemir
arith proof rules shuffle & add ARITH_SUM_UB (#6118)
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
Introduce inference ids for quantifier instantiation...
commit
|
commitdiff
|
tree
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
commit
|
commitdiff
|
tree
2021-03-11
MikolasJanota
Improvements and refactoring for enumeratative strategy...
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
(proof-new) Clean up uses of witness with skolem lemmas...
commit
|
commitdiff
|
tree
2021-03-11
Andrew Reynolds
Direct lemmas and inference ids for sygus extension...
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Fix compile warnings when compiling with GLPK. (#6115)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Remove obsolete test/api/statistics.cpp. (#6116)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Clean up ownership of Datatypes in NodeManager. (#6113)
commit
|
commitdiff
|
tree
2021-03-11
Aina Niemetz
Refactor Node::getOperator() to fix compiler warning...
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)
commit
|
commitdiff
|
tree
2021-03-11
Mathias Preiner
Add GitHub action to automatically update approved...
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
Use Assert instead of assert. (#6095)
commit
|
commitdiff
|
tree
2021-03-10
Aina Niemetz
New C++ Api: Add missing argument checks in Solver...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Add Env class (#6093)
commit
|
commitdiff
|
tree
2021-03-10
Andrew V. Jones
Improved handing of 'lib64' vs. 'lib' for glpk-cut...
commit
|
commitdiff
|
tree
2021-03-10
Haniel Barbosa
[proof-new] Clarifying doc (#6108)
commit
|
commitdiff
|
tree
2021-03-10
Aina Niemetz
Move ExprManager::isNAryKind to NodeManager. (#6107)
commit
|
commitdiff
|
tree
2021-03-10
Gereon Kremer
Improve arithmetic proofs (#6106)
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
cmake: Fix optimization level for debug builds. (#6097)
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
(proof-new) Update ppRewrite to use skolem lemmas ...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Fix extended equality rewrite involving replace. (...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Fix term registration and non-theory-preprocessed terms...
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
Add quant elim regression (#6103)
commit
|
commitdiff
|
tree
2021-03-10
Andrew Reynolds
(proof-new) Replace witness form by original form in...
commit
|
commitdiff
|
tree
2021-03-10
Mathias Preiner
test: Fix missing std::. (#6096)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ Api: Use const ref for arguments when possible...
commit
|
commitdiff
|
tree
2021-03-09
Andrew Reynolds
Merge initialization steps in TheoryModelBuilder (...
commit
|
commitdiff
|
tree
2021-03-09
Andrew Reynolds
Remove logic request (#6089)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ Api: Migrate stats collection for consts, vars...
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
ContextObj::destroy(): Guard against invalid use. ...
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ Api: Clean up usage of internal kind. (#6087)
commit
|
commitdiff
|
tree
2021-03-09
Andrew Reynolds
(proof-new) Minor fix and allow proof option (#6085)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ API: Reorder and clean up cpp file. (#6086)
commit
|
commitdiff
|
tree
2021-03-09
Gereon Kremer
Add missing include if GLPK is enabled. (#6084)
commit
|
commitdiff
|
tree
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
commit
|
commitdiff
|
tree
2021-03-09
Aina Niemetz
New C++ API: Migrate to Node layer. (#6070)
commit
|
commitdiff
|
tree
2021-03-08
Aina Niemetz
Refactor ouroborous API test to not use Expr. (#6079)
commit
|
commitdiff
|
tree
2021-03-08
Mathias Preiner
contrib: Do not use HOST env variable for cross-compila...
commit
|
commitdiff
|
tree
2021-03-08
Andrew Reynolds
Fix handling of negation of Boolean bound variables...
commit
|
commitdiff
|
tree
2021-03-08
Aina Niemetz
Build api tests in build/bin/test/api. (#6076)
commit
|
commitdiff
|
tree
2021-03-08
Andrew Reynolds
(proof-new) Separating optimizations for strings skolem...
commit
|
commitdiff
|
tree
2021-03-08
Andrew Reynolds
(proof-new) Prepare arithmetic for changes to ppRewrite...
commit
|
commitdiff
|
tree
2021-03-08
Andrew Reynolds
Simplify theory preprocessing (#6058)
commit
|
commitdiff
|
tree
2021-03-08
Gereon Kremer
Fix justification heuristic again (#6074)
commit
|
commitdiff
|
tree
2021-03-08
Andrew Reynolds
Do not process conjunctions as facts in strings (#6065)
commit
|
commitdiff
|
tree
2021-03-06
Mathias Preiner
Remove partial UDIV/UREM operators. (#6069)
commit
|
commitdiff
|
tree
2021-03-06
Mathias Preiner
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
commit
|
commitdiff
|
tree
2021-03-05
yoni206
Set logic in interpolation unit test. (#6067)
commit
|
commitdiff
|
tree
2021-03-05
mcjuneho
Initial implementation of an optimization solver with...
commit
|
commitdiff
|
tree
2021-03-05
Aina Niemetz
google test: Remove obsolete Expr test fixtures. (...
commit
|
commitdiff
|
tree
2021-03-05
Gereon Kremer
Reimplement time limit mechanism for windows (#6049)
commit
|
commitdiff
|
tree
2021-03-05
Aina Niemetz
google test: Remove dependency on ExprManager in type_c...
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
New C++ API: Clean up usage of interal datatype classes...
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
Add initial bit-blaster for proof logging. (#6053)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
New C++ Api: Clean up usage of internal types in Term...
commit
|
commitdiff
|
tree
2021-03-04
Gereon Kremer
Add proper define for libpoly usage (#6050)
commit
|
commitdiff
|
tree
2021-03-04
Gereon Kremer
Add cmake scripts for iwyu targets. (#6042)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
Fix nightlies. (#6052)
commit
|
commitdiff
|
tree
next