ToySolver.FOLModelFinder

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

Formula types

type Var = String

Variable

type FSym = String

Function Symbol

type PSym = String

Predicate Symbol

data GenLit a

Generalized literal type parameterized by atom type

Constructors

Pos a

Neg a

Instances

Eq a => Eq (GenLit a)

Ord a => Ord (GenLit a)

Show a => Show (GenLit a)

data Term

Term

Constructors

TmApp FSym [Term]

TmVar Var

Instances

Eq Term

Ord Term

Show Term

data Atom

Constructors

PApp PSym [Term]

Instances

Eq Atom

Ord Atom

Show Atom

type Lit = GenLit Atom

type Clause = [Lit]

type Formula = GenFormula Atom

data GenFormula a

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

Eq a => Eq (GenFormula a)

Ord a => Ord (GenFormula a)

Show a => Show (GenFormula a)

toSkolemNF :: forall m. Monad m => (String -> Int -> m FSym) -> Formula -> m [Clause]

normalize a formula into a skolem normal form.

TODO:

• Tseitin encoding

Model types

data Model

Constructors

Model

Fields

mUniverse :: [Entity]

mRelations :: Map PSym [[Entity]]

mFunctions :: Map FSym [([Entity], Entity)]

type Entity = Int

Element of model.

showModel :: Model -> [String]

showEntity :: Entity -> String

print entity

Main function

findModel :: Int -> [Clause] -> IO (Maybe Model)