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

data FlatTerm
  = FTConst !FSym
  | FTApp !FSym !FSym
  deriving (Eq 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
Ord, FlatTerm -> FlatTerm -> Bool
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, FSym -> FlatTerm -> ShowS
[FlatTerm] -> ShowS
FlatTerm -> String
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FlatTerm] -> ShowS
$cshowList :: [FlatTerm] -> ShowS
show :: FlatTerm -> String
$cshow :: FlatTerm -> String
showsPrec :: FSym -> FlatTerm -> ShowS
$cshowsPrec :: FSym -> 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
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
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
Ord, FSym -> Eqn0 -> ShowS
[Eqn0] -> ShowS
Eqn0 -> String
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Eqn0] -> ShowS
$cshowList :: [Eqn0] -> ShowS
show :: Eqn0 -> String
$cshow :: Eqn0 -> String
showsPrec :: FSym -> Eqn0 -> ShowS
$cshowsPrec :: FSym -> 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
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
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
Ord, FSym -> Eqn1 -> ShowS
[Eqn1] -> ShowS
Eqn1 -> String
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Eqn1] -> ShowS
$cshowList :: [Eqn1] -> ShowS
show :: Eqn1 -> String
$cshow :: Eqn1 -> String
showsPrec :: FSym -> Eqn1 -> ShowS
$cshowsPrec :: FSym -> 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
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Class] -> ShowS
$cshowList :: [Class] -> ShowS
show :: Class -> String
$cshow :: Class -> String
showsPrec :: FSym -> Class -> ShowS
$cshowsPrec :: FSym -> Class -> ShowS
Show)

instance Semigroup Class where
  Class
xs <> :: Class -> Class -> Class
<> Class
ys = FSym -> Class -> Class -> Class
ClassUnion (Class -> FSym
classSize Class
xs 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 forall a. a -> [a] -> [a]
:)
    f (ClassUnion FSym
_ Class
xs Class
ys) = Class -> [FSym] -> [FSym]
f Class
xs 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 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     <- forall a. a -> IO (IORef a)
newIORef (forall a. IntMap a
IntMap.empty, forall k a. Map k a
Map.empty)
  UVec FSym
rep      <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec Class
classes  <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  IORef (IntMap (FSym, Eqn))
parent   <- forall a. a -> IO (IORef a)
newIORef forall a. IntMap a
IntMap.empty
  IORef (IntMap [(Eqn1, FSym, FSym)])
useList  <- forall a. a -> IO (IORef a)
newIORef forall a. IntMap a
IntMap.empty
  IORef (IntMap (IntMap Eqn1))
lookup   <- forall a. a -> IO (IORef a)
newIORef forall a. IntMap a
IntMap.empty

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

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

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

  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svRepresentativeTable Solver
solver) FSym
v
  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)
  forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) (forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
v [])
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svERepresentativeTable Solver
solver) FSym
v
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec Class
svEClassList Solver
solver) forall a. HasCallStack => a
undefined
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec FSym
svEHighestNodeTable Solver
solver) FSym
v
  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 = forall a. VAFun a => ([Term] -> Term) -> a
withVArgs (\[Term]
xs -> [Term] -> Term
k (Term
x 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
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. VAFun a => ([Term] -> Term) -> a
withVArgs (FSym -> [Term] -> Term
TApp FSym
c)

newConst :: Solver -> IO Term
newConst :: Solver -> IO Term
newConst = 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 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 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 (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 forall a b. (a -> b) -> a -> b
$ 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
          forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) forall a b. (a -> b) -> a -> b
$
            forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
gen) forall a. a -> [a] -> [a]
:) FSym
a1' forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
gen) 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 <- forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> Vec Eqn
svPending Solver
solver)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
n forall a. Eq a => a -> a -> Bool
== FSym
0) forall a b. (a -> b) -> a -> b
$ do
        Eqn -> IO ()
processEqn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a' forall a. Eq a => a -> a -> Bool
== FSym
b') forall a b. (a -> b) -> a -> b
$ do
        Class
classA <- 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 <- 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) <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          if Class -> FSym
classSize Class
classA 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
      forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
classA forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
        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'
      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 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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver)
      [(Eqn1, FSym, FSym)]
useList_a' <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IntMap [(Eqn1, FSym, FSym)]
useList forall a. IntMap a -> FSym -> a
IntMap.! FSym
a') 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 forall a. Ord a => a -> a -> Bool
<= FSym
lv Bool -> Bool -> Bool
&& FSym
lv2_gen2 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
          forall a. HasCallStack => Bool -> a -> a
assert (FSym
b' forall a. Eq a => a -> a -> Bool
== FSym
c1' Bool -> Bool -> Bool
|| FSym
b' forall a. Eq a => a -> a -> Bool
== FSym
c2') forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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
              forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust ((Eqn1
eq1, FSym
lv, FSym
lv_gen) forall a. a -> [a] -> [a]
:) FSym
b'
              forall (m :: * -> *) a. Monad m => a -> m a
return ()
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else do
          -- out-of-date entry
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap [(Eqn1, FSym, FSym)])
svUseList Solver
solver) (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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver)
            forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver) (forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
d (FSym
c, Eqn
c_eq_d) IntMap (FSym, Eqn)
tbl)
            case forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
d IntMap (FSym, Eqn)
tbl of
              Maybe (FSym, Eqn)
Nothing -> 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
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FlatTerm
u1 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) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FSym -> FlatTerm
FTConst 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) -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM FSym -> FlatTerm
FTConst forall a b. (a -> b) -> a -> b
$ Solver -> FSym -> IO FSym
getRepresentative Solver
solver FSym
a
    Maybe Eqn1
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkInvariant Solver
solver = do
  FSym
nv <- Solver -> IO FSym
getNFSyms Solver
solver

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

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

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

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

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

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) forall a b. (a -> b) -> a -> b
$ \FSym
b -> do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntSet -> [FSym]
IntSet.toList IntSet
representatives) 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 -> 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
b forall a. Eq a => a -> a -> Bool
== FSym
a1' Bool -> Bool -> Bool
&& FSym
c forall a. Eq a => a -> a -> Bool
== FSym
a2') forall a b. (a -> b) -> a -> b
$
            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
  forall (m :: * -> *) a.
Monad m =>
a -> (a -> Bool) -> (a -> a) -> (a -> m ()) -> m ()
forLoop FSym
0 (forall a. Ord a => a -> a -> Bool
<FSym
n) (forall a. Num a => a -> a -> a
+FSym
1) forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    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
    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)
    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 <- 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 <- 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 forall a. Ord a => a -> a -> Bool
< Class -> FSym
classSize Class
classB then do
            forall (m :: * -> *) a. Monad m => a -> m a
return (FSym
b', Class
classA, Class
classB)
          else
            forall (m :: * -> *) a. Monad m => a -> m a
return (FSym
a', Class
classB, Class
classA)
        forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
classA forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
          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''
        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 forall a. Semigroup a => a -> a -> a
<> Class
classB)
        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

  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver)
  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 <- forall a. a -> IO (IORef a)
newIORef IntSet
IntSet.empty

  let loop :: IO Bool
loop = do
        FSym
n <- forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> Vec (FSym, FSym)
svEPendingProofs Solver
solver)
        if FSym
n forall a. Eq a => a -> a -> Bool
== FSym
0 then
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        else do
          (FSym
a,FSym
b) <- 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 -> 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 =
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
a forall a. Eq a => a -> a -> Bool
== FSym
c) 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
                    forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result (Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid 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
                    forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef IntSet
result ((Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid1 forall a. Semigroup a => a -> a -> a
<> Maybe FSym -> IntSet
maybeToIntSet Maybe FSym
cid2) forall a. Semigroup a => a -> a -> a
<>)
                    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)
                    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 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 forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef IntSet
result
  else forall (m :: * -> *) a. Monad m => a -> m a
return 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
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Model] -> ShowS
$cshowList :: [Model] -> ShowS
show :: Model -> String
$cshow :: Model -> String
showsPrec :: FSym -> Model -> ShowS
$cshowsPrec :: FSym -> Model -> ShowS
Show)

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

  IntMap (IntMap Eqn1)
lookups <- 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 = forall a. (a -> a -> a) -> [(FSym, a)] -> IntMap a
IntMap.fromListWith forall a. Ord a => Set a -> Set a -> Set a
Set.union forall a b. (a -> b) -> a -> b
$
        [ (IntMap FSym
repr forall a. IntMap a -> FSym -> a
IntMap.! FSym
c, forall a. a -> Set a
Set.singleton (IntMap FSym
repr forall a. IntMap a -> FSym -> a
IntMap.! FSym
a, IntMap FSym
repr forall a. IntMap a -> FSym -> a
IntMap.! FSym
b))
        | (FSym
a,IntMap Eqn1
m) <- forall a. IntMap a -> [(FSym, a)]
IntMap.toList IntMap (IntMap Eqn1)
lookups, (FSym
b, Eqn1 Maybe FSym
_ FSym
_ FSym
_ FSym
c) <- 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 <- forall a. IntMap a -> [a]
IntMap.elems IntMap (Set (FSym, FSym))
appRel, (FSym
b,FSym
_) <- forall a. Set a -> [a]
Set.toList Set (FSym, FSym)
xs]

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

      xs2 :: IntMap (Map EntityTuple Entity)
      xs2 :: IntMap (Map [FSym] FSym)
xs2 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k a. k -> a -> Map k a
Map.singleton []) (IntMap FSym
repr 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 = forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith 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 = forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [[FSym] -> IntSet
IntSet.fromList (FSym
y forall a. a -> [a] -> [a]
: [FSym]
xs) | Map [FSym] FSym
m <- forall a. IntMap a -> [a]
IntMap.elems IntMap (Map [FSym] FSym)
funcs, ([FSym]
xs,FSym
y) <- forall k a. Map k a -> [(k, a)]
Map.toList Map [FSym] FSym
m]

  [(Set Term, FSym)]
classes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (IntSet -> [FSym]
IntSet.toList IntSet
used) forall a b. (a -> b) -> a -> b
$ \FSym
a -> do
    Class
classA <- 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' <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> FSym -> IO Term
fsymToTerm Solver
solver) (Class -> [FSym]
classToList Class
classA)
    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) forall a b. (a -> b) -> a -> b
$ [FSym] -> IntSet
IntSet.fromList [FSym
0 .. IntSet -> FSym
IntSet.size IntSet
used forall a. Num a => a -> a -> a
- FSym
1]

      to_univ2' :: IntMap Entity
      to_univ2' :: IntMap FSym
to_univ2' = forall a. [(FSym, a)] -> IntMap a
IntMap.fromList (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' forall a. IntMap a -> FSym -> a
IntMap.!)

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

  forall (m :: * -> *) a. Monad m => a -> m a
return 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 (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 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 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
forall a.
(FSym -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TrailItem] -> ShowS
$cshowList :: [TrailItem] -> ShowS
show :: TrailItem -> String
$cshow :: TrailItem -> String
showsPrec :: FSym -> TrailItem -> ShowS
$cshowsPrec :: FSym -> 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
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
lv forall a. Eq a => a -> a -> Bool
/= FSym
0) forall a b. (a -> b) -> a -> b
$ do
    seq :: forall a b. a -> b -> b
seq TrailItem
item forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> (e -> e) -> IO ()
Vec.unsafeModify (Solver -> Vec [TrailItem]
svTrail Solver
solver) (FSym
lv forall a. Num a => a -> a -> a
- FSym
1) (TrailItem
item forall a. a -> [a] -> [a]
:)

getCurrentLevel :: Solver -> IO Level
getCurrentLevel :: Solver -> IO FSym
getCurrentLevel Solver
solver = 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 = 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
  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 <- forall (a :: * -> * -> *) e. GenericVec a e -> IO FSym
Vec.getSize (Solver -> UVec FSym
svLevelGen Solver
solver)
  if FSym
lv forall a. Ord a => a -> a -> Bool
< FSym
size then do
    FSym
g <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> UVec FSym
svLevelGen Solver
solver) FSym
lv
    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 forall a. Num a => a -> a -> a
+ FSym
1)
  else
    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
  forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver) Bool
True
  [TrailItem]
xs <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec [TrailItem]
svTrail Solver
solver)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TrailItem]
xs forall a b. (a -> b) -> a -> b
$ \TrailItem
item -> do
    case TrailItem
item of
      TrailSetLookup FSym
a' FSym
b' -> do
        forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver) (forall a. (a -> a) -> FSym -> IntMap a -> IntMap a
IntMap.adjust (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 <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> FSym -> IO e
Vec.unsafeRead (Solver -> Vec Class
svClassList Solver
solver) FSym
b'
        forall (m :: * -> *). Monad m => Class -> (FSym -> m ()) -> m ()
classForM_ Class
origClassA forall a b. (a -> b) -> a -> b
$ \FSym
c -> do
          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'
        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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver)
              forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver) (forall a. (a -> Maybe a) -> FSym -> IntMap a -> IntMap a
IntMap.update (forall a b. a -> b -> a
const Maybe (FSym, Eqn)
p) FSym
c IntMap (FSym, Eqn)
tbl)
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FSym
c forall a. Eq a => a -> a -> Bool
== FSym
a) forall a b. (a -> b) -> a -> b
$ do
                let (FSym
d, Eqn
c_eq_d) = IntMap (FSym, Eqn)
tbl forall a. IntMap a -> FSym -> a
IntMap.! FSym
c
                FSym -> Maybe (FSym, Eqn) -> IO ()
loop FSym
d (forall a. a -> Maybe a
Just (FSym
c, Eqn
c_eq_d))
        FSym -> Maybe (FSym, Eqn) -> IO ()
loop FSym
origRootA forall a. Maybe a
Nothing

initAfterBacktracking :: Solver -> IO ()
initAfterBacktracking :: Solver -> IO ()
initAfterBacktracking Solver
solver = do
  Bool
b <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b forall a b. (a -> b) -> a -> b
$ do
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
svIsAfterBacktracking Solver
solver) Bool
False
    (IntMap (FSym, FSym)
defs, Map (FSym, FSym) FSym
_) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver)
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(FSym, a)]
IntMap.toList IntMap (FSym, FSym)
defs) 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
     IntMap Eqn1
m <- forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
c1 IntMap (IntMap Eqn1)
tbl
     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
  forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef (IntMap (IntMap Eqn1))
svLookupTable Solver
solver) forall a b. (a -> b) -> a -> b
$
    forall a. (a -> a -> a) -> FSym -> a -> IntMap a -> IntMap a
IntMap.insertWith forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union FSym
a1 (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 = 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 = 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, Eqn))
svParent Solver
solver
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = 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
  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 -> 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
          forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. a -> Maybe a
Just 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return 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' <- 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
        FSym
t' <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
t
        FSym
u' <- Solver -> FlatTerm -> IO FSym
flatTermToFSym Solver
solver FlatTerm
u
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FSym -> FSym -> FlatTerm
FTApp FSym
t' FSym
u'
  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) = 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) <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver
  FSym
a <- case 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return FSym
a
         Maybe FSym
Nothing -> do
           FSym
a <- Solver -> IO FSym
newFSym Solver
solver
           forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver) (forall a. FSym -> a -> IntMap a -> IntMap a
IntMap.insert FSym
a (FSym
c,FSym
d) IntMap (FSym, FSym)
defs1, 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
           forall (m :: * -> *) a. Monad m => a -> m a
return FSym
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
_) <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ Solver -> IORef (IntMap (FSym, FSym), Map (FSym, FSym) FSym)
svDefs Solver
solver
  case forall a. FSym -> IntMap a -> Maybe a
IntMap.lookup FSym
a IntMap (FSym, FSym)
defs1 of
    Just (FSym
c,FSym
d) -> forall (m :: * -> *) a. Monad m => a -> m a
return (FSym -> FSym -> FlatTerm
FTApp FSym
c FSym
d)
    Maybe (FSym, FSym)
Nothing -> 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 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
_) <- forall a. IORef a -> IO a
readIORef 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 (forall a. [a] -> [a]
reverse [Term]
xs)
      convert' :: FSym -> (FSym, [Term])
      convert' :: FSym -> (FSym, [Term])
convert' FSym
a =
        case 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 forall a. a -> [a] -> [a]
: [Term]
xs)
  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