`unknown constant` error for axioms over uninterpreted functions + uninterpreted sorts

[octalsrc]

Is there a "proper" way to avoid the unknown constant error when using addAxiom for uninterpreted functions over uninterpreted sorts?

(Also, while searching for a solution, I seem to have found a bug in registerUISMTFunction)

My goal is to:

1. Declare an uninterpreted sort
2. Declare some uninterpreted functions over that sort
3. Add axioms over those functions
4. Prove some theorems using the axioms

However, trying to prove a theorem that does not reference all axiom-covered functions results in the unknown constant error.

The Unknown Constant error

(I tested my examples using sbv-9.1, the current latest version on Hackage)

Here's a small example of the problem:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}

module SmtTest where

import Data.SBV
import Data.SBV.Control

-- 1. Declare an uninterpreted sort

data Thing

mkUninterpretedSort ''Thing

-- 2. Declare some uninterpreted functions over that sort

thingCompare :: SBV Thing -> SBV Thing -> SBV Bool
thingCompare = uninterpret "thingCompare"

thingMerge :: SBV Thing -> SBV Thing -> SBV Thing
thingMerge = uninterpret "thingMerge"

-- 3. Add axioms over those functions

axioms =
  -- thingCompare is reflexive
  ["(assert (forall ((k1 Thing))"
  ,"  (thingCompare k1 k1)))"
  -- thingMerge produces a new, distinct thing
  ,"(assert (forall ((k1 Thing) (k2 Thing))"
  ,"  (distinct k1 (thingMerge k1 k2))))"
  ]

-- 4. Prove some theorems using the axioms

testThings = prove $ do
  addAxiom "things" axioms
  k1 <- sbvForall_
  k2 <- sbvForall_

  -- Check that thingCompare is reflexive
  return $ (k1 .== k2) .=> (thingCompare k1 k2)

Running testThings produces the following error:

*** Exception:
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (assert (forall ((k1 Thing) (k2 Thing))
***                  (distinct k1 (thingMerge k1 k2))))
***    Expected  : success
***    Received  : (error "line 15 column 32: unknown constant thingMerge (Thing Thing) ")

I understand that thingMerge is unknown because SBV never sends its declaration to the solver, due to thingMerge not appearing in the actual SBV expression.

Is there a nice way to manually ask SBV to declare a set of uninterpreted functions, so that a collection of axioms defined over those functions never produces the unknown constant error?

Using registerUISMTFunction encounters a bug

Searching for a solution, I saw this issue comment that seemed to recommend registerUISMTFunction for this problem. Unfortunately, this function did not help me.

Here is an updated version of testThings, in which I attempt to use registerUISMTFunction to force thingMerge to be declared.

testThings = prove $ do
  addAxiom "things" axioms

  -- Force SBV to declare thingMerge?
  registerUISMTFunction thingMerge

  k1 <- sbvForall_
  k2 <- sbvForall_
  -- Check that thingCompare is reflexive
  return $ (thingCompare k1 k2) .=> (k1 .== k2)

Running this version of testThings produces the following error, which claims to be a bug:

*** Exception:
*** Data.SBV.smtFunSaturate: Impossible happened!
*** Unable to create a valid parameter for kind: Thing
*** Please report this as an SBV bug!

I believe this is related to Thing being an uninterpreted sort: it seems that using registerUISMTFunction on any function over an uninterpreted sort produces this error.

It's also possible that I've misunderstood the purpose of registerUISMTFunction, and I'm using it in a completely wrong way.

The workaround I've been using

To avoid these errors, I've been using a workaround: adding tautological constraints that reference all axiom-covered uninterpreted functions, so that they all get declared.

testThings = prove $ do
  addAxiom "things" axioms
  k1 <- sbvForall_
  k2 <- sbvForall_

  -- Use thingMerge trivially, so that it gets declared
  constrain $ thingMerge k1 k2 .== thingMerge k1 k2

  -- Check that thingCompare is reflexive
  return $ (k1 .== k2) .=> (thingCompare k1 k2)

*** Exit code: ExitSuccess
Q.E.D.

This works, but it gets tedious for many functions with many arguments, and I'm worried that it makes the solving process less efficient by adding more constraints, even if they're tautological.

Using registerUISMTFunction or some equivalent would be preferable, if that worked.

Thanks!

Just wanted to say, I've found SBV to be an very useful library for experimenting with tools built around SMT solvers—thanks so much for developing and maintaining it!

[LeventErkok]

Your workaround is the only way to handle this case right now. I'll see if I can add functionality to make it simpler.

[LeventErkok]

@octalsrc

I've put in a patch that should handle this case. Note that you have to use the registerUISMTFunction, which takes care of telling the solver the existence of these types.

Let me know if that works as expected..

[octalsrc]

Yes, registerUISMTFunction now fixes the unknown constant error in the way that I expected it to. Thanks for the quick fix!

For the record, here is the complete example that now works:

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}

module SmtTest where

import Data.SBV
import Data.SBV.Control

-- 1. Declare an uninterpreted sort

data Thing

mkUninterpretedSort ''Thing

-- 2. Declare some uninterpreted functions over that sort

thingCompare :: SBV Thing -> SBV Thing -> SBV Bool
thingCompare = uninterpret "thingCompare"

thingMerge :: SBV Thing -> SBV Thing -> SBV Thing
thingMerge = uninterpret "thingMerge"

-- 3. Add axioms over those functions

axioms =
  -- thingCompare is reflexive
  ["(assert (forall ((k1 Thing))"
  ,"  (thingCompare k1 k1)))"
  -- thingMerge produces a new, distinct thing
  ,"(assert (forall ((k1 Thing) (k2 Thing))"
  ,"  (distinct k1 (thingMerge k1 k2))))"
  ]

-- 4. Prove some theorems using the axioms

testThings = prove $ do
  addAxiom "things" axioms

  -- Force SBV to declare thingMerge; this is needed because
  -- thingMerge is not used outside the axioms.
  registerUISMTFunction thingMerge

  k1 <- sbvForall_
  k2 <- sbvForall_
  return $ (k1 .== k2) .=> (thingCompare k1 k2)

[LeventErkok]

@octalsrc Glad to hear it's resolved.

I might do a release in a few days time to hackage to get it out there. In the meantime, I hope using a local copy is OK for your purposes. (Or you can always use the workaround you discovered, by adding a constraint that uses the type in a trivial way.)

[LeventErkok]

@octalsrc SBV 9.2 is now on hackage, with this fix included: https://hackage.haskell.org/package/sbv

Thanks for the report.