{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":707345590,"defaultBranch":"main","name":"PeanutProver","ownerLogin":"PeanutProver","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-10-19T17:50:27.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/148484810?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1701868012.0","currentOid":""},"activityList":{"items":[{"before":"66d3d98599cddc6a6e64b2f2cdfcb585039bf909","after":"b5f2bf0c9caa0ee8697cf2b3b48aac61b8e8a416","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-09T15:35:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add basic processing of \\forall quantifier\n\nUnresolved!! Required nfa -> dfa function before complement","shortMessageHtmlLink":"Add basic processing of \\forall quantifier"}},{"before":"8cf4bb3e3290c85d775c2748494c22848857eb09","after":"e9a4b752bb6c08b7e8b7841f8a5a3e3cba1fcf36","ref":"refs/heads/main","pushedAt":"2023-12-09T15:12:10.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"},"commit":{"message":"Add constant equality support","shortMessageHtmlLink":"Add constant equality support"}},{"before":"5c72d8f7a251ec7bfa165bdc153ee473b824b07a","after":"66d3d98599cddc6a6e64b2f2cdfcb585039bf909","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-09T08:48:11.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add basic processing of \\forall quantifier\n\nUnresolved!! Required nfa -> dfa function before complement","shortMessageHtmlLink":"Add basic processing of \\forall quantifier"}},{"before":"5a569e2de7c16bcb1199613aecb771603d6ec517","after":"5c72d8f7a251ec7bfa165bdc153ee473b824b07a","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-08T19:59:33.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add basic processing of \\forall quantifier\n\nUnresolved!! Required nfa -> dfa function before complement","shortMessageHtmlLink":"Add basic processing of \\forall quantifier"}},{"before":"8874788b575ca822b4eedeee56e566fe946d9bf3","after":"5a569e2de7c16bcb1199613aecb771603d6ec517","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-08T19:58:52.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add basic processing of \\forall quantifier\n\nUnresolved!! Required nfa -> dfa function before complement","shortMessageHtmlLink":"Add basic processing of \\forall quantifier"}},{"before":"fe8fcd0f192041b8ad70662145aa1da3ac875bef","after":"8874788b575ca822b4eedeee56e566fe946d9bf3","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-06T16:27:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Fix pattern-matching in NfaResultToBool","shortMessageHtmlLink":"Fix pattern-matching in NfaResultToBool"}},{"before":"4e6e27be0855c6a42fd0f0d7be5735af8dccf3a1","after":"fe8fcd0f192041b8ad70662145aa1da3ac875bef","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-06T16:22:36.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add processing of formulas and preprocessing of it\n\nRebuild tree if formula contains complex terms as variables.\nParse it into nfa and work with it. Example of working:\n$even(x) /\\ $even (y)\nExample, that doesn`t work:\n\\exists a (x + y = a /\\ $even(a)).\n\nCo-authored-by: Nikolai Ponomarev <wowasterdev@gmail.com>","shortMessageHtmlLink":"Add processing of formulas and preprocessing of it"}},{"before":"a892826cae6c9780ab09a82062855092cd70d3c4","after":"4e6e27be0855c6a42fd0f0d7be5735af8dccf3a1","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-06T13:14:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add processing long chains of sum\n\nTree formula will rework, for example, if you want to write smth like that\nx + y + z + u = v\nthen it rebuild into\n\\exists e0 (x + y = e0 /\\ (\\exists e1 (e0 + z = e1 /\\ (\\exists e2 (e1 + u = e2 /\\ e2 = v)))))\nfor now it works only with sum and equals, but it probably can be useful\nfor processing formulas like that:\n\\forall x, y (even(x) /\\ even(y) -> even(x + y))","shortMessageHtmlLink":"Add processing long chains of sum"}},{"before":"8c1110f90a7fabd7afe8cce194a9a1d6d15c1ec8","after":null,"ref":"refs/heads/inflate_transitions","pushedAt":"2023-12-06T13:06:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"}},{"before":"d2be455bc5798d8027194da353bb174045104b06","after":null,"ref":"refs/heads/dfa","pushedAt":"2023-12-06T13:06:42.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"}},{"before":"160d46e3972f03210135d489e61cad757f2eab26","after":null,"ref":"refs/heads/cli","pushedAt":"2023-12-06T13:06:37.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"}},{"before":"0c16fa878cf9bd26cac1f96f3a50bd303194ca9e","after":null,"ref":"refs/heads/minimization","pushedAt":"2023-12-06T13:06:22.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"}},{"before":"952cb387be01e162257cc06506e7833b406e9f7d","after":"8cf4bb3e3290c85d775c2748494c22848857eb09","ref":"refs/heads/main","pushedAt":"2023-12-06T13:06:18.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"},"commit":{"message":"Make minimization faster","shortMessageHtmlLink":"Make minimization faster"}},{"before":"71c958515c67eb3775563885e225c8cc450bc67a","after":"0c16fa878cf9bd26cac1f96f3a50bd303194ca9e","ref":"refs/heads/minimization","pushedAt":"2023-12-06T13:01:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Make minimization faster","shortMessageHtmlLink":"Make minimization faster"}},{"before":"1f861dd873f6fab63a24a6291cfdec62c09be1da","after":"a892826cae6c9780ab09a82062855092cd70d3c4","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-06T11:43:57.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add processing long chains of sum\n\nTree formula will rework, for example, if you want to write smth like that\nx + y + z + u = v\nthen it rebuild into\n\\exists e0 (x + y = e0 /\\ (\\exists e1 (e0 + z = e1 /\\ (\\exists e2 (e1 + u = e2 /\\ e2 = v)))))\nfor now it works only with sum and equals, but it probably can be useful\nfor processing formulas like that:\n\\forall x, y (even(x) /\\ even(y) -> even(x + y))","shortMessageHtmlLink":"Add processing long chains of sum"}},{"before":"5f3f5a719c0d786e4fcc75d0db6f85c48e67e11d","after":"71c958515c67eb3775563885e225c8cc450bc67a","ref":"refs/heads/minimization","pushedAt":"2023-12-04T10:45:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Fix major mistake in main algorithm","shortMessageHtmlLink":"Fix major mistake in main algorithm"}},{"before":"0a12d9a342818df6be3f1f7bc14f16b550fecec7","after":"1f861dd873f6fab63a24a6291cfdec62c09be1da","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-04T09:51:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add processing long chains of sum\n\nTree formula will rework, for example, if you want to write smth like that\nx + y + z + u = v\nthen it rebuild into\n\\exists e0 (x + y = e0 /\\ (\\exists e1 (e0 + z = e1 /\\ (\\exists e2 (e1 + u = e2 /\\ e2 = v)))))\nfor now it works only with sum and equals, but it probably can be useful\nfor processing formulas like that:\n\\forall x, y (even(x) /\\ even(y) -> even(x + y))","shortMessageHtmlLink":"Add processing long chains of sum"}},{"before":"07c50a4c35212552aa5d99a5d264d97de8914ab1","after":"5f3f5a719c0d786e4fcc75d0db6f85c48e67e11d","ref":"refs/heads/minimization","pushedAt":"2023-12-03T09:37:08.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add minimization and implement it into FolToNFA\n\nSquashed commits:\nAdd basic minimize function\nRewrite AllStates function into function-style\nRename newTransaction to newTransitions and rework AllStates\nAdd deleting unreachable from start states and add Reachable from state\nfunction into nfa","shortMessageHtmlLink":"Add minimization and implement it into FolToNFA"}},{"before":"4f22a739cc8a7d68c6caedee213cdc6ea32c1cfa","after":"07c50a4c35212552aa5d99a5d264d97de8914ab1","ref":"refs/heads/minimization","pushedAt":"2023-12-03T08:58:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add deleting unreachable from start states","shortMessageHtmlLink":"Add deleting unreachable from start states"}},{"before":"f54684e93d2ec1aaeded62b11a5724b53193f2c7","after":"4f22a739cc8a7d68c6caedee213cdc6ea32c1cfa","ref":"refs/heads/minimization","pushedAt":"2023-12-02T19:51:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Rename newTransaction to newTransitions and rework newStates","shortMessageHtmlLink":"Rename newTransaction to newTransitions and rework newStates"}},{"before":"96d6d193b3aa2441679ec6fd79f716ea0fe91134","after":"f54684e93d2ec1aaeded62b11a5724b53193f2c7","ref":"refs/heads/minimization","pushedAt":"2023-12-02T17:32:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Rewrite AllStates function into function-style","shortMessageHtmlLink":"Rewrite AllStates function into function-style"}},{"before":null,"after":"0a12d9a342818df6be3f1f7bc14f16b550fecec7","ref":"refs/heads/automaton_calling","pushedAt":"2023-12-02T15:36:06.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add processing of formula","shortMessageHtmlLink":"Add processing of formula"}},{"before":"0b134e7b486d12b391fa88457d65987b3c1e0347","after":"96d6d193b3aa2441679ec6fd79f716ea0fe91134","ref":"refs/heads/minimization","pushedAt":"2023-12-02T15:30:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Some prettier changes","shortMessageHtmlLink":"Some prettier changes"}},{"before":"95fb3a42326769d49548f79fff20942b551957dc","after":"0b134e7b486d12b391fa88457d65987b3c1e0347","ref":"refs/heads/minimization","pushedAt":"2023-12-02T13:35:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add minimization and implement it into FolToNFA","shortMessageHtmlLink":"Add minimization and implement it into FolToNFA"}},{"before":null,"after":"95fb3a42326769d49548f79fff20942b551957dc","ref":"refs/heads/minimization","pushedAt":"2023-12-02T13:14:15.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add minimization and implement it into FolToNFA","shortMessageHtmlLink":"Add minimization and implement it into FolToNFA"}},{"before":"12c27475e79b29afe6a554f7afea610b7e209da6","after":"952cb387be01e162257cc06506e7833b406e9f7d","ref":"refs/heads/main","pushedAt":"2023-12-01T15:54:35.000Z","pushType":"pr_merge","commitsCount":11,"pusher":{"login":"WoWaster","name":"Nikolai Ponomarev","path":"/WoWaster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/11057754?s=80&v=4"},"commit":{"message":"Fix ToDot output","shortMessageHtmlLink":"Fix ToDot output"}},{"before":"632746b2e383e1df8b31be93eafded7c8a84f662","after":"8c1110f90a7fabd7afe8cce194a9a1d6d15c1ec8","ref":"refs/heads/inflate_transitions","pushedAt":"2023-11-24T09:03:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Fix finding place function","shortMessageHtmlLink":"Fix finding place function"}},{"before":"9a6ad754e24a5669abcd355778084bc84bc44058","after":"632746b2e383e1df8b31be93eafded7c8a84f662","ref":"refs/heads/inflate_transitions","pushedAt":"2023-11-23T19:46:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add permutation\n\nPermutation at moment of building dfa: you need to permute it correctly\nto union or intersect, because if you do this at 'eval' moment, then\nyou worked with same dfas and at many cases it useless or wrong","shortMessageHtmlLink":"Add permutation"}},{"before":"1d17e76868a22cb676616273a17eb7c3e0c53220","after":"266c2be672a9250f18af30625ffa6db106473123","ref":"refs/heads/dfa1","pushedAt":"2023-11-23T10:58:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Anya497","name":"Anya Chistyakova","path":"/Anya497","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/57658770?s=80&v=4"},"commit":{"message":"Rename DFA to FA","shortMessageHtmlLink":"Rename DFA to FA"}},{"before":"9e5ad710017e4d025a12de0c70f7909a7b019772","after":"9a6ad754e24a5669abcd355778084bc84bc44058","ref":"refs/heads/inflate_transitions","pushedAt":"2023-11-23T10:05:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"KubEF","name":"Efim Kubishkin","path":"/KubEF","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/78155213?s=80&v=4"},"commit":{"message":"Add zero padding for input","shortMessageHtmlLink":"Add zero padding for input"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAADxiQDUgA","startCursor":null,"endCursor":null}},"title":"Activity · PeanutProver/PeanutProver"}