e025d35 | Anish Tondwalkar | 17 October 2019, 00:19:16 UTC | turn off tracing in Transfomrations | 17 October 2019, 00:19:16 UTC |
3b31634 | mkolosick | 27 September 2019, 16:00:49 UTC | Fixed pi defining constraints | 27 September 2019, 16:00:49 UTC |
6ec8bb1 | mkolosick | 27 September 2019, 14:54:55 UTC | Temp | 27 September 2019, 15:30:46 UTC |
381b2ab | Anish Tondwalkar | 26 September 2019, 22:33:45 UTC | WIP MERGE | 26 September 2019, 22:33:45 UTC |
f5feb84 | Anish Tondwalkar | 26 September 2019, 22:11:28 UTC | rewrite scope | 26 September 2019, 22:11:28 UTC |
478762f | mkolosick | 20 September 2019, 22:12:54 UTC | temp | 20 September 2019, 22:12:54 UTC |
3d0e94e | Anish Tondwalkar | 19 August 2019, 15:27:42 UTC | Update config.yml | 19 August 2019, 15:27:42 UTC |
e782f4a | Anish Tondwalkar | 19 August 2019, 08:43:17 UTC | update lts | 19 August 2019, 08:43:17 UTC |
fe737ea | Anish Tondwalkar | 19 August 2019, 08:29:25 UTC | Merge branch 'develop' into new-horntx | 19 August 2019, 08:29:25 UTC |
bab728a | Anish Tondwalkar | 20 July 2019, 22:20:48 UTC | rewrite scope again, fix warnings | 20 July 2019, 22:20:48 UTC |
11f0b80 | Anish Tondwalkar | 11 July 2019, 03:24:10 UTC | DONE with popl20 tests | 11 July 2019, 03:24:10 UTC |
16d8962 | mkolosick | 10 July 2019, 17:32:37 UTC | Collecting all the equalities | 10 July 2019, 17:32:37 UTC |
6d06405 | mkolosick | 10 July 2019, 08:26:02 UTC | Working on equality solver | 10 July 2019, 08:26:02 UTC |
3b569f8 | mkolosick | 09 July 2019, 12:28:25 UTC | Initial eGraph version | 09 July 2019, 12:28:25 UTC |
5c2db18 | mkolosick | 09 July 2019, 05:14:39 UTC | Properly capturing acyclic and cut kvars | 09 July 2019, 05:14:39 UTC |
d73b9b4 | mkolosick | 09 July 2019, 05:14:28 UTC | Making cLabel more robust | 09 July 2019, 05:14:28 UTC |
31fc379 | mkolosick | 09 July 2019, 01:47:24 UTC | Equality solving seems to work | 09 July 2019, 01:47:24 UTC |
2e8d84e | mkolosick | 08 July 2019, 09:05:02 UTC | Started writing qe | 08 July 2019, 09:05:02 UTC |
a5d57c5 | mkolosick | 08 July 2019, 07:46:00 UTC | WIP | 08 July 2019, 07:54:07 UTC |
b3fbc62 | Ranjit Jhala | 23 June 2019, 23:55:59 UTC | name SortSubst | 23 June 2019, 23:55:59 UTC |
60e773c | Ranjit Jhala | 20 June 2019, 18:13:42 UTC | Merge pull request #406 from ucsd-progsys/horn-monoid Horn Monoid | 20 June 2019, 18:13:42 UTC |
907cf99 | Ranjit Jhala | 18 June 2019, 18:41:01 UTC | next L5 | 18 June 2019, 18:41:01 UTC |
4f0f101 | Ranjit Jhala | 18 June 2019, 16:50:20 UTC | asd Merge branch 'develop' into horn-monoid | 18 June 2019, 16:50:20 UTC |
90639c5 | Niki Vazou | 14 June 2019, 12:18:57 UTC | Merge pull request #405 from zgrannan/tuples Allow Tuple Syntax in Refinements | 14 June 2019, 12:18:57 UTC |
1ea4357 | Zack Grannan | 13 June 2019, 05:32:14 UTC | Initial tuple implementation, add tests | 13 June 2019, 07:02:17 UTC |
d5ec36a | Niki Vazou | 12 June 2019, 06:00:21 UTC | Merge pull request #403 from ucsd-progsys/synonym-set Synonym set | 12 June 2019, 06:00:21 UTC |
f785084 | Ranjit Jhala | 11 June 2019, 18:00:51 UTC | asd | 11 June 2019, 18:00:51 UTC |
8b0f947 | nikivazou | 11 June 2019, 08:56:05 UTC | Merge branch 'develop' of https://github.com/ucsd-progsys/liquid-fixpoint into synonym-set | 11 June 2019, 08:56:05 UTC |
ef3d52b | Niki Vazou | 07 June 2019, 19:14:21 UTC | Merge pull request #404 from ucsd-progsys/kill-extensionality Remove some used lambda features | 07 June 2019, 19:14:21 UTC |
73a1fba | nikivazou | 07 June 2019, 12:51:57 UTC | remove more dead code | 07 June 2019, 12:51:57 UTC |
2805b9a | nikivazou | 07 June 2019, 12:21:46 UTC | lambda is on by default | 07 June 2019, 12:21:46 UTC |
384d306 | nikivazou | 07 June 2019, 12:13:41 UTC | kill normalize too | 07 June 2019, 12:13:41 UTC |
368b0c1 | nikivazou | 07 June 2019, 12:06:42 UTC | kill alphas | 07 June 2019, 12:06:42 UTC |
42ac2d8 | nikivazou | 07 June 2019, 11:35:33 UTC | kill extensionality | 07 June 2019, 11:35:33 UTC |
2d880d1 | Niki Vazou | 04 June 2019, 14:48:25 UTC | Merge pull request #402 from googleson78/synonym-set Synonym set | 04 June 2019, 14:48:25 UTC |
c6555dd | Georgi Lyubenov | 04 June 2019, 12:55:03 UTC | Document LSet naming | 04 June 2019, 12:55:13 UTC |
f91eb65 | Georgi Lyubenov | 04 June 2019, 12:49:58 UTC | Rename LH Set to work around Z3's Set | 04 June 2019, 12:49:58 UTC |
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 |