projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-04-01 Aina NiemetzFP: Factor out symfpu traits. (#6246) commit | commitdiff | tree
2021-04-01 Andrew ReynoldsFix type rule for to_real (#6257) commit | commitdiff | tree
2021-04-01 Andrew ReynoldsAdd regression for issue 6191 (#6264) commit | commitdiff | tree
2021-04-01 Aina NiemetzDelete hashsmt example. (#6263) commit | commitdiff | tree
2021-04-01 Gereon KremerRefactor CLN dependency & Cleanup (#6251) commit | commitdiff | tree
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) commit | commitdiff | tree
2021-04-01 Aina Niemetzkinds: Remove non-existent properties. (#6253) commit | commitdiff | tree
2021-04-01 Andrew Reynolds Add debug traces to theory inference manager (#6250) commit | commitdiff | tree
2021-04-01 Andrew ReynoldsFix non-linear for unknown case (#6252) commit | commitdiff | tree
2021-04-01 Gereon KremerMake ResetCommand go through APISolver (#6172) commit | commitdiff | tree
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) commit | commitdiff | tree
2021-03-31 Gereon KremerRefactor GMP and Poly dependencies (#6245) commit | commitdiff | tree
2021-03-31 Gereon KremerRefactor dependencies for external SAT solvers (#6215) commit | commitdiff | tree
2021-03-31 Gereon KremerRefactor SymFPU dependency (#6218) commit | commitdiff | tree
2021-03-31 Aina NiemetzBags: Move implementation of type rules from header... commit | commitdiff | tree
2021-03-31 Aina NiemetzFix years in COPYING. (#6248) commit | commitdiff | tree
2021-03-31 Andrew ReynoldsEliminate dependencies on quantifiers engine in interna... commit | commitdiff | tree
2021-03-31 Andrew ReynoldsAdd missing inference ids (#6242) commit | commitdiff | tree
2021-03-31 Aina NiemetzFP: Move implementation of type rules from header to... commit | commitdiff | tree
2021-03-31 yoni206Fix compilation of Python bindings for named build... commit | commitdiff | tree
2021-03-30 Andrew ReynoldsFix printing for double patterns (#6235) commit | commitdiff | tree
2021-03-30 Andrew ReynoldsMake SEXPR simply typed (#6160) commit | commitdiff | tree
2021-03-30 Andrew ReynoldsImplement simple tracking of instantiation lemmas ... commit | commitdiff | tree
2021-03-30 Andrew ReynoldsRefactoring quantifier annotation kinds, add kinds... commit | commitdiff | tree
2021-03-30 Andrew ReynoldsEliminate use of rational from tptp parser (#6239) commit | commitdiff | tree
2021-03-30 Abdalrhman... Give a better error when sygus grammar rules contain... commit | commitdiff | tree
2021-03-30 Gereon KremerFix total time statistic (#6233) commit | commitdiff | tree
2021-03-30 Andrew ReynoldsMiscellaneous elimination of dependencies on quantifier... commit | commitdiff | tree
2021-03-29 Gereon KremerAdd external project to install gtest (#6229) commit | commitdiff | tree
2021-03-29 Andrew ReynoldsEliminate the use of quantifiers engine in sygus solver... commit | commitdiff | tree
2021-03-29 Aina NiemetzFix configuration printing. (#6236) commit | commitdiff | tree
2021-03-29 Andrew ReynoldsEliminate use of quantifiers engine in enumerative... commit | commitdiff | tree
2021-03-29 Andrew ReynoldsMove decision manager into theory inference manager... commit | commitdiff | tree
2021-03-29 yoni206Modular bv2int part 1 (#6212) commit | commitdiff | tree
2021-03-29 Aina NiemetzFloatingPointLiteral: Constructor for special consts... commit | commitdiff | tree
2021-03-27 Andrew V. JonesWhen building ANTLR via CMake, do not require javac... commit | commitdiff | tree
2021-03-27 Gereon KremerRefactor ANTLR3 dependency (#6202) commit | commitdiff | tree
2021-03-27 Aina NiemetzUse color output to print configuration. (#6219) commit | commitdiff | tree
2021-03-26 Aina NiemetzFloatingPointLiteral: Make constructors that shouldn... commit | commitdiff | tree
2021-03-26 Andrew ReynoldsPass term registry to quantifiers modules (#6216) commit | commitdiff | tree
2021-03-25 Gereon KremerEnsure nonlinear extensions properly reconsiders its... commit | commitdiff | tree
2021-03-25 Aina NiemetzFP: Refactor FloatingPointLiteral in preparation for... commit | commitdiff | tree
2021-03-25 Andrew ReynoldsRefactor construction of triggers (#6209) commit | commitdiff | tree
2021-03-25 Mathias PreinerDo not use Configuration class in API black tests.... commit | commitdiff | tree
2021-03-25 Gereon KremerAdd missing includes. (#6207) commit | commitdiff | tree
2021-03-25 Haniel BarbosaDeleting old LFSC signatures (#6194) commit | commitdiff | tree
2021-03-24 Andrew ReynoldsUse inference manager to access intantiate utility... commit | commitdiff | tree
2021-03-24 Gereon KremerOnly consider relevant terms for integer branches ... commit | commitdiff | tree
2021-03-24 Gereon KremerRefactor our integration of LFSC (#6201) commit | commitdiff | tree
2021-03-23 Andrew ReynoldsRemove unused code for axioms (#6197) commit | commitdiff | tree
2021-03-23 Haniel BarbosaRemoving unused build options and deprecated proof... commit | commitdiff | tree
2021-03-23 Andrew ReynoldsPassing term registry to ematching utilities (#6190) commit | commitdiff | tree
2021-03-23 Aina NiemetzRemove internal includes of Api header. (#6193) commit | commitdiff | tree
2021-03-23 Abdalrhman... Replace old sygus term reconstruction algorithm with... commit | commitdiff | tree
2021-03-23 Andrew ReynoldsMoving instantiate and skolemize into quantifiers infer... commit | commitdiff | tree
2021-03-22 Gereon KremerMove statistics from the driver into the SmtEngine... commit | commitdiff | tree
2021-03-22 Andrew ReynoldsMove equality query utility into quantifiers model... commit | commitdiff | tree
2021-03-22 Andrew Reynolds Function types are always first-class (#6167) commit | commitdiff | tree
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187) commit | commitdiff | tree
2021-03-22 Aina NiemetzFP: Add documentation for FloatingPointLiteral construc... commit | commitdiff | tree
2021-03-22 Andrew ReynoldsGuard for non-unique skolems in term formula removal... commit | commitdiff | tree
2021-03-21 Andrew ReynoldsSimplify strings term registration (#6174) commit | commitdiff | tree
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161) commit | commitdiff | tree
2021-03-20 Andrew ReynoldsImproved tracing for equivalence classes of EE (#6169) commit | commitdiff | tree
2021-03-20 mudathirmahgoubGenerate cvc/Kind.java for the java API (#6143) commit | commitdiff | tree
2021-03-19 Andrew ReynoldsRefactor initialization of quantifiers model and builde... commit | commitdiff | tree
2021-03-19 Aina NiemetzBitVector: Change setBit to set the bit in place. ... commit | commitdiff | tree
2021-03-19 Aina NiemetzFP: Use setBit instead of bv or in conversion from... commit | commitdiff | tree
2021-03-18 Haniel BarbosaWhen giving an SMT-LIB version, defaulting to SMT-LIB... commit | commitdiff | tree
2021-03-18 Gereon KremerMove stats registry to env. (#6173) commit | commitdiff | tree
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
next