CVC3  2.4.1
uf_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file uf_theorem_producer.h
4  *\brief TRUSTED implementation of uninterpreted function/predicate proof rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Tue Aug 31 23:14:54 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  * CLASS: UFTheoremProducer
20  *
21  */
22 /*****************************************************************************/
23 #ifndef _cvc3__theory_uf__uf_theorem_producer_h_
24 #define _cvc3__theory_uf__uf_theorem_producer_h_
25 
26 #include "uf_proof_rules.h"
27 #include "theorem_producer.h"
28 
29 namespace CVC3 {
30 
31  class TheoryUF;
32 
35  private:
36  public:
37  //! Constructor
39  TheoremProducer(tm), d_theoryUF(theoryUF) { }
40 
41  Theorem relToClosure(const Theorem& rel);
42  Theorem relTrans(const Theorem& t1, const Theorem& t2);
43  Theorem applyLambda(const Expr& e);
44  Theorem rewriteOpDef(const Expr& e);
45 
46  }; // end of class UFTheoremProducer
47 } // end of namespace CVC3
48 
49 #endif
50 
Data structure of expressions in CVC3.
Definition: expr.h:133
Theorem rewriteOpDef(const Expr &e)
Replace LETDECL in the operator with the definition.
This theory handles uninterpreted functions.
Definition: theory_uf.h:48
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)
Definition: expr.cpp:35