cvc5.git
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)
2021-04-01 Andrew ReynoldsSimplify caching of regular expression unfolding (...
2021-04-01 Aina NiemetzFP: Factor out symfpu traits. (#6246)
2021-04-01 Andrew ReynoldsFix type rule for to_real (#6257)
2021-04-01 Andrew ReynoldsAdd regression for issue 6191 (#6264)
2021-04-01 Aina NiemetzDelete hashsmt example. (#6263)
2021-04-01 Gereon KremerRefactor CLN dependency & Cleanup (#6251)
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258)
2021-04-01 Aina Niemetzkinds: Remove non-existent properties. (#6253)
2021-04-01 Andrew Reynolds Add debug traces to theory inference manager (#6250)
2021-04-01 Andrew ReynoldsFix non-linear for unknown case (#6252)
2021-04-01 Gereon KremerMake ResetCommand go through APISolver (#6172)
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249)
2021-03-31 Gereon KremerRefactor GMP and Poly dependencies (#6245)
2021-03-31 Gereon KremerRefactor dependencies for external SAT solvers (#6215)
2021-03-31 Gereon KremerRefactor SymFPU dependency (#6218)
2021-03-31 Aina NiemetzBags: Move implementation of type rules from header...
2021-03-31 Aina NiemetzFix years in COPYING. (#6248)
2021-03-31 Andrew ReynoldsEliminate dependencies on quantifiers engine in interna...
2021-03-31 Andrew ReynoldsAdd missing inference ids (#6242)
2021-03-31 Aina NiemetzFP: Move implementation of type rules from header to...
2021-03-31 yoni206Fix compilation of Python bindings for named build...
2021-03-30 Andrew ReynoldsFix printing for double patterns (#6235)
2021-03-30 Andrew ReynoldsMake SEXPR simply typed (#6160)
2021-03-30 Andrew ReynoldsImplement simple tracking of instantiation lemmas ...
2021-03-30 Andrew ReynoldsRefactoring quantifier annotation kinds, add kinds...
2021-03-30 Andrew ReynoldsEliminate use of rational from tptp parser (#6239)
2021-03-30 Abdalrhman... Give a better error when sygus grammar rules contain...
2021-03-30 Gereon KremerFix total time statistic (#6233)
2021-03-30 Andrew ReynoldsMiscellaneous elimination of dependencies on quantifier...
2021-03-29 Gereon KremerAdd external project to install gtest (#6229)
2021-03-29 Andrew ReynoldsEliminate the use of quantifiers engine in sygus solver...
2021-03-29 Aina NiemetzFix configuration printing. (#6236)
2021-03-29 Andrew ReynoldsEliminate use of quantifiers engine in enumerative...
2021-03-29 Andrew ReynoldsMove decision manager into theory inference manager...
2021-03-29 yoni206Modular bv2int part 1 (#6212)
2021-03-29 Aina NiemetzFloatingPointLiteral: Constructor for special consts...
2021-03-27 Andrew V. JonesWhen building ANTLR via CMake, do not require javac...
2021-03-27 Gereon KremerRefactor ANTLR3 dependency (#6202)
2021-03-27 Aina NiemetzUse color output to print configuration. (#6219)
2021-03-26 Aina NiemetzFloatingPointLiteral: Make constructors that shouldn...
2021-03-26 Andrew ReynoldsPass term registry to quantifiers modules (#6216)
2021-03-25 Gereon KremerEnsure nonlinear extensions properly reconsiders its...
2021-03-25 Aina NiemetzFP: Refactor FloatingPointLiteral in preparation for...
2021-03-25 Andrew ReynoldsRefactor construction of triggers (#6209)
2021-03-25 Mathias PreinerDo not use Configuration class in API black tests....
2021-03-25 Gereon KremerAdd missing includes. (#6207)
2021-03-25 Haniel BarbosaDeleting old LFSC signatures (#6194)
2021-03-24 Andrew ReynoldsUse inference manager to access intantiate utility...
2021-03-24 Gereon KremerOnly consider relevant terms for integer branches ...
2021-03-24 Gereon KremerRefactor our integration of LFSC (#6201)
2021-03-23 Andrew ReynoldsRemove unused code for axioms (#6197)
2021-03-23 Haniel BarbosaRemoving unused build options and deprecated proof...
2021-03-23 Andrew ReynoldsPassing term registry to ematching utilities (#6190)
2021-03-23 Aina NiemetzRemove internal includes of Api header. (#6193)
2021-03-23 Abdalrhman... Replace old sygus term reconstruction algorithm with...
2021-03-23 Andrew ReynoldsMoving instantiate and skolemize into quantifiers infer...
2021-03-22 Gereon KremerMove statistics from the driver into the SmtEngine...
2021-03-22 Andrew ReynoldsMove equality query utility into quantifiers model...
next