Encoding extended naturals in SBV

Question

I'm experimenting with the following way of encoding extended naturals in SMT-LIB (I define a datatype analogous to Maybe Integer):

; extended integers -- if first field is true, then the value is infinity
(declare-datatypes () ((IntX (mk-int-x (is-infty Bool) (not-infty Int)))))

; addition
(define-fun plus ((x IntX) (y IntX)) IntX
  (ite (or (is-infty x) (is-infty y))
           (mk-int-x true 0)
           (mk-int-x false (+ (not-infty x) (not-infty y)))))

(declare-fun x () IntX)
(assert (= x (plus x (mk-int-x false 1))))
; x = x+1 when x |-> infty
(get-model)
(exit)

How would I go about to encode this in SBV? I tried the following, but that just crashed SBV. Also I somehow doubt that this would do what I want, but I'm not familiar enough with how SBV works.

!/usr/bin/env stack
{- stack script
  --resolver nightly-2018-11-23
  --package sbv
  --package syb
-}

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Generics
import Data.SBV

data IntX = IntX (Maybe Integer) deriving (Eq, Ord, Data, Read, Show, SymWord, HasKind)

pretty :: IntX -> String
pretty = \case
  IntX Nothing -> "∞"
  IntX n -> show n

instance Num IntX where
  (+) (IntX x) (IntX y) = IntX $ (+) <$> x <*> y
  (*) (IntX x) (IntX y) = IntX $ (*) <$> x <*> y
  fromInteger = IntX . Just

ex1 = sat $ do
  x :: SBV IntX <- free "x"
  return $ x .== x + 1

main :: IO ()
main = print =<< ex1

---

~/temp ✘ ./sbv.hs
sbv.hs: SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: s0 + s1
CallStack (from HasCallStack):

  error, called at ./Data/SBV/SMT/SMTLib2.hs:681:13 in sbv-7.12-9AiNAYtrUhB8YA6mr6BTn4:Data.SBV.SMT.SMTLib2

Answer 1

The fundamental issue here is that your code is mixing Haskell's concrete Maybe type and trying to treat it as a symbolic object. But you're on the right track with how you implemented that in SMT-Lib2: You essentially need to write the corresponding code in SBV.

I'd start with:

{-# LANGUAGE DeriveAnyClass  #-}
{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE NamedFieldPuns  #-}

import Data.SBV
import Data.SBV.Control
import GHC.Generics (Generic)

This is just boilerplate; and you don't need the Data.SBV.Control import unless you want to use the query mode, but it does come in handy as we shall see.

The first thing to do is to encode your IntX type symbolically; just like you did in SMTLib:

data SIntX = SIntX { isInf :: SBool
                   , xVal  :: SInteger
                   }
                   deriving (Generic, Mergeable)

instance Show SIntX where
  show (SIntX inf val) = case (unliteral inf, unliteral val) of
                           (Just True,  _)      -> "oo"
                           (Just False, Just n) -> show n
                           _                    -> "<symbolic>"

Nothing above should be surprising, except perhaps the deriving of Generic and Mergeable. It simply enables SBV to be able to use ite on your extended naturals. Also note how the Show instance is careful in distinguishing concrete and symbolic values by using unliteral.

Next, we add a few convenience functions, again nothing surprising:

inf :: SIntX
inf = SIntX { isInf = true, xVal = 0 }

nat :: SInteger -> SIntX
nat v = SIntX { isInf = false, xVal = v }

liftU :: (SInteger -> SInteger) -> SIntX -> SIntX
liftU op a = ite (isInf a) inf (nat (op (xVal a)))

liftB :: (SInteger -> SInteger -> SInteger) -> SIntX -> SIntX -> SIntX
liftB op a b = ite (isInf a ||| isInf b) inf (nat (xVal a `op` xVal b))

Now we can make IntX a number:

instance Num SIntX where
  (+)         = liftB (+)
  (*)         = liftB (*)
  negate      = liftU negate
  abs         = liftU abs
  signum      = liftU signum
  fromInteger = nat . literal

(Note that the semantics of this means oo - oo = oo, which is at best questionable. But that's besides the point. You might have to explicitly define - and deal with that as you wish. Similar comments apply for signum.)

Since you want to test for equality, we also have to define the symbolic version of that:

instance EqSymbolic SIntX where
  a .== b = ite (isInf a &&& isInf b) true
          $ ite (isInf a ||| isInf b) false
          $ xVal a .== xVal b

Similarly, if you want to compare, you'll have to define an OrdSymbolic instance; but the idea remains the same.

We need a way to create symbolic extended naturals. The following function does it nicely:

freeSIntX :: String -> Symbolic SIntX
freeSIntX nm = do i <- sBool    $ nm ++ "_isInf"
                  v <- sInteger $ nm ++ "_xVal"
                  return $ SIntX { isInf = i, xVal = v }

Strictly speaking, you don't need to name the variables. (i.e., the nm parameter isn't needed.) But I find it helpful to always name my variables for obvious reasons.

Now, we can code your example:

ex1 :: IO SatResult
ex1 = sat $ do x <- freeSIntX "x"
               return $ x .== x+1

When I run this, I get:

*Main> ex1
Satisfiable. Model:
  x_isInf = True :: Bool
  x_xVal  =    0 :: Integer

Which is what you were looking for, I believe.

When you're dealing with larger programs, it's beneficial to be able to extract IntX values more directly and program further with them. This is when the query mode comes in handy. First, a helper:

data IntX = IntX (Maybe Integer) deriving Show

queryX :: SIntX -> Query IntX
queryX (SIntX {isInf, xVal}) = do
          b <- getValue isInf
          v <- getValue xVal
          return $ IntX $ if b then Nothing
                               else Just v

Now we can code:

ex2 :: IO ()
ex2 = runSMT $ do x <- freeSIntX "x"
                  constrain $ x .== x+1

                  query $ do cs <- checkSat
                             case cs of
                               Unk   -> error "Solver said Unknown!"
                               Unsat -> error "Solver said Unsatisfiable!"
                               Sat   -> do v <- queryX x
                                           io $ print v

And we get:

*Main> ex2
IntX Nothing

I hope this helps. I've put all this code in a gist: https://gist.github.com/LeventErkok/facfd067b813028390c89803b3a0e887