CVC3
2.4.1
|
#include <uf_theorem_producer.h>
CVC3::UFTheoremProducer::UFTheoremProducer | ( | TheoremManager * | tm, |
TheoryUF * | theoryUF | ||
) | [inline] |
Constructor.
Definition at line 38 of file uf_theorem_producer.h.
Implements CVC3::UFProofRules.
Definition at line 54 of file uf_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isApply(), CVC3::Expr::arity(), CLASS_NAME, CVC3::Expr::toString(), CVC3::Theorem::getProof(), CVC3::Expr::getOp(), CVC3::Op::getExpr(), CVC3::Expr::getName(), and CVC3::Theorem::getAssumptionsRef().
Implements CVC3::UFProofRules.
Definition at line 76 of file uf_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getOpKind(), CVC3::TRANS_CLOSURE, CVC3::Expr::arity(), CLASS_NAME, CVC3::Expr::toString(), CVC3::Expr::getOpExpr(), CVC3::Expr::getName(), CVC3::Theorem::getProof(), and CVC3::Expr::getOp().
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
Implements CVC3::UFProofRules.
Definition at line 114 of file uf_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isApply(), CVC3::Expr::getOpKind(), LAMBDA, CVC3::Expr::toString(), CVC3::Expr::getOpExpr(), CVC3::Expr::arity(), and CVC3::Expr::getKids().
Replace LETDECL in the operator with the definition.
Implements CVC3::UFProofRules.
Definition at line 149 of file uf_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isApply(), CVC3::Expr::toString(), CVC3::Expr::getOpExpr(), CVC3::Expr::getKind(), LETDECL, CVC3::Expr::arity(), CVC3::Expr::mkOp(), and CVC3::Expr::getKids().
TheoryUF* CVC3::UFTheoremProducer::d_theoryUF [private] |
Definition at line 34 of file uf_theorem_producer.h.