{-# LANGUAGE CPP #-}
{- |
Module      :  ./CASL/CompositionTable/ModelChecker.hs
Description :  checks validity of models regarding a composition table
Copyright   :  (c) Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable

checks validity of models regarding a composition table
-}

module CASL.CompositionTable.ModelChecker (modelCheck) where

import CASL.CompositionTable.CompositionTable
import CASL.CompositionTable.ModelTable
import CASL.CompositionTable.ModelFormula
import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.ToDoc
import CASL.Logic_CASL
import Logic.Logic

import Common.AS_Annotation
import Common.Result
import Common.Id
import qualified Common.Lib.MapSet as MapSet
import Common.Utils

import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map

import Data.Function
import Data.Maybe
import Data.List

modelCheck :: Int -> (Sign () (), [Named (FORMULA ())])
           -> Table2 -> Result ()
modelCheck :: Int -> (Sign () (), [Named (FORMULA ())]) -> Table2 -> Result ()
modelCheck c :: Int
c (sign :: Sign () ()
sign, sent :: [Named (FORMULA ())]
sent) t :: Table2
t = do
  let sm :: Map OP_SYMB String
sm = [(OP_SYMB, String)] -> Map OP_SYMB String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(OP_SYMB, String)] -> Map OP_SYMB String)
-> [(OP_SYMB, String)] -> Map OP_SYMB String
forall a b. (a -> b) -> a -> b
$ MapSet Symbol Annotation -> [(OP_SYMB, String)]
extractAnnotations (Sign () () -> MapSet Symbol Annotation
forall f e. Sign f e -> MapSet Symbol Annotation
annoMap Sign () ()
sign)
  (Named (FORMULA ()) -> Result ())
-> [Named (FORMULA ())] -> Result ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int
-> Map OP_SYMB String
-> Sign () ()
-> Table2
-> Named (FORMULA ())
-> Result ()
modelCheckTest Int
c Map OP_SYMB String
sm Sign () ()
sign Table2
t) [Named (FORMULA ())]
sent

extractAnnotations :: MapSet.MapSet Symbol Annotation -> [(OP_SYMB, String)]
extractAnnotations :: MapSet Symbol Annotation -> [(OP_SYMB, String)]
extractAnnotations m :: MapSet Symbol Annotation
m =
    [Maybe (OP_SYMB, String)] -> [(OP_SYMB, String)]
forall a. [Maybe a] -> [a]
catMaybes [(Symbol, [Annotation]) -> Maybe (OP_SYMB, String)
extractAnnotation (Symbol
a, [Annotation]
b) | (a :: Symbol
a, b :: [Annotation]
b) <- MapSet Symbol Annotation -> [(Symbol, [Annotation])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList MapSet Symbol Annotation
m]

extractAnnotation :: (Symbol, [Annotation]) -> Maybe (OP_SYMB, String)
extractAnnotation :: (Symbol, [Annotation]) -> Maybe (OP_SYMB, String)
extractAnnotation (Symbol symbname :: Id
symbname symbtype :: SymbType
symbtype, set :: [Annotation]
set) = case SymbType
symbtype of
    OpAsItemType _ -> (OP_SYMB, String) -> Maybe (OP_SYMB, String)
forall a. a -> Maybe a
Just (Id -> SymbType -> OP_SYMB
createOpSymb Id
symbname SymbType
symbtype, [Annotation] -> String
getAnno [Annotation]
set)
    _ -> Maybe (OP_SYMB, String)
forall a. Maybe a
Nothing

createOpSymb :: Id -> SymbType -> OP_SYMB
createOpSymb :: Id -> SymbType -> OP_SYMB
createOpSymb i :: Id
i st :: SymbType
st = case SymbType
st of
  OpAsItemType ty :: OpType
ty -> Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
i (OpType -> OP_TYPE
toOP_TYPE OpType
ty) Range
nullRange
  _ -> String -> OP_SYMB
forall a. HasCallStack => String -> a
error "CASL.CompositionTable.ModelChecker.createOpSymb"

getAnno :: [Annotation] -> String
getAnno :: [Annotation] -> String
getAnno as :: [Annotation]
as = case [Annotation]
as of
   [a :: Annotation
a] -> Annotation -> String
getAnnoAux Annotation
a
   _ -> "failure"

getAnnoAux :: Annotation -> String
getAnnoAux :: Annotation -> String
getAnnoAux a :: Annotation
a = case Annotation
a of
    Unparsed_anno (Annote_word word :: String
word) _ _ -> String
word
    _ -> ""

modelCheckTest :: Int -> Map.Map OP_SYMB String -> Sign () () -> Table2
  -> Named (FORMULA ()) -> Result ()
modelCheckTest :: Int
-> Map OP_SYMB String
-> Sign () ()
-> Table2
-> Named (FORMULA ())
-> Result ()
modelCheckTest c :: Int
c symbs :: Map OP_SYMB String
symbs sign :: Sign () ()
sign t :: Table2
t x :: Named (FORMULA ())
x = let
    (n :: Int
n, d :: [String]
d) = Int
-> FORMULA () -> Table2 -> Map OP_SYMB String -> (Int, [String])
modelCheckTest1 Int
c (Named (FORMULA ()) -> FORMULA ()
forall s a. SenAttr s a -> s
sentence Named (FORMULA ())
x) Table2
t Map OP_SYMB String
symbs
    fstr :: String
fstr = Doc -> ShowS
forall a. Show a => a -> ShowS
shows (Named (FORMULA ()) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula ((FORMULA () -> FORMULA ())
-> Named (FORMULA ()) -> Named (FORMULA ())
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (CASL -> Sign () () -> FORMULA () -> FORMULA ()
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen CASL
CASL Sign () ()
sign) Named (FORMULA ())
x)) "\n"
      in if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
d
      then () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
hint () ("Formula succeeded:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fstr) Range
nullRange
      else () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () ("Formula failed:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fstr String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ " counter example" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then "s" else "")
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [String]
d) Range
nullRange

ifind :: Int -> IntMap.IntMap a -> a
ifind :: Int -> IntMap a -> a
ifind = a -> Int -> IntMap a -> a
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (String -> a
forall a. HasCallStack => String -> a
error "CompositionTable.ifind")

modelCheckTest1 :: Int -> FORMULA () -> Table2 -> Map.Map OP_SYMB String
  -> (Int, [String])
modelCheckTest1 :: Int
-> FORMULA () -> Table2 -> Map OP_SYMB String -> (Int, [String])
modelCheckTest1 c :: Int
c sen :: FORMULA ()
sen t :: Table2
t symbs :: Map OP_SYMB String
symbs = let
  vs :: [(VAR, Int)]
vs = [VAR] -> [(VAR, Int)]
forall a. [a] -> [(a, Int)]
number ([VAR] -> [(VAR, Int)]) -> [VAR] -> [(VAR, Int)]
forall a b. (a -> b) -> a -> b
$ Set VAR -> [VAR]
forall a. Set a -> [a]
Set.toList (Set VAR -> [VAR]) -> Set VAR -> [VAR]
forall a b. (a -> b) -> a -> b
$ FORMULA () -> Set VAR
forall f. FORMULA f -> Set VAR
vars FORMULA ()
sen
  vm :: Map VAR Int
vm = [(VAR, Int)] -> Map VAR Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(VAR, Int)]
vs
  rm :: IntMap String
rm = [(Int, String)] -> IntMap String
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, String)] -> IntMap String)
-> [(Int, String)] -> IntMap String
forall a b. (a -> b) -> a -> b
$ ((VAR, Int) -> (Int, String)) -> [(VAR, Int)] -> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: VAR
a, b :: Int
b) -> (Int
b, VAR -> String
forall a. Show a => a -> String
show VAR
a)) [(VAR, Int)]
vs
  nf :: Form
nf = Record () Form Term -> FORMULA () -> Form
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Map OP_SYMB String -> Map VAR Int -> Record () Form Term
forall f. Map OP_SYMB String -> Map VAR Int -> Record f Form Term
fromCASL Map OP_SYMB String
symbs Map VAR Int
vm) FORMULA ()
sen
  in case Form
nf of
    Quant quant :: QUANTIFIER
quant decl :: [Int]
decl f :: Form
f -> Maybe Int
-> (Int -> String)
-> QUANTIFIER
-> Form
-> Table2
-> [Assignment]
-> (Int, [String])
calculateQuantification (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
c) (Int -> IntMap String -> String
forall a. Int -> IntMap a -> a
`ifind` IntMap String
rm)
        QUANTIFIER
quant Form
f Table2
t ([Assignment] -> (Int, [String]))
-> [Assignment] -> (Int, [String])
forall a b. (a -> b) -> a -> b
$ [Int] -> Table2 -> [Assignment]
generateVariableAssignments [Int]
decl Table2
t
    _ -> if Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
forall a. IntMap a
IntMap.empty Form
nf then
       (0, []) else (1, ["formula as given above."])

calculateQuantification :: Maybe Int -> (Int -> String) -> QUANTIFIER -> Form
  -> Table2 -> [Assignment] -> (Int, [String])
calculateQuantification :: Maybe Int
-> (Int -> String)
-> QUANTIFIER
-> Form
-> Table2
-> [Assignment]
-> (Int, [String])
calculateQuantification mc :: Maybe Int
mc si :: Int -> String
si quant :: QUANTIFIER
quant f :: Form
f t :: Table2
t@(Table2 _ _ l :: IntMap Baserel
l _ _ _) vs :: [Assignment]
vs =
      let calc :: Assignment -> Bool
calc ass :: Assignment
ass = Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
ass Form
f
          nD :: Assignment -> String
nD = (Int -> String) -> IntMap Baserel -> Assignment -> String
showAssignments Int -> String
si IntMap Baserel
l
      in case QUANTIFIER
quant of
           Universal -> case Maybe Int
mc of
             Just c :: Int
c -> let
               fall :: (Int, [String]) -> Assignment -> (Int, [String])
fall (c0 :: Int
c0, ds :: [String]
ds) ass :: Assignment
ass = let
                 res :: Bool
res = Assignment -> Bool
calc Assignment
ass
                 nC0 :: Int
nC0 = if Bool
res then Int
c0 else Int
c0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
                 nDs :: [String]
nDs = if Bool
res Bool -> Bool -> Bool
|| Int
nC0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
c then [String]
ds else Assignment -> String
nD Assignment
ass String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ds
                 in [String] -> (Int, [String]) -> (Int, [String])
forall a b. a -> b -> b
seq (Int -> [String] -> [String]
forall a b. a -> b -> b
seq Int
nC0 [String]
nDs) (Int
nC0, [String]
nDs)
               in ((Int, [String]) -> Assignment -> (Int, [String]))
-> (Int, [String]) -> [Assignment] -> (Int, [String])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, [String]) -> Assignment -> (Int, [String])
fall (0, []) [Assignment]
vs
             Nothing -> (Assignment -> (Int, [String]) -> (Int, [String]))
-> (Int, [String]) -> [Assignment] -> (Int, [String])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ass :: Assignment
ass p :: (Int, [String])
p@(_, ds :: [String]
ds) ->
               if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ds then if Assignment -> Bool
calc Assignment
ass then (Int, [String])
p else (1, [Assignment -> String
nD Assignment
ass]) else (Int, [String])
p)
               (0, []) [Assignment]
vs
           Existential -> if (Assignment -> Bool) -> [Assignment] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Assignment -> Bool
calc [Assignment]
vs then (0, []) else
               (1, ["Existential not fulfilled"])
           Unique_existential -> let
               funi :: Assignment -> [String] -> [String]
funi ass :: Assignment
ass ds :: [String]
ds = case [String]
ds of
                 _ : _ : _ -> [String]
ds
                 _ | Assignment -> Bool
calc Assignment
ass -> Assignment -> String
nD Assignment
ass String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ds
                 _ -> [String]
ds
             in case (Assignment -> [String] -> [String])
-> [String] -> [Assignment] -> [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Assignment -> [String] -> [String]
funi [] [Assignment]
vs of
             [] -> (1, ["Unique Existential not fulfilled"])
             [_] -> (0, [])
             ds :: [String]
ds -> (1, [String]
ds)

type Assignment = IntMap.IntMap Int

showAssignments :: (Int -> String) -> IntMap.IntMap Baserel -> Assignment
  -> String
showAssignments :: (Int -> String) -> IntMap Baserel -> Assignment -> String
showAssignments si :: Int -> String
si l :: IntMap Baserel
l xs :: Assignment
xs =
    '[' Char -> ShowS
forall a. a -> [a] -> [a]
: String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " (((Int, Int) -> String) -> [(Int, Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> String) -> IntMap Baserel -> (Int, Int) -> String
showSingleAssignment Int -> String
si IntMap Baserel
l) ([(Int, Int)] -> [String]) -> [(Int, Int)] -> [String]
forall a b. (a -> b) -> a -> b
$ Assignment -> [(Int, Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList Assignment
xs)
     String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"

showSingleAssignment :: (Int -> String) -> IntMap.IntMap Baserel -> (Int, Int)
  -> String
showSingleAssignment :: (Int -> String) -> IntMap Baserel -> (Int, Int) -> String
showSingleAssignment si :: Int -> String
si m :: IntMap Baserel
m (v :: Int
v, i :: Int
i) = Int -> String
si Int
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ "->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ case Int -> IntMap Baserel -> Baserel
forall a. Int -> IntMap a -> a
ifind Int
i IntMap Baserel
m of
  Baserel b :: String
b -> String
b

calculateTerm :: Assignment -> Table2 -> Term -> BSet
calculateTerm :: Assignment -> Table2 -> Term -> BSet
calculateTerm ass :: Assignment
ass t :: Table2
t trm :: Term
trm = case Term
trm of
    Var var :: Int
var -> Int -> Assignment -> BSet
getBaseRelForVariable Int
var Assignment
ass
    Appl opSymb :: Op
opSymb terms :: [Term]
terms -> Op -> [Term] -> Table2 -> Assignment -> BSet
applyOperation Op
opSymb [Term]
terms Table2
t Assignment
ass
    Cond t1 :: Term
t1 fo :: Form
fo t2 :: Term
t2 -> (BSet -> BSet -> BSet) -> (Term -> BSet) -> Term -> Term -> BSet
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (\ a :: BSet
a b :: BSet
b -> if Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
ass Form
fo then BSet
a else BSet
b)
      (Assignment -> Table2 -> Term -> BSet
calculateTerm Assignment
ass Table2
t) Term
t1 Term
t2

applyOperation :: Op -> [Term] -> Table2 -> Assignment -> BSet
applyOperation :: Op -> [Term] -> Table2 -> Assignment -> BSet
applyOperation ra :: Op
ra ts :: [Term]
ts table :: Table2
table@(Table2 _ id_ :: Int
id_ _ baserels :: BSet
baserels cmpentries :: CmpTbl
cmpentries convtbl :: ConTables
convtbl) ass :: Assignment
ass =
  let err :: a
err = String -> a
forall a. HasCallStack => String -> a
error "CompositionTable.applyOperator"
  in case [Term]
ts of
    ft :: Term
ft : rt :: [Term]
rt -> let r1 :: BSet
r1 = Assignment -> Table2 -> Term -> BSet
calculateTerm Assignment
ass Table2
table Term
ft
      in case [Term]
rt of
         [sd :: Term
sd] -> case Op
ra of
               Comp -> CmpTbl -> BSet -> BSet -> BSet
calculateComposition CmpTbl
cmpentries BSet
r1
               Inter -> BSet -> BSet -> BSet
IntSet.intersection BSet
r1
               Union -> BSet -> BSet -> BSet
IntSet.union BSet
r1
               _ -> BSet -> BSet
forall a. a
err
             (BSet -> BSet) -> BSet -> BSet
forall a b. (a -> b) -> a -> b
$ Assignment -> Table2 -> Term -> BSet
calculateTerm Assignment
ass Table2
table Term
sd
         [] -> let (conv :: ConTable
conv, inv :: ConTable
inv, shortc :: ConTable
shortc, hom :: ConTable
hom) = ConTables
convtbl in case Op
ra of
             Compl -> BSet -> BSet -> BSet
IntSet.difference BSet
baserels
             Conv -> ConTable -> BSet -> BSet
calculateConverse ConTable
conv
             Shortcut -> ConTable -> BSet -> BSet
calculateConverse ConTable
shortc
             Inv -> ConTable -> BSet -> BSet
calculateConverse ConTable
inv
             Home -> ConTable -> BSet -> BSet
calculateConverse ConTable
hom
             _ -> BSet -> BSet
forall a. a
err
           (BSet -> BSet) -> BSet -> BSet
forall a b. (a -> b) -> a -> b
$ BSet
r1
         _ -> BSet
forall a. a
err
    [] -> case Op
ra of
      One -> BSet
baserels
      Iden -> Int -> BSet
IntSet.singleton Int
id_
      Zero -> BSet
IntSet.empty
      _ -> BSet
forall a. a
err

intSetFold :: (Int -> b -> b) -> b -> IntSet.IntSet -> b
intSetFold :: (Int -> b -> b) -> b -> BSet -> b
intSetFold =
#if __GLASGOW_HASKELL__ < 704
  IntSet.fold
#else
  (Int -> b -> b) -> b -> BSet -> b
forall b. (Int -> b -> b) -> b -> BSet -> b
IntSet.foldr'
#endif

calculateComposition :: CmpTbl -> BSet -> BSet -> BSet
calculateComposition :: CmpTbl -> BSet -> BSet -> BSet
calculateComposition entries :: CmpTbl
entries rels1 :: BSet
rels1 rels2 :: BSet
rels2 = (Int -> BSet -> BSet) -> BSet -> BSet -> BSet
forall b. (Int -> b -> b) -> b -> BSet -> b
intSetFold
  (\ s1 :: Int
s1 t :: BSet
t -> case Int -> CmpTbl -> ConTable
forall a. Int -> IntMap a -> a
ifind Int
s1 CmpTbl
entries of
      m1 :: ConTable
m1 -> (Int -> BSet -> BSet) -> BSet -> BSet -> BSet
forall b. (Int -> b -> b) -> b -> BSet -> b
intSetFold
         (\ s2 :: Int
s2 -> case Int -> ConTable -> BSet
forall a. Int -> IntMap a -> a
ifind Int
s2 ConTable
m1 of
            m2 :: BSet
m2 -> BSet -> BSet -> BSet
IntSet.union BSet
m2)
         BSet
t BSet
rels2)
  BSet
IntSet.empty BSet
rels1

calculateConverse :: ConTable -> BSet -> BSet
calculateConverse :: ConTable -> BSet -> BSet
calculateConverse t :: ConTable
t =
    [BSet] -> BSet
forall (f :: * -> *). Foldable f => f BSet -> BSet
IntSet.unions ([BSet] -> BSet) -> (BSet -> [BSet]) -> BSet -> BSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> BSet) -> [Int] -> [BSet]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> ConTable -> BSet
forall a. Int -> IntMap a -> a
`ifind` ConTable
t)
    ([Int] -> [BSet]) -> (BSet -> [Int]) -> BSet -> [BSet]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BSet -> [Int]
IntSet.toList

getBaseRelForVariable :: Int -> Assignment -> BSet
getBaseRelForVariable :: Int -> Assignment -> BSet
getBaseRelForVariable var :: Int
var = Int -> BSet
IntSet.singleton (Int -> BSet) -> (Assignment -> Int) -> Assignment -> BSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Assignment -> Int
forall a. Int -> IntMap a -> a
ifind Int
var

calculateFormula :: Table2 -> Assignment -> Form -> Bool
calculateFormula :: Table2 -> Assignment -> Form -> Bool
calculateFormula t :: Table2
t varass :: Assignment
varass qf :: Form
qf = case Form
qf of
    Quant q :: QUANTIFIER
q vardecls :: [Int]
vardecls f :: Form
f ->
       [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool)
-> ([Assignment] -> [String]) -> [Assignment] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, [String]) -> [String]
forall a b. (a, b) -> b
snd ((Int, [String]) -> [String])
-> ([Assignment] -> (Int, [String])) -> [Assignment] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Int
-> (Int -> String)
-> QUANTIFIER
-> Form
-> Table2
-> [Assignment]
-> (Int, [String])
calculateQuantification Maybe Int
forall a. Maybe a
Nothing Int -> String
forall a. Show a => a -> String
show QUANTIFIER
q Form
f Table2
t
         ([Assignment] -> Bool) -> [Assignment] -> Bool
forall a b. (a -> b) -> a -> b
$ Assignment -> [Int] -> Table2 -> [Assignment]
appendVariableAssignments Assignment
varass [Int]
vardecls Table2
t
    Junct j :: Bool
j formulas :: [Form]
formulas -> (if Bool
j then (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all else (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any)
        (Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
varass) [Form]
formulas
    Impl isImpl :: Bool
isImpl f1 :: Form
f1 f2 :: Form
f2 -> (Bool -> Bool -> Bool) -> (Form -> Bool) -> Form -> Form -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (if Bool
isImpl then Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=) else Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==))
                 (Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
varass) Form
f1 Form
f2
    Neg f :: Form
f -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Table2 -> Assignment -> Form -> Bool
calculateFormula Table2
t Assignment
varass Form
f
    Const b :: Bool
b -> Bool
b
    Eq term1 :: Term
term1 term2 :: Term
term2 -> (BSet -> BSet -> Bool) -> (Term -> BSet) -> Term -> Term -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on BSet -> BSet -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Assignment -> Table2 -> Term -> BSet
calculateTerm Assignment
varass Table2
t) Term
term1 Term
term2

generateVariableAssignments :: [Int] -> Table2 -> [Assignment]
generateVariableAssignments :: [Int] -> Table2 -> [Assignment]
generateVariableAssignments vs :: [Int]
vs =
  [Int] -> [Int] -> [Assignment]
gVAs [Int]
vs ([Int] -> [Assignment])
-> (Table2 -> [Int]) -> Table2 -> [Assignment]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BSet -> [Int]
IntSet.toList (BSet -> [Int]) -> (Table2 -> BSet) -> Table2 -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Table2 -> BSet
getBaseRelations

gVAs :: [Int] -> [Int] -> [Assignment]
gVAs :: [Int] -> [Int] -> [Assignment]
gVAs vs :: [Int]
vs brs :: [Int]
brs = (Int -> [Assignment] -> [Assignment])
-> [Assignment] -> [Int] -> [Assignment]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ v :: Int
v rs :: [Assignment]
rs -> [Int -> Int -> Assignment -> Assignment
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v Int
b Assignment
r | Int
b <- [Int]
brs, Assignment
r <- [Assignment]
rs])
  [Assignment
forall a. IntMap a
IntMap.empty] [Int]
vs

getBaseRelations :: Table2 -> BSet
getBaseRelations :: Table2 -> BSet
getBaseRelations (Table2 _ _ _ br :: BSet
br _ _) = BSet
br

appendVariableAssignments :: Assignment -> [Int] -> Table2 -> [Assignment]
appendVariableAssignments :: Assignment -> [Int] -> Table2 -> [Assignment]
appendVariableAssignments vm :: Assignment
vm decls :: [Int]
decls t :: Table2
t =
     (Assignment -> Assignment) -> [Assignment] -> [Assignment]
forall a b. (a -> b) -> [a] -> [b]
map (Assignment -> Assignment -> Assignment
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` Assignment
vm) ([Int] -> Table2 -> [Assignment]
generateVariableAssignments [Int]
decls Table2
t)