23 #ifndef _cvc3__theory_uf__uf_theorem_producer_h_
24 #define _cvc3__theory_uf__uf_theorem_producer_h_
Data structure of expressions in CVC3.
Theorem rewriteOpDef(const Expr &e)
Replace LETDECL in the operator with the definition.
This theory handles uninterpreted functions.
UFTheoremProducer(TheoremManager *tm, TheoryUF *theoryUF)
Constructor.
Theorem relTrans(const Theorem &t1, const Theorem &t2)
Theorem applyLambda(const Expr &e)
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
Abstract interface for uninterpreted function/predicate proof rules.
Theorem relToClosure(const Theorem &rel)