Sam Bayless

Yes, that should be possible. monosat is closely based on minisat, and it should be relatively easy to integrate the monotonic theory solvers in monosat into any similar SMT solver...

I see that recent versions of minisat guard this setting the way you've suggested: https://github.com/niklasso/minisat/blob/master/minisat/utils/System.cc#L100 ``` #if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW) ``` I should be able to...

I haven't thought too deeply about the Datalog/MonoSAT connection before; but it could be promising. Maybe something like: rules in data log become edges in a graph, facts are modeled...

I'd be all for it, but I'm not sure what would be involved. Can you point me to any resources for packing python libraries that rely on native libraries?