{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.EUF.FiniteModelFinder
-- Copyright   :  (c) Masahiro Sakai 2012, 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- A simple model finder.
--
-- References:
--
-- * Koen Claessen and Niklas Sörensson.
--   New Techniques that Improve MACE-style Finite Model Finding.
--   CADE-19. 2003.
--   <http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.EUF.FiniteModelFinder
  (
  -- * Formula types
    Var
  , FSym
  , PSym
  , GenLit (..)
  , Term (..)
  , Atom (..)
  , Lit
  , Clause
  , Formula
  , GenFormula (..)
  , toSkolemNF

  -- * Model types
  , Model (..)
  , Entity
  , EntityTuple
  , showModel
  , showEntity
  , evalFormula
  , evalAtom
  , evalTerm
  , evalLit
  , evalClause
  , evalClauses
  , evalClausesU

  -- * Main function
  , findModel
  ) where

import Control.Monad
import Control.Monad.State
import Data.Array.IArray
import Data.Interned (intern, unintern)
import Data.Interned.Text
import Data.IORef
import Data.List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String
import Data.Text (Text)
import qualified Data.Text as Text
import Text.Printf

import ToySolver.Data.Boolean
import qualified ToySolver.SAT as SAT

-- ---------------------------------------------------------------------------

-- | Variable
type Var = InternedText

-- | Function Symbol
type FSym = InternedText

-- | Predicate Symbol
type PSym = InternedText

class Vars a where
  vars :: a -> Set Var

instance Vars a => Vars [a] where
  vars :: [a] -> Set Var
vars = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Vars a => a -> Set Var
vars

-- | Generalized literal type parameterized by atom type
data GenLit a
  = Pos a
  | Neg a
  deriving (Entity -> GenLit a -> [Char] -> [Char]
forall a. Show a => Entity -> GenLit a -> [Char] -> [Char]
forall a. Show a => [GenLit a] -> [Char] -> [Char]
forall a. Show a => GenLit a -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [GenLit a] -> [Char] -> [Char]
$cshowList :: forall a. Show a => [GenLit a] -> [Char] -> [Char]
show :: GenLit a -> [Char]
$cshow :: forall a. Show a => GenLit a -> [Char]
showsPrec :: Entity -> GenLit a -> [Char] -> [Char]
$cshowsPrec :: forall a. Show a => Entity -> GenLit a -> [Char] -> [Char]
Show, GenLit a -> GenLit a -> Bool
forall a. Eq a => GenLit a -> GenLit a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenLit a -> GenLit a -> Bool
$c/= :: forall a. Eq a => GenLit a -> GenLit a -> Bool
== :: GenLit a -> GenLit a -> Bool
$c== :: forall a. Eq a => GenLit a -> GenLit a -> Bool
Eq, GenLit a -> GenLit a -> Bool
GenLit a -> GenLit a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (GenLit a)
forall a. Ord a => GenLit a -> GenLit a -> Bool
forall a. Ord a => GenLit a -> GenLit a -> Ordering
forall a. Ord a => GenLit a -> GenLit a -> GenLit a
min :: GenLit a -> GenLit a -> GenLit a
$cmin :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
max :: GenLit a -> GenLit a -> GenLit a
$cmax :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
>= :: GenLit a -> GenLit a -> Bool
$c>= :: forall a. Ord a => GenLit a -> GenLit a -> Bool
> :: GenLit a -> GenLit a -> Bool
$c> :: forall a. Ord a => GenLit a -> GenLit a -> Bool
<= :: GenLit a -> GenLit a -> Bool
$c<= :: forall a. Ord a => GenLit a -> GenLit a -> Bool
< :: GenLit a -> GenLit a -> Bool
$c< :: forall a. Ord a => GenLit a -> GenLit a -> Bool
compare :: GenLit a -> GenLit a -> Ordering
$ccompare :: forall a. Ord a => GenLit a -> GenLit a -> Ordering
Ord)

instance Complement (GenLit a) where
  notB :: GenLit a -> GenLit a
notB (Pos a
a) = forall a. a -> GenLit a
Neg a
a
  notB (Neg a
a) = forall a. a -> GenLit a
Pos a
a

instance Vars a => Vars (GenLit a) where
  vars :: GenLit a -> Set Var
vars (Pos a
a) = forall a. Vars a => a -> Set Var
vars a
a
  vars (Neg a
a) = forall a. Vars a => a -> Set Var
vars a
a

-- ---------------------------------------------------------------------------

-- | Term
data Term
  = TmApp FSym [Term]
  | TmVar Var
  deriving (Entity -> Term -> [Char] -> [Char]
[Term] -> [Char] -> [Char]
Term -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [Term] -> [Char] -> [Char]
$cshowList :: [Term] -> [Char] -> [Char]
show :: Term -> [Char]
$cshow :: Term -> [Char]
showsPrec :: Entity -> Term -> [Char] -> [Char]
$cshowsPrec :: Entity -> Term -> [Char] -> [Char]
Show, Term -> Term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
Ord)

data Atom = PApp PSym [Term]
  deriving (Entity -> Atom -> [Char] -> [Char]
[Atom] -> [Char] -> [Char]
Atom -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [Atom] -> [Char] -> [Char]
$cshowList :: [Atom] -> [Char] -> [Char]
show :: Atom -> [Char]
$cshow :: Atom -> [Char]
showsPrec :: Entity -> Atom -> [Char] -> [Char]
$cshowsPrec :: Entity -> Atom -> [Char] -> [Char]
Show, Atom -> Atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
Ord)

type Lit = GenLit Atom

type Clause = [Lit]

instance Vars Term where
  vars :: Term -> Set Var
vars (TmVar Var
v)    = forall a. a -> Set a
Set.singleton Var
v
  vars (TmApp Var
_ [Term]
ts) = forall a. Vars a => a -> Set Var
vars [Term]
ts

instance Vars Atom where
  vars :: Atom -> Set Var
vars (PApp Var
_ [Term]
ts) = forall a. Vars a => a -> Set Var
vars [Term]
ts

-- ---------------------------------------------------------------------------

-- Formula type
type Formula = GenFormula Atom

-- Generalized formula parameterized by atom type
data GenFormula a
  = T
  | F
  | Atom a
  | And (GenFormula a) (GenFormula a)
  | Or (GenFormula a) (GenFormula a)
  | Not (GenFormula a)
  | Imply (GenFormula a) (GenFormula a)
  | Equiv (GenFormula a) (GenFormula a)
  | Forall Var (GenFormula a)
  | Exists Var (GenFormula a)
  deriving (Entity -> GenFormula a -> [Char] -> [Char]
forall a. Show a => Entity -> GenFormula a -> [Char] -> [Char]
forall a. Show a => [GenFormula a] -> [Char] -> [Char]
forall a. Show a => GenFormula a -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [GenFormula a] -> [Char] -> [Char]
$cshowList :: forall a. Show a => [GenFormula a] -> [Char] -> [Char]
show :: GenFormula a -> [Char]
$cshow :: forall a. Show a => GenFormula a -> [Char]
showsPrec :: Entity -> GenFormula a -> [Char] -> [Char]
$cshowsPrec :: forall a. Show a => Entity -> GenFormula a -> [Char] -> [Char]
Show, GenFormula a -> GenFormula a -> Bool
forall a. Eq a => GenFormula a -> GenFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenFormula a -> GenFormula a -> Bool
$c/= :: forall a. Eq a => GenFormula a -> GenFormula a -> Bool
== :: GenFormula a -> GenFormula a -> Bool
$c== :: forall a. Eq a => GenFormula a -> GenFormula a -> Bool
Eq, GenFormula a -> GenFormula a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (GenFormula a)
forall a. Ord a => GenFormula a -> GenFormula a -> Bool
forall a. Ord a => GenFormula a -> GenFormula a -> Ordering
forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
min :: GenFormula a -> GenFormula a -> GenFormula a
$cmin :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
max :: GenFormula a -> GenFormula a -> GenFormula a
$cmax :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
>= :: GenFormula a -> GenFormula a -> Bool
$c>= :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
> :: GenFormula a -> GenFormula a -> Bool
$c> :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
<= :: GenFormula a -> GenFormula a -> Bool
$c<= :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
< :: GenFormula a -> GenFormula a -> Bool
$c< :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
compare :: GenFormula a -> GenFormula a -> Ordering
$ccompare :: forall a. Ord a => GenFormula a -> GenFormula a -> Ordering
Ord)

instance MonotoneBoolean (GenFormula a) where
  true :: GenFormula a
true = forall a. GenFormula a
T
  false :: GenFormula a
false = forall a. GenFormula a
F
  .&&. :: GenFormula a -> GenFormula a -> GenFormula a
(.&&.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
And
  .||. :: GenFormula a -> GenFormula a -> GenFormula a
(.||.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Or

instance Complement (GenFormula a) where
  notB :: GenFormula a -> GenFormula a
notB = forall a. GenFormula a -> GenFormula a
Not

instance IfThenElse (GenFormula a) (GenFormula a) where
  ite :: GenFormula a -> GenFormula a -> GenFormula a -> GenFormula a
ite = forall a. Boolean a => a -> a -> a -> a
iteBoolean

instance Boolean (GenFormula a) where
  .=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.=>.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Imply
  .<=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.<=>.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Equiv

instance Vars a => Vars (GenFormula a) where
  vars :: GenFormula a -> Set Var
vars GenFormula a
T               = forall a. Set a
Set.empty
  vars GenFormula a
F               = forall a. Set a
Set.empty
  vars (Atom a
a)        = forall a. Vars a => a -> Set Var
vars a
a
  vars (And GenFormula a
phi GenFormula a
psi)   = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Or GenFormula a
phi GenFormula a
psi)    = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Not GenFormula a
phi)       = forall a. Vars a => a -> Set Var
vars GenFormula a
phi
  vars (Imply GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Equiv GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Forall Var
v GenFormula a
phi)  = forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (forall a. Vars a => a -> Set Var
vars GenFormula a
phi)
  vars (Exists Var
v GenFormula a
phi)  = forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (forall a. Vars a => a -> Set Var
vars GenFormula a
phi)

toNNF :: Formula -> Formula
toNNF :: Formula -> Formula
toNNF = Formula -> Formula
f
  where
    f :: Formula -> Formula
f (And Formula
phi Formula
psi)   = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
f Formula
psi
    f (Or Formula
phi Formula
psi)    = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
f Formula
psi
    f (Not Formula
phi)       = Formula -> Formula
g Formula
phi
    f (Imply Formula
phi Formula
psi) = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
f Formula
psi
    f (Equiv Formula
phi Formula
psi) = Formula -> Formula
f ((Formula
phi forall a. Boolean a => a -> a -> a
.=>. Formula
psi) forall a. MonotoneBoolean a => a -> a -> a
.&&.  (Formula
psi forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
    f (Forall Var
v Formula
phi)  = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
f Formula
phi)
    f (Exists Var
v Formula
phi)  = forall a. Var -> GenFormula a -> GenFormula a
Exists Var
v (Formula -> Formula
f Formula
phi)
    f Formula
phi = Formula
phi

    g :: Formula -> Formula
    g :: Formula -> Formula
g Formula
T = forall a. GenFormula a
F
    g Formula
F = forall a. GenFormula a
T
    g (And Formula
phi Formula
psi)   = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
g Formula
psi
    g (Or Formula
phi Formula
psi)    = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
g Formula
psi
    g (Not Formula
phi)       = Formula -> Formula
f Formula
phi
    g (Imply Formula
phi Formula
psi) = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
g Formula
psi
    g (Equiv Formula
phi Formula
psi) = Formula -> Formula
g ((Formula
phi forall a. Boolean a => a -> a -> a
.=>. Formula
psi) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
psi forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
    g (Forall Var
v Formula
phi)  = forall a. Var -> GenFormula a -> GenFormula a
Exists Var
v (Formula -> Formula
g Formula
phi)
    g (Exists Var
v Formula
phi)  = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
g Formula
phi)
    g (Atom Atom
a)        = forall a. Complement a => a -> a
notB (forall a. a -> GenFormula a
Atom Atom
a)

-- | normalize a formula into a skolem normal form.
--
-- TODO:
--
-- * Tseitin encoding
toSkolemNF :: forall m. Monad m => (Var -> Int -> m FSym) -> Formula -> m [Clause]
toSkolemNF :: forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> m Var
skolem Formula
phi = [Var] -> Map Var Term -> Formula -> m [Clause]
f [] forall k a. Map k a
Map.empty (Formula -> Formula
toNNF Formula
phi)
  where
    f :: [Var] -> Map Var Term -> Formula -> m [Clause]
    f :: [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
_ Map Var Term
_ Formula
T = forall (m :: * -> *) a. Monad m => a -> m a
return []
    f [Var]
_ Map Var Term
_ Formula
F = forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
    f [Var]
_ Map Var Term
s (Atom Atom
a) = forall (m :: * -> *) a. Monad m => a -> m a
return [[forall a. a -> GenLit a
Pos (Map Var Term -> Atom -> Atom
substAtom Map Var Term
s Atom
a)]]
    f [Var]
_ Map Var Term
s (Not (Atom Atom
a)) = forall (m :: * -> *) a. Monad m => a -> m a
return [[forall a. a -> GenLit a
Neg (Map Var Term -> Atom -> Atom
substAtom Map Var Term
s Atom
a)]]
    f [Var]
uvs Map Var Term
s (And Formula
phi Formula
psi) = do
      [Clause]
phi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
phi
      [Clause]
psi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
psi
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Clause]
phi' forall a. [a] -> [a] -> [a]
++ [Clause]
psi'
    f [Var]
uvs Map Var Term
s (Or Formula
phi Formula
psi) = do
      [Clause]
phi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
phi
      [Clause]
psi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
psi
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Clause
c1forall a. [a] -> [a] -> [a]
++Clause
c2 | Clause
c1 <- [Clause]
phi', Clause
c2 <- [Clause]
psi']
    f [Var]
uvs Map Var Term
s psi :: Formula
psi@(Forall Var
v Formula
phi) = do
      let v' :: Var
v' = Text -> Set Var -> Var
gensym (forall t. Uninternable t => t -> Uninterned t
unintern Var
v) (forall a. Vars a => a -> Set Var
vars Formula
psi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList [Var]
uvs)
      [Var] -> Map Var Term -> Formula -> m [Clause]
f (Var
v' forall a. a -> [a] -> [a]
: [Var]
uvs) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v (Var -> Term
TmVar Var
v') Map Var Term
s) Formula
phi
    f [Var]
uvs Map Var Term
s (Exists Var
v Formula
phi) = do
      Var
fsym <- Var -> Entity -> m Var
skolem Var
v (forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Var]
uvs)
      [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v (Var -> [Term] -> Term
TmApp Var
fsym [Var -> Term
TmVar Var
v | Var
v <- forall a. [a] -> [a]
reverse [Var]
uvs]) Map Var Term
s) Formula
phi
    f [Var]
_ Map Var Term
_ Formula
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"ToySolver.EUF.FiniteModelFinder.toSkolemNF: should not happen"

    gensym :: Text -> Set Var -> Var
    gensym :: Text -> Set Var -> Var
gensym Text
template Set Var
vs = forall a. [a] -> a
head [Var
name | Var
name <- [Var]
names, forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
name Set Var
vs]
      where
        names :: [Var]
names = forall a b. (a -> b) -> [a] -> [b]
map forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ Text
template forall a. a -> [a] -> [a]
: [Text
template forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n) | Integer
n <-[Integer
1..]]

    substAtom :: Map Var Term -> Atom -> Atom
    substAtom :: Map Var Term -> Atom -> Atom
substAtom Map Var Term
s (PApp Var
p [Term]
ts) = Var -> [Term] -> Atom
PApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map (Map Var Term -> Term -> Term
substTerm Map Var Term
s) [Term]
ts)

    substTerm :: Map Var Term -> Term -> Term
    substTerm :: Map Var Term -> Term -> Term
substTerm Map Var Term
s (TmVar Var
v)    = forall a. a -> Maybe a -> a
fromMaybe (Var -> Term
TmVar Var
v) (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v Map Var Term
s)
    substTerm Map Var Term
s (TmApp Var
f [Term]
ts) = Var -> [Term] -> Term
TmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map (Map Var Term -> Term -> Term
substTerm Map Var Term
s) [Term]
ts)

test_toSkolemNF :: IO ()
test_toSkolemNF = do
  IORef Integer
ref <- forall a. a -> IO (IORef a)
newIORef Integer
0
  let skolem :: Var -> Int -> IO FSym
      skolem :: Var -> Entity -> IO Var
skolem Var
name Entity
_ = do
        Integer
n <- forall a. IORef a -> IO a
readIORef IORef Integer
ref
        let fsym :: Var
fsym = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ forall t. Uninternable t => t -> Uninterned t
unintern Var
name forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n)
        forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nforall a. Num a => a -> a -> a
+Integer
1)
        forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym

  -- ∀x. animal(a) → (∃y. heart(y) ∧ has(x,y))
  let phi :: Formula
phi = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
"x" forall a b. (a -> b) -> a -> b
$
                forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"animal" [Var -> Term
TmVar Var
"x"]) forall a. Boolean a => a -> a -> a
.=>.
                (forall a. Var -> GenFormula a -> GenFormula a
Exists Var
"y" forall a b. (a -> b) -> a -> b
$
                   forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"heart" [Var -> Term
TmVar Var
"y"]) forall a. MonotoneBoolean a => a -> a -> a
.&&.
                   forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"has" [Var -> Term
TmVar Var
"x", Var -> Term
TmVar Var
"y"]))

  [Clause]
phi' <- forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> IO Var
skolem Formula
phi

  forall a. Show a => a -> IO ()
print [Clause]
phi'
{-
[[Neg (PApp "animal" [TmVar "x"]),Pos (PApp "heart" [TmApp "y#0" [TmVar "x"]])],[Neg (PApp "animal" [TmVar "x"]),Pos (PApp "has" [TmVar "x",TmApp "y#0" [TmVar "x"]])]]

{¬animal(x) ∨ heart(y#1(x)), ¬animal(x) ∨ has(x1, y#0(x))}
-}

-- ---------------------------------------------------------------------------

-- | Shallow term
data SGenTerm v
  = STmApp FSym [v]
  | STmVar v
  deriving (Entity -> SGenTerm v -> [Char] -> [Char]
forall v. Show v => Entity -> SGenTerm v -> [Char] -> [Char]
forall v. Show v => [SGenTerm v] -> [Char] -> [Char]
forall v. Show v => SGenTerm v -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [SGenTerm v] -> [Char] -> [Char]
$cshowList :: forall v. Show v => [SGenTerm v] -> [Char] -> [Char]
show :: SGenTerm v -> [Char]
$cshow :: forall v. Show v => SGenTerm v -> [Char]
showsPrec :: Entity -> SGenTerm v -> [Char] -> [Char]
$cshowsPrec :: forall v. Show v => Entity -> SGenTerm v -> [Char] -> [Char]
Show, SGenTerm v -> SGenTerm v -> Bool
forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SGenTerm v -> SGenTerm v -> Bool
$c/= :: forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
== :: SGenTerm v -> SGenTerm v -> Bool
$c== :: forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
Eq, SGenTerm v -> SGenTerm v -> Bool
SGenTerm v -> SGenTerm v -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {v}. Ord v => Eq (SGenTerm v)
forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
forall v. Ord v => SGenTerm v -> SGenTerm v -> Ordering
forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
min :: SGenTerm v -> SGenTerm v -> SGenTerm v
$cmin :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
max :: SGenTerm v -> SGenTerm v -> SGenTerm v
$cmax :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
>= :: SGenTerm v -> SGenTerm v -> Bool
$c>= :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
> :: SGenTerm v -> SGenTerm v -> Bool
$c> :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
<= :: SGenTerm v -> SGenTerm v -> Bool
$c<= :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
< :: SGenTerm v -> SGenTerm v -> Bool
$c< :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
compare :: SGenTerm v -> SGenTerm v -> Ordering
$ccompare :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Ordering
Ord)

-- | Shallow atom
data SGenAtom v
  = SPApp PSym [v]
  | SEq (SGenTerm v) v
  deriving (Entity -> SGenAtom v -> [Char] -> [Char]
forall v. Show v => Entity -> SGenAtom v -> [Char] -> [Char]
forall v. Show v => [SGenAtom v] -> [Char] -> [Char]
forall v. Show v => SGenAtom v -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [SGenAtom v] -> [Char] -> [Char]
$cshowList :: forall v. Show v => [SGenAtom v] -> [Char] -> [Char]
show :: SGenAtom v -> [Char]
$cshow :: forall v. Show v => SGenAtom v -> [Char]
showsPrec :: Entity -> SGenAtom v -> [Char] -> [Char]
$cshowsPrec :: forall v. Show v => Entity -> SGenAtom v -> [Char] -> [Char]
Show, SGenAtom v -> SGenAtom v -> Bool
forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SGenAtom v -> SGenAtom v -> Bool
$c/= :: forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
== :: SGenAtom v -> SGenAtom v -> Bool
$c== :: forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
Eq, SGenAtom v -> SGenAtom v -> Bool
SGenAtom v -> SGenAtom v -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {v}. Ord v => Eq (SGenAtom v)
forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
forall v. Ord v => SGenAtom v -> SGenAtom v -> Ordering
forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
min :: SGenAtom v -> SGenAtom v -> SGenAtom v
$cmin :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
max :: SGenAtom v -> SGenAtom v -> SGenAtom v
$cmax :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
>= :: SGenAtom v -> SGenAtom v -> Bool
$c>= :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
> :: SGenAtom v -> SGenAtom v -> Bool
$c> :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
<= :: SGenAtom v -> SGenAtom v -> Bool
$c<= :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
< :: SGenAtom v -> SGenAtom v -> Bool
$c< :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
compare :: SGenAtom v -> SGenAtom v -> Ordering
$ccompare :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Ordering
Ord)

type STerm   = SGenTerm Var
type SAtom   = SGenAtom Var
type SLit    = GenLit SAtom
type SClause = [SLit]

instance Vars STerm where
  vars :: STerm -> Set Var
vars (STmApp Var
_ [Var]
xs) = forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
  vars (STmVar Var
v)    = forall a. a -> Set a
Set.singleton Var
v

instance Vars SAtom where
  vars :: SAtom -> Set Var
vars (SPApp Var
_ [Var]
xs) = forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
  vars (SEq STerm
t Var
v) = forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v (forall a. Vars a => a -> Set Var
vars STerm
t)

-- ---------------------------------------------------------------------------

type M = State (Set Var, Int, Map (FSym, [Var]) Var, [SLit])

flatten :: Clause -> Maybe SClause
flatten :: Clause -> Maybe [SLit]
flatten Clause
c =
  case forall s a. State s a -> s -> (a, s)
runState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GenLit Atom -> M SLit
flattenLit Clause
c) (forall a. Vars a => a -> Set Var
vars Clause
c, Entity
0, forall k a. Map k a
Map.empty, []) of
    ([SLit]
c, (Set Var
_,Entity
_,Map (Var, [Var]) Var
_,[SLit]
ls)) -> [SLit] -> Maybe [SLit]
removeTautology forall a b. (a -> b) -> a -> b
$ [SLit] -> [SLit]
removeNegEq forall a b. (a -> b) -> a -> b
$ [SLit]
ls forall a. [a] -> [a] -> [a]
++ [SLit]
c
  where
    gensym :: M Var
    gensym :: M Var
gensym = do
      (Set Var
vs, Entity
n, Map (Var, [Var]) Var
defs, [SLit]
ls) <- forall s (m :: * -> *). MonadState s m => m s
get
      let go :: Int -> M Var
          go :: Entity -> M Var
go Entity
m = do
            let v :: Var
v = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Entity
m)
            if Var
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Var
vs
              then Entity -> M Var
go (Entity
mforall a. Num a => a -> a -> a
+Entity
1)
              else do
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v Set Var
vs, Entity
mforall a. Num a => a -> a -> a
+Entity
1, Map (Var, [Var]) Var
defs, [SLit]
ls)
                forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
      Entity -> M Var
go Entity
n

    flattenLit :: Lit -> M SLit
    flattenLit :: GenLit Atom -> M SLit
flattenLit (Pos Atom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Atom -> M SAtom
flattenAtom Atom
a
    flattenLit (Neg Atom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Atom -> M SAtom
flattenAtom Atom
a

    flattenAtom :: Atom -> M SAtom
    flattenAtom :: Atom -> M SAtom
flattenAtom (PApp Var
"=" [TmVar Var
x, TmVar Var
y])    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. v -> SGenTerm v
STmVar Var
x) Var
y
    flattenAtom (PApp Var
"=" [TmVar Var
x, TmApp Var
f [Term]
ts]) = do
      [Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
    flattenAtom (PApp Var
"=" [TmApp Var
f [Term]
ts, TmVar Var
x]) = do
      [Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
    flattenAtom (PApp Var
"=" [TmApp Var
f [Term]
ts, Term
t2]) = do
      [Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      Var
x <- Term -> M Var
flattenTerm Term
t2
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
    flattenAtom (PApp Var
p [Term]
ts) = do
      [Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. Var -> [v] -> SGenAtom v
SPApp Var
p [Var]
xs

    flattenTerm :: Term -> M Var
    flattenTerm :: Term -> M Var
flattenTerm (TmVar Var
x)    = forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
    flattenTerm (TmApp Var
f [Term]
ts) = do
      [Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      (Set Var
_, Entity
_, Map (Var, [Var]) Var
defs, [SLit]
_) <- forall s (m :: * -> *). MonadState s m => m s
get
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var
f, [Var]
xs) Map (Var, [Var]) Var
defs of
        Just Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
        Maybe Var
Nothing -> do
          Var
x <- M Var
gensym
          (Set Var
vs, Entity
n, Map (Var, [Var]) Var
defs, [SLit]
ls) <- forall s (m :: * -> *). MonadState s m => m s
get
          forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Var
vs, Entity
n, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Var
f, [Var]
xs) Var
x Map (Var, [Var]) Var
defs, forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x) forall a. a -> [a] -> [a]
: [SLit]
ls)
          forall (m :: * -> *) a. Monad m => a -> m a
return Var
x

    removeNegEq :: SClause -> SClause
    removeNegEq :: [SLit] -> [SLit]
removeNegEq = [SLit] -> [SLit] -> [SLit]
go []
      where
        go :: [SLit] -> [SLit] -> [SLit]
go [SLit]
r [] = [SLit]
r
        go [SLit]
r (Neg (SEq (STmVar Var
x) Var
y) : [SLit]
ls) = [SLit] -> [SLit] -> [SLit]
go (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) [SLit]
r) (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) [SLit]
ls)
        go [SLit]
r (SLit
l : [SLit]
ls) = [SLit] -> [SLit] -> [SLit]
go (SLit
l forall a. a -> [a] -> [a]
: [SLit]
r) [SLit]
ls

        substLit :: Var -> Var -> SLit -> SLit
        substLit :: Var -> Var -> SLit -> SLit
substLit Var
x Var
y (Pos SAtom
a) = forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y SAtom
a
        substLit Var
x Var
y (Neg SAtom
a) = forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y SAtom
a

        substAtom :: Var -> Var -> SAtom -> SAtom
        substAtom :: Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y (SPApp Var
p [Var]
xs) = forall v. Var -> [v] -> SGenAtom v
SPApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> Var -> Var
substVar Var
x Var
y) [Var]
xs)
        substAtom Var
x Var
y (SEq STerm
t Var
v)    = forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> Var -> STerm -> STerm
substTerm Var
x Var
y STerm
t) (Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v)

        substTerm :: Var -> Var -> STerm -> STerm
        substTerm :: Var -> Var -> STerm -> STerm
substTerm Var
x Var
y (STmApp Var
f [Var]
xs) = forall v. Var -> [v] -> SGenTerm v
STmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> Var -> Var
substVar Var
x Var
y) [Var]
xs)
        substTerm Var
x Var
y (STmVar Var
v)    = forall v. v -> SGenTerm v
STmVar (Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v)

        substVar :: Var -> Var -> Var -> Var
        substVar :: Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v
          | Var
vforall a. Eq a => a -> a -> Bool
==Var
x      = Var
y
          | Bool
otherwise = Var
v

    removeTautology :: SClause -> Maybe SClause
    removeTautology :: [SLit] -> Maybe [SLit]
removeTautology [SLit]
lits
      | forall a. Set a -> Bool
Set.null (Set SAtom
pos forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set SAtom
neg) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [forall a. a -> GenLit a
Neg SAtom
l | SAtom
l <- forall a. Set a -> [a]
Set.toList Set SAtom
neg] forall a. [a] -> [a] -> [a]
++ [forall a. a -> GenLit a
Pos SAtom
l | SAtom
l <- forall a. Set a -> [a]
Set.toList Set SAtom
pos]
      | Bool
otherwise = forall a. Maybe a
Nothing
      where
        pos :: Set SAtom
pos = forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Pos SAtom
l <- [SLit]
lits]
        neg :: Set SAtom
neg = forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Neg SAtom
l <- [SLit]
lits]

test_flatten :: Maybe [SLit]
test_flatten = Clause -> Maybe [SLit]
flatten [forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"P" [Var -> [Term] -> Term
TmApp Var
"a" [], Var -> [Term] -> Term
TmApp Var
"f" [Var -> Term
TmVar Var
"x"]]]

{-
[Pos $ PApp "P" [TmApp "a" [], TmApp "f" [TmVar "x"]]]

P(a, f(x))

[Pos (SPApp "P" ["#0","#1"]),Neg (SEq (STmApp "a" []) "#0"),Neg (SEq (STmApp "f" ["x"]) "#1")]

f(x) ≠ z ∨ a ≠ y ∨ P(y,z)
(f(x) = z ∧ a = y) → P(y,z)
-}

-- ---------------------------------------------------------------------------

-- | Element of model.
type Entity = Int

type EntityTuple = [Entity]

-- | print entity
showEntity :: Entity -> String
showEntity :: Entity -> [Char]
showEntity Entity
e = [Char]
"$" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Entity
e

showEntityTuple :: EntityTuple -> String
showEntityTuple :: EntityTuple -> [Char]
showEntityTuple EntityTuple
xs = forall r. PrintfType r => [Char] -> r
printf [Char]
"(%s)" forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Entity -> [Char]
showEntity EntityTuple
xs

-- ---------------------------------------------------------------------------

type GroundTerm   = SGenTerm Entity
type GroundAtom   = SGenAtom Entity
type GroundLit    = GenLit GroundAtom
type GroundClause = [GroundLit]

type Subst = Map Var Entity

enumSubst :: Set Var -> [Entity] -> [Subst]
enumSubst :: Set Var -> EntityTuple -> [Subst]
enumSubst Set Var
vs EntityTuple
univ = do
  [(Var, Entity)]
ps <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(Var
v,Entity
e) | Entity
e <- EntityTuple
univ] | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
vs]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var, Entity)]
ps

applySubst :: Subst -> SClause -> GroundClause
applySubst :: Subst -> [SLit] -> GroundClause
applySubst Subst
s = forall a b. (a -> b) -> [a] -> [b]
map SLit -> GroundLit
substLit
  where
    substLit :: SLit -> GroundLit
    substLit :: SLit -> GroundLit
substLit (Pos SAtom
a) = forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a
    substLit (Neg SAtom
a) = forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a

    substAtom :: SAtom -> GroundAtom
    substAtom :: SAtom -> GroundAtom
substAtom (SPApp Var
p [Var]
xs) = forall v. Var -> [v] -> SGenAtom v
SPApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map Var -> Entity
substVar [Var]
xs)
    substAtom (SEq STerm
t Var
v)    = forall v. SGenTerm v -> v -> SGenAtom v
SEq (STerm -> GroundTerm
substTerm STerm
t) (Var -> Entity
substVar Var
v)

    substTerm :: STerm ->  GroundTerm
    substTerm :: STerm -> GroundTerm
substTerm (STmApp Var
f [Var]
xs) = forall v. Var -> [v] -> SGenTerm v
STmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map Var -> Entity
substVar [Var]
xs)
    substTerm (STmVar Var
v)    = forall v. v -> SGenTerm v
STmVar (Var -> Entity
substVar Var
v)

    substVar :: Var -> Entity
    substVar :: Var -> Entity
substVar = (Subst
s forall k a. Ord k => Map k a -> k -> a
Map.!)

simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GroundLit -> Maybe GroundClause
f
  where
    f :: GroundLit -> Maybe [GroundLit]
    f :: GroundLit -> Maybe GroundClause
f (Pos (SEq (STmVar Entity
x) Entity
y)) = if Entity
xforall a. Eq a => a -> a -> Bool
==Entity
y then forall a. Maybe a
Nothing else forall (m :: * -> *) a. Monad m => a -> m a
return []
    f GroundLit
lit = forall (m :: * -> *) a. Monad m => a -> m a
return [GroundLit
lit]

collectFSym :: Clause -> Set (FSym, Int)
collectFSym :: Clause -> Set (Var, Entity)
collectFSym = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map GenLit Atom -> Set (Var, Entity)
f
  where
    f :: Lit -> Set (FSym, Int)
    f :: GenLit Atom -> Set (Var, Entity)
f (Pos Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
    f (Neg Atom
a) = Atom -> Set (Var, Entity)
g Atom
a

    g :: Atom -> Set (FSym, Int)
    g :: Atom -> Set (Var, Entity)
g (PApp Var
_ [Term]
xs) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Term -> Set (Var, Entity)
h [Term]
xs

    h :: Term -> Set (FSym, Int)
    h :: Term -> Set (Var, Entity)
h (TmVar Var
_) = forall a. Set a
Set.empty
    h (TmApp Var
f [Term]
xs) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton (Var
f, forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Term]
xs) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Term -> Set (Var, Entity)
h [Term]
xs

collectPSym :: Clause -> Set (PSym, Int)
collectPSym :: Clause -> Set (Var, Entity)
collectPSym = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map GenLit Atom -> Set (Var, Entity)
f
  where
    f :: Lit -> Set (PSym, Int)
    f :: GenLit Atom -> Set (Var, Entity)
f (Pos Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
    f (Neg Atom
a) = Atom -> Set (Var, Entity)
g Atom
a

    g :: Atom -> Set (PSym, Int)
    g :: Atom -> Set (Var, Entity)
g (PApp Var
"=" [Term
_,Term
_]) = forall a. Set a
Set.empty
    g (PApp Var
p [Term]
xs) = forall a. a -> Set a
Set.singleton (Var
p, forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Term]
xs)

-- ---------------------------------------------------------------------------

data Model
  = Model
  { Model -> EntityTuple
mUniverse  :: [Entity]
  , Model -> Map Var (Set EntityTuple)
mRelations :: Map PSym (Set EntityTuple)
  , Model -> Map Var (Map EntityTuple Entity)
mFunctions :: Map FSym (Map EntityTuple Entity)
  }

showModel :: Model -> [String]
showModel :: Model -> [[Char]]
showModel Model
m =
  forall r. PrintfType r => [Char] -> r
printf [Char]
"DOMAIN = {%s}" (forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a b. (a -> b) -> [a] -> [b]
map Entity -> [Char]
showEntity (Model -> EntityTuple
mUniverse Model
m))) forall a. a -> [a] -> [a]
:
  [ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s = { %s }" (Text -> [Char]
Text.unpack (forall t. Uninternable t => t -> Uninterned t
unintern Var
p)) [Char]
s
  | (Var
p, Set EntityTuple
xss) <- forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Set EntityTuple)
mRelations Model
m)
  , let s :: [Char]
s = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [if forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs forall a. Eq a => a -> a -> Bool
== Entity
1 then Entity -> [Char]
showEntity (forall a. [a] -> a
head EntityTuple
xs) else EntityTuple -> [Char]
showEntityTuple EntityTuple
xs | EntityTuple
xs <- forall a. Set a -> [a]
Set.toList Set EntityTuple
xss]
  ] forall a. [a] -> [a] -> [a]
++
  [ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s%s = %s" (Text -> [Char]
Text.unpack (forall t. Uninternable t => t -> Uninterned t
unintern Var
f)) (if forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs forall a. Eq a => a -> a -> Bool
== Entity
0 then [Char]
"" else EntityTuple -> [Char]
showEntityTuple EntityTuple
xs) (Entity -> [Char]
showEntity Entity
y)
  | (Var
f, Map EntityTuple Entity
xss) <- forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Map EntityTuple Entity)
mFunctions Model
m)
  , (EntityTuple
xs, Entity
y) <- forall k a. Map k a -> [(k, a)]
Map.toList Map EntityTuple Entity
xss
  ]

evalFormula :: Model -> Formula -> Bool
evalFormula :: Model -> Formula -> Bool
evalFormula Model
m = Subst -> Formula -> Bool
f forall k a. Map k a
Map.empty
  where
    f :: Map Var Entity -> Formula -> Bool
    f :: Subst -> Formula -> Bool
f Subst
env Formula
T = Bool
True
    f Subst
env Formula
F = Bool
False
    f Subst
env (Atom Atom
a) = Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
a
    f Subst
env (And Formula
phi1 Formula
phi2) = Subst -> Formula -> Bool
f Subst
env Formula
phi1 Bool -> Bool -> Bool
&& Subst -> Formula -> Bool
f Subst
env Formula
phi2
    f Subst
env (Or Formula
phi1 Formula
phi2)  = Subst -> Formula -> Bool
f Subst
env Formula
phi1 Bool -> Bool -> Bool
|| Subst -> Formula -> Bool
f Subst
env Formula
phi2
    f Subst
env (Not Formula
phi) = Bool -> Bool
not (Subst -> Formula -> Bool
f Subst
env Formula
phi)
    f Subst
env (Imply Formula
phi1 Formula
phi2) = Bool -> Bool
not (Subst -> Formula -> Bool
f Subst
env Formula
phi1) Bool -> Bool -> Bool
|| Subst -> Formula -> Bool
f Subst
env Formula
phi2
    f Subst
env (Equiv Formula
phi1 Formula
phi2) = Subst -> Formula -> Bool
f Subst
env Formula
phi1 forall a. Eq a => a -> a -> Bool
== Subst -> Formula -> Bool
f Subst
env Formula
phi2
    f Subst
env (Forall Var
v Formula
phi) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Entity
e -> Subst -> Formula -> Bool
f (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Entity
e Subst
env) Formula
phi) (Model -> EntityTuple
mUniverse Model
m)
    f Subst
env (Exists Var
v Formula
phi) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Entity
e -> Subst -> Formula -> Bool
f (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Entity
e Subst
env) Formula
phi) (Model -> EntityTuple
mUniverse Model
m)

evalAtom :: Model -> Map Var Entity -> Atom -> Bool
evalAtom :: Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env (PApp Var
"=" [Term
x1,Term
x2]) = Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env Term
x1 forall a. Eq a => a -> a -> Bool
== Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env Term
x2
evalAtom Model
m Subst
env (PApp Var
p [Term]
xs) = forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env) [Term]
xs forall a. Ord a => a -> Set a -> Bool
`Set.member` (Model -> Map Var (Set EntityTuple)
mRelations Model
m forall k a. Ord k => Map k a -> k -> a
Map.! Var
p)

evalTerm :: Model -> Map Var Entity -> Term -> Entity
evalTerm :: Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env (TmVar Var
v) = Subst
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
evalTerm Model
m Subst
env (TmApp Var
f [Term]
xs) = (Model -> Map Var (Map EntityTuple Entity)
mFunctions Model
m forall k a. Ord k => Map k a -> k -> a
Map.! Var
f) forall k a. Ord k => Map k a -> k -> a
Map.! forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env) [Term]
xs

evalLit :: Model -> Map Var Entity -> Lit -> Bool
evalLit :: Model -> Subst -> GenLit Atom -> Bool
evalLit Model
m Subst
env (Pos Atom
atom) = Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
atom
evalLit Model
m Subst
env (Neg Atom
atom) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
atom

evalClause :: Model -> Map Var Entity -> Clause -> Bool
evalClause :: Model -> Subst -> Clause -> Bool
evalClause Model
m Subst
env = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Model -> Subst -> GenLit Atom -> Bool
evalLit Model
m Subst
env)

evalClauses :: Model -> Map Var Entity -> [Clause] -> Bool
evalClauses :: Model -> Subst -> [Clause] -> Bool
evalClauses Model
m Subst
env = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Model -> Subst -> Clause -> Bool
evalClause Model
m Subst
env)

evalClausesU :: Model -> [Clause] -> Bool
evalClausesU :: Model -> [Clause] -> Bool
evalClausesU Model
m [Clause]
cs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Subst
env -> Model -> Subst -> [Clause] -> Bool
evalClauses Model
m Subst
env [Clause]
cs) (Set Var -> EntityTuple -> [Subst]
enumSubst (forall a. Vars a => a -> Set Var
vars [Clause]
cs) (Model -> EntityTuple
mUniverse Model
m))

-- ---------------------------------------------------------------------------

findModel :: Int -> [Clause] -> IO (Maybe Model)
findModel :: Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
size [Clause]
cs = do
  let univ :: EntityTuple
univ = [Entity
0..Entity
sizeforall a. Num a => a -> a -> a
-Entity
1]

  let cs2 :: [[SLit]]
cs2 = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Clause -> Maybe [SLit]
flatten [Clause]
cs
      fs :: Set (Var, Entity)
fs = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Clause -> Set (Var, Entity)
collectFSym [Clause]
cs
      ps :: Set (Var, Entity)
ps = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Clause -> Set (Var, Entity)
collectPSym [Clause]
cs

  Solver
solver <- IO Solver
SAT.newSolver

  IORef (Map GroundAtom Entity)
ref <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty

  let translateAtom :: GroundAtom -> IO SAT.Var
      translateAtom :: GroundAtom -> IO Entity
translateAtom (SEq (STmVar Entity
_) Entity
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
      translateAtom GroundAtom
a = do
        Map GroundAtom Entity
m <- forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Entity)
ref
        case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GroundAtom
a Map GroundAtom Entity
m of
          Just Entity
b  -> forall (m :: * -> *) a. Monad m => a -> m a
return Entity
b
          Maybe Entity
Nothing -> do
            Entity
b <- forall (m :: * -> *) a. NewVar m a => a -> m Entity
SAT.newVar Solver
solver
            forall a. IORef a -> a -> IO ()
writeIORef IORef (Map GroundAtom Entity)
ref (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert GroundAtom
a Entity
b Map GroundAtom Entity
m)
            forall (m :: * -> *) a. Monad m => a -> m a
return Entity
b

      translateLit :: GroundLit -> IO SAT.Lit
      translateLit :: GroundLit -> IO Entity
translateLit (Pos GroundAtom
a) = GroundAtom -> IO Entity
translateAtom GroundAtom
a
      translateLit (Neg GroundAtom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ GroundAtom -> IO Entity
translateAtom GroundAtom
a

      translateClause :: GroundClause -> IO SAT.Clause
      translateClause :: GroundClause -> IO EntityTuple
translateClause = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GroundLit -> IO Entity
translateLit

  -- Instances
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[SLit]]
cs2 forall a b. (a -> b) -> a -> b
$ \[SLit]
c -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set Var -> EntityTuple -> [Subst]
enumSubst (forall a. Vars a => a -> Set Var
vars [SLit]
c) EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \Subst
s -> do
      case GroundClause -> Maybe GroundClause
simplifyGroundClause (Subst -> [SLit] -> GroundClause
applySubst Subst
s [SLit]
c) of
        Maybe GroundClause
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just GroundClause
c' -> forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GroundClause -> IO EntityTuple
translateClause GroundClause
c'

  -- Functional definitions
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs) forall a b. (a -> b) -> a -> b
$ \(Var
f, Entity
arity) -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (m :: * -> *) a. Applicative m => Entity -> m a -> m [a]
replicateM Entity
arity EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \EntityTuple
args ->
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Entity
y1,Entity
y2) | Entity
y1 <- EntityTuple
univ, Entity
y2 <- EntityTuple
univ, Entity
y1 forall a. Ord a => a -> a -> Bool
< Entity
y2] forall a b. (a -> b) -> a -> b
$ \(Entity
y1,Entity
y2) -> do
        let c :: GroundClause
c = [forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y1), forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y2)]
        EntityTuple
c' <- GroundClause -> IO EntityTuple
translateClause GroundClause
c
        forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver EntityTuple
c'

  -- Totality definitions
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs) forall a b. (a -> b) -> a -> b
$ \(Var
f, Entity
arity) -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (m :: * -> *) a. Applicative m => Entity -> m a -> m [a]
replicateM Entity
arity EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \EntityTuple
args -> do
        let c :: GroundClause
c = [forall a. a -> GenLit a
Pos (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y) | Entity
y <- EntityTuple
univ]
        EntityTuple
c' <- GroundClause -> IO EntityTuple
translateClause GroundClause
c
        forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver EntityTuple
c'

  Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
  if Bool
ret
    then do
      Model
bmodel <- Solver -> IO Model
SAT.getModel Solver
solver
      Map GroundAtom Entity
m <- forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Entity)
ref

      let rels :: Map Var (Set EntityTuple)
rels = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
            (Var
p,Entity
_) <- forall a. Set a -> [a]
Set.toList Set (Var, Entity)
ps
            let tbl :: Set EntityTuple
tbl = forall a. Ord a => [a] -> Set a
Set.fromList [EntityTuple
xs | (SPApp Var
p' EntityTuple
xs, Entity
b) <- forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Entity
m, Var
p forall a. Eq a => a -> a -> Bool
== Var
p', Model
bmodel forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Entity
b]
            forall (m :: * -> *) a. Monad m => a -> m a
return (Var
p, Set EntityTuple
tbl)
      let funs :: Map Var (Map EntityTuple Entity)
funs = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
            (Var
f,Entity
_) <- forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs
            let tbl :: Map EntityTuple Entity
tbl = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(EntityTuple
xs, Entity
y) | (SEq (STmApp Var
f' EntityTuple
xs) Entity
y, Entity
b) <- forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Entity
m, Var
f forall a. Eq a => a -> a -> Bool
== Var
f', Model
bmodel forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Entity
b]
            forall (m :: * -> *) a. Monad m => a -> m a
return (Var
f, Map EntityTuple Entity
tbl)

      let model :: Model
model = Model
            { mUniverse :: EntityTuple
mUniverse  = EntityTuple
univ
            , mRelations :: Map Var (Set EntityTuple)
mRelations = Map Var (Set EntityTuple)
rels
            , mFunctions :: Map Var (Map EntityTuple Entity)
mFunctions = Map Var (Map EntityTuple Entity)
funs
            }

      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Model
model)
    else do
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

-- ---------------------------------------------------------------------------

{-
∀x. ∃y. x≠y && f(y)=x
∀x. x≠g(x) ∧ f(g(x))=x
-}

test :: IO ()
test = do
  let c1 :: Clause
c1 = [forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"=" [Var -> [Term] -> Term
TmApp Var
"f" [Var -> [Term] -> Term
TmApp Var
"g" [Var -> Term
TmVar Var
"x"]], Var -> Term
TmVar Var
"x"]]
      c2 :: Clause
c2 = [forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"=" [Var -> Term
TmVar Var
"x", Var -> [Term] -> Term
TmApp Var
"g" [Var -> Term
TmVar Var
"x"]]]
  Maybe Model
ret <- Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
3 [Clause
c1, Clause
c2]
  case Maybe Model
ret of
    Maybe Model
Nothing -> [Char] -> IO ()
putStrLn [Char]
"=== NO MODEL FOUND ==="
    Just Model
m -> do
      [Char] -> IO ()
putStrLn [Char]
"=== A MODEL FOUND ==="
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m

test2 :: IO ()
test2 = do
  let phi :: Formula
phi = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
"x" forall a b. (a -> b) -> a -> b
$ forall a. Var -> GenFormula a -> GenFormula a
Exists Var
"y" forall a b. (a -> b) -> a -> b
$
              forall a. Complement a => a -> a
notB (forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"=" [Var -> Term
TmVar Var
"x", Var -> Term
TmVar Var
"y"])) forall a. MonotoneBoolean a => a -> a -> a
.&&.
              forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"=" [Var -> [Term] -> Term
TmApp Var
"f" [Var -> Term
TmVar Var
"y"], Var -> Term
TmVar Var
"x"])

  IORef Integer
ref <- forall a. a -> IO (IORef a)
newIORef Integer
0
  let skolem :: Var -> Int -> IO FSym
      skolem :: Var -> Entity -> IO Var
skolem Var
name Entity
_ = do
        Integer
n <- forall a. IORef a -> IO a
readIORef IORef Integer
ref
        let fsym :: Var
fsym = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ forall t. Uninternable t => t -> Uninterned t
unintern Var
name forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n)
        forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nforall a. Num a => a -> a -> a
+Integer
1)
        forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym
  [Clause]
cs <- forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> IO Var
skolem Formula
phi

  Maybe Model
ret <- Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
3 [Clause]
cs
  case Maybe Model
ret of
    Maybe Model
Nothing -> [Char] -> IO ()
putStrLn [Char]
"=== NO MODEL FOUND ==="
    Just Model
m -> do
      [Char] -> IO ()
putStrLn [Char]
"=== A MODEL FOUND ==="
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m

-- ---------------------------------------------------------------------------