CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
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
/*****************************************************************************/
42
class
TheoryDatatypeLazy
:
public
TheoryDatatype
{
43
44
typedef
enum
{
45
MERGE1
= 0,
46
MERGE2
,
47
ENQUEUE
48
}
ProcessKinds
;
49
50
CDList<Theorem>
d_processQueue
;
51
CDList<ProcessKinds>
d_processQueueKind
;
52
CDO<unsigned>
d_processIndex
;
53
CDO<bool>
d_typeComplete
;
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
:
63
TheoryDatatypeLazy
(
TheoryCore
*
theoryCore
);
64
~TheoryDatatypeLazy
() {}
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
Generated on Sat May 18 2013 12:01:28 for CVC3 by
1.8.3.1