CVC3

theory_datatype_lazy.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file theory_datatype_lazy.h
00004  *
00005  * Author: Clark Barrett
00006  *
00007  * Created: Wed Dec  1 22:24:32 2004
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
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  *\class TheoryDatatypeLazy
00034  *\ingroup Theories
00035  *\brief This theory handles datatypes.
00036  *
00037  * Author: Clark Barrett
00038  *
00039  * Created: Wed Dec  1 22:27:12 2004
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   // Theory interface
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