{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.EUF.CongruenceClosure
-- Copyright   :  (c) Masahiro Sakai 2012, 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- References:
--
-- * R. Nieuwenhuis and A. Oliveras, "Fast congruence closure and extensions,"
--   Information and Computation, vol. 205, no. 4, pp. 557-580, Apr. 2007.
--   <http://www.lsi.upc.edu/~oliveras/espai/papers/IC.pdf>
--
-----------------------------------------------------------------------------
module ToySolver.EUF.CongruenceClosure
  (
  -- * The @Solver@ type
    Solver
  , newSolver

  -- * Problem description
  , FSym
  , Term (..)
  , FlatTerm (..)
  , ConstrID
  , newFSym
  , VAFun (..)
  , newFun
  , newConst
  , merge
  , merge'
  , mergeFlatTerm
  , mergeFlatTerm'

  -- * Query
  , areCongruent
  , areCongruentFlatTerm

  -- * Explanation
  , explain
  , explainFlatTerm
  , explainConst

  -- * Model Construction
  , Entity
  , EntityTuple
  , Model (..)
  , getModel
  , eval
  , evalAp

  -- * Backtracking
  , pushBacktrackPoint
  , popBacktrackPoint

  -- * Low-level operations
  , termToFlatTerm
  , termToFSym
  , fsymToTerm
  , fsymToFlatTerm
  , flatTermToFSym
  ) where

import Prelude hiding (lookup)

import Control.Exception (assert)
import Control.Loop
import Control.Monad
import Data.IORef
import Data.IntMap.Strict (IntMap)
import qualified Data.IntMap.Strict as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set

import qualified ToySolver.Internal.Data.Vec as Vec

type FSym = Int

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

data FlatTerm
  = FTConst !FSym
  | FTApp !FSym !FSym
  deriving (Eq FlatTerm
Eq FlatTerm =>
(FlatTerm -> FlatTerm -> Ordering)
-> (FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> FlatTerm)
-> (FlatTerm -> FlatTerm -> FlatTerm)
-> Ord FlatTerm
FlatTerm -> FlatTerm -> Bool
FlatTerm -> FlatTerm -> Ordering
FlatTerm -> FlatTerm -> FlatTerm
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FlatTerm -> FlatTerm -> Ordering
compare :: FlatTerm -> FlatTerm -> Ordering
$c< :: FlatTerm -> FlatTerm -> Bool
< :: FlatTerm -> FlatTerm -> Bool
$c<= :: FlatTerm -> FlatTerm -> Bool
<= :: FlatTerm -> FlatTerm -> Bool
$c> :: FlatTerm -> FlatTerm -> Bool
> :: FlatTerm -> FlatTerm -> Bool
$c>= :: FlatTerm -> FlatTerm -> Bool
>= :: FlatTerm -> FlatTerm -> Bool
$cmax :: FlatTerm -> FlatTerm -> FlatTerm
max :: FlatTerm -> FlatTerm -> FlatTerm
$cmin :: FlatTerm -> FlatTerm -> FlatTerm
min :: FlatTerm -> FlatTerm -> FlatTerm
Ord, FlatTerm -> FlatTerm -> Bool
(FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> Bool) -> Eq FlatTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FlatTerm -> FlatTerm -> Bool
== :: FlatTerm -> FlatTerm -> Bool
$c/= :: FlatTerm -> FlatTerm -> Bool
/= :: FlatTerm -> FlatTerm -> Bool
Eq, FSym -> FlatTerm -> ShowS
[FlatTerm] -> ShowS
FlatTerm -> String
(FSym -> FlatTerm -> ShowS)
-> (FlatTerm -> String) -> ([FlatTerm] -> ShowS) -> Show FlatTerm
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> FlatTerm -> ShowS
showsPrec :: FSym -> FlatTerm -> ShowS
$cshow :: FlatTerm -> String
show :: FlatTerm -> String
$cshowList :: [FlatTerm] -> ShowS
showList :: [FlatTerm] -> ShowS
Show)

type ConstrID = Int

-- | @Eqn0 cid a b@ represents an equation "a = b"
data Eqn0 = Eqn0 (Maybe ConstrID) !FSym !FSym
  deriving (Eqn0 -> Eqn0 -> Bool
(Eqn0 -> Eqn0 -> Bool) -> (Eqn0 -> Eqn0 -> Bool) -> Eq Eqn0
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Eqn0 -> Eqn0 -> Bool
== :: Eqn0 -> Eqn0 -> Bool
$c/= :: Eqn0 -> Eqn0 -> Bool
/= :: Eqn0 -> Eqn0 -> Bool
Eq, Eq Eqn0
Eq Eqn0 =>
(Eqn0 -> Eqn0 -> Ordering)
-> (Eqn0 -> Eqn0 -> Bool)
-> (Eqn0 -> Eqn0 -> Bool)
-> (Eqn0 -> Eqn0 -> Bool)
-> (Eqn0 -> Eqn0 -> Bool)
-> (Eqn0 -> Eqn0 -> Eqn0)
-> (Eqn0 -> Eqn0 -> Eqn0)
-> Ord Eqn0
Eqn0 -> Eqn0 -> Bool
Eqn0 -> Eqn0 -> Ordering
Eqn0 -> Eqn0 -> Eqn0
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Eqn0 -> Eqn0 -> Ordering
compare :: Eqn0 -> Eqn0 -> Ordering
$c< :: Eqn0 -> Eqn0 -> Bool
< :: Eqn0 -> Eqn0 -> Bool
$c<= :: Eqn0 -> Eqn0 -> Bool
<= :: Eqn0 -> Eqn0 -> Bool
$c> :: Eqn0 -> Eqn0 -> Bool
> :: Eqn0 -> Eqn0 -> Bool
$c>= :: Eqn0 -> Eqn0 -> Bool
>= :: Eqn0 -> Eqn0 -> Bool
$cmax :: Eqn0 -> Eqn0 -> Eqn0
max :: Eqn0 -> Eqn0 -> Eqn0
$cmin :: Eqn0 -> Eqn0 -> Eqn0
min :: Eqn0 -> Eqn0 -> Eqn0
Ord, FSym -> Eqn0 -> ShowS
[Eqn0] -> ShowS
Eqn0 -> String
(FSym -> Eqn0 -> ShowS)
-> (Eqn0 -> String) -> ([Eqn0] -> ShowS) -> Show Eqn0
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> Eqn0 -> ShowS
showsPrec :: FSym -> Eqn0 -> ShowS
$cshow :: Eqn0 -> String
show :: Eqn0 -> String
$cshowList :: [Eqn0] -> ShowS
showList :: [Eqn0] -> ShowS
Show)

-- | @Eqn1 cid a b c@ represents an equation "f(a,b) = c"
data Eqn1 = Eqn1 (Maybe ConstrID) !FSym !FSym !FSym
  deriving (Eqn1 -> Eqn1 -> Bool
(Eqn1 -> Eqn1 -> Bool) -> (Eqn1 -> Eqn1 -> Bool) -> Eq Eqn1
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Eqn1 -> Eqn1 -> Bool
== :: Eqn1 -> Eqn1 -> Bool
$c/= :: Eqn1 -> Eqn1 -> Bool
/= :: Eqn1 -> Eqn1 -> Bool
Eq, Eq Eqn1
Eq Eqn1 =>
(Eqn1 -> Eqn1 -> Ordering)
-> (Eqn1 -> Eqn1 -> Bool)
-> (Eqn1 -> Eqn1 -> Bool)
-> (Eqn1 -> Eqn1 -> Bool)
-> (Eqn1 -> Eqn1 -> Bool)
-> (Eqn1 -> Eqn1 -> Eqn1)
-> (Eqn1 -> Eqn1 -> Eqn1)
-> Ord Eqn1
Eqn1 -> Eqn1 -> Bool
Eqn1 -> Eqn1 -> Ordering
Eqn1 -> Eqn1 -> Eqn1
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Eqn1 -> Eqn1 -> Ordering
compare :: Eqn1 -> Eqn1 -> Ordering
$c< :: Eqn1 -> Eqn1 -> Bool
< :: Eqn1 -> Eqn1 -> Bool
$c<= :: Eqn1 -> Eqn1 -> Bool
<= :: Eqn1 -> Eqn1 -> Bool
$c> :: Eqn1 -> Eqn1 -> Bool
> :: Eqn1 -> Eqn1 -> Bool
$c>= :: Eqn1 -> Eqn1 -> Bool
>= :: Eqn1 -> Eqn1 -> Bool
$cmax :: Eqn1 -> Eqn1 -> Eqn1
max :: Eqn1 -> Eqn1 -> Eqn1
$cmin :: Eqn1 -> Eqn1 -> Eqn1
min :: Eqn1 -> Eqn1 -> Eqn1
Ord, FSym -> Eqn1 -> ShowS
[Eqn1] -> ShowS
Eqn1 -> String
(FSym -> Eqn1 -> ShowS)
-> (Eqn1 -> String) -> ([Eqn1] -> ShowS) -> Show Eqn1
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> Eqn1 -> ShowS
showsPrec :: FSym -> Eqn1 -> ShowS
$cshow :: Eqn1 -> String
show :: Eqn1 -> String
$cshowList :: [Eqn1] -> ShowS
showList :: [Eqn1] -> ShowS
Show)

-- | An equation @a = b@ represented as either
--
-- * @a = b@ or
--
-- * @f(a1,a2) = a, f(b1,b2) = b@ where @a1 = b1@ and @a2 = b2@ has already been derived.
--
type Eqn = Either Eqn0 (Eqn1, Eqn1)

data Class
  = ClassSingleton !FSym
  | ClassUnion !Int Class Class
  deriving (FSym -> Class -> ShowS
[Class] -> ShowS
Class -> String
(FSym -> Class -> ShowS)
-> (Class -> String) -> ([Class] -> ShowS) -> Show Class
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> Class -> ShowS
showsPrec :: FSym -> Class -> ShowS
$cshow :: Class -> String
show :: Class -> String
$cshowList :: [Class] -> ShowS
showList :: [Class] -> ShowS
Show)

instance Semigroup Class where
  Class
xs <> :: Class -> Class -> Class
<> Class
ys = FSym -> Class -> Class -> Class
ClassUnion (Class -> FSym
classSize Class
xs FSym -> FSym -> FSym
forall a. Num a => a -> a -> a
+ Class -> FSym
classSize Class
ys) Class
xs Class
ys

classSize :: Class -> Int
classSize :: Class -> FSym
classSize (ClassSingleton FSym
_) = FSym
1
classSize (ClassUnion FSym
size Class
_ Class
_) = FSym
size

-- Use mono-traversable package?
classToList :: Class -> [FSym]
classToList :: Class -> [FSym]
classToList Class
c = Class -> [FSym] -> [FSym]
f Class
c []
  where
    f :: Class -> [FSym] -> [FSym]
f (ClassSingleton FSym
v) = (FSym
v FSym -> [FSym] -> [FSym]
forall a. a -> [a] -> [a]
:)
    f (ClassUnion FSym
_ Class
xs Class
ys) = Class -> [FSym] -> [FSym]
f Class
xs ([FSym] -> [FSym]) -> ([FSym] -> [FSym]) -> [FSym] -> [FSym]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Class -> [FSym] -> [FSym]
f Class
ys

-- Use mono-traversable package?
classForM_ :: Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ :: forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
xs FSym -> m ()
f = Class -> m ()
g Class
xs
  where
    g :: Class -> m ()
g (ClassSingleton FSym
v) = FSym -> m ()
f FSym
v
    g (ClassUnion FSym
_ Class
xs Class
ys) = Class -> m ()
g Class
xs m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Class -> m ()
g Class
ys

data Solver
  = Solver
  { Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs                 :: !(IORef (IntMap (FSym,FSym), Map (FSym,FSym) FSym))
  , Solver -> UVec FSym
svRepresentativeTable  :: !(Vec.UVec FSym)
  , Solver -> Vec Class
svClassList            :: !(Vec.Vec Class)
  , Solver -> IORef (IntMap (FSym, Eqn))
svParent               :: !(IORef (IntMap (FSym, Eqn)))
  , Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList              :: !(IORef (IntMap [(Eqn1, Level, Gen)]))
  , Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable          :: !(IORef (IntMap (IntMap Eqn1)))

  -- workspace for constraint propagation
  , Solver -> Vec Eqn
svPending :: !(Vec.Vec Eqn)

  -- workspace for explanation generation
  , Solver -> UVec FSym
svERepresentativeTable :: !(Vec.UVec FSym)
  , Solver -> Vec Class
svEClassList           :: !(Vec.Vec Class)
  , Solver -> UVec FSym
svEHighestNodeTable    :: !(Vec.UVec FSym)
  , Solver -> Vec (FSym, FSym)
svEPendingProofs       :: !(Vec.Vec (FSym,FSym))

  -- for backtracking
  , Solver -> Vec [TrailItem]
svTrail :: !(Vec.Vec [TrailItem])
  , Solver -> UVec FSym
svLevelGen :: !(Vec.UVec Int)
  , Solver -> IORef Bool
svIsAfterBacktracking :: !(IORef Bool)
  }

newSolver :: IO Solver
newSolver :: IO Solver
newSolver = do
  IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
defs     <- (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym))
forall a. a -> IO (IORef a)
newIORef (IntMap (FSym, FSym)
forall a. IntMap a
IntMap.empty, Map (FSym, FSym) FSym
forall k a. Map k a
Map.empty)
  UVec FSym
rep      <- IO (UVec FSym)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec Class
classes  <- IO (Vec Class)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  IORef (IntMap (FSym, Eqn))
parent   <- IntMap (FSym, Eqn) -> IO (IORef (IntMap (FSym, Eqn)))
forall a. a -> IO (IORef a)
newIORef IntMap (FSym, Eqn)
forall a. IntMap a
IntMap.empty
  IORef (IntMap [(Eqn1, FSym, FSym)])
useList  <- IntMap [(Eqn1, FSym, FSym)]
-> IO (IORef (IntMap [(Eqn1, FSym, FSym)]))
forall a. a -> IO (IORef a)
newIORef IntMap [(Eqn1, FSym, FSym)]
forall a. IntMap a
IntMap.empty
  IORef (IntMap (IntMap Eqn1))
lookup   <- IntMap (IntMap Eqn1) -> IO (IORef (IntMap (IntMap Eqn1)))
forall a. a -> IO (IORef a)
newIORef IntMap (IntMap Eqn1)
forall a. IntMap a
IntMap.empty

  Vec Eqn
pending  <- IO (Vec Eqn)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new

  UVec FSym
repE     <- IO (UVec FSym)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec Class
classesE <- IO (Vec Class)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  UVec FSym
highE    <- IO (UVec FSym)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec (FSym, FSym)
pendingE <- IO (Vec (FSym, FSym))
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new

  Vec [TrailItem]
trail <- IO (Vec [TrailItem])
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  UVec FSym
gen <- IO (UVec FSym)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  UVec FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec FSym
gen FSym
0
  IORef Bool
isAfterBT <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False

  Solver -> IO Solver
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> IO Solver) -> Solver -> IO Solver
forall a b. (a -> b) -> a -> b
$
    Solver
    { svDefs :: IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs                = IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
defs
    , svRepresentativeTable :: UVec FSym
svRepresentativeTable = UVec FSym
rep
    , svClassList :: Vec Class
svClassList           = Vec Class
classes
    , svParent :: IORef (IntMap (FSym, Eqn))
svParent              = IORef (IntMap (FSym, Eqn))
parent
    , svUseList :: IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList             = IORef (IntMap [(Eqn1, FSym, FSym)])
useList
    , svLookupTable :: IORef (IntMap (IntMap Eqn1))
svLookupTable         = IORef (IntMap (IntMap Eqn1))
lookup

    -- workspace for constraint propagation
    , svPending :: Vec Eqn
svPending = Vec Eqn
pending

    -- workspace for explanation generation
    , svERepresentativeTable :: UVec FSym
svERepresentativeTable = UVec FSym
repE
    , svEClassList :: Vec Class
svEClassList           = Vec Class
classesE
    , svEHighestNodeTable :: UVec FSym
svEHighestNodeTable    = UVec FSym
highE
    , svEPendingProofs :: Vec (FSym, FSym)
svEPendingProofs       = Vec (FSym, FSym)
pendingE

    -- for backtracking
    , svTrail :: Vec [TrailItem]
svTrail = Vec [TrailItem]
trail
    , svLevelGen :: UVec FSym
svLevelGen = UVec FSym
gen
    , svIsAfterBacktracking :: IORef Bool
svIsAfterBacktracking = IORef Bool
isAfterBT
    }

getNFSyms :: Solver -> IO Int
getNFSyms :: Solver -> IO FSym
getNFSyms Solver
solver = UVec FSym -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> UVec FSym
svRepresentativeTable Solver
solver)

newFSym :: Solver -> IO FSym
newFSym :: Solver -> IO FSym
newFSym Solver
solver = do
  FSym
v <- Solver -> IO FSym
getNFSyms Solver
solver
  UVec FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
v
  Vec Class -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec Class
svClassList Solver
solver) (FSym -> Class
ClassSingleton FSym
v)
  IORef (IntMap [(Eqn1, FSym, FSym)])
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) (FSym
-> [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
v [])
  UVec FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svERepresentativeTable Solver
solver) FSym
v
  Vec Class -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec Class
svEClassList Solver
solver) Class
forall a. HasCallStack => a
undefined
  UVec FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svEHighestNodeTable Solver
solver) FSym
v
  FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
v

class VAFun a where
  withVArgs :: ([Term] -> Term) -> a

instance VAFun Term where
  withVArgs :: ([Term] -> Term) -> Term
withVArgs [Term] -> Term
k = [Term] -> Term
k []

instance VAFun a => VAFun (Term -> a) where
  withVArgs :: ([Term] -> Term) -> Term -> a
withVArgs [Term] -> Term
k Term
x = ([Term] -> Term) -> a
forall a. VAFun a => ([Term] -> Term) -> a
withVArgs (\[Term]
xs -> [Term] -> Term
k (Term
x Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
xs))

newFun :: VAFun a => Solver -> IO a
newFun :: forall a. VAFun a => Solver -> IO a
newFun Solver
solver = do
  FSym
c <- Solver -> IO FSym
newFSym Solver
solver
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> IO a) -> a -> IO a
forall a b. (a -> b) -> a -> b
$ ([Term] -> Term) -> a
forall a. VAFun a => ([Term] -> Term) -> a
withVArgs (FSym -> [Term] -> Term
TApp FSym
c)

newConst :: Solver -> IO Term
newConst :: Solver -> IO Term
newConst = Solver -> IO Term
forall a. VAFun a => Solver -> IO a
newFun

merge :: Solver -> Term -> Term -> IO ()
merge :: Solver -> Term -> Term -> IO ()
merge Solver
solver Term
t Term
u = Solver -> Term -> Term -> Maybe FSym -> IO ()
merge' Solver
solver Term
t Term
u Maybe FSym
forall a. Maybe a
Nothing

merge' :: Solver -> Term -> Term -> Maybe ConstrID -> IO ()
merge' :: Solver -> Term -> Term -> Maybe FSym -> IO ()
merge' Solver
solver Term
t Term
u Maybe FSym
cid = do
  FlatTerm
t' <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t
  FlatTerm
u' <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
u
  case (FlatTerm
t', FlatTerm
u') of
    (FTConst FSym
c, FlatTerm
_) -> Solver -> FlatTerm -> FSym -> Maybe FSym -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
u' FSym
c Maybe FSym
cid
    (FlatTerm
_, FTConst FSym
c) -> Solver -> FlatTerm -> FSym -> Maybe FSym -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
t' FSym
c Maybe FSym
cid
    (FlatTerm, FlatTerm)
_ -> do
      FSym
c <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
u'
      Solver -> FlatTerm -> FSym -> Maybe FSym -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
t' FSym
c Maybe FSym
cid

mergeFlatTerm :: Solver -> FlatTerm -> FSym -> IO ()
mergeFlatTerm :: Solver -> FlatTerm -> FSym -> IO ()
mergeFlatTerm Solver
solver FlatTerm
s FSym
a = Solver -> FlatTerm -> FSym -> Maybe FSym -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
s FSym
a Maybe FSym
forall a. Maybe a
Nothing

mergeFlatTerm' :: Solver -> FlatTerm -> FSym -> Maybe ConstrID -> IO ()
mergeFlatTerm' :: Solver -> FlatTerm -> FSym -> Maybe FSym -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
s FSym
a Maybe FSym
cid = do
  Solver -> IO ()
initAfterBacktracking Solver
solver
  case FlatTerm
s of
    FTConst FSym
c -> do
      let eq1 :: Eqn0
eq1 = Maybe FSym -> FSym -> FSym -> Eqn0
Eqn0 Maybe FSym
cid FSym
c FSym
a
      Solver -> Eqn -> IO ()
addToPending Solver
solver (Eqn0 -> Eqn
forall a b. a -> Either a b
Left Eqn0
eq1)
      Solver -> IO ()
propagate Solver
solver
      Solver -> IO ()
checkInvariant Solver
solver
    FTApp FSym
a1 FSym
a2 -> do
      let eq1 :: Eqn1
eq1 = Maybe FSym -> FSym -> FSym -> FSym -> Eqn1
Eqn1 Maybe FSym
cid FSym
a1 FSym
a2 FSym
a
      FSym
a1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a1
      FSym
a2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a2
      Maybe Eqn1
ret <- Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup Solver
solver FSym
a1' FSym
a2'
      case Maybe Eqn1
ret of
        Just Eqn1
eq2 -> do
          Solver -> Eqn -> IO ()
addToPending Solver
solver (Eqn -> IO ()) -> Eqn -> IO ()
forall a b. (a -> b) -> a -> b
$ (Eqn1, Eqn1) -> Eqn
forall a b. b -> Either a b
Right (Eqn1
eq1, Eqn1
eq2)
          Solver -> IO ()
propagate Solver
solver
          Solver -> IO ()
checkInvariant Solver
solver
        Maybe Eqn1
Nothing -> do
          Solver -> FSym -> FSym -> Eqn1 -> IO ()
setLookup Solver
solver FSym
a1' FSym
a2' Eqn1
eq1
          FSym
lv <- Solver -> IO FSym
getCurrentLevel Solver
solver
          FSym
gen <- Solver -> FSym -> IO FSym
getLevelGen Solver
solver FSym
lv
          IORef (IntMap [(Eqn1, FSym, FSym)])
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) ((IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
 -> IO ())
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a b. (a -> b) -> a -> b
$
            ([(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)])
-> FSym
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
gen) (Eqn1, FSym, FSym) -> [(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)]
forall a. a -> [a] -> [a]
:) FSym
a1' (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            ([(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)])
-> FSym
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
gen) (Eqn1, FSym, FSym) -> [(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)]
forall a. a -> [a] -> [a]
:) FSym
a2'
          Solver -> IO ()
checkInvariant Solver
solver

propagate :: Solver -> IO ()
propagate :: Solver -> IO ()
propagate Solver
solver = IO ()
go
  where
    go :: IO ()
go = do
      Solver -> IO ()
checkInvariant Solver
solver
      FSym
n <- Vec Eqn -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> Vec Eqn
svPending Solver
solver)
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
n FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Eqn -> IO ()
processEqn (Eqn -> IO ()) -> IO Eqn -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Vec Eqn -> IO Eqn
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec Eqn
svPending Solver
solver)
        IO ()
go

    processEqn :: Eqn -> IO ()
processEqn Eqn
p = do
      let (FSym
a,FSym
b) = case Eqn
p of
                    Left (Eqn0 Maybe FSym
_ FSym
a FSym
b) -> (FSym
a,FSym
b)
                    Right (Eqn1 Maybe FSym
_ FSym
_ FSym
_ FSym
a, Eqn1 Maybe FSym
_ FSym
_ FSym
_ FSym
b) -> (FSym
a,FSym
b)
      FSym
a' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a
      FSym
b' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Class
classA <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) FSym
a'
        Class
classB <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) FSym
b'
        (FSym
a,FSym
b,FSym
a',FSym
b',Class
classA,Class
classB) <- (FSym, FSym, FSym, FSym, Class, Class)
-> IO (FSym, FSym, FSym, FSym, Class, Class)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((FSym, FSym, FSym, FSym, Class, Class)
 -> IO (FSym, FSym, FSym, FSym, Class, Class))
-> (FSym, FSym, FSym, FSym, Class, Class)
-> IO (FSym, FSym, FSym, FSym, Class, Class)
forall a b. (a -> b) -> a -> b
$
          if Class -> FSym
classSize Class
classA FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
< Class -> FSym
classSize Class
classB then
            (FSym
a,FSym
b,FSym
a',FSym
b',Class
classA,Class
classB)
          else
            (FSym
b,FSym
a,FSym
b',FSym
a',Class
classB,Class
classA)
        FSym
origRootA <- FSym -> FSym -> Eqn -> IO FSym
updateParent FSym
a FSym
b Eqn
p
        FSym -> FSym -> Class -> Class -> IO ()
update FSym
a' FSym
b' Class
classA Class
classB
        Solver -> TrailItem -> IO ()
addToTrail Solver
solver (FSym -> FSym -> FSym -> FSym -> TrailItem
TrailMerge FSym
a' FSym
b' FSym
a FSym
origRootA)

    update :: FSym -> FSym -> Class -> Class -> IO ()
update FSym
a' FSym
b' Class
classA Class
classB = do
      Class -> (FSym -> IO ()) -> IO ()
forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
classA ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
        UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
c FSym
b'
      Vec Class -> FSym -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> Vec Class
svClassList Solver
solver) FSym
b' (Class
classA Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> Class
classB)

      FSym
lv <- Solver -> IO FSym
getCurrentLevel Solver
solver
      FSym
lv_gen <- Solver -> FSym -> IO FSym
getLevelGen Solver
solver FSym
lv
      IntMap [(Eqn1, FSym, FSym)]
useList <- IORef (IntMap [(Eqn1, FSym, FSym)])
-> IO (IntMap [(Eqn1, FSym, FSym)])
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver)
      [(Eqn1, FSym, FSym)]
useList_a' <- (((Eqn1, FSym, FSym) -> IO Bool)
 -> [(Eqn1, FSym, FSym)] -> IO [(Eqn1, FSym, FSym)])
-> [(Eqn1, FSym, FSym)]
-> ((Eqn1, FSym, FSym) -> IO Bool)
-> IO [(Eqn1, FSym, FSym)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Eqn1, FSym, FSym) -> IO Bool)
-> [(Eqn1, FSym, FSym)] -> IO [(Eqn1, FSym, FSym)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IntMap [(Eqn1, FSym, FSym)]
useList IntMap [(Eqn1, FSym, FSym)] -> FSym -> [(Eqn1, FSym, FSym)]
forall a. IntMap a -> FSym -> a
IntMap.! FSym
a') (((Eqn1, FSym, FSym) -> IO Bool) -> IO [(Eqn1, FSym, FSym)])
-> ((Eqn1, FSym, FSym) -> IO Bool) -> IO [(Eqn1, FSym, FSym)]
forall a b. (a -> b) -> a -> b
$ \(eq1 :: Eqn1
eq1@(Eqn1 Maybe FSym
_ FSym
c1 FSym
c2 FSym
_), FSym
lv2, FSym
lv2_gen2) -> do
        FSym
lv2_gen <- Solver -> FSym -> IO FSym
getLevelGen Solver
solver FSym
lv2
        if FSym
lv2 FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
<= FSym
lv Bool -> Bool -> Bool
&& FSym
lv2_gen2 FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
lv2_gen then do
          FSym
c1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
c1
          FSym
c2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
c2
          Bool -> IO () -> IO ()
forall a. HasCallStack => Bool -> a -> a
assert (FSym
b' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
c1' Bool -> Bool -> Bool
|| FSym
b' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
c2') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          -- unless (b' == c1' || b' == c2') $ error "ToySolver.EUF.CongruenceClosure.propagate.update: should not happen"
          Maybe Eqn1
ret <- Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup Solver
solver FSym
c1' FSym
c2'
          case Maybe Eqn1
ret of
            Just Eqn1
eq2 -> do
              Solver -> Eqn -> IO ()
addToPending Solver
solver (Eqn -> IO ()) -> Eqn -> IO ()
forall a b. (a -> b) -> a -> b
$ (Eqn1, Eqn1) -> Eqn
forall a b. b -> Either a b
Right (Eqn1
eq1, Eqn1
eq2)
            Maybe Eqn1
Nothing -> do
              Solver -> FSym -> FSym -> Eqn1 -> IO ()
setLookup Solver
solver FSym
c1' FSym
c2' Eqn1
eq1
              IORef (IntMap [(Eqn1, FSym, FSym)])
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) ((IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
 -> IO ())
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a b. (a -> b) -> a -> b
$ ([(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)])
-> FSym
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
lv_gen) (Eqn1, FSym, FSym) -> [(Eqn1, FSym, FSym)] -> [(Eqn1, FSym, FSym)]
forall a. a -> [a] -> [a]
:) FSym
b'
              () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else do
          -- out-of-date entry
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      IORef (IntMap [(Eqn1, FSym, FSym)])
-> (IntMap [(Eqn1, FSym, FSym)] -> IntMap [(Eqn1, FSym, FSym)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) (FSym
-> [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
-> IntMap [(Eqn1, FSym, FSym)]
forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
a' [(Eqn1, FSym, FSym)]
useList_a')

    -- Insert edge a→b labelled with a_eq_b into the proof forest, and re-orient its original ancestors.
    updateParent :: FSym -> FSym -> Eqn -> IO FSym
updateParent FSym
a FSym
b Eqn
a_eq_b = do
      let loop :: FSym -> (FSym, Eqn) -> IO FSym
loop FSym
d (FSym
c, Eqn
c_eq_d) = do
            IntMap (FSym, Eqn)
tbl <- IORef (IntMap (FSym, Eqn)) -> IO (IntMap (FSym, Eqn))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver)
            IORef (IntMap (FSym, Eqn)) -> IntMap (FSym, Eqn) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver) (FSym -> (FSym, Eqn) -> IntMap (FSym, Eqn) -> IntMap (FSym, Eqn)
forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
d (FSym
c, Eqn
c_eq_d) IntMap (FSym, Eqn)
tbl)
            case FSym -> IntMap (FSym, Eqn) -> Maybe (FSym, Eqn)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
d IntMap (FSym, Eqn)
tbl of
              Maybe (FSym, Eqn)
Nothing -> FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
d
              Just (FSym
e, Eqn
d_eq_e) -> FSym -> (FSym, Eqn) -> IO FSym
loop FSym
e (FSym
d, Eqn
d_eq_e)
      FSym -> (FSym, Eqn) -> IO FSym
loop FSym
a (FSym
b, Eqn
a_eq_b)

areCongruent :: Solver -> Term -> Term -> IO Bool
areCongruent :: Solver -> Term -> Term -> IO Bool
areCongruent Solver
solver Term
t1 Term
t2 = do
  FlatTerm
u1 <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t1
  FlatTerm
u2 <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t2
  Solver -> FlatTerm -> FlatTerm -> IO Bool
areCongruentFlatTerm Solver
solver FlatTerm
u1 FlatTerm
u2

areCongruentFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO Bool
areCongruentFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO Bool
areCongruentFlatTerm Solver
solver FlatTerm
t1 FlatTerm
t2 = do
  Solver -> IO ()
initAfterBacktracking Solver
solver
  FlatTerm
u1 <- Solver -> FlatTerm -> IO FlatTerm
normalize Solver
solver FlatTerm
t1
  FlatTerm
u2 <- Solver -> FlatTerm -> IO FlatTerm
normalize Solver
solver FlatTerm
t2
  Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ FlatTerm
u1 FlatTerm -> FlatTerm -> Bool
forall a. Eq a => a -> a -> Bool
== FlatTerm
u2

normalize :: Solver -> FlatTerm -> IO FlatTerm
normalize :: Solver -> FlatTerm -> IO FlatTerm
normalize Solver
solver (FTConst FSym
c) = (FSym -> FlatTerm) -> IO FSym -> IO FlatTerm
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FSym -> FlatTerm
FTConst (IO FSym -> IO FlatTerm) -> IO FSym -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
c
normalize Solver
solver (FTApp FSym
t1 FSym
t2) = do
  FSym
u1 <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
t1
  FSym
u2 <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
t2
  Maybe Eqn1
ret <- Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup Solver
solver FSym
u1 FSym
u2
  case Maybe Eqn1
ret of
    Just (Eqn1 Maybe FSym
_ FSym
_ FSym
_ FSym
a) -> (FSym -> FlatTerm) -> IO FSym -> IO FlatTerm
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FSym -> FlatTerm
FTConst (IO FSym -> IO FlatTerm) -> IO FSym -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a
    Maybe Eqn1
Nothing -> FlatTerm -> IO FlatTerm
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FlatTerm -> IO FlatTerm) -> FlatTerm -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ FSym -> FSym -> FlatTerm
FTApp FSym
u1 FSym
u2

checkInvariant :: Solver -> IO ()
checkInvariant :: Solver -> IO ()
checkInvariant Solver
_ | Bool
True = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkInvariant Solver
solver = do
  FSym
nv <- Solver -> IO FSym
getNFSyms Solver
solver

  IntSet
representatives <- ([FSym] -> IntSet) -> IO [FSym] -> IO IntSet
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [FSym] -> IntSet
IntSet.fromList (IO [FSym] -> IO IntSet) -> IO [FSym] -> IO IntSet
forall a b. (a -> b) -> a -> b
$ UVec FSym -> IO [FSym]
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO [e]
Vec.getElems (Solver -> UVec FSym
svRepresentativeTable Solver
solver)

  IORef IntSet
ref <- IntSet -> IO (IORef IntSet)
forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty
  [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
a' -> do
    Class
bs <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.read (Solver -> Vec Class
svClassList Solver
solver) FSym
a'
    [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Class -> [FSym]
classToList Class
bs) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
b -> do
      FSym
b' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.EUF.CongruenceClosure.checkInvariant: inconsistency between classList and representativeTable"
      IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
ref (FSym -> IntSet -> IntSet
IntSet.insert FSym
b)

  IntSet
xs <- IORef IntSet -> IO IntSet
forall a. IORef a -> IO a
readIORef IORef IntSet
ref
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IntSet
xs IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== [FSym] -> IntSet
IntSet.fromList [FSym
0..FSym
nvFSym -> FSym -> FSym
forall a. Num a => a -> a -> a
-FSym
1]) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.EUF.CongruenceClosure.checkInvariant: classList is not exhaustive"

  [Eqn]
pendings <- Vec Eqn -> IO [Eqn]
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO [e]
Vec.getElems (Solver -> Vec Eqn
svPending Solver
solver)
  [Eqn] -> (Eqn -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Eqn]
pendings ((Eqn -> IO ()) -> IO ()) -> (Eqn -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Eqn
p -> do
    case Eqn
p of
      Left Eqn0
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Right (Eqn1 Maybe FSym
_ FSym
a1 FSym
a2 FSym
_, Eqn1 Maybe FSym
_ FSym
b1 FSym
b2 FSym
_) -> do
        FSym
a1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a1
        FSym
a2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a2
        FSym
b1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b1
        FSym
b2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b2
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a1' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b1' Bool -> Bool -> Bool
&& FSym
a2' FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b2') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
          String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.EUF.CongruenceClosure.checkInvariant: error in pendingList"

  IntMap [(Eqn1, FSym, FSym)]
useList <- IORef (IntMap [(Eqn1, FSym, FSym)])
-> IO (IntMap [(Eqn1, FSym, FSym)])
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver)
  FSym
lv <- Solver -> IO FSym
getCurrentLevel Solver
solver
  [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    [(Eqn1, FSym, FSym)] -> ((Eqn1, FSym, FSym) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap [(Eqn1, FSym, FSym)]
useList IntMap [(Eqn1, FSym, FSym)] -> FSym -> [(Eqn1, FSym, FSym)]
forall a. IntMap a -> FSym -> a
IntMap.! FSym
a) (((Eqn1, FSym, FSym) -> IO ()) -> IO ())
-> ((Eqn1, FSym, FSym) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Eqn1 Maybe FSym
_ FSym
b1 FSym
b2 FSym
_, FSym
lv2, FSym
lv2_gen2) -> do
      FSym
lv2_gen <- Solver -> FSym -> IO FSym
getLevelGen Solver
solver FSym
lv2
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
lv2 FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
<= FSym
lv Bool -> Bool -> Bool
&& FSym
lv2_gen2 FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
lv2_gen) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        FSym
b1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b1
        FSym
b2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
b2
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b1' Bool -> Bool -> Bool
|| FSym
a FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
b2') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
          String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.EUF.CongruenceClosure.checkInvariant: error in useList"

  [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
b -> do
    [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
      Maybe Eqn1
m <- Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup Solver
solver FSym
b FSym
c
      case Maybe Eqn1
m of
        Maybe Eqn1
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just (Eqn1 Maybe FSym
_ FSym
a1 FSym
a2 FSym
_) -> do
          FSym
a1' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a1
          FSym
a2' <- Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a2
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
b FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
a1' Bool -> Bool -> Bool
&& FSym
c FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
a2') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
            String -> IO ()
forall a. HasCallStack => String -> a
error String
"ToySolver.EUF.CongruenceClosure.checkInvariant: error in lookupTable"

-- -------------------------------------------------------------------
-- Explanation
-- -------------------------------------------------------------------

explain :: Solver -> Term -> Term -> IO (Maybe IntSet)
explain :: Solver -> Term -> Term -> IO (Maybe IntSet)
explain Solver
solver Term
t1 Term
t2 = do
  FlatTerm
c1 <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t1
  FlatTerm
c2 <- Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t2
  Solver -> FlatTerm -> FlatTerm -> IO (Maybe IntSet)
explainFlatTerm Solver
solver FlatTerm
c1 FlatTerm
c2

explainFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO (Maybe IntSet)
explainFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO (Maybe IntSet)
explainFlatTerm Solver
solver FlatTerm
t1 FlatTerm
t2 = do
  FSym
c1 <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
t1
  FSym
c2 <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
t2
  Solver -> FSym -> FSym -> IO (Maybe IntSet)
explainConst Solver
solver FSym
c1 FSym
c2

explainConst :: Solver -> FSym -> FSym -> IO (Maybe IntSet)
explainConst :: Solver -> FSym -> FSym -> IO (Maybe IntSet)
explainConst Solver
solver FSym
c1 FSym
c2 = do
  Solver -> IO ()
initAfterBacktracking Solver
solver
  FSym
n <- Solver -> IO FSym
getNFSyms Solver
solver

  -- Additional union-find data structure
  FSym
-> (FSym -> Bool) -> (FSym -> FSym) -> (FSym -> IO ()) -> IO ()
forall (m :: * -> *) a.
Monad m =>
a -> (a -> Bool) -> (a -> a) -> (a -> m ()) -> m ()
forLoop FSym
0 (FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
<FSym
n) (FSym -> FSym -> FSym
forall a. Num a => a -> a -> a
+FSym
1) ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svERepresentativeTable Solver
solver) FSym
a FSym
a
    Vec Class -> FSym -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> Vec Class
svEClassList Solver
solver) FSym
a (FSym -> Class
ClassSingleton FSym
a)
    UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svEHighestNodeTable Solver
solver) FSym
a FSym
a

  let union :: FSym -> FSym -> IO ()
      union :: FSym -> FSym -> IO ()
union FSym
a FSym
b = do
        FSym
a' <- Solver -> FSym -> IO FSym
getERepresentative Solver
solver FSym
a
        FSym
b' <- Solver -> FSym -> IO FSym
getERepresentative Solver
solver FSym
b
        Class
classA <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svEClassList Solver
solver) FSym
a'
        Class
classB <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svEClassList Solver
solver) FSym
b'
        FSym
h <- Solver -> FSym -> IO FSym
getHighestNode Solver
solver FSym
b'
        (FSym
b'', Class
classA, Class
classB) <-
          if Class -> FSym
classSize Class
classA FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
< Class -> FSym
classSize Class
classB then do
            (FSym, Class, Class) -> IO (FSym, Class, Class)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym
b', Class
classA, Class
classB)
          else
            (FSym, Class, Class) -> IO (FSym, Class, Class)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym
a', Class
classB, Class
classA)
        Class -> (FSym -> IO ()) -> IO ()
forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
classA ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
          UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svERepresentativeTable Solver
solver) FSym
c FSym
b''
        Vec Class -> FSym -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> Vec Class
svEClassList Solver
solver) FSym
b'' (Class
classA Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> Class
classB)
        UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svEHighestNodeTable Solver
solver) FSym
b'' FSym
h

  Vec (FSym, FSym) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver)
  Vec (FSym, FSym) -> (FSym, FSym) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver) (FSym
c1,FSym
c2)
  IORef IntSet
result <- IntSet -> IO (IORef IntSet)
forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty

  let loop :: IO Bool
loop = do
        FSym
n <- Vec (FSym, FSym) -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver)
        if FSym
n FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
0 then
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else do
          (FSym
a,FSym
b) <- Vec (FSym, FSym) -> IO (FSym, FSym)
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver)
          Maybe FSym
m <- Solver -> FSym -> FSym -> IO (Maybe FSym)
nearestCommonAncestor Solver
solver FSym
a FSym
b
          case Maybe FSym
m of
            Maybe FSym
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Just FSym
c -> do
              FSym -> FSym -> IO ()
explainAlongPath FSym
a FSym
c
              FSym -> FSym -> IO ()
explainAlongPath FSym
b FSym
c
              IO Bool
loop

      explainAlongPath :: FSym -> FSym -> IO ()
      explainAlongPath :: FSym -> FSym -> IO ()
explainAlongPath FSym
a FSym
c = do
        FSym
a <- Solver -> FSym -> IO FSym
getHighestNode Solver
solver FSym
a
        -- note that c is already @getHighestNode solver c@
        let loop :: FSym -> IO ()
loop FSym
a =
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
c) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                Just (FSym
b, Eqn
eq) <- Solver -> FSym -> IO (Maybe (FSym, Eqn))
getParent Solver
solver FSym
a
                case Eqn
eq of
                  Left (Eqn0 Maybe FSym
cid FSym
_ FSym
_) -> do
                    IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result (Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<>)
                  Right (Eqn1 Maybe FSym
cid1 FSym
a1 FSym
a2 FSym
_, Eqn1 Maybe FSym
cid2 FSym
b1 FSym
b2 FSym
_) -> do
                    IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result ((Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid1 IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid2) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<>)
                    Vec (FSym, FSym) -> (FSym, FSym) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver) (FSym
a1,FSym
b1)
                    Vec (FSym, FSym) -> (FSym, FSym) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver) (FSym
a2,FSym
b2)
                FSym -> FSym -> IO ()
union FSym
a FSym
b
                FSym -> IO ()
loop (FSym -> IO ()) -> IO FSym -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> FSym -> IO FSym
getHighestNode Solver
solver FSym
b
        FSym -> IO ()
loop FSym
a

  Bool
b <- IO Bool
loop
  if Bool
b
  then (IntSet -> Maybe IntSet) -> IO IntSet -> IO (Maybe IntSet)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> Maybe IntSet
forall a. a -> Maybe a
Just (IO IntSet -> IO (Maybe IntSet)) -> IO IntSet -> IO (Maybe IntSet)
forall a b. (a -> b) -> a -> b
$ IORef IntSet -> IO IntSet
forall a. IORef a -> IO a
readIORef IORef IntSet
result
  else Maybe IntSet -> IO (Maybe IntSet)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe IntSet
forall a. Maybe a
Nothing

-- -------------------------------------------------------------------
-- Model construction
-- -------------------------------------------------------------------

type Entity = Int
type EntityTuple = [Entity]

data Model
  = Model
  { Model -> IntSet
mUniverse    :: !IntSet
  , Model -> IntMap (Map [FSym] FSym)
mFunctions   :: !(IntMap (Map EntityTuple Entity))
  , Model -> FSym
mUnspecified :: !Entity
  , Model -> [(Set Term, FSym)]
mEquivClasses :: [(Set Term, Entity)]
  }
  deriving (FSym -> Model -> ShowS
[Model] -> ShowS
Model -> String
(FSym -> Model -> ShowS)
-> (Model -> String) -> ([Model] -> ShowS) -> Show Model
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> Model -> ShowS
showsPrec :: FSym -> Model -> ShowS
$cshow :: Model -> String
show :: Model -> String
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show)

getModel :: Solver -> IO Model
getModel :: Solver -> IO Model
getModel Solver
solver = do
  FSym
n <- UVec FSym -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> UVec FSym
svRepresentativeTable Solver
solver)
  IORef IntSet
univRef <- IntSet -> IO (IORef IntSet)
forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty
  IORef (IntMap FSym)
reprRef <- IntMap FSym -> IO (IORef (IntMap FSym))
forall a. a -> IO (IORef a)
newIORef IntMap FSym
forall a. IntMap a
IntMap.empty
  [FSym] -> (FSym -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [FSym
0..FSym
nFSym -> FSym -> FSym
forall a. Num a => a -> a -> a
-FSym
1] ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    FSym
a' <- UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
a
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
a FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
a') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
univRef (FSym -> IntSet -> IntSet
IntSet.insert FSym
a)
    IORef (IntMap FSym) -> (IntMap FSym -> IntMap FSym) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (IntMap FSym)
reprRef (FSym -> FSym -> IntMap FSym -> IntMap FSym
forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
a FSym
a')
  -- univ <- readIORef univRef
  IntMap FSym
repr <- IORef (IntMap FSym) -> IO (IntMap FSym)
forall a. IORef a -> IO a
readIORef IORef (IntMap FSym)
reprRef

  IntMap (IntMap Eqn1)
lookups <- IORef (IntMap (IntMap Eqn1)) -> IO (IntMap (IntMap Eqn1))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver)
  -- (defs1,_) <- readIORef (svDefs solver)

  let -- "(b,c) ∈ appRel[a]" means f(b,c)=a
      appRel :: IntMap (Set (FSym, FSym))
      appRel :: IntMap (Set (FSym, FSym))
appRel = (Set (FSym, FSym) -> Set (FSym, FSym) -> Set (FSym, FSym))
-> [(FSym, Set (FSym, FSym))] -> IntMap (Set (FSym, FSym))
forall a. (a -> a -> a) -> [(FSym, a)] -> IntMap a
IntMap.fromListWith Set (FSym, FSym) -> Set (FSym, FSym) -> Set (FSym, FSym)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([(FSym, Set (FSym, FSym))] -> IntMap (Set (FSym, FSym)))
-> [(FSym, Set (FSym, FSym))] -> IntMap (Set (FSym, FSym))
forall a b. (a -> b) -> a -> b
$
        [ (IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
c, (FSym, FSym) -> Set (FSym, FSym)
forall a. a -> Set a
Set.singleton (IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
a, IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
b))
        | (FSym
a,IntMap Eqn1
m) <- IntMap (IntMap Eqn1) -> [(FSym, IntMap Eqn1)]
forall a. IntMap a -> [(FSym, a)]
IntMap.toList IntMap (IntMap Eqn1)
lookups, (FSym
b, Eqn1 Maybe FSym
_ FSym
_ FSym
_ FSym
c) <- IntMap Eqn1 -> [(FSym, Eqn1)]
forall a. IntMap a -> [(FSym, a)]
IntMap.toList IntMap Eqn1
m
        ]

      partialApps :: IntSet
      partialApps :: IntSet
partialApps = [FSym] -> IntSet
IntSet.fromList [FSym
b | Set (FSym, FSym)
xs <- IntMap (Set (FSym, FSym)) -> [Set (FSym, FSym)]
forall a. IntMap a -> [a]
IntMap.elems IntMap (Set (FSym, FSym))
appRel, (FSym
b,FSym
_) <- Set (FSym, FSym) -> [(FSym, FSym)]
forall a. Set a -> [a]
Set.toList Set (FSym, FSym)
xs]

      xs1 :: IntMap (Map EntityTuple Entity)
      xs1 :: IntMap (Map [FSym] FSym)
xs1 = (Map [FSym] FSym -> Map [FSym] FSym -> Map [FSym] FSym)
-> [(FSym, Map [FSym] FSym)] -> IntMap (Map [FSym] FSym)
forall a. (a -> a -> a) -> [(FSym, a)] -> IntMap a
IntMap.fromListWith Map [FSym] FSym -> Map [FSym] FSym -> Map [FSym] FSym
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(FSym, Map [FSym] FSym)] -> IntMap (Map [FSym] FSym))
-> [(FSym, Map [FSym] FSym)] -> IntMap (Map [FSym] FSym)
forall a b. (a -> b) -> a -> b
$
              [ (FSym
f, [FSym] -> FSym -> Map [FSym] FSym
forall k a. k -> a -> Map k a
Map.singleton ([FSym] -> [FSym]
forall a. [a] -> [a]
reverse [FSym]
argsRev) (IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
a))
              | FSym
a <- IntMap (Set (FSym, FSym)) -> [FSym]
forall a. IntMap a -> [FSym]
IntMap.keys (IntMap (Set (FSym, FSym)) -> IntSet -> IntMap (Set (FSym, FSym))
forall a. IntMap a -> IntSet -> IntMap a
IntMap.withoutKeys IntMap (Set (FSym, FSym))
appRel IntSet
partialApps)
              , (FSym
f, [FSym]
argsRev) <- FSym -> [(FSym, [FSym])]
expand FSym
a
              ]
        where
          expand :: FSym -> [(FSym, [FSym])]
          expand :: FSym -> [(FSym, [FSym])]
expand FSym
a =
            case FSym -> IntMap (Set (FSym, FSym)) -> Maybe (Set (FSym, FSym))
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
a IntMap (Set (FSym, FSym))
appRel of
              Maybe (Set (FSym, FSym))
Nothing -> (FSym, [FSym]) -> [(FSym, [FSym])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
a, [])
              Just Set (FSym, FSym)
xs -> do
                (FSym
c,FSym
d) <- Set (FSym, FSym) -> [(FSym, FSym)]
forall a. Set a -> [a]
Set.toList Set (FSym, FSym)
xs
                (FSym
f,[FSym]
xs) <- FSym -> [(FSym, [FSym])]
expand FSym
c
                (FSym, [FSym]) -> [(FSym, [FSym])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym
f, IntMap FSym
repr IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.! FSym
d FSym -> [FSym] -> [FSym]
forall a. a -> [a] -> [a]
: [FSym]
xs)

      xs2 :: IntMap (Map EntityTuple Entity)
      xs2 :: IntMap (Map [FSym] FSym)
xs2 = (FSym -> Map [FSym] FSym)
-> IntMap FSym -> IntMap (Map [FSym] FSym)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([FSym] -> FSym -> Map [FSym] FSym
forall k a. k -> a -> Map k a
Map.singleton []) (IntMap FSym
repr IntMap FSym -> IntMap (Map [FSym] FSym) -> IntMap FSym
forall a b. IntMap a -> IntMap b -> IntMap a
`IntMap.difference` IntMap (Map [FSym] FSym)
xs1)

      funcs :: IntMap (Map EntityTuple Entity)
      funcs :: IntMap (Map [FSym] FSym)
funcs = (Map [FSym] FSym -> Map [FSym] FSym -> Map [FSym] FSym)
-> IntMap (Map [FSym] FSym)
-> IntMap (Map [FSym] FSym)
-> IntMap (Map [FSym] FSym)
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith Map [FSym] FSym -> Map [FSym] FSym -> Map [FSym] FSym
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union IntMap (Map [FSym] FSym)
xs1 IntMap (Map [FSym] FSym)
xs2

      used :: IntSet
      used :: IntSet
used = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [[FSym] -> IntSet
IntSet.fromList (FSym
y FSym -> [FSym] -> [FSym]
forall a. a -> [a] -> [a]
: [FSym]
xs) | Map [FSym] FSym
m <- IntMap (Map [FSym] FSym) -> [Map [FSym] FSym]
forall a. IntMap a -> [a]
IntMap.elems IntMap (Map [FSym] FSym)
funcs, ([FSym]
xs,FSym
y) <- Map [FSym] FSym -> [([FSym], FSym)]
forall k a. Map k a -> [(k, a)]
Map.toList Map [FSym] FSym
m]

  [(Set Term, FSym)]
classes <- [FSym] -> (FSym -> IO (Set Term, FSym)) -> IO [(Set Term, FSym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (IntSet -> [FSym]
IntSet.toList IntSet
used) ((FSym -> IO (Set Term, FSym)) -> IO [(Set Term, FSym)])
-> (FSym -> IO (Set Term, FSym)) -> IO [(Set Term, FSym)]
forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    Class
classA <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) FSym
a
    Set Term
classA' <- ([Term] -> Set Term) -> IO [Term] -> IO (Set Term)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Term] -> Set Term
forall a. Ord a => [a] -> Set a
Set.fromList (IO [Term] -> IO (Set Term)) -> IO [Term] -> IO (Set Term)
forall a b. (a -> b) -> a -> b
$ (FSym -> IO Term) -> [FSym] -> IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Solver -> FSym -> IO Term
fsymToTerm Solver
solver) (Class -> [FSym]
classToList Class
classA)
    (Set Term, FSym) -> IO (Set Term, FSym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Term
classA', FSym
a)

  -- renaming
  let univ2 :: IntSet
      univ2 :: IntSet
univ2 = FSym -> IntSet -> IntSet
IntSet.insert (-FSym
1) (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$ [FSym] -> IntSet
IntSet.fromList [FSym
0 .. IntSet -> FSym
IntSet.size IntSet
used FSym -> FSym -> FSym
forall a. Num a => a -> a -> a
- FSym
1]

      to_univ2' :: IntMap Entity
      to_univ2' :: IntMap FSym
to_univ2' = [(FSym, FSym)] -> IntMap FSym
forall a. [(FSym, a)] -> IntMap a
IntMap.fromList ([FSym] -> [FSym] -> [(FSym, FSym)]
forall a b. [a] -> [b] -> [(a, b)]
zip (IntSet -> [FSym]
IntSet.toList IntSet
used) [FSym
0..])

      to_univ2 :: FSym -> Entity
      to_univ2 :: FSym -> FSym
to_univ2 = (IntMap FSym
to_univ2' IntMap FSym -> FSym -> FSym
forall a. IntMap a -> FSym -> a
IntMap.!)

      funcs2 :: IntMap (Map EntityTuple Entity)
      funcs2 :: IntMap (Map [FSym] FSym)
funcs2 = (Map [FSym] FSym -> Map [FSym] FSym)
-> IntMap (Map [FSym] FSym) -> IntMap (Map [FSym] FSym)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Map [FSym] FSym
m -> [([FSym], FSym)] -> Map [FSym] FSym
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [((FSym -> FSym) -> [FSym] -> [FSym]
forall a b. (a -> b) -> [a] -> [b]
map FSym -> FSym
to_univ2 [FSym]
xs, FSym -> FSym
to_univ2 FSym
y) | ([FSym]
xs,FSym
y) <- Map [FSym] FSym -> [([FSym], FSym)]
forall k a. Map k a -> [(k, a)]
Map.toList Map [FSym] FSym
m]) IntMap (Map [FSym] FSym)
funcs

      classes2 :: [(Set Term, Entity)]
      classes2 :: [(Set Term, FSym)]
classes2 = [(Set Term
classA, FSym -> FSym
to_univ2 FSym
a) | (Set Term
classA,FSym
a) <- [(Set Term, FSym)]
classes]

  Model -> IO Model
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Model -> IO Model) -> Model -> IO Model
forall a b. (a -> b) -> a -> b
$
    Model
    { mUniverse :: IntSet
mUniverse    = IntSet
univ2
    , mFunctions :: IntMap (Map [FSym] FSym)
mFunctions   = IntMap (Map [FSym] FSym)
funcs2
    , mUnspecified :: FSym
mUnspecified = -FSym
1
    , mEquivClasses :: [(Set Term, FSym)]
mEquivClasses = [(Set Term, FSym)]
classes2
    }

eval :: Model -> Term -> Entity
eval :: Model -> Term -> FSym
eval Model
m (TApp FSym
f [Term]
xs) = Model -> FSym -> [FSym] -> FSym
evalAp Model
m FSym
f ((Term -> FSym) -> [Term] -> [FSym]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Term -> FSym
eval Model
m) [Term]
xs)

evalAp :: Model -> FSym -> [Entity] -> Entity
evalAp :: Model -> FSym -> [FSym] -> FSym
evalAp Model
m FSym
f [FSym]
xs =
  case FSym -> IntMap (Map [FSym] FSym) -> Maybe (Map [FSym] FSym)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
f (Model -> IntMap (Map [FSym] FSym)
mFunctions Model
m) of
    Maybe (Map [FSym] FSym)
Nothing -> Model -> FSym
mUnspecified Model
m
    Just Map [FSym] FSym
fdef ->
      case [FSym] -> Map [FSym] FSym -> Maybe FSym
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup [FSym]
xs Map [FSym] FSym
fdef of
        Maybe FSym
Nothing -> Model -> FSym
mUnspecified Model
m
        Just FSym
e -> FSym
e

-- -------------------------------------------------------------------
-- Backtracking
-- -------------------------------------------------------------------

type Level = Int
type Gen = Int

data TrailItem
  = TrailMerge !FSym !FSym !FSym !FSym
  | TrailSetLookup !FSym !FSym
  deriving (FSym -> TrailItem -> ShowS
[TrailItem] -> ShowS
TrailItem -> String
(FSym -> TrailItem -> ShowS)
-> (TrailItem -> String)
-> ([TrailItem] -> ShowS)
-> Show TrailItem
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: FSym -> TrailItem -> ShowS
showsPrec :: FSym -> TrailItem -> ShowS
$cshow :: TrailItem -> String
show :: TrailItem -> String
$cshowList :: [TrailItem] -> ShowS
showList :: [TrailItem] -> ShowS
Show)

addToTrail :: Solver -> TrailItem -> IO ()
addToTrail :: Solver -> TrailItem -> IO ()
addToTrail Solver
solver TrailItem
item = do
  FSym
lv <- Solver -> IO FSym
getCurrentLevel Solver
solver
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
lv FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
/= FSym
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    TrailItem -> IO () -> IO ()
forall a b. a -> b -> b
seq TrailItem
item (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Vec [TrailItem] -> FSym -> ([TrailItem] -> [TrailItem]) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> (e -> e) -> IO ()
Vec.unsafeModify (Solver -> Vec [TrailItem]
svTrail Solver
solver) (FSym
lv FSym -> FSym -> FSym
forall a. Num a => a -> a -> a
- FSym
1) (TrailItem
item TrailItem -> [TrailItem] -> [TrailItem]
forall a. a -> [a] -> [a]
:)

getCurrentLevel :: Solver -> IO Level
getCurrentLevel :: Solver -> IO FSym
getCurrentLevel Solver
solver = Vec [TrailItem] -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> Vec [TrailItem]
svTrail Solver
solver)

getLevelGen :: Solver -> Level -> IO Gen
getLevelGen :: Solver -> FSym -> IO FSym
getLevelGen Solver
solver FSym
lv = UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svLevelGen Solver
solver) FSym
lv

pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint Solver
solver = do
  Vec [TrailItem] -> [TrailItem] -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec [TrailItem]
svTrail Solver
solver) []
  FSym
lv <- Solver -> IO FSym
getCurrentLevel Solver
solver
  FSym
size <- UVec FSym -> IO FSym
forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> UVec FSym
svLevelGen Solver
solver)
  if FSym
lv FSym -> FSym -> Bool
forall a. Ord a => a -> a -> Bool
< FSym
size then do
    FSym
g <- UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svLevelGen Solver
solver) FSym
lv
    UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svLevelGen Solver
solver) FSym
lv (FSym
g FSym -> FSym -> FSym
forall a. Num a => a -> a -> a
+ FSym
1)
  else
    UVec FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svLevelGen Solver
solver) FSym
0

popBacktrackPoint :: Solver -> IO ()
popBacktrackPoint :: Solver -> IO ()
popBacktrackPoint Solver
solver = do
  IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver) Bool
True
  [TrailItem]
xs <- Vec [TrailItem] -> IO [TrailItem]
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec [TrailItem]
svTrail Solver
solver)
  [TrailItem] -> (TrailItem -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TrailItem]
xs ((TrailItem -> IO ()) -> IO ()) -> (TrailItem -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \TrailItem
item -> do
    case TrailItem
item of
      TrailSetLookup FSym
a' FSym
b' -> do
        IORef (IntMap (IntMap Eqn1))
-> (IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver) ((IntMap Eqn1 -> IntMap Eqn1)
-> FSym -> IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)
forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust (FSym -> IntMap Eqn1 -> IntMap Eqn1
forall a. FSym -> IntMap a -> IntMap a
IntMap.delete FSym
b') FSym
a')
      TrailMerge FSym
a' FSym
b' FSym
a FSym
origRootA -> do
        -- Revert changes to Union-Find data strucutres
        ClassUnion FSym
_ Class
origClassA Class
origClassB <- Vec Class -> FSym -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList Solver
solver) FSym
b'
        Class -> (FSym -> IO ()) -> IO ()
forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
origClassA ((FSym -> IO ()) -> IO ()) -> (FSym -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
          UVec FSym -> FSym -> FSym -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
c FSym
a'
        Vec Class -> FSym -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> e -> IO ()
Vec.unsafeWrite (Solver -> Vec Class
svClassList Solver
solver) FSym
b' Class
origClassB

        -- Revert changes to proof-forest data strucutres
        let loop :: FSym -> Maybe (FSym, Eqn) -> IO ()
loop FSym
c Maybe (FSym, Eqn)
p = do
              IntMap (FSym, Eqn)
tbl <- IORef (IntMap (FSym, Eqn)) -> IO (IntMap (FSym, Eqn))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver)
              IORef (IntMap (FSym, Eqn)) -> IntMap (FSym, Eqn) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver) (((FSym, Eqn) -> Maybe (FSym, Eqn))
-> FSym -> IntMap (FSym, Eqn) -> IntMap (FSym, Eqn)
forall a. (a -> Maybe a) -> FSym -> IntMap a -> IntMap a
IntMap.update (Maybe (FSym, Eqn) -> (FSym, Eqn) -> Maybe (FSym, Eqn)
forall a b. a -> b -> a
const Maybe (FSym, Eqn)
p) FSym
c IntMap (FSym, Eqn)
tbl)
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
c FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
a) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                let (FSym
d, Eqn
c_eq_d) = IntMap (FSym, Eqn)
tbl IntMap (FSym, Eqn) -> FSym -> (FSym, Eqn)
forall a. IntMap a -> FSym -> a
IntMap.! FSym
c
                FSym -> Maybe (FSym, Eqn) -> IO ()
loop FSym
d ((FSym, Eqn) -> Maybe (FSym, Eqn)
forall a. a -> Maybe a
Just (FSym
c, Eqn
c_eq_d))
        FSym -> Maybe (FSym, Eqn) -> IO ()
loop FSym
origRootA Maybe (FSym, Eqn)
forall a. Maybe a
Nothing

initAfterBacktracking :: Solver -> IO ()
initAfterBacktracking :: Solver -> IO ()
initAfterBacktracking Solver
solver = do
  Bool
b <- IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    IORef Bool -> Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver) Bool
False
    (IntMap (FSym, FSym)
defs, Map (FSym, FSym) FSym
_) <- IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver)
    [(FSym, (FSym, FSym))] -> ((FSym, (FSym, FSym)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (FSym, FSym) -> [(FSym, (FSym, FSym))]
forall a. IntMap a -> [(FSym, a)]
IntMap.toList IntMap (FSym, FSym)
defs) (((FSym, (FSym, FSym)) -> IO ()) -> IO ())
-> ((FSym, (FSym, FSym)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(FSym
a,(FSym
a1,FSym
a2)) -> do
      Solver -> FlatTerm -> FSym -> IO ()
mergeFlatTerm Solver
solver (FSym -> FSym -> FlatTerm
FTApp FSym
a1 FSym
a2) FSym
a

{--------------------------------------------------------------------
  Helper funcions
--------------------------------------------------------------------}

lookup :: Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup :: Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup Solver
solver FSym
c1 FSym
c2 = do
  IntMap (IntMap Eqn1)
tbl <- IORef (IntMap (IntMap Eqn1)) -> IO (IntMap (IntMap Eqn1))
forall a. IORef a -> IO a
readIORef (IORef (IntMap (IntMap Eqn1)) -> IO (IntMap (IntMap Eqn1)))
-> IORef (IntMap (IntMap Eqn1)) -> IO (IntMap (IntMap Eqn1))
forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver
  Maybe Eqn1 -> IO (Maybe Eqn1)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Eqn1 -> IO (Maybe Eqn1)) -> Maybe Eqn1 -> IO (Maybe Eqn1)
forall a b. (a -> b) -> a -> b
$ do
     IntMap Eqn1
m <- FSym -> IntMap (IntMap Eqn1) -> Maybe (IntMap Eqn1)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
c1 IntMap (IntMap Eqn1)
tbl
     FSym -> IntMap Eqn1 -> Maybe Eqn1
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
c2 IntMap Eqn1
m

setLookup :: Solver -> FSym -> FSym -> Eqn1 -> IO ()
setLookup :: Solver -> FSym -> FSym -> Eqn1 -> IO ()
setLookup Solver
solver FSym
a1 FSym
a2 Eqn1
eqn = do
  IORef (IntMap (IntMap Eqn1))
-> (IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver) ((IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)) -> IO ())
-> (IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)) -> IO ()
forall a b. (a -> b) -> a -> b
$
    (IntMap Eqn1 -> IntMap Eqn1 -> IntMap Eqn1)
-> FSym
-> IntMap Eqn1
-> IntMap (IntMap Eqn1)
-> IntMap (IntMap Eqn1)
forall a. (a -> a -> a) -> FSym -> a -> IntMap a -> IntMap a
IntMap.insertWith IntMap Eqn1 -> IntMap Eqn1 -> IntMap Eqn1
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union FSym
a1 (FSym -> Eqn1 -> IntMap Eqn1
forall a. FSym -> a -> IntMap a
IntMap.singleton FSym
a2 Eqn1
eqn)
  Solver -> TrailItem -> IO ()
addToTrail Solver
solver (FSym -> FSym -> TrailItem
TrailSetLookup FSym
a1 FSym
a2)

addToPending :: Solver -> Eqn -> IO ()
addToPending :: Solver -> Eqn -> IO ()
addToPending Solver
solver Eqn
eqn = Vec Eqn -> Eqn -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec Eqn
svPending Solver
solver) Eqn
eqn

getRepresentative :: Solver -> FSym -> IO FSym
getRepresentative :: Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
c = UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
c

getParent :: Solver -> FSym -> IO (Maybe (FSym, Eqn))
getParent :: Solver -> FSym -> IO (Maybe (FSym, Eqn))
getParent Solver
solver FSym
c = do
  IntMap (FSym, Eqn)
m <- IORef (IntMap (FSym, Eqn)) -> IO (IntMap (FSym, Eqn))
forall a. IORef a -> IO a
readIORef (IORef (IntMap (FSym, Eqn)) -> IO (IntMap (FSym, Eqn)))
-> IORef (IntMap (FSym, Eqn)) -> IO (IntMap (FSym, Eqn))
forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver
  Maybe (FSym, Eqn) -> IO (Maybe (FSym, Eqn))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (FSym, Eqn) -> IO (Maybe (FSym, Eqn)))
-> Maybe (FSym, Eqn) -> IO (Maybe (FSym, Eqn))
forall a b. (a -> b) -> a -> b
$ FSym -> IntMap (FSym, Eqn) -> Maybe (FSym, Eqn)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
c IntMap (FSym, Eqn)
m

getERepresentative :: Solver -> FSym -> IO FSym
getERepresentative :: Solver -> FSym -> IO FSym
getERepresentative Solver
solver FSym
a = UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svERepresentativeTable Solver
solver) FSym
a

getHighestNode :: Solver -> FSym -> IO FSym
getHighestNode :: Solver -> FSym -> IO FSym
getHighestNode Solver
solver FSym
c = do
  FSym
d <- Solver -> FSym -> IO FSym
getERepresentative Solver
solver FSym
c
  UVec FSym -> FSym -> IO FSym
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svEHighestNodeTable Solver
solver) FSym
d

nearestCommonAncestor :: Solver -> FSym -> FSym -> IO (Maybe FSym)
nearestCommonAncestor :: Solver -> FSym -> FSym -> IO (Maybe FSym)
nearestCommonAncestor Solver
solver FSym
a FSym
b = do
  let loop :: FSym -> IntSet -> IO IntSet
loop FSym
c !IntSet
ret = do
        Maybe (FSym, Eqn)
m <- Solver -> FSym -> IO (Maybe (FSym, Eqn))
getParent Solver
solver FSym
c
        case Maybe (FSym, Eqn)
m of
          Maybe (FSym, Eqn)
Nothing -> IntSet -> IO IntSet
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return IntSet
ret
          Just (FSym
d,Eqn
_) -> FSym -> IntSet -> IO IntSet
loop FSym
d (FSym -> IntSet -> IntSet
IntSet.insert FSym
d IntSet
ret)
  IntSet
a_ancestors <- FSym -> IntSet -> IO IntSet
loop FSym
a (FSym -> IntSet
IntSet.singleton FSym
a)

  let loop2 :: FSym -> IO (Maybe FSym)
loop2 FSym
c = do
        if FSym
c FSym -> IntSet -> Bool
`IntSet.member` IntSet
a_ancestors then
          (FSym -> Maybe FSym) -> IO FSym -> IO (Maybe FSym)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FSym -> Maybe FSym
forall a. a -> Maybe a
Just (IO FSym -> IO (Maybe FSym)) -> IO FSym -> IO (Maybe FSym)
forall a b. (a -> b) -> a -> b
$ Solver -> FSym -> IO FSym
getHighestNode Solver
solver FSym
c
        else do
          Maybe (FSym, Eqn)
m <- Solver -> FSym -> IO (Maybe (FSym, Eqn))
getParent Solver
solver FSym
c
          case Maybe (FSym, Eqn)
m of
            Maybe (FSym, Eqn)
Nothing -> Maybe FSym -> IO (Maybe FSym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FSym
forall a. Maybe a
Nothing
            Just (FSym
d,Eqn
_) -> FSym -> IO (Maybe FSym)
loop2 FSym
d
  FSym -> IO (Maybe FSym)
loop2 FSym
b

termToFlatTerm :: Solver -> Term -> IO FlatTerm
termToFlatTerm :: Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver (TApp FSym
f [Term]
xs) = do
  [FlatTerm]
xs' <- (Term -> IO FlatTerm) -> [Term] -> IO [FlatTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver) [Term]
xs
  let phi :: FlatTerm -> FlatTerm -> IO FlatTerm
phi FlatTerm
t FlatTerm
u = do
        FSym
t' <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
t
        FSym
u' <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
u
        FlatTerm -> IO FlatTerm
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FlatTerm -> IO FlatTerm) -> FlatTerm -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ FSym -> FSym -> FlatTerm
FTApp FSym
t' FSym
u'
  (FlatTerm -> FlatTerm -> IO FlatTerm)
-> FlatTerm -> [FlatTerm] -> IO FlatTerm
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM FlatTerm -> FlatTerm -> IO FlatTerm
phi (FSym -> FlatTerm
FTConst FSym
f) [FlatTerm]
xs'

flatTermToFSym :: Solver -> FlatTerm -> IO FSym
flatTermToFSym :: Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
_ (FTConst FSym
c) = FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
c
flatTermToFSym Solver
solver (FTApp FSym
c FSym
d) = do
  (IntMap (FSym, FSym)
defs1,Map (FSym, FSym) FSym
defs2) <- IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a. IORef a -> IO a
readIORef (IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
 -> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym))
-> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver
  FSym
a <- case (FSym, FSym) -> Map (FSym, FSym) FSym -> Maybe FSym
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (FSym
c,FSym
d) Map (FSym, FSym) FSym
defs2 of
         Just FSym
a -> FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
a
         Maybe FSym
Nothing -> do
           FSym
a <- Solver -> IO FSym
newFSym Solver
solver
           IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> (IntMap (FSym, FSym), Map (FSym, FSym) FSym) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver) (FSym -> (FSym, FSym) -> IntMap (FSym, FSym) -> IntMap (FSym, FSym)
forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
a (FSym
c,FSym
d) IntMap (FSym, FSym)
defs1, (FSym, FSym)
-> FSym -> Map (FSym, FSym) FSym -> Map (FSym, FSym) FSym
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (FSym
c,FSym
d) FSym
a Map (FSym, FSym) FSym
defs2)
           Solver -> FlatTerm -> FSym -> IO ()
mergeFlatTerm Solver
solver (FSym -> FSym -> FlatTerm
FTApp FSym
c FSym
d) FSym
a
           FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
a
  FSym -> IO FSym
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FSym
a

fsymToFlatTerm :: Solver -> FSym -> IO FlatTerm
fsymToFlatTerm :: Solver -> FSym -> IO FlatTerm
fsymToFlatTerm Solver
solver FSym
a = do
  (IntMap (FSym, FSym)
defs1,Map (FSym, FSym) FSym
_) <- IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a. IORef a -> IO a
readIORef (IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
 -> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym))
-> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver
  case FSym -> IntMap (FSym, FSym) -> Maybe (FSym, FSym)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
a IntMap (FSym, FSym)
defs1 of
    Just (FSym
c,FSym
d) -> FlatTerm -> IO FlatTerm
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym -> FSym -> FlatTerm
FTApp FSym
c FSym
d)
    Maybe (FSym, FSym)
Nothing -> FlatTerm -> IO FlatTerm
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym -> FlatTerm
FTConst FSym
a)

termToFSym :: Solver -> Term -> IO FSym
termToFSym :: Solver -> Term -> IO FSym
termToFSym Solver
solver Term
t = Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver (FlatTerm -> IO FSym) -> IO FlatTerm -> IO FSym
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver Term
t

fsymToTerm :: Solver -> FSym -> IO Term
fsymToTerm :: Solver -> FSym -> IO Term
fsymToTerm Solver
solver FSym
a = do
  (IntMap (FSym, FSym)
defs1,Map (FSym, FSym) FSym
_) <- IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a. IORef a -> IO a
readIORef (IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
 -> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym))
-> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
-> IO (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver
  let convert :: FSym -> Term
      convert :: FSym -> Term
convert FSym
a =
        case FSym -> (FSym, [Term])
convert' FSym
a of
          (FSym
f, [Term]
xs) -> FSym -> [Term] -> Term
TApp FSym
f ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
xs)
      convert' :: FSym -> (FSym, [Term])
      convert' :: FSym -> (FSym, [Term])
convert' FSym
a =
        case FSym -> IntMap (FSym, FSym) -> Maybe (FSym, FSym)
forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
a IntMap (FSym, FSym)
defs1 of
          Maybe (FSym, FSym)
Nothing -> (FSym
a, [])
          Just (FSym
c,FSym
d) ->
            case FSym -> (FSym, [Term])
convert' FSym
c of
              (FSym
f,[Term]
xs) -> (FSym
f, FSym -> Term
convert FSym
d Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
xs)
  Term -> IO Term
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FSym -> Term
convert FSym
a)

maybeToIntSet :: Maybe Int -> IntSet
maybeToIntSet :: Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
Nothing  = IntSet
IntSet.empty
maybeToIntSet (Just FSym
x) = FSym -> IntSet
IntSet.singleton FSym
x