How to test for data-type constructor via API?

[ranjitjhala]

Hi all,

[my apologies in advance for posting this q here -- LMK if you prefer it on e.g. stackoverflow or similar!]

Thanks again for fixing that odd regression in record time!

I have an unrelated question I wanted to ask you, about encoding "computation" in Z3.

You might recall a talk I gave at the workshop in Essaouira several years ago

  https://ranjitjhala.github.io/static/reasoning-about-functions.pdf

the high-level bit is one can have user defined functions and the above describes an algorithm to "run" those functions on symbolic inputs via SMT queries (without axioms
fuel etc.) We've been really pushing it quite a bit and people are writing large functions with hundreds of computation steps which take rather too long using the SMT-LIB interface.

What I'm wondering is whether it would be faster if we had access to the congruence closure context e.g. via the C/Python API. Abstractly, the procedure would look like this:

  while (some condition):    
    check-if-terms-are-of-a-certain-constructor (e.g. is-Nil, is-Cons)
    assert-some-equalities-on-terms

   
So basically I want to assert a bunch of equalities e.g.

   x = Nil 
   y = Cons(h1, x)

 
Then check if some terms are constructors e.g.

   isCons(x)   
   isCons(y)

  
and then depending on the result of the above, add more equalities and continue.

Do you have any advice for how I might go about doing this?

The key missing piece in the API seems to be how to check whether a term is
of a given constructor -- isCons -- maybe I just missed it?

Any tips would be most welcome!

Thanks!

[NikolajBjorner]

Maybe the following: You could try to enumerate consequences. For instance you
create atoms ((_ is Cons) x) ((_ is Nil) x) and see which one is a consequence, if any.

If you want to hack your own solver (of course you do), then use the new API for user-propagation. You need to register the atomic formulas you want to track. Basic example usage is given here in Section 7: http://theory.stanford.edu/~nikolaj/navigate.html
For tracked atomic formulas you get a callback from the solver when they are assigned. You can then propagate as you please (or just observe and report).

Of course, all of this can be explained much better on a bench at Scripps.

[ranjitjhala]

First off: thanks, I didn't know about this new discussions thing -- very useful

Excellent -- thanks for the suggestions, I'll try to play around with this.

Most importantly, my goal was to see if you might be interested in this problem, which is to say, please consider this a formal invitation to come down and explain on a bench at Scripps! I can also send by official letterhead if needed :-)