{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.EUF.CongruenceClosure
(
Solver
, newSolver
, FSym
, Term (..)
, FlatTerm (..)
, ConstrID
, newFSym
, VAFun (..)
, newFun
, newConst
, merge
, merge'
, mergeFlatTerm
, mergeFlatTerm'
, areCongruent
, areCongruentFlatTerm
, explain
, explainFlatTerm
, explainConst
, Entity
, EntityTuple
, Model (..)
, getModel
, eval
, evalAp
, pushBacktrackPoint
, popBacktrackPoint
, 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
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)
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)
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
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
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)))
, Solver -> Vec Eqn
svPending :: !(Vec.Vec Eqn)
, 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))
, 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
, svPending :: Vec Eqn
svPending = Vec Eqn
pending
, 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
, 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 ()
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
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')
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"
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
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
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
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')
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)
let
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)
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
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
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
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
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