summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-03-11First refactoring of statistics classes (#6105)Gereon Kremer
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-11Improvements and refactoring for enumeratative strategy (#6030)MikolasJanota
2021-03-11(proof-new) Clean up uses of witness with skolem lemmas (#6109)Andrew Reynolds
2021-03-11Direct lemmas and inference ids for sygus extension (#5960)Andrew Reynolds
2021-03-11Fix compile warnings when compiling with GLPK. (#6115)Mathias Preiner
2021-03-11Remove obsolete test/api/statistics.cpp. (#6116)Aina Niemetz
2021-03-11Clean up ownership of Datatypes in NodeManager. (#6113)Aina Niemetz
2021-03-11Refactor Node::getOperator() to fix compiler warning. (#6110)Aina Niemetz
2021-03-11Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)Mathias Preiner
2021-03-10Add GitHub action to automatically update approved PRs. (#6114)Mathias Preiner
2021-03-10Use Assert instead of assert. (#6095)Mathias Preiner
2021-03-10New C++ Api: Add missing argument checks in Solver functions. (#6094)Aina Niemetz
2021-03-10Add Env class (#6093)Andrew Reynolds
2021-03-10Improved handing of 'lib64' vs. 'lib' for glpk-cut-log and antlr-3.4 (#6091)Andrew V. Jones
2021-03-10[proof-new] Clarifying doc (#6108)Haniel Barbosa
2021-03-10Move ExprManager::isNAryKind to NodeManager. (#6107)Aina Niemetz
2021-03-10Improve arithmetic proofs (#6106)Gereon Kremer
2021-03-10cmake: Fix optimization level for debug builds. (#6097)Mathias Preiner
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
2021-03-10Fix extended equality rewrite involving replace. (#6104)Andrew Reynolds
2021-03-10Fix term registration and non-theory-preprocessed terms in substitutions (#6080)Andrew Reynolds
2021-03-10Add quant elim regression (#6103)Andrew Reynolds
2021-03-10(proof-new) Replace witness form by original form in the internal proof calcu...Andrew Reynolds
2021-03-10test: Fix missing std::. (#6096)Mathias Preiner
2021-03-09New C++ Api: Use const ref for arguments when possible. (#6092)Aina Niemetz
2021-03-09Merge initialization steps in TheoryModelBuilder (#4901)Andrew Reynolds
2021-03-09Remove logic request (#6089)Andrew Reynolds
2021-03-09New C++ Api: Migrate stats collection for consts, vars, terms. (#6090)Aina Niemetz
2021-03-09ContextObj::destroy(): Guard against invalid use. (#6082)Aina Niemetz
2021-03-09New C++ Api: Clean up usage of internal kind. (#6087)Aina Niemetz
2021-03-09(proof-new) Minor fix and allow proof option (#6085)Andrew Reynolds
2021-03-09New C++ API: Reorder and clean up cpp file. (#6086)Aina Niemetz
2021-03-09Add missing include if GLPK is enabled. (#6084)Gereon Kremer
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08New C++ API: Migrate to Node layer. (#6070)Aina Niemetz
2021-03-08Refactor ouroborous API test to not use Expr. (#6079)Aina Niemetz
2021-03-08contrib: Do not use HOST env variable for cross-compilation host target. (#6078)Mathias Preiner
2021-03-08Fix handling of negation of Boolean bound variables in FMF (#6066)Andrew Reynolds
2021-03-08Build api tests in build/bin/test/api. (#6076)Aina Niemetz
2021-03-08(proof-new) Separating optimizations for strings skolem caching (#6064)Andrew Reynolds
2021-03-08(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)Andrew Reynolds
2021-03-08Simplify theory preprocessing (#6058)Andrew Reynolds
2021-03-08Fix justification heuristic again (#6074)Gereon Kremer
2021-03-08Do not process conjunctions as facts in strings (#6065)Andrew Reynolds
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-03-05Set logic in interpolation unit test. (#6067)yoni206
2021-03-05Initial implementation of an optimization solver with unit tests. (#5849)mcjuneho
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback