toysolver-0.5.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 (BangPatterns, ScopedTypeVariables, FlexibleInstances)
Safe HaskellNone
LanguageHaskell2010

ToySolver.EUF.CongruenceClosure

Contents

Description

References:

Synopsis

The Solver type

Problem description

type FSym = Int Source #

data Term Source #

Constructors

TApp FSym [Term] 

Instances

Eq Term Source # 

Methods

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

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

Ord Term Source # 

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 # 

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

VAFun Term Source # 

Methods

withVArgs :: ([Term] -> Term) -> Term Source #

VAFun a => VAFun (Term -> a) Source # 

Methods

withVArgs :: ([Term] -> Term) -> Term -> a Source #

class VAFun a where Source #

Minimal complete definition

withVArgs

Methods

withVArgs :: ([Term] -> Term) -> a Source #

Instances

VAFun Term Source # 

Methods

withVArgs :: ([Term] -> Term) -> Term Source #

VAFun a => VAFun (Term -> a) Source # 

Methods

withVArgs :: ([Term] -> Term) -> Term -> a Source #

newFun :: VAFun a => Solver -> IO a Source #

merge :: Solver -> Term -> Term -> IO () Source #

Query

Explanation

Model Construction

Backtracking

Low-level operations