CVC3  2.4.1
uf_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file uf_proof_rules.h
4  *\brief Abstract interface for uninterpreted function/predicate proof rules
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Tue Aug 31 23:12:01 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: UFProofRules
20  *
21  */
22 /*****************************************************************************/
23 
24 #ifndef _cvc3__theory_uf__uf_proof_rules_h_
25 #define _cvc3__theory_uf__uf_proof_rules_h_
26 
27 namespace CVC3 {
28 
29  class Expr;
30  class Theorem;
31 
32  class UFProofRules {
33  public:
34  // Destructor
35  virtual ~UFProofRules() { }
36 
37  ////////////////////////////////////////////////////////////////////
38  // Proof rules
39  ////////////////////////////////////////////////////////////////////
40 
41  virtual Theorem relToClosure(const Theorem& rel) = 0;
42  virtual Theorem relTrans(const Theorem& t1, const Theorem& t2) = 0;
43 
44  //! Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
45  virtual Theorem applyLambda(const Expr& e) = 0;
46  //! Replace LETDECL in the operator with the definition
47  virtual Theorem rewriteOpDef(const Expr& e) = 0;
48 
49  }; // end of class UFProofRules
50 
51 } // end of namespace CVC3
52 
53 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem applyLambda(const Expr &e)=0
Beta reduction: |- (lambda x. f(x))(arg) = f(arg)
virtual Theorem relToClosure(const Theorem &rel)=0
virtual ~UFProofRules()
Definition: expr.cpp:35
virtual Theorem relTrans(const Theorem &t1, const Theorem &t2)=0
virtual Theorem rewriteOpDef(const Expr &e)=0
Replace LETDECL in the operator with the definition.