Argthtjtr

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

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