First, I decided to rearrange how code for this series is organized. All the episode code will go to this repo, and crystal-z3 repo will be the place where the library is going to live once it's a bit more ready.
Anyway, time to add some specs, and fill in some missing operators.
Specs in Crystal
In the Ruby gem I'm unit testing Z3 like this:
module Z3
describe IntExpr do
let(:a) { Z3.Int("a") }
let(:b) { Z3.Int("b") }
let(:c) { Z3.Int("c") }
let(:x) { Z3.Bool("x") }
it "+" do
expect([a == 2, b == 4, c == a + b]).to have_solution(c => 6)
end
it "-" do
expect([a == 2, b == 4, c == a - b]).to have_solution(c => -2)
end
it "*" do
expect([a == 2, b == 4, c == a * b]).to have_solution(c => 8)
end
...
Crystal comes with builtin rspec-like test runner. I was confused by documentation, especially around two questions - what's equivalent of RSpec's let, and how can I do custom matchers?
I can suspend the let question for now. For Rails it's common to do very fancy let chains - where top of an example group defines a lot of defaults with let, then individual scenarios just override some of them. I only really needed to setup some variables.
I checked inside Crystal standard library for some examples, and they were full of macros, and not the most readable. There was one custom matcher for BigInt, and it was doing some __FILE__/__LINE__ magic.
spec/spec_helper.rb
After some digging in Crystal's source code, I managed to recreate custom expectation, positive case only:
require "spec"
class SolutionExpectation(T)
def initialize(@expected : Hash(T, String))
end
def setup_solver(asts)
solver = Z3::Solver.new
asts.each do |ast|
solver.assert(ast)
end
solver
end
def match(asts)
solver = setup_solver(asts)
return false unless solver.satisfiable?
model = solver.model
@expected.each do |ast, expected_value|
return false unless model[ast] == expected_value
end
true
end
def failure_message(asts)
solver = setup_solver(asts)
unless solver.satisfiable?
return "Expected #{asts.inspect} to have a solution, but no solution was found"
end
model = solver.model
"Solution found, but it does not match expectations:\n" +
@expected.map do |ast, expected_value|
"#{asts} (actual #{model[ast]}, expected #{expected_value})"
end.join("\n")
end
end
module Spec::Expectations
def have_solution(solution)
SolutionExpectation.new solution.transform_values(&.to_s)
end
end
At first I tried to define it as @expected : Hash(Z3::BoolExpr | Z3::IntExpr, String), but Crystal did not like that, saying it conflicts with me passing @expected : Hash(Z3::IntExpr, String) to it.
It looks like some subtyping variance issue, which are really infuriating. Notably TypeScript decided to just accept technically invalid types for such cases by default, as there's no sane way to do this fully correctly.
Crystal has more flexible type inference algorithm, so this could be fixable in principle. Anyway, I just avoided the whole problem using generics.
spec/int_spec.cr
It's mostly based on Ruby version, but some functionality is still missing:
require "./spec_helper"
require "../src/z3"
describe Z3::IntExpr do
a = Z3.int("a")
b = Z3.int("b")
c = Z3.int("c")
x = Z3.bool("x")
it "+" do
[a == 10, b == 20, c == a + b].should have_solution({c => 30})
[a == 2, b == 10 + a].should have_solution({b => 12})
[a == 2, b == a + 10].should have_solution({b => 12})
end
it "*" do
[a == 10, b == 20, c == a * b].should have_solution({c => 200})
[a == 2, b == 10 * a].should have_solution({b => 20})
[a == 2, b == a * 10].should have_solution({b => 20})
end
it "-" do
[a == 10, b == 20, c == a - b].should have_solution({c => 30})
[a == 2, b == 10 - a].should have_solution({b => 12})
[a == 2, b == a - 10].should have_solution({b => 12})
end
it "/" do
[a == 10, b == 3, c == a / b].should have_solution({c => 3})
[a == -10, b == 3, c == a / b].should have_solution({c => -4})
[a == 10, b == -3, c == a / b].should have_solution({c => -3})
[a == -10, b == -3, c == a / b].should have_solution({c => 4})
end
# Can't say these make much sense, but let's document what Z3 actually does
it "rem" do
[a == 10, b == 3, c == a.rem(b)].should have_solution({c => 10 - 3 * 3})
[a == -10, b == 3, c == a.rem(b)].should have_solution({c =>-10 - 3 * -4})
[a == 10, b == -3, c == a.rem(b)].should have_solution({c =>-( 10 - -3 * -3)})
[a == -10, b == -3, c == a.rem(b)].should have_solution({c =>-(-10 - -3 * 4)})
end
it "mod" do
[a == 10, b == 3, c == a.mod(b)].should have_solution({c => 1})
[a == 10, b == -3, c == a.mod(b)].should have_solution({c => 1})
[a == -10, b == 3, c == a.mod(b)].should have_solution({c => 2})
[a == -10, b == -3, c == a.mod(b)].should have_solution({c => 2})
end
it "==" do
[a == 2, b == 2, x == (a == b)].should have_solution({x => true})
[a == 2, b == 3, x == (a == b)].should have_solution({x => false})
end
it "!=" do
[a == 2, b == 2, x == (a != b)].should have_solution({x => false})
[a == 2, b == 3, x == (a != b)].should have_solution({x => true})
end
it ">" do
[a == 3, b == 2, x == (a > b)].should have_solution({x => true})
[a == 2, b == 2, x == (a > b)].should have_solution({x => false})
[a == 1, b == 2, x == (a > b)].should have_solution({x => false})
end
it ">=" do
[a == 3, b == 2, x == (a >= b)].should have_solution({x => true})
[a == 2, b == 2, x == (a >= b)].should have_solution({x => true})
[a == 1, b == 2, x == (a >= b)].should have_solution({x => false})
end
it "<" do
[a == 3, b == 2, x == (a < b)].should have_solution({x => false})
[a == 2, b == 2, x == (a < b)].should have_solution({x => false})
[a == 1, b == 2, x == (a < b)].should have_solution({x => true})
end
it "<=" do
[a == 3, b == 2, x == (a <= b)].should have_solution({x => false})
[a == 2, b == 2, x == (a <= b)].should have_solution({x => true})
[a == 1, b == 2, x == (a <= b)].should have_solution({x => true})
end
it "**" do
[a == 3, b == 4, c == (a ** b)].should have_solution({c => 81})
end
it "unary -" do
[a == 3, b == -a].should have_solution({b => -3})
end
end
Other than extra {}s, the syntax looks just fine.
Some hacks
At some point we'll need to write Ast#to_s. Using one included with Z3 is not really sustainable, as it prints everything as Lisp expression. Most notably it prints negative numbers as Lisp expressions, so -420 is returned as (- 420), which is definitely not what we want.
For now I just hacked it a bit, here's IntExpr:
# This is hacky as hell, we need our own printer as these are
# just Lisp-style S-expression and won't even handle negatives in a sensible way
# For example -4 is "(- 4)"
def to_s(io)
s = API.ast_to_string(@expr)
if s =~ /\A\(- (\d+)\)\z/
s = "-#{$1}"
end
io << s
end
The same code is repeated in Model (which now uses out argument):
def model_eval(model, ast, complete)
result = LibZ3.model_eval(Context, model, ast, complete, out result_ast)
raise "Cannot evaluate" unless result == true
# Full conversion is complicated, this is a good start
s = ast_to_string result_ast
if s =~ /\A\(- (\d+)\)\z/
s = "-#{$1}"
end
s
end
Story so far
All the episode code is in this repo.
Coming next
In the next episode I'll add support for boolean operations, and some integration tests.
Top comments (0)