Кодирование расширенных натуральных чисел в SBV - PullRequest
Новая
       31

Кодирование расширенных натуральных чисел в SBV

0 голосов
/ 23 ноября 2018

Я экспериментирую со следующим способом кодирования расширенных натуральных чисел в SMT-LIB (я определяю тип данных, аналогичный 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)

Как я собираюсь кодировать это в SBV?Я попробовал следующее, но это просто разбил SBV.Также я почему-то сомневаюсь, что это будет делать то, что я хочу, но я недостаточно знаком с тем, как работает SBV. 

!/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

1 Ответ

0 голосов
/ 23 ноября 2018

Основная проблема здесь заключается в том, что ваш код смешивает конкретный тип Maybe на Haskell и пытается рассматривать его как символический объект.Но вы на правильном пути к тому, как вы реализовали это в SMT-Lib2: вам по сути нужно написать соответствующий код в SBV.

Я бы начал с: 

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

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

Это просто шаблон;и вам не нужен импорт Data.SBV.Control, если вы не хотите использовать режим запроса, но, как мы увидим, он пригодится.

Первое, что нужно сделать, это закодировать ваш тип IntXсимволически;так же, как вы сделали в 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>"

Ничто из вышеперечисленного не должно удивлять, кроме, возможно, получения Generic и Mergeable.Это просто позволяет SBV использовать ite для ваших расширенных натуральных объектов.Также обратите внимание, как экземпляр Show осторожен в различении конкретных и символических значений с помощью unliteral.

Далее мы добавим несколько удобных функций, опять же ничего удивительного: 

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))

Теперь мы можем сделать IntX число: 

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

(Обратите внимание, что семантика этого означает oo - oo = oo, что в лучшем случае сомнительно. Но это помимо сути. Возможно, вам придется явно определить - и разберитесь с этим, как хотите. Аналогичные комментарии применимы к signum.)

Поскольку вы хотите проверить на равенство, мы также должны определить символическую версию этого: 

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

Аналогично, если вы хотите сравнить, вам нужно определить экземпляр OrdSymbolic;но идея остается прежней.

Нам нужен способ создания символических расширенных натуральных чисел.Следующая функция делает это красиво: 

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

Строго говоря, вам не нужно называть переменные.(т. е. параметр nm не требуется.) Но я считаю полезным всегда называть мои переменные по очевидным причинам.

Теперь мы можем написать ваш пример: 

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

Когда я запускаю это, я получаю: 

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

Я думаю, именно это вы и искали.

Когда вы работаете с более крупными программами, полезно иметь возможностьизвлекать IntX значения более напрямую и программировать их дальше.Это когда режим запроса пригодится.Сначала помощник: 

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

Теперь мы можем кодировать: 

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

И мы получаем: 

*Main> ex2
IntX Nothing

Надеюсь, это поможет.Я положил весь этот код в суть: https://gist.github.com/LeventErkok/facfd067b813028390c89803b3a0e887

...