projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-05-23 Andrew ReynoldsMake model core robust to when we cannot show the model... commit | commitdiff | tree
2022-05-22 Mathias Preinerbv: Add resource limits support for CaDiCaL. (#8788) commit | commitdiff | tree
2022-05-22 Andrew ReynoldsSimplification of smt2 printer for type ascriptions... commit | commitdiff | tree
2022-05-21 Andrew ReynoldsMove smt_util to preprocessing/util (#8799) commit | commitdiff | tree
2022-05-21 Andrew ReynoldsReenable assertion in skolem definition manager (#8797) commit | commitdiff | tree
2022-05-21 Andrew ReynoldsAdd option to send all instantiations in a bounded... commit | commitdiff | tree
2022-05-21 Gereon KremerAdd cross-compilation for arm64 on macOS (#8758) commit | commitdiff | tree
2022-05-20 Andrew ReynoldsMore removing of unused code (#8806) commit | commitdiff | tree
2022-05-20 vinciusbTrying to break cycles when printing a .dot DAG (#8698) commit | commitdiff | tree
2022-05-20 vinciusbNew way to identify THEORY_LEMMA clusters when printing... commit | commitdiff | tree
2022-05-19 Andrew ReynoldsMinor deleting of unused code (#8800) commit | commitdiff | tree
2022-05-19 Andrew ReynoldsAdd options and regressions to increase coverage (... commit | commitdiff | tree
2022-05-18 Andrew ReynoldsBasic cleanup of sep theory (#8790) commit | commitdiff | tree
2022-05-18 Andrew ReynoldsMake skolem definition manager robust to definitions... commit | commitdiff | tree
2022-05-18 Andrew ReynoldsEliminate subtypes (#8783) commit | commitdiff | tree
2022-05-17 Andrew ReynoldsRefactor declare oracle command (#8742) commit | commitdiff | tree
2022-05-17 Andrew ReynoldsMinor cleanup of datatypes theory (#8791) commit | commitdiff | tree
2022-05-17 Andrew ReynoldsFix LFSC proof construction for concat clash of sequenc... commit | commitdiff | tree
2022-05-17 Mathias Preinerdocs: Remove references to checkEntailed(). (#8789) commit | commitdiff | tree
2022-05-17 Andrew ReynoldsGeneralize pto constraint tracking for multiple heaps... commit | commitdiff | tree
2022-05-17 Ying ShengAdd getInterpolant with a grammar in the unit test... commit | commitdiff | tree
2022-05-17 yoni206new test for resolved issue (#8784) commit | commitdiff | tree
2022-05-16 Andrew ReynoldsLast remaining fixes for eliminating subtyping (#8772) commit | commitdiff | tree
2022-05-16 Haniel Barbosa[proofs] Generalize handling of constants merged in... commit | commitdiff | tree
2022-05-16 Haniel BarbosaRename equality engine trace to print E-graph (#8780) commit | commitdiff | tree
2022-05-15 Andrew ReynoldsEliminate the use of CAST_TO_REAL (#8759) commit | commitdiff | tree
2022-05-15 Andrew ReynoldsEliminate ops for parameterized type constructors ... commit | commitdiff | tree
2022-05-13 Andrew ReynoldsMake arith substitute its own utility (#8765) commit | commitdiff | tree
2022-05-13 Amalee WilsonAdd heap-trail partitioning strategy, checks between... commit | commitdiff | tree
2022-05-13 Andrew ReynoldsFixes and improvement for IAND solver (#8771) commit | commitdiff | tree
2022-05-13 Andrew ReynoldsEliminate use of getBaseType (#8764) commit | commitdiff | tree
2022-05-13 Andrew ReynoldsAdd utilities in preparation for supporting str.nth... commit | commitdiff | tree
2022-05-13 Andrew ReynoldsFix debug failures in LFSC proofs due to curried arithm... commit | commitdiff | tree
2022-05-13 Andrew ReynoldsRefactor logic exceptions during preregistration for... commit | commitdiff | tree
2022-05-13 Gereon KremerUpdate CoCoALib version (#8757) commit | commitdiff | tree
2022-05-13 Andrew ReynoldsMinor refactoring for sep theory (#8753) commit | commitdiff | tree
2022-05-12 Andrew ReynoldsFix type of null terminator for ADD/MULT for LFSC ... commit | commitdiff | tree
2022-05-12 Andrew ReynoldsEliminate use of subtypes from remainder of type rules... commit | commitdiff | tree
2022-05-12 Andrew ReynoldsPreserve types in rewriter and make core type rules... commit | commitdiff | tree
2022-05-12 Haniel Barbosa[docs] Marking internal comment in proofs docs (#8747) commit | commitdiff | tree
2022-05-12 Gereon KremerMake regular options access const (#8754) commit | commitdiff | tree
2022-05-11 Gereon KremerRemove --build from GMP configure line (#8752) commit | commitdiff | tree
2022-05-11 Andrew ReynoldsRelax an assertion in the evaluator (#8751) commit | commitdiff | tree
2022-05-10 Gereon KremerEnsure substitutions in nonlinear solver are properly... commit | commitdiff | tree
2022-05-10 Gereon KremerFix some issues with the Python API tests (#8746) commit | commitdiff | tree
2022-05-10 Gereon KremerAdd test coverage for almost everything from the Java... commit | commitdiff | tree
2022-05-10 Gereon KremerCompress debug symbols to make libcvc5 smaller (#8743) commit | commitdiff | tree
2022-05-09 Andrew ReynoldsImprovements for evaluation in model (#8738) commit | commitdiff | tree
2022-05-09 Andrew ReynoldsDo not depend on subtyping for APPLY_UF in TPTP parser... commit | commitdiff | tree
2022-05-09 Andrew ReynoldsAdd unit tests for getInstantiations (#8741) commit | commitdiff | tree
2022-05-07 Andrew ReynoldsDo not rely on subtyping in real-to-int preprocessing... commit | commitdiff | tree
2022-05-07 Abdalrhman... Disable proof testers for delicate regressions. (#8735) commit | commitdiff | tree
2022-05-07 Andrew ReynoldsMore preparation for strict type rules (#8733) commit | commitdiff | tree
2022-05-07 Andrew ReynoldsFix proofs for ppAssert for theory Bool (#8708) commit | commitdiff | tree
2022-05-06 Andrew ReynoldsFallback for sequential substitution proof reconstructi... commit | commitdiff | tree
2022-05-06 Andrew ReynoldsEliminate arithmetic subtyping for (dis)equalities... commit | commitdiff | tree
2022-05-06 Andrew ReynoldsSeparate ill-typed portion of arith models (#8734) commit | commitdiff | tree
2022-05-06 Andrew ReynoldsFix LFSC side condition for matching premise of concat_... commit | commitdiff | tree
2022-05-05 Gereon KremerAdd test coverage for almost everything from the Python... commit | commitdiff | tree
2022-05-05 Andrew ReynoldsPreparation for making equality strictly typed (#8728) commit | commitdiff | tree
2022-05-05 Andrew ReynoldsFix cache in learned rewrite preprocessing pass (#8725) commit | commitdiff | tree
2022-05-05 Andrew ReynoldsFix more issues with subtypes in regressions (#8727) commit | commitdiff | tree
2022-05-05 mudathirmahgoubAdd operators table.aggr and table.join (#8681) commit | commitdiff | tree
2022-05-05 Andrew ReynoldsUse purification for set comprehension reduction (... commit | commitdiff | tree
2022-05-04 Andres NoetzliImprove finding Python library/includes (#8718) commit | commitdiff | tree
2022-05-04 yoni206fix link to `Testing cvc5` in `INSTALL.md` (#8675) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsMake equality solver the entry point for all equality... commit | commitdiff | tree
2022-05-04 Gereon KremerMake printStatisticsSafe public (#8721) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsAdd declareOracleFun interface to SolverEngine (#8622) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsRefactor oracles using new std::function backend (... commit | commitdiff | tree
2022-05-04 Andrew ReynoldsRemove unecessary calls to equality engine from congrue... commit | commitdiff | tree
2022-05-04 Gereon KremerRemove obsolete private methods from API (#8716) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsFix rewrite for to_real in division by zero (#8714) commit | commitdiff | tree
2022-05-04 Andrew ReynoldsAdd support for oracle constant nodes (#8707) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsFix LFSC node converter for 0-ary tuples (#8706) commit | commitdiff | tree
2022-05-03 Andres NoetzliUpdate LFSC version (#8713) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsUse (non-recursive) unpurified form instead of original... commit | commitdiff | tree
2022-05-03 Aina Niemetzdocs: Some fixes in options docs. (#8710) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsChange option name for mbqi in fmf (#8701) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsSimplify representation of datatypes at the TypeNode... commit | commitdiff | tree
2022-05-03 Andrew ReynoldsFinal preparation for CONST_INTEGER (#8700) commit | commitdiff | tree
2022-05-03 Andrew ReynoldsMigrate basic EqualityEngine management from Congruence... commit | commitdiff | tree
2022-05-02 Amalee WilsonAdd strict-cube and decision-trail partitioning strateg... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsMore robust treatment of flattening in arith rewriter... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsMake arith msum utility agnostic to Int (#8694) commit | commitdiff | tree
2022-05-02 Gereon KremerAdd missing tests for some corners of the API (#8688) commit | commitdiff | tree
2022-05-02 Aina Niemetzdocs: Do not use explicit line numbers in literalinclud... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsFurther refactoring in preparation for CONST_INTEGER... commit | commitdiff | tree
2022-05-02 Andrew ReynoldsFix tuple printing in LFSC (#8696) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsProperly represent Tuples in the TypeNode AST (#8648) commit | commitdiff | tree
2022-04-29 Andres NoetzliAdd simple type rule for real-or-int arguments (#8685) commit | commitdiff | tree
2022-04-29 Gereon KremerReplace mkConst(CONST_RATIONAL) by mkConstReal (#8686) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsTowards proper usage of TO_REAL (#8680) commit | commitdiff | tree
2022-04-29 Andres NoetzliDocument non-standard string operators (#8679) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsEnsure mkConstInt is used on integral rationals only... commit | commitdiff | tree
2022-04-29 Andrew ReynoldsRefactor interfaces for E-matching (#8665) commit | commitdiff | tree
2022-04-29 Andrew ReynoldsMake extended rewriter use standard Subs utility (... commit | commitdiff | tree
2022-04-29 Abdalrhman... Add an option to enable all testers. (#8676) commit | commitdiff | tree
2022-04-29 yoni206Add missing parenthesis for bags documentation (#8673) commit | commitdiff | tree
2022-04-29 Gereon KremerAdd unit test for code not exposed by java API (#8678) commit | commitdiff | tree
next