21 #ifndef _cvc3__include__theory_datatype_h_
22 #define _cvc3__include__theory_datatype_h_
30 class DatatypeProofRules;
80 unsigned position,
bool positive);
93 virtual void checkSat(
bool fullEffort);
100 bool enumerate,
bool computeSize);
109 const std::vector<std::string>& constructors,
110 const std::vector<std::vector<std::string> >& selectors,
111 const std::vector<std::vector<Expr> >& types);
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);
120 const std::vector<Expr>& args);