blob: 1f0108581f27cc3032856d74066dfaef8ae5c16b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = builtin booleans uf arith arrays bv datatypes quantifiers rewriterules
DIST_SUBDIRS = $(SUBDIRS) example
noinst_LTLIBRARIES = libtheory.la
libtheory_la_SOURCES = \
logic_info.h \
logic_info.cpp \
output_channel.h \
interrupted.h \
type_enumerator.h \
theory_engine.h \
theory_engine.cpp \
theory_test_utils.h \
theory.h \
theory.cpp \
theoryof_mode.h \
theory_registrar.h \
rewriter.h \
rewriter_attributes.h \
rewriter.cpp \
substitutions.h \
substitutions.cpp \
valuation.h \
valuation.cpp \
shared_terms_database.h \
shared_terms_database.cpp \
term_registration_visitor.h \
term_registration_visitor.cpp \
ite_simplifier.h \
ite_simplifier.cpp \
unconstrained_simplifier.h \
unconstrained_simplifier.cpp \
quantifiers_engine.h \
quantifiers_engine.cpp \
model.h \
model.cpp \
rep_set.h \
rep_set.cpp
nodist_libtheory_la_SOURCES = \
rewriter_tables.h \
instantiator_tables.cpp \
theory_traits.h \
type_enumerator.cpp
libtheory_la_LIBADD = \
@builddir@/builtin/libbuiltin.la \
@builddir@/booleans/libbooleans.la \
@builddir@/uf/libuf.la \
@builddir@/arith/libarith.la \
@builddir@/arrays/libarrays.la \
@builddir@/bv/libbv.la \
@builddir@/datatypes/libdatatypes.la \
@builddir@/quantifiers/libquantifiers.la \
@builddir@/rewriterules/librewriterules.la
EXTRA_DIST = \
logic_info.i \
options_handlers.h \
rewriter_tables_template.h \
instantiator_tables_template.cpp \
theory_traits_template.h \
type_enumerator_template.cpp \
mktheorytraits \
mkrewriter \
mkinstantiator \
Makefile.subdirs
BUILT_SOURCES = \
rewriter_tables.h \
instantiator_tables.cpp \
theory_traits.h \
type_enumerator.cpp
CLEANFILES = \
rewriter_tables.h \
instantiator_tables.cpp \
theory_traits.h \
type_enumerator.cpp
include @top_srcdir@/src/theory/Makefile.subdirs
rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkrewriter
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkrewriter \
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
instantiator_tables.cpp: instantiator_tables_template.cpp mkinstantiator @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkinstantiator
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkinstantiator \
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mktheorytraits
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mktheorytraits \
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
type_enumerator.cpp: type_enumerator_template.cpp mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mktheorytraits
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mktheorytraits \
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
|