| 1 |
/* |
| 2 |
* Boundary Module |
| 3 |
* Created: 04/97 |
| 4 |
* Version: $Revision: 1.10 $ |
| 5 |
* Version control file: $RCSfile: bnd.h,v $ |
| 6 |
* Date last modified: $Date: 1997/07/18 12:13:55 $ |
| 7 |
* Last modified by: $Author: mthomas $ |
| 8 |
* |
| 9 |
* This file is part of the SLV solver. |
| 10 |
* |
| 11 |
* The SLV solver is free software; you can redistribute |
| 12 |
* it and/or modify it under the terms of the GNU General Public License as |
| 13 |
* published by the Free Software Foundation; either version 2 of the |
| 14 |
* License, or (at your option) any later version. |
| 15 |
* |
| 16 |
* The SLV solver is distributed in hope that it will be |
| 17 |
* useful, but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 18 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
| 19 |
* General Public License for more details. |
| 20 |
* |
| 21 |
* You should have received a copy of the GNU General Public License |
| 22 |
* along with the program; if not, write to the Free Software Foundation, |
| 23 |
* Inc., 675 Mass Ave, Cambridge, MA 02139 USA. Check the file named |
| 24 |
* COPYING. COPYING is found in ../compiler. |
| 25 |
* |
| 26 |
*/ |
| 27 |
|
| 28 |
/* |
| 29 |
* Description: This is the ascend version of the boundary module. |
| 30 |
* This version should be used by any user who receives |
| 31 |
* his/her formulation directly from an instance tree |
| 32 |
* created by the ASCEND compiler. |
| 33 |
*/ |
| 34 |
|
| 35 |
|
| 36 |
#ifndef bnd__already_included |
| 37 |
#define bnd__already_included |
| 38 |
|
| 39 |
/* Need a better way of doing this, dynamic allocation */ |
| 40 |
#define MAXNUM_OF_SAT_TERMS 5 |
| 41 |
|
| 42 |
/* requires #include "base.h" */ |
| 43 |
/* requires #include "rel.h" */ |
| 44 |
/* requires #include "logrel.h" */ |
| 45 |
|
| 46 |
|
| 47 |
/* The condition is a rel or a logrel */ |
| 48 |
enum bnd_enum { |
| 49 |
e_bnd_rel, |
| 50 |
e_bnd_logrel, |
| 51 |
e_bnd_undefined |
| 52 |
}; |
| 53 |
|
| 54 |
union bnd_union { |
| 55 |
struct rel_relation *relbnd; |
| 56 |
struct logrel_relation *logrelbnd; |
| 57 |
}; |
| 58 |
|
| 59 |
struct bnd_boundary { |
| 60 |
enum bnd_enum kind; /* real or logical condition */ |
| 61 |
union bnd_union cond; /* condition */ |
| 62 |
struct gl_list_t *logrels; /* logrel using the truth value of condition */ |
| 63 |
real64 tolerance; /* assume a unique and consistent value for the |
| 64 |
tolerance. Used only when the condition is a |
| 65 |
rel_relation. Needs FIX for arbitrary |
| 66 |
values */ |
| 67 |
int32 mindex; /* index in the slv_system_t master list */ |
| 68 |
int32 sindex; /* index in the slv_system_t solver list */ |
| 69 |
int32 model; /* index of a hypothetical MODEL bnd is from */ |
| 70 |
uint32 flags; /* flags */ |
| 71 |
}; |
| 72 |
|
| 73 |
extern struct bnd_boundary *bnd_create(struct bnd_boundary *); |
| 74 |
/* |
| 75 |
* bnd_create(bnd) |
| 76 |
* bnd = bnd_create(NULL) |
| 77 |
* struct bnd_boundary *bnd; |
| 78 |
* |
| 79 |
* Creates a boundary. |
| 80 |
* If the bnd supplied is NULL, we allocate the memory for the |
| 81 |
* bnd we return, else we just init the memory you hand us and |
| 82 |
* Setting the the information is the job |
| 83 |
* of the bridge building function between the ascend instance |
| 84 |
* tree and the slv_system_t. |
| 85 |
*/ |
| 86 |
|
| 87 |
extern void bnd_destroy(struct bnd_boundary *); |
| 88 |
/* |
| 89 |
* bnd_destroy(bnd) |
| 90 |
* struct bnd_boundary *bnd; |
| 91 |
* |
| 92 |
* Destroys a boundary. |
| 93 |
*/ |
| 94 |
|
| 95 |
extern void bnd_set_kind(struct bnd_boundary *,enum bnd_enum); |
| 96 |
extern enum bnd_enum bnd_kind(struct bnd_boundary *); |
| 97 |
/* |
| 98 |
* kind = bnd_kind(bnd); |
| 99 |
* bnd_enum kind; |
| 100 |
* struct bnd_boundary *bnd; |
| 101 |
* Set/Retrieves the type of the condition of the given boundary. |
| 102 |
*/ |
| 103 |
|
| 104 |
#define bnd_log_cond(b) ((b)->cond.logrelbnd) |
| 105 |
#define bnd_real_cond(b) ((b)->cond.relbnd) |
| 106 |
#define bnd_logrel(b) ((struct logrel_relation *)(b)) |
| 107 |
#define bnd_rel(b) ((struct rel_relation *)(b)) |
| 108 |
|
| 109 |
extern void bnd_set_logrels(struct bnd_boundary *,struct gl_list_t *); |
| 110 |
extern struct gl_list_t *bnd_logrels(struct bnd_boundary *); |
| 111 |
/* |
| 112 |
* logrels = bnd_logrels(bnd) |
| 113 |
* struct bnd_logrels *bnd; |
| 114 |
* struct gl_list_t *logrels; |
| 115 |
* |
| 116 |
* Set/Retrieves the list of pointers to the logrels using |
| 117 |
* the condition. |
| 118 |
*/ |
| 119 |
|
| 120 |
extern void bnd_set_tolerance(struct bnd_boundary *,real64); |
| 121 |
extern real64 bnd_tolerance(struct bnd_boundary *); |
| 122 |
/* |
| 123 |
* tolerance = bnd_tolerance(bnd) |
| 124 |
* struct bnd_boundary *bnd; |
| 125 |
* real64 tolerance; |
| 126 |
* |
| 127 |
* Set/Retrieves the tolerance used to determine the truth value |
| 128 |
* of the condition. Assume only one sucha a value. If different |
| 129 |
* values, this needs a FIX. |
| 130 |
*/ |
| 131 |
|
| 132 |
extern char *bnd_make_name(slv_system_t,struct bnd_boundary *); |
| 133 |
/* |
| 134 |
* name = bnd_make_name(sys,bnd) |
| 135 |
* slv_system_t sys; |
| 136 |
* struct bnd_boundary *bnd; |
| 137 |
* char *name; |
| 138 |
* |
| 139 |
* Copies of the condition instance name can be made and returned. |
| 140 |
* The string returned should be freed when no longer in use. |
| 141 |
*/ |
| 142 |
|
| 143 |
extern int32 bnd_mindex(struct bnd_boundary *); |
| 144 |
extern void bnd_set_mindex(struct bnd_boundary *,int32); |
| 145 |
/* |
| 146 |
* index = bnd_mindex(bnd) |
| 147 |
* bnd_set_mindex(bnd,index) |
| 148 |
* int32 index; |
| 149 |
* struct bnd_boundary *bnd; |
| 150 |
* |
| 151 |
* Sets or retrieves the index number of the given boundary as it |
| 152 |
* appears in a slv_system_t master boundary list. |
| 153 |
*/ |
| 154 |
|
| 155 |
extern int32 bnd_sindex(const struct bnd_boundary *); |
| 156 |
extern void bnd_set_sindex(struct bnd_boundary *,int32); |
| 157 |
/* |
| 158 |
* index = bnd_sindex(bnd) |
| 159 |
* bnd_set_sindex(bnd,index) |
| 160 |
* int32 index; |
| 161 |
* struct bnd_boundary *bnd; |
| 162 |
* |
| 163 |
* Sets or retrieves the index number of the given boundary as it |
| 164 |
* appears in a solvers boundary list. |
| 165 |
*/ |
| 166 |
|
| 167 |
extern int32 bnd_model(const struct bnd_boundary *); |
| 168 |
extern void bnd_set_model(struct bnd_boundary *,int32); |
| 169 |
/* |
| 170 |
* index = bnd_model(bnd) |
| 171 |
* bnd_set_model(bnd,index) |
| 172 |
* int32 index; |
| 173 |
* struct bnd_boundary *bnd; |
| 174 |
* |
| 175 |
* Sets or retrieves the model number of the given boundary. |
| 176 |
* In a hierarchy, boundaries come in groups associated with |
| 177 |
* models. Models are numbered from 1 to some upper limit. |
| 178 |
*/ |
| 179 |
|
| 180 |
extern struct var_variable **bnd_real_incidence(struct bnd_boundary *); |
| 181 |
/* |
| 182 |
* Get the list of variables incident in the relation constituting |
| 183 |
* the boundary. |
| 184 |
*/ |
| 185 |
|
| 186 |
extern int32 bnd_n_real_incidences(struct bnd_boundary *); |
| 187 |
/* |
| 188 |
* Get the number of variables incident in the relation constituting |
| 189 |
* the boundary. |
| 190 |
*/ |
| 191 |
|
| 192 |
/* |
| 193 |
* Boundary filtration functions. |
| 194 |
* We have a lot (32) of binary (one bit) flags a client may want to query |
| 195 |
* in arbitrary combinations and paying attention to only certain of |
| 196 |
* the bits. We will provide a set of macros and functions for each of |
| 197 |
* these bits and for operations on the whole set. |
| 198 |
*/ |
| 199 |
|
| 200 |
typedef struct bnd_filter_structure { |
| 201 |
uint32 matchbits; |
| 202 |
uint32 matchvalue; |
| 203 |
} bnd_filter_t; |
| 204 |
|
| 205 |
extern int bnd_apply_filter(const struct bnd_boundary *,bnd_filter_t *); |
| 206 |
/* |
| 207 |
* value = bnd_apply_filter(bnd,filter) |
| 208 |
* int value; |
| 209 |
* struct bnd_boundary *bnd; |
| 210 |
* bnd_filter_t *filter; |
| 211 |
* |
| 212 |
* Returns 1 only if all of the positions specified in |
| 213 |
* filter->matchbits have the same values in |
| 214 |
* filter->matchvalue and the boundary's flags value. |
| 215 |
* Bits set to 0 in filter->matchbits are ignored for the test. |
| 216 |
*/ |
| 217 |
|
| 218 |
extern unsigned int bnd_flags(struct bnd_boundary *); |
| 219 |
extern void bnd_set_flags(struct bnd_boundary *,uint32); |
| 220 |
/* |
| 221 |
* struct bnd_boundary *bnd; |
| 222 |
* uint32 flags; |
| 223 |
* |
| 224 |
* bnd_flags(bnd) returns the flags field of the boundary. |
| 225 |
* bnd_set_flags(bnd,flags) sets the entire flag field to the |
| 226 |
* value of flags given. |
| 227 |
*/ |
| 228 |
|
| 229 |
extern uint32 bnd_flagbit(struct bnd_boundary *,uint32); |
| 230 |
/* |
| 231 |
* bnd_flagbit(bnd,name); |
| 232 |
* struct bnd_boundary *bnd; |
| 233 |
* uint32 name; |
| 234 |
* name should be a BND_xx flag defined above) |
| 235 |
* Returns the value of the bit specified from the boundary flags. |
| 236 |
*/ |
| 237 |
|
| 238 |
extern void bnd_set_flagbit(struct bnd_boundary *,uint32, uint32); |
| 239 |
/* |
| 240 |
* struct bnd_boundary *bnd; |
| 241 |
* unsigned int NAME,oneorzero; |
| 242 |
* bnd_set_flagbit(bnd,NAME,oneorzero) |
| 243 |
* |
| 244 |
* Sets the bit, which should be referred to by its macro name, |
| 245 |
* on if oneorzero is >0 and off is oneorzero is 0. |
| 246 |
* The macro names are the defined up at the top of this file. |
| 247 |
*/ |
| 248 |
|
| 249 |
/* the bit flags.*/ |
| 250 |
#define BND_REAL 0x1 |
| 251 |
#define BND_IN_LOGREL 0x2 |
| 252 |
#define BND_EQUALITY 0x4 |
| 253 |
#define BND_AT_ZERO 0x8 |
| 254 |
#define BND_CUR_STATUS 0x10 |
| 255 |
#define BND_PRE_STATUS 0x20 |
| 256 |
#define BND_CROSSED 0x40 |
| 257 |
#define BND_PERTURB 0x80 |
| 258 |
|
| 259 |
|
| 260 |
/* |
| 261 |
* BND_REAL is the boundary a real relation ? |
| 262 |
* BND_IN_LOGREL is the boundary used in some logical relation ? |
| 263 |
* BND_EQUALITY is the boundary an equality? readonly for clients. |
| 264 |
* BND_AT_ZERO Am I at the "zero" of a conditional boundary ? |
| 265 |
* BND_CUR_STATUS Is the Boundary boundary currently satisfied ? |
| 266 |
* BND_PRE_STATUS Was the Boundary boundary satisfied in the previous |
| 267 |
* iteration ? (The last two help to answer the query |
| 268 |
* "Was the boundary crossed ?") |
| 269 |
* BND_CROSSED Was the boundary crossed ? |
| 270 |
* BND_PERTURB Should I perturb this boundary in the calculation |
| 271 |
* of logical variables ? |
| 272 |
*/ |
| 273 |
|
| 274 |
/* |
| 275 |
* the bit flag lookups |
| 276 |
*/ |
| 277 |
#ifdef NDEBUG |
| 278 |
#define bnd_real(b) ((b)->flags & BND_REAL) |
| 279 |
#define bnd_in_logrel(b) ((b)->flags & BND_IN_LOGREL) |
| 280 |
#define bnd_equality(b) ((b)->flags & BND_EQUALITY) |
| 281 |
#define bnd_at_zero(b) ((b)->flags & BND_AT_ZERO) |
| 282 |
#define bnd_cur_status(b) ((b)->flags & BND_CUR_STATUS) |
| 283 |
#define bnd_pre_status(b) ((b)->flags & BND_PRE_STATUS) |
| 284 |
#define bnd_crossed(b) ((b)->flags & BND_CROSSED) |
| 285 |
#define bnd_perturb(b) ((b)->flags & BND_PERTURB) |
| 286 |
#else |
| 287 |
#define bnd_real(b) bnd_flagbit((b),BND_REAL) |
| 288 |
#define bnd_in_logrel(b) bnd_flagbit((b),BND_IN_LOGREL) |
| 289 |
#define bnd_equality(b) bnd_flagbit((b),BND_EQUALITY) |
| 290 |
#define bnd_at_zero(b) bnd_flagbit((b),BND_AT_ZERO) |
| 291 |
#define bnd_cur_status(b) bnd_flagbit((b),BND_CUR_STATUS) |
| 292 |
#define bnd_pre_status(b) bnd_flagbit((b),BND_PRE_STATUS) |
| 293 |
#define bnd_crossed(b) bnd_flagbit((b),BND_CROSSED) |
| 294 |
#define bnd_perturb(b) bnd_flagbit((b),BND_PERTURB) |
| 295 |
#endif /* NDEBUG */ |
| 296 |
|
| 297 |
/* |
| 298 |
* bit flag assignments. any value other than 0 for bv turns the |
| 299 |
* named flag to 1. 0 sets it to 0. |
| 300 |
*/ |
| 301 |
#define bnd_set_real(b,bv) bnd_set_flagbit((b),BND_REAL,(bv)) |
| 302 |
#define bnd_set_in_logrel(b,bv) bnd_set_flagbit((b),BND_IN_LOGREL,(bv)) |
| 303 |
#define bnd_set_equality(b,bv) bnd_set_flagbit((b),BND_EQUALITY,(bv)) |
| 304 |
#define bnd_set_at_zero(b,bv) bnd_set_flagbit((b),BND_AT_ZERO,(bv)) |
| 305 |
#define bnd_set_cur_status(b,bv) bnd_set_flagbit((b),BND_CUR_STATUS,(bv)) |
| 306 |
#define bnd_set_pre_status(b,bv) bnd_set_flagbit((b),BND_PRE_STATUS,(bv)) |
| 307 |
#define bnd_set_crossed(b,bv) bnd_set_flagbit((b),BND_CROSSED,(bv)) |
| 308 |
#define bnd_set_perturb(b,bv) bnd_set_flagbit((b),BND_PERTURB,(bv)) |
| 309 |
|
| 310 |
extern int32 bnd_status_cur( struct bnd_boundary *); |
| 311 |
extern int32 bnd_status_pre( struct bnd_boundary *); |
| 312 |
/* |
| 313 |
* Functions returning an int32 (0 or 1) instead of an arbitrary nonzero |
| 314 |
* or zero value. It is silly, but it makes easier to deal with comparisons |
| 315 |
* between the current and the previous status of a boundary. |
| 316 |
*/ |
| 317 |
|
| 318 |
#endif /* bnd__already_included */ |
Parent Directory
| 
Revision Log