Solver.hs

-- | Correctness of sat solver as in Trellys
-- | http://www.seas.upenn.edu/~sweirich/papers/popl14-trellys.pdf

-- | This code is terrible.
-- | Should use cases and auto translate like in the paper's theory
-- | Also, &&, not and rest logical operators are not in scope in the axioms

{-@ LIQUID "--higherorder"     @-}
{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--pruneunsorted"   @-}

-- TAG: absref 
-- TAG: termination

module Solver where

import Data.Tuple
import Data.List (nub)
import Language.Haskell.Liquid.Prelude ((==>))
import Prelude hiding (map)

-- | Formula
type Var     = Int
data Lit     = Pos Var | Neg Var
type Clause  = L Lit
type Formula = L Clause

-- | Assignment

type Asgn = L (P Var Bool)

-- | Top-level "solver"


{-@ solve :: f:Formula -> Maybe {a:Asgn | sat a f } @-}
solve   :: Formula -> Maybe Asgn
solve f = find (`sat` f) (asgns f)

{-@ find :: forall <p :: a -> Bool, w :: a -> Bool -> Bool>. 
            {y::a, b::{v:Bool<w y> | v} |- {v:a | v == y} <: a<p>}
            (x:a -> Bool<w x>) -> [a] -> Maybe (a<p>) @-}
find :: (a -> Bool) -> [a] -> Maybe a
find f [] = Nothing
find f (x:xs) | f x       = Just x
              | otherwise = Nothing


-- | Generate all assignments

asgns :: Formula -> [Asgn] -- generates all possible T/F vectors
asgns = go . vars
  where
  	go []     = []
  	go (x:xs) = let ass = go xs in (inject (P x True) ass) ++ (inject (P x False) ass)

  	inject x xs = (\y -> x:::y) <$> xs

vars :: Formula -> [Var]
vars = nub . toList .  go
  where
  	go Emp       = Emp
  	go (ls:::xs) = map go' ls `append` go xs

  	go' (Pos x) = x
  	go' (Neg x) = x


{-@ axiomatize sat @-}
sat :: Asgn -> Formula -> Bool
{-@ sat :: Asgn -> f:Formula -> Bool / [llen f] @-}
sat a f
  | llen f == 0
  = True
  | satClause a (hd f)
  = sat a (tl f)
  | otherwise
  = False

{-@ axiomatize satClause @-}
{-@ satClause :: Asgn -> c:Clause -> Bool /[llen c] @-}
satClause :: Asgn -> Clause -> Bool
satClause a c
  | llen c == 0
  = False
  | satLit a (hd c)
  = True
  | otherwise
  = satClause a (tl c)

{-@ axiomatize satLit @-}
satLit :: Asgn -> Lit -> Bool
satLit a l
  | isPos l   = isPosVar (fromPos l) a
  | isNeg l   = isNegVar (fromNeg l) a
  | otherwise = False

{-@ axiomatize isPosVar @-}
{-@ axiomatize isNegVar @-}
{-@ isNegVar :: Var -> a:Asgn -> Bool / [llen a] @-}
{-@ isPosVar :: Var -> a:Asgn -> Bool / [llen a] @-}
isNegVar, isPosVar :: Var -> Asgn -> Bool
isPosVar v a
  | llen a == 0
  = False
  | (myfst (hd a)) == v
  = mysndB (hd a)
  | otherwise
  = isPosVar v (tl a)


isNegVar v a
  | llen a == 0
  = False
  | (myfst (hd a)) == v
  = if mysndB (hd a) then False else True
  | otherwise
  = isNegVar v (tl a)


{-@ measure myfst @-}
myfst :: P a b -> a
myfst (P x _) = x


{-@ measure mysndB @-}
mysndB :: P a Bool -> Bool
mysndB (P _ x) = x

{-@ measure isPos @-}
isPos (Pos _) = True
isPos _       = False

{-@ measure fromPos @-}
{-@ fromPos :: {l:Lit | isPos l} -> Var @-}
fromPos :: Lit -> Var
fromPos (Pos v) = v

{-@ measure isNeg @-}
isNeg (Neg _) = True
isNeg _       = False

{-@ measure fromNeg @-}
{-@ fromNeg :: {l:Lit | isNeg l} -> Var @-}
fromNeg :: Lit -> Var
fromNeg (Neg v) = v


-- Pairs
data P a b = P a b

-- List definition
data L a = Emp | a ::: L a
{-@ data L [llen] @-}

toList Emp      = []
toList (x ::: xs) = x:toList xs

{-@ measure llen @-}
llen :: L a -> Int
{-@ llen :: L a -> Nat @-}
llen Emp        = 0
llen (_ ::: xs) = 1 + llen xs

{-@ measure hd @-}
{-@ hd :: {v:L a | llen v > 0 } -> a @-}
hd :: L a -> a
hd (x ::: _) = x

{-@ measure tl @-}
{-@ tl :: xs:{L a | llen xs > 0 } -> {v:L a | llen v == llen xs - 1 } @-}
tl :: L a -> L a
tl (_ ::: xs) = xs


{-@ axiomatize append @-}
append :: L a -> L a -> L a
append xs ys
  | llen xs == 0 = ys
  | otherwise    = hd xs ::: append (tl xs) ys
  {-@ axiomatize map @-}

map :: (a -> b) -> L a -> L b
map f xs
    | llen xs == 0 = Emp
    | otherwise    = f (hd xs) ::: map f (tl xs)