| Copyright | (c) Masahiro Sakai 2015 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | unstable |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
ToySolver.EUF.EUFSolver
Description
Synopsis
- data Solver
- newSolver :: IO Solver
- type FSym = Int
- data Term = TApp FSym [Term]
- type ConstrID = Int
- class VAFun a where
- newFSym :: Solver -> IO FSym
- newFun :: VAFun a => Solver -> IO a
- newConst :: Solver -> IO Term
- assertEqual :: Solver -> Term -> Term -> IO ()
- assertEqual' :: Solver -> Term -> Term -> Maybe ConstrID -> IO ()
- assertNotEqual :: Solver -> Term -> Term -> IO ()
- assertNotEqual' :: Solver -> Term -> Term -> Maybe ConstrID -> IO ()
- check :: Solver -> IO Bool
- areEqual :: Solver -> Term -> Term -> IO Bool
- explain :: Solver -> Maybe (Term, Term) -> IO 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 #