CVC3
theory_datatype.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_datatype.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Dec 1 22:24:32 2004
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_datatype_h_
22 #define _cvc3__include__theory_datatype_h_
23 
24 #include "theory.h"
25 #include "smartcdo.h"
26 #include "cdmap.h"
27 
28 namespace CVC3 {
29 
30 class DatatypeProofRules;
31 
32 //! Local kinds for datatypes
33  typedef enum {
39  } DatatypeKinds;
40 
41 /*****************************************************************************/
42 /*!
43  *\class TheoryDatatype
44  *\ingroup Theories
45  *\brief This theory handles datatypes.
46  *
47  * Author: Clark Barrett
48  *
49  * Created: Wed Dec 1 22:27:12 2004
50  */
51 /*****************************************************************************/
52 class TheoryDatatype :public Theory {
53 protected:
55 
56  // maps DATATYPE expressions to map containing constructors for that datatype
58  // maps constructor to its selectors
60  // maps selector to a pair containing the constructor and the position of the selctor for that constructor
62  // maps tester to constructor that it matches
65 
67 
72  const bool& d_smartSplits;
74 
75 protected:
76  virtual void instantiate(const Expr& e, const Unsigned& u);
77  virtual void initializeLabels(const Expr& e, const Type& t);
78  virtual void mergeLabels(const Theorem& thm, const Expr& e1, const Expr& e2);
79  virtual void mergeLabels(const Theorem& thm, const Expr& e,
80  unsigned position, bool positive);
81 
82 public:
84  virtual ~TheoryDatatype();
85 
86  // Trusted method that creates the proof rules class (used in constructor).
87  // Implemented in datatype_theorem_producer.cpp
89 
90  // Theory interface
91  void addSharedTerm(const Expr& e);
92  void assertFact(const Theorem& e);
93  virtual void checkSat(bool fullEffort);
94  Theorem rewrite(const Expr& e);
95  virtual void setup(const Expr& e);
96  virtual void update(const Theorem& e, const Expr& d);
97  Theorem solve(const Theorem& e);
98  void checkType(const Expr& e);
100  bool enumerate, bool computeSize);
101  void computeType(const Expr& e);
102  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
103  Expr computeTCC(const Expr& e);
104  Expr parseExprOp(const Expr& e);
105  ExprStream& print(ExprStream& os, const Expr& e);
106 
107  // Returns Expr(DATATYPE_DECL datatype)
108  Expr dataType(const std::string& name,
109  const std::vector<std::string>& constructors,
110  const std::vector<std::vector<std::string> >& selectors,
111  const std::vector<std::vector<Expr> >& types);
112 
113  // Returns Expr(DATATYPE_DECL type_1, type_2, ...)
114  Expr dataType(const std::vector<std::string>& names,
115  const std::vector<std::vector<std::string> >& constructors,
116  const std::vector<std::vector<std::vector<std::string> > >& selectors,
117  const std::vector<std::vector<std::vector<Expr> > >& types);
118 
119  Expr datatypeConsExpr(const std::string& constructor,
120  const std::vector<Expr>& args);
121  Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
122  Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
123 
124  const std::pair<Expr,unsigned>& getSelectorInfo(const Expr& e);
125  Expr getConsForTester(const Expr& e);
126  unsigned getConsPos(const Expr& e);
127  Expr getConstant(const Type& t);
128  const Op& getReachablePredicate(const Type& t);
129  bool canCollapse(const Expr& e);
130 
131 };
132 
133 inline bool isDatatype(const Type& t)
134  { return t.getExpr().getKind() == DATATYPE; }
135 
136 inline bool isConstructor(const Expr& e)
137  { return (e.getKind() == CONSTRUCTOR && e.getType().arity()==1) ||
138  (e.isApply() && e.getOpKind() == CONSTRUCTOR); }
139 
140 inline bool isSelector(const Expr& e)
141  { return e.isApply() && e.getOpKind() == SELECTOR; }
142 
143 inline bool isTester(const Expr& e)
144  { return e.isApply() && e.getOpKind() == TESTER; }
145 
146 inline Expr getConstructor(const Expr& e)
147  { DebugAssert(isConstructor(e), "Constructor expected");
148  return e.isApply() ? e.getOpExpr() : e; }
149 
150 }
151 
152 #endif