{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":794350381,"defaultBranch":"main","name":"simple-smt-ocaml","ownerLogin":"GaloisInc","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2024-05-01T00:33:47.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/1584774?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1714523793.0","currentOid":""},"activityList":{"items":[{"before":"7749547a4831ef05e5850db3a7d361cc6e78c4c3","after":"772170fe646b3b7a984aee6ba15bcc1be8b52763","ref":"refs/heads/main","pushedAt":"2024-05-16T18:24:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add `is` recognizers","shortMessageHtmlLink":"Add <code>is</code> recognizers"}},{"before":"57af563b5b1deefd19fb1994a86a4918442c6d5a","after":"7749547a4831ef05e5850db3a7d361cc6e78c4c3","ref":"refs/heads/main","pushedAt":"2024-05-16T00:25:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Some not very standtad mod/rem terms","shortMessageHtmlLink":"Some not very standtad mod/rem terms"}},{"before":"1a1109cbe6d6e5287b7819cb22b6c83651e8bbfc","after":"57af563b5b1deefd19fb1994a86a4918442c6d5a","ref":"refs/heads/main","pushedAt":"2024-05-15T23:53:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"More consistent naming of comparison operators.","shortMessageHtmlLink":"More consistent naming of comparison operators."}},{"before":"b99b7c62e9d115bdbf83da8718636f83b2086a25","after":"1a1109cbe6d6e5287b7819cb22b6c83651e8bbfc","ref":"refs/heads/main","pushedAt":"2024-05-15T19:17:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Check if an expression is just an atom.","shortMessageHtmlLink":"Check if an expression is just an atom."}},{"before":"170920a05da961c5b95b885fae9920a652c1758b","after":"b99b7c62e9d115bdbf83da8718636f83b2086a25","ref":"refs/heads/main","pushedAt":"2024-05-15T00:48:00.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add support for let; fix real constants; Allow for variable patterns in match","shortMessageHtmlLink":"Add support for let; fix real constants; Allow for variable patterns …"}},{"before":"1d8590c9f06af80ee0af88e886d5a0cdc44660b4","after":"170920a05da961c5b95b885fae9920a652c1758b","ref":"refs/heads/main","pushedAt":"2024-05-08T18:43:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add `match` for checking datatypes","shortMessageHtmlLink":"Add <code>match</code> for checking datatypes"}},{"before":"3eb14d655fc16e92986972eb9980217a007d0f18","after":"1d8590c9f06af80ee0af88e886d5a0cdc44660b4","ref":"refs/heads/main","pushedAt":"2024-05-08T17:32:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add `const` for array. This is an extension","shortMessageHtmlLink":"Add <code>const</code> for array. This is an extension"}},{"before":"0b469a3b430ee33647e9223149070f2fe55f1650","after":"3eb14d655fc16e92986972eb9980217a007d0f18","ref":"refs/heads/main","pushedAt":"2024-05-07T21:15:51.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Rearrange arguments of `bv_extract` and document it.","shortMessageHtmlLink":"Rearrange arguments of <code>bv_extract</code> and document it."}},{"before":"0093f5c05e97b341d822fd710155b7199d7c0950","after":"0b469a3b430ee33647e9223149070f2fe55f1650","ref":"refs/heads/main","pushedAt":"2024-05-06T21:12:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Make push and pop have their parameters.","shortMessageHtmlLink":"Make push and pop have their parameters."}},{"before":"570d3be37fcc3f63e745e0b8bc48fa08b2427331","after":"0093f5c05e97b341d822fd710155b7199d7c0950","ref":"refs/heads/main","pushedAt":"2024-05-04T00:12:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Separate the S-expressions for commands, from issuing the commands.\n\nThis is useful because it makes it easier to log/collect commands\nthat we are issuing.","shortMessageHtmlLink":"Separate the S-expressions for commands, from issuing the commands."}},{"before":"45034546c3fa0b846e44cd717043fdd370ac9816","after":"570d3be37fcc3f63e745e0b8bc48fa08b2427331","ref":"refs/heads/main","pushedAt":"2024-05-03T21:25:42.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Update docs","shortMessageHtmlLink":"Update docs"}},{"before":"f7f84cd856a2f92196893fda1968305ce060decf","after":"45034546c3fa0b846e44cd717043fdd370ac9816","ref":"refs/heads/main","pushedAt":"2024-05-03T21:13:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Update docs","shortMessageHtmlLink":"Update docs"}},{"before":"2ec557b48793b4e5a6d2de830a72bc36df3d498c","after":"f7f84cd856a2f92196893fda1968305ce060decf","ref":"refs/heads/main","pushedAt":"2024-05-03T21:10:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add support for the theory of sets.\n\nThis is not standard, so it differs a bit between `z3` and `cvc5`","shortMessageHtmlLink":"Add support for the theory of sets."}},{"before":"6f17ca8c4ccdc566c885cd17d73f2e3361a59c53","after":"2ec557b48793b4e5a6d2de830a72bc36df3d498c","ref":"refs/heads/main","pushedAt":"2024-05-03T17:03:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Do `check-sat` before evaluating.\n\nApparently the state where we have a model is very transient,\nand `push`/`pop` breaks it, so we have to reestablish it.","shortMessageHtmlLink":"Do <code>check-sat</code> before evaluating."}},{"before":"2be30c66c08d241f200e53eb7fad77dc044d39f8","after":"6f17ca8c4ccdc566c885cd17d73f2e3361a59c53","ref":"refs/heads/main","pushedAt":"2024-05-02T21:36:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add support for defining locals when evaluating in a model","shortMessageHtmlLink":"Add support for defining locals when evaluating in a model"}},{"before":"ba08bb9e30bed8aabff79cf81e376105a79a810e","after":"2be30c66c08d241f200e53eb7fad77dc044d39f8","ref":"refs/heads/main","pushedAt":"2024-05-02T20:38:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add functionality for evaluating things in the context of a model.","shortMessageHtmlLink":"Add functionality for evaluating things in the context of a model."}},{"before":"3fb61a4f7d17d15aa0d7ffa9097d0a91b3776dd5","after":"ba08bb9e30bed8aabff79cf81e376105a79a810e","ref":"refs/heads/main","pushedAt":"2024-05-02T18:16:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add a function to declare uninterpreted sorts.","shortMessageHtmlLink":"Add a function to declare uninterpreted sorts."}},{"before":"ce76a09491a032554e322294473977dca479e78b","after":"3fb61a4f7d17d15aa0d7ffa9097d0a91b3776dd5","ref":"refs/heads/main","pushedAt":"2024-05-02T18:10:41.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Update docs","shortMessageHtmlLink":"Update docs"}},{"before":"11a4264d2e7042042f6d320cfd0307219f60d167","after":"ce76a09491a032554e322294473977dca479e78b","ref":"refs/heads/main","pushedAt":"2024-05-01T21:04:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Reformat things","shortMessageHtmlLink":"Reformat things"}},{"before":"c5de8dd072f595e4721b46d952cb26db6f40e212","after":"11a4264d2e7042042f6d320cfd0307219f60d167","ref":"refs/heads/main","pushedAt":"2024-05-01T20:34:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Some functions for working with tuple-like types.","shortMessageHtmlLink":"Some functions for working with tuple-like types."}},{"before":"9b93057a0866458ad413dc56b930508ca70ae0b4","after":"c5de8dd072f595e4721b46d952cb26db6f40e212","ref":"refs/heads/main","pushedAt":"2024-05-01T17:31:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Rewrite to use explicit comparisons.","shortMessageHtmlLink":"Rewrite to use explicit comparisons."}},{"before":"07ac7581de33b20a830b4030f40a2cd2c6690cdf","after":"9b93057a0866458ad413dc56b930508ca70ae0b4","ref":"refs/heads/main","pushedAt":"2024-05-01T00:49:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add a link to the library functions","shortMessageHtmlLink":"Add a link to the library functions"}},{"before":"87222923a2617b80d01637c0701697847250cf7c","after":"07ac7581de33b20a830b4030f40a2cd2c6690cdf","ref":"refs/heads/main","pushedAt":"2024-05-01T00:48:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Add documentation, so we can serve it.","shortMessageHtmlLink":"Add documentation, so we can serve it."}},{"before":null,"after":"87222923a2617b80d01637c0701697847250cf7c","ref":"refs/heads/main","pushedAt":"2024-05-01T00:36:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"yav","name":"Iavor S. Diatchki","path":"/yav","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12394?s=80&v=4"},"commit":{"message":"Initial commit.\n\nThis is a port of the Haskell SimpleSMT library to OCaml","shortMessageHtmlLink":"Initial commit."}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAES_O-tQA","startCursor":null,"endCursor":null}},"title":"Activity · GaloisInc/simple-smt-ocaml"}