{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# 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
#if !MIN_VERSION_base(4,11,0)
import Data.Semigroup
#endif
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
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show)

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
min :: FlatTerm -> FlatTerm -> FlatTerm
$cmin :: FlatTerm -> FlatTerm -> FlatTerm
max :: FlatTerm -> FlatTerm -> FlatTerm
$cmax :: FlatTerm -> FlatTerm -> FlatTerm
>= :: FlatTerm -> FlatTerm -> Bool
$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
compare :: FlatTerm -> FlatTerm -> Ordering
$ccompare :: FlatTerm -> FlatTerm -> Ordering
$cp1Ord :: Eq FlatTerm
Ord, FlatTerm -> FlatTerm -> Bool
(FlatTerm -> FlatTerm -> Bool)
-> (FlatTerm -> FlatTerm -> Bool) -> Eq FlatTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FlatTerm -> FlatTerm -> Bool
$c/= :: FlatTerm -> FlatTerm -> Bool
== :: FlatTerm -> FlatTerm -> Bool
$c== :: FlatTerm -> FlatTerm -> Bool
Eq, Int -> FlatTerm -> ShowS
[FlatTerm] -> ShowS
FlatTerm -> String
(Int -> FlatTerm -> ShowS)
-> (FlatTerm -> String) -> ([FlatTerm] -> ShowS) -> Show FlatTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FlatTerm] -> ShowS
$cshowList :: [FlatTerm] -> ShowS
show :: FlatTerm -> String
$cshow :: FlatTerm -> String
showsPrec :: Int -> FlatTerm -> ShowS
$cshowsPrec :: Int -> 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
/= :: Eqn0 -> Eqn0 -> Bool
$c/= :: Eqn0 -> Eqn0 -> Bool
== :: Eqn0 -> Eqn0 -> Bool
$c== :: 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
min :: Eqn0 -> Eqn0 -> Eqn0
$cmin :: Eqn0 -> Eqn0 -> Eqn0
max :: Eqn0 -> Eqn0 -> Eqn0
$cmax :: Eqn0 -> Eqn0 -> Eqn0
>= :: Eqn0 -> Eqn0 -> Bool
$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
compare :: Eqn0 -> Eqn0 -> Ordering
$ccompare :: Eqn0 -> Eqn0 -> Ordering
$cp1Ord :: Eq Eqn0
Ord, Int -> Eqn0 -> ShowS
[Eqn0] -> ShowS
Eqn0 -> String
(Int -> Eqn0 -> ShowS)
-> (Eqn0 -> String) -> ([Eqn0] -> ShowS) -> Show Eqn0
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Eqn0] -> ShowS
$cshowList :: [Eqn0] -> ShowS
show :: Eqn0 -> String
$cshow :: Eqn0 -> String
showsPrec :: Int -> Eqn0 -> ShowS
$cshowsPrec :: Int -> 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
/= :: Eqn1 -> Eqn1 -> Bool
$c/= :: Eqn1 -> Eqn1 -> Bool
== :: Eqn1 -> Eqn1 -> Bool
$c== :: 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
min :: Eqn1 -> Eqn1 -> Eqn1
$cmin :: Eqn1 -> Eqn1 -> Eqn1
max :: Eqn1 -> Eqn1 -> Eqn1
$cmax :: Eqn1 -> Eqn1 -> Eqn1
>= :: Eqn1 -> Eqn1 -> Bool
$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
compare :: Eqn1 -> Eqn1 -> Ordering
$ccompare :: Eqn1 -> Eqn1 -> Ordering
$cp1Ord :: Eq Eqn1
Ord, Int -> Eqn1 -> ShowS
[Eqn1] -> ShowS
Eqn1 -> String
(Int -> Eqn1 -> ShowS)
-> (Eqn1 -> String) -> ([Eqn1] -> ShowS) -> Show Eqn1
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Eqn1] -> ShowS
$cshowList :: [Eqn1] -> ShowS
show :: Eqn1 -> String
$cshow :: Eqn1 -> String
showsPrec :: Int -> Eqn1 -> ShowS
$cshowsPrec :: Int -> 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 (Int -> Class -> ShowS
[Class] -> ShowS
Class -> String
(Int -> Class -> ShowS)
-> (Class -> String) -> ([Class] -> ShowS) -> Show Class
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Class] -> ShowS
$cshowList :: [Class] -> ShowS
show :: Class -> String
$cshow :: Class -> String
showsPrec :: Int -> Class -> ShowS
$cshowsPrec :: Int -> Class -> ShowS
Show)

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

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

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

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

data Solver
  = Solver
  { Solver -> IORef (IntMap (Int, Int), Map (Int, Int) Int)
svDefs                 :: !(IORef (IntMap (FSym,FSym), Map (FSym,FSym) FSym))
  , Solver -> UVec Int
svRepresentativeTable  :: !(Vec.UVec FSym)
  , Solver -> Vec Class
svClassList            :: !(Vec.Vec Class)
  , Solver -> IORef (IntMap (Int, Eqn))
svParent               :: !(IORef (IntMap (FSym, Eqn)))
  , Solver -> IORef (IntMap [(Eqn1, Int, Int)])
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 Int
svERepresentativeTable :: !(Vec.UVec FSym)
  , Solver -> Vec Class
svEClassList           :: !(Vec.Vec Class)
  , Solver -> UVec Int
svEHighestNodeTable    :: !(Vec.UVec FSym)
  , Solver -> Vec (Int, Int)
svEPendingProofs       :: !(Vec.Vec (FSym,FSym))

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

newSolver :: IO Solver
newSolver :: IO Solver
newSolver = do
  IORef (IntMap (Int, Int), Map (Int, Int) Int)
defs     <- (IntMap (Int, Int), Map (Int, Int) Int)
-> IO (IORef (IntMap (Int, Int), Map (Int, Int) Int))
forall a. a -> IO (IORef a)
newIORef (IntMap (Int, Int)
forall a. IntMap a
IntMap.empty, Map (Int, Int) Int
forall k a. Map k a
Map.empty)
  UVec Int
rep      <- IO (UVec Int)
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 (Int, Eqn))
parent   <- IntMap (Int, Eqn) -> IO (IORef (IntMap (Int, Eqn)))
forall a. a -> IO (IORef a)
newIORef IntMap (Int, Eqn)
forall a. IntMap a
IntMap.empty
  IORef (IntMap [(Eqn1, Int, Int)])
useList  <- IntMap [(Eqn1, Int, Int)] -> IO (IORef (IntMap [(Eqn1, Int, Int)]))
forall a. a -> IO (IORef a)
newIORef IntMap [(Eqn1, Int, Int)]
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 Int
repE     <- IO (UVec Int)
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 Int
highE    <- IO (UVec Int)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec (Int, Int)
pendingE <- IO (Vec (Int, Int))
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 Int
gen <- IO (UVec Int)
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  UVec Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Int
gen Int
0
  IORef Bool
isAfterBT <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False

  Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> IO Solver) -> Solver -> IO Solver
forall a b. (a -> b) -> a -> b
$
    Solver :: IORef (IntMap (Int, Int), Map (Int, Int) Int)
-> UVec Int
-> Vec Class
-> IORef (IntMap (Int, Eqn))
-> IORef (IntMap [(Eqn1, Int, Int)])
-> IORef (IntMap (IntMap Eqn1))
-> Vec Eqn
-> UVec Int
-> Vec Class
-> UVec Int
-> Vec (Int, Int)
-> Vec [TrailItem]
-> UVec Int
-> IORef Bool
-> Solver
Solver
    { svDefs :: IORef (IntMap (Int, Int), Map (Int, Int) Int)
svDefs                = IORef (IntMap (Int, Int), Map (Int, Int) Int)
defs
    , svRepresentativeTable :: UVec Int
svRepresentativeTable = UVec Int
rep
    , svClassList :: Vec Class
svClassList           = Vec Class
classes
    , svParent :: IORef (IntMap (Int, Eqn))
svParent              = IORef (IntMap (Int, Eqn))
parent
    , svUseList :: IORef (IntMap [(Eqn1, Int, Int)])
svUseList             = IORef (IntMap [(Eqn1, Int, Int)])
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 Int
svERepresentativeTable = UVec Int
repE
    , svEClassList :: Vec Class
svEClassList           = Vec Class
classesE
    , svEHighestNodeTable :: UVec Int
svEHighestNodeTable    = UVec Int
highE
    , svEPendingProofs :: Vec (Int, Int)
svEPendingProofs       = Vec (Int, Int)
pendingE

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

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

newFSym :: Solver -> IO FSym
newFSym :: Solver -> IO Int
newFSym Solver
solver = do
  Int
v <- Solver -> IO Int
getNFSyms Solver
solver
  UVec Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Int
svRepresentativeTable Solver
solver) Int
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) (Int -> Class
ClassSingleton Int
v)
  IORef (IntMap [(Eqn1, Int, Int)])
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver) (Int
-> [(Eqn1, Int, Int)]
-> IntMap [(Eqn1, Int, Int)]
-> IntMap [(Eqn1, Int, Int)]
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v [])
  UVec Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Int
svERepresentativeTable Solver
solver) Int
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 Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Int
svEHighestNodeTable Solver
solver) Int
v
  Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
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 :: Solver -> IO a
newFun Solver
solver = do
  Int
c <- Solver -> IO Int
newFSym Solver
solver
  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 (Int -> [Term] -> Term
TApp Int
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 Int -> IO ()
merge' Solver
solver Term
t Term
u Maybe Int
forall a. Maybe a
Nothing

merge' :: Solver -> Term -> Term -> Maybe ConstrID -> IO ()
merge' :: Solver -> Term -> Term -> Maybe Int -> IO ()
merge' Solver
solver Term
t Term
u Maybe Int
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 Int
c, FlatTerm
_) -> Solver -> FlatTerm -> Int -> Maybe Int -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
u' Int
c Maybe Int
cid
    (FlatTerm
_, FTConst Int
c) -> Solver -> FlatTerm -> Int -> Maybe Int -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
t' Int
c Maybe Int
cid
    (FlatTerm, FlatTerm)
_ -> do
      Int
c <- Solver -> FlatTerm -> IO Int
flatTermToFSym Solver
solver FlatTerm
u'
      Solver -> FlatTerm -> Int -> Maybe Int -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
t' Int
c Maybe Int
cid

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

mergeFlatTerm' :: Solver -> FlatTerm -> FSym -> Maybe ConstrID -> IO ()
mergeFlatTerm' :: Solver -> FlatTerm -> Int -> Maybe Int -> IO ()
mergeFlatTerm' Solver
solver FlatTerm
s Int
a Maybe Int
cid = do
  Solver -> IO ()
initAfterBacktracking Solver
solver
  case FlatTerm
s of
    FTConst Int
c -> do
      let eq1 :: Eqn0
eq1 = Maybe Int -> Int -> Int -> Eqn0
Eqn0 Maybe Int
cid Int
c Int
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 Int
a1 Int
a2 -> do
      let eq1 :: Eqn1
eq1 = Maybe Int -> Int -> Int -> Int -> Eqn1
Eqn1 Maybe Int
cid Int
a1 Int
a2 Int
a
      Int
a1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a1
      Int
a2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a2
      Maybe Eqn1
ret <- Solver -> Int -> Int -> IO (Maybe Eqn1)
lookup Solver
solver Int
a1' Int
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 -> Int -> Int -> Eqn1 -> IO ()
setLookup Solver
solver Int
a1' Int
a2' Eqn1
eq1
          Int
lv <- Solver -> IO Int
getCurrentLevel Solver
solver
          Int
gen <- Solver -> Int -> IO Int
getLevelGen Solver
solver Int
lv
          IORef (IntMap [(Eqn1, Int, Int)])
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver) ((IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)]) -> IO ())
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a b. (a -> b) -> a -> b
$
            ([(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)])
-> Int -> IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)]
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, Int
lv, Int
gen) (Eqn1, Int, Int) -> [(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)]
forall a. a -> [a] -> [a]
:) Int
a1' (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IntMap [(Eqn1, Int, Int)]
-> IntMap [(Eqn1, Int, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            ([(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)])
-> Int -> IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)]
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, Int
lv, Int
gen) (Eqn1, Int, Int) -> [(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)]
forall a. a -> [a] -> [a]
:) Int
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
      Int
n <- Vec Eqn -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec Eqn
svPending Solver
solver)
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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 (Int
a,Int
b) = case Eqn
p of
                    Left (Eqn0 _ a b) -> (Int
a,Int
b)
                    Right (Eqn1 _ _ _ a, Eqn1 _ _ _ b) -> (Int
a,Int
b)
      Int
a' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a
      Int
b' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
a' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Class
classA <- Vec Class -> Int -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) Int
a'
        Class
classB <- Vec Class -> Int -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) Int
b'
        (Int
a,Int
b,Int
a',Int
b',Class
classA,Class
classB) <- (Int, Int, Int, Int, Class, Class)
-> IO (Int, Int, Int, Int, Class, Class)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, Int, Int, Int, Class, Class)
 -> IO (Int, Int, Int, Int, Class, Class))
-> (Int, Int, Int, Int, Class, Class)
-> IO (Int, Int, Int, Int, Class, Class)
forall a b. (a -> b) -> a -> b
$
          if Class -> Int
classSize Class
classA Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Class -> Int
classSize Class
classB then
            (Int
a,Int
b,Int
a',Int
b',Class
classA,Class
classB)
          else
            (Int
b,Int
a,Int
b',Int
a',Class
classB,Class
classA)
        Int
origRootA <- Int -> Int -> Eqn -> IO Int
updateParent Int
a Int
b Eqn
p
        Int -> Int -> Class -> Class -> IO ()
update Int
a' Int
b' Class
classA Class
classB
        Solver -> TrailItem -> IO ()
addToTrail Solver
solver (Int -> Int -> Int -> Int -> TrailItem
TrailMerge Int
a' Int
b' Int
a Int
origRootA)

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

      Int
lv <- Solver -> IO Int
getCurrentLevel Solver
solver
      Int
lv_gen <- Solver -> Int -> IO Int
getLevelGen Solver
solver Int
lv
      IntMap [(Eqn1, Int, Int)]
useList <- IORef (IntMap [(Eqn1, Int, Int)]) -> IO (IntMap [(Eqn1, Int, Int)])
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver)
      [(Eqn1, Int, Int)]
useList_a' <- (((Eqn1, Int, Int) -> IO Bool)
 -> [(Eqn1, Int, Int)] -> IO [(Eqn1, Int, Int)])
-> [(Eqn1, Int, Int)]
-> ((Eqn1, Int, Int) -> IO Bool)
-> IO [(Eqn1, Int, Int)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Eqn1, Int, Int) -> IO Bool)
-> [(Eqn1, Int, Int)] -> IO [(Eqn1, Int, Int)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IntMap [(Eqn1, Int, Int)]
useList IntMap [(Eqn1, Int, Int)] -> Int -> [(Eqn1, Int, Int)]
forall a. IntMap a -> Int -> a
IntMap.! Int
a') (((Eqn1, Int, Int) -> IO Bool) -> IO [(Eqn1, Int, Int)])
-> ((Eqn1, Int, Int) -> IO Bool) -> IO [(Eqn1, Int, Int)]
forall a b. (a -> b) -> a -> b
$ \(eq1 :: Eqn1
eq1@(Eqn1 Maybe Int
_ Int
c1 Int
c2 Int
_), Int
lv2, Int
lv2_gen2) -> do
        Int
lv2_gen <- Solver -> Int -> IO Int
getLevelGen Solver
solver Int
lv2
        if Int
lv2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lv Bool -> Bool -> Bool
&& Int
lv2_gen2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lv2_gen then do
          Int
c1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
c1
          Int
c2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
c2
          Bool -> IO () -> IO ()
forall a. HasCallStack => Bool -> a -> a
assert (Int
b' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c1' Bool -> Bool -> Bool
|| Int
b' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c2') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
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 -> Int -> Int -> IO (Maybe Eqn1)
lookup Solver
solver Int
c1' Int
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 -> Int -> Int -> Eqn1 -> IO ()
setLookup Solver
solver Int
c1' Int
c2' Eqn1
eq1
              IORef (IntMap [(Eqn1, Int, Int)])
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver) ((IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)]) -> IO ())
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a b. (a -> b) -> a -> b
$ ([(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)])
-> Int -> IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)]
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, Int
lv, Int
lv_gen) (Eqn1, Int, Int) -> [(Eqn1, Int, Int)] -> [(Eqn1, Int, Int)]
forall a. a -> [a] -> [a]
:) Int
b'
              () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else do
          -- out-of-date entry
          Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      IORef (IntMap [(Eqn1, Int, Int)])
-> (IntMap [(Eqn1, Int, Int)] -> IntMap [(Eqn1, Int, Int)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver) (Int
-> [(Eqn1, Int, Int)]
-> IntMap [(Eqn1, Int, Int)]
-> IntMap [(Eqn1, Int, Int)]
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
a' [(Eqn1, Int, Int)]
useList_a')

    -- Insert edge a→b labelled with a_eq_b into the proof forest, and re-orient its original ancestors.
    updateParent :: Int -> Int -> Eqn -> IO Int
updateParent Int
a Int
b Eqn
a_eq_b = do
      let loop :: Int -> (Int, Eqn) -> IO Int
loop Int
d (Int
c, Eqn
c_eq_d) = do
            IntMap (Int, Eqn)
tbl <- IORef (IntMap (Int, Eqn)) -> IO (IntMap (Int, Eqn))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (Int, Eqn))
svParent Solver
solver)
            IORef (IntMap (Int, Eqn)) -> IntMap (Int, Eqn) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (Int, Eqn))
svParent Solver
solver) (Int -> (Int, Eqn) -> IntMap (Int, Eqn) -> IntMap (Int, Eqn)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
d (Int
c, Eqn
c_eq_d) IntMap (Int, Eqn)
tbl)
            case Int -> IntMap (Int, Eqn) -> Maybe (Int, Eqn)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
d IntMap (Int, Eqn)
tbl of
              Maybe (Int, Eqn)
Nothing -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
d
              Just (Int
e, Eqn
d_eq_e) -> Int -> (Int, Eqn) -> IO Int
loop Int
e (Int
d, Eqn
d_eq_e)
      Int -> (Int, Eqn) -> IO Int
loop Int
a (Int
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 (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 Int
c) = (Int -> FlatTerm) -> IO Int -> IO FlatTerm
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> FlatTerm
FTConst (IO Int -> IO FlatTerm) -> IO Int -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> IO Int
getRepresentative Solver
solver Int
c
normalize Solver
solver (FTApp Int
t1 Int
t2) = do
  Int
u1 <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
t1
  Int
u2 <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
t2
  Maybe Eqn1
ret <- Solver -> Int -> Int -> IO (Maybe Eqn1)
lookup Solver
solver Int
u1 Int
u2
  case Maybe Eqn1
ret of
    Just (Eqn1 Maybe Int
_ Int
_ Int
_ Int
a) -> (Int -> FlatTerm) -> IO Int -> IO FlatTerm
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> FlatTerm
FTConst (IO Int -> IO FlatTerm) -> IO Int -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a
    Maybe Eqn1
Nothing -> FlatTerm -> IO FlatTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FlatTerm -> IO FlatTerm) -> FlatTerm -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Int -> Int -> FlatTerm
FTApp Int
u1 Int
u2

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

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

  IORef IntSet
ref <- IntSet -> IO (IORef IntSet)
forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty
  [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
representatives) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
a' -> do
    Class
bs <- Vec Class -> Int -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.read (Solver -> Vec Class
svClassList Solver
solver) Int
a'
    [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Class -> [Int]
classToList Class
bs) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
b -> do
      Int
b' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
a' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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 (Int -> IntSet -> IntSet
IntSet.insert Int
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
== [Int] -> IntSet
IntSet.fromList [Int
0..Int
nvInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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 (m :: * -> *) a. Monad m => a -> m a
return ()
      Right (Eqn1 Maybe Int
_ Int
a1 Int
a2 Int
_, Eqn1 Maybe Int
_ Int
b1 Int
b2 Int
_) -> do
        Int
a1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a1
        Int
a2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a2
        Int
b1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b1
        Int
b2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b2
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
a1' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b1' Bool -> Bool -> Bool
&& Int
a2' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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, Int, Int)]
useList <- IORef (IntMap [(Eqn1, Int, Int)]) -> IO (IntMap [(Eqn1, Int, Int)])
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap [(Eqn1, Int, Int)])
svUseList Solver
solver)
  Int
lv <- Solver -> IO Int
getCurrentLevel Solver
solver
  [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
representatives) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
a -> do
    [(Eqn1, Int, Int)] -> ((Eqn1, Int, Int) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap [(Eqn1, Int, Int)]
useList IntMap [(Eqn1, Int, Int)] -> Int -> [(Eqn1, Int, Int)]
forall a. IntMap a -> Int -> a
IntMap.! Int
a) (((Eqn1, Int, Int) -> IO ()) -> IO ())
-> ((Eqn1, Int, Int) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Eqn1 Maybe Int
_ Int
b1 Int
b2 Int
_, Int
lv2, Int
lv2_gen2) -> do
      Int
lv2_gen <- Solver -> Int -> IO Int
getLevelGen Solver
solver Int
lv2
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
lv2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lv Bool -> Bool -> Bool
&& Int
lv2_gen2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lv2_gen) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Int
b1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b1
        Int
b2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
b2
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b1' Bool -> Bool -> Bool
|| Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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"

  [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
representatives) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
b -> do
    [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [Int]
IntSet.toList IntSet
representatives) ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
c -> do
      Maybe Eqn1
m <- Solver -> Int -> Int -> IO (Maybe Eqn1)
lookup Solver
solver Int
b Int
c
      case Maybe Eqn1
m of
        Maybe Eqn1
Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just (Eqn1 Maybe Int
_ Int
a1 Int
a2 Int
_) -> do
          Int
a1' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a1
          Int
a2' <- Solver -> Int -> IO Int
getRepresentative Solver
solver Int
a2
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
a1' Bool -> Bool -> Bool
&& Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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
  Int
c1 <- Solver -> FlatTerm -> IO Int
flatTermToFSym Solver
solver FlatTerm
t1
  Int
c2 <- Solver -> FlatTerm -> IO Int
flatTermToFSym Solver
solver FlatTerm
t2
  Solver -> Int -> Int -> IO (Maybe IntSet)
explainConst Solver
solver Int
c1 Int
c2

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

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

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

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

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

      explainAlongPath :: FSym -> FSym -> IO ()
      explainAlongPath :: Int -> Int -> IO ()
explainAlongPath Int
a Int
c = do
        Int
a <- Solver -> Int -> IO Int
getHighestNode Solver
solver Int
a
        -- note that c is already @getHighestNode solver c@
        let loop :: Int -> IO ()
loop Int
a =
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                Just (Int
b, Eqn
eq) <- Solver -> Int -> IO (Maybe (Int, Eqn))
getParent Solver
solver Int
a
                case Eqn
eq of
                  Left (Eqn0 Maybe Int
cid Int
_ Int
_) -> do
                    IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result (Maybe Int -> IntSet
maybeToIntSet Maybe Int
cid IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<>)
                  Right (Eqn1 Maybe Int
cid1 Int
a1 Int
a2 Int
_, Eqn1 Maybe Int
cid2 Int
b1 Int
b2 Int
_) -> do
                    IORef IntSet -> (IntSet -> IntSet) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result ((Maybe Int -> IntSet
maybeToIntSet Maybe Int
cid1 IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> Maybe Int -> IntSet
maybeToIntSet Maybe Int
cid2) IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<>)
                    Vec (Int, Int) -> (Int, Int) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (Int, Int)
svEPendingProofs Solver
solver) (Int
a1,Int
b1)
                    Vec (Int, Int) -> (Int, Int) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (Int, Int)
svEPendingProofs Solver
solver) (Int
a2,Int
b2)
                Int -> Int -> IO ()
union Int
a Int
b
                Int -> IO ()
loop (Int -> IO ()) -> IO Int -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Int -> IO Int
getHighestNode Solver
solver Int
b
        Int -> IO ()
loop Int
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 (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 [Int] Int)
mFunctions   :: !(IntMap (Map EntityTuple Entity))
  , Model -> Int
mUnspecified :: !Entity
  , Model -> [(Set Term, Int)]
mEquivClasses :: [(Set Term, Entity)]
  }
  deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> String
(Int -> Model -> ShowS)
-> (Model -> String) -> ([Model] -> ShowS) -> Show Model
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Model] -> ShowS
$cshowList :: [Model] -> ShowS
show :: Model -> String
$cshow :: Model -> String
showsPrec :: Int -> Model -> ShowS
$cshowsPrec :: Int -> Model -> ShowS
Show)

getModel :: Solver -> IO Model
getModel :: Solver -> IO Model
getModel Solver
solver = do
  Int
n <- UVec Int -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> UVec Int
svRepresentativeTable Solver
solver)
  IORef IntSet
univRef <- IntSet -> IO (IORef IntSet)
forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty
  IORef (IntMap Int)
reprRef <- IntMap Int -> IO (IORef (IntMap Int))
forall a. a -> IO (IORef a)
newIORef IntMap Int
forall a. IntMap a
IntMap.empty
  [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
a -> do
    Int
a' <- UVec Int -> Int -> IO Int
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> UVec Int
svRepresentativeTable Solver
solver) Int
a
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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 (Int -> IntSet -> IntSet
IntSet.insert Int
a)
    IORef (IntMap Int) -> (IntMap Int -> IntMap Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (IntMap Int)
reprRef (Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
a Int
a')
  -- univ <- readIORef univRef
  IntMap Int
repr <- IORef (IntMap Int) -> IO (IntMap Int)
forall a. IORef a -> IO a
readIORef IORef (IntMap Int)
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 (Int, Int))
appRel = (Set (Int, Int) -> Set (Int, Int) -> Set (Int, Int))
-> [(Int, Set (Int, Int))] -> IntMap (Set (Int, Int))
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMap.fromListWith Set (Int, Int) -> Set (Int, Int) -> Set (Int, Int)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([(Int, Set (Int, Int))] -> IntMap (Set (Int, Int)))
-> [(Int, Set (Int, Int))] -> IntMap (Set (Int, Int))
forall a b. (a -> b) -> a -> b
$
        [ (IntMap Int
repr IntMap Int -> Int -> Int
forall a. IntMap a -> Int -> a
IntMap.! Int
c, (Int, Int) -> Set (Int, Int)
forall a. a -> Set a
Set.singleton (IntMap Int
repr IntMap Int -> Int -> Int
forall a. IntMap a -> Int -> a
IntMap.! Int
a, IntMap Int
repr IntMap Int -> Int -> Int
forall a. IntMap a -> Int -> a
IntMap.! Int
b))
        | (Int
a,IntMap Eqn1
m) <- IntMap (IntMap Eqn1) -> [(Int, IntMap Eqn1)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (IntMap Eqn1)
lookups, (Int
b, Eqn1 Maybe Int
_ Int
_ Int
_ Int
c) <- IntMap Eqn1 -> [(Int, Eqn1)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Eqn1
m
        ]

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

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

      xs2 :: IntMap (Map EntityTuple Entity)
      xs2 :: IntMap (Map [Int] Int)
xs2 = (Map [Int] Int -> Map [Int] Int -> Map [Int] Int)
-> [(Int, Map [Int] Int)] -> IntMap (Map [Int] Int)
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMap.fromListWith Map [Int] Int -> Map [Int] Int -> Map [Int] Int
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ([(Int, Map [Int] Int)] -> IntMap (Map [Int] Int))
-> [(Int, Map [Int] Int)] -> IntMap (Map [Int] Int)
forall a b. (a -> b) -> a -> b
$
              [ (Int
a, [Int] -> Int -> Map [Int] Int
forall k a. k -> a -> Map k a
Map.singleton [] Int
a') | (Int
a, Int
a') <- IntMap Int -> [(Int, Int)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Int
repr, Int
a Int -> IntMap (Map [Int] Int) -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.notMember` IntMap (Map [Int] Int)
xs1 ]

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

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

  [(Set Term, Int)]
classes <- [Int] -> (Int -> IO (Set Term, Int)) -> IO [(Set Term, Int)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (IntSet -> [Int]
IntSet.toList IntSet
used) ((Int -> IO (Set Term, Int)) -> IO [(Set Term, Int)])
-> (Int -> IO (Set Term, Int)) -> IO [(Set Term, Int)]
forall a b. (a -> b) -> a -> b
$ \Int
a -> do
    Class
classA <- Vec Class -> Int -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList  Solver
solver) Int
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
$ (Int -> IO Term) -> [Int] -> IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Int -> IO Term
fsymToTerm Solver
solver) (Class -> [Int]
classToList Class
classA)
    (Set Term, Int) -> IO (Set Term, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Term
classA', Int
a)

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

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

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

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

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

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

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

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

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

type Level = Int
type Gen = Int

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

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

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

getLevelGen :: Solver -> Level -> IO Gen
getLevelGen :: Solver -> Int -> IO Int
getLevelGen Solver
solver Int
lv = UVec Int -> Int -> IO Int
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> UVec Int
svLevelGen Solver
solver) Int
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) []
  Int
lv <- Solver -> IO Int
getCurrentLevel Solver
solver
  Int
size <- UVec Int -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> UVec Int
svLevelGen Solver
solver)
  if Int
lv Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size then do
    Int
g <- UVec Int -> Int -> IO Int
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> UVec Int
svLevelGen Solver
solver) Int
lv
    UVec Int -> Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Int
svLevelGen Solver
solver) Int
lv (Int
g Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  else
    UVec Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Int
svLevelGen Solver
solver) Int
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 Int
a' Int
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)
-> Int -> IntMap (IntMap Eqn1) -> IntMap (IntMap Eqn1)
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust (Int -> IntMap Eqn1 -> IntMap Eqn1
forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
b') Int
a')
      TrailMerge Int
a' Int
b' Int
a Int
origRootA -> do
        -- Revert changes to Union-Find data strucutres
        ClassUnion Int
_ Class
origClassA Class
origClassB <- Vec Class -> Int -> IO Class
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList Solver
solver) Int
b'
        Class -> (Int -> IO ()) -> IO ()
forall (m :: * -> *). Monad m => Class -> (Int -> m ()) -> m ()
classForM_ Class
origClassA ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
c -> do
          UVec Int -> Int -> Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Int
svRepresentativeTable Solver
solver) Int
c Int
a'
        Vec Class -> Int -> Class -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> e -> IO ()
Vec.unsafeWrite (Solver -> Vec Class
svClassList Solver
solver) Int
b' Class
origClassB

        -- Revert changes to proof-forest data strucutres
        let loop :: Int -> Maybe (Int, Eqn) -> IO ()
loop Int
c Maybe (Int, Eqn)
p = do
              IntMap (Int, Eqn)
tbl <- IORef (IntMap (Int, Eqn)) -> IO (IntMap (Int, Eqn))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (Int, Eqn))
svParent Solver
solver)
              IORef (IntMap (Int, Eqn)) -> IntMap (Int, Eqn) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (Int, Eqn))
svParent Solver
solver) (((Int, Eqn) -> Maybe (Int, Eqn))
-> Int -> IntMap (Int, Eqn) -> IntMap (Int, Eqn)
forall a. (a -> Maybe a) -> Int -> IntMap a -> IntMap a
IntMap.update (Maybe (Int, Eqn) -> (Int, Eqn) -> Maybe (Int, Eqn)
forall a b. a -> b -> a
const Maybe (Int, Eqn)
p) Int
c IntMap (Int, Eqn)
tbl)
              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
a) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                let (Int
d, Eqn
c_eq_d) = IntMap (Int, Eqn)
tbl IntMap (Int, Eqn) -> Int -> (Int, Eqn)
forall a. IntMap a -> Int -> a
IntMap.! Int
c
                Int -> Maybe (Int, Eqn) -> IO ()
loop Int
d ((Int, Eqn) -> Maybe (Int, Eqn)
forall a. a -> Maybe a
Just (Int
c, Eqn
c_eq_d))
        Int -> Maybe (Int, Eqn) -> IO ()
loop Int
origRootA Maybe (Int, 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 (Int, Int)
defs, Map (Int, Int) Int
_) <- IORef (IntMap (Int, Int), Map (Int, Int) Int)
-> IO (IntMap (Int, Int), Map (Int, Int) Int)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (Int, Int), Map (Int, Int) Int)
svDefs Solver
solver)
    [(Int, (Int, Int))] -> ((Int, (Int, Int)) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Int, Int) -> [(Int, (Int, Int))]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Int, Int)
defs) (((Int, (Int, Int)) -> IO ()) -> IO ())
-> ((Int, (Int, Int)) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
a,(Int
a1,Int
a2)) -> do
      Solver -> FlatTerm -> Int -> IO ()
mergeFlatTerm Solver
solver (Int -> Int -> FlatTerm
FTApp Int
a1 Int
a2) Int
a

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

lookup :: Solver -> FSym -> FSym -> IO (Maybe Eqn1)
lookup :: Solver -> Int -> Int -> IO (Maybe Eqn1)
lookup Solver
solver Int
c1 Int
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 (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 <- Int -> IntMap (IntMap Eqn1) -> Maybe (IntMap Eqn1)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c1 IntMap (IntMap Eqn1)
tbl
     Int -> IntMap Eqn1 -> Maybe Eqn1
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c2 IntMap Eqn1
m

setLookup :: Solver -> FSym -> FSym -> Eqn1 -> IO ()
setLookup :: Solver -> Int -> Int -> Eqn1 -> IO ()
setLookup Solver
solver Int
a1 Int
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)
-> Int
-> IntMap Eqn1
-> IntMap (IntMap Eqn1)
-> IntMap (IntMap Eqn1)
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IntMap.insertWith IntMap Eqn1 -> IntMap Eqn1 -> IntMap Eqn1
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union Int
a1 (Int -> Eqn1 -> IntMap Eqn1
forall a. Int -> a -> IntMap a
IntMap.singleton Int
a2 Eqn1
eqn)
  Solver -> TrailItem -> IO ()
addToTrail Solver
solver (Int -> Int -> TrailItem
TrailSetLookup Int
a1 Int
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 -> Int -> IO Int
getRepresentative Solver
solver Int
c = UVec Int -> Int -> IO Int
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.unsafeRead (Solver -> UVec Int
svRepresentativeTable Solver
solver) Int
c

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

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

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

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

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

termToFlatTerm :: Solver -> Term -> IO FlatTerm
termToFlatTerm :: Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver (TApp Int
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)
mapM (Solver -> Term -> IO FlatTerm
termToFlatTerm Solver
solver) [Term]
xs
  let phi :: FlatTerm -> FlatTerm -> IO FlatTerm
phi FlatTerm
t FlatTerm
u = do
        Int
t' <- Solver -> FlatTerm -> IO Int
flatTermToFSym Solver
solver FlatTerm
t
        Int
u' <- Solver -> FlatTerm -> IO Int
flatTermToFSym Solver
solver FlatTerm
u
        FlatTerm -> IO FlatTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FlatTerm -> IO FlatTerm) -> FlatTerm -> IO FlatTerm
forall a b. (a -> b) -> a -> b
$ Int -> Int -> FlatTerm
FTApp Int
t' Int
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 (Int -> FlatTerm
FTConst Int
f) [FlatTerm]
xs'

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

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

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

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