blob: b80985c4711481d9d196e888c04bcb0ebc3a2c99 (
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
|
#!/bin/bash
#
# mktheoryof
# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
# Copyright (c) 2010 The CVC4 Project
#
# The purpose of this script is to create theoryof_table.h from a
# prologue, epilogue, and a list of theory kinds.
#
# Invocation:
#
# mktheoryof prologue-file epilogue-file theory-kind-files...
#
# Output is to standard out.
#
cat <<EOF
/********************* -*- C++ -*- */
/** theoryof_table.h
**
** Copyright 2010 The AcSys Group, New York University, and as below.
**
** This header file automatically generated by:
**
** $0 $@
**
** for the CVC4 project.
**/
EOF
prologue=$1; shift
middle=$1; shift
epilogue=$1; shift
registers=
function special {
r=$1
comment=$2
registers="$registers d_table[::CVC4::kind::$r] = th;
"
}
function operator {
special "$1" "$2"
}
function parameterized {
special "$1" "$2"
}
function constant {
special "$1" "$3"
}
cat "$prologue"
while [ $# -gt 0 ]; do
b=$(basename $(dirname "$1"))
B=$(echo "$b" | tr 'a-z' 'A-Z')
echo "#include \"theory/$b/theory_def.h\""
registers="$registers
/* from $b */
void registerTheory(::CVC4::theory::$b::Theory$B* th) {
"
source "$1"
registers="$registers }
"
shift
done
echo
cat "$middle"
echo "$registers"
cat "$epilogue"
|