Current implementation of renderSMTFunction only works for non-recursive definitions. We need a better variant that can handle both recursive and non-recursive ones, so long as they're named. We probably want to change the whole API for this, shouldn't need a name or anything like that, just take a definition that's been defined with smtFunction. Given:
import Data.SBV
foo, bar :: SInteger -> SInteger
foo = smtFunction "foo" (\a -> bar a + 1)
bar = smtFunction "bar" (\a -> foo a + 1)
We currently get:
*Main> putStrLn =<< renderSMTFunction "foo" foo
; -- user given definition: foo [Recursive]
(define-fun-rec foo ((l1_s0 Int)) Int
(foo l1_s0))
I'm not sure why this is actually rendered as such. The actual output is:
Current implementation of
renderSMTFunction
only works for non-recursive definitions. We need a better variant that can handle both recursive and non-recursive ones, so long as they're named. We probably want to change the whole API for this, shouldn't need a name or anything like that, just take a definition that's been defined withsmtFunction
. Given:We currently get:
I'm not sure why this is actually rendered as such. The actual output is:
Need to accomplish the same directly from a function API.