projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-03-18 Andrew ReynoldsEliminate 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 NiemetzNew 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 ReynoldsMove utilities for inferred bounds on quantifers to... commit | commitdiff | tree
2021-03-17 Aina NiemetzNew C++ Api: Comprehensive guards for member functions... commit | commitdiff | tree
2021-03-17 Aina NiemetzRename test/unit/expr to test/unit/node. (#6156) commit | commitdiff | tree
2021-03-17 Aina NiemetzRename fixtures in test/unit/context to conform to... commit | commitdiff | tree
2021-03-17 Aina NiemetzRename fixtures in test/unit/base to conform to naming... commit | commitdiff | tree
2021-03-16 Mathias Preinerci: 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 ReynoldsFurther standardization of strings statistics (#6128) commit | commitdiff | tree
2021-03-16 Mathias Preinercmake: 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 NiemetzNew C++ Api: Comprehensive guards for member functions... commit | commitdiff | tree
2021-03-15 Andrew ReynoldsFix rewrite for double replace (#6152) commit | commitdiff | tree
2021-03-15 Aina NiemetzNew C++ Api: Comprehensive guards for member functions... commit | commitdiff | tree
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) commit | commitdiff | tree
2021-03-15 Gereon KremerDisable sqlite (#6145) commit | commitdiff | tree
2021-03-15 Andrew ReynoldsMake nonlinear extension account for relevant term... commit | commitdiff | tree
2021-03-15 Andrew ReynoldsSplit inst match generator class to own file (#6125) commit | commitdiff | tree
2021-03-15 Andrew ReynoldsLetify quantifier bodies independently (#6112) commit | commitdiff | tree
2021-03-15 Andrew ReynoldsReorganizing initialization of term registry in quantif... commit | commitdiff | tree
2021-03-15 Aina NiemetzNew C++ Api: Comprehensive guards for member functions... commit | commitdiff | tree
2021-03-15 Aina NiemetzNew 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 NiemetzNew C++ Api: Move checks to separate file. (#6138) commit | commitdiff | tree
2021-03-12 Aina NiemetzNew C++ API: Rename TRY CATCH macros. (#6135) commit | commitdiff | tree
2021-03-12 Andres NoetzliSchedule preregistration lemmas to be satisfied after... commit | commitdiff | tree
2021-03-12 Mathias Preinercmake: 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 KremerAdd missing includes for statistics (#6124) commit | commitdiff | tree
2021-03-12 Andrew ReynoldsSimplify instantiation match generator interface (... commit | commitdiff | tree
2021-03-12 Aina NiemetzAdd more unit tests for api::Sort. (#6122) commit | commitdiff | tree
2021-03-12 Mathias Preinerci: Replace debug builds with assertion enabled product... commit | commitdiff | tree
2021-03-11 Gereon KremerMake linear arithmetic use its inference manager (... commit | commitdiff | tree
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) commit | commitdiff | tree
2021-03-11 Andrew ReynoldsIntroduce inference ids for quantifier instantiation... commit | commitdiff | tree
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) commit | commitdiff | tree
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) commit | commitdiff | tree
2021-03-11 MikolasJanotaImprovements 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 ReynoldsDirect lemmas and inference ids for sygus extension... commit | commitdiff | tree
2021-03-11 Mathias PreinerFix compile warnings when compiling with GLPK. (#6115) commit | commitdiff | tree
2021-03-11 Aina NiemetzRemove obsolete test/api/statistics.cpp. (#6116) commit | commitdiff | tree
2021-03-11 Aina NiemetzClean up ownership of Datatypes in NodeManager. (#6113) commit | commitdiff | tree
2021-03-11 Aina NiemetzRefactor Node::getOperator() to fix compiler warning... commit | commitdiff | tree
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099) commit | commitdiff | tree
2021-03-11 Mathias PreinerAdd GitHub action to automatically update approved... commit | commitdiff | tree
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095) commit | commitdiff | tree
2021-03-10 Aina NiemetzNew C++ Api: Add missing argument checks in Solver... commit | commitdiff | tree
2021-03-10 Andrew ReynoldsAdd Env class (#6093) commit | commitdiff | tree
2021-03-10 Andrew V. JonesImproved 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 NiemetzMove ExprManager::isNAryKind to NodeManager. (#6107) commit | commitdiff | tree
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) commit | commitdiff | tree
2021-03-10 Mathias Preinercmake: 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 ReynoldsFix extended equality rewrite involving replace. (... commit | commitdiff | tree
2021-03-10 Andrew ReynoldsFix term registration and non-theory-preprocessed terms... commit | commitdiff | tree
2021-03-10 Andrew ReynoldsAdd 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 Preinertest: Fix missing std::. (#6096) commit | commitdiff | tree
2021-03-09 Aina NiemetzNew C++ Api: Use const ref for arguments when possible... commit | commitdiff | tree
2021-03-09 Andrew ReynoldsMerge initialization steps in TheoryModelBuilder (... commit | commitdiff | tree
2021-03-09 Andrew ReynoldsRemove logic request (#6089) commit | commitdiff | tree
2021-03-09 Aina NiemetzNew C++ Api: Migrate stats collection for consts, vars... commit | commitdiff | tree
2021-03-09 Aina NiemetzContextObj::destroy(): Guard against invalid use. ... commit | commitdiff | tree
2021-03-09 Aina NiemetzNew 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 NiemetzNew C++ API: Reorder and clean up cpp file. (#6086) commit | commitdiff | tree
2021-03-09 Gereon KremerAdd missing include if GLPK is enabled. (#6084) commit | commitdiff | tree
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) commit | commitdiff | tree
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) commit | commitdiff | tree
2021-03-09 Aina NiemetzNew C++ API: Migrate to Node layer. (#6070) commit | commitdiff | tree
2021-03-08 Aina NiemetzRefactor ouroborous API test to not use Expr. (#6079) commit | commitdiff | tree
2021-03-08 Mathias Preinercontrib: Do not use HOST env variable for cross-compila... commit | commitdiff | tree
2021-03-08 Andrew ReynoldsFix handling of negation of Boolean bound variables... commit | commitdiff | tree
2021-03-08 Aina NiemetzBuild 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 ReynoldsSimplify theory preprocessing (#6058) commit | commitdiff | tree
2021-03-08 Gereon KremerFix justification heuristic again (#6074) commit | commitdiff | tree
2021-03-08 Andrew ReynoldsDo not process conjunctions as facts in strings (#6065) commit | commitdiff | tree
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) commit | commitdiff | tree
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) commit | commitdiff | tree
2021-03-05 yoni206Set logic in interpolation unit test. (#6067) commit | commitdiff | tree
2021-03-05 mcjunehoInitial implementation of an optimization solver with... commit | commitdiff | tree
2021-03-05 Aina Niemetzgoogle test: Remove obsolete Expr test fixtures. (... commit | commitdiff | tree
2021-03-05 Gereon KremerReimplement time limit mechanism for windows (#6049) commit | commitdiff | tree
2021-03-05 Aina Niemetzgoogle test: Remove dependency on ExprManager in type_c... commit | commitdiff | tree
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of interal datatype classes... commit | commitdiff | tree
2021-03-04 Aina NiemetzAdd initial bit-blaster for proof logging. (#6053) commit | commitdiff | tree
2021-03-04 Aina NiemetzNew C++ Api: Clean up usage of internal types in Term... commit | commitdiff | tree
2021-03-04 Gereon KremerAdd proper define for libpoly usage (#6050) commit | commitdiff | tree
2021-03-04 Gereon KremerAdd cmake scripts for iwyu targets. (#6042) commit | commitdiff | tree
2021-03-04 Aina NiemetzFix nightlies. (#6052) commit | commitdiff | tree
2021-03-04 Gereon KremerIgnore isInConflict when adding conflicts (#5995) commit | commitdiff | tree
next