Get more information on model

[buggymcbugfix]

Z3 is giving a lot more information in its model than what is returned by SBV. Is there a way of getting the whole model that Z3 produces?

Example

(declare-sort U)
(declare-const m U)
(declare-const s U)
(declare-fun Mult (U U) U)

(assert (exists ((v U) (x U) (t U)) (and (and (= x m) (= t s))
                                          (= v (Mult x t)))))
(check-sat)
(get-model)

The above gives the following model in Z3:

sat
(model 
  ;; universe for U:
  ;;   U!val!1 U!val!0 U!val!2 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun U!val!1 () U)
  (declare-fun U!val!0 () U)
  (declare-fun U!val!2 () U)
  ;; cardinality constraint:
  (forall ((x U)) (or (= x U!val!1) (= x U!val!0) (= x U!val!2)))
  ;; -----------
  (define-fun x!1 () U
    U!val!0)
  (define-fun s () U
    U!val!1)
  (define-fun t!0 () U
    U!val!1)
  (define-fun v!2 () U
    U!val!2)
  (define-fun m () U
    U!val!0)
  (define-fun Mult ((x!0 U) (x!1 U)) U
    (ite (and (= x!0 U!val!0) (= x!1 U!val!1)) U!val!2
      U!val!2))
)

The equivalent in SBV is only giving back this:

Satisfiable. Model:
  units(v) = Units :: Units
  units(x) = Units :: Units
  units(t) = Units :: Units

[LeventErkok]

The answer is "depends," as usual. But before we discuss exactly what you mean by "extra-information" can you share your SBV program that produced that? Perhaps there might be a slightly better way to do so. We can take the discussion from there.

[buggymcbugfix]

So when I said "equivalent", I should have probably said "something similar".

What we wrote is the following (sloppy code, just toying around):

type SUnits = SBV Units

data Units = Units
   deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SatModel)

mul :: SUnits -> SUnits -> SUnits
mul = uninterpret "MUL"

add :: SUnits -> SUnits -> SUnits
add = uninterpret "ADD"

example2 =  do
  satResult <- sat predicate
  thmResult <- prove predicate
  case thmResult of
    ThmResult (Unknown _ model) -> putStrLn $ "Unknown: " ++ show model
    _ -> return ()
  print $ satResult
  case satResult of
    SatResult (Unknown _ model) -> do
      putStrLn $ "Unknown (SAT): " ++ show model
    _ -> return ()
  return (satResult, thmResult)
  where
    predicate = do
      addAxiom "comm" [ "(assert (forall ((u Units) (v Units))"
                      , "  (= (MUL u v)"
                      , "     (MUL v u))))" ]

      let m = literal Units
      let s = literal Units

      (uv :: SUnits) <- exists "units(v)"
      (ux :: SUnits) <- exists "units(x)"
      (ut :: SUnits) <- exists "units(t)"

      let sig1 = uv .== (ux `mul` ut) &&& ux .== m &&& ut .== s

      return $ sig1

Background info:

We are working on a refactoring tool for scientific programming in Fortran, written in Haskell. We provide facilities for annotating functions with unit information in order to flag unit mismatches like adding metres and seconds.

For units inference, we are using a hand-rolled constraint solver that relies on Gaussian elimination. We are building a single, huge constraint matrix.

The scientific simulations that we are targeting may well consist of millions of lines of Fortran, so you can imagine that we have efficiency problems with this approach. There is a lot that can be done to improve efficiency, but we thought we could take this as an opportunity to outsource this to an external constraint solver. We already have z3 and sbv as a dependency, but we are still unsure whether our units inference can be done with sbv as-is or whether we may need to extend it.

At any rate, many thanks for your excellent work on this package!

[LeventErkok]

I think SMT-Solvers would do a fantastic job with unit analysis, and SBV would be able to let you code it up just fine. Having said that, the SBV code you posted is quite unconventional, and it probably doesn't mean what you had in mind. In particular:

      let m = literal Units
      let s = literal Units

would make m and s exactly the same thing. (Note that this follows from Haskell and has nothing to do with SBV. Same RHS, same LHS.) Also, calling both sat/prove on the same goal sounds suspicious.

If you can answer a few questions, I might be able to give some suggestions:

• Do you have a fixed set of units? Or do you not know that ahead of time? (i.e., meters, seconds,.. etc., for a fixed sets, or does the system need to be able to deal with new units dynamically?) SBV can deal with both, but modeling them would be quite different.

• What sort of a property would you want to prove? A sample would be nice to see, doesn't have to be in SBV notation at all.

[buggymcbugfix]

Thank you for your comments concerning issues with my code.

Regarding your first question: we need to be able to deal with arbitrary units, given by the user, i.e. there is not a set of units that we know ahead of time.

Regarding your second question: I will give examples in pseudo-Haskell with units in angle brackets:

We are doing the following three things—

1. Check for consistent use of units

dist :: Double <m>
dist = 5

time :: Double <s>
time = 2

time' :: Double <s>
time' = dist -- bad: unit mismatch

speed = dist / time -- good

speed' = dist + time -- bad: can't add quantities of different units!

2. Infer units

speed = dist / time -- should infer `speed :: Double <m s⁻¹>`

square x = x*x -- unit-polymorphic function

a = square dist -- should infer `a :: Double <m²>`
b = square time -- should infer `b :: Double <s²>`

3. Suggest a minimal (critical) set of variables to annotate

f = 4.76
s = 78.5
work = f * s
-- suggest `f`and `s` as critical, the unit of `work` can be derived

On top of this users can define unit aliases like <n> = <kg m s⁻²>, but I believe that this is not relevant here.

[LeventErkok]

I see. That sounds like a very cool project. A few notes:

• Even if you may have to deal with arbitrary units, I'm going to guess that by the time you actually check consistency you have the entire set. If that's the case, you should use an enumeration type instead of an uninterpreted sort in SBV, which will properly translate the constants back and forth. See this as an example: https://hackage.haskell.org/package/sbv-6.1/docs/Data-SBV-Examples-Misc-Enumerate.html

  • It is best to delay all constraints solving to the end and send them to the SMT solver in one shot. (You can use getUnsatCores to find minimal conflicting sets at the end.)

  • This problem sounds like it can be best dealt with as a type-inference sort of problem. Have you looked into those approaches? You can still use an SMT solver via SBV to discharge those type-checking constraints, but that could give you a better handle on the way to structure these. I'm sure you're well aware of the existing work regarding this.

I'll keep this ticket open and please feel free to ask further questions regarding SBV usage. For your original query about "can we get more out of the solver:" The answer is yes, as demonstrated by this example: https://hackage.haskell.org/package/sbv-6.1/docs/Data-SBV-Examples-Misc-Enumerate.html You cannot extract function values in general, but if you have a finite domain you can definitely enumerate the interesting points. If you come up with a more specific use case that you'd like SBV to support, I'd definitely be interested in looking into it.

Also, I'll mention in passing that the next release of SBV will have an interactive component; where you'll be able to query the SMT solver based on the results it returns, i.e., use it in an incremental fashion. That might be useful for you too. I expect that to be released within the next couple of weeks.

[buggymcbugfix]

Thank you for your pointers, very much appreciated!

So I've been playing around a little and I have come up with the following:

test :: IO SatResult
test = sat $ do dist <- exists "dist"
                time <- exists "time"
                time' <- exists "time'"
                constrain $ (literal M) .== dist
                constrain $ (literal S) .== time
                constrain $ time .== time'
                return ()

Am I going to need to use Template Haskell to generate the constraints at runtime?

[LeventErkok]

That program fragment is essentially asking SBV to find an assignment for the variable time' such that it is equal to literal S. I doubt you meant that. Let's go the other way around: What do you want SBV to prove? (Or give you a model of?)

[buggymcbugfix]

I tried to encode a trivial program like this:

dist :: Double <m>
dist = 5

time :: Double <s>
time = 2

time' = time

Is my sbv example above not how you would do this?

Also, I'm still struggling to understand how we would generate this at runtime.

[buggymcbugfix]

By the way, to encode

dist :: Double <m>
dist = 5

time :: Double <s>
time = 2

time' = dist + time

I did the following:

uc :: Goal
uc = do dist <- exists "dist"
        time <- exists "time"
        time' <- exists "time'"

        setOption $ ProduceUnsatCores True

        namedConstraint "unit dist = m" $ (literal M) .== dist
        namedConstraint "unit time = s" $ (literal S) .== time
        namedConstraint "unit time = unit time'" $ time .== time'
        namedConstraint "unit dist = unit time'" $ dist .== time'

        query $ do cs <- checkSat
                   case cs of
                      Unsat -> do core <- getUnsatCore
                                  io $ putStrLn $ "Unsat core is: " ++ show core
                      _     -> io $ putStrLn "Problem is satisfiable."

                   sbvResume

[buggymcbugfix]

Sorry for the hassle, I will try and get a more experienced team member to help me with this before bugging you here. Unfortunately I'm not very experienced with sbv yet.

[LeventErkok]

Sure.. But it seems to me that you are conflating "inference" from "constraint solving."

I'd expect the inference phase to be similar to type-checking, where you'd solve the time = time' issue. This would be just percolating the types. No constraints needed.

Later on, when you see distance + time, you'd generate a constraint that the type of distance and type of time is "addable." SMT wouldn't tell you what that result be. It would tell you whether you can add them. The phase distinction is important here. All constraints should be generated ahead of time before SMT comes into picture.

I'd also recommend staying out of the query mode for the time being. It is under development and the details are changing daily. In any case, I don't think you need it to solve your problem anyhow.

[dorchard]

Hi Levent, Thanks for your comments. I am working with @vimuel on this. I think we have an idea of how to encode what we want into SMTLIB to pass to Z3 - but the output we see working with Z3 directly is not the output we are getting from SBV, possibly because SBV is not passing all the relevant information back to us. Going back to @vimuel's introductory example we gave Z3 the following SMT-LIB script:

(declare-sort U)
(declare-const m U)
(declare-const s U)
(declare-fun Mult (U U) U)

(assert (exists ((v U) (x U) (t U)) (and (and (= x m) (= t s))
                                          (= v (Mult x t)))))
(check-sat)
(get-model)

To which it responds with:

sat
(model 
  ;; universe for U:
  ;;   U!val!1 U!val!0 U!val!2 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun U!val!1 () U)
  (declare-fun U!val!0 () U)
  (declare-fun U!val!2 () U)
  ;; cardinality constraint:
  (forall ((x U)) (or (= x U!val!1) (= x U!val!0) (= x U!val!2)))
  ;; -----------
  (define-fun x!1 () U
    U!val!0)
  (define-fun s () U
    U!val!1)
  (define-fun t!0 () U
    U!val!1)
  (define-fun v!2 () U
    U!val!2)
  (define-fun m () U
    U!val!0)
  (define-fun Mult ((x!0 U) (x!1 U)) U
    (ite (and (= x!0 U!val!0) (= x!1 U!val!1)) U!val!2
      U!val!2))
)

This is exactly the information we need for this problem. We attempted to encode the same input using SBV (using uninterpreted sorts) with the following (cleaned-up version of what @vimuel posted):

type SUnits = SBV Units
data Units = Units
   deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SatModel)

mul :: SUnits -> SUnits -> SUnits
mul = uninterpret "MUL"

example =  do
   satResult <- sat predicate
   print satResult
  where
    predicate = do
      let m = literal Units
      let s = literal Units

      (v :: SUnits) <- exists "v"
      (x :: SUnits) <- exists "x"
      (t :: SUnits) <- exists "t"

      return $ v .== (x `mul` t) &&& x .== m &&& t .== s

However, the sat result we get out of SBV includes none of the information about MUL which Z3 give us. There are three possible explanations for this:

- We are translating our Z3 code incorrectly into SBV, so SBV is passing something semantically different to our original script to Z3.
- SBV is not giving us all the information from the SAT model.
- A combination of the above.

Any ideas which? I haven't been able to get any of the SBV examples to provide SAT information about uninterpreted function constants. This is what we need. Even if we use replace Units here with an enumeration, we still cannot get information about MUL.

[dorchard]

We also tried something like this (as an alternate approach to get something like our original Z3 input):

example2 =  do
  satResult <- sat predicate
  print satResult
  where
    predicate = do
      let (mul :: SUnits -> SUnits -> SUnits) = uninterpret "MUL"
      let (m :: SUnits) = uninterpret "m"
      let (s :: SUnits) = uninterpret "s"

      (v :: SUnits) <- exists "v"
      (x :: SUnits) <- exists "x"
      (t :: SUnits) <- exists "t"
      let sig1 = v .== (x `mul` t) &&& x .== m &&& t .== s
      return $ sig1

Is there a way we can more of Z3's model information out of SBV?

[LeventErkok]

Hi Dominic,

When you say:

Is there a way we can more of Z3's model information out of SBV?

I'm guessing you're referring to this output:

sat
(model 
  ;; universe for U:
  ;;   U!val!1 U!val!0 U!val!2 
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun U!val!1 () U)
  (declare-fun U!val!0 () U)
  (declare-fun U!val!2 () U)
  ;; cardinality constraint:
  (forall ((x U)) (or (= x U!val!1) (= x U!val!0) (= x U!val!2)))
  ;; -----------
  (define-fun x!1 () U
    U!val!0)
  (define-fun s () U
    U!val!1)
  (define-fun t!0 () U
    U!val!1)
  (define-fun v!2 () U
    U!val!2)
  (define-fun m () U
    U!val!0)
  (define-fun Mult ((x!0 U) (x!1 U)) U
    (ite (and (= x!0 U!val!0) (= x!1 U!val!1)) U!val!2
      U!val!2))
)

Can you tell me exactly which part of the Z3's output you'd like to obtain via SBV? Is it the definition of Mult it produces that you are after?

[dorchard]

Hi Levent- thanks for the response. Sorry for being unclear. Yes, that's exactly it: we would like to get the definition of Mult produced in the SAT model.

[dorchard]

Also we would really need all the define-funs coming out of the SAT solver.

[LeventErkok]

You cannot directly extract functions. The trick is to:

• Write point-values of interest explicitly
• Put in sufficient axioms to restrict the model domain

Then you can extract the function point-wise, which you can further process in Haskell.

Here's how I'd be inclined to code your example:

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveAnyClass     #-}

import Data.Generics
import Data.SBV

newtype Unit = Unit () deriving (Eq, Ord, Data, Read, Show, SymWord, HasKind)
type SUnit = SBV Unit

p :: Goal
p = do v <- free "v"
       x <- free "x"
       t <- free "t"

       let mul :: SUnit -> SUnit -> SUnit
           mul = uninterpret "mul"

           m, s :: SUnit
           m = uninterpret "m"
           s = uninterpret "s"

       constrain $ x .== m
       constrain $ t .== s
       constrain $ v .== mul x t

       -- Add a few axioms on mul's comm/assoc
       addAxiom "mul is commutative" [ "(assert (forall ((x Unit) (y Unit))"
                                     , "                (= (mul x y) (mul y x))))"
                                     ]

       addAxiom "mul is associative" [ "(assert (forall ((x Unit) (y Unit) (z Unit))"
                                     , "                (= (mul x (mul y z))"
                                     , "                   (mul (mul x y) z))))"
                                     ]

       -- extract the definition of mul via explicit query
       let mkMult (a, anm) (b, bnm) = do
                r <- free $ "mult(" ++ anm ++ ", " ++ bnm ++ ")"
                constrain $ r .== a `mul` b

       let elts = [(v, "v"), (x, "x"), (t, "t")]
       sequence_ [mkMult e1 e2 | e1 <- elts, e2 <- elts]

main :: IO ()
main = print =<< sat p

To which I get:

*Main> main
Satisfiable. Model:
  v          = Unit!val!2 :: Unit
  x          = Unit!val!0 :: Unit
  t          = Unit!val!1 :: Unit
  mult(v, v) = Unit!val!3 :: Unit
  mult(v, x) = Unit!val!4 :: Unit
  mult(v, t) = Unit!val!6 :: Unit
  mult(x, v) = Unit!val!4 :: Unit
  mult(x, x) = Unit!val!5 :: Unit
  mult(x, t) = Unit!val!2 :: Unit
  mult(t, v) = Unit!val!6 :: Unit
  mult(t, x) = Unit!val!2 :: Unit
  mult(t, t) = Unit!val!7 :: Unit

Note that in this case Z3 finds a "larger" model, which is still legitimate. You might have to add further axioms to equate some of those values to get a more compact model.

Is this what you are after?

I should add that the best way would be to actually not leave Unit uninterpreted, but use an enumerated type directly as we discussed before; if you happen to know which units are present in the system. That way you'll have a fully typed interaction, without the funky values like "Unit!val!0" etc. The example for something along those lines is here: https://hackage.haskell.org/package/sbv-6.1/docs/Data-SBV-Examples-Misc-Enumerate.html

[dorchard]

Thanks Levent. I'm not sure the above approach with querying every pair of possibly inputs to mult would scale well for our purposes in any case. That said, I think we've found a better approach overall, but the above suggested method is good to know. Many thanks.

[LeventErkok]

@dorchard Cool. If you are still using SBV in your new approach and run into issues, do let me know. I'm also interested in hearing applications, and also what we can further provide to make it an easier system to use.

[LeventErkok]

@vimuel @dorchard I'm closing this ticket as I clean-up issues for the new releases. Feel free to reopen if there's any action to be done on the SBV side.