Hi,
I wrote a miniKanren variant integrated with Rosette. It uses Rosette (SMT) as a backend for constraints solving. Now you can use SMT assertions as constraints. It significantly improves the expressiveness of miniKanren. See GitHub  chansey97/clprosetteminiKanren: CLP(Rosette) on top of miniKanren.
For example, you can define a factorial
relation in miniKanren and run it forward or backward.
#lang racket
(require "../mk.rkt")
(require "../rosettebridge.rkt")
(define (faco n out)
(conde
((== n 0) (== out 1))
((rosettetypeo n r/@integer?)
(rosetteasserto `(,r/@! (,r/@= ,n 0)))
(fresh (n1 r)
(rosettetypeo n1 r/@integer?)
(rosettetypeo r r/@integer?)
(rosettetypeo out r/@integer?)
(rosetteasserto `(,r/@= (,r/@ ,n 1) ,n1))
(rosetteasserto `(,r/@= (,r/@* ,n ,r) ,out))
(faco n1 r)))))
;; run factorial forward
(run* (q)
(fresh (out)
(faco 5 out)
(== q out)))
;; '(120)
;; run factorial backward
(run* (q)
(fresh (n)
(faco n 120)
(== q n)))
;; '(5)
;; No solution such that fac n = 500
(run* (q)
(fresh (n)
(faco n 500)
(== q n)))
;; '()
;; Get all factorials
(run 7 (q)
(fresh (n out)
(faco n out)
(== q `(,n ,out))))
;; '((0 1) (1 1) (2 2) (3 6) (4 24) (5 120) (6 720))
Here,

(rosettetypeo <var> <type)
is a Rosette type constraint.It constraints a miniKanren variable's domain as a Rosette type. You can put all Rosette solvable types in
<type>
, but prefix it withr/
. 
(rosetteasserto <formula>)
checks a SMT formula satisfiable.The
<formula>
can include any miniKanren variables, as long as they have been constrained byrosettetypeo
. Again, you can put all Rosette operators in<formula>
, but prefix it withr/
.
Note that the factorial example is not easy to be implemented in "vanilla miniKanren" (e.g. miniKanrensymbolicconstraints), because "vanilla miniKanren" does not support relational arithmetic operations.
P.s. The Reasoned Schemer introduced Kiselyov Arithmetic, which encodes natural numbers as lists of binary digits, but it is difficult to use and not flexible (e.g. it doesn't support negative numbers, rational, real, etc). CLP(Rosette)miniKanren supports all Rosette solvable types out of the box (e.g. booleans, integers, reals, bitvectors, and uninterpreted functions). Also, I believe extending other SMT theories is not difficult.
This project is still working in progress, any advice would be appreciated.
Enjoy .