{-# 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 = [Set Var] -> Set Var
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Var] -> Set Var) -> ([a] -> [Set Var]) -> [a] -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set Var) -> [a] -> [Set Var]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set Var
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]
[GenLit a] -> [Char] -> [Char]
GenLit a -> [Char]
(Entity -> GenLit a -> [Char] -> [Char])
-> (GenLit a -> [Char])
-> ([GenLit a] -> [Char] -> [Char])
-> Show (GenLit a)
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
$cshowsPrec :: forall a. Show a => Entity -> GenLit a -> [Char] -> [Char]
showsPrec :: Entity -> GenLit a -> [Char] -> [Char]
$cshow :: forall a. Show a => GenLit a -> [Char]
show :: GenLit a -> [Char]
$cshowList :: forall a. Show a => [GenLit a] -> [Char] -> [Char]
showList :: [GenLit a] -> [Char] -> [Char]
Show, GenLit a -> GenLit a -> Bool
(GenLit a -> GenLit a -> Bool)
-> (GenLit a -> GenLit a -> Bool) -> Eq (GenLit a)
forall a. Eq a => GenLit a -> GenLit a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: GenLit a -> GenLit a -> Bool
Eq, Eq (GenLit a)
Eq (GenLit a) =>
(GenLit a -> GenLit a -> Ordering)
-> (GenLit a -> GenLit a -> Bool)
-> (GenLit a -> GenLit a -> Bool)
-> (GenLit a -> GenLit a -> Bool)
-> (GenLit a -> GenLit a -> Bool)
-> (GenLit a -> GenLit a -> GenLit a)
-> (GenLit a -> GenLit a -> GenLit a)
-> Ord (GenLit a)
GenLit a -> GenLit a -> Bool
GenLit a -> GenLit a -> Ordering
GenLit a -> GenLit a -> GenLit a
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
$ccompare :: forall a. Ord a => GenLit a -> GenLit a -> Ordering
compare :: GenLit a -> GenLit a -> Ordering
$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
>= :: GenLit a -> GenLit a -> Bool
$cmax :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
max :: GenLit a -> GenLit a -> GenLit a
$cmin :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
min :: GenLit a -> GenLit a -> GenLit a
Ord)

instance Complement (GenLit a) where
  notB :: GenLit a -> GenLit a
notB (Pos a
a) = a -> GenLit a
forall a. a -> GenLit a
Neg a
a
  notB (Neg a
a) = a -> GenLit 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) = a -> Set Var
forall a. Vars a => a -> Set Var
vars a
a
  vars (Neg a
a) = a -> Set Var
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]
(Entity -> Term -> [Char] -> [Char])
-> (Term -> [Char]) -> ([Term] -> [Char] -> [Char]) -> Show Term
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Entity -> Term -> [Char] -> [Char]
showsPrec :: Entity -> Term -> [Char] -> [Char]
$cshow :: Term -> [Char]
show :: Term -> [Char]
$cshowList :: [Term] -> [Char] -> [Char]
showList :: [Term] -> [Char] -> [Char]
Show, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord 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
$ccompare :: Term -> Term -> Ordering
compare :: Term -> Term -> Ordering
$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
>= :: Term -> Term -> Bool
$cmax :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
min :: Term -> Term -> Term
Ord)

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

type Lit = GenLit Atom

type Clause = [Lit]

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

instance Vars Atom where
  vars :: Atom -> Set Var
vars (PApp Var
_ [Term]
ts) = [Term] -> Set Var
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]
[GenFormula a] -> [Char] -> [Char]
GenFormula a -> [Char]
(Entity -> GenFormula a -> [Char] -> [Char])
-> (GenFormula a -> [Char])
-> ([GenFormula a] -> [Char] -> [Char])
-> Show (GenFormula a)
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
$cshowsPrec :: forall a. Show a => Entity -> GenFormula a -> [Char] -> [Char]
showsPrec :: Entity -> GenFormula a -> [Char] -> [Char]
$cshow :: forall a. Show a => GenFormula a -> [Char]
show :: GenFormula a -> [Char]
$cshowList :: forall a. Show a => [GenFormula a] -> [Char] -> [Char]
showList :: [GenFormula a] -> [Char] -> [Char]
Show, GenFormula a -> GenFormula a -> Bool
(GenFormula a -> GenFormula a -> Bool)
-> (GenFormula a -> GenFormula a -> Bool) -> Eq (GenFormula a)
forall a. Eq a => GenFormula a -> GenFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: GenFormula a -> GenFormula a -> Bool
Eq, Eq (GenFormula a)
Eq (GenFormula a) =>
(GenFormula a -> GenFormula a -> Ordering)
-> (GenFormula a -> GenFormula a -> Bool)
-> (GenFormula a -> GenFormula a -> Bool)
-> (GenFormula a -> GenFormula a -> Bool)
-> (GenFormula a -> GenFormula a -> Bool)
-> (GenFormula a -> GenFormula a -> GenFormula a)
-> (GenFormula a -> GenFormula a -> GenFormula a)
-> Ord (GenFormula a)
GenFormula a -> GenFormula a -> Bool
GenFormula a -> GenFormula a -> Ordering
GenFormula a -> GenFormula a -> GenFormula a
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
$ccompare :: forall a. Ord a => GenFormula a -> GenFormula a -> Ordering
compare :: GenFormula a -> GenFormula a -> Ordering
$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
>= :: GenFormula a -> GenFormula a -> Bool
$cmax :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
max :: GenFormula a -> GenFormula a -> GenFormula a
$cmin :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
min :: GenFormula a -> GenFormula a -> GenFormula a
Ord)

instance MonotoneBoolean (GenFormula a) where
  true :: GenFormula a
true = GenFormula a
forall a. GenFormula a
T
  false :: GenFormula a
false = GenFormula a
forall a. GenFormula a
F
  .&&. :: GenFormula a -> GenFormula a -> GenFormula a
(.&&.) = GenFormula a -> GenFormula a -> GenFormula a
forall a. GenFormula a -> GenFormula a -> GenFormula a
And
  .||. :: GenFormula a -> GenFormula a -> GenFormula a
(.||.) = 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 = GenFormula a -> GenFormula a
forall a. GenFormula a -> GenFormula a
Not

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

instance Boolean (GenFormula a) where
  .=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.=>.) = GenFormula a -> GenFormula a -> GenFormula a
forall a. GenFormula a -> GenFormula a -> GenFormula a
Imply
  .<=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.<=>.) = 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               = Set Var
forall a. Set a
Set.empty
  vars GenFormula a
F               = Set Var
forall a. Set a
Set.empty
  vars (Atom a
a)        = a -> Set Var
forall a. Vars a => a -> Set Var
vars a
a
  vars (And GenFormula a
phi GenFormula a
psi)   = GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Or GenFormula a
phi GenFormula a
psi)    = GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Not GenFormula a
phi)       = GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi
  vars (Imply GenFormula a
phi GenFormula a
psi) = GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Equiv GenFormula a
phi GenFormula a
psi) = GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
psi
  vars (Forall Var
v GenFormula a
phi)  = Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (GenFormula a -> Set Var
forall a. Vars a => a -> Set Var
vars GenFormula a
phi)
  vars (Exists Var
v GenFormula a
phi)  = Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (GenFormula a -> Set Var
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 Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
f Formula
psi
    f (Or Formula
phi Formula
psi)    = Formula -> Formula
f Formula
phi Formula -> Formula -> Formula
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 Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
f Formula
psi
    f (Equiv Formula
phi Formula
psi) = Formula -> Formula
f ((Formula
phi Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
psi) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&.  (Formula
psi Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
    f (Forall Var
v Formula
phi)  = Var -> Formula -> Formula
forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
f Formula
phi)
    f (Exists Var
v Formula
phi)  = Var -> Formula -> Formula
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 = Formula
forall a. GenFormula a
F
    g Formula
F = Formula
forall a. GenFormula a
T
    g (And Formula
phi Formula
psi)   = Formula -> Formula
g Formula
phi Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
g Formula
psi
    g (Or Formula
phi Formula
psi)    = Formula -> Formula
g Formula
phi Formula -> Formula -> Formula
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 Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
g Formula
psi
    g (Equiv Formula
phi Formula
psi) = Formula -> Formula
g ((Formula
phi Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
psi) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
psi Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
    g (Forall Var
v Formula
phi)  = Var -> Formula -> Formula
forall a. Var -> GenFormula a -> GenFormula a
Exists Var
v (Formula -> Formula
g Formula
phi)
    g (Exists Var
v Formula
phi)  = Var -> Formula -> Formula
forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
g Formula
phi)
    g (Atom Atom
a)        = Formula -> Formula
forall a. Complement a => a -> a
notB (Atom -> Formula
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 [] Map Var Term
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 = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    f [Var]
_ Map Var Term
_ Formula
F = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
    f [Var]
_ Map Var Term
s (Atom Atom
a) = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Atom -> GenLit Atom
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)) = [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Atom -> GenLit Atom
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
      [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> m [Clause]) -> [Clause] -> m [Clause]
forall a b. (a -> b) -> a -> b
$ [Clause]
phi' [Clause] -> [Clause] -> [Clause]
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
      [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> m [Clause]) -> [Clause] -> m [Clause]
forall a b. (a -> b) -> a -> b
$ [Clause
c1Clause -> Clause -> Clause
forall 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 (Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
v) (Formula -> Set Var
forall a. Vars a => a -> Set Var
vars Formula
psi Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
uvs)
      [Var] -> Map Var Term -> Formula -> m [Clause]
f (Var
v' Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: [Var]
uvs) (Var -> Term -> Map Var Term -> Map Var Term
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 ([Var] -> Entity
forall a. [a] -> Entity
forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Var]
uvs)
      [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs (Var -> Term -> Map Var Term -> Map Var Term
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 <- [Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
uvs]) Map Var Term
s) Formula
phi
    f [Var]
_ Map Var Term
_ Formula
_ = [Char] -> m [Clause]
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 = [Var] -> Var
forall a. HasCallStack => [a] -> a
head [Var
name | Var
name <- [Var]
names, Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
name Set Var
vs]
      where
        names :: [Var]
names = (Text -> Var) -> [Text] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Var
Uninterned Var -> Var
forall t. Interned t => Uninterned t -> t
intern ([Text] -> [Var]) -> [Text] -> [Var]
forall a b. (a -> b) -> a -> b
$ Text
template Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text
template Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
forall a. IsString a => [Char] -> a
fromString (Integer -> [Char]
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 ((Term -> Term) -> [Term] -> [Term]
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)    = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe (Var -> Term
TmVar Var
v) (Var -> Map Var Term -> Maybe Term
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 ((Term -> Term) -> [Term] -> [Term]
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 <- Integer -> IO (IORef Integer)
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 <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
ref
        let fsym :: Var
fsym = Uninterned Var -> Var
forall t. Interned t => Uninterned t -> t
intern (Uninterned Var -> Var) -> Uninterned Var -> Var
forall a b. (a -> b) -> a -> b
$ Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
name Uninterned Var -> Uninterned Var -> Uninterned Var
forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" Uninterned Var -> Uninterned Var -> Uninterned Var
forall a. Semigroup a => a -> a -> a
<> [Char] -> Uninterned Var
forall a. IsString a => [Char] -> a
fromString (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n)
        IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
        Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym

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

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

  [Clause] -> IO ()
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]
[SGenTerm v] -> [Char] -> [Char]
SGenTerm v -> [Char]
(Entity -> SGenTerm v -> [Char] -> [Char])
-> (SGenTerm v -> [Char])
-> ([SGenTerm v] -> [Char] -> [Char])
-> Show (SGenTerm v)
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
$cshowsPrec :: forall v. Show v => Entity -> SGenTerm v -> [Char] -> [Char]
showsPrec :: Entity -> SGenTerm v -> [Char] -> [Char]
$cshow :: forall v. Show v => SGenTerm v -> [Char]
show :: SGenTerm v -> [Char]
$cshowList :: forall v. Show v => [SGenTerm v] -> [Char] -> [Char]
showList :: [SGenTerm v] -> [Char] -> [Char]
Show, SGenTerm v -> SGenTerm v -> Bool
(SGenTerm v -> SGenTerm v -> Bool)
-> (SGenTerm v -> SGenTerm v -> Bool) -> Eq (SGenTerm v)
forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: SGenTerm v -> SGenTerm v -> Bool
Eq, Eq (SGenTerm v)
Eq (SGenTerm v) =>
(SGenTerm v -> SGenTerm v -> Ordering)
-> (SGenTerm v -> SGenTerm v -> Bool)
-> (SGenTerm v -> SGenTerm v -> Bool)
-> (SGenTerm v -> SGenTerm v -> Bool)
-> (SGenTerm v -> SGenTerm v -> Bool)
-> (SGenTerm v -> SGenTerm v -> SGenTerm v)
-> (SGenTerm v -> SGenTerm v -> SGenTerm v)
-> Ord (SGenTerm v)
SGenTerm v -> SGenTerm v -> Bool
SGenTerm v -> SGenTerm v -> Ordering
SGenTerm v -> SGenTerm v -> SGenTerm v
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
$ccompare :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Ordering
compare :: SGenTerm v -> SGenTerm v -> Ordering
$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
>= :: SGenTerm v -> SGenTerm v -> Bool
$cmax :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
max :: SGenTerm v -> SGenTerm v -> SGenTerm v
$cmin :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
min :: SGenTerm v -> SGenTerm v -> SGenTerm v
Ord)

-- | Shallow atom
data SGenAtom v
  = SPApp PSym [v]
  | SEq (SGenTerm v) v
  deriving (Entity -> SGenAtom v -> [Char] -> [Char]
[SGenAtom v] -> [Char] -> [Char]
SGenAtom v -> [Char]
(Entity -> SGenAtom v -> [Char] -> [Char])
-> (SGenAtom v -> [Char])
-> ([SGenAtom v] -> [Char] -> [Char])
-> Show (SGenAtom v)
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
$cshowsPrec :: forall v. Show v => Entity -> SGenAtom v -> [Char] -> [Char]
showsPrec :: Entity -> SGenAtom v -> [Char] -> [Char]
$cshow :: forall v. Show v => SGenAtom v -> [Char]
show :: SGenAtom v -> [Char]
$cshowList :: forall v. Show v => [SGenAtom v] -> [Char] -> [Char]
showList :: [SGenAtom v] -> [Char] -> [Char]
Show, SGenAtom v -> SGenAtom v -> Bool
(SGenAtom v -> SGenAtom v -> Bool)
-> (SGenAtom v -> SGenAtom v -> Bool) -> Eq (SGenAtom v)
forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: SGenAtom v -> SGenAtom v -> Bool
Eq, Eq (SGenAtom v)
Eq (SGenAtom v) =>
(SGenAtom v -> SGenAtom v -> Ordering)
-> (SGenAtom v -> SGenAtom v -> Bool)
-> (SGenAtom v -> SGenAtom v -> Bool)
-> (SGenAtom v -> SGenAtom v -> Bool)
-> (SGenAtom v -> SGenAtom v -> Bool)
-> (SGenAtom v -> SGenAtom v -> SGenAtom v)
-> (SGenAtom v -> SGenAtom v -> SGenAtom v)
-> Ord (SGenAtom v)
SGenAtom v -> SGenAtom v -> Bool
SGenAtom v -> SGenAtom v -> Ordering
SGenAtom v -> SGenAtom v -> SGenAtom v
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
$ccompare :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Ordering
compare :: SGenAtom v -> SGenAtom v -> Ordering
$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
>= :: SGenAtom v -> SGenAtom v -> Bool
$cmax :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
max :: SGenAtom v -> SGenAtom v -> SGenAtom v
$cmin :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
min :: SGenAtom v -> SGenAtom v -> SGenAtom v
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) = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
  vars (STmVar Var
v)    = Var -> Set Var
forall a. a -> Set a
Set.singleton Var
v

instance Vars SAtom where
  vars :: SAtom -> Set Var
vars (SPApp Var
_ [Var]
xs) = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
  vars (SEq STerm
t Var
v) = Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v (STerm -> Set Var
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 State (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) [SLit]
-> (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
-> ([SLit], (Set Var, Entity, Map (Var, [Var]) Var, [SLit]))
forall s a. State s a -> s -> (a, s)
runState ((GenLit Atom
 -> StateT
      (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit)
-> Clause
-> State (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) [SLit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM GenLit Atom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
flattenLit Clause
c) (Clause -> Set Var
forall a. Vars a => a -> Set Var
vars Clause
c, Entity
0, Map (Var, [Var]) Var
forall k a. Map k a
Map.empty, []) of
    ([SLit]
c, (Set Var
_,Entity
_,Map (Var, [Var]) Var
_,[SLit]
ls)) -> [SLit] -> Maybe [SLit]
removeTautology ([SLit] -> Maybe [SLit]) -> [SLit] -> Maybe [SLit]
forall a b. (a -> b) -> a -> b
$ [SLit] -> [SLit]
removeNegEq ([SLit] -> [SLit]) -> [SLit] -> [SLit]
forall a b. (a -> b) -> a -> b
$ [SLit]
ls [SLit] -> [SLit] -> [SLit]
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) <- StateT
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
  Identity
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
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 = Uninterned Var -> Var
forall t. Interned t => Uninterned t -> t
intern (Uninterned Var -> Var) -> Uninterned Var -> Var
forall a b. (a -> b) -> a -> b
$ Uninterned Var
"#" Uninterned Var -> Uninterned Var -> Uninterned Var
forall a. Semigroup a => a -> a -> a
<> [Char] -> Uninterned Var
forall a. IsString a => [Char] -> a
fromString (Entity -> [Char]
forall a. Show a => a -> [Char]
show Entity
m)
            if Var
v Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Var
vs
              then Entity -> M Var
go (Entity
mEntity -> Entity -> Entity
forall a. Num a => a -> a -> a
+Entity
1)
              else do
                (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v Set Var
vs, Entity
mEntity -> Entity -> Entity
forall a. Num a => a -> a -> a
+Entity
1, Map (Var, [Var]) Var
defs, [SLit]
ls)
                Var -> M Var
forall a.
a
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
      Entity -> M Var
go Entity
n

    flattenLit :: Lit -> M SLit
    flattenLit :: GenLit Atom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
flattenLit (Pos Atom
a) = (SAtom -> SLit)
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SAtom -> SLit
forall a. a -> GenLit a
Pos (StateT
   (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
 -> StateT
      (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit)
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
forall a b. (a -> b) -> a -> b
$ Atom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
flattenAtom Atom
a
    flattenLit (Neg Atom
a) = (SAtom -> SLit)
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SAtom -> SLit
forall a. a -> GenLit a
Neg (StateT
   (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
 -> StateT
      (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit)
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SLit
forall a b. (a -> b) -> a -> b
$ Atom
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity SAtom
flattenAtom Atom
a

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

    flattenTerm :: Term -> M Var
    flattenTerm :: Term -> M Var
flattenTerm (TmVar Var
x)    = Var -> M Var
forall a.
a
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
    flattenTerm (TmApp Var
f [Term]
ts) = do
      [Var]
xs <- (Term -> M Var)
-> [Term]
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term -> M Var
flattenTerm [Term]
ts
      (Set Var
_, Entity
_, Map (Var, [Var]) Var
defs, [SLit]
_) <- StateT
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
  Identity
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
forall s (m :: * -> *). MonadState s m => m s
get
      case (Var, [Var]) -> Map (Var, [Var]) Var -> Maybe Var
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 -> Var -> M Var
forall a.
a
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity a
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) <- StateT
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
  Identity
  (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
forall s (m :: * -> *). MonadState s m => m s
get
          (Set Var, Entity, Map (Var, [Var]) Var, [SLit])
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Var
vs, Entity
n, (Var, [Var]) -> Var -> Map (Var, [Var]) Var -> Map (Var, [Var]) Var
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, SAtom -> SLit
forall a. a -> GenLit a
Neg (STerm -> Var -> SAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> [Var] -> STerm
forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x) SLit -> [SLit] -> [SLit]
forall a. a -> [a] -> [a]
: [SLit]
ls)
          Var -> M Var
forall a.
a
-> StateT
     (Set Var, Entity, Map (Var, [Var]) Var, [SLit]) Identity a
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 ((SLit -> SLit) -> [SLit] -> [SLit]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) [SLit]
r) ((SLit -> SLit) -> [SLit] -> [SLit]
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 SLit -> [SLit] -> [SLit]
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) = SAtom -> SLit
forall a. a -> GenLit a
Pos (SAtom -> SLit) -> SAtom -> SLit
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) = SAtom -> SLit
forall a. a -> GenLit a
Neg (SAtom -> SLit) -> SAtom -> SLit
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) = Var -> [Var] -> SAtom
forall v. Var -> [v] -> SGenAtom v
SPApp Var
p ((Var -> Var) -> [Var] -> [Var]
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)    = STerm -> Var -> SAtom
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) = Var -> [Var] -> STerm
forall v. Var -> [v] -> SGenTerm v
STmApp Var
f ((Var -> Var) -> [Var] -> [Var]
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)    = Var -> STerm
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
vVar -> Var -> Bool
forall 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
      | Set SAtom -> Bool
forall a. Set a -> Bool
Set.null (Set SAtom
pos Set SAtom -> Set SAtom -> Set SAtom
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set SAtom
neg) = [SLit] -> Maybe [SLit]
forall a. a -> Maybe a
Just ([SLit] -> Maybe [SLit]) -> [SLit] -> Maybe [SLit]
forall a b. (a -> b) -> a -> b
$ [SAtom -> SLit
forall a. a -> GenLit a
Neg SAtom
l | SAtom
l <- Set SAtom -> [SAtom]
forall a. Set a -> [a]
Set.toList Set SAtom
neg] [SLit] -> [SLit] -> [SLit]
forall a. [a] -> [a] -> [a]
++ [SAtom -> SLit
forall a. a -> GenLit a
Pos SAtom
l | SAtom
l <- Set SAtom -> [SAtom]
forall a. Set a -> [a]
Set.toList Set SAtom
pos]
      | Bool
otherwise = Maybe [SLit]
forall a. Maybe a
Nothing
      where
        pos :: Set SAtom
pos = [SAtom] -> Set SAtom
forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Pos SAtom
l <- [SLit]
lits]
        neg :: Set SAtom
neg = [SAtom] -> Set SAtom
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 [Atom -> GenLit Atom
forall a. a -> GenLit a
Pos (Atom -> GenLit Atom) -> Atom -> GenLit Atom
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]
"$" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Entity -> [Char]
forall a. Show a => a -> [Char]
show Entity
e

showEntityTuple :: EntityTuple -> String
showEntityTuple :: EntityTuple -> [Char]
showEntityTuple EntityTuple
xs = [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"(%s)" ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Entity -> [Char]) -> EntityTuple -> [[Char]]
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 <- [[(Var, Entity)]] -> [[(Var, Entity)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [[(Var
v,Entity
e) | Entity
e <- EntityTuple
univ] | Var
v <- Set Var -> [Var]
forall a. Set a -> [a]
Set.toList Set Var
vs]
  Subst -> [Subst]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> [Subst]) -> Subst -> [Subst]
forall a b. (a -> b) -> a -> b
$ [(Var, Entity)] -> Subst
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 = (SLit -> GroundLit) -> [SLit] -> GroundClause
forall a b. (a -> b) -> [a] -> [b]
map SLit -> GroundLit
substLit
  where
    substLit :: SLit -> GroundLit
    substLit :: SLit -> GroundLit
substLit (Pos SAtom
a) = GroundAtom -> GroundLit
forall a. a -> GenLit a
Pos (GroundAtom -> GroundLit) -> GroundAtom -> GroundLit
forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a
    substLit (Neg SAtom
a) = GroundAtom -> GroundLit
forall a. a -> GenLit a
Neg (GroundAtom -> GroundLit) -> GroundAtom -> GroundLit
forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a

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

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

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

simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause = ([GroundClause] -> GroundClause)
-> Maybe [GroundClause] -> Maybe GroundClause
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [GroundClause] -> GroundClause
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Maybe [GroundClause] -> Maybe GroundClause)
-> (GroundClause -> Maybe [GroundClause])
-> GroundClause
-> Maybe GroundClause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GroundLit -> Maybe GroundClause)
-> GroundClause -> Maybe [GroundClause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
xEntity -> Entity -> Bool
forall a. Eq a => a -> a -> Bool
==Entity
y then Maybe GroundClause
forall a. Maybe a
Nothing else GroundClause -> Maybe GroundClause
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    f GroundLit
lit = GroundClause -> Maybe GroundClause
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [GroundLit
lit]

collectFSym :: Clause -> Set (FSym, Int)
collectFSym :: Clause -> Set (Var, Entity)
collectFSym = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> (Clause -> [Set (Var, Entity)]) -> Clause -> Set (Var, Entity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenLit Atom -> Set (Var, Entity)) -> Clause -> [Set (Var, Entity)]
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) = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> [Set (Var, Entity)] -> Set (Var, Entity)
forall a b. (a -> b) -> a -> b
$ (Term -> Set (Var, Entity)) -> [Term] -> [Set (Var, Entity)]
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
_) = Set (Var, Entity)
forall a. Set a
Set.empty
    h (TmApp Var
f [Term]
xs) = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> [Set (Var, Entity)] -> Set (Var, Entity)
forall a b. (a -> b) -> a -> b
$ (Var, Entity) -> Set (Var, Entity)
forall a. a -> Set a
Set.singleton (Var
f, [Term] -> Entity
forall a. [a] -> Entity
forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Term]
xs) Set (Var, Entity) -> [Set (Var, Entity)] -> [Set (Var, Entity)]
forall a. a -> [a] -> [a]
: (Term -> Set (Var, Entity)) -> [Term] -> [Set (Var, Entity)]
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 = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> (Clause -> [Set (Var, Entity)]) -> Clause -> Set (Var, Entity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenLit Atom -> Set (Var, Entity)) -> Clause -> [Set (Var, Entity)]
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
_]) = Set (Var, Entity)
forall a. Set a
Set.empty
    g (PApp Var
p [Term]
xs) = (Var, Entity) -> Set (Var, Entity)
forall a. a -> Set a
Set.singleton (Var
p, [Term] -> Entity
forall a. [a] -> Entity
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 =
  [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"DOMAIN = {%s}" ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ((Entity -> [Char]) -> EntityTuple -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Entity -> [Char]
showEntity (Model -> EntityTuple
mUniverse Model
m))) [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
  [ [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"%s = { %s }" (Text -> [Char]
Text.unpack (Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
p)) [Char]
s
  | (Var
p, Set EntityTuple
xss) <- Map Var (Set EntityTuple) -> [(Var, Set EntityTuple)]
forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Set EntityTuple)
mRelations Model
m)
  , let s :: [Char]
s = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [if EntityTuple -> Entity
forall a. [a] -> Entity
forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs Entity -> Entity -> Bool
forall a. Eq a => a -> a -> Bool
== Entity
1 then Entity -> [Char]
showEntity (EntityTuple -> Entity
forall a. HasCallStack => [a] -> a
head EntityTuple
xs) else EntityTuple -> [Char]
showEntityTuple EntityTuple
xs | EntityTuple
xs <- Set EntityTuple -> [EntityTuple]
forall a. Set a -> [a]
Set.toList Set EntityTuple
xss]
  ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
  [ [Char] -> [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"%s%s = %s" (Text -> [Char]
Text.unpack (Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
f)) (if EntityTuple -> Entity
forall a. [a] -> Entity
forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs Entity -> Entity -> Bool
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) <- Map Var (Map EntityTuple Entity) -> [(Var, Map EntityTuple Entity)]
forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Map EntityTuple Entity)
mFunctions Model
m)
  , (EntityTuple
xs, Entity
y) <- Map EntityTuple Entity -> [(EntityTuple, Entity)]
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 Subst
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 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Subst -> Formula -> Bool
f Subst
env Formula
phi2
    f Subst
env (Forall Var
v Formula
phi) = (Entity -> Bool) -> EntityTuple -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Entity
e -> Subst -> Formula -> Bool
f (Var -> Entity -> Subst -> Subst
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) = (Entity -> Bool) -> EntityTuple -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Entity
e -> Subst -> Formula -> Bool
f (Var -> Entity -> Subst -> Subst
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 Entity -> Entity -> Bool
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) = (Term -> Entity) -> [Term] -> EntityTuple
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env) [Term]
xs EntityTuple -> Set EntityTuple -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` (Model -> Map Var (Set EntityTuple)
mRelations Model
m Map Var (Set EntityTuple) -> Var -> Set EntityTuple
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 Subst -> Var -> Entity
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 Map Var (Map EntityTuple Entity) -> Var -> Map EntityTuple Entity
forall k a. Ord k => Map k a -> k -> a
Map.! Var
f) Map EntityTuple Entity -> EntityTuple -> Entity
forall k a. Ord k => Map k a -> k -> a
Map.! (Term -> Entity) -> [Term] -> EntityTuple
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 (Bool -> Bool) -> Bool -> Bool
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 = (GenLit Atom -> Bool) -> Clause -> Bool
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 = (Clause -> Bool) -> [Clause] -> Bool
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 = (Subst -> Bool) -> [Subst] -> Bool
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 ([Clause] -> Set Var
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
sizeEntity -> Entity -> Entity
forall a. Num a => a -> a -> a
-Entity
1]

  let cs2 :: [[SLit]]
cs2 = (Clause -> Maybe [SLit]) -> [Clause] -> [[SLit]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Clause -> Maybe [SLit]
flatten [Clause]
cs
      fs :: Set (Var, Entity)
fs = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> [Set (Var, Entity)] -> Set (Var, Entity)
forall a b. (a -> b) -> a -> b
$ (Clause -> Set (Var, Entity)) -> [Clause] -> [Set (Var, Entity)]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Set (Var, Entity)
collectFSym [Clause]
cs
      ps :: Set (Var, Entity)
ps = [Set (Var, Entity)] -> Set (Var, Entity)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (Var, Entity)] -> Set (Var, Entity))
-> [Set (Var, Entity)] -> Set (Var, Entity)
forall a b. (a -> b) -> a -> b
$ (Clause -> Set (Var, Entity)) -> [Clause] -> [Set (Var, Entity)]
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 <- Map GroundAtom Entity -> IO (IORef (Map GroundAtom Entity))
forall a. a -> IO (IORef a)
newIORef Map GroundAtom Entity
forall k a. Map k a
Map.empty

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

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

  -- Instances
  [[SLit]] -> ([SLit] -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[SLit]]
cs2 (([SLit] -> IO ()) -> IO ()) -> ([SLit] -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \[SLit]
c -> do
    [Subst] -> (Subst -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set Var -> EntityTuple -> [Subst]
enumSubst ([SLit] -> Set Var
forall a. Vars a => a -> Set Var
vars [SLit]
c) EntityTuple
univ) ((Subst -> IO ()) -> IO ()) -> (Subst -> IO ()) -> IO ()
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 -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just GroundClause
c' -> Solver -> EntityTuple -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver (EntityTuple -> IO ()) -> IO EntityTuple -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GroundClause -> IO EntityTuple
translateClause GroundClause
c'

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

  -- Totality definitions
  [(Var, Entity)] -> ((Var, Entity) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set (Var, Entity) -> [(Var, Entity)]
forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs) (((Var, Entity) -> IO ()) -> IO ())
-> ((Var, Entity) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
f, Entity
arity) -> do
    [EntityTuple] -> (EntityTuple -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Entity -> EntityTuple -> [EntityTuple]
forall (m :: * -> *) a. Applicative m => Entity -> m a -> m [a]
replicateM Entity
arity EntityTuple
univ) ((EntityTuple -> IO ()) -> IO ())
-> (EntityTuple -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EntityTuple
args -> do
        let c :: GroundClause
c = [GroundAtom -> GroundLit
forall a. a -> GenLit a
Pos (SGenTerm Entity -> Entity -> GroundAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> EntityTuple -> SGenTerm Entity
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
        Solver -> EntityTuple -> IO ()
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 <- IORef (Map GroundAtom Entity) -> IO (Map GroundAtom Entity)
forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Entity)
ref

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

      Maybe Model -> IO (Maybe Model)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model -> Maybe Model
forall a. a -> Maybe a
Just Model
model)
    else do
      Maybe Model -> IO (Maybe Model)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Model
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 = [Atom -> GenLit Atom
forall a. a -> GenLit a
Pos (Atom -> GenLit Atom) -> Atom -> GenLit Atom
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 = [Atom -> GenLit Atom
forall a. a -> GenLit a
Neg (Atom -> GenLit Atom) -> Atom -> GenLit Atom
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 ==="
      ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn ([[Char]] -> IO ()) -> [[Char]] -> IO ()
forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m

test2 :: IO ()
test2 = do
  let phi :: Formula
phi = Var -> Formula -> Formula
forall a. Var -> GenFormula a -> GenFormula a
Forall Var
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ Var -> Formula -> Formula
forall a. Var -> GenFormula a -> GenFormula a
Exists Var
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
              Formula -> Formula
forall a. Complement a => a -> a
notB (Atom -> Formula
forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"=" [Var -> Term
TmVar Var
"x", Var -> Term
TmVar Var
"y"])) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&.
              Atom -> Formula
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 <- Integer -> IO (IORef Integer)
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 <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
ref
        let fsym :: Var
fsym = Uninterned Var -> Var
forall t. Interned t => Uninterned t -> t
intern (Uninterned Var -> Var) -> Uninterned Var -> Var
forall a b. (a -> b) -> a -> b
$ Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
name Uninterned Var -> Uninterned Var -> Uninterned Var
forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" Uninterned Var -> Uninterned Var -> Uninterned Var
forall a. Semigroup a => a -> a -> a
<> [Char] -> Uninterned Var
forall a. IsString a => [Char] -> a
fromString (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n)
        IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)
        Var -> IO Var
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym
  [Clause]
cs <- (Var -> Entity -> IO Var) -> Formula -> IO [Clause]
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 ==="
      ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn ([[Char]] -> IO ()) -> [[Char]] -> IO ()
forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m

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