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
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Definition: theory_uf.cpp:471
Data structure of expressions in CVC3.
Definition: expr.h:133
ExprMap< CDList< Theorem > * > appearsFirstMap
Definition: theory_uf.h:55
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
ExprMap< CDList< Theorem > * > appearsSecondMap
Definition: theory_uf.h:56
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Definition: theory_uf.cpp:1139
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Definition: theory_uf.cpp:236
CDO< size_t > d_sharedIdx2
Definition: theory_uf.h:68
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Definition: theory_uf.cpp:591
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
This theory handles uninterpreted functions.
Definition: theory_uf.h:48
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Definition: theory_uf.cpp:700
CDMap< Expr, bool > d_sharedTermsMap
The set of all shared terms.
Definition: theory_uf.h:70
virtual Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
Definition: theory_uf.cpp:1015
TheoryUF(TheoryCore *core)
Definition: theory_uf.cpp:42
CDList< Expr > d_funApplications
Backtracking list of function applications.
Definition: theory_uf.h:64
const bool & d_applicationsInModel
Flag to include function applications to the concrete model.
Definition: theory_uf.h:51
CDO< size_t > d_funApplicationsIdx
Pointer to the last unprocessed element (for lambda expansions)
Definition: theory_uf.h:66
void computeType(const Expr &e)
Compute and store the type of e.
Definition: theory_uf.cpp:417
void checkType(const Expr &e)
Check that e is a valid Type expr.
Definition: theory_uf.cpp:337
ExprMap< TCMapPair * > d_transClosureMap
Definition: theory_uf.h:59
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
Definition: theory_uf.cpp:491
CDO< size_t > d_sharedIdx1
The pointers to the last unprocessed shared pair.
Definition: theory_uf.h:68
Expr lambdaExpr(const std::vector< Expr > &vars, const Expr &body)
Create a new LAMBDA-abstraction.
Definition: theory_uf.cpp:1129
Expr transClosureExpr(const std::string &name, const Expr &e1, const Expr &e2)
Create a transitive closure expression.
Definition: theory_uf.cpp:1134
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
Definition: theory_uf.cpp:509
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
Definition: theory_uf.cpp:368
struct CVC3::TheoryUF::TCMapPair TCMapPair
UFProofRules * createProofRules()
Generic API for Theories plus methods commonly used by theories.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Definition: theory_uf.cpp:79
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Definition: theory_uf.cpp:257
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
Definition: expr.cpp:35
UFKinds
Local kinds for transitive closure of binary relations.
Definition: theory_uf.h:32
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Definition: theory_uf.cpp:156
void printSmtLibShared(ExprStream &os, const Expr &e)
Definition: theory_uf.cpp:657
UFProofRules * d_rules
Definition: theory_uf.h:49
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Definition: theory_uf.cpp:211