CVC3  2.4.1
theory_datatype_lazy.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_datatype_lazy.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Dec 1 22:24:32 2004
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_datatype_lazy_h_
22 #define _cvc3__include__theory_datatype_lazy_h_
23 
24 #include "theory.h"
25 #include "smartcdo.h"
26 #include "cdmap.h"
27 #include "theory_datatype.h"
28 
29 namespace CVC3 {
30 
31 /*****************************************************************************/
32 /*!
33  *\class TheoryDatatypeLazy
34  *\ingroup Theories
35  *\brief This theory handles datatypes.
36  *
37  * Author: Clark Barrett
38  *
39  * Created: Wed Dec 1 22:27:12 2004
40  */
41 /*****************************************************************************/
43 
44  typedef enum {
45  MERGE1 = 0,
48  } ProcessKinds;
49 
54 
55 private:
56  void instantiate(const Expr& e, const Unsigned& u);
57  void initializeLabels(const Expr& e, const Type& t);
58  void mergeLabels(const Theorem& thm, const Expr& e1, const Expr& e2);
59  void mergeLabels(const Theorem& thm, const Expr& e,
60  unsigned position, bool positive);
61 
62 public:
65 
66  // Theory interface
67  void checkSat(bool fullEffort);
68  void setup(const Expr& e);
69  void update(const Theorem& e, const Expr& d);
70 
71 };
72 
73 }
74 
75 #endif
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Definition: theory.h:93
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
MS C++ specific settings.
Definition: type.h:42
TheoryDatatypeLazy(TheoryCore *theoryCore)
This theory handles datatypes.
This theory handles datatypes.
void initializeLabels(const Expr &e, const Type &t)
void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
Generic API for Theories plus methods commonly used by theories.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void instantiate(const Expr &e, const Unsigned &u)
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
CDList< ProcessKinds > d_processQueueKind
CDList< Theorem > d_processQueue
Smart context-dependent object wrapper.