| 843ee3e | Anish Tondwalkar | 31 May 2019, 08:20:30 UTC | Flatten pisols (to improve debugging) | 31 May 2019, 08:20:30 UTC |
| e06d483 | Anish Tondwalkar | 30 May 2019, 21:10:36 UTC | hornify finalhorn as well | 30 May 2019, 21:10:36 UTC |
| 648fcc9 | Ranjit Jhala | 25 May 2019, 04:31:12 UTC | Merge pull request #400 from ucsd-progsys/horn-subst Subable instances for Horn constraints | 25 May 2019, 04:31:12 UTC |
| 0d1c66c | Ranjit Jhala | 24 May 2019, 08:28:49 UTC | remove tracing | 24 May 2019, 08:28:49 UTC |
| 7d6b858 | Ranjit Jhala | 24 May 2019, 07:49:06 UTC | use parens for kvar sort-params | 24 May 2019, 07:49:06 UTC |
| ae9a010 | Ranjit Jhala | 23 May 2019, 22:22:26 UTC | asd | 23 May 2019, 22:22:26 UTC |
| f146bba | Ranjit Jhala | 22 May 2019, 12:48:12 UTC | don't allow ueq on bool | 22 May 2019, 12:48:12 UTC |
| a378948 | Ranjit Jhala | 22 May 2019, 12:41:46 UTC | don't allow ueq on bool | 22 May 2019, 12:41:46 UTC |
| 9f7060c | Ranjit Jhala | 22 May 2019, 12:32:01 UTC | don't allow ueq on bool | 22 May 2019, 12:32:01 UTC |
| 362a902 | Ranjit Jhala | 20 May 2019, 21:29:43 UTC | twiddle | 20 May 2019, 21:29:43 UTC |
| 782dbd0 | Niki Vazou | 15 May 2019, 08:25:13 UTC | Merge pull request #398 from googleson78/extensionality-typo Fix typo: extentionality -> extensionality | 15 May 2019, 08:25:13 UTC |
| cc674cf | Ranjit Jhala | 14 May 2019, 02:15:17 UTC | add subable instance for Horn.Pred | 14 May 2019, 02:15:17 UTC |
| 62bcb96 | Ranjit Jhala | 14 May 2019, 02:12:29 UTC | add subable instance for Horn.Pred | 14 May 2019, 02:12:29 UTC |
| b051e64 | Ranjit Jhala | 10 May 2019, 05:05:54 UTC | L3 implemented; next: test! | 10 May 2019, 05:05:54 UTC |
| 79d55fe | Georgi Lyubenov | 09 May 2019, 07:48:16 UTC | Fix typo: extentionality -> extensionality | 09 May 2019, 07:49:02 UTC |
| f858a49 | Ranjit Jhala | 08 May 2019, 18:27:32 UTC | remove bogus Eq constraint | 08 May 2019, 18:27:32 UTC |
| 042da8a | Ranjit Jhala | 08 May 2019, 18:23:08 UTC | Merge pull request #397 from ucsd-progsys/horn-poly Make the horn solver "polymorphic" in the constraint label | 08 May 2019, 18:23:08 UTC |
| 0b2b364 | Ranjit Jhala | 08 May 2019, 18:15:02 UTC | require top-level sigs | 08 May 2019, 18:15:02 UTC |
| b8fa582 | Ranjit Jhala | 08 May 2019, 18:10:31 UTC | require top-level sigs | 08 May 2019, 18:10:31 UTC |
| 027b15b | Ranjit Jhala | 08 May 2019, 18:06:30 UTC | require top-level sigs | 08 May 2019, 18:06:30 UTC |
| 2895aae | Ranjit Jhala | 08 May 2019, 17:07:28 UTC | asd Merge branch 'develop' of github.com:ucsd-progsys/liquid-fixpoint into develop | 08 May 2019, 17:07:28 UTC |
| b5b2cd5 | Ranjit Jhala | 08 May 2019, 17:06:47 UTC | expose individual errors | 08 May 2019, 17:06:47 UTC |
| d41fc59 | Ranjit Jhala | 03 May 2019, 20:04:11 UTC | Merge pull request #396 from ucsd-progsys/horn-tx Horn Transformations | 03 May 2019, 20:04:11 UTC |
| 48ba4e8 | Anish Tondwalkar | 03 May 2019, 18:29:16 UTC | Merge remote-tracking branch 'origin/develop' into horn-tx | 03 May 2019, 18:29:16 UTC |
| 76fad45 | Anish Tondwalkar | 02 May 2019, 21:19:55 UTC | Don't (incorrectly) memoize pivars | 02 May 2019, 21:19:55 UTC |
| 4452548 | Anish Tondwalkar | 02 May 2019, 21:18:18 UTC | Unfuck doctests | 02 May 2019, 21:18:18 UTC |
| 5d2eb8f | Ranjit Jhala | 28 April 2019, 23:33:34 UTC | no, really | 28 April 2019, 23:33:34 UTC |
| d1f8af2 | Ranjit Jhala | 28 April 2019, 23:03:39 UTC | no, really | 28 April 2019, 23:03:39 UTC |
| 5b531cf | Ranjit Jhala | 28 April 2019, 22:54:46 UTC | make horn-solver generic | 28 April 2019, 22:54:46 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 |
