Кодирование расширенных натуральных чисел в SBV
Я экспериментирую со следующим способом кодирования расширенных натуральных чисел в 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 ответ
Фундаментальная проблема здесь в том, что ваш код смешивает бетон Хаскелла Maybe наберите и попытайтесь трактовать его как символический объект. Но вы на правильном пути к тому, как вы реализовали это в 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