projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2021-03-04
Gereon Kremer
Ignore isInConflict when adding conflicts (#5995)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
Fix nightlies. (#6048)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
context_black: Clean up classes. (#6046)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
New C++ API: Clean up usage of internal Type/TypeNodes...
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
New C++ API: Clean up usage of internal Result. (#6043)
commit
|
commitdiff
|
tree
2021-03-04
Aina Niemetz
New C++ API: Clean up usage of internal types in Op...
commit
|
commitdiff
|
tree
2021-03-03
Gereon Kremer
Remove obsolete gcc check. (#6041)
commit
|
commitdiff
|
tree
2021-03-03
Andrew Reynolds
(proof-new) Simplifications to arithmetic operator...
commit
|
commitdiff
|
tree
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
commit
|
commitdiff
|
tree
2021-03-03
Abdalrhman...
Remove uses of SExpr class. (#6035)
commit
|
commitdiff
|
tree
2021-03-03
mudathirmahgoub
Add tuple projection operator (#5904)
commit
|
commitdiff
|
tree
2021-03-02
Mathias Preiner
Remove non-ASCII characters from source files. (#6039)
commit
|
commitdiff
|
tree
2021-03-02
Gereon Kremer
Improve handling of utf8 encoded inputs (#5694)
commit
|
commitdiff
|
tree
2021-03-02
Aina Niemetz
Remove obsolete dependency on CxxTest. (#6038)
commit
|
commitdiff
|
tree
2021-03-02
Mathias Preiner
Add aarch64 (ARM64) cross-compile support. (#6033)
commit
|
commitdiff
|
tree
2021-03-02
Mathias Preiner
Fix nightly errors. (#6034)
commit
|
commitdiff
|
tree
2021-03-02
Andrew Reynolds
Introduce quantifiers term registry (#5983)
commit
|
commitdiff
|
tree
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
commit
|
commitdiff
|
tree
2021-03-02
Aina Niemetz
google test: util: Migrate floatingpoint_black. (#6021)
commit
|
commitdiff
|
tree
2021-03-01
Aina Niemetz
google test: theory: Migrate theory_quantifiers_bv_inve...
commit
|
commitdiff
|
tree
2021-03-01
Aina Niemetz
google test: util: Migrate bitvector_black. (#6015)
commit
|
commitdiff
|
tree
2021-03-01
Aina Niemetz
google test: theory: Migrate theory_quantifiers_bv_inst...
commit
|
commitdiff
|
tree
2021-03-01
Gereon Kremer
Refactor collection of debug and trace tags (#5996)
commit
|
commitdiff
|
tree
2021-03-01
Mathias Preiner
Make -Werror optional but enable it for CI. (#6032)
commit
|
commitdiff
|
tree
2021-03-01
Aina Niemetz
google test: util: Migrate stats_black. (#6029)
commit
|
commitdiff
|
tree
2021-03-01
Aina Niemetz
google test: util: Migrate real_algebraic_number_black...
commit
|
commitdiff
|
tree
next