ToySolver.EUF.EUFSolver

The Solver type

data Solver

newSolver

Problem description

type FSym

data Term

type ConstrID

class VAFun a

newFSym

newFun

newConst

assertEqual

assertEqual'

assertNotEqual

assertNotEqual'

Query

check

areEqual

Explanation

explain

Model Construction

type Entity

type EntityTuple

data Model

getModel

eval

evalAp

Backtracking

pushBacktrackPoint

popBacktrackPoint

Low-level operations

termToFlatTerm

termToFSym

fsymToTerm

fsymToFlatTerm

flatTermToFSym