Support for recursive functions?

[pjljvandelaar]

We would like to over yices and yicesNL as solvers to the users of TorXakis (see https://github.com/TorXakis/TorXakis/issues/265).

However, we are using a feature of smt2.5 which currently is not yet supported by yices 2.6.0.

For example the attached file gives the following output:

C:\experiments> yices-smt2 --incremental .\logSMT.2018-07-06-09-40-29.9686366.txt
(:name "Yices")
(:version "2.6.0")
(error "option :produce-models can't be set now. It must be set before (set-logic ...)")
(error "at line 12, column 17: syntax error: define-funs-rec is not a command")

logSMT.2018-07-06-09-40-29.9686366.txt

due to

(define-funs-rec
  (
    (f1044$validInt((x$$1045 Int)) Bool)
  )
  (
    (and (<= 0 x$$1045) (<= 0 (+ 10 (- x$$1045))))
  )
)

Note: changing it to define-fun, which for this particular function is possible, yields the desired results. So when this feature is implemented we must be able to offer Yices as an alternative.

[BrunoDutertre]

Don't use recursive functions. Yices will not support them any time soon.

Here's why:

1. simple logics that are decidable become undecidable if you allow recursive functions.
2. to do anything reasonable, you need something like e-graph matching or some variant to instantiate. Yices does not support this.
3. things get very messy if your recursive functions are incorrect, and there's nothing to ensure that recursive definitions are well founded.