Compiling to Categories
Ok, here's my equation for the solver, written in plain Haskell:
equation :: (Num a, Ord a) => a -> a -> Bool
equation x y =
x < y &&
y < 100 &&
0 <= x - 3 + 7 * y &&
(x == y || y + 20 == x + 30)
Here's how I run the solver:
res <- evalZ3With Nothing opts $ do
x <- mkFreshIntVar "x"
y <- mkFreshIntVar "y"
PrimE ast <-
runKleisli (runZ3Cat (ccc @Z3Cat (uncurry (equation @Int))))
(PairE (PrimE x) (PrimE y))
assertShow ast
-- check and get solution
fmap snd $ withModel $ \m ->
catMaybes <$> mapM (evalInt m) [x, y]
case res of
Nothing -> error "No solution found."
Just sol -> do
putStrLn $ "Solution: " ++ show sol
And here's the result, which also show you the equation we submitted to Z3:
(let ((a!1 (ite (<= 0 (+ (- x!0 3) (* 7 y!1)))
(ite (= x!0 y!1) true (= (+ y!1 20) (+ x!0 30)))
false)))
(ite (< x!0 y!1) (ite (< y!1 100) a!1 false) false))
Solution: [-8,2]
Now with one function, I have either a predicate that I can use in Haskell
code, or an input to Z3 for finding possible arguments for which it is true!
______________
[1]. https://github.com/conal/concat/issues/4
[2]. http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf
TAGS (EDIT) ccc, smt