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_lazy_h_
00022 #define _cvc3__include__theory_datatype_lazy_h_
00023
00024 #include "theory.h"
00025 #include "smartcdo.h"
00026 #include "cdmap.h"
00027 #include "theory_datatype.h"
00028
00029 namespace CVC3 {
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042 class TheoryDatatypeLazy :public TheoryDatatype {
00043
00044 typedef enum {
00045 MERGE1 = 0,
00046 MERGE2,
00047 ENQUEUE
00048 } ProcessKinds;
00049
00050 CDList<Theorem> d_processQueue;
00051 CDList<ProcessKinds> d_processQueueKind;
00052 CDO<unsigned> d_processIndex;
00053 CDO<bool> d_typeComplete;
00054
00055 private:
00056 void instantiate(const Expr& e, const Unsigned& u);
00057 void initializeLabels(const Expr& e, const Type& t);
00058 void mergeLabels(const Theorem& thm, const Expr& e1, const Expr& e2);
00059 void mergeLabels(const Theorem& thm, const Expr& e,
00060 unsigned position, bool positive);
00061
00062 public:
00063 TheoryDatatypeLazy(TheoryCore* theoryCore);
00064 ~TheoryDatatypeLazy() {}
00065
00066
00067 void checkSat(bool fullEffort);
00068 void setup(const Expr& e);
00069 void update(const Theorem& e, const Expr& d);
00070
00071 };
00072
00073 }
00074
00075 #endif