toysolver-0.7.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2012 2015
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010
Extensions
  • ScopedTypeVariables
  • OverloadedStrings
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • ExplicitForAll

ToySolver.EUF.FiniteModelFinder

Description

A simple model finder.

References:

Synopsis

Formula types

type Var = InternedText Source #

Variable

type FSym = InternedText Source #

Function Symbol

type PSym = InternedText Source #

Predicate Symbol

data GenLit a Source #

Generalized literal type parameterized by atom type

Constructors

Pos a 
Neg a 

Instances

Instances details
Eq a => Eq (GenLit a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

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

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

Ord a => Ord (GenLit a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

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) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

showsPrec :: Int -> GenLit a -> ShowS #

show :: GenLit a -> String #

showList :: [GenLit a] -> ShowS #

Complement (GenLit a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

notB :: GenLit a -> GenLit a Source #

data Term Source #

Term

Constructors

TmApp FSym [Term] 
TmVar Var 

Instances

Instances details
Eq Term Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

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

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

Ord Term Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

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 Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

data Atom Source #

Constructors

PApp PSym [Term] 

Instances

Instances details
Eq Atom Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

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

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

Ord Atom Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

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 Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

showsPrec :: Int -> Atom -> ShowS #

show :: Atom -> String #

showList :: [Atom] -> ShowS #

type Clause = [Lit] Source #

data GenFormula a Source #

Instances

Instances details
Eq a => Eq (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

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

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

Ord a => Ord (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Show a => Show (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Boolean (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Complement (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

Methods

notB :: GenFormula a -> GenFormula a Source #

MonotoneBoolean (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

IfThenElse (GenFormula a) (GenFormula a) Source # 
Instance details

Defined in ToySolver.EUF.FiniteModelFinder

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

type Entity = Int Source #

Element of model.

showEntity :: Entity -> String Source #

print entity

Main function