{- CAO Compiler
Copyright (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see . -}
{- |
Module : $Header$
Description : Decision procedures for constraints
Copyright : (C) 2014 Cryptography and Information Security Group, HASLab - INESC TEC and Universidade do Minho
License : GPL
Maintainer : Paulo Silva
Stability : experimental
Portability : non-portable
-}
module Language.CAO.Typechecker.Solver
( valid
, valid'
) where
import Control.Monad
import Language.CAO.Common.Error
import Language.CAO.Common.Monad
import Language.CAO.Common.State
import Language.CAO.Common.Var
import Language.CAO.Index
import Language.CAO.Index.Eval
import Language.CAO.Typechecker.SMT
valid :: CaoMonad m => [ICond Var] -> ErrorCode Var -> m ()
valid i e = do
r <- validEval $ IAnd i
unless r $ tcError e
valid' :: CaoMonad m => [ICond Var] -> m Bool
valid' i = validEval $ IAnd i
validEval :: CaoMonad m => ICond Var -> m Bool
validEval c = case evalCond c of
IBool b -> return b
IAnd i -> do
hyp <- getHypothesis
case fromHyp hyp i of
IBool b -> return b
r -> checkValidity (IAnd hyp) r
_ -> error $ ": unexpected canonical form."
fromHyp :: [ICond Var] -> [ICond Var] -> ICond Var
fromHyp hyp cond = let
cond' = filter (not . checkHyp hyp) cond
in if null cond' then IBool True else IAnd cond'
where
checkHyp :: [ICond Var] -> ICond Var -> Bool
checkHyp hyp' c = any (exactHyp c) hyp'
exactHyp :: ICond Var -> ICond Var -> Bool
-- C, a |= a
exactHyp c h
| c == h = True
-- C, 0 <= a |= 0 <= b <== |= a <= b'
exactHyp (ILeq b) (ILeq a) = let
(n, c, i) = decompose b
(n', c', i') = decompose a
in if i == i'
then if evalBool [c .<. IInt 0, c' .<. IInt 0]
then evalBool [(n .*. c') .<=. (n' .*. c)]
else if evalBool [c .>. IInt 0, c' .>. IInt 0]
then evalBool [(n' .*. c) .<=. (n .*. c')]
else evalBool [a .<=. b]
else evalBool [a .<=. b]
exactHyp c (IAnd l) = checkHyp l c
exactHyp _ _ = False
evalBool :: [ICond Var] -> Bool
evalBool = toBool . evalCond . IAnd
toBool :: ICond Var -> Bool
toBool (IBool b) = b
toBool _ = False
-- (Term, Coeficient, Variable)
decompose :: IExpr Var -> (IExpr Var, IExpr Var, IExpr Var)
decompose (ISum [IInt n, IArith ITimes c i]) = (IInt n, c, i)
decompose (ISum [IInt n, i]) = (IInt n, IInt 1, i)
decompose (ISum [IArith ITimes c i]) = (IInt 0, c, i)
decompose (IArith ITimes c i) = (IInt 0, c, i)
decompose i = (IInt 0, IInt 1, i)