We are hiring ! See our job offers.

sort by:
Revision Author Date Message Commit Date
163b815 Fixing uniq 16 November 2019, 17:37:16 UTC
d4c6f6f Fix bug involving true PiVars 08 November 2019, 23:31:48 UTC
1fc8b1d Fixed bug when kvar appeared in a PAnd 08 November 2019, 00:00:02 UTC
fd8b69c Debugging reformatting 07 November 2019, 23:59:33 UTC
235aabb Better error message on unconstrained pi variable 01 November 2019, 18:08:00 UTC
ae9f5b9 bump iterations in Transformations.hs 20 October 2019, 06:45:47 UTC
eba2590 fixed warnings 20 October 2019, 06:45:26 UTC
e025d35 turn off tracing in Transfomrations 17 October 2019, 00:19:16 UTC
3b31634 Fixed pi defining constraints 27 September 2019, 16:00:49 UTC
6ec8bb1 Temp 27 September 2019, 15:30:46 UTC
381b2ab WIP MERGE 26 September 2019, 22:33:45 UTC
f5feb84 rewrite scope 26 September 2019, 22:11:28 UTC
478762f temp 20 September 2019, 22:12:54 UTC
3d0e94e Update config.yml 19 August 2019, 15:27:42 UTC
e782f4a update lts 19 August 2019, 08:43:17 UTC
fe737ea Merge branch 'develop' into new-horntx 19 August 2019, 08:29:25 UTC
bab728a rewrite scope again, fix warnings 20 July 2019, 22:20:48 UTC
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
b3fbc62 name SortSubst 23 June 2019, 23:55:59 UTC
60e773c Merge pull request #406 from ucsd-progsys/horn-monoid Horn Monoid 20 June 2019, 18:13:42 UTC
907cf99 next L5 18 June 2019, 18:41:01 UTC
4f0f101 asd Merge branch 'develop' into horn-monoid 18 June 2019, 16:50:20 UTC
90639c5 Merge pull request #405 from zgrannan/tuples Allow Tuple Syntax in Refinements 14 June 2019, 12:18:57 UTC
1ea4357 Initial tuple implementation, add tests 13 June 2019, 07:02:17 UTC
d5ec36a Merge pull request #403 from ucsd-progsys/synonym-set Synonym set 12 June 2019, 06:00:21 UTC
f785084 asd 11 June 2019, 18:00:51 UTC
8b0f947 Merge branch 'develop' of https://github.com/ucsd-progsys/liquid-fixpoint into synonym-set 11 June 2019, 08:56:05 UTC
ef3d52b Merge pull request #404 from ucsd-progsys/kill-extensionality Remove some used lambda features 07 June 2019, 19:14:21 UTC
73a1fba remove more dead code 07 June 2019, 12:51:57 UTC
2805b9a lambda is on by default 07 June 2019, 12:21:46 UTC
384d306 kill normalize too 07 June 2019, 12:13:41 UTC
368b0c1 kill alphas 07 June 2019, 12:06:42 UTC
42ac2d8 kill extensionality 07 June 2019, 11:35:33 UTC
2d880d1 Merge pull request #402 from googleson78/synonym-set Synonym set 04 June 2019, 14:48:25 UTC
c6555dd Document LSet naming 04 June 2019, 12:55:13 UTC
f91eb65 Rename LH Set to work around Z3's Set 04 June 2019, 12:49:58 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
back to top