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_array_h_
00022 #define _cvc3__include__theory_array_h_
00023
00024 #include "theory.h"
00025
00026 namespace CVC3 {
00027
00028 class ArrayProofRules;
00029
00030 typedef enum {
00031 ARRAY = 2000,
00032 READ,
00033 WRITE,
00034
00035
00036 ARRAY_LITERAL
00037 } ArrayKinds;
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050 class TheoryArray :public Theory {
00051 ArrayProofRules* d_rules;
00052
00053
00054 CDList<Expr> d_reads;
00055
00056 ExprMap<Theorem> d_renameThms;
00057
00058 const bool& d_applicationsInModel;
00059
00060 const bool& d_liftReadIte;
00061
00062
00063 Theorem renameExpr(const Expr& e);
00064
00065 public:
00066 TheoryArray(TheoryCore* core);
00067 ~TheoryArray();
00068
00069
00070
00071 ArrayProofRules* createProofRules();
00072
00073
00074 void addSharedTerm(const Expr& e) {}
00075 void assertFact(const Theorem& e) {}
00076 void checkSat(bool fullEffort) {}
00077 Theorem rewrite(const Expr& e);
00078 void setup(const Expr& e);
00079 void update(const Theorem& e, const Expr& d);
00080 Theorem solve(const Theorem& e);
00081 void checkType(const Expr& e);
00082 void computeType(const Expr& e);
00083 Type computeBaseType(const Type& t);
00084 void computeModelTerm(const Expr& e, std::vector<Expr>& v);
00085 void computeModel(const Expr& e, std::vector<Expr>& vars);
00086 Expr computeTCC(const Expr& e);
00087 virtual Expr parseExprOp(const Expr& e);
00088 ExprStream& print(ExprStream& os, const Expr& e);
00089 };
00090
00091
00092 inline bool isArray(const Type& t) { return t.getExpr().getKind() == ARRAY; }
00093 inline bool isRead(const Expr& e) { return e.getKind() == READ; }
00094 inline bool isWrite(const Expr& e) { return e.getKind() == WRITE; }
00095 inline bool isArrayLiteral(const Expr& e)
00096 { return (e.isClosure() && e.getKind() == ARRAY_LITERAL); }
00097
00098
00099 inline Type arrayType(const Type& type1, const Type& type2)
00100 { return Type(Expr(ARRAY, type1.getExpr(), type2.getExpr())); }
00101
00102
00103
00104 Expr arrayLiteral(const Expr& ind, const Expr& body);
00105 }
00106
00107 #endif