| 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.FiniteModelFinder
Description
A simple model finder.
References:
- Koen Claessen and Niklas Sörensson. New Techniques that Improve MACE-style Finite Model Finding. CADE-19. 2003. http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf
Synopsis
- type Var = InternedText
- type FSym = InternedText
- type PSym = InternedText
- data GenLit a
- data Term
- data Atom = PApp PSym [Term]
- type Lit = GenLit Atom
- type Clause = [Lit]
- type Formula = GenFormula Atom
- data GenFormula a
- = T
- | F
- | Atom a
- | And (GenFormula a) (GenFormula a)
- | Or (GenFormula a) (GenFormula a)
- | Not (GenFormula a)
- | Imply (GenFormula a) (GenFormula a)
- | Equiv (GenFormula a) (GenFormula a)
- | Forall Var (GenFormula a)
- | Exists Var (GenFormula a)
- toSkolemNF :: forall m. Monad m => (Var -> Int -> m FSym) -> Formula -> m [Clause]
- data Model = Model {
- mUniverse :: [Entity]
- mRelations :: Map PSym (Set EntityTuple)
- mFunctions :: Map FSym (Map EntityTuple Entity)
- type Entity = Int
- type EntityTuple = [Entity]
- showModel :: Model -> [String]
- showEntity :: Entity -> String
- evalFormula :: Model -> Formula -> Bool
- evalAtom :: Model -> Map Var Entity -> Atom -> Bool
- evalTerm :: Model -> Map Var Entity -> Term -> Entity
- evalLit :: Model -> Map Var Entity -> Lit -> Bool
- evalClause :: Model -> Map Var Entity -> Clause -> Bool
- evalClauses :: Model -> Map Var Entity -> [Clause] -> Bool
- evalClausesU :: Model -> [Clause] -> Bool
- findModel :: Int -> [Clause] -> IO (Maybe Model)
Formula types
type Var = InternedText Source #
Variable
type FSym = InternedText Source #
Function Symbol
type PSym = InternedText Source #
Predicate Symbol
Generalized literal type parameterized by atom type
type Formula = GenFormula Atom Source #
data GenFormula a Source #
Constructors
| T | |
| F | |
| Atom a | |
| And (GenFormula a) (GenFormula a) | |
| Or (GenFormula a) (GenFormula a) | |
| Not (GenFormula a) | |
| Imply (GenFormula a) (GenFormula a) | |
| Equiv (GenFormula a) (GenFormula a) | |
| Forall Var (GenFormula a) | |
| Exists Var (GenFormula a) |
Instances
toSkolemNF :: forall m. Monad m => (Var -> Int -> m FSym) -> Formula -> m [Clause] Source #
normalize a formula into a skolem normal form.
TODO:
- Tseitin encoding
Model types
Constructors
| Model | |
Fields
| |
type EntityTuple = [Entity] Source #
showEntity :: Entity -> String Source #
print entity