clpsmt-miniKanren

clpsmt-miniKanren copied to clipboard

See the following program: ``` (run* (q) (z/ `(declare-const ,q Int)) (z/assert `(and (>= ,q 1) (= ,x 1) (

chansey97

Conference Call

7

Hi @chansey97, @michaelballantyne, @webyrd and everyone, We would like to set up a conference call to discuss the future of CLP(SMT)-miniKanren and welcome @chansey97 as a new contributor. We want...

namin

The current state of `clpsmt-miniKanren`

13

There are two main repos of miniKanren's SMT hook: [clpsmt-miniKanren](https://github.com/namin/clpsmt-miniKanren) and [smt-assumptions](https://github.com/namin/faster-miniKanren/tree/smt-assumptions) These two repos seemly have their own advantages and restrictions. 1. `smt-assumptions` uses `check-sat-assuming` to improve performance and...

chansey97

Confirm a bug about `declare-const` and `==`

32

Executing the following program crash: ``` (run 2 (q) (z/ `(declare-const ,q Int)) (== q 6)) Exception in call-z3: error in z3 out.smt > out.txt ``` smt.out ``` (declare-const 6...

chansey97

Some test cases failed, and which z3 version should I use?

14

Hi, I am trying to use clpsmt-miniKanren for constraint logic programming, it's great work! But I am not sure which z3 version should I use? I initially used z3-4.8.12, but...

chansey97