Does anyone know if there's a datalog-like embeddable language that is suitable for simple integer constraints (the sum of a, b, c, and d must be e; e=10.,b>2.)?
But I really just want some simple constraints-oriented form validation (you have 100 points, please feel free to by x's for 1 point each, y's for a cost of 5 points. You don't have to spend all points - with feedback of how many points are left as more x and y are bought. But for more variables, where there are clear rules that can be modeled naturally as constraints rather than with state and callbacks on change).
It has bindings for other languages and is able to make some rather sophisticated arithmetical and logical deductions in an often pretty efficient way. I've used it successfully for parts of puzzle competitions and CTFs (and I'm really only beginning to scratch the surface of what it can do).
You can read more about the options in that area at
These systems can feel pretty magical and are getting more powerful all the time. (Of course there are cases where there is a better algorithm that you could find, perhaps a much more efficient one, and using these solvers will be asymptotically or worst-case slower than it had to be given more human insight.)
Some of these could be overkill for your application, and Z3 doesn't have a Javascript binding, so I guess it's not as helpful for web forms.
Do you have any suggestions on how to get started? I remember reading "The unreasonable effectiveness of SAT solvers" or whatever it was called which showed that SAT solvers are not always the most efficient performers, but they can take you within a factor 10 in much less time. I remember thinking, "Oh, but what about SMT solvers, then?" But not getting anywhere with that.
SAT, SMT, constraint programming lie on a continuum. SMT is SAT plus machinery from constraint programming. I'm not an expert on this, just info from this video. According to him constraint programming will win in the long run because of constraint programming has larger structures which can be exploited with global constraints (SAT is only a flat sequence).
If your main use case is browser form validation, have a look at Tau Prolog. It doesn't have constraint library but standard Prolog should be enough for something like this.
I've not been able to find something similar for datalog - but to be honest, I don't think I've managed to find solid documentation for datalog. Not that I've been able to really grok the language from enough to build an intuition for what's an idiomatic approach, at least.
You also mentioned CLP(Z) in the parent comment. Not sure if familiar you are with these tools, but here's a nice intro: https://www.metalevel.at/prolog/clpz
Ed: the introduction looks like exactly what I need from the prolog side, last I looked at this stuff in prolog, I only found some proof of concept/instructive texts using Peano numbers - which works after a fashion, but is slow and painful.
There's nothing analogous for datalog or some other minimal, embeddable logic/predicate system?
Tau Prolog[0] runs in the browser, but it's still a bit heavy for forms.
What someone needs to do is take an implementation of Hitchhiker Prolog[1] like this one[2] – because it's so lightweight – and make it JavaScript developer friendly so one can use it on a web page without a second thought.
For prolog, there's apparently https://github.com/triska/clpz/
But I really just want some simple constraints-oriented form validation (you have 100 points, please feel free to by x's for 1 point each, y's for a cost of 5 points. You don't have to spend all points - with feedback of how many points are left as more x and y are bought. But for more variables, where there are clear rules that can be modeled naturally as constraints rather than with state and callbacks on change).
Ed: specifically for forms, there's https://developer.mozilla.org/en-US/docs/Web/Guide/HTML/HTML... - but it feels like it gets messy with interdependent fields.