00:01:27 [[1CP=1ICL]] https://esolangs.org/w/index.php?diff=77019&oldid=77018 * Heavpoot * (-138) 00:01:56 [[Talk:1CP=1ICL]] N https://esolangs.org/w/index.php?oldid=77020 * Heavpoot * (+108) Created page with "dont be soundofspouting ~~~~" 00:07:09 -!- adu has joined. 00:16:40 -!- t20kdc has quit (Remote host closed the connection). 01:32:45 [[Talk:1CP=1ICL]] M https://esolangs.org/w/index.php?diff=77021&oldid=77020 * SoundOfScripting * (+124) * do 01:41:56 [[1CP=1ICL]] https://esolangs.org/w/index.php?diff=77022&oldid=77019 * Heavpoot * (+150) 01:43:02 [[1CP=1ICL]] https://esolangs.org/w/index.php?diff=77023&oldid=77022 * Heavpoot * (+3) 02:23:51 -!- Heavpoot has quit (Remote host closed the connection). 02:40:11 -!- adu has quit (Quit: adu). 02:42:15 Generic data structures in Zig are just compile-time functions, and I think my brain broke 02:58:20 -!- adu has joined. 03:18:32 -!- kkd has joined. 03:38:45 -!- tromp has joined. 03:43:33 -!- tromp has quit (Ping timeout: 272 seconds). 04:36:09 jix: whoa, what's going on in SATland? 04:37:19 shachaf: huh? 04:37:27 I don't remember what I last said about my solver. I added (very simple) clause deletion, and Luby restarts, and it actually became reasonably fast on some inputs. 04:38:06 But it sounds like your solver is way fancier and also world-famous now. 04:39:03 it's not famous at all, it's good enough to be practically useful but it's not state of the art stuff 04:39:27 but a somewhat well known rust person started using it (for some not (yet?) public project) 04:40:05 and that person seems to have quite a few followers on github, so now the traffic on my project suddenly increased 04:42:09 Aha. 04:44:12 I should get back to working on it. 04:44:23 so do I... 04:44:35 but I want to rewrite half of it... again 04:44:37 It got more fun when I stopped using random instances and started using real instances. 04:44:46 -!- Lord_of_Life_ has joined. 04:44:51 I should pick a good representative set of instances to be testing on. 04:45:37 yeah first that makes it more fun.... but then you realize you need a good way to benchmark stuff and that's another rabbit hole 04:45:54 Yes, definitely trickier than I thought. 04:46:08 -!- Lord_of_Life has quit (Ping timeout: 265 seconds). 04:46:08 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 04:49:20 What's it being used for? 04:50:04 Or is the project unknown? 04:50:05 I wonder whether I should improve my SAT solver or try figuring out how SMT solvers work. 04:52:57 unknown, but he commented on an open issue related to timeouts and mentioned that he added cancellation from another thread and asked whether I'd be interested in merging something like that 04:53:34 where he mentioned that he's using it in an interactive setting... and IIRC he recently started working on games, so that'd be my guess 04:53:41 Aha, the Io person. 04:53:56 My friend was using a SAT solver to design levels in a puzzle game. 04:54:04 Io? 04:54:17 http://canonical.org/~kragen/raph-io.html 04:56:06 jix: For my own solver, instead of a timeout, I was thinking of adding a more iterator-like API for the solver loop. 04:56:42 Well, I guess for a SAT solver it's pretty simple, if it looks like a classic CDCL solver. 04:57:49 yeah I also thought about that, (for the same reason, it's somewhat natural given the CDCL loop), but I do want to offer convenience APIs for a) callback based termination to match the IPASIR api and b) cancellation from a different thread using an atomic bool as flag and c) timeouts without requiring a second thread 04:58:30 The loop looks like while (1) { unit_propagation(); if (conflict) { if (level == 0) return false; backtrack(); } else { if (all_assigned) return true; guess(); } }, right? 04:58:47 -!- Arcorann__ has joined. 04:58:49 Where most time is spent in unit propagation. 04:59:05 Yes, makes sense that you've had the same thought. 04:59:29 What puzzle game levels are designing by SAT solver? 04:59:30 well there are also restarts but roughly like that 04:59:31 Convenience APIs seem good to provide, but as the core API I think something like this is much nicer. 04:59:52 I was already getting into more detail than I meant to. 05:00:32 Really I should have said while (1) { /* something that takes a relatively long time */ }. I was just trying to remember how it worked. 05:01:05 -!- glowcoil_ has joined. 05:01:12 more like while (1) { /* something that takes a short amount of time, but you need to do it many, many, many times */ } 05:01:13 zzo38: It's still a secret game unfortunately. 05:01:34 -!- glowcoil has quit (Ping timeout: 240 seconds). 05:01:34 -!- Arcorann_ has quit (Read error: Connection reset by peer). 05:01:34 -!- ocharles has quit (Ping timeout: 240 seconds). 05:01:35 -!- olsner has quit (Ping timeout: 240 seconds). 05:01:35 -!- sftp has quit (Ping timeout: 240 seconds). 05:01:35 -!- glowcoil_ has changed nick to glowcoil. 05:01:42 I guess the thing I was wondering was whether having an API boundary there would have a performance impact. 05:01:51 But I doubt it. 05:01:57 -!- ocharles has joined. 05:02:35 so returning after each conflict should be perfectly safe (in my solver and IIRC many others)finding a conflict is a sub-loop) 05:02:41 -!- sftp has joined. 05:03:05 returning each time after running unit propagation to completion, I'm not quite sure 05:03:33 Sure, unit propagation + handling the conflict sort of goes together. 05:03:59 Though I guess it doesn't have to, you can just save your state. 05:04:32 yeah but I meant if you need multiple guesses to find a conflict, returning inbetween might not be a good idea performance wise 05:04:57 (if returning implies you're going to check termination criteria and potentially other stuff that could slow down things) 05:05:29 but I haven't tested that at all, I just know you're pretty safe doing that after a conflict given all the other stuff that happens anyway for a conflict 05:06:52 whoa, I just looked up IPASIR, I didn't know about this at all. 05:08:05 I always end up needing functionallity outside of that API, sometimes supported by solver specific APIs... but often enough not even that, even though it wouldn't be too hard to add it 05:08:37 It's too bad it's callback-based. Callback APIs aren't fun when you can avoid them. 05:08:49 And you should certainly be able to, for something like this. 05:09:08 it's inteded to be easy to add to existing solvers, and callbacks make that easier 05:09:24 Fair enough. 05:09:46 for a lot of uses you don't even need any of the callback APIs though 05:10:21 Just being able to add new clauses without deleting the clause database is presumably most of the incrementality people need. 05:10:39 yeah that and solving under assumptions 05:11:14 Hmm, how do assumptions work? I guess that just means adding things to the trail? 05:11:47 yeah it's exactly just that, you fix a prefix on the trail and if you'd backtrack beyond that you return unsat (under assumptions) 05:12:13 -!- olsner has joined. 05:12:20 I was briefly wondering whether you'd learn wrong clauses that way but of course you wouldn't. 05:12:51 from the conflict analysis you do to detect that you'd backtrack beyond that you also get a subset of assumptions causing the conflict for free (which is also part of the IPASIR api) 05:13:27 Oh, that's nice. 05:13:47 [[User talk:Challenger5]] https://esolangs.org/w/index.php?diff=77024&oldid=76991 * Challenger5 * (+107) 05:14:22 [[User:Challenger5]] https://esolangs.org/w/index.php?diff=77025&oldid=76950 * Challenger5 * (+16) 05:14:50 Do you know if SMT solvers need more of an API than this? 05:15:12 it depends AFAIK 05:15:38 Not knowing much about what is SMT solvers, I don't know really 05:15:50 [[Aubergine]] https://esolangs.org/w/index.php?diff=77026&oldid=74883 * Challenger5 * (+95) 05:16:20 you don't need more than that for CDCL(T) or for bitblasting AFAICT 05:16:58 but if you want to do eager theory propagation (not sure if that's an established term) you need a way to hook into unit propagation 05:17:13 I have no idea how much that is done or if it is important at all 05:18:16 Just a few minutes ago I found and corrected a bug in TeXnicard involving division by zero when the total available vertical space is rigid, resulting in alternating lines of text being displayed and hidden. 05:39:35 -!- tromp has joined. 05:44:42 -!- tromp has quit (Ping timeout: 260 seconds). 05:57:10 zzo38: Do you like SAT solvers? 06:01:11 shachaf: I do not know much about SAT solvers. 06:01:27 (If I knew, maybe I would be able to answer your other questions too, but I don't know.) 06:01:37 Do you like graph coloring solvers? 06:02:16 they are more logic solver systems than one might expect and they are competing against themselves quite regularly 06:05:13 Hmm, maybe I should actually learn about integer programming solvers. I hear they're pretty good.. 06:05:16 s/.$// 06:05:38 Plus I don't even really know about linear programming. 06:05:59 a friend of mine writes a mip solver in his spare time to optimize his factorio world 06:06:25 linear programming is not that hard, really 06:07:50 shachaf: as you already know how SAT solvers work, learning about MIP will make you annoyed that SAT solvers are bad at what MIP solvers are good at and that MIP solvers are bad at what SAT solvers are good at (well, at least it does that for me) 06:07:55 integer programms make it quite a bit harder 06:08:32 and apparently it's difficult enough to combine them in a way that gets the advantages of both 06:08:47 iirc linear programms are in P 06:08:55 jix: That was my impression. Well, I really only know one direction, in seeing some problems that MIP solvers are good at and SAT solvers are bad at. 06:09:05 But I heard it went both ways. 06:09:32 There's a lot more industrial use of MIP, I think? 06:09:58 yeah I think so 06:10:13 even for problems where SAT or SMT solvers would be better 06:10:30 that's not that surprising, SAT solvers only decide, MIP solvers optimize 06:11:10 myname: that's not really a distinction that matters though, if you can do one you can do the other, in theory as well as in practice 06:11:31 now it might be that it works in theory but is too slow in practice, but with incremental SAT solvers optimizing is also fast in practice 06:11:33 jix: well, at additional cost, yeah 06:12:34 and you have to state your problem in such a way that you can make good guesses about what change in the corresponding sat problem 06:13:18 Not having seen graph coloring solvers, I don't really know. But at least I can understand a bit of what is meant, I suppose. How difficult are they to solve, though? 06:13:49 graph coloring is NP complete 06:13:59 so i guess it's about as hard as SAT solvers 06:14:54 O, OK. 06:15:41 to be fair, a lot more work has been put into sat sovlers, I think, and polynomial time is... well theoretically not that bad but in practice it can get pretty bad 06:17:31 Well, yes, depending on the algorithm and how much data, it can be, considering, there are many kind of polynomials, some of which are big. 06:17:33 yeah, we had a lecture on algorithms to solve euclidean tsp that aren't really worth attempting with real data sets, if you could just brute-force 06:21:27 -!- adu has quit (Quit: adu). 07:01:41 -!- tromp has joined. 07:04:12 Just now I found the new documentation about the schema table for SQLite, and about the new name "sqlite_schema" instead of "sqlite_master". I knew about this before from the Fossil timeline. I am glad that "For historical reasons, callbacks from the sqlite3_set_authorizer() interface always refer to the schema table using names (1) or (3)" because that is the part that I was concerned about. 07:04:29 So, good, now my concern has been considered, so it is OK now. 07:16:53 How should I choose which learnt clauses to delete? 07:16:59 Right now I just delete the longest ones. 07:17:11 Also, how should I store watch lists? 07:32:41 Unfortunately, I don't know. Hopefully, we can learn which way is good. 07:49:57 shachaf: the classic approach (used by minisat and probably solvers before it) uses clause activities, glucose added LBDs (aka as clause glues or glue levels) as a metric for that, chanseok oh's solvers added a strategy that partitions learned clauses into 3 tiers and uses activities and LBDs and whether they've been part of a conflict recently (IIRC it's been a time) and that's the state of the 07:49:59 art unless something changed in the past 1.5 years 08:10:26 -!- hendursa1 has joined. 08:12:23 -!- hendursaga has quit (Ping timeout: 240 seconds). 08:38:26 [[,,,]] https://esolangs.org/w/index.php?diff=77027&oldid=77004 * SunnyMoon * (-46) I am going to talk about this later. 08:39:36 [[,,,]] M https://esolangs.org/w/index.php?diff=77028&oldid=77027 * SunnyMoon * (-83) And this too. 09:10:43 -!- b_jonas has quit (Quit: leaving). 09:12:25 -!- Sgeo_ has quit (Read error: Connection reset by peer). 09:18:25 -!- imode has quit (Ping timeout: 240 seconds). 09:30:07 [[,,,]] https://esolangs.org/w/index.php?diff=77029&oldid=77028 * SunnyMoon * (+490) Introducing IO! 09:52:33 -!- S_Gautam has joined. 10:15:20 -!- wib_jonas has joined. 10:16:08 spruit: what does "non-monadic" mean in that context? 10:26:32 -!- hendursa1 has quit (Remote host closed the connection). 10:26:59 -!- hendursaga has joined. 10:31:49 wth just how many ways can you spell fairy in English? "fairy, fairie, faerie, færie, faery, fae, fey, fay"; plus any of those suffixed with " folk" and "fair folk" apparently 10:32:09 they're worse than djinns 10:38:56 [[110010000100110110010]] https://esolangs.org/w/index.php?diff=77030&oldid=74384 * Stasoid * (+4) 11:19:03 [[,,,]] https://esolangs.org/w/index.php?diff=77031&oldid=77029 * SunnyMoon * (+720) Introducing DATA TYPES! 12:02:17 -!- kritixilithos has joined. 12:09:41 -!- hendursaga has quit (Quit: hendursaga). 12:09:57 -!- hendursaga has joined. 12:24:23 -!- kritixilithos has quit (Ping timeout: 240 seconds). 12:32:08 -!- S_Gautam has quit (Quit: Connection closed for inactivity). 12:51:19 -!- kritixilithos has joined. 12:59:40 -!- Lord_of_Life has quit (Read error: Connection reset by peer). 13:00:09 -!- Lord_of_Life has joined. 13:10:19 [[,,,]] https://esolangs.org/w/index.php?diff=77032&oldid=77031 * SunnyMoon * (+731) Introducing CONTROL FLOW! 13:11:32 [[,,,]] M https://esolangs.org/w/index.php?diff=77033&oldid=77032 * SunnyMoon * (+0) Emphasizing 'if'. 13:14:06 [[,,,]] M https://esolangs.org/w/index.php?diff=77034&oldid=77033 * SunnyMoon * (+95) Introducing I! 13:16:43 -!- kritixilithos has quit (Ping timeout: 240 seconds). 13:59:31 -!- kritixilithos has joined. 14:24:38 [[Hello world program in esoteric languages]] M https://esolangs.org/w/index.php?diff=77035&oldid=76960 * Abyxlrz * (+76) 14:29:35 [[Truth-machine]] M https://esolangs.org/w/index.php?diff=77036&oldid=76961 * Abyxlrz * (+101) 15:01:40 -!- adu has joined. 15:04:43 -!- kritixilithos has quit (Ping timeout: 240 seconds). 15:22:17 `pbflist https://pbfcomics.com/comics/obscenery/ 15:22:19 pbflist https://pbfcomics.com/comics/obscenery/: shachaf Sgeo quintopia ion b_jonas Cale 15:22:50 [[,,,]] https://esolangs.org/w/index.php?diff=77037&oldid=77034 * SunnyMoon * (+666) Introducing PROGRAMS! 15:23:51 [[Talk:Modulous]] M https://esolangs.org/w/index.php?diff=77038&oldid=76980 * Abyxlrz * (+150) 15:32:01 [[,,,]] https://esolangs.org/w/index.php?diff=77039&oldid=77037 * SunnyMoon * (+181) Introducing EXTERNAL RESOURCES! 15:46:05 -!- kritixilithos has joined. 15:50:47 -!- wib_jonas has quit (Quit: Connection closed). 15:52:58 [[,,,]] https://esolangs.org/w/index.php?diff=77040&oldid=77039 * SunnyMoon * (+23) Introducing REDIRECTS! 15:53:24 [[,,,]] https://esolangs.org/w/index.php?diff=77041&oldid=77040 * SunnyMoon * (-23) Wait what? 15:56:03 [[Commata]] N https://esolangs.org/w/index.php?oldid=77042 * SunnyMoon * (+17) Redirection fora golfing language. 15:57:39 [[,,,]] M https://esolangs.org/w/index.php?diff=77043&oldid=77041 * SunnyMoon * (+0) Capitalization: The beginnings 15:58:25 [[,,,]] M https://esolangs.org/w/index.php?diff=77044&oldid=77043 * SunnyMoon * (+4) Link to the esolang page 16:01:00 [[,,,]] M https://esolangs.org/w/index.php?diff=77045&oldid=77044 * SunnyMoon * (+133) A bit more clarification. 16:01:06 -!- kritixilithos has quit (Remote host closed the connection). 16:01:27 -!- kritixilithos has joined. 16:01:28 [[,,,]] M https://esolangs.org/w/index.php?diff=77046&oldid=77045 * SunnyMoon * (+9) Grammar Fix 16:03:20 [[,,,]] M https://esolangs.org/w/index.php?diff=77047&oldid=77046 * SunnyMoon * (+45) Space is a nop! 16:04:45 [[,,,]] M https://esolangs.org/w/index.php?diff=77048&oldid=77047 * SunnyMoon * (+0) Actually, these 'nops' do have a purpose. 16:06:05 -!- Arcorann__ has quit (Read error: Connection reset by peer). 16:10:35 [[Language list]] https://esolangs.org/w/index.php?diff=77049&oldid=77008 * SunnyMoon * (+10) ,,, Joins the battle! 16:18:38 [[,,,]] M https://esolangs.org/w/index.php?diff=77050&oldid=77048 * SunnyMoon * (+57) Bit more ClaRiFiCaTion. 16:19:40 [[,,,]] M https://esolangs.org/w/index.php?diff=77051&oldid=77050 * SunnyMoon * (-83) AHH MY FOCUS 16:21:36 [[,,,]] M https://esolangs.org/w/index.php?diff=77052&oldid=77051 * SunnyMoon * (+11) ClArIfIcAtIoN 16:22:15 [[,,,]] M https://esolangs.org/w/index.php?diff=77053&oldid=77052 * SunnyMoon * (+0) ... 16:23:00 [[,,,]] M https://esolangs.org/w/index.php?diff=77054&oldid=77053 * SunnyMoon * (+0) .:.:. 16:46:33 -!- Lord_of_Life_ has joined. 16:47:39 -!- Lord_of_Life has quit (Ping timeout: 258 seconds). 16:49:23 -!- Lord_of_Life_ has changed nick to Lord_of_Life. 17:10:27 -!- arseniiv has joined. 17:22:58 -!- b_jonas has joined. 18:02:43 -!- kritixilithos has quit (Ping timeout: 240 seconds). 18:06:01 -!- kritixilithos has joined. 18:11:38 -!- Sgeo has joined. 18:17:21 -!- adu has quit (Quit: adu). 18:21:25 -!- adu has joined. 18:32:19 -!- kritixilithos has quit (Quit: quit). 18:41:42 -!- adu has quit (Quit: adu). 18:45:00 [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77055&oldid=76971 * SunnyMoon * (+143) Something more... 18:49:54 [[QuineLang]] M https://esolangs.org/w/index.php?diff=77056&oldid=69523 * SunnyMoon * (+8) When creating articles, it is good to write them in 3rd-person perspective. :) 18:54:32 [[User:SunnyMoon]] https://esolangs.org/w/index.php?diff=77057&oldid=77055 * SunnyMoon * (-175) I guess this sentence is not needed. 18:55:45 [[1CP=1ICL]] https://esolangs.org/w/index.php?diff=77058&oldid=77023 * Osmarks * (+199) 18:58:30 [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77059&oldid=77057 * SunnyMoon * (+152) A bit more stuff about esolangs. 18:59:10 [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77060&oldid=77059 * SunnyMoon * (-10) Aw man 19:00:22 [[1CP=1ICL]] https://esolangs.org/w/index.php?diff=77061&oldid=77058 * Osmarks * (+79) 19:01:45 [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77062&oldid=77060 * SunnyMoon * (+48) More... MORE! 19:02:37 [[User:SunnyMoon]] M https://esolangs.org/w/index.php?diff=77063&oldid=77062 * SunnyMoon * (+1) OH NOES 19:07:45 -!- imode has joined. 19:14:20 another homepage where if the browser window isn't very wide, then essential links are hidden. I was searching for how to log in. 19:17:20 [[Hello world program in esoteric languages]] https://esolangs.org/w/index.php?diff=77064&oldid=77035 * SunnyMoon * (+30) ,,, 19:24:34 -!- arseniiv has quit (Ping timeout: 256 seconds). 19:24:36 b_jonas: Non-monadic in the sense that you don't use an explicit structure like the monad from Haskell? 19:26:41 spruit11: ok, though I don't understand how that would apply to a prime sieve 19:29:03 It's surprising that this is possible: https://tomas.rokicki.com/logic_puzzle.html 19:29:06 "You can use any number of 'and' and 'or' gates, with any number of inputs each, but only two 'not' gates. You must build a circuit that computes for inputs A, B, and C, the three separate values not A, not B, and not C." 19:30:23 huh, interesting 19:30:29 i will think about that 19:31:28 is it possible? i would assume it works with stuff similar two the variable switch without a temporary one 19:32:32 It is possible. 19:32:43 shachaf: hmm 19:33:14 I have a computer-found solution but I'm not sure I understand how it works entirely. 19:33:26 shachaf: let me think about that one 19:35:26 I know there's some easy description of functions that you can build from just & and | gates, IIRC think a function can be built that way iff it is monotonous, gives 0 for all-0 input, and gives 1 for all-1 input. 19:35:52 sounds about right 19:37:36 b_jonas: My language is eager. So the 'standard' Haskell short definition of a prime sieve doesn't work. 19:38:19 There are ways to deal with that. I listed two manners which mimic lazy lists. 19:39:00 [[Esolang talk:Categorization]] https://esolangs.org/w/index.php?diff=77065&oldid=74234 * SunnyMoon * (+663) /* Subcategories for the Non-Textual category. */ new section 19:41:52 The manner which I didn't list would be to use monads to model lazy behavior in an eager language. 19:42:05 I am trying to avoid that. 19:47:12 shachaf: is your computer-found solution a boolean function or a circuit? 19:52:27 ah I see 19:53:28 I would not specifically think of monads to avoid lazyness, just of a list-like iterator interface 19:53:59 or possibly the caching style a lazy list, since that's what you need for a prime sieve 19:57:40 Ah, but iterators fit into monads too. If you want it. 19:58:32 If you have any other possible solutions I would be very interested. 20:00:12 sure, but just the monad interface isn't really enough here 20:00:50 and I don't even see why it would really help much 20:01:34 the (>>=) method for lists is mapConcat, but you just need a filter, which is a special case of that, plus you need to iterate on the list of divisors and stop when they grow too large, for which monads don't really help 20:02:50 Looks like we have tangent thoughts on this. 20:04:51 [[Talk:Truth-machine]] https://esolangs.org/w/index.php?diff=77066&oldid=38410 * SunnyMoon * (+315) /* Is it possible to add "psuedo-truth-machines"? */ new section 20:07:34 yeah, ideally I should try to read your code and write the sieve with lazy lists like I thought, to make this clearer, but right now I'm busy with some stupid webpage 20:08:25 it's a webpage where I ordered something and want to order more, but I'm trying to write a userstyle to make the important control link visible, it's currently hidden by some stupid HTML+CSS thing that sets a height too small 20:08:45 and no, changing the height isn't enough, because then it overlaps something else 20:09:49 I don't understand why this user CSS rule doesn't match this element 20:11:15 Did you check its effects in the inspector? (At least, that is what I did.) 20:11:45 yes, that's what I'm trying to do 20:12:52 For if you change your mind. https://github.com/egel-lang/egel/blob/master/examples/sieve.eg https://github.com/egel-lang/egel/blob/master/examples/sieveK.eg 20:13:30 Well, what I think would be useful to have "meta-CSS" which is only usable in user CSS codes and cannot be specified by the web page author, and can be used for making selections based on other CSS commands, setting priorities differently, etc. 20:14:01 the inspector says `