It's time to extend API supported by Crystal Z3, but first we need to deal with all the copypasta in z3/api.cr. It already has so many definitions like this:
def mk_power(a, b)
LibZ3.mk_power(Context, a, b)
end
And we really would rather not add 700 more. Booleans are straightforward to add. Reals and BitVectors will need some API changes, so I'll leave them for later.
There's a lot of code changes, so here's just the highlights.
VSCode Crystal extension isssue
A small annoyance with the extension is that it really thinks that code after fun snhould be indented:
fun mk_true = Z3_mk_true(ctx : Context) : Ast
If you copy and paste it a few times, here's how it's going to format it:
fun mk_true = Z3_mk_true(ctx : Context) : Ast
fun mk_true = Z3_mk_true(ctx : Context) : Ast
fun mk_true = Z3_mk_true(ctx : Context) : Ast
fun mk_true = Z3_mk_true(ctx : Context) : Ast
fun mk_true = Z3_mk_true(ctx : Context) : Ast
fun mk_true = Z3_mk_true(ctx : Context) : Ast
I didn't encounter any other issues, but worth fixing this one.
Bool types
I tried to do this, Haskell style:
module Z3
class BoolSort
def self.[](true)
BoolExpr.new API.mk_true
end
def self.[](false)
BoolExpr.new API.mk_false
end
It feels like it should work, but I'm getting Error: cannot use 'true' as a parameter name.
I can't do this either, as there's no TrueClass and FalseClass in Crystal:
module Z3
class BoolSort
def self.[](b : TrueClass)
BoolExpr.new API.mk_true
end
def self.[](b : FalseClass)
BoolExpr.new API.mk_false
end
I can do this, but it looks a lot less elegant:
module Z3
class BoolSort
def self.[](t : Bool)
if t
BoolExpr.new API.mk_true
else
BoolExpr.new API.mk_false
end
end
! pseudo-method
Ruby and Crystal both allow redefining operators, but in both cases some are hardcoded. Notably &&, ||, and, or, ?: are all hardcoded, as they're really control structures and cannot be implemented as methods using normal semantics of evaluating arguments first.
This makes the Z3 API a bit awkward, as it needs to do (a >= 0) & (a <= 9) instead of more natural0 a >= 0 && a <= 9 - and due to different operator precedence that requires extra parentheses.
Anyway, there's one difference in what's supported. Crystal doesn't support overloading !, while Ruby does. Interestingly, Ruby 1.x also did not support overloading !.
In principle, there's no reason why it shouldn't be supported. ! uses standard evaluation order.
Anyway, Crystal Z3 will have to use ~ for boolean negation, not !. Ruby Z3 supports both as aliases.
.ite type inference problem
.ite (if-then-else) is Z3 equivalent of ?: operator.
You can pass whatever you want to it, as long as both arguments have the same sort. So someBoolean.ite(anInt, anotherInt) is valid, as it someBoolean.ite(aBool, anotherBool) etc.
This is fine, but we also want to be able to be able to pass regular constants without explilictly casting them, like someBoolean.ite(anInt, 0) or even someBoolean.ite(10, 20).
So here's what I'd like to happen:
def ite(a, b) : IntExpr
IntExpr.new API.mk_ite(@expr, IntSort[a]._expr, IntSort[b]._expr)
end
def ite(a, b) : BoolExpr
BoolExpr.new API.mk_ite(@expr, BoolSort[a]._expr, BoolSort[b]._expr)
end
If a and b are both of types that can survive IntSort[], then use that definition. If they are of types that survive BoolSort[], use that definition. Otherwise, type error.
I don't think Crystal can quite do this.
So instead I need to do this explicitly:
def ite(a : (IntExpr | Int), b : (IntExpr | Int)) : IntExpr
IntExpr.new API.mk_ite(@expr, IntSort[a]._expr, IntSort[b]._expr)
end
def ite(a : (BoolExpr | Bool), b : (BoolExpr | Bool)) : BoolExpr
BoolExpr.new API.mk_ite(@expr, BoolSort[a]._expr, BoolSort[b]._expr)
end
And I'll need to add support for every new sort here.
There's another reason why what I want doesn't quite work, as in current api both accept String to mean a variable of given type, like IntSort["a"] and BoolSort["a"], so aBoolean.ite("a", "b") would type check both ways in my original definition. This is not really intentional, but I'll need to do some tweaks to the API to support reals and bitvectors anyway, so I'll leave it for now.
API macros
Here's api.cr with some very simple macros. Most methods just add Context argument. Some do other things like dealing with passing arrays, allocating strings etc., and that's also somewhat repetitive, but this is a lot less copypasta already.
module Z3
module API
extend self
Context = LibZ3.mk_context(LibZ3.mk_config)
{% for name in %w[
mk_div
mk_eq
mk_false
mk_ge
mk_gt
mk_iff
mk_implies
mk_ite
mk_le
mk_lt
mk_mod
mk_not
mk_power
mk_rem
mk_solver
mk_true
mk_unary_minus
mk_xor
simplify
solver_assert
solver_check
solver_get_model
] %}
def {{name.id}}(*args)
LibZ3.{{name.id}}(Context, *args)
end
{% end %}
{% for name in %w[
mk_add
mk_and
mk_distinct
mk_mul
mk_or
mk_sub
] %}
def {{name.id}}(asts)
LibZ3.{{name.id}}(Context, asts.size, asts)
end
{% end %}
def mk_numeral(num : Int, sort)
LibZ3.mk_numeral(Context, num.to_s, sort)
end
def mk_const(name, sort)
name_sym = LibZ3.mk_string_symbol(Context, name)
var = LibZ3.mk_const(Context, name_sym, sort)
end
# Not a real Z3 function
def mk_ne(a, b)
LibZ3.mk_distinct(Context, 2, [a, b])
end
def model_to_string(model)
String.new LibZ3.model_to_string(Context, model)
end
def ast_to_string(ast)
String.new LibZ3.ast_to_string(Context, ast)
end
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
end
end
New Int Functionality
I added one extra method #simplify. It's currently copy&pasted for every type:
it "simplify" do
a = Z3::IntSort[5]
b = Z3::IntSort[3]
((a+b).to_s).should eq("(+ 5 3)")
((a+b).simplify.to_s).should eq("8")
end
Bool Spec
Here's the spec for all the new Bool functionality:
require "./spec_helper"
describe Z3::BoolExpr do
a = Z3.bool("a")
b = Z3.bool("b")
c = Z3.bool("c")
x = Z3.int("x")
it "&" do
[a == true, b == true, c == (a & b)].should have_solution({c => true})
[a == true, b == false, c == (a & b)].should have_solution({c => false})
[a == false, b == true, c == (a & b)].should have_solution({c => false})
[a == false, b == false, c == (a & b)].should have_solution({c => false})
end
it "|" do
[a == true, b == true, c == (a | b)].should have_solution({c => true})
[a == true, b == false, c == (a | b)].should have_solution({c => true})
[a == false, b == true, c == (a | b)].should have_solution({c => true})
[a == false, b == false, c == (a | b)].should have_solution({c => false})
end
it "^" do
[a == true, b == true, c == (a ^ b)].should have_solution({c => false})
[a == true, b == false, c == (a ^ b)].should have_solution({c => true})
[a == false, b == true, c == (a ^ b)].should have_solution({c => true})
[a == false, b == false, c == (a ^ b)].should have_solution({c => false})
end
it "!=" do
[a == true, b == true, c == (a != b)].should have_solution({c => false})
[a == true, b == false, c == (a != b)].should have_solution({c => true})
[a == false, b == true, c == (a != b)].should have_solution({c => true})
[a == false, b == false, c == (a != b)].should have_solution({c => false})
end
it "implies" do
[a == true, b == true, c == a.implies(b)].should have_solution({c => true})
[a == true, b == false, c == a.implies(b)].should have_solution({c => false})
[a == false, b == true, c == a.implies(b)].should have_solution({c => true})
[a == false, b == false, c == a.implies(b)].should have_solution({c => true})
end
it "iff" do
[a == true, b == true, c == a.iff(b)].should have_solution({c => true})
[a == true, b == false, c == a.iff(b)].should have_solution({c => false})
[a == false, b == true, c == a.iff(b)].should have_solution({c => false})
[a == false, b == false, c == a.iff(b)].should have_solution({c => true})
end
it "==" do
[a == true, b == true, c == (a == b)].should have_solution({c => true})
[a == true, b == false, c == (a == b)].should have_solution({c => false})
[a == false, b == true, c == (a == b)].should have_solution({c => false})
[a == false, b == false, c == (a == b)].should have_solution({c => true})
end
# ! not possible
it "~" do
[a == true, b == ~a].should have_solution({b => false})
[a == false, b == ~a].should have_solution({b => true})
end
it "if then else" do
[a == true, x == a.ite(2, 3)].should have_solution({x => 2})
[a == false, x == a.ite(2, 3)].should have_solution({x => 3})
[a == true, b == a.ite(true, false)].should have_solution({b => true})
[a == false, b == a.ite(true, false)].should have_solution({b => false})
[a == true, b == a.ite(false, true)].should have_solution({b => false})
[a == false, b == a.ite(false, true)].should have_solution({b => true})
end
it "simplify" do
a = Z3::BoolSort[true]
b = Z3::BoolSort[false]
((a&b).to_s).should eq("(and true false)")
((a&b).simplify.to_s).should eq("false")
end
end
Story so far
All the episode code is in this repo.
We reached the point where abuot 80% of examples from my Ruby Z3 library could be ported to Crystal. The biggest missing piece is some way to extract data from the model better than stringifying the ASTs. Additional sorts like reals and bitvectors would be nice as well, and now that we can do it with less copy&pasting it should be easy enough.
Coming next
In the next episodes we'll see about adding additional sorts, better ways to extract data from the model, and some integration tests. Then I'll turn this into a proper shard you'll be able to use.
Top comments (0)