Skip to content
CLP(SMT) on top of miniKanren
Scheme Racket Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.io.livecode.ch
rai-clojure
==-tests.scm
LICENSE
README.md
absento-closure-tests.scm
absento-tests.scm
abstract-interp-tagged.scm
abstract-interp.scm
bouncing.rkt
boxes.rkt
boxes.scm
clpset-tests.scm
clpset.scm
clpsmt-basic-tests.scm
clpsmt-tests.scm
cvc4-driver.scm
cvc4-set-tests.scm
disequality-tests.scm
ex-model-unsat.smt
ex-model.smt
ex-sat.smt
ex-unsat.smt
exp.scm
exp2.scm
full-abstract-interp-extended-tests.scm
full-abstract-interp-extended.scm
full-interp-extended-memo-lambda-tests.scm
full-interp-extended-memo-lambda.scm
full-interp-extended-tests.scm
full-interp-extended-with-amb-tests.scm
full-interp-extended-with-amb.scm
full-interp-extended.scm
full-interp-mutation-apply-tests.scm
full-interp-mutation-apply.scm
full-interp-quine.scm
full-interp-with-let.scm
full-interp.scm
interp-program-synthesizer-blog-post.scm
mk-streaming-interface.scm
mk.rkt
mk.scm
mkf.scm
music.scm
numbero-tests.scm
numbers.scm
old-twenty-four-puzzle.scm
program-synthesizer-blog-post.scm
property-based-synthesis-tests.scm
radi-tests.scm
radi.scm
radif-tests.scm
radif.scm
radiw-concrete-tests.scm
radiw-concrete.scm
radiw-tests.scm
radiw.scm
rcd.scm
rcd.smt
reactive.rkt
reactive1.rkt
reactive2.rkt
reactive3.rkt
reactive4.rkt
recordsub.scm
rsa.scm
sign-domain-tests.scm
sign-domain.scm
simple-interp.scm
soft.smt
sudoku.rkt
symbolic-execution-tests.scm
symbolo-numbero-tests.scm
symbolo-tests.scm
synthesis.scm
tabling-tests.scm
tabling.scm
talk.rkt
talk.scm
tapl.scm
tapl.smt
tapl_cvc4.smt
test-all.scm
test-check.scm
test-full-suite.scm
test-header-with-tabling.scm
test-header.scm
test-numbers.scm
test-simple-interp.scm
test-suite-tabling.scm
twenty-four-puzzle-depth-limit.scm
twenty-four-puzzle-smart-transcript.scm
twenty-four-puzzle-smart.scm
twenty-four-puzzle.scm
while-abort-tests.scm
while-abort.scm
z3-driver.rkt
z3-driver.scm
z3-noserver.scm
z3-server.scm
z3-tests.scm

README.md

CLP(SMT)-miniKanren

Canonical miniKanren implementation, augmented with CLP(SMT).

Added SMT hooks: z/assert takes a boolean arithmetic expression with variables (integer by default), z/ takes an SMT statement, z/purge manually purges the SMT constraints into an enumeration of models, z/check only fails if the constraints are unsatisfiable.

Background on miniKanren

Starts with the language described in the paper:

William E. Byrd, Eric Holk, and Daniel P. Friedman. miniKanren, Live and Untagged: Quine Generation via Relational Interpreters (Programming Pearl). To appear in the Proceedings of the 2012 Workshop on Scheme and Functional Programming, Copenhagen, Denmark, 2012.

CORE LANGUAGE

Logical operators:

== fresh conde

Interface operators:

run run*

EXTENDED LANGUAGE

Constraint operators:

=/= symbolo numbero absento

You can’t perform that action at this time.