cvc5.git
2021-04-19 Andrew ReynoldsFully incorporate quantifiers macros into ppAssert...
2021-04-19 Gereon KremerRemove linking against gmp and cln in tests and parser...
2021-04-16 Gereon KremerFix dependencies for stats options (#6378)
2021-04-16 Andrew ReynoldsFix ONCE for post-rewrite (#6372)
2021-04-16 Gereon KremerRefactor cmake: auto-download and default-on dependenci...
2021-04-16 Gereon KremerReplace SExpr class by simpler conversion routines...
2021-04-16 Mathias Preinercmake: Build object libraries for base and context...
2021-04-15 Aina Niemetzpreprocessing context: Add wrapper for model substituti...
2021-04-15 Mathias PreinerBuild support library from base and context. (#6368)
2021-04-15 Gereon KremerAvoid options listener for resource manager. (#6366)
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351)
2021-04-15 Gereon KremerFix printing of stats when aborted. (#6362)
2021-04-15 Andrew ReynoldsReenable regression for minimizing instantiations ...
2021-04-14 Andrew ReynoldsFix type rule for relations join image (#6349)
2021-04-14 Gereon KremerImprove documentation for FP rounding mode, add bibliog...
2021-04-14 Gereon KremerImprove documentation of API kinds (#6341)
2021-04-14 Gereon KremerImprove documentation for API exceptions (#6340)
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162)
2021-04-14 Aina NiemetzRename public and private headers in src/include. ...
2021-04-14 Haniel Barbosa[unsat-cores] Improving new unsat cores (#6356)
2021-04-14 Andrew ReynoldsAdd internal API methods for pool-based instantiation...
2021-04-14 Andrew ReynoldsAdd interface for getting relevant assertions (#5131)
2021-04-14 Abdalrhman... Merge equivalent sub-obligations instead of discarding...
2021-04-14 Andrew ReynoldsWarn about infeasible SyGuS conjectures (#6345)
2021-04-14 Haniel Barbosa[proof-new] Fix explanation of literals in SAT proof...
2021-04-14 Haniel Barbosa[proof-new] Miscellaneous improvements to dot printer...
2021-04-14 Gereon KremerFix libpoly build and use new release (#6354)
2021-04-13 Andrew ReynoldsAdd pool instantiation strategy (#6308)
2021-04-13 Andrew ReynoldsRefactor quantifiers macros (#6348)
2021-04-13 Mathias Preinerci: Use CVC5_REGRESSION_ARGS. (#6347)
2021-04-13 Andrew ReynoldsFormalize more skolems (#6307)
2021-04-13 Aina NiemetzAPI docs: Add custom target to build for GH pages....
2021-04-13 Abdalrhman... Avoid using substitute's input cache after the method...
2021-04-13 Abdalrhman... Fix sexpr bug with AST output language. (#6329)
2021-04-13 Aina NiemetzBags: Move more implementation of type rule from header...
2021-04-12 Aina NiemetzStrings: Move implementation of type rules from header...
2021-04-12 Andrew ReynoldsFix computation of whether a type is finite (#6312)
2021-04-12 Gereon KremerRefactor resource manager (#6322)
2021-04-12 Gereon KremerOnly require GMP 6.1 (#6332)
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316)
2021-04-12 Andrew ReynoldsConsolidate interface to prop engine (#6189)
2021-04-12 Andres NoetzliFix GitHub Actions macOS build (#6331)
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327)
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326)
2021-04-09 Aina NiemetzNew C++ Api: Initial layout of Api documentation. ...
2021-04-09 Haniel Barbosa[proof-new] Optimizing sat proof (#6324)
2021-04-09 Andrew ReynoldsAdd identifiers for extended function reductions (...
2021-04-09 Andrew ReynoldsAdd regressions for issue 6214 (#6305)
2021-04-09 Andres NoetzliLearn equalities involving Boolean variables (#6323)
2021-04-09 Andrew ReynoldsAvoid spurious runs in run_regression.py (#6318)
2021-04-09 Andrew ReynoldsUse expr miner timeout (#6321)
2021-04-09 Gereon KremerAdd missing InferenceIds to toString (#6320)
2021-04-08 Andrew ReynoldsFix run_regression for cvc expected outputs (#6317)
2021-04-08 Gereon KremerUse newer version of update-pr-branch action. (#6315)
2021-04-08 Andrew ReynoldsUse exceptions when constructing malformed datatypes...
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311)
2021-04-08 Andrew ReynoldsAdd benchmark for issue 5101 (#6301)
2021-04-08 Andrew ReynoldsAdd benchmark for issue 4400 (#6288)
2021-04-08 Andrew ReynoldsInitial support for parametric datatypes in sygus ...
2021-04-07 Aina NiemetzRemove old API header. (#6309)
2021-04-07 Andrew ReynoldsAdd cardinality class definition (#6302)
2021-04-07 Andrew ReynoldsAdd benchmark for 6270 (#6283)
2021-04-07 Haniel Barbosa[proof-new] Fixing SMT post-processor's handling of...
2021-04-07 Andrew ReynoldsAdd benchmark for issue 4420 (#6286)
2021-04-07 Andrew ReynoldsSet incomplete if not applying ho extensionality (...
2021-04-07 Andrew ReynoldsFixes for abducts (#6279)
2021-04-07 Aina NiemetzNew C++ Api: Rename and move checks.h. (#6306)
2021-04-07 Andrew Reynolds(proof-new) Proper implementation of proof node cloning...
2021-04-07 Andrew ReynoldsAdd term pools utility (#6243)
2021-04-07 Aina NiemetzNew C++ Api: Initial setup of Api documentation. (...
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag...
2021-04-07 Mathias Preinercmake: Do not always regenerate cvc4kinds.{pxi,pxd...
2021-04-06 Mathias Preinercmake: Add helper to check if a given Python module...
2021-04-06 Andrew ReynoldsAdd benchmark for issue 5942 (#6296)
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290)
2021-04-06 Andrew ReynoldsFix tptp parser for negative rational (#6297)
2021-04-06 Andrew ReynoldsFix issue with lemma during equality engine iterator...
2021-04-06 Mathias Preinergenkinds: Do not use relative paths to find src directo...
2021-04-06 Andrew ReynoldsRemove stdPrintAscii option (#6280)
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292)
2021-04-06 Mathias Preinerparsekinds: Remove DEFAULT_HEADER. (#6294)
2021-04-05 mudathirmahgoubAdd documentation for theory_bags_type_rules.h (#6268)
2021-04-05 Andrew ReynoldsFix spurious antecedant for symbolic regular expression...
2021-04-05 Andrew ReynoldsAdd benchmark for issue 4412 (#6287)
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from...
2021-04-05 Andrew ReynoldsEnable UF when pre-skolem nested option is enabled...
2021-04-05 NicolaasWeidemanpython: Fix type casting in mkBitVector (#6261)
2021-04-05 Andrew ReynoldsFix subtyping for sets care graph (#6278)
2021-04-05 Andrew ReynoldsAdd interface for skolem functions in SkolemManager...
2021-04-05 yoni206A proposal for python api unit tests (#6255)
2021-04-05 Yancheng OuOptimizer for BitVectors (#6213)
2021-04-03 Andrew ReynoldsDisable substring component contains in strip endpoints...
2021-04-02 Gereon KremerAdd cache for new dependencies folder. (#6265)
2021-04-02 Mathias Preinercmake: Do not link against main object library. (#6269)
2021-04-02 Gereon KremerNew statistics registry (#6210)
2021-04-02 Gereon KremerMinor refactoring (#6273)
2021-04-02 Andrew ReynoldsCleaning up friend relationships for commands (#6254)
2021-04-02 Andrew ReynoldsFix case where RE unfolding generates a trivially true...
2021-04-02 Gereon KremerFindCaDiCaL: Avoid redirect to file (#6272)
2021-04-01 Gereon KremerAdd utility classes for new statistics (#6178)
next