module Lava.Satzoo
( satzoo
)
where
import Lava.Signal
import Lava.Netlist
import Lava.Generic
import Lava.Sequent
import Lava.Property
import Lava.Error
import Lava.LavaDir
import Lava.Verification
import Data.List
( intersperse
, nub
)
import System.IO
( openFile
, IOMode(..)
, hPutStr
, hClose
)
import Lava.IOBuffering
( noBuffering
)
import Data.IORef
import System.Process (system)
import System.Exit (ExitCode(..))
satzoo :: Checkable a => a -> IO ProofResult
satzoo :: a -> IO ProofResult
satzoo a :: a
a =
do IO ()
checkVerifyDir
IO ()
noBuffering
(props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
String -> IO () -> IO ProofResult
proveFile String
defsFile (String -> [Signal Bool] -> IO ()
writeDefinitions String
defsFile [Signal Bool]
props)
where
defsFile :: String
defsFile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.cnf"
writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
writeDefinitions :: String -> [Signal Bool] -> IO ()
writeDefinitions file :: String
file props :: [Signal Bool]
props =
do Handle
firstHandle <- String -> IOMode -> IO Handle
openFile String
firstFile IOMode
WriteMode
Handle
secondHandle <- String -> IOMode -> IO Handle
openFile String
secondFile IOMode
WriteMode
IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0
IORef Integer
cls <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0
Handle -> String -> IO ()
hPutStr Handle
firstHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ "c Generated by Lava"
, "c "
]
let new :: IO Integer
new =
do Integer
n <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
var
let n' :: Integer
n' = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1
IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
var Integer
n'
Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n'
clause :: [a] -> IO ()
clause xs :: [a]
xs =
do Integer
n <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
cls
let n' :: Integer
n' = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1 in Integer
n' Integer -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
cls Integer
n'
Handle -> String -> IO ()
hPutStr Handle
secondHandle ([String] -> String
unwords [ a -> String
forall a. Show a => a -> String
show a
x | a
x <- [a]
xs ] String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 0\n")
define :: s -> S s -> IO ()
define v :: s
v s :: S s
s =
case S s
s of
Bool True -> [s] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ s
v ]
Bool False -> [s] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ -s
v ]
Inv x :: s
x -> [s] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ -s
x, -s
v ] IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [s] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ s
x, s
v ]
And [] -> s -> S s -> IO ()
define s
v (Bool -> S s
forall s. Bool -> S s
Bool Bool
True)
And xs :: [s]
xs -> s -> [s] -> IO ()
forall a. (Show a, Num a) => a -> [a] -> IO ()
conjunction s
v [s]
xs
Or [] -> s -> S s -> IO ()
define s
v (Bool -> S s
forall s. Bool -> S s
Bool Bool
False)
Or xs :: [s]
xs -> s -> [s] -> IO ()
forall a. (Show a, Num a) => a -> [a] -> IO ()
conjunction (-s
v) ((s -> s) -> [s] -> [s]
forall a b. (a -> b) -> [a] -> [b]
map s -> s
forall a. Num a => a -> a
negate [s]
xs)
Xor [] -> s -> S s -> IO ()
define s
v (Bool -> S s
forall s. Bool -> S s
Bool Bool
False)
Xor xs :: [s]
xs -> s -> [s] -> IO ()
forall a. (Show a, Num a) => a -> [a] -> IO ()
exactly1 s
v [s]
xs
VarBool s :: String
s -> Handle -> String -> IO ()
hPutStr Handle
firstHandle ("c " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ s -> String
forall a. Show a => a -> String
show s
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
DelayBool x :: s
x y :: s
y -> Error -> IO ()
forall a. Error -> a
wrong Error
Lava.Error.DelayEval
_ -> Error -> IO ()
forall a. Error -> a
wrong Error
Lava.Error.NoArithmetic
where
conjunction :: a -> [a] -> IO ()
conjunction v :: a
v xs :: [a]
xs =
do [a] -> IO ()
forall a. Show a => [a] -> IO ()
clause (a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. Num a => a -> a
negate [a]
xs)
[IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ [a] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ -a
v, a
x ] | a
x <- [a]
xs ]
exactly1 :: a -> [a] -> IO ()
exactly1 v :: a
v xs :: [a]
xs =
do [a] -> IO ()
forall a. Show a => [a] -> IO ()
clause (-a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)
[IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ [a] -> IO ()
forall a. Show a => [a] -> IO ()
clause [ -a
v, -a
x, -a
y ] | (x :: a
x,y :: a
y) <- [a] -> [(a, a)]
forall b. [b] -> [(b, b)]
pairs [a]
xs ]
[IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ [a] -> IO ()
forall a. Show a => [a] -> IO ()
clause ( a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: -a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys) | (x :: a
x,ys :: [a]
ys) <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
pick [a]
xs ]
pairs :: [b] -> [(b, b)]
pairs [] = []
pairs (x :: b
x:xs :: [b]
xs) = [ (b
x,b
y) | b
y <- [b]
xs ] [(b, b)] -> [(b, b)] -> [(b, b)]
forall a. [a] -> [a] -> [a]
++ [b] -> [(b, b)]
pairs [b]
xs
pick :: [a] -> [(a, [a])]
pick [] = []
pick (x :: a
x:xs :: [a]
xs) = (a
x,[a]
xs) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [ (a
y,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys) | (y :: a
y,ys :: [a]
ys) <- [a] -> [(a, [a])]
pick [a]
xs ]
Struct Integer
outvs <- IO Integer
-> (Integer -> S Integer -> IO ())
-> Struct Symbol
-> IO (Struct Integer)
forall (f :: * -> *) v.
Sequent f =>
IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistIO IO Integer
new Integer -> S Integer -> IO ()
forall s. (Show s, Num s) => s -> S s -> IO ()
define ([Signal Bool] -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct [Signal Bool]
props)
[Integer] -> IO ()
forall a. Show a => [a] -> IO ()
clause ((Integer -> Integer) -> [Integer] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> Integer
forall a. Num a => a -> a
negate (Struct Integer -> [Integer]
forall a. Struct a -> [a]
flatten Struct Integer
outvs))
Integer
nvar <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
var
Integer
ncls <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
cls
Handle -> String -> IO ()
hPutStr Handle
firstHandle ("p cnf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
nvar String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
ncls String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
Handle -> IO ()
hClose Handle
firstHandle
Handle -> IO ()
hClose Handle
secondHandle
String -> IO ExitCode
system ("cat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
firstFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
secondFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file)
String -> IO ExitCode
system ("rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
firstFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
secondFile)
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
firstFile :: String
firstFile = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-1"
secondFile :: String
secondFile = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "-2"
proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
do String -> IO ()
putStr "Satzoo: "
IO ()
before
String -> IO ()
putStr "... "
String
lavadir <- IO String
getLavaDir
ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/satzoo.wrapper "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file
String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime"
)
let res :: ProofResult
res = case ExitCode
x of
ExitSuccess -> ProofResult
Valid
ExitFailure 1 -> ProofResult
Indeterminate
ExitFailure _ -> ProofResult
Falsifiable
String -> IO ()
putStrLn (ProofResult -> String
forall a. Show a => a -> String
show ProofResult
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".")
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res