Thanks, MiniKanren implemented in C and Lua seems like the right way. SWI Prolog seems to use global state, which becomes no-no without using GILs and whatnot.

Thanks, MiniKanren implemented in C and Lua seems like the right way. SWI Prolog seems to use global state, which becomes no-no without using GILs and whatnot. Z3 I've use before in college, but it wasn't really a scripting tool, unless something changed in the meantime.