| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Language.REST.KBO
Synopsis
- kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO
- kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool
Documentation
kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO Source #
OCA for a quasi-order extension to the Knuth-Bendix ordering
kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool Source #
kboGTE t u returns the SMT expression describing constraints
on the weights of function symbols such that t is greater than u
in the KBO ordering.