ToySolver.EUF.FiniteModelFinder

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)

Methods

(==) :: GenLit a -> GenLit a -> Bool

(/=) :: GenLit a -> GenLit a -> Bool

Ord a => Ord (GenLit a)

Methods

compare :: GenLit a -> GenLit a -> Ordering

(<) :: GenLit a -> GenLit a -> Bool

(<=) :: GenLit a -> GenLit a -> Bool

(>) :: GenLit a -> GenLit a -> Bool

(>=) :: GenLit a -> GenLit a -> Bool

max :: GenLit a -> GenLit a -> GenLit a

min :: GenLit a -> GenLit a -> GenLit a

Show a => Show (GenLit a)

Methods

showsPrec :: Int -> GenLit a -> ShowS

show :: GenLit a -> String

showList :: [GenLit a] -> ShowS

Complement (GenLit a)

Methods

notB :: GenLit a -> GenLit a

data Term

Term

Constructors

TmApp FSym [Term]

TmVar Var

Instances

Eq Term

Methods

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

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

Ord Term

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

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

data Atom

Constructors

PApp PSym [Term]

Instances

Eq Atom

Methods

(==) :: Atom -> Atom -> Bool

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

Ord Atom

Methods

compare :: Atom -> Atom -> Ordering

(<) :: Atom -> Atom -> Bool

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

(>) :: Atom -> Atom -> Bool

(>=) :: Atom -> Atom -> Bool

max :: Atom -> Atom -> Atom

min :: Atom -> Atom -> Atom

Show Atom

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

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)

Methods

(==) :: GenFormula a -> GenFormula a -> Bool

(/=) :: GenFormula a -> GenFormula a -> Bool

Ord a => Ord (GenFormula a)

Methods

compare :: GenFormula a -> GenFormula a -> Ordering

(<) :: GenFormula a -> GenFormula a -> Bool

(<=) :: GenFormula a -> GenFormula a -> Bool

(>) :: GenFormula a -> GenFormula a -> Bool

(>=) :: GenFormula a -> GenFormula a -> Bool

max :: GenFormula a -> GenFormula a -> GenFormula a

min :: GenFormula a -> GenFormula a -> GenFormula a

Show a => Show (GenFormula a)

Methods

showsPrec :: Int -> GenFormula a -> ShowS

show :: GenFormula a -> String

showList :: [GenFormula a] -> ShowS

Boolean (GenFormula a)

Methods

(.=>.) :: GenFormula a -> GenFormula a -> GenFormula a

(.<=>.) :: GenFormula a -> GenFormula a -> GenFormula a

Complement (GenFormula a)

Methods

notB :: GenFormula a -> GenFormula a

MonotoneBoolean (GenFormula a)

Methods

true :: GenFormula a

false :: GenFormula a

(.&&.) :: GenFormula a -> GenFormula a -> GenFormula a

(.||.) :: GenFormula a -> GenFormula a -> GenFormula a

andB :: [GenFormula a] -> GenFormula a

orB :: [GenFormula a] -> GenFormula a

IfThenElse (GenFormula a) (GenFormula a)

Methods

ite :: GenFormula a -> GenFormula a -> GenFormula a -> 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 (Set EntityTuple)
• mFunctions :: Map FSym (Map EntityTuple Entity)

type Entity = Int

Element of model.

type EntityTuple = [Entity]

showModel :: Model -> [String]

showEntity :: Entity -> String

print entity

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

Main function

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