sort by:
Revision Author Date Message Commit Date
11f0b80 DONE with popl20 tests 11 July 2019, 03:24:10 UTC
16d8962 Collecting all the equalities 10 July 2019, 17:32:37 UTC
6d06405 Working on equality solver 10 July 2019, 08:26:02 UTC
3b569f8 Initial eGraph version 09 July 2019, 12:28:25 UTC
5c2db18 Properly capturing acyclic and cut kvars 09 July 2019, 05:14:39 UTC
d73b9b4 Making cLabel more robust 09 July 2019, 05:14:28 UTC
31fc379 Equality solving seems to work 09 July 2019, 01:47:24 UTC
2e8d84e Started writing qe 08 July 2019, 09:05:02 UTC
a5d57c5 WIP 08 July 2019, 07:54:07 UTC
843ee3e Flatten pisols (to improve debugging) 31 May 2019, 08:20:30 UTC
e06d483 hornify finalhorn as well 30 May 2019, 21:10:36 UTC
648fcc9 Merge pull request #400 from ucsd-progsys/horn-subst Subable instances for Horn constraints 25 May 2019, 04:31:12 UTC
0d1c66c remove tracing 24 May 2019, 08:28:49 UTC
7d6b858 use parens for kvar sort-params 24 May 2019, 07:49:06 UTC
ae9a010 asd 23 May 2019, 22:22:26 UTC
f146bba don't allow ueq on bool 22 May 2019, 12:48:12 UTC
a378948 don't allow ueq on bool 22 May 2019, 12:41:46 UTC
9f7060c don't allow ueq on bool 22 May 2019, 12:32:01 UTC
362a902 twiddle 20 May 2019, 21:29:43 UTC
782dbd0 Merge pull request #398 from googleson78/extensionality-typo Fix typo: extentionality -> extensionality 15 May 2019, 08:25:13 UTC
cc674cf add subable instance for Horn.Pred 14 May 2019, 02:15:17 UTC
62bcb96 add subable instance for Horn.Pred 14 May 2019, 02:12:29 UTC
b051e64 L3 implemented; next: test! 10 May 2019, 05:05:54 UTC
79d55fe Fix typo: extentionality -> extensionality 09 May 2019, 07:49:02 UTC
f858a49 remove bogus Eq constraint 08 May 2019, 18:27:32 UTC
042da8a 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 require top-level sigs 08 May 2019, 18:15:02 UTC
b8fa582 require top-level sigs 08 May 2019, 18:10:31 UTC
027b15b require top-level sigs 08 May 2019, 18:06:30 UTC
2895aae asd Merge branch 'develop' of github.com:ucsd-progsys/liquid-fixpoint into develop 08 May 2019, 17:07:28 UTC
b5b2cd5 expose individual errors 08 May 2019, 17:06:47 UTC
d41fc59 Merge pull request #396 from ucsd-progsys/horn-tx Horn Transformations 03 May 2019, 20:04:11 UTC
48ba4e8 Merge remote-tracking branch 'origin/develop' into horn-tx 03 May 2019, 18:29:16 UTC
76fad45 Don't (incorrectly) memoize pivars 02 May 2019, 21:19:55 UTC
4452548 Unfuck doctests 02 May 2019, 21:18:18 UTC
5d2eb8f no, really 28 April 2019, 23:33:34 UTC
d1f8af2 no, really 28 April 2019, 23:03:39 UTC
5b531cf make horn-solver generic 28 April 2019, 22:54:46 UTC
097f354 Merge remote-tracking branch 'origin/develop' into horn-tx 27 April 2019, 21:01:51 UTC
06cff38 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 Merge pull request #394 from ucsd-progsys/ple2 Encode coercions as uninterpreted functions 12 April 2019, 18:59:25 UTC
130f3a9 done: coerce-apply, see ucsd-progsys/liquidhaskell#1424 11 April 2019, 19:50:01 UTC
876cd13 first constraint OK 11 April 2019, 18:12:14 UTC
93b8d45 Merge pull request #393 from peti/develop drop redundant dependencies from Cabal file 28 March 2019, 10:06:09 UTC
d325af5 liquid-fixpoint.cabal: pretty-print the file with stylish-cabal 28 March 2019, 09:15:27 UTC
17e752c liquid-fixpoint.cabal: drop redundant dependencies & simplify the file 28 March 2019, 09:13:10 UTC
42c027a Merge pull request #391 from ucsd-progsys/ghc-863 Update to GHC 8.6.4 23 March 2019, 17:03:33 UTC
ac3e9dd bump cabal version 19 March 2019, 03:42:32 UTC
a255d28 bump cabal version 18 March 2019, 23:14:25 UTC
abb3595 horn pi elim: qe in side condition 18 March 2019, 22:40:56 UTC
9ab4954 builds against 863 17 March 2019, 19:21:09 UTC
04cf502 drop useless quantifiers 26 February 2019, 00:20:39 UTC
13c01e3 transformations inside solve, NOT solveHorn 24 February 2019, 08:00:21 UTC
549322c Flatten (simplify) constraints before solving 24 February 2019, 05:30:17 UTC
b3f6430 Add support for constants and distincts to Horn 23 February 2019, 21:45:35 UTC
546ca77 Finished horn side conditions. needs refactoring 19 February 2019, 19:51:49 UTC
4dc2659 minor cleanup 18 February 2019, 22:05:03 UTC
28caf05 DONE: QE. Next: checkSides 18 February 2019, 10:30:05 UTC
542ffcc QE works on ebind-03 (ad-hoc) 18 February 2019, 09:49:54 UTC
80ce62f 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 checking in QE before starting over on it 17 February 2019, 12:42:53 UTC
cc01aa8 futzing around with QE 17 February 2019, 10:28:06 UTC
2fdaa49 elimKs: gracefully handle cycles 17 February 2019, 09:33:25 UTC
7f0a9eb 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 Add command line for --eliminate=existentials (only works with the Horn format) 16 February 2019, 22:14:42 UTC
fdc9f6a 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 Merge pull request #390 from ucsd-progsys/missing-sort Two bug fixes 13 February 2019, 05:18:55 UTC
d370604 TODO: add mossaka.fq test 13 February 2019, 04:58:34 UTC
13a0a7e only eval partial appls if Ok 13 February 2019, 03:20:22 UTC
7ae5906 only eval partial appls if Ok 13 February 2019, 03:13:49 UTC
84dab94 only eval partial appls if Ok 13 February 2019, 01:47:37 UTC
aa8ecc6 banging head against mossaka bug 13 February 2019, 00:02:39 UTC
6d17b8a add MJ test 12 February 2019, 19:24:00 UTC
60df75e make poke use pivars instead of reusing the ebind 12 February 2019, 09:40:34 UTC
4605e7f asd 12 February 2019, 07:44:37 UTC
5096722 temp checkin: missing sort 12 February 2019, 07:14:33 UTC
62e9c57 don't generate equations for data-constructors 12 February 2019, 04:04:53 UTC
43076c4 aha, add binders for ... binders 12 February 2019, 00:22:18 UTC
a7becfd Add tests from ICFP paper for eliminate=horn 11 February 2019, 18:55:49 UTC
5d3d171 Pretty Print constraints 11 February 2019, 18:55:49 UTC
e9df778 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 implement uniq pass on horn 11 February 2019, 18:55:49 UTC
eec773f Merge pull request #389 from ucsd-progsys/T1371 Update no-eval-ite for mutrec functions 10 February 2019, 02:14:36 UTC
7870d9e update no-eval-ite for mutrec functions 10 February 2019, 01:30:04 UTC
6fb5657 Merge pull request #388 from ucsd-progsys/T1371 T1371 10 February 2019, 00:06:44 UTC
f60841d next: fix StlcBug and T1371 09 February 2019, 23:03:00 UTC
e5737f5 don't eval recursive-funs under unknown guard 09 February 2019, 22:37:02 UTC
27ad9b6 Disable tracpp 08 February 2019, 23:23:03 UTC
7bdce09 temp checkin 08 February 2019, 20:05:15 UTC
1411b21 about to add 'stack' to eval 08 February 2019, 17:04:50 UTC
8c10920 Fixed substitutions in Horn/elim 08 February 2019, 12:30:02 UTC
54797c1 Start debugging Horn.elim 07 February 2019, 23:57:23 UTC
0ac8aec don't eval under unknown guard. sigh. 07 February 2019, 23:31:37 UTC
d4ca29f don't eval under unknown guard. sigh. 07 February 2019, 22:03:47 UTC
50ad58d merged in reflect-string 07 February 2019, 21:50:18 UTC
78ac477 yuck 07 February 2019, 21:32:36 UTC
683e85c add minimal test 07 February 2019, 21:26:27 UTC
983264c add minimal test 07 February 2019, 20:46:38 UTC
a91c833 Merge pull request #385 from ucsd-progsys/T1409 T1409 07 February 2019, 17:34:30 UTC
9f4df57 fixes liquidhaskell/#1409 07 February 2019, 14:31:58 UTC
back to top