msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

52.22

/src/ToySolver/EUF/FiniteModelFinder.hs

{-# 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 (intercalate)
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 = Set.unions . map vars

-- | Generalized literal type parameterized by atom type
data GenLit a
  = Pos a
  | Neg a
  deriving (Show, Eq, Ord)

instance Complement (GenLit a) where
  notB (Pos a) = Neg a
  notB (Neg a) = Pos a

instance Vars a => Vars (GenLit a) where
  vars (Pos a) = vars a
  vars (Neg a) = vars a

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

-- | Term
data Term
  = TmApp FSym [Term]
  | TmVar Var
  deriving (Show, Eq, Ord)

data Atom = PApp PSym [Term]
  deriving (Show, Eq, Ord)

type Lit = GenLit Atom

type Clause = [Lit]

instance Vars Term where
  vars (TmVar v)    = Set.singleton v
  vars (TmApp _ ts) = vars ts

instance Vars Atom where
  vars (PApp _ ts) = vars 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 (Show, Eq, Ord)

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

instance Complement (GenFormula a) where
  notB = Not

instance IfThenElse (GenFormula a) (GenFormula a) where
  ite = iteBoolean

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

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

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

    g :: Formula -> Formula
    g T = F
    g F = T
    g (And phi psi)   = g phi .||. g psi
    g (Or phi psi)    = g phi .&&. g psi
    g (Not phi)       = f phi
    g (Imply phi psi) = f phi .&&. g psi
    g (Equiv phi psi) = g ((phi .=>. psi) .&&. (psi .=>. phi))
    g (Forall v phi)  = Exists v (g phi)
    g (Exists v phi)  = Forall v (g phi)
    g (Atom a)        = notB (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 skolem phi = f [] Map.empty (toNNF phi)
  where
    f :: [Var] -> Map Var Term -> Formula -> m [Clause]
    f _ _ T = return []
    f _ _ F = return [[]]
    f _ s (Atom a) = return [[Pos (substAtom s a)]]
    f _ s (Not (Atom a)) = return [[Neg (substAtom s a)]]
    f uvs s (And phi psi) = do
      phi' <- f uvs s phi
      psi' <- f uvs s psi
      return $ phi' ++ psi'
    f uvs s (Or phi psi) = do
      phi' <- f uvs s phi
      psi' <- f uvs s psi
      return $ [c1++c2 | c1 <- phi', c2 <- psi']
    f uvs s psi@(Forall v phi) = do
      let v' = gensym (unintern v) (vars psi `Set.union` Set.fromList uvs)
      f (v' : uvs) (Map.insert v (TmVar v') s) phi
    f uvs s (Exists v phi) = do
      fsym <- skolem v (length uvs)
      f uvs (Map.insert v (TmApp fsym [TmVar v | v <- reverse uvs]) s) phi
    f _ _ _ = error "ToySolver.EUF.FiniteModelFinder.toSkolemNF: should not happen"

    gensym :: Text -> Set Var -> Var
    gensym template vs = head [name | name <- names, Set.notMember name vs]
      where
        names = map intern $ template : [template <> fromString (show n) | n <-[1..]]

    substAtom :: Map Var Term -> Atom -> Atom
    substAtom s (PApp p ts) = PApp p (map (substTerm s) ts)

    substTerm :: Map Var Term -> Term -> Term
    substTerm s (TmVar v)    = fromMaybe (TmVar v) (Map.lookup v s)
    substTerm s (TmApp f ts) = TmApp f (map (substTerm s) ts)

test_toSkolemNF = do
  ref <- newIORef 0
  let skolem :: Var -> Int -> IO FSym
      skolem name _ = do
        n <- readIORef ref
        let fsym = intern $ unintern name <> "#" <> fromString (show n)
        writeIORef ref (n+1)
        return fsym

  -- ∀x. animal(a) → (∃y. heart(y) ∧ has(x,y))
  let phi = Forall "x" $
                Atom (PApp "animal" [TmVar "x"]) .=>.
                (Exists "y" $
                   Atom (PApp "heart" [TmVar "y"]) .&&.
                   Atom (PApp "has" [TmVar "x", TmVar "y"]))

  phi' <- toSkolemNF skolem phi

  print 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 (Show, Eq, Ord)

-- | Shallow atom
data SGenAtom v
  = SPApp PSym [v]
  | SEq (SGenTerm v) v
  deriving (Show, Eq, Ord)

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

instance Vars STerm where
  vars (STmApp _ xs) = Set.fromList xs
  vars (STmVar v)    = Set.singleton v

instance Vars SAtom where
  vars (SPApp _ xs) = Set.fromList xs
  vars (SEq t v) = Set.insert v (vars t)

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

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

flatten :: Clause -> Maybe SClause
flatten c =
  case runState (mapM flattenLit c) (vars c, 0, Map.empty, []) of
    (c, (_,_,_,ls)) -> removeTautology $ removeNegEq $ ls ++ c
  where
    gensym :: M Var
    gensym = do
      (vs, n, defs, ls) <- get
      let go :: Int -> M Var
          go m = do
            let v = intern $ "#" <> fromString (show m)
            if v `Set.member` vs
              then go (m+1)
              else do
                put (Set.insert v vs, m+1, defs, ls)
                return v
      go n

    flattenLit :: Lit -> M SLit
    flattenLit (Pos a) = liftM Pos $ flattenAtom a
    flattenLit (Neg a) = liftM Neg $ flattenAtom a

    flattenAtom :: Atom -> M SAtom
    flattenAtom (PApp "=" [TmVar x, TmVar y])    = return $ SEq (STmVar x) y
    flattenAtom (PApp "=" [TmVar x, TmApp f ts]) = do
      xs <- mapM flattenTerm ts
      return $ SEq (STmApp f xs) x
    flattenAtom (PApp "=" [TmApp f ts, TmVar x]) = do
      xs <- mapM flattenTerm ts
      return $ SEq (STmApp f xs) x
    flattenAtom (PApp "=" [TmApp f ts, t2]) = do
      xs <- mapM flattenTerm ts
      x <- flattenTerm t2
      return $ SEq (STmApp f xs) x
    flattenAtom (PApp p ts) = do
      xs <- mapM flattenTerm ts
      return $ SPApp p xs

    flattenTerm :: Term -> M Var
    flattenTerm (TmVar x)    = return x
    flattenTerm (TmApp f ts) = do
      xs <- mapM flattenTerm ts
      (_, _, defs, _) <- get
      case Map.lookup (f, xs) defs of
        Just x -> return x
        Nothing -> do
          x <- gensym
          (vs, n, defs, ls) <- get
          put (vs, n, Map.insert (f, xs) x defs, Neg (SEq (STmApp f xs) x) : ls)
          return x

    removeNegEq :: SClause -> SClause
    removeNegEq = go []
      where
        go r [] = r
        go r (Neg (SEq (STmVar x) y) : ls) = go (map (substLit x y) r) (map (substLit x y) ls)
        go r (l : ls) = go (l : r) ls

        substLit :: Var -> Var -> SLit -> SLit
        substLit x y (Pos a) = Pos $ substAtom x y a
        substLit x y (Neg a) = Neg $ substAtom x y a

        substAtom :: Var -> Var -> SAtom -> SAtom
        substAtom x y (SPApp p xs) = SPApp p (map (substVar x y) xs)
        substAtom x y (SEq t v)    = SEq (substTerm x y t) (substVar x y v)

        substTerm :: Var -> Var -> STerm -> STerm
        substTerm x y (STmApp f xs) = STmApp f (map (substVar x y) xs)
        substTerm x y (STmVar v)    = STmVar (substVar x y v)

        substVar :: Var -> Var -> Var -> Var
        substVar x y v
          | v==x      = y
          | otherwise = v

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

test_flatten = flatten [Pos $ PApp "P" [TmApp "a" [], TmApp "f" [TmVar "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 e = "$" ++ show e

showEntityTuple :: EntityTuple -> String
showEntityTuple xs = printf "(%s)" $ intercalate ", " $ map showEntity 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 vs univ = do
  ps <- sequence [[(v,e) | e <- univ] | v <- Set.toList vs]
  return $ Map.fromList ps

applySubst :: Subst -> SClause -> GroundClause
applySubst s = map substLit
  where
    substLit :: SLit -> GroundLit
    substLit (Pos a) = Pos $ substAtom a
    substLit (Neg a) = Neg $ substAtom a

    substAtom :: SAtom -> GroundAtom
    substAtom (SPApp p xs) = SPApp p (map substVar xs)
    substAtom (SEq t v)    = SEq (substTerm t) (substVar v)

    substTerm :: STerm ->  GroundTerm
    substTerm (STmApp f xs) = STmApp f (map substVar xs)
    substTerm (STmVar v)    = STmVar (substVar v)

    substVar :: Var -> Entity
    substVar = (s Map.!)

simplifyGroundClause :: GroundClause -> Maybe GroundClause
simplifyGroundClause = liftM concat . mapM f
  where
    f :: GroundLit -> Maybe [GroundLit]
    f (Pos (SEq (STmVar x) y)) = if x==y then Nothing else return []
    f lit = return [lit]

collectFSym :: Clause -> Set (FSym, Int)
collectFSym = Set.unions . map f
  where
    f :: Lit -> Set (FSym, Int)
    f (Pos a) = g a
    f (Neg a) = g a

    g :: Atom -> Set (FSym, Int)
    g (PApp _ xs) = Set.unions $ map h xs

    h :: Term -> Set (FSym, Int)
    h (TmVar _) = Set.empty
    h (TmApp f xs) = Set.unions $ Set.singleton (f, length xs) : map h xs

collectPSym :: Clause -> Set (PSym, Int)
collectPSym = Set.unions . map f
  where
    f :: Lit -> Set (PSym, Int)
    f (Pos a) = g a
    f (Neg a) = g a

    g :: Atom -> Set (PSym, Int)
    g (PApp "=" [_,_]) = Set.empty
    g (PApp p xs) = Set.singleton (p, length xs)

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

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

showModel :: Model -> [String]
showModel m =
  printf "DOMAIN = {%s}" (intercalate ", " (map showEntity (mUniverse m))) :
  [ printf "%s = { %s }" (Text.unpack (unintern p)) s
  | (p, xss) <- Map.toList (mRelations m)
  , let s = intercalate ", " [if length xs == 1 then showEntity (head xs) else showEntityTuple xs | xs <- Set.toList xss]
  ] ++
  [ printf "%s%s = %s" (Text.unpack (unintern f)) (if length xs == 0 then "" else showEntityTuple xs) (showEntity y)
  | (f, xss) <- Map.toList (mFunctions m)
  , (xs, y) <- Map.toList xss
  ]

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

evalAtom :: Model -> Map Var Entity -> Atom -> Bool
evalAtom m env (PApp "=" [x1,x2]) = evalTerm m env x1 == evalTerm m env x2
evalAtom m env (PApp p xs) = map (evalTerm m env) xs `Set.member` (mRelations m Map.! p)

evalTerm :: Model -> Map Var Entity -> Term -> Entity
evalTerm m env (TmVar v) = env Map.! v
evalTerm m env (TmApp f xs) = (mFunctions m Map.! f) Map.! map (evalTerm m env) xs

evalLit :: Model -> Map Var Entity -> Lit -> Bool
evalLit m env (Pos atom) = evalAtom m env atom
evalLit m env (Neg atom) = not $ evalAtom m env atom

evalClause :: Model -> Map Var Entity -> Clause -> Bool
evalClause m env = any (evalLit m env)

evalClauses :: Model -> Map Var Entity -> [Clause] -> Bool
evalClauses m env = all (evalClause m env)

evalClausesU :: Model -> [Clause] -> Bool
evalClausesU m cs = all (\env -> evalClauses m env cs) (enumSubst (vars cs) (mUniverse m))

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

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

  let cs2 = mapMaybe flatten cs
      fs = Set.unions $ map collectFSym cs
      ps = Set.unions $ map collectPSym cs

  solver <- SAT.newSolver

  ref <- newIORef Map.empty

  let translateAtom :: GroundAtom -> IO SAT.Var
      translateAtom (SEq (STmVar _) _) = error "should not happen"
      translateAtom a = do
        m <- readIORef ref
        case Map.lookup a m of
          Just b  -> return b
          Nothing -> do
            b <- SAT.newVar solver
            writeIORef ref (Map.insert a b m)
            return b

      translateLit :: GroundLit -> IO SAT.Lit
      translateLit (Pos a) = translateAtom a
      translateLit (Neg a) = liftM negate $ translateAtom a

      translateClause :: GroundClause -> IO SAT.Clause
      translateClause = mapM translateLit

  -- Instances
  forM_ cs2 $ \c -> do
    forM_ (enumSubst (vars c) univ) $ \s -> do
      case simplifyGroundClause (applySubst s c) of
        Nothing -> return ()
        Just c' -> SAT.addClause solver =<< translateClause c'

  -- Functional definitions
  forM_ (Set.toList fs) $ \(f, arity) -> do
    forM_ (replicateM arity univ) $ \args ->
      forM_ [(y1,y2) | y1 <- univ, y2 <- univ, y1 < y2] $ \(y1,y2) -> do
        let c = [Neg (SEq (STmApp f args) y1), Neg (SEq (STmApp f args) y2)]
        c' <- translateClause c
        SAT.addClause solver c'

  -- Totality definitions
  forM_ (Set.toList fs) $ \(f, arity) -> do
    forM_ (replicateM arity univ) $ \args -> do
        let c = [Pos (SEq (STmApp f args) y) | y <- univ]
        c' <- translateClause c
        SAT.addClause solver c'

  ret <- SAT.solve solver
  if ret
    then do
      bmodel <- SAT.getModel solver
      m <- readIORef ref

      let rels = Map.fromList $ do
            (p,_) <- Set.toList ps
            let tbl = Set.fromList [xs | (SPApp p' xs, b) <- Map.toList m, p == p', bmodel ! b]
            return (p, tbl)
      let funs = Map.fromList $ do
            (f,_) <- Set.toList fs
            let tbl = Map.fromList [(xs, y) | (SEq (STmApp f' xs) y, b) <- Map.toList m, f == f', bmodel ! b]
            return (f, tbl)

      let model = Model
            { mUniverse  = univ
            , mRelations = rels
            , mFunctions = funs
            }

      return (Just model)
    else do
      return Nothing

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

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

test = do
  let c1 = [Pos $ PApp "=" [TmApp "f" [TmApp "g" [TmVar "x"]], TmVar "x"]]
      c2 = [Neg $ PApp "=" [TmVar "x", TmApp "g" [TmVar "x"]]]
  ret <- findModel 3 [c1, c2]
  case ret of
    Nothing -> putStrLn "=== NO MODEL FOUND ==="
    Just m -> do
      putStrLn "=== A MODEL FOUND ==="
      mapM_ putStrLn $ showModel m

test2 = do
  let phi = Forall "x" $ Exists "y" $
              notB (Atom (PApp "=" [TmVar "x", TmVar "y"])) .&&.
              Atom (PApp "=" [TmApp "f" [TmVar "y"], TmVar "x"])

  ref <- newIORef 0
  let skolem :: Var -> Int -> IO FSym
      skolem name _ = do
        n <- readIORef ref
        let fsym = intern $ unintern name <> "#" <> fromString (show n)
        writeIORef ref (n+1)
        return fsym
  cs <- toSkolemNF skolem phi

  ret <- findModel 3 cs
  case ret of
    Nothing -> putStrLn "=== NO MODEL FOUND ==="
    Just m -> do
      putStrLn "=== A MODEL FOUND ==="
      mapM_ putStrLn $ showModel m

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

1	{-# OPTIONS_HADDOCK show-extensions #-}
2	{-# LANGUAGE FlexibleInstances #-}
3	{-# LANGUAGE MultiParamTypeClasses #-}
4	{-# LANGUAGE OverloadedStrings #-}
5	{-# LANGUAGE ScopedTypeVariables #-}
6	{-# LANGUAGE TypeSynonymInstances #-}
7	-----------------------------------------------------------------------------
8	-- \|
9	-- Module : ToySolver.EUF.FiniteModelFinder
10	-- Copyright : (c) Masahiro Sakai 2012, 2015
11	-- License : BSD-style
12	--
13	-- Maintainer : masahiro.sakai@gmail.com
14	-- Stability : provisional
15	-- Portability : non-portable
16	--
17	-- A simple model finder.
18	--
19	-- References:
20	--
21	-- * Koen Claessen and Niklas Sörensson.
22	-- New Techniques that Improve MACE-style Finite Model Finding.
23	-- CADE-19. 2003.
24	-- <http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf>
25	--
26	-----------------------------------------------------------------------------
27	module ToySolver.EUF.FiniteModelFinder
28	(
29	-- * Formula types
30	Var
31	, FSym
32	, PSym
33	, GenLit (..)
34	, Term (..)
35	, Atom (..)
36	, Lit
37	, Clause
38	, Formula
39	, GenFormula (..)
40	, toSkolemNF
41
42	-- * Model types
43	, Model (..)
44	, Entity
45	, EntityTuple
46	, showModel
47	, showEntity
48	, evalFormula
49	, evalAtom
50	, evalTerm
51	, evalLit
52	, evalClause
53	, evalClauses
54	, evalClausesU
55
56	-- * Main function
57	, findModel
58	) where
59
60	import Control.Monad
61	import Control.Monad.State
62	import Data.Array.IArray
63	import Data.Interned (intern, unintern)
64	import Data.Interned.Text
65	import Data.IORef
66	import Data.List (intercalate)
67	import Data.Maybe
68	import Data.Map (Map)
69	import qualified Data.Map as Map
70	import Data.Monoid
71	import Data.Set (Set)
72	import qualified Data.Set as Set
73	import Data.String
74	import Data.Text (Text)
75	import qualified Data.Text as Text
76	import Text.Printf
77
78	import ToySolver.Data.Boolean
79	import qualified ToySolver.SAT as SAT
80
81	-- ---------------------------------------------------------------------------
82
83	-- \| Variable
84	type Var = InternedText
85
86	-- \| Function Symbol
87	type FSym = InternedText
88
89	-- \| Predicate Symbol
90	type PSym = InternedText
91
92	class Vars a where
93	vars :: a -> Set Var
94
95	instance Vars a => Vars [a] where
96	vars = Set.unions . map vars	1✔
97
98	-- \| Generalized literal type parameterized by atom type
99	data GenLit a
100	= Pos a
101	\| Neg a
102	deriving (Show, Eq, Ord)	×
103
104	instance Complement (GenLit a) where
105	notB (Pos a) = Neg a	×
106	notB (Neg a) = Pos a	×
107
108	instance Vars a => Vars (GenLit a) where
109	vars (Pos a) = vars a	1✔
110	vars (Neg a) = vars a	1✔
111
112	-- ---------------------------------------------------------------------------
113
114	-- \| Term
115	data Term
116	= TmApp FSym [Term]
117	\| TmVar Var
118	deriving (Show, Eq, Ord)	×
119
120	data Atom = PApp PSym [Term]
121	deriving (Show, Eq, Ord)	×
122
123	type Lit = GenLit Atom
124
125	type Clause = [Lit]
126
127	instance Vars Term where
128	vars (TmVar v) = Set.singleton v	1✔
129	vars (TmApp _ ts) = vars ts	1✔
130
131	instance Vars Atom where
132	vars (PApp _ ts) = vars ts	1✔
133
134	-- ---------------------------------------------------------------------------
135
136	-- Formula type
137	type Formula = GenFormula Atom
138
139	-- Generalized formula parameterized by atom type
140	data GenFormula a
141	= T
142	\| F
143	\| Atom a
144	\| And (GenFormula a) (GenFormula a)
145	\| Or (GenFormula a) (GenFormula a)
146	\| Not (GenFormula a)
147	\| Imply (GenFormula a) (GenFormula a)
148	\| Equiv (GenFormula a) (GenFormula a)
149	\| Forall Var (GenFormula a)
150	\| Exists Var (GenFormula a)
151	deriving (Show, Eq, Ord)	×
152
153	instance MonotoneBoolean (GenFormula a) where	×
154	true = T	×
155	false = F	×
156	(.&&.) = And	×
157	(.\|\|.) = Or	×
158
159	instance Complement (GenFormula a) where
160	notB = Not	×
161
162	instance IfThenElse (GenFormula a) (GenFormula a) where
163	ite = iteBoolean	×
164
165	instance Boolean (GenFormula a) where
166	(.=>.) = Imply	×
167	(.<=>.) = Equiv	×
168
169	instance Vars a => Vars (GenFormula a) where
170	vars T = Set.empty	×
171	vars F = Set.empty	×
172	vars (Atom a) = vars a	×
173	vars (And phi psi) = vars phi `Set.union` vars psi	×
174	vars (Or phi psi) = vars phi `Set.union` vars psi	×
175	vars (Not phi) = vars phi	×
176	vars (Imply phi psi) = vars phi `Set.union` vars psi	×
177	vars (Equiv phi psi) = vars phi `Set.union` vars psi	×
178	vars (Forall v phi) = Set.delete v (vars phi)	×
179	vars (Exists v phi) = Set.delete v (vars phi)	×
180
181	toNNF :: Formula -> Formula
182	toNNF = f	×
183	where
184	f (And phi psi) = f phi .&&. f psi	×
185	f (Or phi psi) = f phi .\|\|. f psi	×
186	f (Not phi) = g phi	×
187	f (Imply phi psi) = g phi .\|\|. f psi	×
188	f (Equiv phi psi) = f ((phi .=>. psi) .&&. (psi .=>. phi))	×
189	f (Forall v phi) = Forall v (f phi)	×
190	f (Exists v phi) = Exists v (f phi)	×
191	f phi = phi	×
192
193	g :: Formula -> Formula
194	g T = F	×
195	g F = T	×
196	g (And phi psi) = g phi .\|\|. g psi	×
197	g (Or phi psi) = g phi .&&. g psi	×
198	g (Not phi) = f phi	×
199	g (Imply phi psi) = f phi .&&. g psi	×
200	g (Equiv phi psi) = g ((phi .=>. psi) .&&. (psi .=>. phi))	×
201	g (Forall v phi) = Exists v (g phi)	×
202	g (Exists v phi) = Forall v (g phi)	×
203	g (Atom a) = notB (Atom a)	×
204
205	-- \| normalize a formula into a skolem normal form.
206	--
207	-- TODO:
208	--
209	-- * Tseitin encoding
210	toSkolemNF :: forall m. Monad m => (Var -> Int -> m FSym) -> Formula -> m [Clause]
211	toSkolemNF skolem phi = f [] Map.empty (toNNF phi)	×
212	where
213	f :: [Var] -> Map Var Term -> Formula -> m [Clause]
214	f _ _ T = return []	×
215	f _ _ F = return [[]]	×
216	f _ s (Atom a) = return [[Pos (substAtom s a)]]	×
217	f _ s (Not (Atom a)) = return [[Neg (substAtom s a)]]	×
218	f uvs s (And phi psi) = do	×
219	phi' <- f uvs s phi	×
220	psi' <- f uvs s psi	×
221	return $ phi' ++ psi'	×
222	f uvs s (Or phi psi) = do	×
223	phi' <- f uvs s phi	×
224	psi' <- f uvs s psi	×
225	return $ [c1++c2 \| c1 <- phi', c2 <- psi']	×
226	f uvs s psi@(Forall v phi) = do	×
227	let v' = gensym (unintern v) (vars psi `Set.union` Set.fromList uvs)	×
228	f (v' : uvs) (Map.insert v (TmVar v') s) phi	×
229	f uvs s (Exists v phi) = do	×
230	fsym <- skolem v (length uvs)	×
231	f uvs (Map.insert v (TmApp fsym [TmVar v \| v <- reverse uvs]) s) phi	×
232	f _ _ _ = error "ToySolver.EUF.FiniteModelFinder.toSkolemNF: should not happen"	×
233
234	gensym :: Text -> Set Var -> Var
235	gensym template vs = head [name \| name <- names, Set.notMember name vs]	×
236	where
237	names = map intern $ template : [template <> fromString (show n) \| n <-[1..]]	×
238
239	substAtom :: Map Var Term -> Atom -> Atom
240	substAtom s (PApp p ts) = PApp p (map (substTerm s) ts)	×
241
242	substTerm :: Map Var Term -> Term -> Term
243	substTerm s (TmVar v) = fromMaybe (TmVar v) (Map.lookup v s)	×
244	substTerm s (TmApp f ts) = TmApp f (map (substTerm s) ts)	×
245
246	test_toSkolemNF = do	×
247	ref <- newIORef 0	×
248	let skolem :: Var -> Int -> IO FSym
249	skolem name _ = do	×
250	n <- readIORef ref	×
251	let fsym = intern $ unintern name <> "#" <> fromString (show n)	×
252	writeIORef ref (n+1)	×
253	return fsym	×
254
255	-- ∀x. animal(a) → (∃y. heart(y) ∧ has(x,y))
256	let phi = Forall "x" $	×
257	Atom (PApp "animal" [TmVar "x"]) .=>.	×
258	(Exists "y" $	×
259	Atom (PApp "heart" [TmVar "y"]) .&&.	×
260	Atom (PApp "has" [TmVar "x", TmVar "y"]))	×
261
262	phi' <- toSkolemNF skolem phi	×
263
264	print phi'	×
265	{-
266	[[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"]])]]
267
268	{¬animal(x) ∨ heart(y#1(x)), ¬animal(x) ∨ has(x1, y#0(x))}
269	-}
270
271	-- ---------------------------------------------------------------------------
272
273	-- \| Shallow term
274	data SGenTerm v
275	= STmApp FSym [v]
276	\| STmVar v
277	deriving (Show, Eq, Ord)	×
278
279	-- \| Shallow atom
280	data SGenAtom v
281	= SPApp PSym [v]
282	\| SEq (SGenTerm v) v
283	deriving (Show, Eq, Ord)	×
284
285	type STerm = SGenTerm Var
286	type SAtom = SGenAtom Var
287	type SLit = GenLit SAtom
288	type SClause = [SLit]
289
290	instance Vars STerm where
291	vars (STmApp _ xs) = Set.fromList xs	1✔
292	vars (STmVar v) = Set.singleton v	1✔
293
294	instance Vars SAtom where
295	vars (SPApp _ xs) = Set.fromList xs	1✔
296	vars (SEq t v) = Set.insert v (vars t)	1✔
297
298	-- ---------------------------------------------------------------------------
299
300	type M = State (Set Var, Int, Map (FSym, [Var]) Var, [SLit])
301
302	flatten :: Clause -> Maybe SClause
303	flatten c =	1✔
304	case runState (mapM flattenLit c) (vars c, 0, Map.empty, []) of	1✔
305	(c, (_,_,_,ls)) -> removeTautology $ removeNegEq $ ls ++ c	1✔
306	where
307	gensym :: M Var
308	gensym = do	1✔
309	(vs, n, defs, ls) <- get	1✔
310	let go :: Int -> M Var
311	go m = do	1✔
312	let v = intern $ "#" <> fromString (show m)	1✔
313	if v `Set.member` vs	×
314	then go (m+1)	×
315	else do	1✔
316	put (Set.insert v vs, m+1, defs, ls)	1✔
317	return v	1✔
318	go n	1✔
319
320	flattenLit :: Lit -> M SLit
321	flattenLit (Pos a) = liftM Pos $ flattenAtom a	1✔
322	flattenLit (Neg a) = liftM Neg $ flattenAtom a	1✔
323
324	flattenAtom :: Atom -> M SAtom
325	flattenAtom (PApp "=" [TmVar x, TmVar y]) = return $ SEq (STmVar x) y	1✔
326	flattenAtom (PApp "=" [TmVar x, TmApp f ts]) = do	1✔
327	xs <- mapM flattenTerm ts	1✔
328	return $ SEq (STmApp f xs) x	1✔
329	flattenAtom (PApp "=" [TmApp f ts, TmVar x]) = do	1✔
330	xs <- mapM flattenTerm ts	1✔
331	return $ SEq (STmApp f xs) x	1✔
332	flattenAtom (PApp "=" [TmApp f ts, t2]) = do	1✔
333	xs <- mapM flattenTerm ts	1✔
334	x <- flattenTerm t2	1✔
335	return $ SEq (STmApp f xs) x	1✔
336	flattenAtom (PApp p ts) = do	1✔
337	xs <- mapM flattenTerm ts	1✔
338	return $ SPApp p xs	1✔
339
340	flattenTerm :: Term -> M Var
341	flattenTerm (TmVar x) = return x	1✔
342	flattenTerm (TmApp f ts) = do	1✔
343	xs <- mapM flattenTerm ts	1✔
344	(_, _, defs, _) <- get	1✔
345	case Map.lookup (f, xs) defs of	1✔
346	Just x -> return x	1✔
347	Nothing -> do	1✔
348	x <- gensym	1✔
349	(vs, n, defs, ls) <- get	1✔
350	put (vs, n, Map.insert (f, xs) x defs, Neg (SEq (STmApp f xs) x) : ls)	1✔
351	return x	1✔
352
353	removeNegEq :: SClause -> SClause
354	removeNegEq = go []	1✔
355	where
356	go r [] = r	1✔
357	go r (Neg (SEq (STmVar x) y) : ls) = go (map (substLit x y) r) (map (substLit x y) ls)	1✔
358	go r (l : ls) = go (l : r) ls	1✔
359
360	substLit :: Var -> Var -> SLit -> SLit
361	substLit x y (Pos a) = Pos $ substAtom x y a	1✔
362	substLit x y (Neg a) = Neg $ substAtom x y a	1✔
363
364	substAtom :: Var -> Var -> SAtom -> SAtom
365	substAtom x y (SPApp p xs) = SPApp p (map (substVar x y) xs)	×
366	substAtom x y (SEq t v) = SEq (substTerm x y t) (substVar x y v)	1✔
367
368	substTerm :: Var -> Var -> STerm -> STerm
369	substTerm x y (STmApp f xs) = STmApp f (map (substVar x y) xs)	1✔
370	substTerm x y (STmVar v) = STmVar (substVar x y v)	1✔
371
372	substVar :: Var -> Var -> Var -> Var
373	substVar x y v	1✔
374	\| v==x = y	1✔
375	\| otherwise = v	×
376
377	removeTautology :: SClause -> Maybe SClause
378	removeTautology lits	1✔
379	\| Set.null (pos `Set.intersection` neg) = Just $ [Neg l \| l <- Set.toList neg] ++ [Pos l \| l <- Set.toList pos]	1✔
380	\| otherwise = Nothing	×
381	where
382	pos = Set.fromList [l \| Pos l <- lits]	1✔
383	neg = Set.fromList [l \| Neg l <- lits]	1✔
384
385	test_flatten = flatten [Pos $ PApp "P" [TmApp "a" [], TmApp "f" [TmVar "x"]]]	×
386
387	{-
388	[Pos $ PApp "P" [TmApp "a" [], TmApp "f" [TmVar "x"]]]
389
390	P(a, f(x))
391
392	[Pos (SPApp "P" ["#0","#1"]),Neg (SEq (STmApp "a" []) "#0"),Neg (SEq (STmApp "f" ["x"]) "#1")]
393
394	f(x) ≠ z ∨ a ≠ y ∨ P(y,z)
395	(f(x) = z ∧ a = y) → P(y,z)
396	-}
397
398	-- ---------------------------------------------------------------------------
399
400	-- \| Element of model.
401	type Entity = Int
402
403	type EntityTuple = [Entity]
404
405	-- \| print entity
406	showEntity :: Entity -> String
407	showEntity e = "$" ++ show e	×
408
409	showEntityTuple :: EntityTuple -> String
410	showEntityTuple xs = printf "(%s)" $ intercalate ", " $ map showEntity xs	×
411
412	-- ---------------------------------------------------------------------------
413
414	type GroundTerm = SGenTerm Entity
415	type GroundAtom = SGenAtom Entity
416	type GroundLit = GenLit GroundAtom
417	type GroundClause = [GroundLit]
418
419	type Subst = Map Var Entity
420
421	enumSubst :: Set Var -> [Entity] -> [Subst]
422	enumSubst vs univ = do	1✔
423	ps <- sequence [[(v,e) \| e <- univ] \| v <- Set.toList vs]	1✔
424	return $ Map.fromList ps	1✔
425
426	applySubst :: Subst -> SClause -> GroundClause
427	applySubst s = map substLit	1✔
428	where
429	substLit :: SLit -> GroundLit
430	substLit (Pos a) = Pos $ substAtom a	1✔
431	substLit (Neg a) = Neg $ substAtom a	1✔
432
433	substAtom :: SAtom -> GroundAtom
434	substAtom (SPApp p xs) = SPApp p (map substVar xs)	1✔
435	substAtom (SEq t v) = SEq (substTerm t) (substVar v)	1✔
436
437	substTerm :: STerm -> GroundTerm
438	substTerm (STmApp f xs) = STmApp f (map substVar xs)	1✔
439	substTerm (STmVar v) = STmVar (substVar v)	1✔
440
441	substVar :: Var -> Entity
442	substVar = (s Map.!)	1✔
443
444	simplifyGroundClause :: GroundClause -> Maybe GroundClause
445	simplifyGroundClause = liftM concat . mapM f	1✔
446	where
447	f :: GroundLit -> Maybe [GroundLit]
448	f (Pos (SEq (STmVar x) y)) = if x==y then Nothing else return []	1✔
449	f lit = return [lit]	1✔
450
451	collectFSym :: Clause -> Set (FSym, Int)
452	collectFSym = Set.unions . map f	1✔
453	where
454	f :: Lit -> Set (FSym, Int)
455	f (Pos a) = g a	1✔
456	f (Neg a) = g a	1✔
457
458	g :: Atom -> Set (FSym, Int)
459	g (PApp _ xs) = Set.unions $ map h xs	1✔
460
461	h :: Term -> Set (FSym, Int)
462	h (TmVar _) = Set.empty	1✔
463	h (TmApp f xs) = Set.unions $ Set.singleton (f, length xs) : map h xs	1✔
464
465	collectPSym :: Clause -> Set (PSym, Int)
466	collectPSym = Set.unions . map f	1✔
467	where
468	f :: Lit -> Set (PSym, Int)
469	f (Pos a) = g a	1✔
470	f (Neg a) = g a	1✔
471
472	g :: Atom -> Set (PSym, Int)
473	g (PApp "=" [_,_]) = Set.empty	1✔
474	g (PApp p xs) = Set.singleton (p, length xs)	1✔
475
476	-- ---------------------------------------------------------------------------
477
478	data Model
479	= Model
480	{ mUniverse :: [Entity]	1✔
481	, mRelations :: Map PSym (Set EntityTuple)	1✔
482	, mFunctions :: Map FSym (Map EntityTuple Entity)	1✔
483	}
484
485	showModel :: Model -> [String]
486	showModel m =	×
487	printf "DOMAIN = {%s}" (intercalate ", " (map showEntity (mUniverse m))) :	×
488	[ printf "%s = { %s }" (Text.unpack (unintern p)) s	×
489	\| (p, xss) <- Map.toList (mRelations m)	×
490	, let s = intercalate ", " [if length xs == 1 then showEntity (head xs) else showEntityTuple xs \| xs <- Set.toList xss]	×
491	] ++
492	[ printf "%s%s = %s" (Text.unpack (unintern f)) (if length xs == 0 then "" else showEntityTuple xs) (showEntity y)	×
493	\| (f, xss) <- Map.toList (mFunctions m)	×
494	, (xs, y) <- Map.toList xss	×
495	]
496
497	evalFormula :: Model -> Formula -> Bool
498	evalFormula m = f Map.empty	×
499	where
500	f :: Map Var Entity -> Formula -> Bool
501	f env T = True	×
502	f env F = False	×
503	f env (Atom a) = evalAtom m env a	×
504	f env (And phi1 phi2) = f env phi1 && f env phi2	×
505	f env (Or phi1 phi2) = f env phi1 \|\| f env phi2	×
506	f env (Not phi) = not (f env phi)	×
507	f env (Imply phi1 phi2) = not (f env phi1) \|\| f env phi2	×
508	f env (Equiv phi1 phi2) = f env phi1 == f env phi2	×
509	f env (Forall v phi) = all (\e -> f (Map.insert v e env) phi) (mUniverse m)	×
510	f env (Exists v phi) = any (\e -> f (Map.insert v e env) phi) (mUniverse m)	×
511
512	evalAtom :: Model -> Map Var Entity -> Atom -> Bool
513	evalAtom m env (PApp "=" [x1,x2]) = evalTerm m env x1 == evalTerm m env x2	1✔
514	evalAtom m env (PApp p xs) = map (evalTerm m env) xs `Set.member` (mRelations m Map.! p)	1✔
515
516	evalTerm :: Model -> Map Var Entity -> Term -> Entity
517	evalTerm m env (TmVar v) = env Map.! v	1✔
518	evalTerm m env (TmApp f xs) = (mFunctions m Map.! f) Map.! map (evalTerm m env) xs	1✔
519
520	evalLit :: Model -> Map Var Entity -> Lit -> Bool
521	evalLit m env (Pos atom) = evalAtom m env atom	1✔
522	evalLit m env (Neg atom) = not $ evalAtom m env atom	1✔
523
524	evalClause :: Model -> Map Var Entity -> Clause -> Bool
525	evalClause m env = any (evalLit m env)	1✔
526
527	evalClauses :: Model -> Map Var Entity -> [Clause] -> Bool
528	evalClauses m env = all (evalClause m env)	1✔
529
530	evalClausesU :: Model -> [Clause] -> Bool
531	evalClausesU m cs = all (\env -> evalClauses m env cs) (enumSubst (vars cs) (mUniverse m))	1✔
532
533	-- ---------------------------------------------------------------------------
534
535	findModel :: Int -> [Clause] -> IO (Maybe Model)
536	findModel size cs = do	1✔
537	let univ = [0..size-1]	1✔
538
539	let cs2 = mapMaybe flatten cs	1✔
540	fs = Set.unions $ map collectFSym cs	1✔
541	ps = Set.unions $ map collectPSym cs	1✔
542
543	solver <- SAT.newSolver	1✔
544
545	ref <- newIORef Map.empty	1✔
546
547	let translateAtom :: GroundAtom -> IO SAT.Var
548	translateAtom (SEq (STmVar _) _) = error "should not happen"	×
549	translateAtom a = do	1✔
550	m <- readIORef ref	1✔
551	case Map.lookup a m of	1✔
552	Just b -> return b	1✔
553	Nothing -> do	1✔
554	b <- SAT.newVar solver	1✔
555	writeIORef ref (Map.insert a b m)	1✔
556	return b	1✔
557
558	translateLit :: GroundLit -> IO SAT.Lit
559	translateLit (Pos a) = translateAtom a	1✔
560	translateLit (Neg a) = liftM negate $ translateAtom a	1✔
561
562	translateClause :: GroundClause -> IO SAT.Clause
563	translateClause = mapM translateLit	1✔
564
565	-- Instances
566	forM_ cs2 $ \c -> do	1✔
567	forM_ (enumSubst (vars c) univ) $ \s -> do	1✔
568	case simplifyGroundClause (applySubst s c) of	1✔
569	Nothing -> return ()	×
570	Just c' -> SAT.addClause solver =<< translateClause c'	1✔
571
572	-- Functional definitions
573	forM_ (Set.toList fs) $ \(f, arity) -> do	1✔
574	forM_ (replicateM arity univ) $ \args ->	1✔
575	forM_ [(y1,y2) \| y1 <- univ, y2 <- univ, y1 < y2] $ \(y1,y2) -> do	1✔
576	let c = [Neg (SEq (STmApp f args) y1), Neg (SEq (STmApp f args) y2)]	1✔
577	c' <- translateClause c	1✔
578	SAT.addClause solver c'	1✔
579
580	-- Totality definitions
581	forM_ (Set.toList fs) $ \(f, arity) -> do	1✔
582	forM_ (replicateM arity univ) $ \args -> do	1✔
583	let c = [Pos (SEq (STmApp f args) y) \| y <- univ]	1✔
584	c' <- translateClause c	1✔
585	SAT.addClause solver c'	1✔
586
587	ret <- SAT.solve solver	1✔
588	if ret	1✔
589	then do	1✔
590	bmodel <- SAT.getModel solver	1✔
591	m <- readIORef ref	1✔
592
593	let rels = Map.fromList $ do	1✔
594	(p,_) <- Set.toList ps	1✔
595	let tbl = Set.fromList [xs \| (SPApp p' xs, b) <- Map.toList m, p == p', bmodel ! b]	1✔
596	return (p, tbl)	1✔
597	let funs = Map.fromList $ do	1✔
598	(f,_) <- Set.toList fs	1✔
599	let tbl = Map.fromList [(xs, y) \| (SEq (STmApp f' xs) y, b) <- Map.toList m, f == f', bmodel ! b]	1✔
600	return (f, tbl)	1✔
601
602	let model = Model	1✔
603	{ mUniverse = univ	1✔
604	, mRelations = rels	1✔
605	, mFunctions = funs	1✔
606	}
607
608	return (Just model)	1✔
609	else do	1✔
610	return Nothing	1✔
611
612	-- ---------------------------------------------------------------------------
613
614	{-
615	∀x. ∃y. x≠y && f(y)=x
616	∀x. x≠g(x) ∧ f(g(x))=x
617	-}
618
619	test = do	×
620	let c1 = [Pos $ PApp "=" [TmApp "f" [TmApp "g" [TmVar "x"]], TmVar "x"]]	×
621	c2 = [Neg $ PApp "=" [TmVar "x", TmApp "g" [TmVar "x"]]]	×
622	ret <- findModel 3 [c1, c2]	×
623	case ret of	×
624	Nothing -> putStrLn "=== NO MODEL FOUND ==="	×
625	Just m -> do	×
626	putStrLn "=== A MODEL FOUND ==="	×
627	mapM_ putStrLn $ showModel m	×
628
629	test2 = do	×
630	let phi = Forall "x" $ Exists "y" $	×
631	notB (Atom (PApp "=" [TmVar "x", TmVar "y"])) .&&.	×
632	Atom (PApp "=" [TmApp "f" [TmVar "y"], TmVar "x"])	×
633
634	ref <- newIORef 0	×
635	let skolem :: Var -> Int -> IO FSym
636	skolem name _ = do	×
637	n <- readIORef ref	×
638	let fsym = intern $ unintern name <> "#" <> fromString (show n)	×
639	writeIORef ref (n+1)	×
640	return fsym	×
641	cs <- toSkolemNF skolem phi	×
642
643	ret <- findModel 3 cs	×
644	case ret of	×
645	Nothing -> putStrLn "=== NO MODEL FOUND ==="	×
646	Just m -> do	×
647	putStrLn "=== A MODEL FOUND ==="	×
648	mapM_ putStrLn $ showModel m	×
649
650	-- ---------------------------------------------------------------------------

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous