The one most competent to maintain it is probably **Double-oxygeN** who wrote
[z3nim](https://github.com/Double-oxygeN/z3nim) last year. Comparing both
packages, z3nim supports more Z3 features but nimz3 is more integrated with Nim
style.
I'm interested in supporting nimz3 but I'm not fully Nim and Z3 proficient
while learning both. Also I'm a poor git user!:-( And I don't have much control
on the time I can dedicate. All this to say that if someone else volunteer too,
we can have a better long term support.
For those who don't know, Z3 allows solve problems by describing constraints
and letting the solver find solutions using different tactics. It can be used
to describe complex problems nicely.
A classical example
import unittest
import z3
suite "z3 puzzles":
test "einstein problem":
# https://en.wikipedia.org/wiki/Zebra_Puzzle
#
# 1. There are five houses.
# 2. The Englishman lives in the red house.
# 3. The Spaniard owns the dog.
# 4. Coffee is drunk in the green house.
# 5. The Ukrainian drinks tea.
# 6. The green house is immediately to the right of the ivory house.
# 7. The Old Gold smoker owns snails.
# 8. Kools are smoked in the yellow house.
# 9. Milk is drunk in the middle house.
# 10. The Norwegian lives in the first house.
# 11. The man who smokes Chesterfields lives in the house next to the
man with the fox.
# 12. Kools are smoked in the house next to the house where the horse
is kept.
# 13. The Lucky Strike smoker drinks orange juice.
# 14. The Japanese smokes Parliaments.
# 15. The Norwegian lives next to the blue house.
#
# Now, who drinks water? Who owns the zebra?
#
# In the interest of clarity, it must be added that each of the five
houses is painted a
# different color, and their inhabitants are of different national
extractions, own different
# pets, drink different beverages and smoke different brands of
American cigarets [sic]. One
# other thing: in statement 6, right means your right.
z3:
# sort declaration
let yellow = Int("yellow")
let blue = Int("blue")
let green = Int("green")
let ivory = Int("ivory")
let red = Int("red")
let englishman = Int("Englishman")
let spaniard = Int("Spaniard")
let ukrainian = Int("Ukrainian")
let norwegian = Int("Norwegian")
let japanese = Int("Japanese")
let water = Int("water")
let tea = Int("tea")
let milk = Int("milk")
let orange_juice = Int("orange juice")
let coffee = Int("coffee")
let kools = Int("Kools")
let chesterfields = Int("Chesterfields")
let old_gold = Int("Old Gold")
let lucky_strike = Int("Lucky Strike")
let parliament = Int("Parliament")
let fox = Int("fox")
let snails = Int("snails")
let horse = Int("horse")
let dog = Int("dog")
let zebra = Int("zebra")
let s = Solver()
s.assert distinc(yellow, blue, red, green, ivory)
s.assert distinc(englishman, spaniard, ukrainian, norwegian, japanese)
s.assert distinc(water, tea, milk, orange_juice, coffee)
s.assert distinc(kools, lucky_strike, parliament, old_gold,
chesterfields)
s.assert distinc(fox, snails, horse, dog, zebra)
# Limit values
s.assert 1 <= yellow and yellow <= 5
s.assert 1 <= blue and blue <= 5
s.assert 1 <= red and red <= 5
s.assert 1 <= green and green <= 5
s.assert 1 <= ivory and ivory <= 5
s.assert 1 <= englishman and englishman <= 5
s.assert 1 <= spaniard and spaniard <= 5
s.assert 1 <= ukrainian and ukrainian <= 5
s.assert 1 <= norwegian and norwegian <= 5
s.assert 1 <= japanese and japanese <= 5
s.assert 1 <= water and water <= 5
s.assert 1 <= tea and tea <= 5
s.assert 1 <= milk and milk <= 5
s.assert 1 <= orange_juice and orange_juice <= 5
s.assert 1 <= coffee and coffee <= 5
s.assert 1 <= kools and kools <= 5
s.assert 1 <= lucky_strike and lucky_strike <= 5
s.assert 1 <= parliament and parliament <= 5
s.assert 1 <= old_gold and old_gold <= 5
s.assert 1 <= chesterfields and chesterfields <= 5
s.assert 1 <= fox and fox <= 5
s.assert 1 <= snails and snails <= 5
s.assert 1 <= horse and horse <= 5
s.assert 1 <= dog and dog <= 5
s.assert 1 <= zebra and zebra <= 5
# 2. The Englishman lives in the red house.
s.assert englishman == red
