toysolver-0.2.0: Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc

Copyright(c) Masahiro Sakai 2012
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable (TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables)
Safe HaskellNone
LanguageHaskell2010

ToySolver.FOLModelFinder

Contents

Description

A simple model finder.

References:

Synopsis

Formula types

type Var = String Source

Variable

type FSym = String Source

Function Symbol

type PSym = String Source

Predicate Symbol

data GenLit a Source

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) 
Complement (GenLit a) 

data Term Source

Term

Constructors

TmApp FSym [Term] 
TmVar Var 

Instances

data Atom Source

Constructors

PApp PSym [Term] 

Instances

type Clause = [Lit] Source

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

normalize a formula into a skolem normal form.

TODO:

  • Tseitin encoding

Model types

data Model Source

Constructors

Model 

type Entity = Int Source

Element of model.

showEntity :: Entity -> String Source

print entity

Main function