{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":7040894,"defaultBranch":"main","name":"cvc5","ownerLogin":"cvc5","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2012-12-06T18:45:04.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/81640843?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1716746331.0","currentOid":""},"activityList":{"items":[{"before":"2c5e476aa34fafb5bcc2797872da5f9c6753fc9d","after":"6129cff8fbac545847a939b2bb31508d564e26aa","ref":"refs/heads/main","pushedAt":"2024-06-07T23:13:51.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Fix C++ api coverage for plugins (#10859)","shortMessageHtmlLink":"Fix C++ api coverage for plugins (#10859)"}},{"before":"a705e4de90635b0f0d21005f63e778cdb924c6b8","after":"a21d22b43061fef6841dedb7a3ac899ca1de4be7","ref":"refs/heads/proof-new","pushedAt":"2024-06-07T13:26:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"[alethe] printing of real constants with gmp notation","shortMessageHtmlLink":"[alethe] printing of real constants with gmp notation"}},{"before":"a640d391ae46ae3e93534e60126beb77b8d90b6e","after":"2c5e476aa34fafb5bcc2797872da5f9c6753fc9d","ref":"refs/heads/main","pushedAt":"2024-06-06T23:18:28.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"aniemetz","name":"Aina Niemetz","path":"/aniemetz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29313325?s=80&v=4"},"commit":{"message":"Expose API for hashing proofs. (#10391)\n\nThis PR exposes hashing and equality of proofs in the API to avoid\r\nreconstructing the same proof step multiple times from the Lean side.\r\n\r\nNotes:\r\n- Proof equality in this PR is referential, not syntactical. However,\r\nthis is still useful for caching (and better than nothing).\r\n- A default constructor, `Proof()`, is added to the Java API to mirror\r\nthe C++ and Python APIs and the `Term()` constructor in the Java API.","shortMessageHtmlLink":"Expose API for hashing proofs. (#10391)"}},{"before":"62aa67e353b3c510546c297d022531bc56230a65","after":"a640d391ae46ae3e93534e60126beb77b8d90b6e","ref":"refs/heads/main","pushedAt":"2024-06-06T14:37:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"Adding UF examples (#10824)\n\nWe don't have simple UF examples. This PR adds such an example in\r\nsmt-lib and all the APIs.","shortMessageHtmlLink":"Adding UF examples (#10824)"}},{"before":"142680488dbd1177d0146ff13acaddd71fbe8403","after":"62aa67e353b3c510546c297d022531bc56230a65","ref":"refs/heads/main","pushedAt":"2024-06-05T23:09:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Fix case where substitution fails to elaborate (#10845)\n\nThis eliminates the 1 occurrence of SUBS_NO_ELABORATE from our regressions.\r\n\r\nThis should fix all further cases where substitutions fail to be elaborated.","shortMessageHtmlLink":"Fix case where substitution fails to elaborate (#10845)"}},{"before":"858d23c7ac87b1e054c9304ffef77abebff96543","after":"142680488dbd1177d0146ff13acaddd71fbe8403","ref":"refs/heads/main","pushedAt":"2024-06-05T21:38:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Add mode for if and when to try THEORY_REWRITE in RARE proof reconstruction (#10826)\n\nThis change is required to avoid circular dependencies if a THEORY_REWRITE can be used to justify its own subgoals.\r\n\r\nWith this change, we disable use of THEORY_REWRITE in the RARE reconstruction when elaborating the subgoals of theory rewrites, specifically those marked with id MACRO_THEORY_REWRITE_RCONS_SIMPLE.\r\n\r\nIt also simplifies the interface by removing deprecated debugging info.","shortMessageHtmlLink":"Add mode for if and when to try THEORY_REWRITE in RARE proof reconstr…"}},{"before":"fa90865f20aac935083620775878006a00573702","after":"858d23c7ac87b1e054c9304ffef77abebff96543","ref":"refs/heads/main","pushedAt":"2024-06-05T20:07:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Eliminate witness from BV invertibility instantiations (#10848)\n\nThis makes an explicit pass to eliminate WITNESS terms from instantiations in the instantiation strategy from Niemetz et al CAV 2018.\r\n\r\nThe motivation is two-fold:\r\n(1) It is work towards eliminating an incorrect dependency on proofs from SkolemManager. Proofs are local to solving instances, while SkolemManager has a lifetime that is equivalent to its containing NodeManager.\r\n(2) It will make proofs easier to track from the BV instantiator later, as they now can be given on individual lemmas instead of relying on a central utility.\r\n\r\nA followup PR will eliminate support for WITNESS in skolem manager and the term formula removal pass.","shortMessageHtmlLink":"Eliminate witness from BV invertibility instantiations (#10848)"}},{"before":"409b61d2ada2dbb85abd0f65f7e4ca6420f32306","after":"a705e4de90635b0f0d21005f63e778cdb924c6b8","ref":"refs/heads/proof-new","pushedAt":"2024-06-05T18:33:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"update carcara version","shortMessageHtmlLink":"update carcara version"}},{"before":"442e6cb23c4867a307ac451a1174b0153cdd3f2d","after":"409b61d2ada2dbb85abd0f65f7e4ca6420f32306","ref":"refs/heads/proof-new","pushedAt":"2024-06-05T18:27:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"update carcara version","shortMessageHtmlLink":"update carcara version"}},{"before":"5a989da99809141eca27b145981de8c7ceed2baa","after":"fa90865f20aac935083620775878006a00573702","ref":"refs/heads/main","pushedAt":"2024-06-05T16:17:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Make sets theory solver proof producing (#10751)\n\nAdds proofs for theory lemmas from sets for the main theory inference ids (upwards/downwards closure, extensionality, singleton injectivity).\r\n\r\nOther more specific inferences will be added in followup PRs as needed.","shortMessageHtmlLink":"Make sets theory solver proof producing (#10751)"}},{"before":"aa749226911f8656ee7d878508349bf55990d324","after":"5a989da99809141eca27b145981de8c7ceed2baa","ref":"refs/heads/main","pushedAt":"2024-06-05T15:29:15.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"aniemetz","name":"Aina Niemetz","path":"/aniemetz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29313325?s=80&v=4"},"commit":{"message":"Another unit test for plugins (#10739)\n\nFixes some of the C++ coverage failures in nightlies.","shortMessageHtmlLink":"Another unit test for plugins (#10739)"}},{"before":"94b6eb7290ef4f785dc8ad50c35547f63724e502","after":"aa749226911f8656ee7d878508349bf55990d324","ref":"refs/heads/main","pushedAt":"2024-06-05T14:11:36.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Add RARE rule for bv2nat inequality elimination (#10849)\n\nTowards eliminating the diversity of trusted steps from our regressions.\r\n\r\nThis is required to fill the remaining 5 PP_STATIC_REWRITE proof holes from our regressions.\r\n\r\nAlso updates the ALF signature as we now have a symbolic term in an index position in int2bv.","shortMessageHtmlLink":"Add RARE rule for bv2nat inequality elimination (#10849)"}},{"before":"48d3546ed6083d9318ab80ec249ac2d2fdbb98bc","after":"94b6eb7290ef4f785dc8ad50c35547f63724e502","ref":"refs/heads/main","pushedAt":"2024-06-04T22:40:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"aniemetz","name":"Aina Niemetz","path":"/aniemetz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29313325?s=80&v=4"},"commit":{"message":"Move slow regression to regress3 (#10851)\n\nFixes a timeout on the nightlies, this benchmark has been slow (7\r\nseconds on production) and is timing out on our model tester in a build\r\non the nightlies.","shortMessageHtmlLink":"Move slow regression to regress3 (#10851)"}},{"before":"f6748e08d96b797826e13556f88b67ed1752e5ea","after":"48d3546ed6083d9318ab80ec249ac2d2fdbb98bc","ref":"refs/heads/main","pushedAt":"2024-06-04T22:01:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Test DSL proofs with ALF by default (#10840)","shortMessageHtmlLink":"Test DSL proofs with ALF by default (#10840)"}},{"before":"b8d6875b5b7a10c09cb093de49663f3a6f641de0","after":"f6748e08d96b797826e13556f88b67ed1752e5ea","ref":"refs/heads/main","pushedAt":"2024-06-04T21:27:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Update syntax for list operators in ALF (#10853)\n\nThis updates the syntax of list operators in ALF to one that has no ambiguity in terms of arity, using the updated operator names.","shortMessageHtmlLink":"Update syntax for list operators in ALF (#10853)"}},{"before":"1c32dca437dfd8ab1692453d9674edd49673fb76","after":"442e6cb23c4867a307ac451a1174b0153cdd3f2d","ref":"refs/heads/proof-new","pushedAt":"2024-06-04T19:07:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"[alethe] cleaning printer","shortMessageHtmlLink":"[alethe] cleaning printer"}},{"before":"d4f3860dd446b97514b64a59f1aeaa856dd7c3f8","after":"b8d6875b5b7a10c09cb093de49663f3a6f641de0","ref":"refs/heads/main","pushedAt":"2024-06-04T18:47:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"c api: Add sort functions and tests. (#10787)","shortMessageHtmlLink":"c api: Add sort functions and tests. (#10787)"}},{"before":"e72822c9d7aaeb545bb0753b3e3523b18dab0515","after":"1c32dca437dfd8ab1692453d9674edd49673fb76","ref":"refs/heads/proof-new","pushedAt":"2024-06-04T16:55:09.000Z","pushType":"push","commitsCount":80,"pusher":{"login":"HanielB","name":"Haniel Barbosa","path":"/HanielB","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2821688?s=80&v=4"},"commit":{"message":"fixes","shortMessageHtmlLink":"fixes"}},{"before":"c91bea9fb0b50a3ebfe7355c1c3e4edeac5432a4","after":"d4f3860dd446b97514b64a59f1aeaa856dd7c3f8","ref":"refs/heads/main","pushedAt":"2024-06-04T16:43:03.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"aniemetz","name":"Aina Niemetz","path":"/aniemetz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/29313325?s=80&v=4"},"commit":{"message":"Improve error message when 'patch' command is missing (#10760)\n\nPreviously, if the 'patch' command was absent from the system when using\r\nCoCoA, the configuration phase proceeded without issues. However, upon\r\nrunning 'make' to build the system, the following error message was\r\nencountered:\r\n\r\n```\r\n[ 7%] No update step for 'CoCoA-EP'\r\n[ 7%] Performing patch step for 'CoCoA-EP'\r\nCMake Error at /home/alan/cvc5/build/deps/src/CoCoA-EP-stamp/CoCoA-EP-patch-Production.cmake:37 (message):\r\n Command failed: No such file or directory\r\n\r\n 'patch' '-p1' '-d' '/home/alan/cvc5/build/deps/src/CoCoA-EP' '-i' '/home/alan/cvc5/cmake/deps-utils/CoCoALib-0.9980\r\n\r\n\r\n\r\n0-trace.patch'\r\n\r\n See also\r\n\r\n /home/alan/cvc5/build/deps/src/CoCoA-EP-stamp/CoCoA-EP-patch.log\r\n\r\n\r\n-- Log output is:\r\n\r\nCMake Error at /home/alan/cvc5/build/deps/src/CoCoA-EP-stamp/CoCoA-EP-patch-Production.cmake:47 (message):\r\n Stopping after outputting logs.\r\n\r\n\r\nmake[2]: *** [CMakeFiles/CoCoA-EP.dir/build.make:122: deps/src/CoCoA-EP-stamp/CoCoA-EP-patch] Error 1\r\nmake[1]: *** [CMakeFiles/Makefile2:620: CMakeFiles/CoCoA-EP.dir/all] Error 2\r\nmake[1]: *** Waiting for unfinished jobs....\r\n```\r\n\r\nIn addition to lacking clarity regarding the underlying issue, the\r\nmessage is somewhat misleading because the file 'CoCoA-EP-patch.log' is\r\nempty. This PR addresses these issues by checking the presence of the\r\n'patch' command in the user's system during the configuration phase of\r\nCVC5 (naturally, this occurs only if the '--cocoa' option is set and\r\n'CoCoA' isn't already installed).\r\n\r\nThese changes do not affect users that are configuring CVC5 without the\r\n'--cocoa' flag, regardless of having the 'patch' package installed on\r\ntheir system.\r\n\r\nThe improved error message provided is:\r\n\r\n```\r\n-- Could NOT find Patch (missing: Patch_EXECUTABLE) \r\nCMake Error at cmake/FindCoCoA.cmake:58 (MESSAGE):\r\n The command `patch` required for installing CoCoA was not found.\r\n\r\n Please install it using one of the following commands:\r\n\r\n - On Debian/Ubuntu: sudo apt install patch\r\n - On Fedora/Red Hat: sudo dnf install patch\r\n - For other OS's, refer to system-specific resources for guidance on installing `patch`.\r\n\r\nCall Stack (most recent call first):\r\n CMakeLists.txt:541 (find_package)\r\n\r\n\r\n-- Configuring incomplete, errors occurred!\r\n```\r\n\r\nSigned-off-by: Alan Prado ","shortMessageHtmlLink":"Improve error message when 'patch' command is missing (#10760)"}},{"before":"a0ac967b2d6890fa418cfac0844f44e369f4ee72","after":"c91bea9fb0b50a3ebfe7355c1c3e4edeac5432a4","ref":"refs/heads/main","pushedAt":"2024-06-04T16:04:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Specify Threads as a dependency explicitly (#10790)\n\nBuilding cvc5 with CryptoMiniSat generates a dependency on the thread library. The config file cvc5Targets.cmake automatically generated by CMake didn't reflect this because the dependency was not explicitly specified. It was relying on passing the -pthread compiler and linker flag. This PR explicitly adds Threads as a dependency.","shortMessageHtmlLink":"Specify Threads as a dependency explicitly (#10790)"}},{"before":"0297d3fbd09a107aa52cd8877af32113582df3c7","after":"a0ac967b2d6890fa418cfac0844f44e369f4ee72","ref":"refs/heads/main","pushedAt":"2024-06-04T14:12:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Add support for sets is-empty theory rewrite in ALF (#10842)","shortMessageHtmlLink":"Add support for sets is-empty theory rewrite in ALF (#10842)"}},{"before":"f072fede9cf36418caf9b4145b936c6aae4f2fce","after":"0297d3fbd09a107aa52cd8877af32113582df3c7","ref":"refs/heads/main","pushedAt":"2024-06-04T12:02:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Do not multiply by one in MACRO_ARITH_SUM_UB (#10846)\n\nThis modifies the MACRO_ARITH_SUM_UB to sum (lhs,rhs) instead of ((* 1 lhs), (* 1 rhs)) when multiplying a relation by 1.\r\n\r\nThis reductions our overall average proof size by about 1.7%, on regressions:","shortMessageHtmlLink":"Do not multiply by one in MACRO_ARITH_SUM_UB (#10846)"}},{"before":"d2295e513514b632aac4e5ad8a12c52030ee9f7f","after":"f072fede9cf36418caf9b4145b936c6aae4f2fce","ref":"refs/heads/main","pushedAt":"2024-06-04T11:41:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Change variable comparison order in ALF signature (#10843)\n\nThis change leads to significantly better proof checking times, as most instances of ACI_NORM will leave terms close to unchanged.\r\n\r\nPreviously, we were doing worse-case performance where terms would mostly always be reversed.\r\n\r\nAlso removes a mistakenly duplicated side condition.","shortMessageHtmlLink":"Change variable comparison order in ALF signature (#10843)"}},{"before":"bd8437a04920b8764eca86c61885d5e3538b9479","after":"d2295e513514b632aac4e5ad8a12c52030ee9f7f","ref":"refs/heads/main","pushedAt":"2024-06-04T02:04:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Implement new simple proof rewrite rules for strings (#10830)\n\nAdds the implementation required for elaborating proofs into the rewrites introduced here: 0e3316f\r\n\r\nThis currently fixes a timeout in the nightlies related to proof elaboration, where STR_IN_RE_EVAL is necessary.","shortMessageHtmlLink":"Implement new simple proof rewrite rules for strings (#10830)"}},{"before":"88b3de12e96f17b96a863e99b3813b16b803723c","after":"bd8437a04920b8764eca86c61885d5e3538b9479","ref":"refs/heads/main","pushedAt":"2024-06-04T01:31:32.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Update skolem definitions in ALF to use opaque arguments (#10841)\n\nThis removes the current hack for handling skolems in the ALF signature.\r\n\r\nIt makes use of the new :opaque feature in alfc for representing arguments that are assumed to be part of the operator.\r\n\r\nA followup PR will make the ALF printer rely on the printer for skolems (once #10835 is merged).","shortMessageHtmlLink":"Update skolem definitions in ALF to use opaque arguments (#10841)"}},{"before":"a85346296d5be71a33f900185b20d3ee0e828b65","after":"88b3de12e96f17b96a863e99b3813b16b803723c","ref":"refs/heads/main","pushedAt":"2024-06-03T19:51:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Use SET_CHOOSE operator for bounded set instantiation (#10847)\n\nThis eliminates the use of WITNESS for bounded set instantiation.\r\n\r\nTowards further simplification of skolem manager and term formula removal passes.\r\n\r\nEliminates 6 trusted proofs steps in our regressions of id WITNESS_AXIOM.","shortMessageHtmlLink":"Use SET_CHOOSE operator for bounded set instantiation (#10847)"}},{"before":"6b5f25ba281ea2ec4d59e4b3459b12cb11afc7bd","after":"a85346296d5be71a33f900185b20d3ee0e828b65","ref":"refs/heads/main","pushedAt":"2024-06-02T17:27:28.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"[alethe] Updates to node converter (#10659)\n\nMakes it track errors that can result from unsupported elements in the proof, as well as proper support for the new architecture of Skolem handling, besides other miscellaneous changes.","shortMessageHtmlLink":"[alethe] Updates to node converter (#10659)"}},{"before":"78be2504476666271272045c1252d0abba773df3","after":"6b5f25ba281ea2ec4d59e4b3459b12cb11afc7bd","ref":"refs/heads/main","pushedAt":"2024-06-02T16:59:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Add remaining arithmetic and string RARE rewrites (#10832)\n\nEliminates 3 rules that are very specific cases of an ad-hoc theory rewrite.\r\n\r\nGeneralizes one existing RARE rewrite str-contains-concat-find.","shortMessageHtmlLink":"Add remaining arithmetic and string RARE rewrites (#10832)"}},{"before":"635a2acb8393c1812b99d22fd12bb583e4d3cd7e","after":"78be2504476666271272045c1252d0abba773df3","ref":"refs/heads/main","pushedAt":"2024-06-01T00:11:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Update string util for regexp concatenation (#10839)\n\nWhen the proof rewrite rule corresponding to STR_IN_RE_CONSUME is added, it will require update to the mkConcat utility to ensure we handle regular expression concatenation as well.","shortMessageHtmlLink":"Update string util for regexp concatenation (#10839)"}},{"before":"f1816c75c9151cfcc24b8e1be74a9a93056d77a5","after":"635a2acb8393c1812b99d22fd12bb583e4d3cd7e","ref":"refs/heads/main","pushedAt":"2024-05-31T23:41:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"ajreynol","name":"Andrew Reynolds","path":"/ajreynol","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2973467?s=80&v=4"},"commit":{"message":"Refactor strings entailment utility in preparation for new proof rewrite rule (#10838)\n\nAnalogous to the arithmetic utility, we need a version of this utility which does not use the rewriter as a subroutine.","shortMessageHtmlLink":"Refactor strings entailment utility in preparation for new proof rewr…"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEX6fiDAA","startCursor":null,"endCursor":null}},"title":"Activity · cvc5/cvc5"}