| Copyright | (c) Masahiro Sakai 2012 2015 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
| Extensions |
|
ToySolver.EUF.CongruenceClosure
Description
- 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
Synopsis
- data Solver
- newSolver :: IO Solver
- type FSym = Int
- data Term = TApp FSym [Term]
- data FlatTerm
- type ConstrID = Int
- newFSym :: Solver -> IO FSym
- class VAFun a where
- 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 ()
- areCongruent :: Solver -> Term -> Term -> IO Bool
- areCongruentFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO Bool
- explain :: Solver -> Term -> Term -> IO (Maybe IntSet)
- explainFlatTerm :: Solver -> FlatTerm -> FlatTerm -> IO (Maybe IntSet)
- explainConst :: Solver -> FSym -> FSym -> IO (Maybe IntSet)
- type Entity = Int
- type EntityTuple = [Entity]
- data Model = Model {
- mUniverse :: !IntSet
- mFunctions :: !(IntMap (Map EntityTuple Entity))
- mUnspecified :: !Entity
- mEquivClasses :: [(Set Term, Entity)]
- getModel :: Solver -> IO Model
- eval :: Model -> Term -> Entity
- evalAp :: Model -> FSym -> [Entity] -> Entity
- pushBacktrackPoint :: Solver -> IO ()
- popBacktrackPoint :: Solver -> IO ()
- 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
The Solver type
Problem description
Query
Explanation
Model Construction
type EntityTuple = [Entity] Source #
Constructors
| Model | |
Fields
| |
Backtracking
pushBacktrackPoint :: Solver -> IO () Source #
popBacktrackPoint :: Solver -> IO () Source #