Some time ago I made a little Nim binding and DSL around the Z3 theorem prover, which can be found at https://github.com/zevv/nimz3.
I made this mostly for fun and learning purposes, but never got to properly maintain or document it. Nimz3 has recently be picked up by Araq for the new "DrNim" project, and I start getting some issues and pull requests on the repo as well.
Unfortunately I currently lack both time and motivation to give this package the love it deserves, so I'm looking for someone who wants to adopt to prevent it from gathering dust and unanswered github issues.
The one most competent to maintain it is probably Double-oxygeN who wrote 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
# 3. The Spaniard owns the dog.
s.assert spaniard == dog
# 4. Coffee is drunk in the green house.
s.assert coffee == green
# 5. The Ukrainian drinks tea.
s.assert ukrainian == tea
# 6. The green house is immediately to the right of the ivory house.
s.assert green == ivory + 1
# 7. The Old Gold smoker owns snails.
s.assert old_gold == snails
# 8. Kools are smoked in the yellow house.
s.assert kools == yellow
# 9. Milk is drunk in the middle house.
s.assert milk == 3
# 10. The Norwegian lives in the first house.
s.assert norwegian == 1
# 11. The man who smokes Chesterfields lives in the house next to the man with the fox.
s.assert (chesterfields == fox + 1) or (chesterfields == fox - 1)
# 12. Kools are smoked in the house next to the house where the horse is kept.
s.assert (kools == horse + 1) or (kools == horse - 1)
# 13. The Lucky Strike smoker drinks orange juice.
s.assert lucky_strike == orange_juice
# 14. The Japanese smokes Parliaments.
s.assert japanese == parliament
# 15. The Norwegian lives next to the blue house.
s.assert (norwegian == blue + 1) or (norwegian == blue - 1)
# Now, who drinks water? Who owns the zebra?
s.check_model():
echo model
You can create an organization and add people there. It can be named nimZ3 or nim-proofs or solving-nim.
In any case I have absolutely no knowledge of Z3 but I have plenty of use-cases for it. And I did try to create a solver that would work at compile-time for array-bound checking for a polyhedral compiler (https://github.com/mratsim/hydra/blob/master/tests/test_sets.nim)