ToySolver.EUF.CongruenceClosure

• 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

The Solver type

data Solver

newSolver :: IO Solver

Problem description

type FSym = Int

data Term

Constructors

TApp FSym [Term]

Instances

Eq Term

Defined in ToySolver.EUF.CongruenceClosure

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Ord Term

Defined in ToySolver.EUF.CongruenceClosure

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Show Term

Defined in ToySolver.EUF.CongruenceClosure

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

VAFun Term

Defined in ToySolver.EUF.CongruenceClosure

Methods

withVArgs :: ([Term] -> Term) -> Term

VAFun a => VAFun (Term -> a)

Defined in ToySolver.EUF.CongruenceClosure

Methods

withVArgs :: ([Term] -> Term) -> Term -> a

data FlatTerm

Constructors

FTConst !FSym

FTApp !FSym !FSym

Instances

Eq FlatTerm

Defined in ToySolver.EUF.CongruenceClosure

Methods

(==) :: FlatTerm -> FlatTerm -> Bool

(/=) :: FlatTerm -> FlatTerm -> Bool

Ord FlatTerm

Defined in ToySolver.EUF.CongruenceClosure

Methods

compare :: FlatTerm -> FlatTerm -> Ordering

(<) :: FlatTerm -> FlatTerm -> Bool

(<=) :: FlatTerm -> FlatTerm -> Bool

(>) :: FlatTerm -> FlatTerm -> Bool

(>=) :: FlatTerm -> FlatTerm -> Bool

max :: FlatTerm -> FlatTerm -> FlatTerm

min :: FlatTerm -> FlatTerm -> FlatTerm

Show FlatTerm

Defined in ToySolver.EUF.CongruenceClosure

Methods

showsPrec :: Int -> FlatTerm -> ShowS

show :: FlatTerm -> String

showList :: [FlatTerm] -> ShowS

type ConstrID = Int

newFSym :: Solver -> IO FSym

class VAFun a where

Methods

withVArgs :: ([Term] -> Term) -> a

Instances

VAFun Term

Defined in ToySolver.EUF.CongruenceClosure

Methods

withVArgs :: ([Term] -> Term) -> Term

VAFun a => VAFun (Term -> a)

Defined in ToySolver.EUF.CongruenceClosure

Methods

withVArgs :: ([Term] -> Term) -> Term -> a

newFun :: VAFun a => Solver -> IO a

newConst :: Solver -> IO Term

merge :: Solver -> Term -> Term -> IO ()

merge' :: Solver -> Term -> Term -> Maybe ConstrID -> IO ()

mergeFlatTerm :: Solver -> FlatTerm -> FSym -> IO ()

mergeFlatTerm' :: Solver -> FlatTerm -> FSym -> Maybe ConstrID -> IO ()

Query

areCongruent :: Solver -> Term -> Term -> IO Bool

areCongruentFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO Bool

Explanation

explain :: Solver -> Term -> Term -> IO (Maybe IntSet)

explainFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO (Maybe IntSet)

explainConst :: Solver -> FSym -> FSym -> IO (Maybe IntSet)

Model Construction

type Entity = Int

type EntityTuple = [Entity]

data Model

Constructors

Model

Fields

• mUniverse :: !IntSet
• mFunctions :: !(IntMap (Map EntityTuple Entity))
• mUnspecified :: !Entity
• mEquivClasses :: [(Set Term, Entity)]

Instances

Show Model

Defined in ToySolver.EUF.CongruenceClosure

Methods

showsPrec :: Int -> Model -> ShowS

show :: Model -> String

showList :: [Model] -> ShowS

getModel :: Solver -> IO Model

eval :: Model -> Term -> Entity

evalAp :: Model -> FSym -> [Entity] -> Entity

Backtracking

pushBacktrackPoint :: Solver -> IO ()

popBacktrackPoint :: Solver -> IO ()

Low-level operations

termToFlatTerm :: Solver -> Term -> IO FlatTerm

termToFSym :: Solver -> Term -> IO FSym

fsymToTerm :: Solver -> FSym -> IO Term

fsymToFlatTerm :: Solver -> FSym -> IO FlatTerm

flatTermToFSym :: Solver -> FlatTerm -> IO FSym