cvc5.git
2021-03-18 Andrew ReynoldsEliminate dependency on quantifiers engine in quantifie...
2021-03-18 Abdalrhman... Eliminate more uses of SExpr. (#6149)
2021-03-18 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-17 Andrew Reynolds(proof-new) Fixes to set defaults (#6163)
2021-03-17 Andrew ReynoldsMove utilities for inferred bounds on quantifers to...
2021-03-17 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-17 Aina NiemetzRename test/unit/expr to test/unit/node. (#6156)
2021-03-17 Aina NiemetzRename fixtures in test/unit/context to conform to...
2021-03-17 Aina NiemetzRename fixtures in test/unit/base to conform to naming...
2021-03-16 Mathias Preinerci: Enable checking of proofs + unsat cores. (#6088)
2021-03-16 Haniel Barbosa[proof-new] Activating proofs when dumping proofs ...
2021-03-16 Andrew ReynoldsFurther standardization of strings statistics (#6128)
2021-03-16 Mathias Preinercmake: Generate cvc4_export.h and set visibility to...
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with...
2021-03-16 Haniel Barbosa[proof-new] Disabling proofs on regressions with known...
2021-03-16 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-15 Andrew ReynoldsFix rewrite for double replace (#6152)
2021-03-15 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126)
2021-03-15 Gereon KremerDisable sqlite (#6145)
2021-03-15 Andrew ReynoldsMake nonlinear extension account for relevant term...
2021-03-15 Andrew ReynoldsSplit inst match generator class to own file (#6125)
2021-03-15 Andrew ReynoldsLetify quantifier bodies independently (#6112)
2021-03-15 Andrew ReynoldsReorganizing initialization of term registry in quantif...
2021-03-15 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-15 Aina NiemetzNew C++ Api: Comprehensive guards for member functions...
2021-03-14 Diego Della... [proof-new] Adding a dot printer for proof nodes (...
2021-03-12 Aina NiemetzNew C++ Api: Move checks to separate file. (#6138)
2021-03-12 Aina NiemetzNew C++ API: Rename TRY CATCH macros. (#6135)
2021-03-12 Andres NoetzliSchedule preregistration lemmas to be satisfied after...
2021-03-12 Mathias Preinercmake: Remove install rules for old API headers. (...
2021-03-12 Andrew Reynolds(proof-new) Miscellaneous sync to master (#6129)
2021-03-12 Haniel Barbosa[proof-new] Fix arity check when building equality...
2021-03-12 Gereon KremerAdd missing includes for statistics (#6124)
2021-03-12 Andrew ReynoldsSimplify instantiation match generator interface (...
2021-03-12 Aina NiemetzAdd more unit tests for api::Sort. (#6122)
2021-03-12 Mathias Preinerci: Replace debug builds with assertion enabled product...
2021-03-11 Gereon KremerMake linear arithmetic use its inference manager (...
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118)
2021-03-11 Andrew ReynoldsIntroduce inference ids for quantifier instantiation...
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105)
2021-03-11 Aina NiemetzDelete Expr layer. (#6117)
2021-03-11 MikolasJanotaImprovements and refactoring for enumeratative strategy...
2021-03-11 Andrew Reynolds(proof-new) Clean up uses of witness with skolem lemmas...
2021-03-11 Andrew ReynoldsDirect lemmas and inference ids for sygus extension...
2021-03-11 Mathias PreinerFix compile warnings when compiling with GLPK. (#6115)
2021-03-11 Aina NiemetzRemove obsolete test/api/statistics.cpp. (#6116)
2021-03-11 Aina NiemetzClean up ownership of Datatypes in NodeManager. (#6113)
2021-03-11 Aina NiemetzRefactor Node::getOperator() to fix compiler warning...
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099)
2021-03-11 Mathias PreinerAdd GitHub action to automatically update approved...
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095)
2021-03-10 Aina NiemetzNew C++ Api: Add missing argument checks in Solver...
2021-03-10 Andrew ReynoldsAdd Env class (#6093)
2021-03-10 Andrew V. JonesImproved handing of 'lib64' vs. 'lib' for glpk-cut...
2021-03-10 Haniel Barbosa[proof-new] Clarifying doc (#6108)
2021-03-10 Aina NiemetzMove ExprManager::isNAryKind to NodeManager. (#6107)
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106)
2021-03-10 Mathias Preinercmake: Fix optimization level for debug builds. (#6097)
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ...
2021-03-10 Andrew ReynoldsFix extended equality rewrite involving replace. (...
2021-03-10 Andrew ReynoldsFix term registration and non-theory-preprocessed terms...
2021-03-10 Andrew ReynoldsAdd quant elim regression (#6103)
2021-03-10 Andrew Reynolds(proof-new) Replace witness form by original form in...
2021-03-10 Mathias Preinertest: Fix missing std::. (#6096)
2021-03-09 Aina NiemetzNew C++ Api: Use const ref for arguments when possible...
2021-03-09 Andrew ReynoldsMerge initialization steps in TheoryModelBuilder (...
2021-03-09 Andrew ReynoldsRemove logic request (#6089)
2021-03-09 Aina NiemetzNew C++ Api: Migrate stats collection for consts, vars...
2021-03-09 Aina NiemetzContextObj::destroy(): Guard against invalid use. ...
2021-03-09 Aina NiemetzNew C++ Api: Clean up usage of internal kind. (#6087)
2021-03-09 Andrew Reynolds(proof-new) Minor fix and allow proof option (#6085)
2021-03-09 Aina NiemetzNew C++ API: Reorder and clean up cpp file. (#6086)
2021-03-09 Gereon KremerAdd missing include if GLPK is enabled. (#6084)
2021-03-09 Gereon KremerSome more cleanup of includes (#6083)
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081)
2021-03-09 Aina NiemetzNew C++ API: Migrate to Node layer. (#6070)
2021-03-08 Aina NiemetzRefactor ouroborous API test to not use Expr. (#6079)
2021-03-08 Mathias Preinercontrib: Do not use HOST env variable for cross-compila...
2021-03-08 Andrew ReynoldsFix handling of negation of Boolean bound variables...
2021-03-08 Aina NiemetzBuild api tests in build/bin/test/api. (#6076)
2021-03-08 Andrew Reynolds(proof-new) Separating optimizations for strings skolem...
2021-03-08 Andrew Reynolds(proof-new) Prepare arithmetic for changes to ppRewrite...
2021-03-08 Andrew ReynoldsSimplify theory preprocessing (#6058)
2021-03-08 Gereon KremerFix justification heuristic again (#6074)
2021-03-08 Andrew ReynoldsDo not process conjunctions as facts in strings (#6065)
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069)
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068)
2021-03-05 yoni206Set logic in interpolation unit test. (#6067)
2021-03-05 mcjunehoInitial implementation of an optimization solver with...
2021-03-05 Aina Niemetzgoogle test: Remove obsolete Expr test fixtures. (...
2021-03-05 Gereon KremerReimplement time limit mechanism for windows (#6049)
2021-03-05 Aina Niemetzgoogle test: Remove dependency on ExprManager in type_c...
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of interal datatype classes...
2021-03-04 Aina NiemetzAdd initial bit-blaster for proof logging. (#6053)
2021-03-04 Aina NiemetzNew C++ Api: Clean up usage of internal types in Term...
2021-03-04 Gereon KremerAdd proper define for libpoly usage (#6050)
2021-03-04 Gereon KremerAdd cmake scripts for iwyu targets. (#6042)
2021-03-04 Aina NiemetzFix nightlies. (#6052)
2021-03-04 Gereon KremerIgnore isInConflict when adding conflicts (#5995)
next