Is there an online chat for SMT solvers?

Stream: general

[Srivatsa Srinivas]

Hi all,

I wanted to know if there was an online chat for SMT solvers. While we're at it I would also like to know if there is an SMT solver that can solve the following

Construct a list with a 100 elements such that list has only 2 elements equal to 1

Best,
Vatsa

[Henrik Böving]

SMT solvers like Z3 do have a theory of inductive data types so I'd guess you can certainly define this constraint

[Kim Morrison]

Not sure if this what you meant by "online chat", or if the answer is at all correct, but: https://chat.openai.com/share/d1046f16-61fb-41e2-a189-033b17c6e0cb

[Jason Rute]

Or do you mean something like this Zulip, but for discussing SMT solvers.

[David Renshaw]

z3 has an online playground here: https://microsoft.github.io/z3guide/playground/Freeform%20Editing/

[David Renshaw]

(for submitting code to be run, not for talking to other humans)

[Srivatsa Srinivas]

Jason Rute said:

Or do you mean something like this Zulip, but for discussing SMT solvers.

Yep!

[Srivatsa Srinivas]

Henrik Böving said:

SMT solvers like Z3 do have a theory of inductive data types so I'd guess you can certainly define this constraint

That is true, but is there a concrete reference to a solver that can actually solve the above problem with a list of length 100? Other people online showed me examples in z3 which work when the list length is small, about 10 elements long

[Jason Rute]

The are constraint solvers. I don’t know much, but I think they handle stuff like this.

[Luigi Massacci]

Srivatsa Srinivas said:

That is true, but is there a concrete reference to a solver that can actually solve the above problem with a list of length 100? Other people online showed me examples in z3 which work when the list length is small, about 10 elements long

surely prolog should be able to do this?

[Mark Fischer]

Here's a naive, first-attempt prolog solution:

% Base case.
ocurrenceof([], _, 0).

% Count the head of the list
ocurrenceof([H|T], H, NewCount) :-
    ocurrenceof(T, H, OldCount),
    NewCount is OldCount + 1.

% Don't Count the head of the list
ocurrenceof([H|T], H2, Count) :-
    dif(H, H2),
    ocurrenceof(T, H2, Count).

% Query for a list of length 100 with two occurrences of 1
?-  length(MyList, 100),
    ocurrenceof(MyList, 1, 2)

which will find lot of solutions. Something like 4950 solutions — one for each unique way you can place two 1s in a list of length 100. The first solution looks like (The ... just means "and so on"):

MyList = [1, 1, _A, _B, _C, ...],
dif(_A,1),
dif(_B,1),
dif(_C,1),
...

So, that's conclusive proof that Prolog can do this.

---

Mind you, I'm sure prolog has a compiled version of ocurrenceof that would run this MUCH faster (This is pretty slow for me). I'm also certain that somebody who didn't last use Prolog 10+ years ago could do this with more elegance and style.