00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #ifndef _cvc3__include__theory_records_h_
00021 #define _cvc3__include__theory_records_h_
00022
00023 #include "theory.h"
00024
00025 namespace CVC3 {
00026
00027 class RecordsProofRules;
00028
00029 typedef enum {
00030 RECORD = 2500,
00031 RECORD_SELECT,
00032 RECORD_UPDATE,
00033 RECORD_TYPE,
00034 TUPLE,
00035 TUPLE_SELECT,
00036 TUPLE_UPDATE,
00037 TUPLE_TYPE
00038 } RecordKinds;
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051 class TheoryRecords :public Theory {
00052 RecordsProofRules* d_rules;
00053
00054 Theorem rewriteAux(const Expr& e);
00055
00056 Theorem rewriteAux(const Theorem& thm);
00057
00058 public:
00059 TheoryRecords(TheoryCore* core);
00060 ~TheoryRecords();
00061
00062 RecordsProofRules* createProofRules();
00063
00064
00065
00066
00067 void assertFact(const Theorem& e);
00068
00069 void checkSat(bool fullEffort) {}
00070
00071 Theorem rewrite(const Expr& e);
00072
00073 void checkType(const Expr& e);
00074
00075 void computeType(const Expr& e);
00076 Type computeBaseType(const Type& t);
00077
00078 Expr computeTypePred(const Type& t, const Expr& e);
00079 void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00080 void computeModel(const Expr& e, std::vector<Expr>& vars);
00081
00082 Expr computeTCC(const Expr& e);
00083 virtual Expr parseExprOp(const Expr& e);
00084 void setup(const Expr& e);
00085 void update(const Theorem& e, const Expr& d);
00086
00087 ExprStream& print(ExprStream& os, const Expr& e);
00088
00089 bool isRecord(const Expr& e) {
00090 return e.isApply() && e.getOpKind() == RECORD;
00091 }
00092
00093 bool isRecordType(const Expr& e) {
00094 return e.isApply() && e.getOpKind() == RECORD_TYPE;
00095 }
00096
00097 bool isRecordType(const Type& t) {
00098 return isRecordType(t.getExpr());
00099 }
00100
00101 bool isRecordAccess(const Expr& e)
00102 { return e.isApply() &&
00103 (e.getOpKind() == RECORD_SELECT || e.getOpKind() == RECORD_UPDATE); }
00104
00105 Expr recordExpr(const std::vector<std::string>& fields,
00106 const std::vector<Expr>& kids);
00107
00108 Expr recordExpr(const std::vector<Expr>& fields,
00109 const std::vector<Expr>& kids);
00110
00111 Type recordType(const std::vector<std::string>& fields,
00112 const std::vector<Type>& types);
00113
00114 Type recordType(const std::vector<std::string>& fields,
00115 const std::vector<Expr>& types);
00116
00117 Type recordType(const std::vector<Expr>& fields,
00118 const std::vector<Expr>& types);
00119
00120 Expr recordSelect(const Expr& r, const std::string& field);
00121
00122 Expr recordUpdate(const Expr& r, const std::string& field, const Expr& val);
00123
00124 const std::vector<Expr>& getFields(const Expr& r);
00125
00126 const std::string& getField(const Expr& e, int i);
00127
00128
00129 int getFieldIndex(const Expr& e, const std::string& field);
00130
00131 const std::string& getField(const Expr& e);
00132
00133 Expr tupleExpr(const std::vector<Expr>& kids);
00134
00135 Type tupleType(const std::vector<Type>& types);
00136
00137 Type tupleType(const std::vector<Expr>& types);
00138
00139 Expr tupleSelect(const Expr& tup, int i);
00140
00141 Expr tupleUpdate(const Expr& tup, int i, const Expr& val);
00142
00143 int getIndex(const Expr& e);
00144
00145 bool isTupleAccess(const Expr& e)
00146 { return e.isApply() &&
00147 (e.getOpKind() == TUPLE_SELECT || e.getOpKind() == TUPLE_UPDATE); }
00148
00149 bool isTuple(const Expr& e) { return e.isApply() && e.getOpKind() == TUPLE; }
00150
00151 bool isTupleType(const Expr& e)
00152 { return e.isApply() && e.getOpKind() == TUPLE_TYPE; }
00153
00154 bool isTupleType(const Type& tp) { return isTupleType(tp.getExpr()); }
00155 };
00156
00157 }
00158
00159 #endif