| 4452548 | Anish Tondwalkar | 02 May 2019, 21:18:18 UTC | Unfuck doctests | 02 May 2019, 21:18:18 UTC |
| 097f354 | Anish Tondwalkar | 27 April 2019, 21:01:51 UTC | Merge remote-tracking branch 'origin/develop' into horn-tx | 27 April 2019, 21:01:51 UTC |
| 06cff38 | Anish Tondwalkar | 27 April 2019, 19:51:14 UTC | Update quantifier elimination for side conditions - Drop terms less agressively - When we produce a kvar in the head position, split that constraint | 27 April 2019, 19:51:14 UTC |
| c47a4df | Ranjit Jhala | 12 April 2019, 18:59:25 UTC | Merge pull request #394 from ucsd-progsys/ple2 Encode coercions as uninterpreted functions | 12 April 2019, 18:59:25 UTC |
| 130f3a9 | Ranjit Jhala | 11 April 2019, 19:50:01 UTC | done: coerce-apply, see ucsd-progsys/liquidhaskell#1424 | 11 April 2019, 19:50:01 UTC |
| 876cd13 | Ranjit Jhala | 11 April 2019, 18:12:14 UTC | first constraint OK | 11 April 2019, 18:12:14 UTC |
| 93b8d45 | Niki Vazou | 28 March 2019, 10:06:09 UTC | Merge pull request #393 from peti/develop drop redundant dependencies from Cabal file | 28 March 2019, 10:06:09 UTC |
| d325af5 | Peter Simons | 28 March 2019, 09:15:27 UTC | liquid-fixpoint.cabal: pretty-print the file with stylish-cabal | 28 March 2019, 09:15:27 UTC |
| 17e752c | Peter Simons | 28 March 2019, 09:13:10 UTC | liquid-fixpoint.cabal: drop redundant dependencies & simplify the file | 28 March 2019, 09:13:10 UTC |
| 42c027a | Ranjit Jhala | 23 March 2019, 17:03:33 UTC | Merge pull request #391 from ucsd-progsys/ghc-863 Update to GHC 8.6.4 | 23 March 2019, 17:03:33 UTC |
| ac3e9dd | Ranjit Jhala | 19 March 2019, 03:42:32 UTC | bump cabal version | 19 March 2019, 03:42:32 UTC |
| a255d28 | Ranjit Jhala | 18 March 2019, 23:14:25 UTC | bump cabal version | 18 March 2019, 23:14:25 UTC |
| abb3595 | Anish Tondwalkar | 10 March 2019, 07:21:30 UTC | horn pi elim: qe in side condition | 18 March 2019, 22:40:56 UTC |
| 9ab4954 | Ranjit Jhala | 17 March 2019, 19:21:09 UTC | builds against 863 | 17 March 2019, 19:21:09 UTC |
| 04cf502 | Anish Tondwalkar | 26 February 2019, 00:20:39 UTC | drop useless quantifiers | 26 February 2019, 00:20:39 UTC |
| 13c01e3 | Anish Tondwalkar | 24 February 2019, 08:00:21 UTC | transformations inside solve, NOT solveHorn | 24 February 2019, 08:00:21 UTC |
| 549322c | Anish Tondwalkar | 24 February 2019, 05:30:17 UTC | Flatten (simplify) constraints before solving | 24 February 2019, 05:30:17 UTC |
| b3f6430 | Anish Tondwalkar | 23 February 2019, 21:45:35 UTC | Add support for constants and distincts to Horn | 23 February 2019, 21:45:35 UTC |
| 546ca77 | Anish Tondwalkar | 19 February 2019, 19:32:21 UTC | Finished horn side conditions. needs refactoring | 19 February 2019, 19:51:49 UTC |
| 4dc2659 | Anish Tondwalkar | 18 February 2019, 22:05:03 UTC | minor cleanup | 18 February 2019, 22:05:03 UTC |
| 28caf05 | Anish Tondwalkar | 18 February 2019, 10:30:05 UTC | DONE: QE. Next: checkSides | 18 February 2019, 10:30:05 UTC |
| 542ffcc | Anish Tondwalkar | 18 February 2019, 09:49:54 UTC | QE works on ebind-03 (ad-hoc) | 18 February 2019, 09:49:54 UTC |
| 80ce62f | Anish Tondwalkar | 18 February 2019, 04:57:12 UTC | Rewrote Horn.solveEbs, so that QE behaves Still need to get QE to work right in the presence of KVars. This amounts to making sure the syntactic form of the kvar solution is amenable to QE. | 18 February 2019, 04:57:12 UTC |
| b757bd6 | Anish Tondwalkar | 17 February 2019, 12:42:53 UTC | checking in QE before starting over on it | 17 February 2019, 12:42:53 UTC |
| cc01aa8 | Anish Tondwalkar | 17 February 2019, 10:28:06 UTC | futzing around with QE | 17 February 2019, 10:28:06 UTC |
| 2fdaa49 | Anish Tondwalkar | 17 February 2019, 09:33:25 UTC | elimKs: gracefully handle cycles | 17 February 2019, 09:33:25 UTC |
| 7f0a9eb | Anish Tondwalkar | 17 February 2019, 09:32:02 UTC | slight refactoring - Horn.solve pull out the uniq phase - hypPred is now readable by mortals^W^W without flipping back and forth to the definition of mrExprInfos | 17 February 2019, 09:32:02 UTC |
| 3c6c72b | Anish Tondwalkar | 16 February 2019, 22:14:42 UTC | Add command line for --eliminate=existentials (only works with the Horn format) | 16 February 2019, 22:14:42 UTC |
| fdc9f6a | Anish Tondwalkar | 16 February 2019, 21:09:57 UTC | Horn solve ebs - sketch/build out control flow - fix poke and sides - add elimPis, elimKs - start work on QE | 16 February 2019, 21:09:57 UTC |
| 46dfead | Ranjit Jhala | 13 February 2019, 05:18:55 UTC | Merge pull request #390 from ucsd-progsys/missing-sort Two bug fixes | 13 February 2019, 05:18:55 UTC |
| d370604 | Ranjit Jhala | 13 February 2019, 04:58:34 UTC | TODO: add mossaka.fq test | 13 February 2019, 04:58:34 UTC |
| 13a0a7e | Ranjit Jhala | 13 February 2019, 03:20:22 UTC | only eval partial appls if Ok | 13 February 2019, 03:20:22 UTC |
| 7ae5906 | Ranjit Jhala | 13 February 2019, 03:13:49 UTC | only eval partial appls if Ok | 13 February 2019, 03:13:49 UTC |
| 84dab94 | Ranjit Jhala | 13 February 2019, 01:47:37 UTC | only eval partial appls if Ok | 13 February 2019, 01:47:37 UTC |
| aa8ecc6 | Ranjit Jhala | 13 February 2019, 00:02:39 UTC | banging head against mossaka bug | 13 February 2019, 00:02:39 UTC |
| 6d17b8a | Ranjit Jhala | 12 February 2019, 19:24:00 UTC | add MJ test | 12 February 2019, 19:24:00 UTC |
| 60df75e | Anish Tondwalkar | 12 February 2019, 09:40:34 UTC | make poke use pivars instead of reusing the ebind | 12 February 2019, 09:40:34 UTC |
| 4605e7f | Ranjit Jhala | 12 February 2019, 07:44:37 UTC | asd | 12 February 2019, 07:44:37 UTC |
| 5096722 | Ranjit Jhala | 12 February 2019, 07:14:33 UTC | temp checkin: missing sort | 12 February 2019, 07:14:33 UTC |
| 62e9c57 | Ranjit Jhala | 12 February 2019, 04:04:53 UTC | don't generate equations for data-constructors | 12 February 2019, 04:04:53 UTC |
| 43076c4 | Ranjit Jhala | 12 February 2019, 00:22:18 UTC | aha, add binders for ... binders | 12 February 2019, 00:22:18 UTC |
| a7becfd | Anish Tondwalkar | 11 February 2019, 18:54:31 UTC | Add tests from ICFP paper for eliminate=horn | 11 February 2019, 18:55:49 UTC |
| 5d3d171 | Anish Tondwalkar | 10 February 2019, 00:18:41 UTC | Pretty Print constraints | 11 February 2019, 18:55:49 UTC |
| e9df778 | Anish Tondwalkar | 09 February 2019, 23:08:29 UTC | Add command line flags for Horn transformations --eliminate=horn now runs eliminate on the NFF HC --eliminate=some is now the default for solveHorn -v --eliminate=horn prints out the uniqified and eliminated NNF HC | 11 February 2019, 18:55:49 UTC |
| b60c46c | Anish Tondwalkar | 09 February 2019, 05:20:15 UTC | implement uniq pass on horn | 11 February 2019, 18:55:49 UTC |
| eec773f | Ranjit Jhala | 10 February 2019, 02:14:36 UTC | Merge pull request #389 from ucsd-progsys/T1371 Update no-eval-ite for mutrec functions | 10 February 2019, 02:14:36 UTC |
| 7870d9e | Ranjit Jhala | 10 February 2019, 01:30:04 UTC | update no-eval-ite for mutrec functions | 10 February 2019, 01:30:04 UTC |
| 6fb5657 | Ranjit Jhala | 10 February 2019, 00:06:44 UTC | Merge pull request #388 from ucsd-progsys/T1371 T1371 | 10 February 2019, 00:06:44 UTC |
| f60841d | Ranjit Jhala | 09 February 2019, 23:03:00 UTC | next: fix StlcBug and T1371 | 09 February 2019, 23:03:00 UTC |
| e5737f5 | Ranjit Jhala | 09 February 2019, 22:37:02 UTC | don't eval recursive-funs under unknown guard | 09 February 2019, 22:37:02 UTC |
| 27ad9b6 | Ranjit Jhala | 08 February 2019, 23:23:03 UTC | Disable tracpp | 08 February 2019, 23:23:03 UTC |
| 7bdce09 | Ranjit Jhala | 08 February 2019, 20:05:15 UTC | temp checkin | 08 February 2019, 20:05:15 UTC |
| 1411b21 | Ranjit Jhala | 08 February 2019, 17:04:50 UTC | about to add 'stack' to eval | 08 February 2019, 17:04:50 UTC |
| 8c10920 | Anish Tondwalkar | 08 February 2019, 12:30:02 UTC | Fixed substitutions in Horn/elim | 08 February 2019, 12:30:02 UTC |
| 54797c1 | Anish Tondwalkar | 07 February 2019, 23:57:23 UTC | Start debugging Horn.elim | 07 February 2019, 23:57:23 UTC |
| 0ac8aec | Ranjit Jhala | 07 February 2019, 23:31:37 UTC | don't eval under unknown guard. sigh. | 07 February 2019, 23:31:37 UTC |
| d4ca29f | Ranjit Jhala | 07 February 2019, 22:03:47 UTC | don't eval under unknown guard. sigh. | 07 February 2019, 22:03:47 UTC |
| 50ad58d | Ranjit Jhala | 07 February 2019, 21:50:18 UTC | merged in reflect-string | 07 February 2019, 21:50:18 UTC |
| 78ac477 | Ranjit Jhala | 07 February 2019, 21:32:36 UTC | yuck | 07 February 2019, 21:32:36 UTC |
| 683e85c | Ranjit Jhala | 07 February 2019, 21:26:27 UTC | add minimal test | 07 February 2019, 21:26:27 UTC |
| 983264c | Ranjit Jhala | 07 February 2019, 20:46:38 UTC | add minimal test | 07 February 2019, 20:46:38 UTC |
| a91c833 | Ranjit Jhala | 07 February 2019, 17:34:30 UTC | Merge pull request #385 from ucsd-progsys/T1409 T1409 | 07 February 2019, 17:34:30 UTC |
| 9f4df57 | Ranjit Jhala | 07 February 2019, 14:31:58 UTC | fixes liquidhaskell/#1409 | 07 February 2019, 14:31:58 UTC |
| b4298e2 | Ranjit Jhala | 07 February 2019, 13:06:07 UTC | dont remove unfolded cands; not FULLY unfolded, cf ple3.fq | 07 February 2019, 13:06:07 UTC |
| c34b3e0 | Ranjit Jhala | 07 February 2019, 12:54:30 UTC | asd | 07 February 2019, 12:54:30 UTC |
| 94c715c | Anish Tondwalkar | 05 February 2019, 11:22:50 UTC | needs scoping to terminate, as written | 05 February 2019, 11:26:06 UTC |
| 860cfd3 | Anish Tondwalkar | 05 February 2019, 10:48:24 UTC | rewrote Horn Eliminate to use cubes | 05 February 2019, 11:26:06 UTC |
| b64b805 | Anish Tondwalkar | 05 February 2019, 09:55:30 UTC | Sketch out Eliminate on Horns | 05 February 2019, 09:55:30 UTC |
| 29ba825 | Anish Tondwalkar | 05 February 2019, 07:13:45 UTC | Add poke transformation | 05 February 2019, 07:13:45 UTC |
| 1a3f61a | Anish Tondwalkar | 05 February 2019, 04:47:40 UTC | Update .gitignore | 05 February 2019, 04:48:08 UTC |
| 624ae6f | Anish Tondwalkar | 05 February 2019, 04:43:48 UTC | Add option parsing to Horn Query files Right now it's just using the sexpr-ified version of the old fq, eg: (fixpoint "--option=value") but that can (should?) be changed to better conform to the smt2 spec | 05 February 2019, 04:48:08 UTC |
| 7fe3a4f | Anish Tondwalkar | 03 February 2019, 01:11:58 UTC | Add ebinds to Horn format This adds another constructor `Any` that mirrors `All, but is parsed in from an exists instead of a forall, and is translated to fq in the same way, except that variables bouned by `Any` are added to the fq's ebinds to indicate that they're existentially bound. | 03 February 2019, 04:56:56 UTC |
| f0cba5f | Ranjit Jhala | 20 December 2018, 04:25:28 UTC | fixes #383 | 20 December 2018, 04:25:28 UTC |
| d7d1d64 | Ranjit Jhala | 20 December 2018, 04:15:19 UTC | use fixpoint-loop in PLE | 20 December 2018, 04:15:19 UTC |
| bc256f7 | Ranjit Jhala | 19 December 2018, 21:42:27 UTC | add fixpoint-loop to OLD PLE | 19 December 2018, 21:42:27 UTC |
| 91546f1 | Ranjit Jhala | 19 December 2018, 19:25:24 UTC | add minimal fq test showing ple get set bug | 19 December 2018, 19:25:24 UTC |
| 95456c1 | Ranjit Jhala | 19 December 2018, 05:01:13 UTC | remove debug | 19 December 2018, 05:01:13 UTC |
| 5b495e8 | Ranjit Jhala | 19 December 2018, 04:46:26 UTC | check isString when computing sortSmtSort | 19 December 2018, 04:46:26 UTC |
| c86dbe4 | Ranjit Jhala | 18 December 2018, 23:55:31 UTC | sigh, declared victory too soon | 18 December 2018, 23:55:31 UTC |
| f3a7f69 | Ranjit Jhala | 17 December 2018, 22:27:21 UTC | fix merge bugs | 17 December 2018, 22:27:21 UTC |
| 03d2a6a | Ranjit Jhala | 17 December 2018, 22:18:59 UTC | add final | 17 December 2018, 22:18:59 UTC |
| dfcf0ec | Ranjit Jhala | 17 December 2018, 22:02:18 UTC | asd | 17 December 2018, 22:02:18 UTC |
| 59410b2 | Ranjit Jhala | 17 December 2018, 22:00:39 UTC | Merge pull request #382 from ucsd-progsys/incr-ple-debug Bug fix for Incr-PLE | 17 December 2018, 22:00:39 UTC |
| f76fc0a | Ranjit Jhala | 16 December 2018, 18:12:29 UTC | remove debug | 16 December 2018, 18:12:29 UTC |
| 95fff16 | Ranjit Jhala | 16 December 2018, 18:08:06 UTC | asd | 16 December 2018, 18:08:06 UTC |
| fd3f6d6 | Ranjit Jhala | 14 December 2018, 23:53:59 UTC | asd | 14 December 2018, 23:53:59 UTC |
| 7d0223f | Ranjit Jhala | 14 December 2018, 21:06:34 UTC | asd Merge branch 'develop' of github.com:ucsd-progsys/liquid-fixpoint into develop | 14 December 2018, 21:06:34 UTC |
| d3f36f2 | Ranjit Jhala | 14 December 2018, 20:20:59 UTC | asd | 14 December 2018, 20:20:59 UTC |
| 68ee9fa | Ranjit Jhala | 14 December 2018, 17:10:14 UTC | asd | 14 December 2018, 17:10:14 UTC |
| cd0ebe4 | Ranjit Jhala | 12 December 2018, 23:04:28 UTC | Merge pull request #381 from ucsd-progsys/ple-opt Incremental PLE | 12 December 2018, 23:04:28 UTC |
| e9abf9b | Ranjit Jhala | 12 December 2018, 19:17:22 UTC | moved to incremental SMT | 12 December 2018, 19:17:22 UTC |
| 57a641b | Ranjit Jhala | 12 December 2018, 18:42:27 UTC | IMPL: incremental BGPUSH | 12 December 2018, 18:42:27 UTC |
| aff8ebc | Ranjit Jhala | 12 December 2018, 18:18:34 UTC | NEXT: incremental BG-PUSH | 12 December 2018, 18:18:34 UTC |
| 8d0ed8c | Ranjit Jhala | 12 December 2018, 18:11:50 UTC | tests pass except wierd z3 SEGFAULT on DataBase.hs | 12 December 2018, 18:11:50 UTC |
| a61cf93 | Ranjit Jhala | 12 December 2018, 17:27:03 UTC | incrementalPLE seems to also be a win; next use incremental Z3 contexts | 12 December 2018, 17:27:03 UTC |
| 0a850b4 | Ranjit Jhala | 12 December 2018, 05:36:14 UTC | See broken part | 12 December 2018, 05:36:14 UTC |
| f42e2a2 | Ranjit Jhala | 11 December 2018, 18:55:47 UTC | next: tests/todo/ple-WHATSIT.bfq | 11 December 2018, 18:55:47 UTC |
| 49f0c0a | Ranjit Jhala | 06 December 2018, 20:47:26 UTC | ok, make incr-ple ACTUALLY incremental. | 06 December 2018, 20:47:26 UTC |
| 5f2eb0b | Ranjit Jhala | 06 December 2018, 20:32:06 UTC | actually do the diff | 06 December 2018, 20:32:06 UTC |
| f861512 | Ranjit Jhala | 06 December 2018, 19:08:21 UTC | fp tests pass FWIW | 06 December 2018, 19:08:21 UTC |
