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

Copyright	(c) Masahiro Sakai 2012
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

ToySolver.CongruenceClosure

Description

References:

R. Nieuwenhuis and A. Oliveras, "Fast congruence closure and extensions," Information and Computation, vol. 205, no. 4, pp. 557-580, Apr. 2007. http://www.lsi.upc.edu/~oliveras/espai/papers/IC.pdf

Documentation

data Solver Source

type Var = Int Source

data FlatTerm Source

Constructors

FTConst Var
FTApp Var Var

Instances

Eq FlatTerm
Ord FlatTerm
Show FlatTerm

newSolver :: IO Solver Source

newVar :: Solver -> IO Var Source

merge :: Solver -> (FlatTerm, Var) -> IO () Source

areCongruent :: Solver -> FlatTerm -> FlatTerm -> IO Bool Source