{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
module ToySolver.EUF.FiniteModelFinder
(
Var
, FSym
, PSym
, GenLit (..)
, Term (..)
, Atom (..)
, Lit
, Clause
, Formula
, GenFormula (..)
, toSkolemNF
, Model (..)
, Entity
, EntityTuple
, showModel
, showEntity
, evalFormula
, evalAtom
, evalTerm
, evalLit
, evalClause
, evalClauses
, evalClausesU
, 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
type Var = InternedText
type FSym = InternedText
type PSym = InternedText
class Vars a where
vars :: a -> Set Var
instance Vars a => Vars [a] where
vars :: [a] -> Set Var
vars = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Vars a => a -> Set Var
vars
data GenLit a
= Pos a
| Neg a
deriving (Entity -> GenLit a -> [Char] -> [Char]
forall a. Show a => Entity -> GenLit a -> [Char] -> [Char]
forall a. Show a => [GenLit a] -> [Char] -> [Char]
forall a. Show a => GenLit a -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [GenLit a] -> [Char] -> [Char]
$cshowList :: forall a. Show a => [GenLit a] -> [Char] -> [Char]
show :: GenLit a -> [Char]
$cshow :: forall a. Show a => GenLit a -> [Char]
showsPrec :: Entity -> GenLit a -> [Char] -> [Char]
$cshowsPrec :: forall a. Show a => Entity -> GenLit a -> [Char] -> [Char]
Show, GenLit a -> GenLit a -> Bool
forall a. Eq a => GenLit a -> GenLit a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenLit a -> GenLit a -> Bool
$c/= :: forall a. Eq a => GenLit a -> GenLit a -> Bool
== :: GenLit a -> GenLit a -> Bool
$c== :: forall a. Eq a => GenLit a -> GenLit a -> Bool
Eq, GenLit a -> GenLit a -> Bool
GenLit a -> GenLit a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (GenLit a)
forall a. Ord a => GenLit a -> GenLit a -> Bool
forall a. Ord a => GenLit a -> GenLit a -> Ordering
forall a. Ord a => GenLit a -> GenLit a -> GenLit a
min :: GenLit a -> GenLit a -> GenLit a
$cmin :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
max :: GenLit a -> GenLit a -> GenLit a
$cmax :: forall a. Ord a => GenLit a -> GenLit a -> GenLit a
>= :: GenLit a -> GenLit a -> Bool
$c>= :: forall a. Ord a => GenLit a -> GenLit a -> Bool
> :: GenLit a -> GenLit a -> Bool
$c> :: forall a. Ord a => GenLit a -> GenLit a -> Bool
<= :: GenLit a -> GenLit a -> Bool
$c<= :: forall a. Ord a => GenLit a -> GenLit a -> Bool
< :: GenLit a -> GenLit a -> Bool
$c< :: forall a. Ord a => GenLit a -> GenLit a -> Bool
compare :: GenLit a -> GenLit a -> Ordering
$ccompare :: forall a. Ord a => GenLit a -> GenLit a -> Ordering
Ord)
instance Complement (GenLit a) where
notB :: GenLit a -> GenLit a
notB (Pos a
a) = forall a. a -> GenLit a
Neg a
a
notB (Neg a
a) = forall a. a -> GenLit a
Pos a
a
instance Vars a => Vars (GenLit a) where
vars :: GenLit a -> Set Var
vars (Pos a
a) = forall a. Vars a => a -> Set Var
vars a
a
vars (Neg a
a) = forall a. Vars a => a -> Set Var
vars a
a
data Term
= TmApp FSym [Term]
| TmVar Var
deriving (Entity -> Term -> [Char] -> [Char]
[Term] -> [Char] -> [Char]
Term -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [Term] -> [Char] -> [Char]
$cshowList :: [Term] -> [Char] -> [Char]
show :: Term -> [Char]
$cshow :: Term -> [Char]
showsPrec :: Entity -> Term -> [Char] -> [Char]
$cshowsPrec :: Entity -> Term -> [Char] -> [Char]
Show, Term -> Term -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
Ord)
data Atom = PApp PSym [Term]
deriving (Entity -> Atom -> [Char] -> [Char]
[Atom] -> [Char] -> [Char]
Atom -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [Atom] -> [Char] -> [Char]
$cshowList :: [Atom] -> [Char] -> [Char]
show :: Atom -> [Char]
$cshow :: Atom -> [Char]
showsPrec :: Entity -> Atom -> [Char] -> [Char]
$cshowsPrec :: Entity -> Atom -> [Char] -> [Char]
Show, Atom -> Atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c== :: Atom -> Atom -> Bool
Eq, Eq Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmax :: Atom -> Atom -> Atom
>= :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c< :: Atom -> Atom -> Bool
compare :: Atom -> Atom -> Ordering
$ccompare :: Atom -> Atom -> Ordering
Ord)
type Lit = GenLit Atom
type Clause = [Lit]
instance Vars Term where
vars :: Term -> Set Var
vars (TmVar Var
v) = forall a. a -> Set a
Set.singleton Var
v
vars (TmApp Var
_ [Term]
ts) = forall a. Vars a => a -> Set Var
vars [Term]
ts
instance Vars Atom where
vars :: Atom -> Set Var
vars (PApp Var
_ [Term]
ts) = forall a. Vars a => a -> Set Var
vars [Term]
ts
type Formula = GenFormula Atom
data GenFormula a
= T
| F
| Atom a
| And (GenFormula a) (GenFormula a)
| Or (GenFormula a) (GenFormula a)
| Not (GenFormula a)
| Imply (GenFormula a) (GenFormula a)
| Equiv (GenFormula a) (GenFormula a)
| Forall Var (GenFormula a)
| Exists Var (GenFormula a)
deriving (Entity -> GenFormula a -> [Char] -> [Char]
forall a. Show a => Entity -> GenFormula a -> [Char] -> [Char]
forall a. Show a => [GenFormula a] -> [Char] -> [Char]
forall a. Show a => GenFormula a -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [GenFormula a] -> [Char] -> [Char]
$cshowList :: forall a. Show a => [GenFormula a] -> [Char] -> [Char]
show :: GenFormula a -> [Char]
$cshow :: forall a. Show a => GenFormula a -> [Char]
showsPrec :: Entity -> GenFormula a -> [Char] -> [Char]
$cshowsPrec :: forall a. Show a => Entity -> GenFormula a -> [Char] -> [Char]
Show, GenFormula a -> GenFormula a -> Bool
forall a. Eq a => GenFormula a -> GenFormula a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GenFormula a -> GenFormula a -> Bool
$c/= :: forall a. Eq a => GenFormula a -> GenFormula a -> Bool
== :: GenFormula a -> GenFormula a -> Bool
$c== :: forall a. Eq a => GenFormula a -> GenFormula a -> Bool
Eq, GenFormula a -> GenFormula a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (GenFormula a)
forall a. Ord a => GenFormula a -> GenFormula a -> Bool
forall a. Ord a => GenFormula a -> GenFormula a -> Ordering
forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
min :: GenFormula a -> GenFormula a -> GenFormula a
$cmin :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
max :: GenFormula a -> GenFormula a -> GenFormula a
$cmax :: forall a. Ord a => GenFormula a -> GenFormula a -> GenFormula a
>= :: GenFormula a -> GenFormula a -> Bool
$c>= :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
> :: GenFormula a -> GenFormula a -> Bool
$c> :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
<= :: GenFormula a -> GenFormula a -> Bool
$c<= :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
< :: GenFormula a -> GenFormula a -> Bool
$c< :: forall a. Ord a => GenFormula a -> GenFormula a -> Bool
compare :: GenFormula a -> GenFormula a -> Ordering
$ccompare :: forall a. Ord a => GenFormula a -> GenFormula a -> Ordering
Ord)
instance MonotoneBoolean (GenFormula a) where
true :: GenFormula a
true = forall a. GenFormula a
T
false :: GenFormula a
false = forall a. GenFormula a
F
.&&. :: GenFormula a -> GenFormula a -> GenFormula a
(.&&.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
And
.||. :: GenFormula a -> GenFormula a -> GenFormula a
(.||.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Or
instance Complement (GenFormula a) where
notB :: GenFormula a -> GenFormula a
notB = forall a. GenFormula a -> GenFormula a
Not
instance IfThenElse (GenFormula a) (GenFormula a) where
ite :: GenFormula a -> GenFormula a -> GenFormula a -> GenFormula a
ite = forall a. Boolean a => a -> a -> a -> a
iteBoolean
instance Boolean (GenFormula a) where
.=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.=>.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Imply
.<=>. :: GenFormula a -> GenFormula a -> GenFormula a
(.<=>.) = forall a. GenFormula a -> GenFormula a -> GenFormula a
Equiv
instance Vars a => Vars (GenFormula a) where
vars :: GenFormula a -> Set Var
vars GenFormula a
T = forall a. Set a
Set.empty
vars GenFormula a
F = forall a. Set a
Set.empty
vars (Atom a
a) = forall a. Vars a => a -> Set Var
vars a
a
vars (And GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
vars (Or GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
vars (Not GenFormula a
phi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi
vars (Imply GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
vars (Equiv GenFormula a
phi GenFormula a
psi) = forall a. Vars a => a -> Set Var
vars GenFormula a
phi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Vars a => a -> Set Var
vars GenFormula a
psi
vars (Forall Var
v GenFormula a
phi) = forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (forall a. Vars a => a -> Set Var
vars GenFormula a
phi)
vars (Exists Var
v GenFormula a
phi) = forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v (forall a. Vars a => a -> Set Var
vars GenFormula a
phi)
toNNF :: Formula -> Formula
toNNF :: Formula -> Formula
toNNF = Formula -> Formula
f
where
f :: Formula -> Formula
f (And Formula
phi Formula
psi) = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
f Formula
psi
f (Or Formula
phi Formula
psi) = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
f Formula
psi
f (Not Formula
phi) = Formula -> Formula
g Formula
phi
f (Imply Formula
phi Formula
psi) = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
f Formula
psi
f (Equiv Formula
phi Formula
psi) = Formula -> Formula
f ((Formula
phi forall a. Boolean a => a -> a -> a
.=>. Formula
psi) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
psi forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
f (Forall Var
v Formula
phi) = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
f Formula
phi)
f (Exists Var
v Formula
phi) = forall a. Var -> GenFormula a -> GenFormula a
Exists Var
v (Formula -> Formula
f Formula
phi)
f Formula
phi = Formula
phi
g :: Formula -> Formula
g :: Formula -> Formula
g Formula
T = forall a. GenFormula a
F
g Formula
F = forall a. GenFormula a
T
g (And Formula
phi Formula
psi) = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.||. Formula -> Formula
g Formula
psi
g (Or Formula
phi Formula
psi) = Formula -> Formula
g Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
g Formula
psi
g (Not Formula
phi) = Formula -> Formula
f Formula
phi
g (Imply Formula
phi Formula
psi) = Formula -> Formula
f Formula
phi forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
g Formula
psi
g (Equiv Formula
phi Formula
psi) = Formula -> Formula
g ((Formula
phi forall a. Boolean a => a -> a -> a
.=>. Formula
psi) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Formula
psi forall a. Boolean a => a -> a -> a
.=>. Formula
phi))
g (Forall Var
v Formula
phi) = forall a. Var -> GenFormula a -> GenFormula a
Exists Var
v (Formula -> Formula
g Formula
phi)
g (Exists Var
v Formula
phi) = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
v (Formula -> Formula
g Formula
phi)
g (Atom Atom
a) = forall a. Complement a => a -> a
notB (forall a. a -> GenFormula a
Atom Atom
a)
toSkolemNF :: forall m. Monad m => (Var -> Int -> m FSym) -> Formula -> m [Clause]
toSkolemNF :: forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> m Var
skolem Formula
phi = [Var] -> Map Var Term -> Formula -> m [Clause]
f [] forall k a. Map k a
Map.empty (Formula -> Formula
toNNF Formula
phi)
where
f :: [Var] -> Map Var Term -> Formula -> m [Clause]
f :: [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
_ Map Var Term
_ Formula
T = forall (m :: * -> *) a. Monad m => a -> m a
return []
f [Var]
_ Map Var Term
_ Formula
F = forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
f [Var]
_ Map Var Term
s (Atom Atom
a) = forall (m :: * -> *) a. Monad m => a -> m a
return [[forall a. a -> GenLit a
Pos (Map Var Term -> Atom -> Atom
substAtom Map Var Term
s Atom
a)]]
f [Var]
_ Map Var Term
s (Not (Atom Atom
a)) = forall (m :: * -> *) a. Monad m => a -> m a
return [[forall a. a -> GenLit a
Neg (Map Var Term -> Atom -> Atom
substAtom Map Var Term
s Atom
a)]]
f [Var]
uvs Map Var Term
s (And Formula
phi Formula
psi) = do
[Clause]
phi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
phi
[Clause]
psi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
psi
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Clause]
phi' forall a. [a] -> [a] -> [a]
++ [Clause]
psi'
f [Var]
uvs Map Var Term
s (Or Formula
phi Formula
psi) = do
[Clause]
phi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
phi
[Clause]
psi' <- [Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs Map Var Term
s Formula
psi
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Clause
c1forall a. [a] -> [a] -> [a]
++Clause
c2 | Clause
c1 <- [Clause]
phi', Clause
c2 <- [Clause]
psi']
f [Var]
uvs Map Var Term
s psi :: Formula
psi@(Forall Var
v Formula
phi) = do
let v' :: Var
v' = Text -> Set Var -> Var
gensym (forall t. Uninternable t => t -> Uninterned t
unintern Var
v) (forall a. Vars a => a -> Set Var
vars Formula
psi forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList [Var]
uvs)
[Var] -> Map Var Term -> Formula -> m [Clause]
f (Var
v' forall a. a -> [a] -> [a]
: [Var]
uvs) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v (Var -> Term
TmVar Var
v') Map Var Term
s) Formula
phi
f [Var]
uvs Map Var Term
s (Exists Var
v Formula
phi) = do
Var
fsym <- Var -> Entity -> m Var
skolem Var
v (forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Var]
uvs)
[Var] -> Map Var Term -> Formula -> m [Clause]
f [Var]
uvs (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v (Var -> [Term] -> Term
TmApp Var
fsym [Var -> Term
TmVar Var
v | Var
v <- forall a. [a] -> [a]
reverse [Var]
uvs]) Map Var Term
s) Formula
phi
f [Var]
_ Map Var Term
_ Formula
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"ToySolver.EUF.FiniteModelFinder.toSkolemNF: should not happen"
gensym :: Text -> Set Var -> Var
gensym :: Text -> Set Var -> Var
gensym Text
template Set Var
vs = forall a. [a] -> a
head [Var
name | Var
name <- [Var]
names, forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
name Set Var
vs]
where
names :: [Var]
names = forall a b. (a -> b) -> [a] -> [b]
map forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ Text
template forall a. a -> [a] -> [a]
: [Text
template forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n) | Integer
n <-[Integer
1..]]
substAtom :: Map Var Term -> Atom -> Atom
substAtom :: Map Var Term -> Atom -> Atom
substAtom Map Var Term
s (PApp Var
p [Term]
ts) = Var -> [Term] -> Atom
PApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map (Map Var Term -> Term -> Term
substTerm Map Var Term
s) [Term]
ts)
substTerm :: Map Var Term -> Term -> Term
substTerm :: Map Var Term -> Term -> Term
substTerm Map Var Term
s (TmVar Var
v) = forall a. a -> Maybe a -> a
fromMaybe (Var -> Term
TmVar Var
v) (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v Map Var Term
s)
substTerm Map Var Term
s (TmApp Var
f [Term]
ts) = Var -> [Term] -> Term
TmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map (Map Var Term -> Term -> Term
substTerm Map Var Term
s) [Term]
ts)
test_toSkolemNF :: IO ()
test_toSkolemNF = do
IORef Integer
ref <- forall a. a -> IO (IORef a)
newIORef Integer
0
let skolem :: Var -> Int -> IO FSym
skolem :: Var -> Entity -> IO Var
skolem Var
name Entity
_ = do
Integer
n <- forall a. IORef a -> IO a
readIORef IORef Integer
ref
let fsym :: Var
fsym = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ forall t. Uninternable t => t -> Uninterned t
unintern Var
name forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n)
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nforall a. Num a => a -> a -> a
+Integer
1)
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym
let phi :: Formula
phi = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
"x" forall a b. (a -> b) -> a -> b
$
forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"animal" [Var -> Term
TmVar Var
"x"]) forall a. Boolean a => a -> a -> a
.=>.
(forall a. Var -> GenFormula a -> GenFormula a
Exists Var
"y" forall a b. (a -> b) -> a -> b
$
forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"heart" [Var -> Term
TmVar Var
"y"]) forall a. MonotoneBoolean a => a -> a -> a
.&&.
forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"has" [Var -> Term
TmVar Var
"x", Var -> Term
TmVar Var
"y"]))
[Clause]
phi' <- forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> IO Var
skolem Formula
phi
forall a. Show a => a -> IO ()
print [Clause]
phi'
data SGenTerm v
= STmApp FSym [v]
| STmVar v
deriving (Entity -> SGenTerm v -> [Char] -> [Char]
forall v. Show v => Entity -> SGenTerm v -> [Char] -> [Char]
forall v. Show v => [SGenTerm v] -> [Char] -> [Char]
forall v. Show v => SGenTerm v -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [SGenTerm v] -> [Char] -> [Char]
$cshowList :: forall v. Show v => [SGenTerm v] -> [Char] -> [Char]
show :: SGenTerm v -> [Char]
$cshow :: forall v. Show v => SGenTerm v -> [Char]
showsPrec :: Entity -> SGenTerm v -> [Char] -> [Char]
$cshowsPrec :: forall v. Show v => Entity -> SGenTerm v -> [Char] -> [Char]
Show, SGenTerm v -> SGenTerm v -> Bool
forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SGenTerm v -> SGenTerm v -> Bool
$c/= :: forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
== :: SGenTerm v -> SGenTerm v -> Bool
$c== :: forall v. Eq v => SGenTerm v -> SGenTerm v -> Bool
Eq, SGenTerm v -> SGenTerm v -> Bool
SGenTerm v -> SGenTerm v -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {v}. Ord v => Eq (SGenTerm v)
forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
forall v. Ord v => SGenTerm v -> SGenTerm v -> Ordering
forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
min :: SGenTerm v -> SGenTerm v -> SGenTerm v
$cmin :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
max :: SGenTerm v -> SGenTerm v -> SGenTerm v
$cmax :: forall v. Ord v => SGenTerm v -> SGenTerm v -> SGenTerm v
>= :: SGenTerm v -> SGenTerm v -> Bool
$c>= :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
> :: SGenTerm v -> SGenTerm v -> Bool
$c> :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
<= :: SGenTerm v -> SGenTerm v -> Bool
$c<= :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
< :: SGenTerm v -> SGenTerm v -> Bool
$c< :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Bool
compare :: SGenTerm v -> SGenTerm v -> Ordering
$ccompare :: forall v. Ord v => SGenTerm v -> SGenTerm v -> Ordering
Ord)
data SGenAtom v
= SPApp PSym [v]
| SEq (SGenTerm v) v
deriving (Entity -> SGenAtom v -> [Char] -> [Char]
forall v. Show v => Entity -> SGenAtom v -> [Char] -> [Char]
forall v. Show v => [SGenAtom v] -> [Char] -> [Char]
forall v. Show v => SGenAtom v -> [Char]
forall a.
(Entity -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [SGenAtom v] -> [Char] -> [Char]
$cshowList :: forall v. Show v => [SGenAtom v] -> [Char] -> [Char]
show :: SGenAtom v -> [Char]
$cshow :: forall v. Show v => SGenAtom v -> [Char]
showsPrec :: Entity -> SGenAtom v -> [Char] -> [Char]
$cshowsPrec :: forall v. Show v => Entity -> SGenAtom v -> [Char] -> [Char]
Show, SGenAtom v -> SGenAtom v -> Bool
forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SGenAtom v -> SGenAtom v -> Bool
$c/= :: forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
== :: SGenAtom v -> SGenAtom v -> Bool
$c== :: forall v. Eq v => SGenAtom v -> SGenAtom v -> Bool
Eq, SGenAtom v -> SGenAtom v -> Bool
SGenAtom v -> SGenAtom v -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {v}. Ord v => Eq (SGenAtom v)
forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
forall v. Ord v => SGenAtom v -> SGenAtom v -> Ordering
forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
min :: SGenAtom v -> SGenAtom v -> SGenAtom v
$cmin :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
max :: SGenAtom v -> SGenAtom v -> SGenAtom v
$cmax :: forall v. Ord v => SGenAtom v -> SGenAtom v -> SGenAtom v
>= :: SGenAtom v -> SGenAtom v -> Bool
$c>= :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
> :: SGenAtom v -> SGenAtom v -> Bool
$c> :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
<= :: SGenAtom v -> SGenAtom v -> Bool
$c<= :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
< :: SGenAtom v -> SGenAtom v -> Bool
$c< :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Bool
compare :: SGenAtom v -> SGenAtom v -> Ordering
$ccompare :: forall v. Ord v => SGenAtom v -> SGenAtom v -> Ordering
Ord)
type STerm = SGenTerm Var
type SAtom = SGenAtom Var
type SLit = GenLit SAtom
type SClause = [SLit]
instance Vars STerm where
vars :: STerm -> Set Var
vars (STmApp Var
_ [Var]
xs) = forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
vars (STmVar Var
v) = forall a. a -> Set a
Set.singleton Var
v
instance Vars SAtom where
vars :: SAtom -> Set Var
vars (SPApp Var
_ [Var]
xs) = forall a. Ord a => [a] -> Set a
Set.fromList [Var]
xs
vars (SEq STerm
t Var
v) = forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v (forall a. Vars a => a -> Set Var
vars STerm
t)
type M = State (Set Var, Int, Map (FSym, [Var]) Var, [SLit])
flatten :: Clause -> Maybe SClause
flatten :: Clause -> Maybe [SLit]
flatten Clause
c =
case forall s a. State s a -> s -> (a, s)
runState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GenLit Atom -> M SLit
flattenLit Clause
c) (forall a. Vars a => a -> Set Var
vars Clause
c, Entity
0, forall k a. Map k a
Map.empty, []) of
([SLit]
c, (Set Var
_,Entity
_,Map (Var, [Var]) Var
_,[SLit]
ls)) -> [SLit] -> Maybe [SLit]
removeTautology forall a b. (a -> b) -> a -> b
$ [SLit] -> [SLit]
removeNegEq forall a b. (a -> b) -> a -> b
$ [SLit]
ls forall a. [a] -> [a] -> [a]
++ [SLit]
c
where
gensym :: M Var
gensym :: M Var
gensym = do
(Set Var
vs, Entity
n, Map (Var, [Var]) Var
defs, [SLit]
ls) <- forall s (m :: * -> *). MonadState s m => m s
get
let go :: Int -> M Var
go :: Entity -> M Var
go Entity
m = do
let v :: Var
v = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Entity
m)
if Var
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Var
vs
then Entity -> M Var
go (Entity
mforall a. Num a => a -> a -> a
+Entity
1)
else do
forall s (m :: * -> *). MonadState s m => s -> m ()
put (forall a. Ord a => a -> Set a -> Set a
Set.insert Var
v Set Var
vs, Entity
mforall a. Num a => a -> a -> a
+Entity
1, Map (Var, [Var]) Var
defs, [SLit]
ls)
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
Entity -> M Var
go Entity
n
flattenLit :: Lit -> M SLit
flattenLit :: GenLit Atom -> M SLit
flattenLit (Pos Atom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Atom -> M SAtom
flattenAtom Atom
a
flattenLit (Neg Atom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Atom -> M SAtom
flattenAtom Atom
a
flattenAtom :: Atom -> M SAtom
flattenAtom :: Atom -> M SAtom
flattenAtom (PApp Var
"=" [TmVar Var
x, TmVar Var
y]) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. v -> SGenTerm v
STmVar Var
x) Var
y
flattenAtom (PApp Var
"=" [TmVar Var
x, TmApp Var
f [Term]
ts]) = do
[Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
flattenAtom (PApp Var
"=" [TmApp Var
f [Term]
ts, TmVar Var
x]) = do
[Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
flattenAtom (PApp Var
"=" [TmApp Var
f [Term]
ts, Term
t2]) = do
[Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
Var
x <- Term -> M Var
flattenTerm Term
t2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x
flattenAtom (PApp Var
p [Term]
ts) = do
[Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall v. Var -> [v] -> SGenAtom v
SPApp Var
p [Var]
xs
flattenTerm :: Term -> M Var
flattenTerm :: Term -> M Var
flattenTerm (TmVar Var
x) = forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
flattenTerm (TmApp Var
f [Term]
ts) = do
[Var]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> M Var
flattenTerm [Term]
ts
(Set Var
_, Entity
_, Map (Var, [Var]) Var
defs, [SLit]
_) <- forall s (m :: * -> *). MonadState s m => m s
get
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var
f, [Var]
xs) Map (Var, [Var]) Var
defs of
Just Var
x -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
Maybe Var
Nothing -> do
Var
x <- M Var
gensym
(Set Var
vs, Entity
n, Map (Var, [Var]) Var
defs, [SLit]
ls) <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Var
vs, Entity
n, forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Var
f, [Var]
xs) Var
x Map (Var, [Var]) Var
defs, forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f [Var]
xs) Var
x) forall a. a -> [a] -> [a]
: [SLit]
ls)
forall (m :: * -> *) a. Monad m => a -> m a
return Var
x
removeNegEq :: SClause -> SClause
removeNegEq :: [SLit] -> [SLit]
removeNegEq = [SLit] -> [SLit] -> [SLit]
go []
where
go :: [SLit] -> [SLit] -> [SLit]
go [SLit]
r [] = [SLit]
r
go [SLit]
r (Neg (SEq (STmVar Var
x) Var
y) : [SLit]
ls) = [SLit] -> [SLit] -> [SLit]
go (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) [SLit]
r) (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> SLit -> SLit
substLit Var
x Var
y) [SLit]
ls)
go [SLit]
r (SLit
l : [SLit]
ls) = [SLit] -> [SLit] -> [SLit]
go (SLit
l forall a. a -> [a] -> [a]
: [SLit]
r) [SLit]
ls
substLit :: Var -> Var -> SLit -> SLit
substLit :: Var -> Var -> SLit -> SLit
substLit Var
x Var
y (Pos SAtom
a) = forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y SAtom
a
substLit Var
x Var
y (Neg SAtom
a) = forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y SAtom
a
substAtom :: Var -> Var -> SAtom -> SAtom
substAtom :: Var -> Var -> SAtom -> SAtom
substAtom Var
x Var
y (SPApp Var
p [Var]
xs) = forall v. Var -> [v] -> SGenAtom v
SPApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> Var -> Var
substVar Var
x Var
y) [Var]
xs)
substAtom Var
x Var
y (SEq STerm
t Var
v) = forall v. SGenTerm v -> v -> SGenAtom v
SEq (Var -> Var -> STerm -> STerm
substTerm Var
x Var
y STerm
t) (Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v)
substTerm :: Var -> Var -> STerm -> STerm
substTerm :: Var -> Var -> STerm -> STerm
substTerm Var
x Var
y (STmApp Var
f [Var]
xs) = forall v. Var -> [v] -> SGenTerm v
STmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map (Var -> Var -> Var -> Var
substVar Var
x Var
y) [Var]
xs)
substTerm Var
x Var
y (STmVar Var
v) = forall v. v -> SGenTerm v
STmVar (Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v)
substVar :: Var -> Var -> Var -> Var
substVar :: Var -> Var -> Var -> Var
substVar Var
x Var
y Var
v
| Var
vforall a. Eq a => a -> a -> Bool
==Var
x = Var
y
| Bool
otherwise = Var
v
removeTautology :: SClause -> Maybe SClause
removeTautology :: [SLit] -> Maybe [SLit]
removeTautology [SLit]
lits
| forall a. Set a -> Bool
Set.null (Set SAtom
pos forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set SAtom
neg) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [forall a. a -> GenLit a
Neg SAtom
l | SAtom
l <- forall a. Set a -> [a]
Set.toList Set SAtom
neg] forall a. [a] -> [a] -> [a]
++ [forall a. a -> GenLit a
Pos SAtom
l | SAtom
l <- forall a. Set a -> [a]
Set.toList Set SAtom
pos]
| Bool
otherwise = forall a. Maybe a
Nothing
where
pos :: Set SAtom
pos = forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Pos SAtom
l <- [SLit]
lits]
neg :: Set SAtom
neg = forall a. Ord a => [a] -> Set a
Set.fromList [SAtom
l | Neg SAtom
l <- [SLit]
lits]
test_flatten :: Maybe [SLit]
test_flatten = Clause -> Maybe [SLit]
flatten [forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"P" [Var -> [Term] -> Term
TmApp Var
"a" [], Var -> [Term] -> Term
TmApp Var
"f" [Var -> Term
TmVar Var
"x"]]]
type Entity = Int
type EntityTuple = [Entity]
showEntity :: Entity -> String
showEntity :: Entity -> [Char]
showEntity Entity
e = [Char]
"$" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Entity
e
showEntityTuple :: EntityTuple -> String
showEntityTuple :: EntityTuple -> [Char]
showEntityTuple EntityTuple
xs = forall r. PrintfType r => [Char] -> r
printf [Char]
"(%s)" forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Entity -> [Char]
showEntity EntityTuple
xs
type GroundTerm = SGenTerm Entity
type GroundAtom = SGenAtom Entity
type GroundLit = GenLit GroundAtom
type GroundClause = [GroundLit]
type Subst = Map Var Entity
enumSubst :: Set Var -> [Entity] -> [Subst]
enumSubst :: Set Var -> EntityTuple -> [Subst]
enumSubst Set Var
vs EntityTuple
univ = do
[(Var, Entity)]
ps <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(Var
v,Entity
e) | Entity
e <- EntityTuple
univ] | Var
v <- forall a. Set a -> [a]
Set.toList Set Var
vs]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Var, Entity)]
ps
applySubst :: Subst -> SClause -> GroundClause
applySubst :: Subst -> [SLit] -> GroundClause
applySubst Subst
s = forall a b. (a -> b) -> [a] -> [b]
map SLit -> GroundLit
substLit
where
substLit :: SLit -> GroundLit
substLit :: SLit -> GroundLit
substLit (Pos SAtom
a) = forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a
substLit (Neg SAtom
a) = forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ SAtom -> GroundAtom
substAtom SAtom
a
substAtom :: SAtom -> GroundAtom
substAtom :: SAtom -> GroundAtom
substAtom (SPApp Var
p [Var]
xs) = forall v. Var -> [v] -> SGenAtom v
SPApp Var
p (forall a b. (a -> b) -> [a] -> [b]
map Var -> Entity
substVar [Var]
xs)
substAtom (SEq STerm
t Var
v) = forall v. SGenTerm v -> v -> SGenAtom v
SEq (STerm -> GroundTerm
substTerm STerm
t) (Var -> Entity
substVar Var
v)
substTerm :: STerm -> GroundTerm
substTerm :: STerm -> GroundTerm
substTerm (STmApp Var
f [Var]
xs) = forall v. Var -> [v] -> SGenTerm v
STmApp Var
f (forall a b. (a -> b) -> [a] -> [b]
map Var -> Entity
substVar [Var]
xs)
substTerm (STmVar Var
v) = forall v. v -> SGenTerm v
STmVar (Var -> Entity
substVar Var
v)
substVar :: Var -> Entity
substVar :: Var -> Entity
substVar = (Subst
s forall k a. Ord k => Map k a -> k -> a
Map.!)
simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GroundLit -> Maybe GroundClause
f
where
f :: GroundLit -> Maybe [GroundLit]
f :: GroundLit -> Maybe GroundClause
f (Pos (SEq (STmVar Entity
x) Entity
y)) = if Entity
xforall a. Eq a => a -> a -> Bool
==Entity
y then forall a. Maybe a
Nothing else forall (m :: * -> *) a. Monad m => a -> m a
return []
f GroundLit
lit = forall (m :: * -> *) a. Monad m => a -> m a
return [GroundLit
lit]
collectFSym :: Clause -> Set (FSym, Int)
collectFSym :: Clause -> Set (Var, Entity)
collectFSym = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map GenLit Atom -> Set (Var, Entity)
f
where
f :: Lit -> Set (FSym, Int)
f :: GenLit Atom -> Set (Var, Entity)
f (Pos Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
f (Neg Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
g :: Atom -> Set (FSym, Int)
g :: Atom -> Set (Var, Entity)
g (PApp Var
_ [Term]
xs) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Term -> Set (Var, Entity)
h [Term]
xs
h :: Term -> Set (FSym, Int)
h :: Term -> Set (Var, Entity)
h (TmVar Var
_) = forall a. Set a
Set.empty
h (TmApp Var
f [Term]
xs) = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton (Var
f, forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Term]
xs) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Term -> Set (Var, Entity)
h [Term]
xs
collectPSym :: Clause -> Set (PSym, Int)
collectPSym :: Clause -> Set (Var, Entity)
collectPSym = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map GenLit Atom -> Set (Var, Entity)
f
where
f :: Lit -> Set (PSym, Int)
f :: GenLit Atom -> Set (Var, Entity)
f (Pos Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
f (Neg Atom
a) = Atom -> Set (Var, Entity)
g Atom
a
g :: Atom -> Set (PSym, Int)
g :: Atom -> Set (Var, Entity)
g (PApp Var
"=" [Term
_,Term
_]) = forall a. Set a
Set.empty
g (PApp Var
p [Term]
xs) = forall a. a -> Set a
Set.singleton (Var
p, forall (t :: * -> *) a. Foldable t => t a -> Entity
length [Term]
xs)
data Model
= Model
{ Model -> EntityTuple
mUniverse :: [Entity]
, Model -> Map Var (Set EntityTuple)
mRelations :: Map PSym (Set EntityTuple)
, Model -> Map Var (Map EntityTuple Entity)
mFunctions :: Map FSym (Map EntityTuple Entity)
}
showModel :: Model -> [String]
showModel :: Model -> [[Char]]
showModel Model
m =
forall r. PrintfType r => [Char] -> r
printf [Char]
"DOMAIN = {%s}" (forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (forall a b. (a -> b) -> [a] -> [b]
map Entity -> [Char]
showEntity (Model -> EntityTuple
mUniverse Model
m))) forall a. a -> [a] -> [a]
:
[ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s = { %s }" (Text -> [Char]
Text.unpack (forall t. Uninternable t => t -> Uninterned t
unintern Var
p)) [Char]
s
| (Var
p, Set EntityTuple
xss) <- forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Set EntityTuple)
mRelations Model
m)
, let s :: [Char]
s = forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [if forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs forall a. Eq a => a -> a -> Bool
== Entity
1 then Entity -> [Char]
showEntity (forall a. [a] -> a
head EntityTuple
xs) else EntityTuple -> [Char]
showEntityTuple EntityTuple
xs | EntityTuple
xs <- forall a. Set a -> [a]
Set.toList Set EntityTuple
xss]
] forall a. [a] -> [a] -> [a]
++
[ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s%s = %s" (Text -> [Char]
Text.unpack (forall t. Uninternable t => t -> Uninterned t
unintern Var
f)) (if forall (t :: * -> *) a. Foldable t => t a -> Entity
length EntityTuple
xs forall a. Eq a => a -> a -> Bool
== Entity
0 then [Char]
"" else EntityTuple -> [Char]
showEntityTuple EntityTuple
xs) (Entity -> [Char]
showEntity Entity
y)
| (Var
f, Map EntityTuple Entity
xss) <- forall k a. Map k a -> [(k, a)]
Map.toList (Model -> Map Var (Map EntityTuple Entity)
mFunctions Model
m)
, (EntityTuple
xs, Entity
y) <- forall k a. Map k a -> [(k, a)]
Map.toList Map EntityTuple Entity
xss
]
evalFormula :: Model -> Formula -> Bool
evalFormula :: Model -> Formula -> Bool
evalFormula Model
m = Subst -> Formula -> Bool
f forall k a. Map k a
Map.empty
where
f :: Map Var Entity -> Formula -> Bool
f :: Subst -> Formula -> Bool
f Subst
env Formula
T = Bool
True
f Subst
env Formula
F = Bool
False
f Subst
env (Atom Atom
a) = Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
a
f Subst
env (And Formula
phi1 Formula
phi2) = Subst -> Formula -> Bool
f Subst
env Formula
phi1 Bool -> Bool -> Bool
&& Subst -> Formula -> Bool
f Subst
env Formula
phi2
f Subst
env (Or Formula
phi1 Formula
phi2) = Subst -> Formula -> Bool
f Subst
env Formula
phi1 Bool -> Bool -> Bool
|| Subst -> Formula -> Bool
f Subst
env Formula
phi2
f Subst
env (Not Formula
phi) = Bool -> Bool
not (Subst -> Formula -> Bool
f Subst
env Formula
phi)
f Subst
env (Imply Formula
phi1 Formula
phi2) = Bool -> Bool
not (Subst -> Formula -> Bool
f Subst
env Formula
phi1) Bool -> Bool -> Bool
|| Subst -> Formula -> Bool
f Subst
env Formula
phi2
f Subst
env (Equiv Formula
phi1 Formula
phi2) = Subst -> Formula -> Bool
f Subst
env Formula
phi1 forall a. Eq a => a -> a -> Bool
== Subst -> Formula -> Bool
f Subst
env Formula
phi2
f Subst
env (Forall Var
v Formula
phi) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Entity
e -> Subst -> Formula -> Bool
f (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Entity
e Subst
env) Formula
phi) (Model -> EntityTuple
mUniverse Model
m)
f Subst
env (Exists Var
v Formula
phi) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Entity
e -> Subst -> Formula -> Bool
f (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Entity
e Subst
env) Formula
phi) (Model -> EntityTuple
mUniverse Model
m)
evalAtom :: Model -> Map Var Entity -> Atom -> Bool
evalAtom :: Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env (PApp Var
"=" [Term
x1,Term
x2]) = Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env Term
x1 forall a. Eq a => a -> a -> Bool
== Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env Term
x2
evalAtom Model
m Subst
env (PApp Var
p [Term]
xs) = forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env) [Term]
xs forall a. Ord a => a -> Set a -> Bool
`Set.member` (Model -> Map Var (Set EntityTuple)
mRelations Model
m forall k a. Ord k => Map k a -> k -> a
Map.! Var
p)
evalTerm :: Model -> Map Var Entity -> Term -> Entity
evalTerm :: Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env (TmVar Var
v) = Subst
env forall k a. Ord k => Map k a -> k -> a
Map.! Var
v
evalTerm Model
m Subst
env (TmApp Var
f [Term]
xs) = (Model -> Map Var (Map EntityTuple Entity)
mFunctions Model
m forall k a. Ord k => Map k a -> k -> a
Map.! Var
f) forall k a. Ord k => Map k a -> k -> a
Map.! forall a b. (a -> b) -> [a] -> [b]
map (Model -> Subst -> Term -> Entity
evalTerm Model
m Subst
env) [Term]
xs
evalLit :: Model -> Map Var Entity -> Lit -> Bool
evalLit :: Model -> Subst -> GenLit Atom -> Bool
evalLit Model
m Subst
env (Pos Atom
atom) = Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
atom
evalLit Model
m Subst
env (Neg Atom
atom) = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Model -> Subst -> Atom -> Bool
evalAtom Model
m Subst
env Atom
atom
evalClause :: Model -> Map Var Entity -> Clause -> Bool
evalClause :: Model -> Subst -> Clause -> Bool
evalClause Model
m Subst
env = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Model -> Subst -> GenLit Atom -> Bool
evalLit Model
m Subst
env)
evalClauses :: Model -> Map Var Entity -> [Clause] -> Bool
evalClauses :: Model -> Subst -> [Clause] -> Bool
evalClauses Model
m Subst
env = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Model -> Subst -> Clause -> Bool
evalClause Model
m Subst
env)
evalClausesU :: Model -> [Clause] -> Bool
evalClausesU :: Model -> [Clause] -> Bool
evalClausesU Model
m [Clause]
cs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Subst
env -> Model -> Subst -> [Clause] -> Bool
evalClauses Model
m Subst
env [Clause]
cs) (Set Var -> EntityTuple -> [Subst]
enumSubst (forall a. Vars a => a -> Set Var
vars [Clause]
cs) (Model -> EntityTuple
mUniverse Model
m))
findModel :: Int -> [Clause] -> IO (Maybe Model)
findModel :: Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
size [Clause]
cs = do
let univ :: EntityTuple
univ = [Entity
0..Entity
sizeforall a. Num a => a -> a -> a
-Entity
1]
let cs2 :: [[SLit]]
cs2 = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Clause -> Maybe [SLit]
flatten [Clause]
cs
fs :: Set (Var, Entity)
fs = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Clause -> Set (Var, Entity)
collectFSym [Clause]
cs
ps :: Set (Var, Entity)
ps = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Clause -> Set (Var, Entity)
collectPSym [Clause]
cs
Solver
solver <- IO Solver
SAT.newSolver
IORef (Map GroundAtom Entity)
ref <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
let translateAtom :: GroundAtom -> IO SAT.Var
translateAtom :: GroundAtom -> IO Entity
translateAtom (SEq (STmVar Entity
_) Entity
_) = forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen"
translateAtom GroundAtom
a = do
Map GroundAtom Entity
m <- forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Entity)
ref
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GroundAtom
a Map GroundAtom Entity
m of
Just Entity
b -> forall (m :: * -> *) a. Monad m => a -> m a
return Entity
b
Maybe Entity
Nothing -> do
Entity
b <- forall (m :: * -> *) a. NewVar m a => a -> m Entity
SAT.newVar Solver
solver
forall a. IORef a -> a -> IO ()
writeIORef IORef (Map GroundAtom Entity)
ref (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert GroundAtom
a Entity
b Map GroundAtom Entity
m)
forall (m :: * -> *) a. Monad m => a -> m a
return Entity
b
translateLit :: GroundLit -> IO SAT.Lit
translateLit :: GroundLit -> IO Entity
translateLit (Pos GroundAtom
a) = GroundAtom -> IO Entity
translateAtom GroundAtom
a
translateLit (Neg GroundAtom
a) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ GroundAtom -> IO Entity
translateAtom GroundAtom
a
translateClause :: GroundClause -> IO SAT.Clause
translateClause :: GroundClause -> IO EntityTuple
translateClause = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM GroundLit -> IO Entity
translateLit
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[SLit]]
cs2 forall a b. (a -> b) -> a -> b
$ \[SLit]
c -> do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Set Var -> EntityTuple -> [Subst]
enumSubst (forall a. Vars a => a -> Set Var
vars [SLit]
c) EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \Subst
s -> do
case GroundClause -> Maybe GroundClause
simplifyGroundClause (Subst -> [SLit] -> GroundClause
applySubst Subst
s [SLit]
c) of
Maybe GroundClause
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just GroundClause
c' -> forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GroundClause -> IO EntityTuple
translateClause GroundClause
c'
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs) forall a b. (a -> b) -> a -> b
$ \(Var
f, Entity
arity) -> do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (m :: * -> *) a. Applicative m => Entity -> m a -> m [a]
replicateM Entity
arity EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \EntityTuple
args ->
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Entity
y1,Entity
y2) | Entity
y1 <- EntityTuple
univ, Entity
y2 <- EntityTuple
univ, Entity
y1 forall a. Ord a => a -> a -> Bool
< Entity
y2] forall a b. (a -> b) -> a -> b
$ \(Entity
y1,Entity
y2) -> do
let c :: GroundClause
c = [forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y1), forall a. a -> GenLit a
Neg (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y2)]
EntityTuple
c' <- GroundClause -> IO EntityTuple
translateClause GroundClause
c
forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver EntityTuple
c'
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs) forall a b. (a -> b) -> a -> b
$ \(Var
f, Entity
arity) -> do
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (m :: * -> *) a. Applicative m => Entity -> m a -> m [a]
replicateM Entity
arity EntityTuple
univ) forall a b. (a -> b) -> a -> b
$ \EntityTuple
args -> do
let c :: GroundClause
c = [forall a. a -> GenLit a
Pos (forall v. SGenTerm v -> v -> SGenAtom v
SEq (forall v. Var -> [v] -> SGenTerm v
STmApp Var
f EntityTuple
args) Entity
y) | Entity
y <- EntityTuple
univ]
EntityTuple
c' <- GroundClause -> IO EntityTuple
translateClause GroundClause
c
forall (m :: * -> *) a. AddClause m a => a -> EntityTuple -> m ()
SAT.addClause Solver
solver EntityTuple
c'
Bool
ret <- Solver -> IO Bool
SAT.solve Solver
solver
if Bool
ret
then do
Model
bmodel <- Solver -> IO Model
SAT.getModel Solver
solver
Map GroundAtom Entity
m <- forall a. IORef a -> IO a
readIORef IORef (Map GroundAtom Entity)
ref
let rels :: Map Var (Set EntityTuple)
rels = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
(Var
p,Entity
_) <- forall a. Set a -> [a]
Set.toList Set (Var, Entity)
ps
let tbl :: Set EntityTuple
tbl = forall a. Ord a => [a] -> Set a
Set.fromList [EntityTuple
xs | (SPApp Var
p' EntityTuple
xs, Entity
b) <- forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Entity
m, Var
p forall a. Eq a => a -> a -> Bool
== Var
p', Model
bmodel forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Entity
b]
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
p, Set EntityTuple
tbl)
let funs :: Map Var (Map EntityTuple Entity)
funs = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ do
(Var
f,Entity
_) <- forall a. Set a -> [a]
Set.toList Set (Var, Entity)
fs
let tbl :: Map EntityTuple Entity
tbl = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(EntityTuple
xs, Entity
y) | (SEq (STmApp Var
f' EntityTuple
xs) Entity
y, Entity
b) <- forall k a. Map k a -> [(k, a)]
Map.toList Map GroundAtom Entity
m, Var
f forall a. Eq a => a -> a -> Bool
== Var
f', Model
bmodel forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Entity
b]
forall (m :: * -> *) a. Monad m => a -> m a
return (Var
f, Map EntityTuple Entity
tbl)
let model :: Model
model = Model
{ mUniverse :: EntityTuple
mUniverse = EntityTuple
univ
, mRelations :: Map Var (Set EntityTuple)
mRelations = Map Var (Set EntityTuple)
rels
, mFunctions :: Map Var (Map EntityTuple Entity)
mFunctions = Map Var (Map EntityTuple Entity)
funs
}
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Model
model)
else do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
test :: IO ()
test = do
let c1 :: Clause
c1 = [forall a. a -> GenLit a
Pos forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"=" [Var -> [Term] -> Term
TmApp Var
"f" [Var -> [Term] -> Term
TmApp Var
"g" [Var -> Term
TmVar Var
"x"]], Var -> Term
TmVar Var
"x"]]
c2 :: Clause
c2 = [forall a. a -> GenLit a
Neg forall a b. (a -> b) -> a -> b
$ Var -> [Term] -> Atom
PApp Var
"=" [Var -> Term
TmVar Var
"x", Var -> [Term] -> Term
TmApp Var
"g" [Var -> Term
TmVar Var
"x"]]]
Maybe Model
ret <- Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
3 [Clause
c1, Clause
c2]
case Maybe Model
ret of
Maybe Model
Nothing -> [Char] -> IO ()
putStrLn [Char]
"=== NO MODEL FOUND ==="
Just Model
m -> do
[Char] -> IO ()
putStrLn [Char]
"=== A MODEL FOUND ==="
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m
test2 :: IO ()
test2 = do
let phi :: Formula
phi = forall a. Var -> GenFormula a -> GenFormula a
Forall Var
"x" forall a b. (a -> b) -> a -> b
$ forall a. Var -> GenFormula a -> GenFormula a
Exists Var
"y" forall a b. (a -> b) -> a -> b
$
forall a. Complement a => a -> a
notB (forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"=" [Var -> Term
TmVar Var
"x", Var -> Term
TmVar Var
"y"])) forall a. MonotoneBoolean a => a -> a -> a
.&&.
forall a. a -> GenFormula a
Atom (Var -> [Term] -> Atom
PApp Var
"=" [Var -> [Term] -> Term
TmApp Var
"f" [Var -> Term
TmVar Var
"y"], Var -> Term
TmVar Var
"x"])
IORef Integer
ref <- forall a. a -> IO (IORef a)
newIORef Integer
0
let skolem :: Var -> Int -> IO FSym
skolem :: Var -> Entity -> IO Var
skolem Var
name Entity
_ = do
Integer
n <- forall a. IORef a -> IO a
readIORef IORef Integer
ref
let fsym :: Var
fsym = forall t. Interned t => Uninterned t -> t
intern forall a b. (a -> b) -> a -> b
$ forall t. Uninternable t => t -> Uninterned t
unintern Var
name forall a. Semigroup a => a -> a -> a
<> Uninterned Var
"#" forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Integer
n)
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
ref (Integer
nforall a. Num a => a -> a -> a
+Integer
1)
forall (m :: * -> *) a. Monad m => a -> m a
return Var
fsym
[Clause]
cs <- forall (m :: * -> *).
Monad m =>
(Var -> Entity -> m Var) -> Formula -> m [Clause]
toSkolemNF Var -> Entity -> IO Var
skolem Formula
phi
Maybe Model
ret <- Entity -> [Clause] -> IO (Maybe Model)
findModel Entity
3 [Clause]
cs
case Maybe Model
ret of
Maybe Model
Nothing -> [Char] -> IO ()
putStrLn [Char]
"=== NO MODEL FOUND ==="
Just Model
m -> do
[Char] -> IO ()
putStrLn [Char]
"=== A MODEL FOUND ==="
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ Model -> [[Char]]
showModel Model
m