CVC3  2.4.1
theory_uf.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_uf.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Fri Jan 17 18:25:40 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_uf_h_
22 #define _cvc3__include__theory_uf_h_
23 
24 #include "theory.h"
25 #include "cdmap.h"
26 
27 namespace CVC3 {
28 
29 class UFProofRules;
30 
31  //! Local kinds for transitive closure of binary relations
32  typedef enum {
34  OLD_ARROW // for backward compatibility with old function declarations
35  } UFKinds;
36 
37 /*****************************************************************************/
38 /*!
39  *\class TheoryUF
40  *\ingroup Theories
41  *\brief This theory handles uninterpreted functions.
42  *
43  * Author: Clark Barrett
44  *
45  * Created: Sat Feb 8 14:51:19 2003
46  */
47 /*****************************************************************************/
48 class TheoryUF :public Theory {
50  //! Flag to include function applications to the concrete model
51  const bool& d_applicationsInModel;
52 
53  // For computing transitive closure of binary relations
54  typedef struct TCMapPair {
57  } TCMapPair;
58 
60 
61  //! Backtracking list of function applications
62  /*! Used for building concrete models and beta-reducing
63  * lambda-expressions. */
65  //! Pointer to the last unprocessed element (for lambda expansions)
67  //! The pointers to the last unprocessed shared pair
69  //! The set of all shared terms
71 
72 public:
73  TheoryUF(TheoryCore* core);
74  ~TheoryUF();
75 
76  // Trusted method that creates the proof rules class (used in constructor).
77  // Implemented in uf_theorem_producer.cpp
79 
80  // Theory interface
81  void addSharedTerm(const Expr& e);
82  void assertFact(const Theorem& e);
83  void checkSat(bool fullEffort);
84  Theorem rewrite(const Expr& e);
85  void setup(const Expr& e);
86  void update(const Theorem& e, const Expr& d);
87  void checkType(const Expr& e);
89  bool enumerate, bool computeSize);
90  void computeType(const Expr& e);
91  Type computeBaseType(const Type& t);
92  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
93  void computeModel(const Expr& e, std::vector<Expr>& vars);
94  Expr computeTCC(const Expr& e);
95  virtual Expr parseExprOp(const Expr& e);
96  ExprStream& print(ExprStream& os, const Expr& e);
97 
98  //! Create a new LAMBDA-abstraction
99  Expr lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
100  //! Create a transitive closure expression
101  Expr transClosureExpr(const std::string& name,
102  const Expr& e1, const Expr& e2);
103 private:
104  void printSmtLibShared(ExprStream& os, const Expr& e);
105 };
106 
107 }
108 
109 #endif