{"push_id":1066325769,"size":25,"distinct_size":1,"ref":"refs/heads/master","head":"3108cf6113d65dcb756cc76f8ae40231fdc2e6fc","before":"a1b8ab6d3e47956ed9b89b806b44dc0536a92107","commits":[{"sha":"0930564b915acb548774d9a2513c2ea51e25fdc0","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add inert fixedpoint responses.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/0930564b915acb548774d9a2513c2ea51e25fdc0"},{"sha":"91fd8607bffc7d9675898fac684638bc44cdcac3","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add (broken) MuZ3 solver.\n\nMuZ3 seems to want us to declare all the variables up-front or\nsomething, but we aren't, so it thinks the variables are\nuninterpreted?\n\nAlso, I'm not sure how to pose an IFF to MuZ3.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/91fd8607bffc7d9675898fac684638bc44cdcac3"},{"sha":"71681b9c8abeb53b446fb824268a49ccc96339dc","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Make viewdefs muZ3 constraints.\n\nThis is probably wrong, but it's easily reversed.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/71681b9c8abeb53b446fb824268a49ccc96339dc"},{"sha":"e47c7f8735e611a5f766c56e5241a1d0c2c83725","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Describe why muz3 returned UNKNOWN.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/e47c7f8735e611a5f766c56e5241a1d0c2c83725"},{"sha":"688149afc9a8aaa8b8dcbaee1d1d81a81c1f3d86","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Use PDR engine.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/688149afc9a8aaa8b8dcbaee1d1d81a81c1f3d86"},{"sha":"3433ab99ed3a310c07d7b345c71dcb8cf780eab7","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Rearrange MuZ3 query into more sensible form.\n\nStill doesn't work, and we may need to move one end of the viewdef\nimplications into the other rules.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/3433ab99ed3a310c07d7b345c71dcb8cf780eab7"},{"sha":"6d4cf20588aeb4589a0005067814ed9cbb9952f4","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Make varsIn return type too.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/6d4cf20588aeb4589a0005067814ed9cbb9952f4"},{"sha":"6dbc6a2dc710a28b36576f13f9300718a3038d3f","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add universal quantifications.\n\nThis gets us further: we now have pdr proofs going through, but\nthey're not the correct ones.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/6dbc6a2dc710a28b36576f13f9300718a3038d3f"},{"sha":"34f959e3348ff42f98cc5266430e4a23fdfbf84a","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Fix doc comment typo.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/34f959e3348ff42f98cc5266430e4a23fdfbf84a"},{"sha":"883800b2b99d6d088b116c51e189f49b66554cc0","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Factor out making FuncTables from ViewDefs.\n\nThe MuZ3 engine is about to use the same thing.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/883800b2b99d6d088b116c51e189f49b66554cc0"},{"sha":"6cf30faa137ddc19a0e670b89c89d6462db716ff","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Fix doc bugs while I'm here.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/6cf30faa137ddc19a0e670b89c89d6462db716ff"},{"sha":"3beda4adcad22a8aeeeb9d26c82e932d9040fcf5","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add intermediate stage to dump fixpoint.\n\nThis allows us to compare the fixpoints with intuition.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/3beda4adcad22a8aeeeb9d26c82e932d9040fcf5"},{"sha":"7a5ae41e9d1193086b58de8ecb0e9e6219edbf0e","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Only translate useful GView funcs.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/7a5ae41e9d1193086b58de8ecb0e9e6219edbf0e"},{"sha":"85296248a9983d5a90d3756d477f2d205c3515b2","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Fix space error.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/85296248a9983d5a90d3756d477f2d205c3515b2"},{"sha":"e797733048a04e7c114d1a65a983c19a8b68fe12","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Don't use flexible_trace.\n\nThis seems to cause incompleteness (unsat things being marked as sat).","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/e797733048a04e7c114d1a65a983c19a8b68fe12"},{"sha":"ade0a4d7b031bbef46f08ed94865a25ceee8254f","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add toString for guarded things.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/ade0a4d7b031bbef46f08ed94865a25ceee8254f"},{"sha":"ae144382a6bfc8e4f52d1220ca65d91b27943016","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Fix type of `gfunc`.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/ae144382a6bfc8e4f52d1220ca65d91b27943016"},{"sha":"7befe3a3652228a63d8866b23c177ab4eae56b10","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Add and use variable extractors for GFuncs and VFuncs.\n\nThese ones, unlike the ad-hoc one we had for mkRule before, actually\nwork properly (ie extract variables for guards).","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/7befe3a3652228a63d8866b23c177ab4eae56b10"},{"sha":"df2c9f258b25ac1a5ad1dd92dc644876a1d9cb8c","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Make muZ3 output easier to read.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/df2c9f258b25ac1a5ad1dd92dc644876a1d9cb8c"},{"sha":"8ccdc9d4d604ab26464bedb4fd4e24db5de3bc8d","author":{"email":"963dc18a2763e998a6a66f3068199883f03729a4@york.ac.uk","name":"Matt Windsor"},"message":"Make rule generation more robust.\n\nWe now don't create a MkForall when the variable list is empty.","distinct":false,"url":"https://api.github.com/repos/septract/starling-tool/commits/8ccdc9d4d604ab26464bedb4fd4e24db5de3bc8d"}]}