cvc5.git
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...
2021-03-22 Andrew Reynolds Function types are always first-class (#6167)
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187)
2021-03-22 Aina NiemetzFP: Add documentation for FloatingPointLiteral construc...
2021-03-22 Andrew ReynoldsGuard for non-unique skolems in term formula removal...
2021-03-21 Andrew ReynoldsSimplify strings term registration (#6174)
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161)
2021-03-20 Andrew ReynoldsImproved tracing for equivalence classes of EE (#6169)
2021-03-20 mudathirmahgoubGenerate cvc/Kind.java for the java API (#6143)
2021-03-19 Andrew ReynoldsRefactor initialization of quantifiers model and builde...
2021-03-19 Aina NiemetzBitVector: Change setBit to set the bit in place. ...
2021-03-19 Aina NiemetzFP: Use setBit instead of bv or in conversion from...
2021-03-18 Haniel BarbosaWhen giving an SMT-LIB version, defaulting to SMT-LIB...
2021-03-18 Gereon KremerMove stats registry to env. (#6173)
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...
next