{-# 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 (Int -> GenLit a -> ShowS
[GenLit a] -> ShowS
GenLit a -> String
(Int -> GenLit a -> ShowS)
-> (GenLit a -> String) -> ([GenLit a] -> ShowS) -> Show (GenLit a)
forall a. Show a => Int -> GenLit a -> ShowS
forall a. Show a => [GenLit a] -> ShowS
forall a. Show a => GenLit a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenLit a] -> ShowS
$cshowList :: forall a. Show a => [GenLit a] -> ShowS
show :: GenLit a -> String
$cshow :: forall a. Show a => GenLit a -> String
showsPrec :: Int -> GenLit a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> GenLit a -> ShowS
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
/= :: 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, 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
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
$cp1Ord :: forall a. Ord a => Eq (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 (Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
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
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
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
$cp1Ord :: Eq Term
Ord)

data Atom = PApp PSym [Term]
  deriving (Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Atom] -> ShowS
$cshowList :: [Atom] -> ShowS
show :: Atom -> String
$cshow :: Atom -> String
showsPrec :: Int -> Atom -> ShowS
$cshowsPrec :: Int -> Atom -> ShowS
Show, Atom -> Atom -> Bool
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
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
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
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
$cp1Ord :: Eq 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 (Int -> GenFormula a -> ShowS
[GenFormula a] -> ShowS
GenFormula a -> String
(Int -> GenFormula a -> ShowS)
-> (GenFormula a -> String)
-> ([GenFormula a] -> ShowS)
-> Show (GenFormula a)
forall a. Show a => Int -> GenFormula a -> ShowS
forall a. Show a => [GenFormula a] -> ShowS
forall a. Show a => GenFormula a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenFormula a] -> ShowS
$cshowList :: forall a. Show a => [GenFormula a] -> ShowS
show :: GenFormula a -> String
$cshow :: forall a. Show a => GenFormula a -> String
showsPrec :: Int -> GenFormula a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> GenFormula a -> ShowS
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
/= :: 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, 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
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
$cp1Ord :: forall a. Ord a => Eq (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 :: (Var -> Int -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Int -> 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 (m :: * -> *) a. Monad m => a -> m a
return []
    f [Var]
_ Map Var Term
_ Formula
F = [Clause] -> m [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
    f [Var]
_ Map Var Term
s (Atom Atom
a) = [Clause] -> m [Clause]
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 (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 (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 (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 -> Int -> m Var
skolem Var
v ([Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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
_ = String -> m [Clause]
forall a. HasCallStack => String -> a
error String
"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. [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
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
<> String -> Text
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
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 -> Int -> IO Var
skolem Var
name Int
_ = 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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
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 (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 -> Int -> IO Var) -> Formula -> IO [Clause]
forall (m :: * -> *).
Monad m =>
(Var -> Int -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Int -> 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 (Int -> SGenTerm v -> ShowS
[SGenTerm v] -> ShowS
SGenTerm v -> String
(Int -> SGenTerm v -> ShowS)
-> (SGenTerm v -> String)
-> ([SGenTerm v] -> ShowS)
-> Show (SGenTerm v)
forall v. Show v => Int -> SGenTerm v -> ShowS
forall v. Show v => [SGenTerm v] -> ShowS
forall v. Show v => SGenTerm v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SGenTerm v] -> ShowS
$cshowList :: forall v. Show v => [SGenTerm v] -> ShowS
show :: SGenTerm v -> String
$cshow :: forall v. Show v => SGenTerm v -> String
showsPrec :: Int -> SGenTerm v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> SGenTerm v -> ShowS
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
/= :: 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, 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
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
$cp1Ord :: forall v. Ord v => Eq (SGenTerm v)
Ord)

-- | Shallow atom
data SGenAtom v
  = SPApp PSym [v]
  | SEq (SGenTerm v) v
  deriving (Int -> SGenAtom v -> ShowS
[SGenAtom v] -> ShowS
SGenAtom v -> String
(Int -> SGenAtom v -> ShowS)
-> (SGenAtom v -> String)
-> ([SGenAtom v] -> ShowS)
-> Show (SGenAtom v)
forall v. Show v => Int -> SGenAtom v -> ShowS
forall v. Show v => [SGenAtom v] -> ShowS
forall v. Show v => SGenAtom v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SGenAtom v] -> ShowS
$cshowList :: forall v. Show v => [SGenAtom v] -> ShowS
show :: SGenAtom v -> String
$cshow :: forall v. Show v => SGenAtom v -> String
showsPrec :: Int -> SGenAtom v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> SGenAtom v -> ShowS
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
/= :: 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, 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
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
$cp1Ord :: forall v. Ord v => Eq (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 SClause
flatten Clause
c =
  case State (Set Var, Int, Map (Var, [Var]) Var, SClause) SClause
-> (Set Var, Int, Map (Var, [Var]) Var, SClause)
-> (SClause, (Set Var, Int, Map (Var, [Var]) Var, SClause))
forall s a. State s a -> s -> (a, s)
runState ((GenLit Atom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit)
-> Clause
-> State (Set Var, Int, Map (Var, [Var]) Var, SClause) SClause
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GenLit Atom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit
flattenLit Clause
c) (Clause -> Set Var
forall a. Vars a => a -> Set Var
vars Clause
c, Int
0, Map (Var, [Var]) Var
forall k a. Map k a
Map.empty, []) of
    (SClause
c, (Set Var
_,Int
_,Map (Var, [Var]) Var
_,SClause
ls)) -> SClause -> Maybe SClause
removeTautology (SClause -> Maybe SClause) -> SClause -> Maybe SClause
forall a b. (a -> b) -> a -> b
$ SClause -> SClause
removeNegEq (SClause -> SClause) -> SClause -> SClause
forall a b. (a -> b) -> a -> b
$ SClause
ls SClause -> SClause -> SClause
forall a. [a] -> [a] -> [a]
++ SClause
c
  where
    gensym :: M Var
    gensym :: M Var
gensym = do
      (Set Var
vs, Int
n, Map (Var, [Var]) Var
defs, SClause
ls) <- StateT
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
  Identity
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
forall s (m :: * -> *). MonadState s m => m s
get
      let go :: Int -> M Var
          go :: Int -> M Var
go Int
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
<> String -> Uninterned Var
forall a. IsString a => String -> a
fromString (Int -> String
forall a. Show a => a -> String
show Int
m)
            if Var
v Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Var
vs
              then Int -> M Var
go (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
              else do
                (Set Var, Int, Map (Var, [Var]) Var, SClause)
-> StateT (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, Map (Var, [Var]) Var
defs, SClause
ls)
                Var -> M Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
      Int -> M Var
go Int
n

    flattenLit :: Lit -> M SLit
    flattenLit :: GenLit Atom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit
flattenLit (Pos Atom
a) = (SAtom -> SLit)
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit)
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit
forall a b. (a -> b) -> a -> b
$ Atom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
flattenAtom Atom
a
    flattenLit (Neg Atom
a) = (SAtom -> SLit)
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit)
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SLit
forall a b. (a -> b) -> a -> b
$ Atom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
flattenAtom Atom
a

    flattenAtom :: Atom -> M SAtom
    flattenAtom :: Atom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
flattenAtom (PApp Var
"=" [TmVar Var
x, TmVar Var
y])    = SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom)
-> SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom)
-> SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom)
-> SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity [Var]
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
      SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom)
-> SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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, Int, Map (Var, [Var]) Var, SClause) Identity [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
      SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom
forall (m :: * -> *) a. Monad m => a -> m a
return (SAtom
 -> StateT
      (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity SAtom)
-> SAtom
-> StateT
     (Set Var, Int, Map (Var, [Var]) Var, SClause) 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 (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, Int, Map (Var, [Var]) Var, SClause) Identity [Var]
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
_, Int
_, Map (Var, [Var]) Var
defs, SClause
_) <- StateT
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
  Identity
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
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 (m :: * -> *) a. Monad m => a -> m a
return Var
x
        Maybe Var
Nothing -> do
          Var
x <- M Var
gensym
          (Set Var
vs, Int
n, Map (Var, [Var]) Var
defs, SClause
ls) <- StateT
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
  Identity
  (Set Var, Int, Map (Var, [Var]) Var, SClause)
forall s (m :: * -> *). MonadState s m => m s
get
          (Set Var, Int, Map (Var, [Var]) Var, SClause)
-> StateT (Set Var, Int, Map (Var, [Var]) Var, SClause) Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Var
vs, Int
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 -> SClause -> SClause
forall a. a -> [a] -> [a]
: SClause
ls)
          Var -> M Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
x

    removeNegEq :: SClause -> SClause
    removeNegEq :: SClause -> SClause
removeNegEq = SClause -> SClause -> SClause
go []
      where
        go :: SClause -> SClause -> SClause
go SClause
r [] = SClause
r
        go SClause
r (Neg (SEq (STmVar Var
x) Var
y) : SClause
ls) = SClause -> SClause -> SClause
go ((SLit -> SLit) -> SClause -> SClause
forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) SClause
r) ((SLit -> SLit) -> SClause -> SClause
forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) SClause
ls)
        go SClause
r (SLit
l : SClause
ls) = SClause -> SClause -> SClause
go (SLit
l SLit -> SClause -> SClause
forall a. a -> [a] -> [a]
: SClause
r) SClause
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 :: SClause -> Maybe SClause
removeTautology SClause
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) = SClause -> Maybe SClause
forall a. a -> Maybe a
Just (SClause -> Maybe SClause) -> SClause -> Maybe SClause
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] SClause -> SClause -> SClause
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 SClause
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 <- SClause
lits]
        neg :: Set SAtom
neg = [SAtom] -> Set SAtom
forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Neg SAtom
l <- SClause
lits]

test_flatten :: Maybe SClause
test_flatten = Clause -> Maybe SClause
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 :: Int -> String
showEntity Int
e = String
"$" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
e

showEntityTuple :: EntityTuple -> String
showEntityTuple :: EntityTuple -> String
showEntityTuple EntityTuple
xs = String -> ShowS
forall r. PrintfType r => String -> r
printf String
"(%s)" ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> EntityTuple -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
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, Int)]
ps <- [[(Var, Int)]] -> [[(Var, Int)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(Var
v,Int
e) | Int
e <- EntityTuple
univ] | Var
v <- Set Var -> [Var]
forall a. Set a -> [a]
Set.toList Set Var
vs]
  Subst -> [Subst]
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> [Subst]) -> Subst -> [Subst]
forall a b. (a -> b) -> a -> b
$ [(Var, Int)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var, Int)]
ps

applySubst :: Subst -> SClause -> GroundClause
applySubst :: Subst -> SClause -> GroundClause
applySubst Subst
s = (SLit -> GroundLit) -> SClause -> 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 -> Int) -> [Var] -> EntityTuple
forall a b. (a -> b) -> [a] -> [b]
map Var -> Int
substVar [Var]
xs)
    substAtom (SEq STerm
t Var
v)    = SGenTerm Int -> Int -> GroundAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (STerm -> SGenTerm Int
substTerm STerm
t) (Var -> Int
substVar Var
v)

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

    substVar :: Var -> Entity
    substVar :: Var -> Int
substVar = (Subst
s Subst -> Var -> Int
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)
mapM GroundLit -> Maybe GroundClause
f
  where
    f :: GroundLit -> Maybe [GroundLit]
    f :: GroundLit -> Maybe GroundClause
f (Pos (SEq (STmVar Int
x) Int
y)) = if Int
xInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
y then Maybe GroundClause
forall a. Maybe a
Nothing else GroundClause -> Maybe GroundClause
forall (m :: * -> *) a. Monad m => a -> m a
return []
    f GroundLit
lit = GroundClause -> Maybe GroundClause
forall (m :: * -> *) a. Monad m => a -> m a
return [GroundLit
lit]

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

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

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

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

    g :: Atom -> Set (PSym, Int)
    g :: Atom -> Set (Var, Int)
g (PApp Var
"=" [Term
_,Term
_]) = Set (Var, Int)
forall a. Set a
Set.empty
    g (PApp Var
p [Term]
xs) = (Var, Int) -> Set (Var, Int)
forall a. a -> Set a
Set.singleton (Var
p, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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 Int)
mFunctions :: Map FSym (Map EntityTuple Entity)
  }

showModel :: Model -> [String]
showModel :: Model -> [String]
showModel Model
m =
  String -> ShowS
forall r. PrintfType r => String -> r
printf String
"DOMAIN = {%s}" (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Int -> String) -> EntityTuple -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
showEntity (Model -> EntityTuple
mUniverse Model
m))) String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
  [ String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s = { %s }" (Text -> String
Text.unpack (Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
p)) String
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 :: String
s = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [if EntityTuple -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EntityTuple
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Int -> String
showEntity (EntityTuple -> Int
forall a. [a] -> a
head EntityTuple
xs) else EntityTuple -> String
showEntityTuple EntityTuple
xs | EntityTuple
xs <- Set EntityTuple -> [EntityTuple]
forall a. Set a -> [a]
Set.toList Set EntityTuple
xss]
  ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
  [ String -> String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"%s%s = %s" (Text -> String
Text.unpack (Var -> Uninterned Var
forall t. Uninternable t => t -> Uninterned t
unintern Var
f)) (if EntityTuple -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length EntityTuple
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String
"" else EntityTuple -> String
showEntityTuple EntityTuple
xs) (Int -> String
showEntity Int
y)
  | (Var
f, Map EntityTuple Int
xss) <- Map Var (Map EntityTuple Int) -> [(Var, Map EntityTuple Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Map EntityTuple Int)
mFunctions Model
m)
  , (EntityTuple
xs, Int
y) <- Map EntityTuple Int -> [(EntityTuple, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map EntityTuple Int
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) = (Int -> Bool) -> EntityTuple -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
e -> Subst -> Formula -> Bool
f (Var -> Int -> Subst -> Subst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Int
e Subst
env) Formula
phi) (Model -> EntityTuple
mUniverse Model
m)
    f Subst
env (Exists Var
v Formula
phi) = (Int -> Bool) -> EntityTuple -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
e -> Subst -> Formula -> Bool
f (Var -> Int -> Subst -> Subst
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Int
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 -> Int
evalTerm Model
m Subst
env Term
x1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Model -> Subst -> Term -> Int
evalTerm Model
m Subst
env Term
x2
evalAtom Model
m Subst
env (PApp Var
p [Term]
xs) = (Term -> Int) -> [Term] -> EntityTuple
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Int
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 -> Int
evalTerm Model
m Subst
env (TmVar Var
v) = Subst
env Subst -> Var -> Int
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 Int)
mFunctions Model
m Map Var (Map EntityTuple Int) -> Var -> Map EntityTuple Int
forall k a. Ord k => Map k a -> k -> a
Map.! Var
f) Map EntityTuple Int -> EntityTuple -> Int
forall k a. Ord k => Map k a -> k -> a
Map.! (Term -> Int) -> [Term] -> EntityTuple
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Int
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 :: Int -> [Clause] -> IO (Maybe Model)
findModel Int
size [Clause]
cs = do
  let univ :: EntityTuple
univ = [Int
0..Int
sizeInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]

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

  Solver
solver <- IO Solver
SAT.newSolver

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

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

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

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

  -- Instances
  [SClause] -> (SClause -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SClause]
cs2 ((SClause -> IO ()) -> IO ()) -> (SClause -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \SClause
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 (SClause -> Set Var
forall a. Vars a => a -> Set Var
vars SClause
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 -> SClause -> GroundClause
applySubst Subst
s SClause
c) of
        Maybe GroundClause
Nothing -> () -> IO ()
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, Int)] -> ((Var, Int) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set (Var, Int) -> [(Var, Int)]
forall a. Set a -> [a]
Set.toList Set (Var, Int)
fs) (((Var, Int) -> IO ()) -> IO ()) -> ((Var, Int) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
f, Int
arity) -> do
    [EntityTuple] -> (EntityTuple -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> EntityTuple -> [EntityTuple]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
arity EntityTuple
univ) ((EntityTuple -> IO ()) -> IO ())
-> (EntityTuple -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \EntityTuple
args ->
      [(Int, Int)] -> ((Int, Int) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Int
y1,Int
y2) | Int
y1 <- EntityTuple
univ, Int
y2 <- EntityTuple
univ, Int
y1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y2] (((Int, Int) -> IO ()) -> IO ()) -> ((Int, Int) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
y1,Int
y2) -> do
        let c :: GroundClause
c = [GroundAtom -> GroundLit
forall a. a -> GenLit a
Neg (SGenTerm Int -> Int -> GroundAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> EntityTuple -> SGenTerm Int
forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Int
y1), GroundAtom -> GroundLit
forall a. a -> GenLit a
Neg (SGenTerm Int -> Int -> GroundAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> EntityTuple -> SGenTerm Int
forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Int
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, Int)] -> ((Var, Int) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set (Var, Int) -> [(Var, Int)]
forall a. Set a -> [a]
Set.toList Set (Var, Int)
fs) (((Var, Int) -> IO ()) -> IO ()) -> ((Var, Int) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Var
f, Int
arity) -> do
    [EntityTuple] -> (EntityTuple -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Int -> EntityTuple -> [EntityTuple]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
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 Int -> Int -> GroundAtom
forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> EntityTuple -> SGenTerm Int
forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Int
y) | Int
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 Int
m <- IORef (Map GroundAtom Int) -> IO (Map GroundAtom Int)
forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Int)
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,Int
_) <- Set (Var, Int) -> [(Var, Int)]
forall a. Set a -> [a]
Set.toList Set (Var, Int)
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, Int
b) <- Map GroundAtom Int -> [(GroundAtom, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Int
m, Var
p Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
p', Model
bmodel Model -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
b]
            (Var, Set EntityTuple) -> [(Var, Set EntityTuple)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
p, Set EntityTuple
tbl)
      let funs :: Map Var (Map EntityTuple Int)
funs = [(Var, Map EntityTuple Int)] -> Map Var (Map EntityTuple Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Var, Map EntityTuple Int)] -> Map Var (Map EntityTuple Int))
-> [(Var, Map EntityTuple Int)] -> Map Var (Map EntityTuple Int)
forall a b. (a -> b) -> a -> b
$ do
            (Var
f,Int
_) <- Set (Var, Int) -> [(Var, Int)]
forall a. Set a -> [a]
Set.toList Set (Var, Int)
fs
            let tbl :: Map EntityTuple Int
tbl = [(EntityTuple, Int)] -> Map EntityTuple Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(EntityTuple
xs, Int
y) | (SEq (STmApp Var
f' EntityTuple
xs) Int
y, Int
b) <- Map GroundAtom Int -> [(GroundAtom, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Int
m, Var
f Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
f', Model
bmodel Model -> Int -> Bool
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
b]
            (Var, Map EntityTuple Int) -> [(Var, Map EntityTuple Int)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
f, Map EntityTuple Int
tbl)

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

      Maybe Model -> IO (Maybe Model)
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 (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 <- Int -> [Clause] -> IO (Maybe Model)
findModel Int
3 [Clause
c1, Clause
c2]
  case Maybe Model
ret of
    Maybe Model
Nothing -> String -> IO ()
putStrLn String
"=== NO MODEL FOUND ==="
    Just Model
m -> do
      String -> IO ()
putStrLn String
"=== A MODEL FOUND ==="
      (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ Model -> [String]
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 -> Int -> IO Var
skolem Var
name Int
_ = 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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
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 (m :: * -> *) a. Monad m => a -> m a
return Var
fsym
  [Clause]
cs <- (Var -> Int -> IO Var) -> Formula -> IO [Clause]
forall (m :: * -> *).
Monad m =>
(Var -> Int -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Int -> IO Var
skolem Formula
phi

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

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