search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
370 stars 47 forks source link

Requesting improved smt2 array support #390

Closed GreenBeard closed 2 years ago

GreenBeard commented 2 years ago

I understand that yices doesn't differentiate between arrays, and functions internally, but I was wondering if the output while using the --smt2-model-format flag could have an option to output the result as an array if the input was an array (or as a function if the input was a function)? Currently, the output being a function when the input was an array makes it harder to use the result in some of the other solvers (e.g. z3, and cvc5) as they seem to differentiate between the two.

Current output:

(define-fun params ((x!0 Int)) Int (ite (= x!0 6) 5 (ite (= x!0 5) 2 (ite (= x!0 4) 2 (ite (= x!0 3) 0 (ite (= x!0 2) 1 14))))))

Desired output (I hand translated this, so I may have made minor mistakes, but I think it is correct):

(define-fun params () (Array Int Int) (store (store (store (store (store ((as const (Array Int Int)) 14) 2 1) 3 0) 4 2) 5 2) 6 5))

Ideally, yices would also support (as const (Array Int Int)) inputs too, but I assume that would be more work. Unfortunately, this means that a separate flag probably is needed (to enable outputting arrays as arrays) as otherwise yices could produce smtlib2 formats that it couldn't read.

Edit: The ((as const (Array Int Int)) 14) syntax appears to be non-standard smt-lib syntax that cvc4, z3, mathsat, and possibly more provers support. I would still appreciate this being supported, but it doesn't appear to be specified in the standards anywhere that I can find, and I see some comments elsewhere on the internet saying it isn't part of the standard. :/

disteph commented 2 years ago

I suspect (as const (Array Int Int)) would be some work, starting with an extension of the SMT2 parser. We may in the near future equip Yices with a generated parser instead of the currently hard-coded one, which would make it easy to do such extensions.

But I suspect the more involved work would be to tweak the algorithm for the array/uninterpreted function theory in order to set the default return value of a lambda-function to whatever is specified in the (as const (Array Int Int)) constructs, and trigger backtracks when hitting conflictual information that essentially amount to (= ((as const (Array Int Int)) 0) ((as const (Array Int Int)) 1).

Quantifiers would be able to specify default values for arrays/functions, but I don't think Yices support for quantifiers would handle the presence of the other theories (etc, for 0, 1, etc), and there must be some simpler way of handling default values for functions that doesn't get into quantifiers, perhaps along the lines above. Do you happen to have pointers? @BrunoDutertre, any thoughts? We don't have a lot of bandwidth for this at the moment at SRI.

Re. the pretty-print of functions as arrays, I sympathize with your need, but it is a low priority on our to-do list. If you are willing to play with the Yices API, you can get the value for the array / uninterpreted function as a lambda-term, and then pretty-print it in whichever way you like by traversing the lambda-term... How do you normally use Yices?

GreenBeard commented 2 years ago

I have decided that I am satisfied with the current method of handling Arrays in Yices. I just adjusted all of my code to use functions instead of arrays. I initially thought that Arrays would be preferable as that is what I was thinking about them in my head as, but as you said you can obtain the values equivalently from both. I'm not sure why the smtlib2 specification even has arrays once I gave it more thought (I was sure that there must be reasons when I initially filled this bug report). I wouldn't mind if anyone closed this issue (especially considering it sounds as though it will be non-trivial levels of work to implement).

disteph commented 2 years ago

OK thanks! We'll keep in mind the handling of constant functions, whenever we get the opportunity to look into that.

BrunoDutertre commented 2 years ago

I'm happy @GreenBeard is fine with functions. It would be tricky otherwise to keep track of what's been declared as an array vs a function. Internally, the Yices type system doesn't do it.

disteph commented 2 years ago

If you are willing to play with the Yices API, you can get the value for the array / uninterpreted function as a lambda-term, and then pretty-print it in whichever way you like by traversing the lambda-term...

Let me slightly amend my remark: as discussed in #395, you can't get the value as a lambda-term directly with yices_get_value_as_term; you have to produce an yval_t and inspect it to get the default value and the mappings.