Z3 Constraint Solver library for Ruby

Wouldn't it be awesome if you could just describe a problem to the computer, like let's say a sudoku, and it would find the answer for you?

That was the premise of "logic programming" in 1970s and 1980s, which was also one of many cases where Japan tried to do something else than everybody else, and failed, but it's not a post about history.

Logic programming suffered a lot worse than other paradigms. Lisp, Smalltalk, Perl, and friends left rich legacy of features for future programming languages to mine, but Prolog variants were all one big dead end.

Which is a bit of a shame, as some problems are really best coded by giving computer a list of constraints, and telling it to have a go at it, and it's very difficult to write a decent custom algorithm for them.

Technically you could use constraint solver libraries even without logic programming, but they were mostly only available in obscure Lisp / Prolog dialects, hard to compile on modern systems, barely documented, and/or extremely limited.

This somewhat changed with Z3 by Microsoft Research, which even got rudimentary Python interface.

But while Python is tolerable, I got tired of all the self. nonsense, and I wanted a nice Ruby DSL, so I wrote Ruby bindings. You can install them as z3 gem but first you need z3 library itself (brew install z3 or whatever works on your system).

If you want a quick look, check examples folder. If you want longer explanation, let's keep going.

Basic model

The basic Z3 workflow is:

• create solver with Z3::Solver.new
• create a bunch of formulas, generally starting with variables like Z3.Int("a"), Z3.Bool("b") etc. - formulas are independent of any solver, they're basically symbol trees.
• assert some facts about those variables, like solver.assert Z3.Int("a") == Z3.Int("b") + Z3.Int("c")
• ask solver to check if your set of formulas is satisfiable with solver.check. If it returns :sat, you're good to go.
• get Z3::Model with solver.model
• ask model for value of various variables with queries like model[Z3.Int("a")] etc.

Sorts

Let's go deeper, one step at a time. Values in Z3 all belong to "Sorts" which are sort of like types.

To create a Sort object, just instantiate its class, like Z3::BoolSort.new, then you can create relevant object like Z3::BoolSort.new.var("my_var") or Z3::IntSort.new.from_const(5). This seems like unnecessary indirection, and it sort of is for most common sorts, but there are fancier ones where it's necessary.

Some of the sorts are:

• Z3::BoolSort.new - boolean variables
• Z3::IntSort.new - integers, unlimited precision
• Z3::RealSort.new - real numbers, unlimited precision 
• Z3::BitvecSort.new(size) - bit vector sorts, of size bits
• Z3::FloatSort.new(esize, ssize) - floating point sort of esize exponent bits and ssize significand bits
• Z3::RoundingModeSort.new - floating point rounding mode sort
• Z3::SetSort.new(elemement_sort) - set sort of elements of elemement_sort sort
• Z3::ArraySort.new(key_sort, value_sort) - associative array sort with keys of key_sort, and values of value_sort
• there are some more sorts in Z3 which are not yet implemented

For vast majority of uses you want Bool and Int sorts, for physics style calculations you want Real sort (generally don't use Floats for them). They have decently completely and nice APIs.

Bitvec and Float sorts should work reasonably well, but their APIs are somewhat awkward - for example a lot of Bitvec operations have separate signed and unsigned operations, so you need to do awkward things like Z3.Bitvec("a", 32).signed_gt(100) instead of more obvious but ambiguous Z3.Bitvec("a", 32) > 100.

Float APIs are even worse as a lot of operations need rounding mode passed - and most operations take rounding mode argument, and printing out results tries to use precise but unintuitive notation like 1.25B+5.

Sets, Arrays, and fancier stuff, are basically unfinished.

The obvious missing sort is any kind of finite domain integer, like Int[1..9] - in Z3 you need to create Int variable, and then tell the solver that it's within certain range, like solver.assert (Z3.Int("a") >= 1) & (Z3.Int("a") <= 9)

ASTs

You want to give Z3 a bunch of formulas, and these generally start with variables like sort.var("name"). As Z3::BoolSort.new.var("name") is fairly long, shortcuts like Z3.Bool("name") are provided.

From that point, you can construct your formulas with fairly straightforward ruby - a + b == c means exactly what you'd expect if a is Z3.Int("a") and so on.

There are of course some complications:

• ruby won't let us override !, &&, and || - so we use ~, & and | for booleans - and they have different parsing priorities so you might need to add some parentheses
• you can't directly check if a value is equal to something else, as foo == 0 will create a z3 Bool expression not give you true/false. It's a great case where some extra operators would be useful, but for now just .to_s whatever you want to extract or check.
• some operations don't have easy operator equivalents, so other syntax is provided. For some common examples - to assert that a bunch of values are all different, you can use Z3.Distinct(a, b, c, ...), for z3 ternary use (bool_expression).ite(if_true, if_false).
• we'll automatically convert ruby values like true or 42 to z3 expressions, but if you try to mix sorts without converting them appropriately you'll generally get an exception
• ASTs are interned, so every Z3.Int("a") + 2 == Z3.Int("b") is going to be the same underlying object.

Library layers

Z3 is a huge library, and it really doesn't map to anything resembling a sensible ruby API, so there are many layers here:

• We use ffi to create Z3::VeryLowLevel interface of raw C calls. You should never use it directly.
• After that there's Z3::LowLevel interface which basically deals with context management, array arguments, and mapping Ruby object arguments (but not return values) to FFI pointers. You should also never use it directly.
• Then there are legitimate Ruby objects. A lot of them are wrappers around C pointers, so using SomeClass.new(c_pointer) to create them directly is not really supported. These pointers can be accessed by attributes starting with underscore (like _ast, _sort etc.), but it's all for internal use only.
• The main reason for this anal system is that if you mess anything up, you'll get a crash. For some things Z3 library raises error which we then turn into Z3::Exception, but other things just crash your program with segmentation fault. I added a lot of checks for operations which might end with segmentation fault so you get Z3::Exception instead, but I'm sure I missed some things.
• Reference counting memory management z3 uses is not exactly compatible with ruby, so if you use it in a very long running process like Rails server, it might cause problems. It's usually going to be no worse than Symbol interning.
• Default interface doesn't give any guarantees for running time. The underlying z3 library has ways to restrict solver check running time, but they're not exposed in any convenient way yet.

No semantic versioning

Z3 is huge library (I only described the basic), and the gem is not only incomplete, but many APIs are fairly poor.

Until I release 1.0, any version can freely break any API, so if you want to rely on a stable version, just depend on exact one - or help me complete it faster.

The regular flow with Bool, Int, Real and Solver shouldn't break too often, but Bitvec, Float etc. feel awkward and could use a nicer API.

Pull requests wellcome.