Nada Amin

I was planning to use Zoom. If something else is more convenient for you, let me know.

This is the Zoom invitation. Nada Amin is inviting you to a scheduled Zoom meeting. Topic: CLP(SMT) Kickoff Time: Aug 16, 2021 03:00 PM Zurich Join Zoom meeting https://harvard.zoom.us/j/94535871330?pwd=RjhISGNzM3dTbE8wUXB5OUhva0VZQT09 Password:...

Reminder that the meeting is in 10 minutes. Meeting link: https://harvard.zoom.us/j/94535871330?pwd=RjhISGNzM3dTbE8wUXB5OUhva0VZQT09 Here is a doc for notes: https://docs.google.com/document/d/1bId06qsQ9fcdK0kveICSHJCtf4ooN5UutjQd8CSf1QI/edit?usp=sharing

Thanks for your thoughtful issue. 1. constraint promotion: I think it's worth exploring. Are there any difficulty for extending it to types other than numbers? did you find it educational...

- In short, we want to make it fast enough to be usable for real use cases. + For example, in Barliman, we played with synthesizing factorial from examples. See...

It's worth also looking at https://github.com/michaelballantyne/faster-miniKanren/commits/smt-numsonly by @michaelballantyne

In the `all-diffo` example, could you reuse the definition of `equalo`? I think it's good to experiment with different approaches. The tag approach seems a bit annoying -- think how...

So instead of grounding SMT variables, you would assert their values?

I don't quite remember. From the commit message, it sounds like I expect users to use `z/assert` instead of `=`. I don't see why this line hurts. We can uncomment...

Thanks for your thoughts and examples. To proceed with a design, I think maybe it makes sense to distinguish between a low-level API, where one uses declare-const and assert and...