Using uninterpreted functions in a quantified formula will not declare it in the top-level

[lsrcz]

There is likely a bug when using uninterpreted functions in a quantified formula. SBV does not declare them in the top-level.

The following code

runSMTWith z3 {verbose = True} $ do
  let f = uninterpret "f" :: SInteger -> SInteger
  query $ do
    constrain $ \(Forall (b :: SInteger)) -> f b .== f b
    checkSat

gives

** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; external query, using all logics.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] ; --- arrayDelayeds ---
[GOOD] ; --- arraySetups ---
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[FAIL] (define-fun s0 () Bool (forall ((l1_s0 Int))
         (let ((l1_s1 (f l1_s0)))
         true)))
[SYNC] Attempting to synchronize with tag: "terminating upon unexpected response (at: 2024-07-11 15:46:38.719348374 PDT)"
[FIRE] (echo "terminating upon unexpected response (at: 2024-07-11 15:46:38.719348374 PDT)")
[SYNC] Synchronization achieved using tag: "terminating upon unexpected response (at: 2024-07-11 15:46:38.719348374 PDT)"
*** Exception: 
*** Data.SBV: Unexpected response from the solver, context: define-fun:
***
***    Sent      : (define-fun s0 () Bool (forall ((l1_s0 Int))
***                  (let ((l1_s1 (f l1_s0)))
***                  true)))
***    Expected  : success
***    Received  : (error "line 8 column 23: unknown constant f (Int) ")
***
***    Executable: z3
***    Options   : -nw -in -smt2

A current workaround I am using is to add a dummy constraint to declare the ufunc:

pab :: IO SBVTC.CheckSatResult
pab = SBV.runSMTWith SBV.z3 {SBV.verbose = True} $ do
  let f = SBV.uninterpret "f" :: SBV.SInteger -> SBV.SInteger
  SBVC.query $ do
    SBV.constrain $ f 1 SBV..== f 1
    SBV.constrain $
      \(SBV.Forall (b :: SBV.SInteger)) ->
        f b SBV..== f b
    SBVC.checkSat

Note that the constraint must be declared before the constraint with forall, and the following code would crash

pab :: IO SBVTC.CheckSatResult
pab = SBV.runSMTWith SBV.z3 {SBV.verbose = True} $ do
  let f = SBV.uninterpret "f" :: SBV.SInteger -> SBV.SInteger
  SBVC.query $ do
    SBV.constrain $
      \(SBV.Forall (b :: SBV.SInteger)) ->
        f b SBV..== f b
    SBV.constrain $ f 1 SBV..== f 1
    SBVC.checkSat

[LeventErkok]

This is a known issue, unfortunately. The "laziness" of execution can sometimes hide things from the symbolic engine. The "official" workaround is:

p = runSMTWith z3 {verbose = True} $ do
  let f = uninterpret "f" :: SInteger -> SInteger
  registerUISMTFunction f
  query $ do
    constrain $ \(Forall (b :: SInteger)) -> f b .== f b
    checkSat

Note the call to registerUISMTFunction whose sole existence is to help with problems like this.

I'm not sure if there's much value in pursuing this to the bitter end; I come across this occasionally, and registerUISMTFunction usually does the trick. If you do end up identifying a fix though, I'd love to hear.

[lsrcz]

Thank you, I'll try it out. A guaranteed workaround is sufficient for me. It might be useful to mention this in the documentation of uninterpreted functions.

Would it be a good idea to provide a function that combines the declaration and registration? Something like:

p = runSMTWith z3 {verbose = True} $ do
  f :: SInteger -> SInteger <- getUninterpret "f"
  query $ do
    constrain $ \(Forall (b :: SInteger)) -> f b .== f b
    checkSat

where

getUninterpret name = do
  let f = uninterpret name
  registerUISMTFunction f
  return f

[LeventErkok]

More/better documentation is always welcome! Please submit a PR.

Regarding getUninterpret: I'm a little weary of the plethora of functions we already have. Do you think it'll make the user experience any better?

[lsrcz]

Sure, I added some documentation to the issue. Please review it.

For the additional API, I am also unsure about it, so I was asking :). Given that I only observed the issue when using quantifiers, it might be okay to stick with the current workaround.

[LeventErkok]

yeah; I don't see much ROI in investigating this in any further depth. Feel free to close the ticket; though if you want to spend some cycles trying to see if we can improve the situation that's fine as well.

[lsrcz]

One more thing I noticed about this issue is that the registration function requires the MonadSymbolic constraint, which is only available for Query, but not for QueryT m. Is this intentional, or there is a missing instance?

[lsrcz]

If the missing instance is intentional, then we cannot do this trick if we are declaring uninterpreted functions in a QueryT m environment, and that's what I am doing.

It turns out that the registerUISMTFunction function might also be overly-constrained though. The MonadSymbolic constraint can be removed from that function as well as from smtFunName, and the system still builds.

Do you think this is a good idea?

[LeventErkok]

If it builds with smaller set of constraints, that'd be just fine. Please do a PR

[LeventErkok]

@lsrcz Thinking about making a release sometime this weekend.. Can we close this ticket, or do you still want to fix up a few things here?

[lsrcz]

Hi @LeventErkok, I will close the ticket for now. Maybe come back to it in the future when I got some time to have a look..