2 * Copyright (c) 2000-2001
3 * The Regents of the University of California. All rights reserved.
5 * Redistribution and use in source and binary forms, with or without
6 * modification, are permitted provided that the following conditions
8 * 1. Redistributions of source code must retain the above copyright
9 * notice, this list of conditions and the following disclaimer.
10 * 2. Redistributions in binary form must reproduce the above copyright
11 * notice, this list of conditions and the following disclaimer in the
12 * documentation and/or other materials provided with the distribution.
13 * 3. Neither the name of the University nor the names of its contributors
14 * may be used to endorse or promote products derived from this software
15 * without specific prior written permission.
17 * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
18 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
19 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
20 * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
21 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
22 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
23 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
24 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
25 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
26 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
51 typedef struct sig_elt sig_elt
;
52 typedef struct constructor
*constructor
;
60 DECLARE_LIST(flowrow_map
,flowrow_field
)
65 extern bool flag_merge_projections
;
66 extern bool flag_eliminate_cycles
;
67 extern bool flag_occurs_check
;
70 Operations for building terms
73 /* Defines a new constructor for sort s with the given signature */
74 constructor
make_constructor(const char *name
,sort_kind sort
, sig_elt
[],
77 /* Build the term c(exps[0]....exps[n]) */
78 gen_e
constructor_expr(constructor c
, gen_e exps
[], int arity
);
80 /* make a constant of sort s */
81 gen_e
setif_constant(const char *name
);
83 gen_e
setst_constant(const char *name
);
85 gen_e
term_constant(const char *name
);
87 /* Creates a projection pattern projpat(c,i,e) */
88 gen_e
setif_proj_pat(constructor c
,int i
,gen_e e
);
90 gen_e
setst_proj_pat(constructor c
, int i
, gen_e e
);
92 /* Adds a constraint e <= projpat(c,i,fv) where fv is a fresh variable */
93 gen_e
setif_proj(constructor c
, int i
, gen_e e
);
95 gen_e
setst_proj(constructor c
, int i
, gen_e e
);
97 /* Make a new variable of sort s */
98 gen_e
setif_fresh(const char *name
);
100 gen_e
term_fresh(const char *name
);
102 gen_e
flowrow_fresh(const char *name
);
104 gen_e
setst_fresh(const char *name
);
106 /* Operations for unions */
108 gen_e
setif_union(gen_e exps
[]);
110 gen_e
setif_inter(gen_e exps
[]);
112 gen_e
setst_union(gen_e exps
[]);
114 gen_e
setst_inter(gen_e exps
[]);
116 /* Empty set of sort s */
117 gen_e
setif_zero(void);
119 gen_e
setst_zero(void);
121 gen_e
flowrow_zero(sort_kind base_sort
);
123 gen_e
term_zero(void);
125 /* Universal set of sort s */
126 gen_e
setif_one(void);
128 gen_e
setst_one(void);
130 gen_e
flowrow_one(sort_kind base_sort
);
132 gen_e
term_one(void);
135 Operations for building flowrows
138 /* Closed flowrow of base sort s */
139 gen_e
flowrow_abs(sort_kind base_sort
);
141 /* Wild flowrow of base sort s */
142 gen_e
flowrow_wild(sort_kind base_sort
);
144 /* Build a flowrow of <l : e>_fields o <rest> */
145 gen_e
flowrow_row(flowrow_map fields
, gen_e rest
);
150 void call_setif_inclusion(gen_e e1
,gen_e e2
);
151 void call_setif_unify(gen_e e1
, gen_e e2
);
153 void call_setst_inclusion(gen_e e1
, gen_e e2
);
154 void call_setst_unify(gen_e e1
, gen_e e2
);
156 void call_flowrow_inclusion(gen_e e1
,gen_e e2
);
157 void call_flowrow_unify(gen_e e1
, gen_e e2
);
159 void call_term_unify(gen_e e1
, gen_e e2
);
160 void call_term_cunify(gen_e e1
, gen_e e2
);
170 struct decon
deconstruct_expr(constructor c
,gen_e e
);
172 gen_e_list
setif_tlb(gen_e e
);
174 gen_e_list
setst_tlb(gen_e e
);
176 gen_e
term_get_ecr(gen_e e
);
178 gen_e
flowrow_extract_field(const char *label
,gen_e row
);
179 flowrow_map
flowrow_extract_fields(gen_e row
);
180 gen_e
flowrow_extract_rest(gen_e row
);
182 void nonspec_init(void);
183 void nonspec_reset(void);
185 void expr_print(FILE *f
,gen_e e
);
189 #endif /* NONSPEC_H */