00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__include__theory_datatype_h_
00022 #define _cvc3__include__theory_datatype_h_
00023
00024 #include "theory.h"
00025 #include "smartcdo.h"
00026 #include "cdmap.h"
00027
00028 namespace CVC3 {
00029
00030 class DatatypeProofRules;
00031
00032
00033 typedef enum {
00034 DATATYPE_DECL = 600,
00035 DATATYPE,
00036 CONSTRUCTOR,
00037 SELECTOR,
00038 TESTER
00039 } DatatypeKinds;
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052 class TheoryDatatype :public Theory {
00053 protected:
00054 DatatypeProofRules* d_rules;
00055
00056
00057 ExprMap<ExprMap<unsigned> > d_datatypes;
00058
00059 ExprMap<std::vector<Expr> > d_constructorMap;
00060
00061 ExprMap<std::pair<Expr,unsigned> > d_selectorMap;
00062
00063 ExprMap<Expr> d_testerMap;
00064 ExprMap<Op> d_reach;
00065
00066 CDMap<Expr, SmartCDO<Unsigned> > d_labels;
00067
00068 CDList<Theorem> d_facts;
00069 CDList<Expr> d_splitters;
00070 CDO<unsigned> d_splittersIndex;
00071 CDO<bool> d_splitterAsserted;
00072 const bool& d_smartSplits;
00073 ExprMap<bool> d_getConstantStack;
00074
00075 protected:
00076 virtual void instantiate(const Expr& e, const Unsigned& u);
00077 virtual void initializeLabels(const Expr& e, const Type& t);
00078 virtual void mergeLabels(const Theorem& thm, const Expr& e1, const Expr& e2);
00079 virtual void mergeLabels(const Theorem& thm, const Expr& e,
00080 unsigned position, bool positive);
00081
00082 public:
00083 TheoryDatatype(TheoryCore* theoryCore);
00084 virtual ~TheoryDatatype();
00085
00086
00087
00088 DatatypeProofRules* createProofRules();
00089
00090
00091 void addSharedTerm(const Expr& e);
00092 void assertFact(const Theorem& e);
00093 virtual void checkSat(bool fullEffort);
00094 Theorem rewrite(const Expr& e);
00095 virtual void setup(const Expr& e);
00096 virtual void update(const Theorem& e, const Expr& d);
00097 Theorem solve(const Theorem& e);
00098 void checkType(const Expr& e);
00099 Cardinality finiteTypeInfo(Expr& e, Unsigned& n,
00100 bool enumerate, bool computeSize);
00101 void computeType(const Expr& e);
00102 void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00103 Expr computeTCC(const Expr& e);
00104 Expr parseExprOp(const Expr& e);
00105 ExprStream& print(ExprStream& os, const Expr& e);
00106
00107
00108 Expr dataType(const std::string& name,
00109 const std::vector<std::string>& constructors,
00110 const std::vector<std::vector<std::string> >& selectors,
00111 const std::vector<std::vector<Expr> >& types);
00112
00113
00114 Expr dataType(const std::vector<std::string>& names,
00115 const std::vector<std::vector<std::string> >& constructors,
00116 const std::vector<std::vector<std::vector<std::string> > >& selectors,
00117 const std::vector<std::vector<std::vector<Expr> > >& types);
00118
00119 Expr datatypeConsExpr(const std::string& constructor,
00120 const std::vector<Expr>& args);
00121 Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
00122 Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
00123
00124 const std::pair<Expr,unsigned>& getSelectorInfo(const Expr& e);
00125 Expr getConsForTester(const Expr& e);
00126 unsigned getConsPos(const Expr& e);
00127 Expr getConstant(const Type& t);
00128 const Op& getReachablePredicate(const Type& t);
00129 bool canCollapse(const Expr& e);
00130
00131 };
00132
00133 inline bool isDatatype(const Type& t)
00134 { return t.getExpr().getKind() == DATATYPE; }
00135
00136 inline bool isConstructor(const Expr& e)
00137 { return (e.getKind() == CONSTRUCTOR && e.getType().arity()==1) ||
00138 (e.isApply() && e.getOpKind() == CONSTRUCTOR); }
00139
00140 inline bool isSelector(const Expr& e)
00141 { return e.isApply() && e.getOpKind() == SELECTOR; }
00142
00143 inline bool isTester(const Expr& e)
00144 { return e.isApply() && e.getOpKind() == TESTER; }
00145
00146 inline Expr getConstructor(const Expr& e)
00147 { DebugAssert(isConstructor(e), "Constructor expected");
00148 return e.isApply() ? e.getOpExpr() : e; }
00149
00150 }
00151
00152 #endif