1/* BEGIN LICENSE BLOCK 2 * Version: CMPL 1.1 3 * 4 * The contents of this file are subject to the Cisco-style Mozilla Public 5 * License Version 1.1 (the "License"); you may not use this file except 6 * in compliance with the License. You may obtain a copy of the License 7 * at www.eclipse-clp.org/license. 8 * 9 * Software distributed under the License is distributed on an "AS IS" 10 * basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 11 * the License for the specific language governing rights and limitations 12 * under the License. 13 * 14 * The Original Code is The ECLiPSe Constraint Logic Programming System. 15 * The Initial Developer of the Original Code is Cisco Systems, Inc. 16 * Portions created by the Initial Developer are 17 * Copyright (C) 2001-2006 Cisco Systems, Inc. All Rights Reserved. 18 * 19 * Contributor(s): Warwick Harvey, IC-Parc 20 * 21 * END LICENSE BLOCK */ 22/*-------------------------------------------------------------------- 23** 24** IC low-level C functions. 25** 26** System: ECLiPSe Constraint Logic Programming System 27** Author/s: Warwick Harvey, IC-Parc 28** 29** $Id: ic.c,v 1.4 2013/02/09 20:27:58 jschimpf Exp $ 30** 31** This file provides low-level primitives in support of the ic_kernel and 32** ic_constraints ECLiPSe modules. This is almost entirely for efficiency 33** reasons; there is very little here that couldn't have been done in 34** ECLiPSe. 35** 36**-------------------------------------------------------------------*/ 37 38/* 39** TODO: 40** - Do something about the dereferences? E.g. assume nobody else is 41** tampering with the structures, etc.? 42** - Implement more special cases/optimisations. 43** - Probably lots of stuff. :) 44*/ 45 46 47#if 0 48#define IC_DEBUG 49#include <stdio.h> 50#endif 51 52#undef USE_BOUND_SET_SHORTCUT 53 54/*---------------------------------------------------------------------- 55** 56** Load some needed header files. 57** 58*/ 59 60#include "external.h" 61#include "error.h" 62#include "bitmap.h" 63#include "intervals.h" 64#include "rounding_control.h" 65#include "emu_export.h" 66#include <math.h> 67#include <string.h> 68 69#if defined(BARRELFISH) && defined(__ARM_ARCH_7A__) && defined(bool) 70#undef bool 71#endif 72 73/*---------------------------------------------------------------------- 74** 75** Define some useful constants and macros. 76** 77*/ 78 79#define min(x,y) ((x) < (y) ? (x) : (y)) 80#define max(x,y) ((x) > (y) ? (x) : (y)) 81 82 /* 83 ** This is for Windows' benefit, but should be fine for all other 84 ** architectures as well. 85 */ 86#define NEG_ZERO (-1 * 0.0) 87 88 /* 89 ** Return the preferred waking priority for the given constraint. 90 */ 91#define ConstraintPriority(con) ((con)->term_count < 3 ? 3 : 4) 92 93/* 94** Offsets (in pwords) of the various fields in the ic var structure. 95** 96** Assumes the ECLiPSe type looks like this: 97** 98** ic( 99** var_type, % atom: 'integer' or 'float' [or 'expression'?] 100** lo, % float: lower bound 101** hi, % float: upper bound 102** bitmap, % 'undefined' or bitmap of integer domain 103** % subst, % substitution 104** % subst_occ, % list of substitution occurrences? 105** XXX variable, % the variable this attribute belongs to 106** min, % suspensions: wake on update of lo 107** max, % suspensions: wake on update of hi 108** hole, % suspensions: wake on new hole in domain 109** % any % suspensions: wake on any domain change 110** % subst % suspensions: wake on substitution 111** type % suspensions: wake on type change (float -> int) 112** ) 113** 114** Note that the variable field is not needed if the constraints don't 115** retain references to variable attributes. 116*/ 117 118#define OFF_TYPE 1 119#define OFF_LO 2 120#define OFF_HI 3 121#define OFF_BITMAP 4 122#ifdef IC_VARS_AS_ATTRS 123#define OFF_VARIABLE 5 124#define OFF_WAKE_LISTS 6 125#else 126#define OFF_WAKE_LISTS 5 127#endif 128#define OFF_WAKE_LO OFF_WAKE_LISTS 129#define OFF_WAKE_HI (OFF_WAKE_LISTS + 1) 130#define OFF_WAKE_HOLE (OFF_WAKE_LISTS + 2) 131#define OFF_WAKE_TYPE (OFF_WAKE_LISTS + 3) 132#define ATTR_ARITY OFF_WAKE_TYPE 133 134#ifdef IC_VARS_AS_ATTRS 135#define Fill_Var_Field(pw, var) Make_Ref(&pw[OFF_VARIABLE], var) 136#else 137#define Fill_Var_Field(pw, var) 138#endif 139 140 141/* Offset of 'constrained' list in 'suspend' attribute, from emu_c_env.c. */ 142#define CONSTRAINED_OFF 2 143 144 145/* 146** Create an IC attribute except the reference to the variable. 147*/ 148#define Create_Default_IC_Attr(attr) \ 149 create_ic_attr(&attr, -HUGE_VAL, HUGE_VAL, 0) 150 151 152/* 153** Retrieve the IC attribute of a variable, assuming the variable has 154** attributes. 'var' must be dereferenced and 'IsMeta'. 155*/ 156#define IC_Var_Get_Attr(var, attr) { \ 157 (attr) = MetaTerm(var); \ 158 Dereference(attr); \ 159 (attr) = (attr)->val.ptr + ic_domain_slot; \ 160 Dereference(attr); \ 161 } 162 163/* 164** Retrieve the "contents" of the IC attribute of a variable (i.e. the 165** vector containing the data, rather than the TCOMP cell pointing to the 166** vector). 'var' must be dereferenced and have a proper IC attribute. 167*/ 168#define IC_Var_Get_Attr_Vec(var, attr) { \ 169 IC_Var_Get_Attr(var, attr) \ 170 (attr) = (attr)->val.ptr; \ 171 Dereference(attr); \ 172 } 173 174/* 175** Retrieve the "contents" of the IC attribute of a variable (i.e. the 176** vector containing the data, rather than the TCOMP cell pointing to the 177** vector), creating the IC attribute if it doesn't exist. 'var' must be 178** dereferenced and 'IsRef'. 179*/ 180#define IC_Var_Attr_Vec(var, attr) { \ 181 (attr) = make_ic_var_attr(var); \ 182 (attr) = (attr)->val.ptr; \ 183 Dereference(attr); \ 184 } 185 186/* 187** Macros for the IC constraint structure. 188** 189** Assumes the ECLiPSe type looks like this: 190** 191** ic_con( 192** data, % flags, RHS constant, etc. in buffer struct 193** boolean, % reification boolean 194** lo_vector, % vector containing lower bounds of term coefficients 195** hi_vector, % vector containing upper bounds of term coefficients 196** var_vector, % vector containing term variables 197** susp % the constraint suspension 198** ) 199*/ 200 201#define CON_OFF_DATA 1 202#define CON_OFF_BOOLEAN 2 203#define CON_OFF_LO_VEC 3 204#define CON_OFF_HI_VEC 4 205#define CON_OFF_VAR_VEC 5 206#define CON_OFF_SUSP 6 207#define CON_ARITY 6 208 209 210/* 211** Macros for dealing with buffer structure used to store "constant" data 212** for a constraint. We could store the flags and (optional) term count in 213** the same word, but since the buffer will take up an even number of pwords 214** anyway, we might as well store them separately. 215** 216** |-------------------------------| 217** | | 218** | - - - - - - - - - - - - - - - | 219** | RHS upper bound (double) | 220** |-------------------------------| 221** | | 222** | - - - - - - - - - - - - - - - | 223** | RHS lower bound (double) | 224** |-------------------------------| 225** | Term count | 226** |-------------------------------| 227** | Flags | 228** |-------------------------------| 229** | TBUFFER | 230** |-------------------------------| 231** | Buffer size | 232** |-------------------------------| 233*/ 234 235 /* Offsets from the start of the buffer, in words. */ 236#define CON_DATA_OFF_FLAGS 0 237#define CON_DATA_OFF_COUNT 1 238#define CON_DATA_OFF_RHS_LO 2 239#define CON_DATA_OFF_RHS_HI 4 240#define CON_DATA_SIZE 6 241#define CON_DATA_SIZE_BYTES (CON_DATA_SIZE * sizeof(pword)) 242 243 /* 244 ** Values for the flags. 245 ** Note that the 3 low bit flags must match op_to_flags in 246 ** ic_constraints.ecl. Note also that we prefer the boolean toggle to 247 ** be in the low bit. 248 */ 249#define CON_LOWER 0x1 250#define CON_UPPER 0x2 251#define CON_INTEGRAL 0x4 252#define CON_INTEGRALITY_PROP 0x8 253 254#define CON_OP_MASK (CON_LOWER + CON_UPPER) 255 256 /* 257 ** Convert a constraint's flags plus a boolean representing whether the 258 ** constraint must be true or false into a single number representing 259 ** the constraint operator. 260 */ 261#define FlagsAndBoolToOp(flags, bool) \ 262 (((flags) & CON_OP_MASK) ^ (CON_OP_MASK * !(bool))) 263 264#define LOWER_BOUND CON_LOWER 265#define UPPER_BOUND CON_UPPER 266 267#define OpIsLowerBound(op) (((op) & LOWER_BOUND) == LOWER_BOUND) 268#define OpIsUpperBound(op) (((op) & UPPER_BOUND) == UPPER_BOUND) 269 270#define OpIsEqual(op) ((op) == LOWER_BOUND + UPPER_BOUND) 271#define OpIsNotEqual(op) ((op) == 0) 272#define OpIsLessEqual(op) ((op) == UPPER_BOUND) 273#define OpIsGreater(op) ((op) == LOWER_BOUND) 274 275 276 /* Returns a pointer to the data buffer entry at the given word offset. */ 277#define ConBufEntry(buf, offset) (&((word *)BufferStart(buf))[offset]) 278 279 /* 280 ** Fill in the data in a constraint data buffer. 281 */ 282#define Set_Con_Data_Buf(con_info) { \ 283 word *tmp; \ 284 tmp = ConBufEntry((con_info)->data, 0); \ 285 tmp[CON_DATA_OFF_FLAGS] = (con_info)->flags; \ 286 tmp[CON_DATA_OFF_COUNT] = (con_info)->term_count; \ 287 *((double *) (tmp + CON_DATA_OFF_RHS_LO)) = (con_info)->c.l; \ 288 *((double *) (tmp + CON_DATA_OFF_RHS_HI)) = (con_info)->c.u; \ 289 } 290 291#define Allocate_Con_Data_Buf(con_info) { \ 292 (con_info)->data = TG; \ 293 Push_Buffer(CON_DATA_SIZE_BYTES); \ 294 } 295 296 /* 297 ** Update the constraint data buffer based on the contents of the 298 ** con_info structure, if the data has changed (currently defined to be 299 ** if there are now fewer terms than there used to be). If the buffer 300 ** needs to be trailed, create a new buffer for the new data, trail it, 301 ** etc. If it doesn't need to be trailed, just overwrite the contents. 302 */ 303#define Update_Con_Data_Buf_If_Needed(con_info) \ 304 if ((con_info)->term_count < (con_info)->old_term_count) { \ 305 int result; \ 306 result = update_con_data_buf(con_info); \ 307 Return_If_Not_Success(result) \ 308 } 309 310 /* Returns a pointer to the first coefficient in the coef vector. */ 311#define CoefVec(pw) ((double *)BufferStart(pw)) 312 313 /* Returns a pointer to the first variable in the variable vector. */ 314#define VarVec(pw) ((pw) + 1) 315 316 317 /* Codes returned when evaluating propagation short-cuts. */ 318#define SHORT_ERROR -1 /* should never be returned on success */ 319#define SHORT_NONE 0 /* no short-cut */ 320#define SHORT_LWB 1 /* set everything to their lower bound */ 321#define SHORT_UPB 2 /* set everything to their upper bound */ 322#define SHORT_ENTAILED 3 /* constraint is entailed */ 323 324/* 325** Useful C data structures for managing variables, constraints, etc. 326*/ 327 328 /* A bounds pair, without type. */ 329typedef struct bounds { 330 double l, u; 331} bounds; 332 333 /* A bounds pair, with type. */ 334typedef struct typed_bounds { 335 bounds b; 336 int i; 337} typed_bounds; 338 339 /* Information about a constraint. */ 340typedef struct con_info { 341 pword *con; 342 pword *data; 343 pword *bool; /* So we have access to it during setup. */ 344 /* May not be valid if not a reified constraint. */ 345 double *lo_vec; 346 double *hi_vec; 347 pword *var_vec; 348 pword *susp; /* Not worthwhile? */ 349 /* orig? */ 350 bounds c; 351 int flags; 352 int term_count, old_term_count; 353 int op; 354 int reified; 355} con_info; 356 357 /* Information about a variable. */ 358typedef struct var_info { 359 pword *var; 360 pword *attr; 361 pword *bitmap; /* XXX Store "uword" bitmap rather than "pword"? */ 362 typed_bounds tb; 363 int prop_int; /* Prop integrality to the var if appropriate */ 364 /* Track what's changed, so can update variable / wake just once? */ 365} var_info; 366 367 /* Information used when propagating a constraint. */ 368typedef struct prop_info { 369 bounds sum; /* lwb == neg_e, upb == f */ 370 word inf_f_idx, inf_e_idx; 371 double inf_f_bound, inf_e_bound; /* ? */ 372 int num_non_int_vars, non_int_idx; 373 int no_prop; /* No propagation/entailment will occur. */ 374 /* Implies all other fields may be invalid. */ 375} prop_info; 376 377 /* 378 ** Note that we leave some fields undefined if it is safe to do so (e.g. 379 ** non_int_idx won't be looked at with num_non_int_vars set to 0). 380 */ 381#define Init_Prop_Info(prop) \ 382 (prop)->sum.l = NEG_ZERO; \ 383 (prop)->sum.u = 0.0; \ 384 (prop)->inf_f_idx = -1; \ 385 (prop)->inf_e_idx = -1; \ 386 (prop)->num_non_int_vars = 0; \ 387 (prop)->no_prop = 0; 388 389 390 /* 391 ** We allow bitmaps over a pretty large range, but for convenience we 392 ** wish to limit them to numbers which can be accurately represented 393 ** both as (machine) integers and doubles. On 32-bit machines, this 394 ** means we're limited by the integers, while on 64-bit machines we're 395 ** limited by doubles. 396 ** 397 ** Note that we stop a little short of the real limits, in particular so 398 ** that "+1" and the like are always safe. 399 */ 400#ifdef DOUBLE_INT_LIMIT 401 402#define MIN_BITMAP_RANGE (-DOUBLE_INT_LIMIT >> 1) 403#define MAX_BITMAP_RANGE ((DOUBLE_INT_LIMIT >> 1) - 1) 404 405#else 406 407#define MIN_BITMAP_RANGE (-1 << (8 * SIZEOF_WORD - 2)) 408#define MAX_BITMAP_RANGE ((1 << (8 * SIZEOF_WORD - 2)) - 1) 409 410#endif 411 412 413 /* Macro for filling an empty space so it can be garbage collected. */ 414 /* Fills a gap of n pwords. */ 415#define Pad(pw, n) \ 416 if ((n) > 1) { \ 417 (pw)->tag.kernel = TBUFFER; \ 418 Set_Buffer_Size(pw, ((n)-1) * sizeof(pword)); \ 419 } else if ((n) == 1) { \ 420 Make_Nil(pw) \ 421 } 422 423 424/* 425** Miscellaneous macros. 426*/ 427 428#define Type_Is_Int(type) ((type) == d_.integer0) 429 430 431/* Round up/down if the type is integer. */ 432#define maybe_round_up(integral, val) \ 433 if (integral) { val = ceil(val); } else 434#define maybe_round_down(integral, val) \ 435 if (integral) { val = floor(val); } else 436 437 438/*---------------------------------------------------------------------- 439** 440** Auxilliary "functions", implemented as macros. 441** 442*/ 443 444 /* 445 ** Return an integer. 446 ** 447 ** NOTE: should only be used when v/t are "fresh" - won't work with old 448 ** vars. 449 */ 450#define Return_Integer(v, t, i) \ 451 { \ 452 v.ptr->val.nint = i; \ 453 v.ptr->tag.kernel = TINT; \ 454 } 455 456 457 /* 458 ** Convert constants to bounds. 459 */ 460 461#define Constant_To_Lower_Bound(vc, tc, bound) \ 462 if (IsDouble(tc)) { \ 463 /* If it's a double here, assume it's accurate. */ \ 464 bound = Dbl(vc); \ 465 } else { \ 466 value ivl; \ 467 tag_desc[TagType(tc)].coerce_to[TIVL](vc, &ivl); \ 468 bound = IvlLwb(ivl.ptr); \ 469 } 470 471#define Constant_To_Upper_Bound(vc, tc, bound) \ 472 if (IsDouble(tc)) { \ 473 /* If it's a double here, assume it's accurate. */ \ 474 bound = Dbl(vc); \ 475 } else { \ 476 value ivl; \ 477 tag_desc[TagType(tc)].coerce_to[TIVL](vc, &ivl); \ 478 bound = IvlUpb(ivl.ptr); \ 479 } 480 481#define Constant_To_Bounds(vc, tc, lwb, upb, integral) \ 482 if (IsDouble(tc)) { \ 483 /* If it's a double here, assume it's accurate. */ \ 484 lwb = upb = Dbl(vc); \ 485 integral = 0; \ 486 } else { \ 487 value ivl; \ 488 tag_desc[TagType(tc)].coerce_to[TIVL](vc, &ivl); \ 489 lwb = IvlLwb(ivl.ptr); \ 490 upb = IvlUpb(ivl.ptr); \ 491 integral = (IsInteger(tc) || IsBignum(tc)); \ 492 } 493 494#define Constant_To_Typed_Bounds(vc, tc, a) \ 495 if (IsDouble(tc)) { \ 496 /* If it's a double here, assume it's accurate. */ \ 497 a.b.l = a.b.u = Dbl(vc); \ 498 a.i = 0; \ 499 } else { \ 500 value ivl; \ 501 tag_desc[TagType(tc)].coerce_to[TIVL](vc, &ivl); \ 502 a.b.l = IvlLwb(ivl.ptr); \ 503 a.b.u = IvlUpb(ivl.ptr); \ 504 a.i = (IsInteger(tc) || IsBignum(tc)); \ 505 } 506 507 508 /* 509 ** Macros for conveniently accessing the low-level arithmetic operations 510 ** provided by RIA. 511 */ 512 513#define Add(a, b, z) \ 514 ec_i_add((a).l, (a).u, (b).l, (b).u, &(z).l, &(z).u) 515 516#define Sub(a, b, z) \ 517 ec_i_sub((a).l, (a).u, (b).l, (b).u, &(z).l, &(z).u) 518 519#define Mul(a, b, z) \ 520 ec_i_mul((a).l, (a).u, (b).l, (b).u, &(z).l, &(z).u) 521 522#define Div(a, b, z) \ 523 ec_i_div((a).l, (a).u, (b).l, (b).u, &(z).l, &(z).u) 524 525 /* 526 ** "Undo" the subtraction of b from a. Like Add, but the upper and 527 ** lower bounds of b have been reversed, which quite conveniently does 528 ** what we want... 529 */ 530#define Undo_Sub(a, b, z) \ 531 ec_i_add((a).l, (a).u, (b).u, (b).l, &(z).l, &(z).u) 532 533 534 /* 535 ** IC_Var_Info(attr, lwb, upb, ic_type, bitmap) 536 ** Convenience macro for extracting the most common information from 537 ** an IC attribute. 538 */ 539#define IC_Var_Info(attr, lwb, upb, ic_type, bitmap) \ 540 { \ 541 pword *tmp; \ 542 \ 543 tmp = attr + OFF_LO; \ 544 Dereference(tmp); \ 545 lwb = Dbl(tmp->val); \ 546 \ 547 tmp = attr + OFF_HI; \ 548 Dereference(tmp); \ 549 upb = Dbl(tmp->val); \ 550 \ 551 tmp = attr + OFF_TYPE; \ 552 Dereference(tmp); \ 553 ic_type = tmp->val.did; \ 554 \ 555 bitmap = attr + OFF_BITMAP; \ 556 Dereference(bitmap); \ 557 } 558 559 560#define Update_Bitmap(var_info, new_bitmap) { \ 561 /* Check whether we need to update the bitmap pointer. */ \ 562 /* Note the test catches both changed and new bitmaps. */ \ 563 if ((var_info)->bitmap->val.wptr != (new_bitmap)) { \ 564 value val; \ 565 type tag; \ 566 val.wptr = (new_bitmap); \ 567 tag.kernel = TBITMAP; \ 568 ec_assign((var_info)->attr + OFF_BITMAP, val, tag); \ 569 (var_info)->bitmap = (var_info)->attr + OFF_BITMAP; \ 570 Dereference((var_info)->bitmap); \ 571 } \ 572 } 573 574 575 /* 576 ** Mark a constraint as entailed; i.e. make sure it doesn't get updated 577 ** any further or propagated again. 578 ** XXX - Assumes the constraint does actually have a suspension set up 579 ** which isn't already dead. 580 */ 581#define Mark_Constraint_Entailed(con_info) { \ 582 /* Don't bother updating the constraint data structures. */ \ 583 (con_info)->old_term_count = 0; \ 584 /* Kill the constraint. */ \ 585 Set_Susp_Dead((con_info)->susp->val.ptr); \ 586 } 587 588#define Unify_Boolean(bool, value, result) { \ 589 pword pw; \ 590 pw.tag.kernel = TINT; \ 591 pw.val.nint = (value); \ 592 (result) = Unify_Pw((bool)->val, (bool)->tag, pw.val, pw.tag); \ 593 } 594 595 596 /* Check for constraints which can be turned into unifications. */ 597#define Check_Con_Is_Unification(con) \ 598 if (OpIsEqual((con)->op) && !(con)->reified && \ 599 (con)->term_count == 2 && \ 600 (con)->c.l == 0.0 && (con)->c.u == 0.0 && \ 601 (con)->lo_vec[0] == (con)->hi_vec[0] && \ 602 (con)->lo_vec[1] == (con)->hi_vec[1] && \ 603 (con)->lo_vec[0] == -(con)->lo_vec[1] && \ 604 (con)->lo_vec[0] != HUGE_VAL && \ 605 (con)->lo_vec[0] != -HUGE_VAL) { \ 606 Mark_Constraint_Entailed(con); \ 607 return Unify_Pw((con)->var_vec[0].val, (con)->var_vec[0].tag, \ 608 (con)->var_vec[1].val, (con)->var_vec[1].tag); \ 609 } 610 611 612 /* XXX - this can be used for any value, not just a bound? */ 613#define Set_Var_To_Value(var_info, bound) { \ 614 int result; \ 615 pword res; \ 616 \ 617 if ((var_info)->prop_int && (bound) == floor(bound)) { \ 618 /* Make it integral before binding. */ \ 619 (var_info)->tb.i = 1; \ 620 (var_info)->prop_int = 0; \ 621 } \ 622 if ((var_info)->tb.i) { \ 623 /* Bind var to integer/bignum. */ \ 624 result = ec_double_to_int_or_bignum(bound, &res); \ 625 Return_If_Not_Success(result); \ 626 } else { \ 627 /* Bind var to bounded real. */ \ 628 Make_Interval(&res, bound, bound); \ 629 } \ 630 result = Unify_Pw((var_info)->var->val, (var_info)->var->tag, res.val, res.tag); \ 631 Return_If_Not_Success(result); \ 632 (var_info)->tb.b.l = (bound); \ 633 (var_info)->tb.b.u = (bound); \ 634 } 635 636 637#if 0 638#define DoublesIdentical(a, b) (memcmp(&(a), &(b), sizeof(double)) == 0) 639#else 640#if SIZEOF_DOUBLE == SIZEOF_WORD 641#define DoublesIdentical(a, b) (*((word*)&(a)) == *((word*)&(b))) 642#elif SIZEOF_DOUBLE == 2*SIZEOF_WORD 643#define DoublesIdentical(a, b) (*((word*)&(a)) == *((word*)&(b)) && \ 644 *(((word*)&(a))+1) == *(((word*)&(b))+1)) 645#else 646PROBLEM: Cannot deal with word size SIZEOF_WORD 647#endif 648#endif 649 650 /* 651 ** Note we want positive and negative zeros to compare different for 652 ** non-integral constants. 653 */ 654#define Bounds_To_Constant(lo, hi, res) { \ 655 if (((lo) == (hi)) \ 656 && ((lo) != -HUGE_VAL) && ((lo) != HUGE_VAL) \ 657 && ((lo) == ceil(lo))) { \ 658 /* Looks like an integer, so treat it as one. */ \ 659 int result; \ 660 result = ec_double_to_int_or_bignum(lo, res); \ 661 Return_If_Not_Success(result); \ 662 } else if (DoublesIdentical(lo, hi)) { \ 663 Make_Double(res, lo); \ 664 } else { \ 665 Make_Interval(res, lo, hi); \ 666 } \ 667 } 668 669 670 /* 671 ** A couple of macros that abstract iterating over an ECLiPSe list of 672 ** linear terms. 673 ** 674 ** XXX - Don't bother with some of the type checking if it's not the 675 ** first pass over the constraint? 676 */ 677#define BeginIterateLinList(plin, pterm, idx, coef, var) \ 678 idx = -1; \ 679 while (!IsNil(plin->tag)) { \ 680 Check_Pair(plin->tag); \ 681 idx++; \ 682 pterm = plin->val.ptr; \ 683 Dereference(pterm); \ 684 Check_Structure(pterm->tag); \ 685 /* Ignore the functor. */ \ 686 /* Extract the coefficient - use var as temporary. */ \ 687 var = pterm->val.ptr + 1; \ 688 Dereference(var); \ 689 Constant_To_Typed_Bounds(var->val, var->tag, coef); \ 690 /* Extract the variable. */ \ 691 var = pterm->val.ptr + 2; \ 692 Dereference(var); 693 694#define EndIterateLinList(plin) \ 695 /* Move on to next list cell. */ \ 696 plin = plin->val.ptr + 1; \ 697 Dereference(plin); \ 698 } 699 700 701 /* 702 ** Global variables for caching values needed for accessing or 703 ** creating IC attributes. 704 */ 705static int ic_domain_slot; /* IC attribute slot */ 706static int suspend_slot; /* Suspend attribute slot */ 707static dident d_ic_attr_functor; /* IC attribute functor dict entry */ 708static dident d_ic_con; /* ic_con/5 dict entry */ 709static dident d_ic_real; /* real/0 dict entry */ 710static dident d_ic_integer; /* integer/0 dict entry */ 711static dident d_ic_undefined; /* undefined/0 dict entry */ 712static dident d_exclude; /* exclude/2 dict entry */ 713static dident d_exclude_range; /* exclude_range/3 dict entry */ 714static dident d_prop_ic_con; /* prop_ic_con/1 dict entry */ 715static void *proc_exclude; /* exclude/2 procedure */ 716static void *proc_exclude_range; /* exclude_range/3 procedure */ 717static void *proc_prop_ic_con; /* prop_ic_con/1 procedure */ 718static void *proc_infq; /* =</2 procedure */ 719static void *proc_supq; /* >=/2 procedure */ 720 721 722/*---------------------------------------------------------------------- 723** 724** Propagation threshold. 725** 726** The propagation threshold is used to limit the amount of propagation 727** performed when bounds changes are very small. Basically, for non-integer 728** variables, bounds are only changed if the absolute and relative changes 729** of the bound exceed the threshold. See ic_kernel.ecl and ic_design for 730** more details and discussion. 731** 732** We do this in C rather than ECLiPSe since we want convenient access to it 733** from C. 734*/ 735 736 /* The threshold. */ 737static double threshold = 1e-8; 738 739 740 /* 741 ** get_threshold(?Threshold) 742 ** Unify Threshold with the propagation threshold. 743 */ 744int 745p_get_threshold(value vthreshold, type tthreshold) 746{ 747 Return_Unify_Double(vthreshold, tthreshold, threshold); 748} 749 750 /* 751 ** set_threshold(++Threshold) 752 ** Set the propagation threshold to Threshold. 753 */ 754int 755p_set_threshold(value vthreshold, type tthreshold) 756{ 757 Check_Double(tthreshold); 758 threshold = Dbl(vthreshold); 759 760 Succeed 761} 762 763 764/*---------------------------------------------------------------------- 765** 766** Primitives for operating on variables/attributes. 767** 768*/ 769 770 /* 771 ** Use the given bounds and type to create an IC attribute except the 772 ** reference to the variable. 773 */ 774void 775create_ic_attr(pword **attr, double lwb, double upb, int integral) 776{ 777 pword *tmp; 778 779 tmp = TG; 780 Push_Struct_Frame(d_ic_attr_functor); 781 Make_Atom(tmp + OFF_TYPE, integral ? d_ic_integer : d_ic_real); 782 Make_Double(tmp + OFF_LO, lwb); 783 Make_Double(tmp + OFF_HI, upb); 784 Make_Atom(tmp + OFF_BITMAP, d_ic_undefined); 785 Make_Nil(tmp + OFF_WAKE_LO); 786 Make_Nil(tmp + OFF_WAKE_HI); 787 Make_Nil(tmp + OFF_WAKE_HOLE); 788 Make_Nil(tmp + OFF_WAKE_TYPE); 789 790 *attr = tmp; 791} 792 793 794/* 795** Retrieve the IC attribute of a variable, creating one if it doesn't 796** exist. 'var' must be dereferenced and 'IsRef'. 797*/ 798pword * 799make_ic_var_attr(pword *var) 800{ 801 pword *attr; 802 803 if (IsMeta(var->tag)) { 804 IC_Var_Get_Attr(var, attr); 805 if (IsRef(attr->tag)) { 806 pword *pattr; 807 Create_Default_IC_Attr(pattr); 808 Fill_Var_Field(pw, var); 809 Bind_Var(attr->val, attr->tag, pattr, TCOMP); 810 notify_constrained(var); 811 } 812 } else { 813 pword *pw, *pattr; 814 Create_Default_IC_Attr(pattr); 815 pw = (pword *)add_attribute(var->tag.all, 816 pattr, TCOMP, ic_domain_slot); 817 Fill_Var_Field(pw, var); 818 Bind_Var(var->val, var->tag, pw, TREF); 819 var = pw; /* Implicit Deref(var) */ 820 IC_Var_Get_Attr(var, attr); 821 } 822 823 return attr; 824} 825 826 827 /* 828 ** Use this one if you know it already has an attribute. 829 */ 830void 831get_var_info(pword *x, var_info *vi) 832{ 833 pword *attr; 834 dident ic_type; 835 vi->var = x; 836 IC_Var_Get_Attr(x, attr); 837 attr = attr->val.ptr; 838 Dereference(attr); 839 vi->attr = attr; 840 IC_Var_Info(vi->attr, vi->tb.b.l, vi->tb.b.u, ic_type, vi->bitmap); 841 vi->tb.i = Type_Is_Int(ic_type); 842 vi->prop_int = 0; 843} 844 845 /* 846 ** Use this one if it might not have an attribute (it will give it one). 847 */ 848void 849make_var_info(pword *x, var_info *vi) 850{ 851 dident ic_type; 852 vi->var = x; 853 IC_Var_Attr_Vec(x, vi->attr); 854 IC_Var_Info(vi->attr, vi->tb.b.l, vi->tb.b.u, ic_type, vi->bitmap); 855 vi->tb.i = Type_Is_Int(ic_type); 856 vi->prop_int = 0; 857} 858 859void 860get_var_info_from_attr(pword *x, pword *attr, var_info *vi) 861{ 862 dident ic_type; 863 vi->var = x; 864 vi->attr = attr->val.ptr; 865 IC_Var_Info(vi->attr, vi->tb.b.l, vi->tb.b.u, ic_type, vi->bitmap); 866 vi->tb.i = Type_Is_Int(ic_type); 867 vi->prop_int = 0; 868} 869 870 871 /* 872 ** set_type_integral(var_info) 873 ** Set the given variable to be integral. Note that this assumes 874 ** that the variable is not already integral. Note also that the 875 ** variable's bounds are not updated, even if they now need 876 ** rounding. However, the constrained and type change wake lists 877 ** are notified. 878 ** cf. set_integral(), which also updates the bounds. 879 */ 880int 881set_type_integral(var_info *vi) 882{ 883 value val; 884 type tag; 885 int result; 886 887 /* Update the type. */ 888 val.did = d_.integer0; 889 tag.kernel = TDICT; 890 ec_assign(vi->attr + OFF_TYPE, val, tag); 891 vi->tb.i = 1; 892 893 /* Notify constrained / type change. */ 894 result = notify_constrained(vi->var); 895 Return_If_Not_Success(result) 896 return ec_schedule_susps(vi->attr + OFF_WAKE_TYPE); 897} 898 899 /* 900 ** ic_lwb(var_info, bound) 901 ** Given info about a variable (var_info), impose the given lower 902 ** bound. 903 */ 904int 905ic_lwb(var_info *vi, double bound) 906{ 907 int result; 908 double abs_delta; 909 value val; 910 type tag; 911 912 if (bound <= vi->tb.b.l) { 913 Succeed 914 } 915 916 if (bound > vi->tb.b.u) { 917 Fail 918 } 919 920 /* 921 ** Note that the following rounding will not change the results of 922 ** the bounds tests made above (since the variable bounds will be 923 ** integers if rounding occurs here). 924 */ 925 maybe_round_up(vi->tb.i, bound); 926 927 if (bound == vi->tb.b.u) { 928 Set_Var_To_Value(vi, bound) 929 /* No more to do. */ 930 Succeed 931 } else /* bound > lwb */ { 932 if (!vi->tb.i) { 933 abs_delta = bound - vi->tb.b.l; 934 if (abs_delta != HUGE_VAL && (abs_delta <= threshold || 935 abs_delta <= threshold * fabs(vi->tb.b.l))) { 936 /* Bound change is below the threshold, so ignore it. */ 937 /* 938 ** XXX - instead of not modifying the bound (so that no 939 ** further propagation occurs), should we instead update 940 ** the bound, and just not wake anything? 941 */ 942 /* 943 bound = vi->tb.b.l; 944 status = IC_SLACK; 945 */ 946 Succeed 947 } 948 } else { 949 if (!IsAtom(vi->bitmap->tag)) { 950 word int_bound; 951 word new_int_bound; 952 953 /* 954 ** Note that due to the existence of a bitmap, we can 955 ** assume it's safe to convert between ints and doubles. 956 */ 957 958 /* Check for holes. */ 959 int_bound = (word) bound; 960 result = next_greater_member(vi->bitmap->val.wptr, 961 int_bound - 1, &new_int_bound); 962 963 if (Result_Is_Empty(result)) { 964 /* No entry in bitmap. */ 965 Fail 966 } 967 968 if (Result_Is_Slack(result)) { 969 /* There was a hole at bound. */ 970 bound = (double) new_int_bound; 971 972 if (bound == vi->tb.b.u) { 973 Set_Var_To_Value(vi, bound) 974 /* No more to do. */ 975 Succeed 976 } 977 } 978 } 979 } 980 } 981 982 /* If we get here, then the bound needs to be updated. */ 983 984 Make_Checked_Double_Val(val, bound); 985 tag.kernel = TDBL; 986 ec_assign(vi->attr + OFF_LO, val, tag); 987 vi->tb.b.l = bound; 988 989 if (!IsAtom(vi->bitmap->tag)) { 990 /* Need to update the bitmap. */ 991 uword *new_bitmap; 992 993 result = set_bitmap_lwb(vi->bitmap->val.wptr, (word) bound, 994 &new_bitmap); 995 996 if (Result_Is_Empty(result)) { 997 /* Bound should not be bitmap empty. */ 998 Bip_Error(EC_EXTERNAL_ERROR); 999 } 1000 1001 /* Update the bitmap. */ 1002 Update_Bitmap(vi, new_bitmap) 1003 } 1004 1005 /* Notify constrained. */ 1006 result = notify_constrained(vi->var); 1007 Return_If_Not_Success(result) 1008 1009 /* Schedule suspensions (lo). */ 1010 return ec_schedule_susps(vi->attr + OFF_WAKE_LO); 1011} 1012 1013 1014 /* 1015 ** ic_impose_min(?Var, ++Bound) 1016 ** Applies the lower bound `Bound' to the variable `Var'. 1017 ** Note that the `Var' must not be ground. 1018 */ 1019int 1020p_ic_impose_min(value vvar, type tvar, value vc, type tc) 1021{ 1022 var_info vi; 1023 double bound; 1024 1025 Check_Ref(tvar); 1026 Constant_To_Lower_Bound(vc, tc, bound); 1027 1028 make_var_info(vvar.ptr, &vi); 1029 1030 return ic_lwb(&vi, bound); 1031} 1032 1033 1034 /* 1035 ** ic_upb(var_info, bound) 1036 ** Given info about a variable (var_info), impose the given upper 1037 ** bound. 1038 */ 1039int 1040ic_upb(var_info *vi, double bound) 1041{ 1042 int result; 1043 double abs_delta; 1044 value val; 1045 type tag; 1046 1047 if (bound >= vi->tb.b.u) { 1048 Succeed 1049 } 1050 1051 if (bound < vi->tb.b.l) { 1052 Fail 1053 } 1054 1055 /* 1056 ** Note that the following rounding will not change the results of 1057 ** the bounds tests made above (since the variable bounds will be 1058 ** integers if rounding occurs here). 1059 */ 1060 maybe_round_down(vi->tb.i, bound); 1061 1062 if (bound == vi->tb.b.l) { 1063 Set_Var_To_Value(vi, bound) 1064 /* No more to do. */ 1065 Succeed 1066 } else /* bound < upb */ { 1067 if (!vi->tb.i) { 1068 abs_delta = vi->tb.b.u - bound; 1069 if (abs_delta != HUGE_VAL && (abs_delta <= threshold || 1070 abs_delta <= threshold * fabs(vi->tb.b.u))) { 1071 /* Bound change is below the threshold, so ignore it. */ 1072 /* 1073 ** XXX - instead of not modifying the bound (so that no 1074 ** further propagation occurs), should we instead update 1075 ** the bound, and just not wake anything? 1076 */ 1077 /* 1078 bound = vi->tb.b.u; 1079 status = IC_SLACK; 1080 */ 1081 Succeed 1082 } 1083 } else { 1084 if (!IsAtom(vi->bitmap->tag)) { 1085 word int_bound; 1086 word new_int_bound; 1087 1088 /* 1089 ** Note that due to the existence of a bitmap, we can 1090 ** assume it's safe to convert between ints and doubles. 1091 */ 1092 1093 /* Check for holes. */ 1094 int_bound = (word) bound; 1095 result = next_smaller_member(vi->bitmap->val.wptr, 1096 int_bound + 1, &new_int_bound); 1097 1098 if (Result_Is_Empty(result)) { 1099 /* No entry in bitmap. */ 1100 Fail 1101 } 1102 1103 if (Result_Is_Slack(result)) { 1104 /* There was a hole at bound. */ 1105 bound = (double) new_int_bound; 1106 1107 if (bound == vi->tb.b.l) { 1108 Set_Var_To_Value(vi, bound) 1109 /* No more to do. */ 1110 Succeed 1111 } 1112 } 1113 } 1114 } 1115 } 1116 1117 /* If we get here, then the bound needs to be updated. */ 1118 1119 Make_Checked_Double_Val(val, bound); 1120 tag.kernel = TDBL; 1121 ec_assign(vi->attr + OFF_HI, val, tag); 1122 vi->tb.b.u = bound; 1123 1124 if (!IsAtom(vi->bitmap->tag)) { 1125 /* Need to update the bitmap. */ 1126 uword *new_bitmap; 1127 1128 result = set_bitmap_upb(vi->bitmap->val.wptr, (word) bound, 1129 &new_bitmap); 1130 1131 if (Result_Is_Empty(result)) { 1132 /* Bound should not be empty. */ 1133 Bip_Error(EC_EXTERNAL_ERROR); 1134 } 1135 1136 /* Update the bitmap. */ 1137 Update_Bitmap(vi, new_bitmap) 1138 } 1139 1140 /* Notify constrained. */ 1141 result = notify_constrained(vi->var); 1142 Return_If_Not_Success(result) 1143 1144 /* Schedule suspensions (hi). */ 1145 return ec_schedule_susps(vi->attr + OFF_WAKE_HI); 1146} 1147 1148 1149 /* 1150 ** ic_impose_max(?Var, ++Bound) 1151 ** Applies the upper bound `Bound' to the variable `Var'. 1152 ** Note that the `Var' must not be ground. 1153 */ 1154int 1155p_ic_impose_max(value vvar, type tvar, value vc, type tc) 1156{ 1157 var_info vi; 1158 double bound; 1159 1160 Check_Ref(tvar); 1161 Constant_To_Upper_Bound(vc, tc, bound); 1162 1163 make_var_info(vvar.ptr, &vi); 1164 1165 return ic_upb(&vi, bound); 1166} 1167 1168 1169 /* 1170 ** ic_impose_bounds(?Var, ++Lwb, ++Upb) 1171 ** Applies the lower bound `Lwb' and upper bound `Upb' to the 1172 ** variable `Var'. Note that the `Var' must not be ground. 1173 */ 1174int 1175p_ic_impose_bounds(value vvar, type tvar, value vlwb, type tlwb, value vupb, type tupb) 1176{ 1177 var_info vi; 1178 double new_lwb, new_upb; 1179 int result; 1180 1181 Check_Ref(tvar); 1182 Constant_To_Lower_Bound(vlwb, tlwb, new_lwb); 1183 Constant_To_Upper_Bound(vupb, tupb, new_upb); 1184 1185 make_var_info(vvar.ptr, &vi); 1186 1187 result = ic_lwb(&vi, new_lwb); 1188 Return_If_Not_Success(result); 1189 return ic_upb(&vi, new_upb); 1190} 1191 1192 1193 /* 1194 ** Create an IC attribute for a variable with the given parameters, or 1195 ** constrain it if it already exists. 'var' must be dereferenced and 1196 ** 'IsRef'; the function returns a suitably dereferenced copy when done. 1197 */ 1198int 1199make_constrained_ic_var(pword **pvar, double lwb, double upb, int integral) 1200{ 1201 pword *var = *pvar; 1202 int result; 1203 1204 if (IsMeta(var->tag)) { 1205 pword *attr; 1206 IC_Var_Get_Attr(var, attr); 1207 if (IsRef(attr->tag)) { 1208 pword *pw; 1209 create_ic_attr(&pw, lwb, upb, integral); 1210 Fill_Var_Field(pw, var); 1211 Bind_Var(attr->val, attr->tag, pw, TCOMP); 1212 notify_constrained(var); 1213 } else { 1214 /* Attribute already exists, so must constrain it. */ 1215 var_info vi; 1216 get_var_info_from_attr(var, attr, &vi); 1217 if (integral && !vi.tb.i) { 1218 result = set_type_integral(&vi); 1219 Return_If_Not_Success(result) 1220 /* Make sure bounds are not left unrounded. */ 1221 if (lwb <= vi.tb.b.l) 1222 lwb = ceil(vi.tb.b.l); 1223 if (upb >= vi.tb.b.u) 1224 upb = floor(vi.tb.b.u); 1225 } 1226 result = ic_lwb(&vi, lwb); 1227 Return_If_Not_Success(result) 1228 result = ic_upb(&vi, upb); 1229 Return_If_Not_Success(result) 1230 1231 /* In case now ground. */ 1232 Dereference(var); 1233 /* var = var->val.ptr; */ 1234 } 1235 } else { 1236 pword *pw, *attr; 1237 create_ic_attr(&attr, lwb, upb, integral); 1238 pw = (pword *)add_attribute(var->tag.all, 1239 attr, TCOMP, ic_domain_slot); 1240 Fill_Var_Field(pw, var); 1241 Bind_Var(var->val, var->tag, pw, TREF); 1242 var = pw; /* Implicit Deref(var) */ 1243 } 1244 1245 *pvar = var; 1246 Succeed 1247} 1248 1249 1250 /* 1251 ** Constrain a variable to be a boolean. 1252 */ 1253int 1254p_make_bool(value vbool, type tbool) 1255{ 1256 if (!IsRef(tbool)) { 1257 Check_Integer(tbool); 1258 if (vbool.nint < 0 || vbool.nint > 1) { 1259 Fail 1260 } 1261 } else { 1262 /* Make sure it's an IC boolean. */ 1263 return make_constrained_ic_var(&vbool.ptr, 0.0, 1.0, 1); 1264 } 1265 1266 Succeed 1267} 1268 1269 1270 /* 1271 ** set_integral(var_info) 1272 ** Set the given variable to be integral. Note that this assumes 1273 ** that the variable is not already integral. The variable's 1274 ** bounds are updated and waking lists woken as appropriate. 1275 ** cf. set_type_integral(), which does not update the bounds. 1276 */ 1277int 1278set_integral(var_info *vi) 1279{ 1280 double bnd; 1281 int result; 1282 1283 result = set_type_integral(vi); 1284 Return_If_Not_Success(result) 1285 bnd = ceil(vi->tb.b.l); 1286 if (bnd > vi->tb.b.l) { 1287 result = ic_lwb(vi, bnd); 1288 Return_If_Not_Success(result) 1289 } 1290 bnd = floor(vi->tb.b.u); 1291 if (bnd < vi->tb.b.u) { 1292 result = ic_upb(vi, bnd); 1293 Return_If_Not_Success(result) 1294 } 1295 1296 Succeed 1297} 1298 1299 1300 /* 1301 ** set_var_integer(?Var) 1302 ** Constrains the variable `Var' to be integral. Note that the 1303 ** variable must not be ground. 1304 */ 1305int 1306p_set_var_integer(value vvar, type tvar) 1307{ 1308 var_info vi; 1309 1310 Check_Ref(tvar); 1311 1312 make_var_info(vvar.ptr, &vi); 1313 1314 if (!vi.tb.i) { 1315 return set_integral(&vi); 1316 } 1317 1318 Succeed 1319} 1320 1321 1322int 1323set_up_exclude_delayed_goal(var_info *vi, word exclude) 1324{ 1325 pword goal, susp, *pw; 1326 int result; 1327 int delayed = 0; 1328 1329 pw = TG; 1330 Push_Struct_Frame(d_exclude); 1331 pw[1].val.ptr = vi->var; 1332 pw[1].tag.kernel = TREF; 1333 pw[2].val.nint = exclude; 1334 pw[2].tag.kernel = TINT; 1335 Make_Struct(&goal, pw); 1336 1337 result = ec_make_suspension(goal, 3, proc_exclude, &susp); 1338 if (result == DEBUG_SUSP_EVENT) { 1339 delayed = 1; 1340 result = PSUCCEED; 1341 } 1342 Return_If_Not_Success(result) 1343 1344 /* Wake on lower/upper bound changes. */ 1345 result = ec_enter_suspension(vi->attr + OFF_WAKE_LO, susp.val.ptr); 1346 Return_If_Not_Success(result) 1347 result = ec_enter_suspension(vi->attr + OFF_WAKE_HI, susp.val.ptr); 1348 Return_If_Not_Success(result) 1349 1350 return delayed ? DEBUG_SUSP_EVENT : PSUCCEED; 1351} 1352 1353 1354 /* 1355 ** ic_exclude(var_info, exclude) 1356 ** Excludes the element `exclude' from the domain of the variable. 1357 ** Note that the variable must be integral and must not be ground. 1358 ** 1359 ** If the value cannot be excluded (because it would result in a 1360 ** bitmap which was considered too large, or the bounds are just 1361 ** too large) then a delayed goal is set up to deal with it later. 1362 */ 1363int 1364ic_exclude(var_info *vi, word exclude) 1365{ 1366 word int_lwb; 1367 word int_upb; 1368 uword *bitmap; 1369 uword *new_bitmap; 1370 int result; 1371 int out_of_range = 0; 1372 1373 if (!vi->tb.i) { 1374 Bip_Error(TYPE_ERROR) 1375 } 1376 1377 if (vi->tb.b.l >= MIN_BITMAP_RANGE && vi->tb.b.l <= MAX_BITMAP_RANGE) { 1378 int_lwb = (word) vi->tb.b.l; 1379 if (exclude < int_lwb) { 1380 Succeed 1381 } 1382 if (exclude == int_lwb) { 1383 return ic_lwb(vi, (double) (exclude+1)); 1384 } 1385 } else { 1386 out_of_range = 1; 1387 } 1388 1389 if (vi->tb.b.u >= MIN_BITMAP_RANGE && vi->tb.b.u <= MAX_BITMAP_RANGE) { 1390 int_upb = (word) vi->tb.b.u; 1391 if (exclude > int_upb) { 1392 Succeed 1393 } 1394 if (exclude == int_upb) { 1395 return ic_upb(vi, (double) (exclude-1)); 1396 } 1397 } else { 1398 out_of_range = 1; 1399 } 1400 1401 if (out_of_range) { 1402 return set_up_exclude_delayed_goal(vi, exclude); 1403 } 1404 1405 /* int_lwb < exclude < int_upb */ 1406 1407 if (IsAtom(vi->bitmap->tag)) { 1408 /* Allocate a new bitmap. */ 1409 result = create_bitmap(int_lwb, int_upb, &bitmap); 1410 Return_If_Not_Success(result) 1411 } else { 1412 bitmap = vi->bitmap->val.wptr; 1413 } 1414 1415 result = remove_bitmap_element(bitmap, exclude, &new_bitmap); 1416 1417 if (Result_Is_Empty(result)) { 1418 /* Bitmap is empty, so no solution. */ 1419 Fail 1420 } 1421 1422 if (Result_Is_Change(result)) { 1423 Update_Bitmap(vi, new_bitmap) 1424 1425 /* Notify constrained. */ 1426 result = notify_constrained(vi->var); 1427 Return_If_Not_Success(result) 1428 1429 /* Schedule suspensions (hole). */ 1430 result = ec_schedule_susps(vi->attr + OFF_WAKE_HOLE); 1431 Return_If_Not_Success(result) 1432 } 1433 1434 Succeed 1435} 1436 1437 1438 /* 1439 ** ic_exclude(?Var, ++Excl) 1440 ** Excludes the element `Excl' from the domain of the variable 1441 ** `Var'. Note that the variable must be integral and must not be 1442 ** ground. 1443 */ 1444int 1445p_ic_exclude(value vvar, type tvar, value vc, type tc) 1446{ 1447 var_info vi; 1448 1449 Check_Ref(tvar); 1450 Check_Integer(tc); 1451 1452 make_var_info(vvar.ptr, &vi); 1453 1454 return ic_exclude(&vi, vc.nint); 1455} 1456 1457 1458int 1459set_up_exclude_range_delayed_goal(var_info *vi, word int_lwb, word int_upb) 1460{ 1461 pword goal, susp, *pw; 1462 int result; 1463 int delayed = 0; 1464 1465 pw = TG; 1466 Push_Struct_Frame(d_exclude_range); 1467 pw[1].val.ptr = vi->var; 1468 pw[1].tag.kernel = TREF; 1469 pw[2].val.nint = int_lwb; 1470 pw[2].tag.kernel = TINT; 1471 pw[3].val.nint = int_upb; 1472 pw[3].tag.kernel = TINT; 1473 Make_Struct(&goal, pw); 1474 1475 result = ec_make_suspension(goal, 3, proc_exclude_range, &susp); 1476 if (result == DEBUG_SUSP_EVENT) { 1477 delayed = 1; 1478 result = PSUCCEED; 1479 } 1480 Return_If_Not_Success(result) 1481 1482 /* Wake on lower/upper bound changes. */ 1483 result = ec_enter_suspension(vi->attr + OFF_WAKE_LO, susp.val.ptr); 1484 Return_If_Not_Success(result) 1485 result = ec_enter_suspension(vi->attr + OFF_WAKE_HI, susp.val.ptr); 1486 Return_If_Not_Success(result) 1487 1488 return delayed ? DEBUG_SUSP_EVENT : PSUCCEED; 1489} 1490 1491 1492 /* 1493 ** ic_exclude_range(var_info, int_lwb, int_upb) 1494 ** Excludes all the elements from `int_lwb' to `int_upb', 1495 ** inclusive, from the domain of the variable `var_info'. Note 1496 ** that the variable must be integral and must not be ground. 1497 ** 1498 ** If the range cannot be excluded (because it would result in a 1499 ** bitmap which was considered too large, or the variable's bounds 1500 ** are just too large) then a delayed goal is set up to deal with 1501 ** it later. 1502 */ 1503int 1504ic_exclude_range(var_info *vi, word int_lwb0, word int_upb0) 1505{ 1506 word int_lwb; 1507 word int_upb; 1508 uword *bitmap; 1509 uword *new_bitmap; 1510 int result; 1511 int out_of_range = 0; 1512 1513 if (!vi->tb.i) { 1514 Bip_Error(TYPE_ERROR) 1515 } 1516 1517 if (vi->tb.b.l >= MIN_BITMAP_RANGE && vi->tb.b.l <= MAX_BITMAP_RANGE) { 1518 int_lwb = (word) vi->tb.b.l; 1519 if (int_upb0 < int_lwb) { 1520 Succeed 1521 } 1522 if (int_upb0 > MAX_BITMAP_RANGE) { 1523 Bip_Error(RANGE_ERROR) 1524 } 1525 if (int_lwb0 <= int_lwb) { 1526 return ic_lwb(vi, (double) (int_upb0 + 1)); 1527 } 1528 } else { 1529 out_of_range = 1; 1530 } 1531 1532 if (vi->tb.b.u >= MIN_BITMAP_RANGE && vi->tb.b.u <= MAX_BITMAP_RANGE) { 1533 int_upb = (word) vi->tb.b.u; 1534 if (int_lwb0 > int_upb) { 1535 Succeed 1536 } 1537 if (int_lwb0 < MIN_BITMAP_RANGE) { 1538 Bip_Error(RANGE_ERROR) 1539 } 1540 if (int_upb0 >= int_upb) { 1541 return ic_upb(vi, (double) (int_lwb0 - 1)); 1542 } 1543 } else { 1544 out_of_range = 1; 1545 } 1546 1547 if (out_of_range) { 1548 return set_up_exclude_range_delayed_goal(vi, int_lwb0, int_upb0); 1549 } 1550 1551 /* int_lwb < int_lwb0 <= int_upb0 < int_upb */ 1552 1553 if (IsAtom(vi->bitmap->tag)) { 1554 /* Allocate a new bitmap. */ 1555 result = create_bitmap(int_lwb, int_upb, &bitmap); 1556 Return_If_Not_Success(result) 1557 } else { 1558 bitmap = vi->bitmap->val.wptr; 1559 } 1560 1561 result = remove_bitmap_range(bitmap, int_lwb0, int_upb0, &new_bitmap); 1562 1563 if (Result_Is_Empty(result)) { 1564 /* Bitmap is empty, so no solution. */ 1565 Fail 1566 } 1567 1568 if (Result_Is_Change(result)) { 1569 Update_Bitmap(vi, new_bitmap) 1570 1571 /* Notify constrained. */ 1572 result = notify_constrained(vi->var); 1573 Return_If_Not_Success(result) 1574 1575 /* Schedule suspensions (hole). */ 1576 result = ec_schedule_susps(vi->attr + OFF_WAKE_HOLE); 1577 Return_If_Not_Success(result) 1578 } 1579 1580 Succeed 1581} 1582 1583 1584 /* 1585 ** ic_exclude_range(?Var, ++Lwb, ++Upb) 1586 ** Excludes all the elements from `Lwb' to `Upb', inclusive, from 1587 ** the domain of the variable `Var'. Note that the variable must 1588 ** be integral and must not be ground. 1589 */ 1590int 1591p_ic_exclude_range(value vvar, type tvar, value vlo, type tlo, value vhi, type thi) 1592{ 1593 var_info vi; 1594 1595 Check_Ref(tvar); 1596 Check_Integer(tlo); 1597 Check_Integer(thi); 1598 1599 make_var_info(vvar.ptr, &vi); 1600 1601 return ic_exclude_range(&vi, vlo.nint, vhi.nint); 1602} 1603 1604 1605 /* Solves a * x (op) c */ 1606 /* op: 1 for lower bound, 2 for upper bound, 3 for both. */ 1607int 1608impose_coef_bounds(int op, int integer_strict, bounds *a, var_info *vi, 1609 bounds *c) 1610{ 1611 bounds res; 1612 int neg_coef; 1613 int result; 1614 1615 neg_coef = ((a->u) <= 0.0); 1616 /* Only propagate if coefficient doesn't span zero. */ 1617 if (neg_coef || ((a->l) >= 0.0)) { 1618 Div(*c, *a, res); 1619 1620 if (OpIsEqual(op)) { 1621 result = ic_lwb(vi, res.l); 1622 Return_If_Not_Success(result) 1623 result = ic_upb(vi, res.u); 1624 Return_If_Not_Success(result) 1625 } else 1626 /* If coef is negative, swap which bounds to impose. */ 1627 if ((op) == neg_coef + 1) { 1628 /* Impose lower bound. */ 1629 if ((integer_strict) && (op) == 1 && 1630 vi->tb.i && res.l == ceil(res.l)) { 1631 set_round_down(); 1632 res.l += 1; 1633 restore_round_mode(); 1634 } 1635 result = ic_lwb(vi, res.l); 1636 Return_If_Not_Success(result) 1637 } else { 1638 /* Impose upper bound. */ 1639 if ((integer_strict) && (op) == 1 && 1640 vi->tb.i && res.u == floor(res.u)) { 1641 set_round_up(); 1642 res.u -= 1; 1643 restore_round_mode(); 1644 } 1645 result = ic_upb(vi, res.u); 1646 Return_If_Not_Success(result) 1647 } 1648 } 1649 1650 Succeed 1651} 1652 1653 /* 1654 ** Solves a * x = c 1655 ** Just binds the variable, if possible & appropriate. 1656 ** solved is a boolean which will be set to zero if the constraint is 1657 ** not fully resolved (i.e. a delayed goal should be left behind). 1658 */ 1659int 1660solve_equal(bounds *a, var_info *vi, bounds *c, int *solved) 1661{ 1662 bounds res; 1663 pword tmp; 1664 int result; 1665 1666 Div(*c, *a, res); 1667 1668 if (vi->prop_int && res.l == res.u && res.l == ceil(res.l)) { 1669 result = ec_double_to_int_or_bignum(res.l, &tmp); 1670 Return_If_Not_Success(result); 1671 result = Unify_Pw(vi->var->val, vi->var->tag, tmp.val, tmp.tag); 1672 Return_If_Not_Success(result); 1673 *solved = 1; 1674 } else if (vi->tb.i) { 1675 res.l = ceil(res.l); 1676 res.u = floor(res.u); 1677 if (res.l == res.u) { 1678 /* Due to rounding, the Div above may suggest a solution when 1679 * none exists. Compute a*X to see if it really overlaps c. 1680 * (was bug 669) */ 1681 bounds computed_c; 1682 Mul(res, *a, computed_c); 1683 if (computed_c.l > c->u || computed_c.u < c->l) { 1684 Fail 1685 } 1686 result = ec_double_to_int_or_bignum(res.l, &tmp); 1687 Return_If_Not_Success(result); 1688 result = Unify_Pw(vi->var->val, vi->var->tag, tmp.val, tmp.tag); 1689 Return_If_Not_Success(result); 1690 *solved = (c->l==c->u && computed_c.l==computed_c.u); 1691 } else if (res.l > res.u) { 1692 Fail 1693 } else { 1694 /* Should avoid rounding bounds again? */ 1695 result = ic_lwb(vi, res.l); 1696 Return_If_Not_Success(result) 1697 result = ic_upb(vi, res.u); 1698 Return_If_Not_Success(result) 1699 *solved = 0; 1700 } 1701 } else { 1702 Make_Interval(&tmp, res.l, res.u); 1703 result = Unify_Pw(vi->var->val, vi->var->tag, tmp.val, tmp.tag); 1704 Return_If_Not_Success(result); 1705 *solved = 1; 1706 } 1707 1708 Succeed 1709} 1710 1711 1712 /* 1713 ** If it's an integer variable, see if we can just 1714 ** exclude a single element from its domain to make it 1715 ** entailed. 1716 ** Note does not check for "out of bounds" entailment. 1717 */ 1718int 1719solve_not_equal(bounds *a, var_info *vi, bounds *c, int *solved) 1720{ 1721 bounds res; 1722 int result; 1723 1724 *solved = 0; 1725 1726 if (c->l == c->u && a->l == a->u && vi->tb.i) { 1727 Div(*c, *a, res); 1728 1729 if ((res.l == res.u) && (ceil(res.l) == res.l)) { 1730 /* Exclude the value. */ 1731 if (res.l < (double) MIN_S_WORD || 1732 res.l >= ((double) MAX_S_WORD + 1.0)) { 1733 /* XXX - update to handle bignums. */ 1734 Bip_Error(RANGE_ERROR) 1735 } 1736 result = ic_exclude(vi, (word) res.l); 1737 Return_If_Not_Success(result); 1738 *solved = 1; 1739 } else if (res.u < ceil(res.l) && res.l > floor(res.u)) { 1740 /* Value falls between integers. */ 1741 *solved = 1; 1742 } 1743 } else { 1744 Mul(*a, vi->tb.b, res); 1745 1746 if (c->l > res.u || c->u < res.l) { 1747 /* Entailed. */ 1748 *solved = 1; 1749 } 1750 } 1751 1752 Succeed 1753} 1754 1755 1756/*---------------------------------------------------------------------- 1757** 1758** Functions for working with constraint data structures. 1759** 1760*/ 1761 1762 /* 1763 ** Update the constraint data buffer based on the contents of the 1764 ** con_info structure. If the buffer needs to be trailed, create a new 1765 ** buffer for the new data, trail it, etc. If it doesn't need to be 1766 ** trailed, just overwrite the contents. 1767 ** 1768 ** Also updates the suspension priority of the constraint, in case the 1769 ** priority should have changed (the constraint has gotten shorter). 1770 */ 1771int 1772update_con_data_buf(con_info *con_info) 1773{ 1774 pword *susp; 1775 pword prio; 1776 1777 if (Trail_Needed(con_info->data)) { 1778 pword *tmp; 1779 Allocate_Con_Data_Buf(con_info); 1780 tmp = con_info->con + CON_OFF_DATA; 1781 Trail_Pword(tmp); 1782 (tmp)->val.ptr = (con_info->data); 1783 (tmp)->tag.kernel = TSTRG; 1784 } 1785 Set_Con_Data_Buf(con_info); 1786 1787 /* Update the priority of the suspension in case it's changed. */ 1788 susp = con_info->con + CON_OFF_SUSP; 1789 Dereference(susp); 1790 prio.val.nint = ConstraintPriority(con_info); 1791 prio.tag.kernel = TINT; 1792 return p_set_suspension_priority(susp->val, susp->tag, prio.val, prio.tag); 1793} 1794 1795 1796 /* 1797 ** Extract the data from the argument vector an ECLiPSe constraint 1798 ** structure, and put it in a con_info structure. 1799 */ 1800void 1801con_struct_vec_to_con_info(pword *con_ecl_struct_vec, con_info* con) 1802{ 1803 pword *tmp; 1804 int status; 1805 1806 con->con = con_ecl_struct_vec; 1807 1808 tmp = con_ecl_struct_vec + CON_OFF_DATA; 1809 Dereference(tmp); 1810 con->data = tmp->val.ptr; 1811 Dereference(con->data); /* Not necessary? */ 1812 1813 con->flags = *ConBufEntry(con->data, CON_DATA_OFF_FLAGS); 1814 con->term_count = *ConBufEntry(con->data, CON_DATA_OFF_COUNT); 1815 con->old_term_count = con->term_count; 1816 con->c.l = *((double *) ConBufEntry(con->data, CON_DATA_OFF_RHS_LO)); 1817 con->c.u = *((double *) ConBufEntry(con->data, CON_DATA_OFF_RHS_HI)); 1818 1819 if (con->term_count > 0) { 1820 tmp = con_ecl_struct_vec + CON_OFF_LO_VEC; 1821 Dereference(tmp); 1822 tmp = tmp->val.ptr; 1823 Dereference(tmp); /* Not necessary? */ 1824 con->lo_vec = CoefVec(tmp); 1825 1826 tmp = con_ecl_struct_vec + CON_OFF_HI_VEC; 1827 Dereference(tmp); 1828 tmp = tmp->val.ptr; 1829 Dereference(tmp); /* Not necessary? */ 1830 con->hi_vec = CoefVec(tmp); 1831 1832 tmp = con_ecl_struct_vec + CON_OFF_VAR_VEC; 1833 Dereference(tmp); 1834 tmp = tmp->val.ptr; 1835 Dereference(tmp); /* Not necessary? */ 1836 con->var_vec = VarVec(tmp); 1837#ifdef IC_DEBUG 1838 } else { 1839 con->lo_vec = 0; 1840 con->hi_vec = 0; 1841 con->var_vec = 0; 1842#endif 1843 } 1844 1845 tmp = con_ecl_struct_vec + CON_OFF_SUSP; 1846 Dereference(tmp); 1847 con->susp = tmp; 1848 1849 tmp = con_ecl_struct_vec + CON_OFF_BOOLEAN; 1850 Dereference(tmp); 1851 con->bool = tmp; 1852 1853 /* 1854 ** Set status to the effective value of the boolean (treat it as 1855 ** true if the boolean is still a variable). 1856 */ 1857 if (IsRef(con->bool->tag)) { 1858 status = 1; 1859 con->reified = 1; 1860 } else { 1861 status = con->bool->val.nint; 1862 con->reified = 0; 1863 } 1864 con->op = FlagsAndBoolToOp(con->flags, status); 1865 1866 /* 1867 (((((flags) & CON_EQUATION) + 1) * (2 * (bool) - 1) + 3) / 2) 1868 bool=1: (((flags & CON_EQUATION) >> 1) + 2) 1869 bool=0: (1 - ((flags & CON_EQUATION) >> 1)) 1870 */ 1871} 1872 1873 1874#if 0 1875This not used yet (but probably should be?). The idea was to have the start 1876and end of the constraint set-up close together in the code... 1877 1878Note that this copy of the code is now a little out-of-date. 1879 1880void 1881start_setting_up_con_struct(con_info *con, int flags, value vbool, type tbool, 1882 value vlin, type tlin) 1883{ 1884 int status; 1885 1886 /* 1887 ** Set status to the effective value of the boolean (treat it as 1888 ** true if the boolean is still a variable). 1889 */ 1890 if (IsRef(tbool)) { 1891 status = 1; 1892 } else { 1893 status = vbool.nint; 1894 } 1895 1896 con->c.l = NEG_ZERO; 1897 con->c.u = 0.0; 1898 con->flags = flags; 1899 con->term_count = 0; 1900 con->op = FlagsAndBoolToOp(flags, status); 1901 1902 /* Create the ic_con structure. */ 1903 con->con = TG; 1904 Push_Struct_Frame(d_ic_con); 1905 1906 con->con[CON_OFF_BOOLEAN].val.all = vbool.all; 1907 con->con[CON_OFF_BOOLEAN].tag.all = tbool.all; 1908#if 0 1909#if 1 1910 con->con[CON_OFF_SUSP].val.all = vsusp.all; 1911 con->con[CON_OFF_SUSP].tag.all = tsusp.all; 1912#else 1913 con->con[CON_OFF_SUSP].val.ptr = con->con + CON_OFF_SUSP; 1914 con->con[CON_OFF_SUSP].tag.kernel = TREF; 1915 result = Unify_Pw(con->con[CON_OFF_SUSP].val, con->con[CON_OFF_SUSP].tag, vsusp, tsusp); 1916 Return_If_Not_Success(result); 1917#endif 1918#endif 1919} 1920#endif 1921 1922 1923 /* 1924 ** finish_setting_up_con_struct 1925 ** Uses the information provided to finish setting up the ECLiPSe 1926 ** constraint structure. 1927 */ 1928void 1929finish_setting_up_con_struct(con_info *con, pword *lo_buf, pword *hi_buf, 1930 pword *var_buf, int count) 1931{ 1932 dident did; 1933 1934#if 0 1935 /* Check whether the coefficient vectors are identical. */ 1936 /* XXX - Turning this on breaks some things for some reason. */ 1937 if (count > 0 && !memcmp(con->lo_vec, con->hi_vec, 1938 count * sizeof(double))) { 1939 /* 1940 ** Make hi_buf/hi_vec the same as lo_buf/lo_vec. Note that we 1941 ** can't reset the stack to pop hi_buf, since other things may 1942 ** have been added since; however, the buffer will be garbage 1943 ** collected, since nothing refers to it. 1944 */ 1945 hi_buf = lo_buf; 1946 con->hi_vec = con->lo_vec; 1947 } 1948#endif 1949 1950 if (count < con->term_count) { 1951#ifdef IC_DEBUG 1952 printf("term count: %d -> %d.\n", con->term_count, count); 1953#endif 1954 /* 1955 ** We didn't get as many terms as expected, presumably because 1956 ** something became ground due to bound rounding for an integer 1957 ** var. Pad things to match. 1958 */ 1959 if (count > 0) { 1960 int n; 1961 pword *gap_start, *gap_end; 1962 1963 did = ec_did("[]", count); 1964 var_buf->val.did = did; 1965 n = con->term_count - count; 1966 Pad(lo_buf - n, n); 1967 gap_end = lo_buf + BufferPwords(lo_buf); 1968 Set_Buffer_Size(lo_buf, count * sizeof(double)); 1969 gap_start = lo_buf + BufferPwords(lo_buf); 1970 Pad(gap_start, gap_end-gap_start); 1971 if (hi_buf != lo_buf) { 1972 gap_end = hi_buf + BufferPwords(hi_buf); 1973 Set_Buffer_Size(hi_buf, count * sizeof(double)); 1974 gap_start = hi_buf + BufferPwords(hi_buf); 1975 Pad(gap_start, gap_end-gap_start); 1976 } 1977 } else { 1978 /* XXX - do we want to arrange that this cannot occur? */ 1979 /* Or rather, have some short-cut code to call. */ 1980 /* 1981 ** Note that we clobber the allocated var struct to make 1982 ** sure the contents are not interpreted by the garbage 1983 ** collector; there is no need to do this for the coef 1984 ** buffers since their contents are not interpreted anyway. 1985 */ 1986 Pad(var_buf, con->term_count + 1); 1987#ifdef IC_DEBUG 1988 var_buf = 0; 1989 lo_buf = 0; 1990 hi_buf = 0; 1991 con->var_vec = 0; 1992 con->lo_vec = 0; 1993 con->hi_vec = 0; 1994#endif 1995 } 1996 1997 con->term_count = count; 1998 } 1999 2000 /* Create and fill in the constraint data buffer. */ 2001 Allocate_Con_Data_Buf(con); 2002 Set_Con_Data_Buf(con); 2003 2004 /* 2005 ** Fill in the constraint struct. 2006 ** Pretend all the buffer structures are strings since we don't have 2007 ** any better tag to use. 2008 */ 2009 con->con[CON_OFF_DATA].val.ptr = con->data; 2010 con->con[CON_OFF_DATA].tag.kernel = TSTRG; 2011 if (count > 0) { 2012 con->con[CON_OFF_LO_VEC].val.ptr = lo_buf; 2013 con->con[CON_OFF_LO_VEC].tag.kernel = TSTRG; 2014 con->con[CON_OFF_HI_VEC].val.ptr = hi_buf; 2015 con->con[CON_OFF_HI_VEC].tag.kernel = TSTRG; 2016 Make_Struct(con->con + CON_OFF_VAR_VEC, var_buf); 2017 } else { 2018 Make_Nil(con->con + CON_OFF_LO_VEC); 2019 Make_Nil(con->con + CON_OFF_HI_VEC); 2020 Make_Nil(con->con + CON_OFF_VAR_VEC); 2021 /* XXX - For reproducible bugs... :) Should remove later. */ 2022 con->con[CON_OFF_LO_VEC].val.ptr = 0; 2023 con->con[CON_OFF_HI_VEC].val.ptr = 0; 2024 con->con[CON_OFF_VAR_VEC].val.ptr = 0; 2025 } 2026} 2027 2028 /* 2029 ** The constraint entry at position idx is ground, and should be swapped 2030 ** with one at the end of the constraint. 2031 */ 2032void 2033swap_entries(int idx, con_info *con, bounds *a) 2034{ 2035 bounds b; 2036 typed_bounds ytb; 2037 pword *tmp; 2038 2039 while (--con->term_count > idx) { 2040 /* Scan backwards to find a variable to swap with. */ 2041 tmp = con->var_vec + con->term_count; 2042 Dereference(tmp); 2043 if (IsRef(tmp->tag)) { 2044 break; 2045 } 2046 Constant_To_Typed_Bounds(tmp->val, tmp->tag, ytb); 2047 if ((con->flags & CON_INTEGRALITY_PROP) && !ytb.i) { 2048 /* No integrality to propagate. */ 2049 con->flags &= ~CON_INTEGRALITY_PROP; 2050 } 2051 b.l = con->lo_vec[con->term_count]; 2052 b.u = con->hi_vec[con->term_count]; 2053 Mul(b, ytb.b, ytb.b); 2054 Sub(con->c, ytb.b, con->c); 2055 } 2056 2057 if (con->term_count > idx) { 2058 pword v; 2059 double d; 2060 int tc = con->term_count; 2061 /* 2062 ** Note that we have to use the raw (not dereferenced) values 2063 ** when swapping variables since we're not restoring on 2064 ** backtracking. 2065 */ 2066 v = con->var_vec[idx]; 2067 con->var_vec[idx] = con->var_vec[tc]; 2068 con->var_vec[tc] = v; 2069 2070 d = con->lo_vec[tc]; 2071 con->lo_vec[tc] = a->l; 2072 a->l = con->lo_vec[idx] = d; 2073 if (con->lo_vec != con->hi_vec) { 2074 d = con->hi_vec[tc]; 2075 con->hi_vec[tc] = a->u; 2076 a->u = con->hi_vec[idx] = d; 2077 } 2078 } 2079} 2080 2081 2082 2083/*---------------------------------------------------------------------- 2084** 2085** Functions for helping propagate/evaluate a linear constraint. 2086** 2087*/ 2088 2089 /* 2090 ** Updates E/F based on the term a * x. 2091 */ 2092void 2093update_ef(prop_info *prop, con_info *con, bounds *a, bounds *x, int idx) 2094{ 2095 bounds res; 2096 2097#ifdef IC_DEBUG 2098 fprintf(stderr, " al = %f, au = %f.\n", a->l, a->u); 2099 fprintf(stderr, " xl = %f, xu = %f.\n", x->l, x->u); 2100#endif 2101 2102 Mul(*a, *x, res); 2103 2104 if (res.l == -HUGE_VAL) { 2105 /* 2106 ** If F is being used for entailment, no entailment 2107 ** possible. If F is being used for propagation and we've 2108 ** already seen an infinite bound, no propagation is 2109 ** possible. 2110 */ 2111 if (OpIsGreater(con->op) || prop->inf_f_idx >= 0) { 2112#if 0 2113 /* Little hack for 1-var constraints. */ 2114 if (prop->inf_f_idx < MAX_S_WORD) { 2115 res.l = min(0.0, res.u); 2116 } 2117#endif 2118 2119 prop->inf_f_idx = MAX_S_WORD; 2120#ifdef IC_DEBUG 2121 fprintf(stderr, " inf_f_idx = %d.\n", prop->inf_f_idx); 2122#endif 2123 2124 if (prop->inf_e_idx >= con->term_count) { 2125 /* 2126 ** No E-based bound updates / (dis)entailment 2127 ** possible either. Don't worry about eliminating 2128 ** any remaining ground terms, which is the only 2129 ** useful work we could do by continuing. 2130 */ 2131#ifdef IC_DEBUG 2132 fprintf(stderr, " No propagation can occur.\n"); 2133#endif 2134 prop->no_prop = 1; 2135 return; 2136 } 2137 } else { 2138 prop->inf_f_idx = idx; 2139 prop->inf_f_bound = res.u; 2140 res.l = min(0.0, res.u); 2141#ifdef IC_DEBUG 2142 fprintf(stderr, " inf_f_idx = %d, inf_f_bound = %f.\n", 2143 prop->inf_f_idx, prop->inf_f_bound); 2144#endif 2145 } 2146 } 2147 2148 if (res.u == HUGE_VAL) { 2149 /* 2150 ** If E is being used for entailment, no entailment 2151 ** possible. If E is being used for propagation and we've 2152 ** already seen an infinite bound, no propagation is 2153 ** possible. 2154 */ 2155 if (OpIsLessEqual(con->op) || prop->inf_e_idx >= 0) { 2156#if 0 2157 /* Little hack for 1-var constraints. */ 2158 if (prop->inf_e_idx < MAX_S_WORD) { 2159 res.u = max(0.0, res.l); 2160 } 2161#endif 2162 2163 prop->inf_e_idx = MAX_S_WORD; 2164#ifdef IC_DEBUG 2165 fprintf(stderr, " inf_e_idx = %d.\n", prop->inf_e_idx); 2166#endif 2167 if (prop->inf_f_idx >= con->term_count) { 2168 /* 2169 ** No F-based bound updates / (dis)entailment 2170 ** possible either. Don't worry about eliminating 2171 ** any remaining ground terms, which is the only 2172 ** useful work we could do by continuing. 2173 */ 2174#ifdef IC_DEBUG 2175 fprintf(stderr, " No propagation can occur.\n"); 2176#endif 2177 prop->no_prop = 1; 2178 return; 2179 } 2180 } else { 2181 prop->inf_e_idx = idx; 2182 prop->inf_e_bound = res.l; /* XXX might have been mod by inf_f */ 2183 res.u = max(0.0, res.l); 2184#ifdef IC_DEBUG 2185 fprintf(stderr, " inf_e_idx = %d, inf_e_bound = %f.\n", 2186 prop->inf_e_idx, prop->inf_e_bound); 2187#endif 2188 } 2189 } 2190 2191 Sub(prop->sum, res, prop->sum); 2192 2193#ifdef IC_DEBUG 2194 fprintf(stderr, " term lo = %f, hi = %f.\n", res.l, res.u); 2195 fprintf(stderr, " neg_e = %f, f = %f.\n", prop->sum.l, prop->sum.u); 2196#endif 2197} 2198 2199 2200 /* 2201 ** Check whether a linear constraint (con) is entailed or disentailed, 2202 ** and if so, unify the boolean from the constraint with the appropriate 2203 ** value and kill the suspension. 2204 */ 2205int 2206evaluate_reified(con_info *con, prop_info *prop, int *solved) 2207{ 2208 int result, inequality; 2209 2210 /* Adjust for any infinities left out of sums. */ 2211 if (prop->inf_f_idx >= 0) { 2212 prop->sum.u = HUGE_VAL; 2213 } 2214 if (prop->inf_e_idx >= 0) { 2215 prop->sum.l = -HUGE_VAL; 2216 } 2217 2218 /* Note that op is either = or =< */ 2219 inequality = OpIsLessEqual(con->op) || OpIsGreater(con->op); 2220 if (prop->sum.u < 0.0 || (!inequality && prop->sum.l > 0.0)) { 2221 /* 2222 ** F < 0, or it's an equation and E < 0 (-E > 0). 2223 ** Result: Constraint is disentailed (false). 2224 */ 2225 Unify_Boolean(con->bool, !OpIsUpperBound(con->op), result); 2226 Return_If_Not_Success(result); 2227 con->reified = 0; 2228 *solved = 1; 2229 Succeed 2230 } else if (prop->sum.l >= 0.0 && (inequality || prop->sum.u <= 0.0)) { 2231 /* 2232 ** E <= 0 (-E >= 0), and if it's an equation F <= 0 (actually, 2233 ** E = F = 0 in this case). 2234 ** Result: Constraint is entailed (true). 2235 */ 2236 Unify_Boolean(con->bool, !!OpIsUpperBound(con->op), result); 2237 Return_If_Not_Success(result); 2238 con->reified = 0; 2239 *solved = 1; 2240 Succeed 2241 } /* else unknown status */ 2242 2243 *solved = 0; 2244 Succeed 2245} 2246 2247 2248 /* 2249 ** Determine the status of a 0-variable constraint. 2250 */ 2251int 2252check_ic_0v_con(con_info *con) 2253{ 2254 switch (con->op) { 2255 case UPPER_BOUND + LOWER_BOUND: 2256 /* Equation. */ 2257 if (0.0 <= con->c.l && 0.0 >= con->c.u) { 2258 /* Entailed. */ 2259 Mark_Constraint_Entailed(con) 2260 Succeed 2261 } else if (0.0 > con->c.u || 0.0 < con->c.l) { 2262 /* Failure. */ 2263 Fail 2264 } 2265 break; 2266 2267 case UPPER_BOUND: 2268 /* Less than or equal constraint. */ 2269 if (0.0 <= con->c.l) { 2270 /* Entailed. */ 2271 Mark_Constraint_Entailed(con) 2272 Succeed 2273 } else if (0.0 > con->c.u) { 2274 /* Failure. */ 2275 Fail 2276 } 2277 break; 2278 2279 case LOWER_BOUND: 2280 /* Greater than constraint. */ 2281 if (0.0 > con->c.u) { 2282 /* Entailed. */ 2283 Mark_Constraint_Entailed(con) 2284 Succeed 2285 } else if (0.0 <= con->c.l) { 2286 /* Failure. */ 2287 Fail 2288 } 2289 break; 2290 2291 default: 2292 Bip_Error(EC_EXTERNAL_ERROR); 2293 } 2294 2295 Update_Con_Data_Buf_If_Needed(con); 2296 2297 Succeed 2298} 2299 2300 2301 /* 2302 ** Propagate a constraint with only 1 variable. 2303 */ 2304int 2305prop_ic_1v_con(con_info *con, prop_info *prop) 2306{ 2307 int result, solved; 2308 pword *tmp; 2309 bounds a, res; 2310 var_info vi; 2311 2312#ifdef IC_DEBUG 2313 fprintf(stderr, "Entering prop_ic_1v_con.\n"); 2314#endif 2315 2316#ifdef IC_DEBUG 2317 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 2318 con->flags, con->term_count, con->c.l, con->c.u); 2319 fprintf(stderr, " reified = %d, op = %x.\n", con->reified, con->op); 2320#endif 2321 2322 a.l = con->lo_vec[0]; 2323 a.u = con->hi_vec[0]; 2324 2325#ifdef IC_DEBUG 2326 fprintf(stderr, " al = %f, au = %f.\n", a.l, a.u); 2327#endif 2328 2329 tmp = con->var_vec; 2330 Dereference(tmp); 2331 2332 if (IsRef(tmp->tag)) { 2333 get_var_info(tmp, &vi); 2334 vi.prop_int = con->flags & CON_INTEGRALITY_PROP; 2335 2336#ifdef IC_DEBUG 2337 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", vi.tb.b.l, vi.tb.b.u, 2338 vi.tb.i); 2339#endif 2340 2341 if (OpIsEqual(con->op)) { 2342 result = solve_equal(&a, &vi, &con->c, &solved); 2343 Return_If_Not_Success(result); 2344 if (solved) { 2345 Mark_Constraint_Entailed(con); 2346 Succeed 2347 } 2348 } else { 2349 result = impose_coef_bounds(con->op, OpIsGreater(con->op), 2350 &a, &vi, &con->c); 2351 Return_If_Not_Success(result); 2352 2353 Mul(a, vi.tb.b, res); 2354 2355 if (OpIsGreater(con->op) && res.u <= con->c.l) { 2356 Fail 2357 } 2358 if (OpIsLessEqual(con->op) ? res.u <= con->c.l : res.l > con->c.u) { 2359 Mark_Constraint_Entailed(con) 2360 Succeed 2361 } 2362 } 2363 } else { 2364 con->term_count = 0; 2365 2366 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 2367 2368#ifdef IC_DEBUG 2369 fprintf(stderr, " Ground x: xl = %f, xu = %f, xi = %d.\n", 2370 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 2371#endif 2372 2373 Mul(a, vi.tb.b, res); 2374 Sub(con->c, res, con->c); 2375 2376 if (OpIsEqual(con->op)) { 2377 if (con->c.l > 0.0 || con->c.u < 0.0) { 2378 Fail 2379 } 2380 if (con->c.l == 0.0 && con->c.u == 0.0) { 2381 Mark_Constraint_Entailed(con) 2382 Succeed 2383 } 2384 } else if (OpIsLessEqual(con->op)) { 2385 if (con->c.u < 0.0) { 2386 Fail 2387 } 2388 if (con->c.l >= 0.0) { 2389 Mark_Constraint_Entailed(con) 2390 Succeed 2391 } 2392 } else { 2393 if (con->c.l >= 0.0) { 2394 Fail 2395 } 2396 if (con->c.u < 0.0) { 2397 Mark_Constraint_Entailed(con) 2398 Succeed 2399 } 2400 } 2401 } 2402 2403 Update_Con_Data_Buf_If_Needed(con); 2404 2405 Succeed 2406} 2407 2408 2409 /* 2410 ** Do the first pass of the two-pass propagation algorithm. 2411 */ 2412int 2413prop_pass_1(con_info *con, prop_info *prop) 2414{ 2415 var_info vi; 2416 bounds a, res; 2417 pword *tmp; 2418 int idx, result; 2419 2420#ifdef IC_DEBUG 2421 fprintf(stderr, "Entering prop_pass_1.\n"); 2422#endif 2423 2424 if (OpIsNotEqual(con->op) && !con->reified) { 2425 Bip_Error(EC_EXTERNAL_ERROR); 2426 } 2427 2428#ifdef IC_DEBUG 2429 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 2430 con->flags, con->term_count, con->c.l, con->c.u); 2431 fprintf(stderr, " op = %x, reified = %d.\n", 2432 con->op, con->reified); 2433#endif 2434 2435 Init_Prop_Info(prop); 2436 2437#ifdef IC_DEBUG 2438 fprintf(stderr, " Commencing e/f computation.\n"); 2439#endif 2440 2441 for (idx = 0; idx < con->term_count; idx++) { 2442 a.l = con->lo_vec[idx]; 2443 a.u = con->hi_vec[idx]; 2444 tmp = con->var_vec + idx; 2445 Dereference(tmp); 2446 2447#ifdef IC_DEBUG 2448 fprintf(stderr, " Term %d.\n", idx); 2449#endif 2450 2451 if (!IsRef(tmp->tag)) { 2452 /* X is ground. */ 2453 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 2454 2455 if ((con->flags & CON_INTEGRALITY_PROP) && !vi.tb.i) { 2456 /* 2457 ** No integrality to propagate. 2458 ** Note that since at least one ground term has been 2459 ** eliminated, modifying the constraint, this change 2460 ** will be written to the constraint later with the 2461 ** other changes. 2462 */ 2463 con->flags &= ~CON_INTEGRALITY_PROP; 2464 } 2465 2466 /* Adjust RHS constant. */ 2467 Mul(a, vi.tb.b, res); 2468 Sub(con->c, res, con->c); 2469 2470 /* Swap X with a yet-to-be-processed variable. */ 2471 swap_entries(idx, con, &a); 2472 2473#ifdef IC_DEBUG 2474 fprintf(stderr, " Adjusted c: cl = %f, cu = %f.\n", con->c.l, con->c.u); 2475#endif 2476 2477 /* If we're at the end now (no more variables), stop. */ 2478 if (idx >= con->term_count) { 2479 break; 2480 } 2481 2482 /* We now have a variable at position idx. */ 2483 tmp = con->var_vec + idx; 2484 Dereference(tmp); 2485 } 2486 2487 get_var_info(tmp, &vi); 2488 2489 if (!vi.tb.i) { 2490 prop->num_non_int_vars++; 2491 prop->non_int_idx = idx; 2492 } 2493 2494 update_ef(prop, con, &a, &vi.tb.b, idx); 2495 if (prop->no_prop) { 2496 break; 2497 } 2498 } 2499 2500 /* Don't move this to the start of the loop! con->c changes... */ 2501 Add(prop->sum, con->c, prop->sum); 2502 2503#ifdef IC_DEBUG 2504 fprintf(stderr, " Final neg_e = %f, f = %f.\n", prop->sum.l, prop->sum.u); 2505#endif 2506 2507 /* 2508 ** Remaining code in this function does not apply to constraints 2509 ** which are still reified. 2510 */ 2511 if (con->reified) { 2512 Succeed 2513 } 2514 2515 if (con->flags & CON_INTEGRALITY_PROP) { 2516 if (prop->num_non_int_vars == 0) { 2517 /* 2518 ** Clearing the flag here isn't necessary, which is lucky 2519 ** since it will only be updated in the structure if the 2520 ** constraint has otherwise been modified. 2521 */ 2522 con->flags &= ~CON_INTEGRALITY_PROP; 2523 prop->non_int_idx = -1; /* Just to be safe. */ 2524 } else if (prop->num_non_int_vars == 1 && !con->reified) { 2525 a.l = con->lo_vec[prop->non_int_idx]; 2526 a.u = con->hi_vec[prop->non_int_idx]; 2527 if ((a.l == 1.0 && a.u == 1.0) || (a.l == -1.0 && a.u == -1.0)) { 2528 tmp = con->var_vec + prop->non_int_idx; 2529 Dereference(tmp); 2530 get_var_info(tmp, &vi); 2531 result = set_integral(&vi); 2532 Return_If_Not_Success(result); 2533 /* Integrality propagation now completely dealt with. */ 2534 con->flags &= ~CON_INTEGRALITY_PROP; 2535 prop->num_non_int_vars = 0; 2536 prop->non_int_idx = -1; 2537 } 2538 } else { 2539 prop->non_int_idx = -1; 2540 } 2541 } else { 2542 prop->non_int_idx = -1; 2543 } 2544 /* 2545 ** Now non_int_idx >= 0 iff we're supposed to be propagating 2546 ** integrality to that variable if we ground it to an integral 2547 ** value. 2548 */ 2549 2550 Succeed 2551} 2552 2553 2554 /* 2555 ** Propagate a linear constraint (ic_con). 2556 ** We assume bool is a ground integer. 2557 */ 2558int 2559prop_pass_2(con_info *con, prop_info *prop) 2560{ 2561 pword *tmp; 2562 var_info vi; 2563 bounds a, res; 2564 int pseudo_op, idx, result, solved; 2565 2566#ifdef IC_DEBUG 2567 fprintf(stderr, "Entering prop_pass_2.\n"); 2568#endif 2569 2570 /* 2571 ** XXX - Do we want to check for short (1 & 2 var) constraints here? 2572 ** Probably not --- by this point just as efficient to use general 2573 ** algorithm, right? 2574 ** Either way, we must check for term_count == 1 && non_int_idx == 0. 2575 */ 2576 if (con->term_count == 1 && OpIsEqual(con->op)) { 2577 a.l = con->lo_vec[0]; 2578 a.u = con->hi_vec[0]; 2579 2580 tmp = con->var_vec; 2581 Dereference(tmp); 2582 get_var_info(tmp, &vi); 2583 vi.prop_int = (prop->non_int_idx == 0); 2584 2585 result = solve_equal(&a, &vi, &con->c, &solved); 2586 Return_If_Not_Success(result); 2587 if (solved) { 2588 Mark_Constraint_Entailed(con); 2589 } else { 2590 Update_Con_Data_Buf_If_Needed(con); 2591 } 2592 2593 Succeed 2594 } 2595 2596 /* Short-cuts and special processing for infinities. */ 2597 2598#if 0 2599 no_f_bounds = OpIsGreater(op) || inf_f_idx >= term_count; 2600 /* XXX - can't just do this --- stuffs up entailment checking? */ 2601 if (no_f_bounds) f = neg_e; 2602 no_e_bounds = OpIsLessEqual(op) || inf_e_idx >= term_count; 2603 /* XXX - can't just do this --- stuffs up entailment checking? */ 2604 if (no_e_bounds) neg_e = f; 2605 2606 prop_bounds = LOWER_BOUND * !no_e_bounds + UPPER_BOUND * !no_f_bounds; 2607#endif 2608 2609 pseudo_op = con->op; 2610 if (prop->inf_f_idx >= con->term_count) { 2611 pseudo_op &= ~UPPER_BOUND; 2612 /* f = neg_e; */ 2613 } 2614 if (prop->inf_e_idx >= con->term_count) { 2615 pseudo_op &= ~LOWER_BOUND; 2616 /* neg_e = f; */ 2617 } 2618 2619#ifdef IC_DEBUG 2620 fprintf(stderr, " pseudo_op = %d.\n", pseudo_op); 2621#endif 2622 2623 /* 2624 ** XXX - update to handle single infinities as described in 2625 ** ic_design.html. 2626 */ 2627 2628 if (OpIsUpperBound(pseudo_op) && prop->inf_f_idx >= 0) { 2629 /* Upper bound update. */ 2630 /* a * x =< f */ 2631#if 0 2632 if (inf_f_bound <= f) { 2633 /* Bound already tight enough. */ 2634 } else 2635#endif 2636 { 2637#ifdef IC_DEBUG 2638 fprintf(stderr, " Upper bound update with single infinity.\n"); 2639#endif 2640 2641 a.l = con->lo_vec[prop->inf_f_idx]; 2642 a.u = con->hi_vec[prop->inf_f_idx]; 2643 2644 tmp = con->var_vec + prop->inf_f_idx; 2645 Dereference(tmp); 2646 get_var_info(tmp, &vi); 2647 2648#ifdef IC_DEBUG 2649 fprintf(stderr, " Term %d.\n", prop->inf_f_idx); 2650 fprintf(stderr, " al = %f, au = %f.\n", a.l, a.u); 2651 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 2652 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 2653#endif 2654 2655 Mul(a, vi.tb.b, res); 2656 2657 /* 2658 ** Specialised infinity adjustment based on the fact that we 2659 ** already know res.l must be -inf. 2660 */ 2661 res.l = min(0.0, res.u); 2662 if (res.u == HUGE_VAL) { 2663 res.u = 0.0; 2664 } 2665 2666 Undo_Sub(prop->sum, res, res); 2667 2668#ifdef IC_DEBUG 2669 fprintf(stderr, " lo = %f, hi = %f.\n", res.l, res.u); 2670#endif 2671 2672 result = impose_coef_bounds(UPPER_BOUND, 0, &a, &vi, &res); 2673 Return_If_Not_Success(result); 2674 /* 2675 ** Note that the above cannot make X ground, even with 2676 ** integer rounding, because the other bound is still 2677 ** infinite. 2678 */ 2679 2680#ifdef IC_DEBUG 2681 fprintf(stderr, " new xl = %f, new xu = %f.\n", vi.tb.b.l, 2682 vi.tb.b.u); 2683#endif 2684 } 2685 pseudo_op &= ~UPPER_BOUND; 2686 } 2687 2688 if (OpIsLowerBound(pseudo_op) && prop->inf_e_idx >= 0) { 2689 /* Lower bound update. */ 2690 /* a * x >= neg_e */ 2691#if 0 2692 if (inf_e_bound > neg_e) { 2693 /* Bound already tight enough. */ 2694 } else 2695#endif 2696 { 2697#ifdef IC_DEBUG 2698 fprintf(stderr, " Lower bound update with single infinity.\n"); 2699#endif 2700 2701 a.l = con->lo_vec[prop->inf_e_idx]; 2702 a.u = con->hi_vec[prop->inf_e_idx]; 2703 2704 tmp = con->var_vec + prop->inf_e_idx; 2705 Dereference(tmp); 2706 get_var_info(tmp, &vi); 2707 2708#ifdef IC_DEBUG 2709 fprintf(stderr, " Term %d.\n", prop->inf_e_idx); 2710 fprintf(stderr, " al = %f, au = %f.\n", a.l, a.u); 2711 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 2712 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 2713#endif 2714 2715 Mul(a, vi.tb.b, res); 2716 2717 /* 2718 ** Specialised infinity adjustment based on the fact that we 2719 ** already know res.u must be +inf. 2720 */ 2721 res.u = max(0.0, res.l); 2722 if (res.l == -HUGE_VAL) { 2723 res.l = 0.0; 2724 } 2725 2726 Undo_Sub(prop->sum, res, res); 2727 2728#ifdef IC_DEBUG 2729 fprintf(stderr, " lo = %f, hi = %f.\n", res.l, res.u); 2730#endif 2731 2732 result = impose_coef_bounds(LOWER_BOUND, 2733 OpIsGreater(con->op), &a, &vi, &res); 2734 Return_If_Not_Success(result); 2735 /* 2736 ** Note that the above cannot make X ground, even with 2737 ** integer rounding, because the other bound is still 2738 ** infinite. 2739 */ 2740 2741#ifdef IC_DEBUG 2742 fprintf(stderr, " new xl = %f, new xu = %f.\n", vi.tb.b.l, 2743 vi.tb.b.u); 2744#endif 2745 } 2746 pseudo_op &= ~LOWER_BOUND; 2747 } 2748 2749 if (pseudo_op) { 2750 /* At least one bound requires the second pass. */ 2751 2752#ifdef IC_DEBUG 2753 fprintf(stderr, " Commencing general propagation.\n"); 2754#endif 2755 2756 for (idx = 0; idx < con->term_count; idx++) { 2757 a.l = con->lo_vec[idx]; 2758 a.u = con->hi_vec[idx]; 2759 2760 tmp = con->var_vec + idx; 2761 Dereference(tmp); 2762 get_var_info(tmp, &vi); 2763 /* Can't rely on index of non-int var remaining stable... :( */ 2764 vi.prop_int = (con->flags & CON_INTEGRALITY_PROP) && 2765 prop->num_non_int_vars == 1 && !vi.tb.i; 2766 2767#ifdef IC_DEBUG 2768 fprintf(stderr, " Term %d.\n", idx); 2769 fprintf(stderr, " al = %f, au = %f.\n", a.l, a.u); 2770 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 2771 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 2772#endif 2773 2774 Mul(a, vi.tb.b, res); 2775 2776 if (res.l == -HUGE_VAL) { 2777 res.l = min(0.0, res.u); 2778 } 2779 if (res.u == HUGE_VAL) { 2780 res.u = max(0.0, res.l); 2781 } 2782 2783 Undo_Sub(prop->sum, res, res); 2784 2785#ifdef IC_DEBUG 2786 fprintf(stderr, " lo = %f, hi = %f.\n", res.l, res.u); 2787#endif 2788 2789 result = impose_coef_bounds(pseudo_op, OpIsGreater(con->op), 2790 &a, &vi, &res); 2791 Return_If_Not_Success(result); 2792 2793#ifdef IC_DEBUG 2794 fprintf(stderr, " new xl = %f, new xu = %f.\n", vi.tb.b.l, 2795 vi.tb.b.u); 2796#endif 2797 2798 /* 2799 ** If X is integral, rounding might have caused it to become 2800 ** ground. Note that xl and xu contain the current bounds 2801 ** of X. 2802 */ 2803 if (vi.tb.b.l == vi.tb.b.u) { 2804 /* X is ground. */ 2805 /* Adjust RHS constant. */ 2806 Mul(a, vi.tb.b, res); 2807 Sub(con->c, res, con->c); 2808 2809 /* Swap X with a yet-to-be-processed variable. */ 2810 swap_entries(idx, con, &a); 2811 2812#ifdef USE_BOUND_SET_SHORTCUT 2813 /* Assume X is integral, so don't update flags. */ 2814#else 2815 if ((con->flags & CON_INTEGRALITY_PROP) && !vi.tb.i) { 2816 /* 2817 ** No integrality to propagate. 2818 ** Note that since at least one ground term has been 2819 ** eliminated, modifying the constraint, this change 2820 ** will be written to the constraint later with the 2821 ** other changes. 2822 */ 2823 con->flags &= ~CON_INTEGRALITY_PROP; 2824 } 2825#endif 2826 2827 /* 2828 ** We now have a variable at position idx. 2829 ** Update idx so that next iter does this position 2830 ** again. (Of course, idx may now be beyond term_count 2831 ** anyway.) 2832 */ 2833 idx--; 2834 } 2835 } 2836 } 2837 2838 /* 2839 ** Check for the constraint now being entailed... 2840 ** E.g. it's now a 0-var equation or perhaps a 1-var int inequality. 2841 ** What kinds of things can be entailed here that weren't detected 2842 ** earlier? Is it only 0-var equations or 0,1 var inequalities? 2843 ** Nope, with integer rounding an inequality with an arbitrary 2844 ** number of variables can become entailed. 2845 ** 2846 ** Actually, can only happen with integer rounding (otherwise a "set 2847 ** to bounds" short-cut would have been used) or with what was a 2848 ** 1-var equality (dealt with above?). 2849 ** 2850 ** Umm, 1-var inequalities are not caught earlier...? 2851 ** 2852 ** Easy to catch if we keep F,E up-to-date (useful for equation 2853 ** propagation). 2854 */ 2855 2856 /* Be lazy for now, and just catch 0-var constraints. */ 2857 if (con->term_count == 0) { 2858 if (OpIsLessEqual(con->op)) { 2859 if (0.0 <= con->c.l) { 2860 /* Entailed. */ 2861 Mark_Constraint_Entailed(con) 2862 Succeed 2863 } 2864 } else if (OpIsGreater(con->op)) { 2865 if (0.0 > con->c.u) { 2866 /* Entailed. */ 2867 Mark_Constraint_Entailed(con) 2868 Succeed 2869 } 2870 } else { 2871 /* op is equality */ 2872 if (con->c.u == 0.0 && con->c.l == 0.0) { 2873 /* Entailed. */ 2874 Mark_Constraint_Entailed(con) 2875 Succeed 2876 } 2877 } 2878 } 2879 2880 /* Check for constraints which can be turned into unifications. */ 2881 Check_Con_Is_Unification(con) 2882 2883 Update_Con_Data_Buf_If_Needed(con); 2884 2885 Succeed 2886} 2887 2888 2889 /* 2890 ** Propagate a linear disequation (ic_con). 2891 */ 2892int 2893prop_ic_neq_con(con_info *con) 2894{ 2895 pword *tmp; 2896 bounds a, res; 2897 var_info vi; 2898 int idx, result, solved; 2899 2900 /* 2901 ** If it's a two-variable constraint, guess that we're going to be 2902 ** able to solve it completely now and try to short-circuit its 2903 ** processing. 2904 */ 2905 if (con->term_count == 2) { 2906 bounds c; 2907 2908 tmp = con->var_vec; 2909 Dereference(tmp); 2910 2911 if (!IsRef(tmp->tag)) { 2912 /* First variable is ground. */ 2913 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 2914 a.l = con->lo_vec[0]; 2915 a.u = con->hi_vec[0]; 2916 2917 Mul(a, vi.tb.b, res); 2918 Sub(con->c, res, c); 2919 2920 tmp = con->var_vec + 1; 2921 Dereference(tmp); 2922 2923 a.l = con->lo_vec[1]; 2924 a.u = con->hi_vec[1]; 2925 2926 if (!IsRef(tmp->tag)) { 2927 /* Second variable is ground too. */ 2928 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 2929 2930 Mul(a, vi.tb.b, res); 2931 Sub(c, res, con->c); 2932 2933 if (con->c.l > 0.0 || con->c.u < 0.0) { 2934 /* Entailed. */ 2935 Mark_Constraint_Entailed(con) 2936 Succeed 2937 } 2938 if (con->c.l == 0.0 && con->c.u == 0.0) { 2939 Fail 2940 } 2941 /* 2942 ** If we get here, we guessed wrong, but the work we did 2943 ** was not wasted. 2944 */ 2945 con->term_count = 0; 2946 } else { 2947 /* Second variable is still a variable. */ 2948 get_var_info(tmp, &vi); 2949 2950 result = solve_not_equal(&a, &vi, &c, &solved); 2951 Return_If_Not_Success(result); 2952 if (solved) { 2953 Mark_Constraint_Entailed(con) 2954 Succeed 2955 } 2956 /* 2957 ** If we get here, we guessed wrong. XXX - Try to 2958 ** exploit the work we did? 2959 */ 2960 } 2961 } else { 2962 /* First variable is still a variable. */ 2963 get_var_info(tmp, &vi); 2964 2965 tmp = con->var_vec + 1; 2966 Dereference(tmp); 2967 2968 if (!IsRef(tmp->tag)) { 2969 /* Second variable is ground. */ 2970 typed_bounds tb; 2971 2972 Constant_To_Typed_Bounds(tmp->val, tmp->tag, tb); 2973 a.l = con->lo_vec[1]; 2974 a.u = con->hi_vec[1]; 2975 2976 Mul(a, tb.b, res); 2977 Sub(con->c, res, c); 2978 2979 a.l = con->lo_vec[0]; 2980 a.u = con->hi_vec[0]; 2981 2982 result = solve_not_equal(&a, &vi, &c, &solved); 2983 Return_If_Not_Success(result); 2984 if (solved) { 2985 Mark_Constraint_Entailed(con) 2986 Succeed 2987 } 2988 /* 2989 ** If we get here, we guessed wrong. XXX - Try to 2990 ** exploit the work we did? 2991 */ 2992 } else { 2993 /* Both variables are still variables: nothing to do. */ 2994 Succeed 2995 } 2996 } 2997 } 2998 2999 for (idx = 0; idx < con->term_count; idx++) { 3000 if (idx >= 2) break; 3001 3002 tmp = con->var_vec + idx; 3003 Dereference(tmp); 3004 3005 if (!IsRef(tmp->tag)) { 3006 /* X is ground. */ 3007 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 3008 a.l = con->lo_vec[idx]; 3009 a.u = con->hi_vec[idx]; 3010 3011 /* Adjust RHS constant. */ 3012 Mul(a, vi.tb.b, res); 3013 Sub(con->c, res, con->c); 3014 3015 /* Swap X with a yet-to-be-processed variable. */ 3016 swap_entries(idx, con, &a); 3017 } 3018 } 3019 3020 if (con->term_count == 0) { 3021 if (con->c.l > 0.0 || con->c.u < 0.0) { 3022 /* Entailed. */ 3023 Mark_Constraint_Entailed(con) 3024 Succeed 3025 } 3026 if (con->c.l == 0.0 && con->c.u == 0.0) { 3027 Fail 3028 } 3029 } else if (con->term_count == 1) { 3030 a.l = con->lo_vec[0]; 3031 a.u = con->hi_vec[0]; 3032 tmp = con->var_vec; 3033 Dereference(tmp); 3034 3035 get_var_info(tmp, &vi); 3036 3037 result = solve_not_equal(&a, &vi, &con->c, &solved); 3038 Return_If_Not_Success(result); 3039 if (solved) { 3040 Mark_Constraint_Entailed(con) 3041 Succeed 3042 } 3043 } 3044 3045 Update_Con_Data_Buf_If_Needed(con); 3046 3047 Succeed 3048} 3049 3050 3051#ifdef USE_BOUND_SET_SHORTCUT 3052int 3053set_vars_to_lwb_list(pword *plin, con_info *con, prop_info *prop) 3054{ 3055 pword *pterm, *tmp; 3056 int idx, result; 3057 typed_bounds a; 3058 bounds res, new_sum; 3059 3060 new_sum = con->c; 3061 3062 BeginIterateLinList(plin, pterm, idx, a, tmp) 3063 if (!IsRef(tmp->tag)) { 3064 /* Variable (X) is ground. */ 3065 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 3066 3067 /* Update sum. */ 3068 Mul(a.b, vi.tb.b, res); 3069 Sub(new_sum, res, new_sum); 3070 } else { 3071 /* Variable is still a variable, so set term to lower bound. */ 3072 get_var_info(tmp, &vi); 3073 if (a.tb.b.l >= 0.0) { 3074 which_var_bound = 0; /* lower */ 3075 bound_value = vi.tb.b.l; 3076 } else if (a.tb.b.u <= 0.0) { 3077 which_var_bound = 1; /* upper */ 3078 bound_value = vi.tb.b.u; 3079 } else { 3080 /* 3081 ** Coefficient spans zero. 3082 ** Try to determine which variable bound is the right 3083 ** one. 3084 */ 3085 ... 3086 } 3087 } 3088 3089 if (vi.tb.i) { 3090 pword bnd; 3091 result = ec_double_to_int_or_bignum(bound_value, &bnd); 3092 Return_If_Not_Success(result); 3093 result = Unify_Pw(tmp->val, tmp->tag, bnd.val, bnd.tag); 3094 Return_If_Not_Success(result); 3095 } else { 3096 pword *bnd; 3097 bnd = var->attr + (which_var_bound ? OFF_HI : OFF_LO); 3098 result = Unify_Pw(tmp->val, tmp->tag, bnd->val, bnd->tag); 3099 Return_If_Not_Success(result); 3100 } 3101 3102 res.l = bound_value; 3103 res.u = bound_value; 3104 Mul(a.b, res, res); 3105 Sub(new_sum, res, new_sum); 3106 EndIterateLinList(plin) 3107 3108 /* Check entailment... */ 3109 ... 3110 3111 Succeed 3112} 3113#endif 3114 3115/* XXX - prop integrality when last non-int var and have unit coef. */ 3116int 3117short_cuts(con_info *con, prop_info *prop, int *short_cut) 3118{ 3119 *short_cut = SHORT_ERROR; 3120 3121 /* Check to see whether we can short-cut the default processing. */ 3122 /* See ic_design.html for more explanation of the logic here. */ 3123 3124 /* Short-cuts based on F and E (if not infinite). */ 3125 if (prop->inf_f_idx < 0) { 3126 if (prop->sum.u < 0.0) { 3127 /* 3128 ** We have failure (= or =<) or entailment (> or \=). 3129 */ 3130 if (OpIsUpperBound(con->op)) { 3131 Fail 3132 } 3133 *short_cut = SHORT_ENTAILED; 3134 Succeed 3135 } 3136 if (prop->sum.u == 0.0) { 3137 if (prop->inf_e_idx < 0 && prop->sum.l == 0.0) { 3138 /* Ground constraint with LHS == RHS. */ 3139 if (OpIsUpperBound(con->op)) { 3140 *short_cut = SHORT_ENTAILED; 3141 Succeed 3142 } else { 3143 Fail 3144 } 3145 } 3146#ifdef USE_BOUND_SET_SHORTCUT 3147 if (OpIsUpperBound(con->op)) { 3148 /* Set everything to lower bounds. */ 3149 *short_cut = SHORT_LWB; 3150 Succeed 3151 } 3152#endif 3153 } 3154 } 3155 3156 if (prop->inf_e_idx < 0) { 3157 if (prop->sum.l > 0.0) { 3158 /* 3159 ** We have failure (= or >) or entailment (=< or \=). 3160 */ 3161 if (OpIsLowerBound(con->op)) { 3162 Fail 3163 } 3164 *short_cut = SHORT_ENTAILED; 3165 Succeed 3166 } 3167 if (prop->sum.l == 0.0) { 3168#ifdef USE_BOUND_SET_SHORTCUT 3169 if (OpIsEqual(con->op)) { 3170 /* Set everything to upper bounds. */ 3171 *short_cut = SHORT_UPB; 3172 Succeed 3173 } 3174#endif 3175 if (OpIsLessEqual(con->op)) { 3176 /* Entailment. */ 3177 *short_cut = SHORT_ENTAILED; 3178 Succeed 3179 } 3180 if (OpIsGreater(con->op)) { 3181 Fail 3182 } 3183 /* No need to check \=, since already covered. */ 3184 } 3185 } 3186 3187 *short_cut = SHORT_NONE; 3188 Succeed 3189} 3190 3191 3192/* 3193** Updates an attribute with a new bitmap, updating bounds and waking lists, 3194** etc. if indicated by result (Result_Is_Slack(), etc.). 3195*/ 3196int 3197sync_attr_with_new_bitmap(var_info *vi, void *bitmap, int result) 3198{ 3199 double lwb, upb; 3200 word min, max; 3201 value val; 3202 type tag; 3203 3204 if (Result_Is_Empty(result)) { 3205 /* New bitmap is empty, so no solution. */ 3206 Fail 3207 } 3208 if (!Result_Is_Change(result)) { 3209 /* No change - nothing to do. */ 3210 Succeed 3211 } 3212 if (Result_Is_Slack(result)) { 3213 /* Intersection resulted in bound change(s). */ 3214 bitmap_range(bitmap, &min, &max); 3215 if (min == max) { 3216 /* Variable is now ground. */ 3217 val.nint = min; 3218 tag.kernel = TINT; 3219 return Unify_Pw(vi->var->val, vi->var->tag, val, tag); 3220 } 3221 lwb = (double) min; 3222 if (lwb > vi->tb.b.l) { 3223 /* Lower bound has changed. */ 3224 Make_Checked_Double_Val(val, lwb); 3225 tag.kernel = TDBL; 3226 ec_assign(vi->attr + OFF_LO, val, tag); 3227 vi->tb.b.l = lwb; 3228 result = ec_schedule_susps(vi->attr + OFF_WAKE_LO); 3229 Return_If_Not_Success(result) 3230 } 3231 upb = (double) max; 3232 if (upb < vi->tb.b.u) { 3233 /* Upper bound has changed. */ 3234 Make_Checked_Double_Val(val, upb); 3235 tag.kernel = TDBL; 3236 ec_assign(vi->attr + OFF_HI, val, tag); 3237 vi->tb.b.u = upb; 3238 result = ec_schedule_susps(vi->attr + OFF_WAKE_HI); 3239 Return_If_Not_Success(result) 3240 } 3241 } 3242 /* Update the attribute if the bitmap has moved. */ 3243 Update_Bitmap(vi, bitmap); 3244 /* Wake things suspended on new holes. */ 3245 /* XXX - maybe there are no new holes? */ 3246 result = ec_schedule_susps(vi->attr + OFF_WAKE_HOLE); 3247 Return_If_Not_Success(result) 3248 /* Notify constrained. */ 3249 return notify_constrained(vi->var); 3250} 3251 3252 3253/* 3254** Enforces initial consistency for ac_eq(X, Y, C). 3255*/ 3256int 3257p_ac_eq_init(value vx, type tx, value vy, type ty, value vc, type tc) 3258{ 3259 var_info vix, viy; 3260 word c; 3261 uword *bitmap_x, *bitmap_y; 3262 double lo, hi; 3263 int result; 3264 3265 Check_Integer(tc); 3266 Check_Ref(tx); 3267 Check_Ref(ty); 3268 3269 c = vc.nint; 3270 if (c < MIN_BITMAP_RANGE || c > MAX_BITMAP_RANGE) { 3271 Bip_Error(RANGE_ERROR) 3272 } 3273 3274 get_var_info(vx.ptr, &vix); 3275 get_var_info(vy.ptr, &viy); 3276 3277 /* Check that between them the variables have "reasonable" bounds. */ 3278 if (c < 0) { 3279 if (vix.tb.b.l < MIN_BITMAP_RANGE 3280 && viy.tb.b.l < MIN_BITMAP_RANGE - c) { 3281 /* Lower bounds too low. */ 3282 Bip_Error(RANGE_ERROR); 3283 } 3284 if (vix.tb.b.u > MAX_BITMAP_RANGE + c 3285 && viy.tb.b.u > MAX_BITMAP_RANGE) { 3286 /* Upper bounds too high. */ 3287 Bip_Error(RANGE_ERROR); 3288 } 3289 } else { 3290 if (vix.tb.b.l < MIN_BITMAP_RANGE + c 3291 && viy.tb.b.l < MIN_BITMAP_RANGE) { 3292 /* Lower bounds too low. */ 3293 Bip_Error(RANGE_ERROR); 3294 } 3295 if (vix.tb.b.u > MAX_BITMAP_RANGE 3296 && viy.tb.b.u > MAX_BITMAP_RANGE - c) { 3297 /* Upper bounds too high. */ 3298 Bip_Error(RANGE_ERROR); 3299 } 3300 } 3301 3302 /* Make sure both variables have bitmaps. */ 3303 if (IsAtom(vix.bitmap->tag)) { 3304 if (IsAtom(viy.bitmap->tag)) { 3305 /* 3306 ** Neither variable has a bitmap; impose bounds and create 3307 ** bitmaps. 3308 */ 3309 /* X */ 3310 lo = max(vix.tb.b.l, viy.tb.b.l + c); 3311 hi = min(vix.tb.b.u, viy.tb.b.u + c); 3312 result = ic_lwb(&vix, lo); 3313 Return_If_Not_Success(result) 3314 result = ic_upb(&vix, hi); 3315 Return_If_Not_Success(result) 3316 result = create_bitmap((word) lo, (word) hi, &bitmap_x); 3317 Return_If_Not_Success(result) 3318 Update_Bitmap(&vix, bitmap_x); 3319 /* Y */ 3320 lo = max(viy.tb.b.l, vix.tb.b.l - c); 3321 hi = min(viy.tb.b.u, vix.tb.b.u - c); 3322 result = ic_lwb(&viy, lo); 3323 Return_If_Not_Success(result) 3324 result = ic_upb(&viy, hi); 3325 Return_If_Not_Success(result) 3326 result = create_bitmap((word) lo, (word) hi, &bitmap_y); 3327 Return_If_Not_Success(result) 3328 Update_Bitmap(&viy, bitmap_y); 3329 } else { 3330 /* 3331 ** Y has a bitmap but X doesn't; impose bounds on Y (in case 3332 ** the bitmap causes them to be tightened), then impose 3333 ** bounds on X and copy Y's bitmap (actually, copy Y's 3334 ** bitmap and extract bounds for X). 3335 */ 3336 /* Y */ 3337 lo = max(viy.tb.b.l, vix.tb.b.l - c); 3338 hi = min(viy.tb.b.u, vix.tb.b.u - c); 3339 result = ic_lwb(&viy, lo); 3340 Return_If_Not_Success(result) 3341 result = ic_upb(&viy, hi); 3342 Return_If_Not_Success(result) 3343 /* X */ 3344 if (viy.tb.b.l == viy.tb.b.u) { 3345 /* Y is ground, so just ground X. */ 3346 Set_Var_To_Value(&vix, viy.tb.b.l + c); 3347 } else { 3348 copy_bitmap_shifted(viy.bitmap->val.wptr, c, &bitmap_x); 3349 result = sync_attr_with_new_bitmap(&vix, bitmap_x, 3350 RES_CHANGED | RES_SLACK); 3351 Return_If_Not_Success(result); 3352 } 3353 } 3354 } else { 3355 if (IsAtom(viy.bitmap->tag)) { 3356 /* 3357 ** X has a bitmap but Y doesn't; impose bounds on X (in case 3358 ** the bitmap causes them to be tightened), then impose 3359 ** bounds on Y and copy X's bitmap (actually, copy X's 3360 ** bitmap and extract bounds for Y). 3361 */ 3362 /* X */ 3363 lo = max(vix.tb.b.l, viy.tb.b.l + c); 3364 hi = min(vix.tb.b.u, viy.tb.b.u + c); 3365 result = ic_lwb(&vix, lo); 3366 Return_If_Not_Success(result) 3367 result = ic_upb(&vix, hi); 3368 Return_If_Not_Success(result) 3369 /* Y */ 3370 if (vix.tb.b.l == vix.tb.b.u) { 3371 /* X is ground, so just ground Y. */ 3372 Set_Var_To_Value(&viy, vix.tb.b.l - c); 3373 } else { 3374 copy_bitmap_shifted(vix.bitmap->val.wptr, -c, &bitmap_y); 3375 result = sync_attr_with_new_bitmap(&viy, bitmap_y, 3376 RES_CHANGED | RES_SLACK); 3377 Return_If_Not_Success(result); 3378 } 3379 } else { 3380 /* They both have bitmaps: intersect into each other. */ 3381 result = bitmap_shifted_intersect_into(vix.bitmap->val.wptr, 3382 viy.bitmap->val.wptr, c, &bitmap_x); 3383 result = sync_attr_with_new_bitmap(&vix, bitmap_x, result); 3384 Return_If_Not_Success(result); 3385 result = bitmap_shifted_intersect_into(viy.bitmap->val.wptr, 3386 bitmap_x, -c, &bitmap_y); 3387 result = sync_attr_with_new_bitmap(&viy, bitmap_y, result); 3388 Return_If_Not_Success(result); 3389 } 3390 } 3391 3392 Succeed 3393} 3394 3395 3396/* 3397** Propagates ac_eq(X, Y, C). 3398*/ 3399int 3400p_ac_eq_prop(value vx, type tx, value vy, type ty, value vc, type tc, 3401 value vsusp, type tsusp) 3402{ 3403 var_info vix, viy; 3404 word c; 3405 uword *bitmap_x, *bitmap_y; 3406 value val; 3407 type tag; 3408 int result; 3409 3410 c = vc.nint; 3411 3412 if (!IsRef(tx)) { 3413 val.nint = vx.nint - c; 3414 tag.kernel = TINT; 3415 result = Unify_Pw(vy, ty, val, tag); 3416 Return_If_Not_Success(result) 3417 Set_Susp_Dead(vsusp.ptr); 3418 Succeed 3419 } 3420 3421 if (!IsRef(ty)) { 3422 val.nint = vy.nint + c; 3423 tag.kernel = TINT; 3424 result = Unify_Pw(vx, tx, val, tag); 3425 Return_If_Not_Success(result) 3426 Set_Susp_Dead(vsusp.ptr); 3427 Succeed 3428 } 3429 3430 /* X and Y are both still variables. */ 3431 3432 get_var_info(vx.ptr, &vix); 3433 get_var_info(vy.ptr, &viy); 3434 3435 result = bitmap_shifted_intersect_into(vix.bitmap->val.wptr, 3436 viy.bitmap->val.wptr, c, &bitmap_x); 3437 result = sync_attr_with_new_bitmap(&vix, bitmap_x, result); 3438 Return_If_Not_Success(result); 3439 result = bitmap_shifted_intersect_into(viy.bitmap->val.wptr, 3440 bitmap_x, -c, &bitmap_y); 3441 result = sync_attr_with_new_bitmap(&viy, bitmap_y, result); 3442 Return_If_Not_Success(result); 3443 3444 Succeed 3445} 3446 3447 3448int 3449p_prop_ic_con(value vcon, type tcon) 3450{ 3451 con_info con; 3452 prop_info prop; 3453 int result, short_cut, solved; 3454 3455 Check_Structure(tcon); 3456 3457 con_struct_vec_to_con_info(vcon.ptr, &con); 3458 3459 if (OpIsNotEqual(con.op) && !con.reified) { 3460 /* Disequality constraint. */ 3461 return prop_ic_neq_con(&con); 3462 } 3463 3464 /* XXX - Should do first pass of propagation here, for use by all? */ 3465 /* XXX - Not for short constraints? */ 3466 result = prop_pass_1(&con, &prop); 3467 Return_If_Not_Success(result); 3468 3469#ifdef IC_DEBUG 3470 fprintf(stderr, "prop_pass_1 completed successfully.\n"); 3471#endif 3472 3473 /* Check for constraints which can be turned into unifications. */ 3474 Check_Con_Is_Unification(&con) 3475 3476 if (prop.no_prop) { 3477 Update_Con_Data_Buf_If_Needed(&con); 3478 Succeed 3479 } 3480 3481 if (con.reified) { 3482 /* No propagation, just check entailment/disentailment. */ 3483 result = evaluate_reified(&con, &prop, &solved); 3484 Return_If_Not_Success(result); 3485 if (solved) { 3486 Mark_Constraint_Entailed(&con) 3487 } else { 3488 Update_Con_Data_Buf_If_Needed(&con); 3489 } 3490 Succeed 3491 } 3492 3493 /* Check short-cuts. */ 3494 result = short_cuts(&con, &prop, &short_cut); 3495 Return_If_Not_Success(result); 3496 3497 switch(short_cut) { 3498 case SHORT_NONE: 3499 /* Continue execution. */ 3500 break; 3501#ifdef USE_BOUND_SET_SHORTCUT 3502 case SHORT_LWB: 3503 ... 3504 break; 3505 case SHORT_UPB: 3506 ... 3507 break; 3508#endif 3509 case SHORT_ENTAILED: 3510 /* Nothing more to do. */ 3511 Mark_Constraint_Entailed(&con); 3512 Succeed 3513 break; 3514 default: 3515 Bip_Error(EC_EXTERNAL_ERROR); 3516 break; 3517 } 3518 3519 /* 3520 ** Should switch on (say) term_count, but for now just call the 3521 ** general propagation routine. 3522 */ 3523 switch (con.term_count) { 3524 case 0: 3525 return check_ic_0v_con(&con); 3526 break; 3527 case 1: 3528 return prop_ic_1v_con(&con, &prop); 3529 break; 3530/* 3531 case 2: 3532 break; 3533*/ 3534 default: 3535 return prop_pass_2(&con, &prop); 3536 break; 3537 } 3538} 3539 3540 3541 3542/*---------------------------------------------------------------------- 3543** 3544** Functions for processing an ECLiPSe linear constraint. 3545** 3546*/ 3547 3548 3549 /* 3550 ** type_check_lin_terms 3551 ** Check a list of linear terms for type errors (expected to be 3552 ** called when we've detected failure, but want to make sure there 3553 ** aren't any errors we should report instead). 3554 */ 3555int 3556type_check_lin_terms(pword *plin, int flags) 3557{ 3558 pword *pterm, *tmp; 3559 int idx; 3560 typed_bounds a; 3561 3562 BeginIterateLinList(plin, pterm, idx, a, tmp) 3563 if ((flags & CON_INTEGRAL) && !a.i) { 3564 Bip_Error(TYPE_ERROR) 3565 } 3566 3567 if (!IsRef(tmp->tag)) { 3568 if (flags & CON_INTEGRAL) { 3569 Check_Integer_Or_Bignum(tmp->tag); 3570 } else { 3571 Check_Number(tmp->tag); 3572 } 3573 } 3574 EndIterateLinList(plin) 3575 3576 Succeed 3577} 3578 3579 3580 /* 3581 ** setup_pass_1 3582 ** Check a list of linear terms for type errors, and constrain the 3583 ** variables to be of the appropriate type, while also performing the 3584 ** first pass of the two-pass linear constraint propagation algorithm 3585 ** and counting the number of non-ground terms. :) 3586 */ 3587int 3588setup_pass_1(pword *plin, con_info *con, prop_info *prop) 3589{ 3590 pword *pterm, *tmp; 3591 int idx, maybe_prop_int; 3592 var_info vi; 3593 typed_bounds a; 3594 bounds res; 3595 int result; 3596 3597#ifdef IC_DEBUG 3598 fprintf(stderr, "Entering setup_pass_1.\n"); 3599#endif 3600 3601#ifdef IC_DEBUG 3602 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 3603 con->flags, con->term_count, con->c.l, con->c.u); 3604 fprintf(stderr, " op = %x, reified = %d.\n", 3605 con->op, con->reified); 3606#endif 3607 3608 Init_Prop_Info(prop); 3609 3610 /* 3611 ** We want to consider propagating integrality only if the 3612 ** constraint is a non-integer equation with reified boolean not 0. 3613 */ 3614 maybe_prop_int = (OpIsEqual(con->op) || 3615 (OpIsNotEqual(con->op) && con->reified)) 3616 && !(con->flags & CON_INTEGRAL); 3617 3618#ifdef IC_DEBUG 3619 fprintf(stderr, " maybe_prop_int = %d.\n", maybe_prop_int); 3620 fprintf(stderr, " Commencing scan and e/f computation.\n"); 3621#endif 3622 3623 BeginIterateLinList(plin, pterm, idx, a, tmp) 3624#ifdef IC_DEBUG 3625 fprintf(stderr, " Term %d.\n", idx); 3626#endif 3627 3628#ifdef IC_DEBUG 3629 fprintf(stderr, " al = %f, au = %f, ai = %d.\n", a.b.l, a.b.u, a.i); 3630#endif 3631 3632 if ((con->flags & CON_INTEGRAL) && !a.i) { 3633 Bip_Error(TYPE_ERROR) 3634 } 3635 maybe_prop_int &= a.i; 3636 3637 if (IsRef(tmp->tag)) { 3638#ifdef IC_DEBUG 3639 fprintf(stderr, " Initial constraining of var.\n"); 3640#endif 3641 /* 3642 ** Make sure it's an IC var, and constrain it to be integral 3643 ** if necessary. 3644 */ 3645 result = make_constrained_ic_var(&tmp, -HUGE_VAL, HUGE_VAL, con->flags & CON_INTEGRAL); 3646 Return_If_Not_Success(result) 3647 } 3648 3649 if (IsRef(tmp->tag)) { 3650 /* Variable is still a variable. */ 3651 con->term_count++; 3652 3653 /* Don't bother updating E/F if there's no point. */ 3654 if (!prop->no_prop) { 3655 get_var_info(tmp, &vi); 3656 3657#ifdef IC_DEBUG 3658 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 3659 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 3660#endif 3661 3662 if (!vi.tb.i) { 3663 prop->num_non_int_vars++; 3664 prop->non_int_idx = idx; 3665 } 3666 3667 update_ef(prop, con, &a.b, &vi.tb.b, idx); 3668 } 3669 } else { 3670 /* Variable is ground. */ 3671#if 1 3672 /* 3673 ** Don't count it as part of idx or infinity tracking won't 3674 ** work properly (an inf idx is assumed to be less than 3675 ** term_count). 3676 */ 3677 idx--; 3678#endif 3679 3680 if (con->flags & CON_INTEGRAL) { 3681 Check_Integer_Or_Bignum(tmp->tag); 3682 } else { 3683 Check_Number(tmp->tag); 3684 } 3685 3686 /* Don't bother updating E/F if there's no point. */ 3687 if (!prop->no_prop) { 3688 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 3689 3690#ifdef IC_DEBUG 3691 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 3692 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 3693 fprintf(stderr, " Adjusting e/f for ground term.\n"); 3694#endif 3695 3696 maybe_prop_int &= vi.tb.i; 3697 3698 Mul(a.b, vi.tb.b, res); 3699 Sub(prop->sum, res, prop->sum); 3700 3701#ifdef IC_DEBUG 3702 fprintf(stderr, " term lo = %f, hi = %f.\n", res.l, res.u); 3703 fprintf(stderr, " neg_e = %f, f = %f.\n", prop->sum.l, prop->sum.u); 3704#endif 3705 } 3706 } 3707 EndIterateLinList(plin) 3708 3709#ifdef IC_DEBUG 3710 fprintf(stderr, " Final neg_e = %f, f = %f.\n", prop->sum.l, prop->sum.u); 3711#endif 3712 3713 /* 3714 ** Don't bother trying to propagate integrality later if all the 3715 ** variables are already integral. 3716 */ 3717 if (maybe_prop_int && prop->num_non_int_vars >= 1) { 3718 con->flags |= CON_INTEGRALITY_PROP; 3719 3720#ifdef IC_DEBUG 3721 fprintf(stderr, " Adjusted flags = %d.\n", con->flags); 3722#endif 3723 } 3724 3725 Succeed 3726} 3727 3728 3729 /* 3730 ** process_lin_terms_to_vectors_and_prop 3731 ** Set up & fill in the coefficient and variable vectors, imposing the 3732 ** relevant propagation bounds in the process. Also set up the 3733 ** constraint data buffer. 3734 */ 3735int 3736process_lin_terms_to_vectors_and_prop(pword *plin, con_info *con, 3737 prop_info *prop) 3738{ 3739 pword *pterm, *tmp; 3740 pword goal; 3741 pword *lo_buf, *hi_buf, *var_buf; 3742 dident did; 3743 int count = 0; 3744 typed_bounds a; 3745 var_info vi; 3746 bounds res; 3747 int strict; 3748 int idx, result; 3749 int delayed = 0; 3750 int pseudo_op, pseudo_op0; 3751 int off_pos, off_neg; 3752 3753#ifdef IC_DEBUG 3754 fprintf(stderr, "Entering process_lin_terms_to_vectors_and_prop.\n"); 3755#endif 3756 3757#ifdef IC_DEBUG 3758 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 3759 con->flags, con->term_count, con->c.l, con->c.u); 3760 fprintf(stderr, " op = %x, reified = %d.\n", 3761 con->op, con->reified); 3762#endif 3763 3764 /* 3765 ** We allocate the variable vector first, so that if we discover the 3766 ** coefficient vectors are identical, we can easily throw one away. 3767 ** 3768 ** Note that we can't automatically assume the vectors are identical 3769 ** for integer constraints, since they may contain bignums not 3770 ** exactly representable as doubles. :( 3771 ** 3772 ** Don't change the order of these allocations without updating the 3773 ** rest of the code. 3774 */ 3775 3776 if (con->term_count > 0) { 3777 var_buf = TG; 3778 con->var_vec = VarVec(var_buf); 3779 did = ec_did("[]", con->term_count); 3780 Push_Struct_Frame(did); 3781 3782 lo_buf = TG; 3783 con->lo_vec = CoefVec(lo_buf); 3784 Push_Buffer(con->term_count * sizeof(double)); 3785 3786 hi_buf = TG; 3787 con->hi_vec = CoefVec(hi_buf); 3788 Push_Buffer(con->term_count * sizeof(double)); 3789 } else { 3790 /* XXX - do we want to arrange that this cannot occur? */ 3791 /* 3792 Make_Nil(TG); 3793 TG->val.ptr = 0; * For reproducible bugs... :) * 3794 var_vec = TG; 3795 lo_vec = TG; 3796 hi_vec = TG; 3797 TG++; 3798 */ 3799#ifdef IC_DEBUG 3800 var_buf = 0; 3801 lo_buf = 0; 3802 hi_buf = 0; 3803 con->var_vec = 0; 3804 con->lo_vec = 0; 3805 con->hi_vec = 0; 3806#endif 3807 } 3808 3809 /* Create the suspension. */ 3810 Make_Struct(&goal, TG); 3811 Push_Struct_Frame(d_prop_ic_con); 3812 goal.val.ptr[1].val.ptr = con->con; 3813 goal.val.ptr[1].tag.kernel = TCOMP; 3814 result = ec_make_suspension(goal, ConstraintPriority(con), 3815 proc_prop_ic_con, con->con + CON_OFF_SUSP); 3816 if (result == DEBUG_SUSP_EVENT) { 3817 delayed = 1; 3818 result = PSUCCEED; 3819 } 3820 Return_If_Not_Success(result); 3821 con->susp = con->con + CON_OFF_SUSP; 3822 Dereference(con->susp); 3823 3824 con->c.l = NEG_ZERO; 3825 con->c.u = 0.0; 3826 3827 /* 3828 ** Compute the default "pseudo" op; i.e. leaving out propagating 3829 ** bounds involving at least one infinity. 3830 */ 3831 pseudo_op0 = con->op; 3832 if (prop->inf_f_idx >= 0) { 3833 pseudo_op0 &= ~UPPER_BOUND; 3834 } 3835 if (prop->inf_e_idx >= 0) { 3836 pseudo_op0 &= ~LOWER_BOUND; 3837 } 3838 3839#ifdef IC_DEBUG 3840 fprintf(stderr, " pseudo_op0 = %d.\n", pseudo_op0); 3841#endif 3842 3843 if ((!(con->flags & CON_INTEGRALITY_PROP)) || prop->num_non_int_vars != 1) { 3844 prop->non_int_idx = -1; 3845 } 3846 3847 strict = OpIsGreater(con->op); 3848 3849 /* 3850 ** If it's an inequality, pre-compute which bounds to wake on for 3851 ** positive & negative coefficients. 3852 */ 3853 if (OpIsGreater(con->op)) { 3854 off_pos = OFF_WAKE_HI; 3855 off_neg = OFF_WAKE_LO; 3856 } else if (OpIsLessEqual(con->op)) { 3857 off_pos = OFF_WAKE_LO; 3858 off_neg = OFF_WAKE_HI; 3859 } 3860 3861#ifdef IC_DEBUG 3862 fprintf(stderr, " Commencing setup and propagation pass.\n"); 3863#endif 3864 3865 BeginIterateLinList(plin, pterm, idx, a, tmp) 3866#ifdef IC_DEBUG 3867 fprintf(stderr, " Term %d.\n", idx); 3868 fprintf(stderr, " al = %f, au = %f.\n", a.b.l, a.b.u); 3869#endif 3870 3871 if (!IsRef(tmp->tag)) { 3872 /* Variable (X) is ground. */ 3873#if 1 3874 /* 3875 ** Don't count it as part of idx or infinity tracking won't 3876 ** work properly (an inf idx is assumed to be less than 3877 ** term_count). 3878 */ 3879 idx--; 3880#endif 3881 3882 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 3883 3884#ifdef IC_DEBUG 3885 fprintf(stderr, " xl = %f, xu = %f, xi = %d (ground).\n", 3886 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 3887#endif 3888 3889 /* Subtract A * X from RHS. */ 3890 Mul(a.b, vi.tb.b, res); 3891 Sub(con->c, res, con->c); 3892 3893#ifdef IC_DEBUG 3894 fprintf(stderr, " Adjusted c: cl = %f, cu = %f.\n", con->c.l, con->c.u); 3895#endif 3896 } else { 3897 /* Variable is still a variable, so propagate, and put */ 3898 /* term in vector. */ 3899 get_var_info(tmp, &vi); 3900 3901#ifdef IC_DEBUG 3902 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", 3903 vi.tb.b.l, vi.tb.b.u, vi.tb.i); 3904#endif 3905 3906 if (con->reified) { 3907 /* 3908 ** Reified constraint. 3909 ** Wake on either bound change. 3910 */ 3911 result = ec_enter_suspension(vi.attr + OFF_WAKE_LO, 3912 con->susp->val.ptr); 3913 Return_If_Not_Success(result) 3914 result = ec_enter_suspension(vi.attr + OFF_WAKE_HI, 3915 con->susp->val.ptr); 3916 Return_If_Not_Success(result) 3917 3918 Make_Ref(con->var_vec + count, tmp); 3919 con->lo_vec[count] = a.b.l; 3920 con->hi_vec[count] = a.b.u; 3921 count++; 3922 } else { 3923 switch(con->op) { 3924 case LOWER_BOUND: 3925 case UPPER_BOUND: 3926 /* 3927 ** We have a (non-reified) inequality. 3928 ** Wake on appropriate bound only. 3929 */ 3930 if (a.b.l > 0.0) { 3931 result = ec_enter_suspension(vi.attr + off_pos, 3932 con->susp->val.ptr); 3933 Return_If_Not_Success(result) 3934 break; 3935 } else if (a.b.u < 0.0) { 3936 result = ec_enter_suspension(vi.attr + off_neg, 3937 con->susp->val.ptr); 3938 Return_If_Not_Success(result) 3939 break; 3940 } 3941 /* Coefficient spans zero: wake on either bound. */ 3942 3943 /* === Fall through to equation case === */ 3944 3945 case LOWER_BOUND + UPPER_BOUND: 3946 /* 3947 ** We have an equation. 3948 ** Wake on either bound change. 3949 */ 3950 result = ec_enter_suspension(vi.attr + OFF_WAKE_LO, 3951 con->susp->val.ptr); 3952 Return_If_Not_Success(result) 3953 result = ec_enter_suspension(vi.attr + OFF_WAKE_HI, 3954 con->susp->val.ptr); 3955 Return_If_Not_Success(result) 3956 break; 3957 3958 case 0: 3959 /* 3960 ** We have a (non-reified) disequality. 3961 ** Wake on instantiation only. 3962 */ 3963 result = insert_suspension(vi.var, 1, 3964 con->susp->val.ptr, suspend_slot); 3965 Return_If_Not_Success(result) 3966 break; 3967 3968 default: 3969 Bip_Error(EC_EXTERNAL_ERROR); 3970 } 3971 3972 /* 3973 ** If we might want to make this variable integral, mark 3974 ** it so. 3975 */ 3976 vi.prop_int = (idx == prop->non_int_idx); 3977 3978 if (!prop->no_prop) { 3979 Mul(a.b, vi.tb.b, res); 3980 3981 /* Adjust any infinite bounds. */ 3982 /* 3983 ** XXX - should go in macro to make sure done 3984 ** exactly the same way everywhere. 3985 ** XXX - except then can't interleave the pseudo_op 3986 ** stuff. :) 3987 */ 3988 pseudo_op = pseudo_op0; 3989 if (res.l == -HUGE_VAL) { 3990 res.l = min(0.0, res.u); 3991 /* If appropriate, propagate the bound for this term. */ 3992 if (idx == prop->inf_f_idx) { 3993 pseudo_op |= (con->op & UPPER_BOUND); 3994 } 3995 } 3996 if (res.u == HUGE_VAL) { 3997 res.u = max(0.0, res.l); 3998 /* If appropriate, propagate the bound for this term. */ 3999 if (idx == prop->inf_e_idx) { 4000 pseudo_op |= (con->op & LOWER_BOUND); 4001 } 4002 } 4003 4004 /* Don't do any more work if there's nothing to do. */ 4005 /* (Besides, impose_coef_bounds requires op != 0.) */ 4006 if (pseudo_op) { 4007 Undo_Sub(prop->sum, res, res); 4008 4009#ifdef IC_DEBUG 4010 fprintf(stderr, " lo = %f, hi = %f.\n", res.l, res.u); 4011#endif 4012 4013 result = impose_coef_bounds(pseudo_op, strict, 4014 &a.b, &vi, &res); 4015 Return_If_Not_Success(result); 4016 } 4017 } 4018 4019 /* 4020 ** If we might want to propagate integrality to this 4021 ** variable, and it has a unit coefficient, then 4022 ** constrain it to be integral. Note that we can't do 4023 ** this before imposing the bounds above, since the 4024 ** integrality may alter the variable's bounds, which 4025 ** would mess up the propagation algorithm. 4026 */ 4027 if (vi.prop_int && (a.b.l == -1.0 || a.b.l == 1.0)) { 4028#ifdef IC_DEBUG 4029 fprintf(stderr, " Propagating integrality.\n"); 4030#endif 4031 result = set_integral(&vi); 4032 Return_If_Not_Success(result); 4033 con->flags -= CON_INTEGRALITY_PROP; 4034 } 4035 4036#ifdef IC_DEBUG 4037 fprintf(stderr, " new xl = %f, new xu = %f.\n", 4038 vi.tb.b.l, vi.tb.b.u); 4039#endif 4040 4041 /* 4042 ** Propagation and/or integer rounding may have caused X 4043 ** to become ground... 4044 */ 4045 if (vi.tb.b.l == vi.tb.b.u) { 4046 /* X is ground. */ 4047#ifdef USE_BOUND_SET_SHORTCUT 4048 /* Assume X is integral, so don't update flags. */ 4049#else 4050 if ((con->flags & CON_INTEGRALITY_PROP) && !vi.tb.i) { 4051 /* No integrality to propagate. */ 4052 con->flags &= ~CON_INTEGRALITY_PROP; 4053 } 4054#endif 4055 4056 /* Adjust RHS constant. */ 4057 Mul(a.b, vi.tb.b, res); 4058 Sub(con->c, res, con->c); 4059 } else { 4060 Make_Ref(con->var_vec + count, tmp); 4061 con->lo_vec[count] = a.b.l; 4062 con->hi_vec[count] = a.b.u; 4063 count++; 4064 } 4065 } 4066 } 4067 EndIterateLinList(plin) 4068 4069#ifdef IC_DEBUG 4070 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 4071 con->flags, con->term_count, con->c.l, con->c.u); 4072 fprintf(stderr, " op = %x, reified = %d.\n", 4073 con->op, con->reified); 4074#endif 4075 4076 /* 4077 ** Catch some annoying cases where the RHS constant is an infinity 4078 ** and clean them up. 4079 */ 4080 if (con->c.l == HUGE_VAL) { 4081 if (OpIsLessEqual(con->op)) { 4082 /* Assume the constraint is entailed. */ 4083 if (con->reified) { 4084 Unify_Boolean(con->bool, 1, result); 4085 Return_If_Not_Success(result); 4086 con->reified = 0; 4087 } 4088 Mark_Constraint_Entailed(con) 4089 } else if (OpIsGreater(con->op)) { 4090 /* Assume the constraint fails. */ 4091 if (con->reified) { 4092 Unify_Boolean(con->bool, 0, result); 4093 Return_If_Not_Success(result); 4094 con->reified = 0; 4095 Mark_Constraint_Entailed(con) 4096 } else { 4097 Fail 4098 } 4099 } 4100 } 4101 4102 if (con->reified) { 4103 /* Suspend on boolean instantiation. */ 4104 result = insert_suspension(con->bool, 1, con->susp->val.ptr, 4105 suspend_slot); 4106 Return_If_Not_Success(result) 4107 } 4108 4109 finish_setting_up_con_struct(con, lo_buf, hi_buf, var_buf, count); 4110 4111 /* Check for constraints which can be turned into unifications. */ 4112 Check_Con_Is_Unification(con) 4113 4114 return delayed ? DEBUG_SUSP_EVENT : PSUCCEED; 4115} 4116 4117 4118#if 0 4119 /* 4120 ** If the first setup pass discovered there were no variables, determine 4121 ** whether the constraint succeeds/fails, or requires a delayed goal. 4122 ** XXX - should really set up the delayed goal here, 4123 */ 4124int 4125setup_0v_con(con_info *con, prop_info *prop, int *solved) 4126{ 4127 *solved = 1; 4128 4129 switch (con->op) { 4130 case UPPER_BOUND + LOWER_BOUND: 4131 /* Equation. */ 4132 if (0.0 <= con->c.l && 0.0 >= con->c.u) { 4133 /* Entailed. */ 4134 Succeed 4135 } else if (0.0 > con->c.u || 0.0 < con->c.l) { 4136 /* Failure. */ 4137 Fail 4138 } 4139 break; 4140 4141 case UPPER_BOUND: 4142 /* Less than or equal constraint. */ 4143 if (0.0 <= con->c.l) { 4144 /* Entailed. */ 4145 Succeed 4146 } else if (0.0 > con->c.u) { 4147 /* Failure. */ 4148 Fail 4149 } 4150 break; 4151 4152 case LOWER_BOUND: 4153 /* Greater than constraint. */ 4154 if (0.0 > con->c.u) { 4155 /* Entailed. */ 4156 Succeed 4157 } else if (0.0 <= con->c.l) { 4158 /* Failure. */ 4159 Fail 4160 } 4161 break; 4162 4163 case 0: 4164 /* Disequality constraint. */ 4165 if (0.0 < con->c.l || 0.0 > con->c.u) { 4166 /* Entailed. */ 4167 Succeed 4168 } else if (0.0 == con->c.l && 0.0 == con->c.u) { 4169 /* Failure. */ 4170 Fail 4171 } 4172 break; 4173 } 4174 4175 *solved = 0; 4176 Succeed 4177} 4178#endif 4179 4180 4181int 4182setup_1v_con(pword *plin, con_info *con, prop_info *prop, int *solved) 4183{ 4184 int idx, result; 4185 pword *tmp, *pterm; 4186 typed_bounds a; 4187 bounds res, sum; 4188 var_info vi; 4189 4190#ifdef IC_DEBUG 4191 fprintf(stderr, "Entering setup_1v_con.\n"); 4192#endif 4193 4194 *solved = 0; 4195 4196#ifdef IC_DEBUG 4197 fprintf(stderr, " flags = %x, term_count = %d, cl = %f, cu = %f.\n", 4198 con->flags, con->term_count, con->c.l, con->c.u); 4199 fprintf(stderr, " reified = %d, op = %x.\n", con->reified, con->op); 4200#endif 4201 4202 sum = con->c; /* Probably zero? */ 4203 4204 BeginIterateLinList(plin, pterm, idx, a, tmp) 4205 if (!IsRef(tmp->tag)) { 4206 Constant_To_Typed_Bounds(tmp->val, tmp->tag, vi.tb); 4207 4208 /* Subtract A * X from sum. */ 4209 Mul(a.b, vi.tb.b, res); 4210 Sub(sum, res, sum); 4211 } else { 4212 get_var_info(tmp, &vi); 4213 vi.prop_int = (con->flags & CON_INTEGRALITY_PROP); 4214 4215#ifdef IC_DEBUG 4216 fprintf(stderr, " xl = %f, xu = %f, xi = %d.\n", vi.tb.b.l, 4217 vi.tb.b.u, 4218 vi.tb.i); 4219#endif 4220 4221 Mul(a.b, vi.tb.b, res); 4222 4223 /* XXX - Why aren't we using inf_f_idx/inf_e_idx for this? */ 4224 if (res.l == -HUGE_VAL) { 4225 res.l = min(0.0, res.u); 4226 } 4227 if (res.u == HUGE_VAL) { 4228 res.u = max(0.0, res.l); 4229 } 4230 4231#if 0 4232 if (prop->inf_f_idx != idx) { 4233 prop->sum.u = HUGE_VAL; 4234 } 4235 if (prop->inf_e_idx != idx) { 4236 prop->sum.l = -HUGE_VAL; 4237 } 4238#endif 4239 4240#ifdef IC_DEBUG 4241 fprintf(stderr, " prop.sum.l = %f, prop.sum.u = %f.\n", prop->sum.l, prop->sum.u); 4242 fprintf(stderr, " res.l = %f, res.u = %f.\n", res.l, res.u); 4243#endif 4244 4245 Undo_Sub(prop->sum, res, res); 4246 4247#ifdef IC_DEBUG 4248 fprintf(stderr, " lo = %f, hi = %f.\n", res.l, res.u); 4249#endif 4250 4251 if (OpIsEqual(con->op)) { 4252 return solve_equal(&a.b, &vi, &res, solved); 4253 } else if (OpIsNotEqual(con->op)) { 4254 return solve_not_equal(&a.b, &vi, &res, solved); 4255 } else { 4256 result = impose_coef_bounds(con->op, 4257 OpIsGreater(con->op), &a.b, &vi, &res); 4258 Return_If_Not_Success(result); 4259 } 4260 4261 /* Subtract A * X from sum. */ 4262 Mul(a.b, vi.tb.b, res); 4263 Sub(sum, res, sum); 4264 } 4265 EndIterateLinList(plin) 4266 4267#ifdef IC_DEBUG 4268 fprintf(stderr, " sum.l = %f, sum.u = %f.\n", sum.l, sum.u); 4269#endif 4270 4271 /* To get here, it must be an inequality. */ 4272 if (OpIsGreater(con->op) && 0.0 <= sum.l) { 4273 Fail 4274 } 4275 if (OpIsLessEqual(con->op) ? 0.0 <= sum.l : 0.0 > sum.u) { 4276 *solved = 1; 4277 } 4278 4279 Succeed 4280} 4281 4282 4283 /* 4284 ** set_up_ic_con(++Flags, ?Bool, +Lin) 4285 ** Sets up a linear constraint, Lin Op 0, where Op is encoded by Flags 4286 ** and Bool gives the reification status of the constraint. 4287 */ 4288int 4289p_set_up_ic_con(value vflags, type tflags, value vbool, type tbool, value vlin, type tlin) 4290{ 4291 int result, result2; 4292 con_info con; 4293 prop_info prop; 4294 pword lin; 4295 int status, delayed, short_cut, solved; 4296 4297 Check_Integer(tflags); 4298 4299 lin.val = vlin; 4300 lin.tag = tlin; 4301 4302 /* Make sure bool is a boolean. */ 4303 result = p_make_bool(vbool, tbool); 4304 Return_If_Error(result); 4305 if (result != PSUCCEED) { 4306 /* Don't fail until we've finished type checking. */ 4307 result2 = type_check_lin_terms(&lin, vflags.nint); 4308 Return_If_Not_Success(result2); 4309 return result; 4310 } 4311 4312 /* Make sure bool is fully dereferenced again. */ 4313 if (IsRef(tbool)) { 4314 pword *bool = vbool.ptr; 4315 Dereference(bool); 4316 vbool.all = bool->val.all; 4317 tbool.all = bool->tag.all; 4318 } 4319 4320 /* 4321 ** Set status to the effective value of the boolean (treat it as 4322 ** true if the boolean is still a variable). 4323 */ 4324 if (IsRef(tbool)) { 4325 status = 1; 4326 con.bool = vbool.ptr; 4327 con.reified = 1; 4328 } else { 4329 status = vbool.nint; 4330 con.bool = 0; 4331 con.reified = 0; 4332 } 4333 4334 con.c.l = NEG_ZERO; 4335 con.c.u = 0.0; 4336 con.flags = vflags.nint; 4337 con.term_count = 0; 4338 con.op = FlagsAndBoolToOp(con.flags, status); 4339 /* Don't try to access these yet... */ 4340 con.con = 0; 4341 con.data = 0; 4342 con.lo_vec = 0; 4343 con.hi_vec = 0; 4344 con.var_vec = 0; 4345 con.susp = 0; 4346 4347 /* Just do a type check and count the terms for now. */ 4348 result = setup_pass_1(&lin, &con, &prop); 4349 Return_If_Not_Success(result); 4350 4351 if (con.reified) { 4352 /* No propagation, just check entailment/disentailment. */ 4353 /* Already know the answer if no_prop has been set. */ 4354 if (!prop.no_prop) { 4355 result = evaluate_reified(&con, &prop, &solved); 4356 Return_If_Not_Success(result); 4357 if (solved) { 4358 Succeed 4359 } 4360 /* 4361 ** Make sure we don't try to propagate later during 4362 ** constraint set up. 4363 */ 4364 prop.no_prop = 1; 4365 } 4366 } else { 4367 /* Check short-cuts. */ 4368 result = short_cuts(&con, &prop, &short_cut); 4369 Return_If_Not_Success(result); 4370 4371 switch(short_cut) { 4372 case SHORT_NONE: 4373 /* Continue execution. */ 4374 break; 4375#ifdef USE_BOUND_SET_SHORTCUT 4376 case SHORT_LWB: 4377 ... 4378 break; 4379 case SHORT_UPB: 4380 ... 4381 break; 4382#endif 4383 case SHORT_ENTAILED: 4384 /* Nothing more to do. */ 4385 Succeed 4386 break; 4387 default: 4388 Bip_Error(EC_EXTERNAL_ERROR); 4389 break; 4390 } 4391 } 4392 4393 /* 4394 ** XXX - check for zero-variable constraints? 4395 ** "Solved" ones should already by short-cutted by the above, but 4396 ** delayed ones could be set up simpler/faster than using the 4397 ** general approach below. 4398 */ 4399#if 0 4400 if (con.term_count == 0) { 4401 result = setup_0v_con(&con, &prop, &solved); 4402 Return_If_Not_Success(result) 4403 if (solved) { 4404 Succeed 4405 } 4406 } else 4407#endif 4408 4409 /* 4410 ** XXX - check for one-variable constraints (likely to be entailed 4411 ** after propagation if all constants are zero-width). 4412 */ 4413 if (!prop.no_prop && !con.reified && con.term_count == 1) { 4414 result = setup_1v_con(&lin, &con, &prop, &solved); 4415 Return_If_Not_Success(result) 4416 if (solved) { 4417 Succeed 4418 } 4419 /* 4420 ** We've already propagated, and doing so again during 4421 ** constraint set up will give the wrong answer if infinities 4422 ** are involved, so make sure we don't. 4423 */ 4424 prop.no_prop = 1; 4425 } 4426 4427 /* XXX - check for two-variable equations to make unifications. */ 4428 4429 /* Create the ic_con structure. */ 4430 con.con = TG; 4431 Push_Struct_Frame(d_ic_con); 4432 4433 con.con[CON_OFF_BOOLEAN].val.all = vbool.all; 4434 con.con[CON_OFF_BOOLEAN].tag.all = tbool.all; 4435 4436 delayed = 0; 4437 result = process_lin_terms_to_vectors_and_prop(&lin, &con, &prop); 4438 if (result == DEBUG_SUSP_EVENT) { 4439 delayed = 1; 4440 result = PSUCCEED; 4441 } 4442 if (result != PSUCCEED) { 4443 /* Restore global stack to remove any garbage we added. */ 4444 TG = con.con; 4445 return result; 4446 } 4447 4448 return delayed ? DEBUG_SUSP_EVENT : PSUCCEED; 4449} 4450 4451int 4452p_get_print_info(value vcon, type tcon, value vflags, type tflags, 4453 value vbool, type tbool, value vcoefs, type tcoefs, 4454 value vvars, type tvars, value vc, type tc) 4455{ 4456 con_info con; 4457 pword *dest; 4458 int result, i; 4459 bounds a; 4460 value val; 4461 type tag; 4462 dident did; 4463 pword res; 4464 4465 /* XXX - check that it really is an IC constraint structure. */ 4466 Check_Structure(tcon); 4467 4468 con_struct_vec_to_con_info(vcon.ptr, &con); 4469 4470 result = Unify_Pw(vbool, tbool, 4471 con.con[CON_OFF_BOOLEAN].val, con.con[CON_OFF_BOOLEAN].tag); 4472 Return_If_Not_Success(result); 4473 4474 val.nint = con.flags; 4475 tag.kernel = TINT; 4476 result = Unify_Pw(vflags, tflags, val, tag); 4477 Return_If_Not_Success(result); 4478 4479 Bounds_To_Constant(con.c.l, con.c.u, &res); 4480 result = Unify_Pw(vc, tc, res.val, res.tag); 4481 Return_If_Not_Success(result); 4482 4483 if (con.term_count > 0) { 4484 did = ec_did("[]", con.term_count); 4485 val.ptr = TG; 4486 tag.kernel = TCOMP; 4487 Push_Struct_Frame(did); 4488 4489 for (i = 0; i < con.term_count; i++) { 4490 a.l = con.lo_vec[i]; 4491 a.u = con.hi_vec[i]; 4492 dest = val.ptr + i + 1; 4493 4494 Bounds_To_Constant(a.l, a.u, dest); 4495 } 4496 result = Unify_Pw(vcoefs, tcoefs, val, tag); 4497 Return_If_Not_Success(result); 4498 4499 val.ptr = TG; 4500 Push_Struct_Frame(did); 4501 /* Copy the first term_count elements from the variable array. */ 4502 memcpy(val.ptr + 1, con.var_vec, con.term_count * sizeof(pword)); 4503 result = Unify_Pw(vvars, tvars, val, tag); 4504 Return_If_Not_Success(result); 4505 } else { 4506 val.ptr = 0; 4507 tag.kernel = TNIL; 4508 4509 result = Unify_Pw(vcoefs, tcoefs, val, tag); 4510 Return_If_Not_Success(result); 4511 result = Unify_Pw(vvars, tvars, val, tag); 4512 Return_If_Not_Success(result); 4513 } 4514 4515 Succeed 4516} 4517 4518 4519#if 0 4520int 4521prop_0v(int flags, pword *bool, double cl, double cu, value vsusp, type tsusp, ...) 4522{ 4523 if (flags & CON_EQUATION) { 4524 /* Equation or disequation. */ 4525 ... 4526 } else { 4527 /* Inequality. */ 4528 ... 4529 } 4530 4531 ... 4532} 4533#endif 4534 4535 4536/*---------------------------------------------------------------------- 4537** 4538** Support for ic_kernel.ecl. 4539** 4540** The functions in this section are mainly in support of the ic_kernel 4541** module. 4542** 4543*/ 4544 4545 /* 4546 ** ic_init() 4547 ** Caches IC attribute slot and auxiliary dictionary 4548 ** entries needed required for attribute 4549 ** extraction/creation from/of an IC variable. 4550 */ 4551int 4552p_ic_init() 4553{ 4554 pword module; 4555 int result; 4556 4557 ic_domain_slot = meta_index(ec_did("ic", 0)); 4558 suspend_slot = meta_index(ec_did("suspend", 0)); 4559 d_ic_attr_functor = ec_did("ic", ATTR_ARITY); 4560 d_ic_con = ec_did("ic_con", CON_ARITY); 4561 d_ic_real = ec_did("real", 0); 4562 d_ic_integer = ec_did("integer", 0); 4563 d_ic_undefined = ec_did("undefined", 0); 4564 4565 module.val.did = ec_did("ic_kernel", 0); 4566 module.tag.kernel = TDICT; 4567 4568/* 4569 d_prop_ic_con = ec_did("prop_ic_con", 1); 4570 result = ec_visible_procedure(d_prop_ic_con, module, 4571 &proc_prop_ic_con); 4572 Return_If_Not_Success(result); 4573*/ 4574 4575 d_exclude = ec_did("exclude", 2); 4576 result = ec_visible_procedure(d_exclude, module, &proc_exclude); 4577 Return_If_Not_Success(result); 4578 4579 d_exclude_range = ec_did("exclude_range", 3); 4580 result = ec_visible_procedure(d_exclude_range, module, 4581 &proc_exclude_range); 4582 Return_If_Not_Success(result); 4583 4584 result = ec_visible_procedure(d_.infq, module, &proc_infq); 4585 Return_If_Not_Success(result); 4586 result = ec_visible_procedure(d_.supq, module, &proc_supq); 4587 Return_If_Not_Success(result); 4588 4589 Succeed; 4590} 4591 4592 /* 4593 ** ic_constraints_init() 4594 ** Initialisation for ic_constraints. 4595 */ 4596int 4597p_ic_constraints_init() 4598{ 4599 pword module; 4600 int result; 4601 4602 module.val.did = ec_did("ic_constraints", 0); 4603 module.tag.kernel = TDICT; 4604 4605 d_prop_ic_con = ec_did("prop_ic_con", 1); 4606 result = ec_visible_procedure(d_prop_ic_con, module, 4607 &proc_prop_ic_con); 4608 Return_If_Not_Success(result); 4609 4610 Succeed; 4611} 4612 4613 4614 /* 4615 ** get_ic_attr(?Var, -Attr) 4616 ** Returns the IC attribute of a variable. If the variable does 4617 ** not have an IC attribute, it is given one first. Attr must be a 4618 ** fresh variable. 4619 */ 4620int 4621p_get_ic_attr(value vvar, type tvar, value vattr, type tattr) 4622{ 4623 pword *res; 4624 4625 if (!IsRef(tvar)) { 4626 Fail 4627 } 4628 4629 res = make_ic_var_attr(vvar.ptr); 4630 Return_Bind_Var(vattr, tattr, res->val.all, res->tag.kernel); 4631} 4632 4633 4634 /* 4635 ** Return the given bounds as integers if possible, or doubles if not 4636 ** (i.e. because they're infinite). 4637 ** Assumes the lower bound cannot be +inf or the upper bound -inf. 4638 */ 4639int 4640unify_integer_bounds(double lwb, double upb, value vlo, type tlo, value vhi, type thi) 4641{ 4642 value val; 4643 type tag; 4644 int result; 4645 4646 tag.kernel = TDBL; 4647 4648 /* Lower bound. */ 4649 Make_Double_Val(val, lwb); 4650 if (lwb != -HUGE_VAL) { 4651 /* Return an integer. */ 4652 result = unary_arith_op(val, tag, vlo, tlo, ARITH_FIX, TINT); 4653 } else { 4654 result = Unify_Pw(vlo, tlo, val, tag); 4655 } 4656 Return_If_Not_Success(result); 4657 4658 /* Upper bound. */ 4659 Make_Double_Val(val, upb); 4660 if (upb != HUGE_VAL) { 4661 /* Return an integer. */ 4662 result = unary_arith_op(val, tag, vhi, thi, ARITH_FIX, 4663 TINT); 4664 } else { 4665 result = Unify_Pw(vhi, thi, val, tag); 4666 } 4667 4668 return result; 4669} 4670 4671 /* 4672 ** get_bounds(?Var, -Lo, -Hi) 4673 ** Unifies Lo and Hi with the lower and upper (resp.) IC bounds of 4674 ** the variable Var. If Var is an integer variable then the bounds 4675 ** returned will be integer (unless they're infinite). Also works 4676 ** if Var is a ground number. 4677 */ 4678int 4679p_get_bounds(value vvar, type tvar, value vlo, type tlo, value vhi, type thi) 4680{ 4681 value val; 4682 type tag; 4683 int result; 4684 4685 tag.kernel = TDBL; 4686 4687 if (IsRef(tvar)) { 4688 var_info vi; 4689 /* For variables, extract the bounds and return them. */ 4690 make_var_info(vvar.ptr, &vi); 4691 if (vi.tb.i) { 4692 return unify_integer_bounds(vi.tb.b.l, vi.tb.b.u, vlo, tlo, vhi, thi); 4693 } else { 4694 Make_Double_Val(val, vi.tb.b.l); 4695 result = Unify_Pw(vlo, tlo, val, tag); 4696 Return_If_Not_Success(result); 4697 Make_Double_Val(val, vi.tb.b.u); 4698 return Unify_Pw(vhi, thi, val, tag); 4699 } 4700 } else if (IsInteger(tvar) || IsBignum(tvar) || IsDouble(tvar)) { 4701 /* For integers and floats, the bounds are equal to the input. */ 4702 result = Unify_Pw(vlo, tlo, vvar, tvar); 4703 Return_If_Not_Success(result); 4704 return Unify_Pw(vhi, thi, vvar, tvar); 4705 } else if (IsNumber(tvar)) { 4706 /* For other numbers, coerce to bounded real and return bounds. */ 4707 value breal; 4708 result = tag_desc[TagType(tvar)].coerce_to[TIVL](vvar, &breal); 4709 Return_If_Not_Success(result); 4710 Make_Double_Val(val, IvlLwb(breal.ptr)); 4711 result = Unify_Pw(vlo, tlo, val, tag); 4712 Return_If_Not_Success(result); 4713 Make_Double_Val(val, IvlUpb(breal.ptr)); 4714 return Unify_Pw(vhi, thi, val, tag); 4715 } else { 4716 Bip_Error(TYPE_ERROR) 4717 } 4718 /* Not reached. */ 4719} 4720 4721 4722 /* 4723 ** get_integer_bounds1(?Var, ++Finite, -Lo, -Hi, -Wake) 4724 ** Unifies Lo and Hi with the lower and upper (resp.) IC bounds of 4725 ** the variable X. Var is constrained to be an integer IC 4726 ** variable. If Finite == 1 then Var is also constrained to be 4727 ** finite (-10000000..10000000 by default). Wake must be a fresh 4728 ** variable, and is set to 1 if something has changed which 4729 ** warrants a call to wake/0 (otherwise it's set to 0). 4730 ** The bounds returned will be integer unless they're infinite. 4731 ** Var must be a variable. 4732 */ 4733int 4734p_get_integer_bounds1(value vvar, type tvar, value vfinite, type tfinite, 4735 value vlo, type tlo, value vhi, type thi, value vwake, type twake) 4736{ 4737 var_info vi; 4738 int wake = 0; 4739 int result; 4740 4741 Check_Ref(tvar); 4742 Check_Integer(tfinite); 4743 4744 make_var_info(vvar.ptr, &vi); 4745 4746 /* Make sure the variable is integral. */ 4747 if (!vi.tb.i) { 4748 /* Update the type. */ 4749 result = set_integral(&vi); 4750 Return_If_Not_Success(result); 4751 wake = 1; 4752 } 4753 4754 /* Make sure the bounds are finite if that's required. */ 4755 if (vfinite.nint) { 4756 if (vi.tb.b.l == -HUGE_VAL) { 4757 result = ic_lwb(&vi, -10000000.0); 4758 Return_If_Not_Success(result); 4759 wake = 1; 4760 } 4761 if (vi.tb.b.u == HUGE_VAL) { 4762 result = ic_upb(&vi, 10000000.0); 4763 Return_If_Not_Success(result); 4764 wake = 1; 4765 } 4766 } 4767 4768 /* Return the bounds. */ 4769 result = unify_integer_bounds(vi.tb.b.l, vi.tb.b.u, vlo, tlo, vhi, thi); 4770 Return_If_Not_Success(result); 4771 4772 Return_Integer(vwake, twake, wake); 4773 4774 Succeed 4775} 4776 4777 4778 /* 4779 ** get_domain_size(?Var, -Size) 4780 ** Returns the number of integer elements in the domain of Var. 4781 ** Returns 1 if Var is a number. 4782 ** Throws a range error if Var is a real variable. 4783 */ 4784int 4785p_get_domain_size(value vvar, type tvar, value vsize, type tsize) 4786{ 4787 pword *attr; 4788 double lwb, upb; 4789 dident ic_type; 4790 pword *bitmap; 4791 pword res; 4792 int result; 4793 4794 if (IsNumber(tvar)) { 4795 /* Unify Size with 1. */ 4796 res.val.nint = 1; 4797 res.tag.kernel = TINT; 4798 Return_Unify_Pw(vsize, tsize, res.val, res.tag); 4799 } 4800 if (!IsMeta(tvar)) { 4801 /* Not a variable or no attributes. */ 4802 Bip_Error(TYPE_ERROR) 4803 } 4804 IC_Var_Get_Attr(vvar.ptr, attr); 4805 if (IsRef(attr->tag)) { 4806 /* No IC attribute. */ 4807 Bip_Error(TYPE_ERROR) 4808 } 4809 /* Get the attribute's vector. */ 4810 attr = attr->val.ptr; 4811 Dereference(attr); 4812 4813 IC_Var_Info(attr, lwb, upb, ic_type, bitmap); 4814 4815 if (!Type_Is_Int(ic_type)) { 4816 /* Not an integer IC variable. */ 4817 Bip_Error(RANGE_ERROR) 4818 } 4819 4820 if (IsAtom(bitmap->tag)) { 4821 /* 4822 ** No bitmap: size is just one more than the difference between 4823 ** the bounds. 4824 ** XXX - Claim that we don't care if it's inaccurate for domains 4825 ** which extend beyond the float-representable integers, since 4826 ** the domain can't represent them all anyway. Hence don't 4827 ** bother being careful with the float operations... 4828 */ 4829 double fsize; 4830 4831 fsize = upb - lwb + 1; 4832 if (fsize == HUGE_VAL) { 4833 /* For compatibility with old version, not unreasonable... */ 4834 Make_Double_Val(res.val, fsize); 4835 res.tag.kernel = TDBL; 4836 } else { 4837 result = ec_double_to_int_or_bignum(fsize, &res); 4838 Return_If_Not_Success(result); 4839 } 4840 } else { 4841 res.val.nint = bitmap_size(bitmap->val.wptr); 4842 res.tag.kernel = TINT; 4843 } 4844 4845 Return_Unify_Pw(vsize, tsize, res.val, res.tag); 4846} 4847 4848 4849/*---------------------------------------------------------------------- 4850** 4851** Unification helper predicate. 4852** 4853*/ 4854 4855 /* 4856 ** Check that the number represented by vnum/tnum is in the domain 4857 ** represented by attr2 and wake any appropriate suspension lists. 4858 */ 4859int 4860unify_number_ic(value vnum, type tnum, pword *attr2vec) 4861{ 4862 double cl, cu; 4863 int ci; 4864 double lwb, upb; 4865 dident ic_type; 4866 pword *bitmap; 4867 pword *pw; 4868 int delayed = 0; 4869 int result; 4870 4871 /* 4872 ** XXX - should we try to do something better with integers which 4873 ** can't be represented exactly as doubles? 4874 */ 4875 4876 Constant_To_Bounds(vnum, tnum, cl, cu, ci); 4877 4878 IC_Var_Info(attr2vec, lwb, upb, ic_type, bitmap); 4879 4880 if (cu < lwb || cl > upb) { 4881 /* Value completely outside domain. */ 4882 Fail 4883 } 4884 4885 if (Type_Is_Int(ic_type)) { 4886 if (!ci) { 4887 /* Don't allow binding an integer var to a non-integer value. */ 4888 Fail 4889 } 4890 4891 if (!IsAtom(bitmap->tag)) { 4892 /* 4893 ** Since there's a bitmap, we can assume anything falling 4894 ** within lwb..upb (which num does if we got here) can 4895 ** safely be cast to a word. This also means we can assume 4896 ** num is a TINT (any integer representable in a word is 4897 ** TINT rather than TBIG). Using vnum.nint means we don't 4898 ** have to worry about any fuzziness in cl/cu if we're on a 4899 ** 64-bit architecture and num is beyond the range exactly 4900 ** representable as a double. 4901 */ 4902 result = bitmap_contains(bitmap->val.wptr, vnum.nint); 4903 Return_If_Not_Success(result) 4904 } 4905 } 4906 4907 /* Check if num implies a type change for attr2. */ 4908 if (ci && !Type_Is_Int(ic_type)) { 4909 result = ec_schedule_susps(attr2vec + OFF_WAKE_TYPE); 4910 Return_If_Not_Success(result) 4911 } 4912 4913 /* Check if num implies bound changes for attr2. */ 4914 if (cl > lwb) { 4915 /* Bound change. */ 4916 result = ec_schedule_susps(attr2vec + OFF_WAKE_LO); 4917 Return_If_Not_Success(result) 4918 } else { 4919 /* No bound change --- postpone the suspensions. */ 4920 result = p_schedule_postponed(attr2vec[OFF_WAKE_LO].val, 4921 attr2vec[OFF_WAKE_LO].tag); 4922 Return_If_Not_Success(result) 4923 if (cl < lwb) { 4924 /* Overlap --- set up delayed goal: Lwb =< Num. */ 4925 pword goal, dummy_susp; 4926 pw = TG; 4927 Push_Struct_Frame(d_.infq); 4928 pw[1].val = attr2vec[OFF_LO].val; 4929 pw[1].tag = attr2vec[OFF_LO].tag; 4930 pw[2].val = vnum; 4931 pw[2].tag = tnum; 4932 Make_Struct(&goal, pw); 4933 result = ec_make_suspension(goal, 0, proc_infq, &dummy_susp); 4934 if (result == DEBUG_SUSP_EVENT) { 4935 delayed = 1; 4936 result = PSUCCEED; 4937 } 4938 Return_If_Not_Success(result) 4939 } 4940 } 4941 if (cu < upb) { 4942 /* Bound change. */ 4943 result = ec_schedule_susps(attr2vec + OFF_WAKE_HI); 4944 Return_If_Not_Success(result) 4945 } else { 4946 /* No bound change --- postpone the suspensions. */ 4947 result = p_schedule_postponed(attr2vec[OFF_WAKE_HI].val, 4948 attr2vec[OFF_WAKE_HI].tag); 4949 Return_If_Not_Success(result) 4950 if (cu > upb) { 4951 /* Overlap --- set up delayed goal: Upb >= Num. */ 4952 pword goal, dummy_susp; 4953 pw = TG; 4954 Push_Struct_Frame(d_.supq); 4955 pw[1].val = attr2vec[OFF_HI].val; 4956 pw[1].tag = attr2vec[OFF_HI].tag; 4957 pw[2].val = vnum; 4958 pw[2].tag = tnum; 4959 Make_Struct(&goal, pw); 4960 result = ec_make_suspension(goal, 0, proc_supq, &dummy_susp); 4961 if (result == DEBUG_SUSP_EVENT) { 4962 delayed = 1; 4963 result = PSUCCEED; 4964 } 4965 Return_If_Not_Success(result) 4966 } 4967 } 4968 4969 return delayed ? DEBUG_SUSP_EVENT : PSUCCEED; 4970} 4971 4972/* 4973Var1 Var2 Actions 4974real real Take max of lower bounds, min of upper bounds, check non-empty. 4975 Impose bounds on var1. 4976 Wake either var slack bounds. 4977real int Round bounds of var1. 4978 Take max of lower bounds, min of upper bounds, check non-empty. 4979 Impose bounds on var1. 4980 Wake var1 type change and either var slack bounds. 4981real bitmap Round bounds of var1. 4982 Impose var1 bounds on var2 bitmap, check non-empty. 4983 Extract (only if slack?) bounds from new bitmap. 4984 Impose bounds on var1 and give it new bitmap. 4985 Wake var1 type change and hole and either var slack bounds. 4986int real Round bounds of var2. 4987 Take max of lower bounds, min of upper bounds, check non-empty. 4988 Impose bounds on var1. 4989 Wake var2 type change and either var slack bounds. 4990int int Take max of lower bounds, min of upper bounds, check non-empty. 4991 Impose bounds on var1. 4992 Wake either var slack bounds. 4993int bitmap Impose var1 bounds on var2 bitmap, check non-empty. 4994 Extract (only if slack?) bounds from new bitmap. 4995 Impose bounds on var1 and give it new bitmap. 4996 Wake var1 hole and either var slack bounds. 4997bitmap real Round bounds of var2. 4998 Impose var2 bounds on var1 bitmap, check non-empty. 4999 Extract (only if slack?) bounds from new bitmap. 5000 Impose bounds on var1 and give it new bitmap (if required). 5001 Wake var2 type change and hole and either var slack bounds. 5002bitmap int Impose var2 bounds on var1 bitmap, check non-empty. 5003 Extract (only if slack?) bounds from new bitmap. 5004 Impose bounds on var1 and give it new bitmap (if required). 5005 Wake var2 hole and either var slack bounds. 5006bitmap bitmap Compare bitmaps to check for subsumption of one by the other. 5007 ... 5008 Intersect var2 bitmap into var1 bitmap, check non-empty. 5009 Extract (only if slack?) bounds from new bitmap. 5010 Impose bounds on var1 and give it new bitmap (if required). 5011*/ 5012 5013 5014 /* 5015 ** Intersect the domain represented by attr2 into that of attr1, merging 5016 ** and waking any appropriate suspension lists. 5017 */ 5018int 5019unify_ic_ic(pword *attr1vec, pword *attr2vec, value vvar, type tvar, value vsusp_attr, type tsusp_attr) 5020{ 5021 double lwb, upb; 5022 word min, max; 5023 double lwb1, upb1; 5024 double lwb2, upb2; 5025 dident ic_type, ic_type1, ic_type2; 5026 pword *bitmap1, *bitmap2; 5027 uword *bitmap_ptr; 5028 value val, a1val, a2val; 5029 type tag, atag; 5030 int integral; 5031 int res; 5032 int result; 5033 int constrained1, constrained2; 5034 5035 IC_Var_Info(attr1vec, lwb1, upb1, ic_type1, bitmap1); 5036 IC_Var_Info(attr2vec, lwb2, upb2, ic_type2, bitmap2); 5037 5038 constrained1 = 0; 5039 constrained2 = 0; 5040 5041#if 1 5042 lwb = lwb1 > lwb2 ? lwb1 : lwb2; 5043 upb = upb1 < upb2 ? upb1 : upb2; 5044 5045 if (upb < lwb) { 5046 Fail 5047 } 5048 5049 if (Type_Is_Int(ic_type1)) { 5050 integral = 1; 5051 if (!Type_Is_Int(ic_type2)) { 5052 /* ic_type2 is real, unified type is integer. */ 5053 lwb = ceil(lwb); /* In case it was lwb2. */ 5054 upb = floor(upb); /* In case it was upb2. */ 5055 if (upb < lwb) { 5056 Fail 5057 } 5058 result = ec_schedule_susps(attr2vec + OFF_WAKE_TYPE); 5059 Return_If_Not_Success(result) 5060 constrained2 = 1; 5061 } 5062 } else { 5063 if (Type_Is_Int(ic_type2)) { 5064 integral = 1; 5065 /* ic_type1 is real, unified type is integer. */ 5066 lwb = ceil(lwb); /* In case it was upb1. */ 5067 upb = floor(upb); /* In case it was upb1. */ 5068 if (upb < lwb) { 5069 Fail 5070 } 5071 result = ec_schedule_susps(attr1vec + OFF_WAKE_TYPE); 5072 Return_If_Not_Success(result) 5073 constrained1 = 1; 5074 /* Update the type field. */ 5075 val.did = d_.integer0; 5076 tag.kernel = TDICT; 5077 ec_assign(attr1vec + OFF_TYPE, val, tag); 5078 } else { 5079 integral = 0; 5080 } 5081 } 5082#else 5083 Unfortunately this version modifies lwb/upb[12], which makes it 5084 harder to check which suspension lists to wake. 5085 5086 if (Type_Is_Int(ic_type1) || Type_Is_Int(ic_type2)) { 5087 ic_type = d_.integer0; 5088 } else { 5089 ic_type = ic_type1; 5090 } 5091 5092 if (ic_type1 != ic_type) { 5093 /* ic_type1 is real, ic_type is integer. */ 5094 lwb1 = ceil(lwb1); 5095 upb1 = floor(upb1); 5096 result = ec_schedule_susps(attr1vec + OFF_WAKE_TYPE); 5097 Return_If_Not_Success(result) 5098 } else if (ic_type2 != ic_type) { 5099 /* ic_type2 is real, ic_type is integer. */ 5100 lwb2 = ceil(lwb2); 5101 upb2 = floor(upb2); 5102 result = ec_schedule_susps(attr2vec + OFF_WAKE_TYPE); 5103 Return_If_Not_Success(result) 5104 } 5105 5106 lwb = max(lwb1, lwb2); 5107 upb = min(upb1, upb2); 5108 5109 if (upb < lwb) { 5110 Fail 5111 } 5112#endif 5113 5114 if (!IsAtom(bitmap1->tag)) { 5115 if (!IsAtom(bitmap2->tag)) { 5116 /* 5117 ** Both vars have bitmaps; compare them before intersecting 5118 ** them, in case the intersection is trivial. 5119 */ 5120 result = compare_bitmaps(bitmap1->val.wptr, 5121 bitmap2->val.wptr, &res); 5122 /* 5123 ** XXX - No convenient/cheap way to know whether internal 5124 ** elements would be removed from bitmap1 or bitmap2 (or 5125 ** even find out whether they were, after an intersection is 5126 ** actually done). 5127 */ 5128 if (result == PSUCCEED) { 5129 if (res < 0) { 5130 /* Bitmap1 is contained in bitmap2. */ 5131 /* Wake things suspended on new holes in second var. */ 5132 result = ec_schedule_susps(attr2vec + OFF_WAKE_HOLE); 5133 Return_If_Not_Success(result) 5134 constrained2 = 1; 5135 } else if (res > 0) { 5136 /* Bitmap1 contains bitmap2. */ 5137 /* Update attr1 to point at bitmap2. */ 5138 ec_assign(attr1vec + OFF_BITMAP, bitmap2->val, 5139 bitmap2->tag); 5140 /* Wake things suspended on new holes in first var. */ 5141 result = ec_schedule_susps(attr1vec + OFF_WAKE_HOLE); 5142 Return_If_Not_Success(result) 5143 constrained1 = 1; 5144 } else { 5145 /* Bitmaps are equal. */ 5146 } 5147 /* Note that the bitmap's bounds don't need updating. */ 5148 } else { 5149 /* Neither bitmap contains the other. */ 5150 /* Intersect the bitmaps. */ 5151 res = bitmap_intersect_into(bitmap1->val.wptr, 5152 bitmap2->val.wptr, 0, &bitmap_ptr); 5153 if (Result_Is_Empty(res)) { 5154 Fail 5155 } 5156 if (Result_Is_Slack(res)) { 5157 /* Intersection resulted in bound change(s). */ 5158 bitmap_range(bitmap_ptr, &min, &max); 5159 lwb = (double) min; 5160 upb = (double) max; 5161 } 5162 /* Update the pointer in attr1 if the bitmap has moved. */ 5163 if (bitmap_ptr != bitmap1->val.wptr) { 5164 val.wptr = bitmap_ptr; 5165 tag.kernel = TBITMAP; 5166 ec_assign(attr1vec + OFF_BITMAP, val, tag); 5167 } 5168 /* Wake things suspended on new holes. */ 5169 result = ec_schedule_susps(attr1vec + OFF_WAKE_HOLE); 5170 Return_If_Not_Success(result) 5171 result = ec_schedule_susps(attr2vec + OFF_WAKE_HOLE); 5172 Return_If_Not_Success(result) 5173 constrained1 = 1; 5174 constrained2 = 1; 5175 } 5176 } else { 5177 /* 5178 ** First var has a bitmap, but second does not: trim 5179 ** bitmap1 to match the new bounds and update the pointer in 5180 ** attr1 if required. 5181 */ 5182 bitmap_ptr = bitmap1->val.wptr; 5183 min = (word) lwb; 5184 res = set_bitmap_lwb(bitmap_ptr, min, &bitmap_ptr); 5185 if (Result_Is_Empty(res)) { 5186 Fail 5187 } 5188 max = (word) upb; 5189 res |= set_bitmap_upb(bitmap_ptr, max, &bitmap_ptr); 5190 if (Result_Is_Empty(res)) { 5191 Fail 5192 } 5193 if (Result_Is_Slack(res)) { 5194 /* Bitmap resulted in trimming one of the bounds. */ 5195 bitmap_range(bitmap_ptr, &min, &max); 5196 lwb = (double) min; 5197 upb = (double) max; 5198 } 5199 /* Update the pointer in attr1 if the bitmap has moved. */ 5200 if (bitmap_ptr != bitmap1->val.wptr) { 5201 val.wptr = bitmap_ptr; 5202 tag.kernel = TBITMAP; 5203 ec_assign(attr1vec + OFF_BITMAP, val, tag); 5204 } 5205 /* Wake things suspended on new holes in the second var. */ 5206 result = ec_schedule_susps(attr2vec + OFF_WAKE_HOLE); 5207 Return_If_Not_Success(result) 5208 constrained2 = 1; 5209 } 5210 } else if (!IsAtom(bitmap2->tag)) { 5211 /* 5212 ** Second var has a bitmap, but first does not: trim bitmap2 to 5213 ** match the new bounds and update attr1 to point to it. 5214 */ 5215 bitmap_ptr = bitmap2->val.wptr; 5216 min = (word) lwb; 5217 res = set_bitmap_lwb(bitmap_ptr, min, &bitmap_ptr); 5218 if (Result_Is_Empty(res)) { 5219 Fail 5220 } 5221 max = (word) upb; 5222 res |= set_bitmap_upb(bitmap_ptr, max, &bitmap_ptr); 5223 if (Result_Is_Empty(res)) { 5224 Fail 5225 } 5226 if (Result_Is_Slack(res)) { 5227 /* Bitmap resulted in trimming one of the bounds. */ 5228 bitmap_range(bitmap_ptr, &min, &max); 5229 lwb = (double) min; 5230 upb = (double) max; 5231 } 5232 /* Add bitmap to attr1. */ 5233 val.wptr = bitmap_ptr; 5234 tag.kernel = TBITMAP; 5235 ec_assign(attr1vec + OFF_BITMAP, val, tag); 5236 /* Wake things suspended on new holes in the first var. */ 5237 result = ec_schedule_susps(attr1vec + OFF_WAKE_HOLE); 5238 Return_If_Not_Success(result) 5239 constrained1 = 1; 5240 } 5241 5242 if (lwb == upb) { 5243 pword num; 5244 5245 if (integral) { 5246 /* Bind var to integer/bignum. */ 5247 result = ec_double_to_int_or_bignum(lwb, &num); 5248 Return_If_Not_Success(result); 5249 } else { 5250 /* Bind var to bounded real. */ 5251 Make_Interval(&num, lwb, lwb); 5252 } 5253 result = Unify_Pw(vvar, tvar, num.val, num.tag); 5254 Return_If_Not_Success(result); 5255 } 5256 5257 /* Update bounds if needed, and wake things suspended on bounds. */ 5258 if (lwb > lwb1) { 5259 /* XXX - Should we avoid creating a new double if lwb == lwb2? */ 5260 Make_Checked_Double_Val(val, lwb); 5261 tag.kernel = TDBL; 5262 ec_assign(attr1vec + OFF_LO, val, tag); 5263 result = ec_schedule_susps(attr1vec + OFF_WAKE_LO); 5264 Return_If_Not_Success(result) 5265 constrained1 = 1; 5266 } 5267 if (upb < upb1) { 5268 /* XXX - Should we avoid creating a new double if upb == upb2? */ 5269 Make_Checked_Double_Val(val, upb); 5270 tag.kernel = TDBL; 5271 ec_assign(attr1vec + OFF_HI, val, tag); 5272 result = ec_schedule_susps(attr1vec + OFF_WAKE_HI); 5273 Return_If_Not_Success(result) 5274 constrained1 = 1; 5275 } 5276 if (lwb > lwb2) { 5277 result = ec_schedule_susps(attr2vec + OFF_WAKE_LO); 5278 Return_If_Not_Success(result) 5279 constrained2 = 1; 5280 } 5281 if (upb < upb2) { 5282 result = ec_schedule_susps(attr2vec + OFF_WAKE_HI); 5283 Return_If_Not_Success(result) 5284 constrained2 = 1; 5285 } 5286 5287 if (constrained1) { 5288 notify_constrained(vvar.ptr); 5289 } 5290 if (constrained2 && IsStructure(tsusp_attr)) { 5291 ec_schedule_susps(vsusp_attr.ptr + CONSTRAINED_OFF); 5292 } 5293 5294 /* Merge the suspension lists. */ 5295 tag.kernel = TINT; 5296 val.nint = OFF_WAKE_LO; 5297 atag.kernel = TCOMP; 5298 a1val.ptr = attr1vec; 5299 a2val.ptr = attr2vec; 5300 result = p_merge_suspension_lists( 5301 val, tag, a2val, atag, 5302 val, tag, a1val, atag); 5303 Return_If_Not_Success(result) 5304 val.nint = OFF_WAKE_HI; 5305 result = p_merge_suspension_lists( 5306 val, tag, a2val, atag, 5307 val, tag, a1val, atag); 5308 Return_If_Not_Success(result) 5309 val.nint = OFF_WAKE_HOLE; 5310 result = p_merge_suspension_lists( 5311 val, tag, a2val, atag, 5312 val, tag, a1val, atag); 5313 Return_If_Not_Success(result) 5314 val.nint = OFF_WAKE_TYPE; 5315 result = p_merge_suspension_lists( 5316 val, tag, a2val, atag, 5317 val, tag, a1val, atag); 5318 Return_If_Not_Success(result) 5319 5320 Succeed 5321} 5322 5323 5324 /* 5325 ** unify_ic(?Term, ?Attr, ?SuspAttr) 5326 ** Unification handler for IC variables. 5327 */ 5328int 5329p_unify_ic(value vterm, type tterm, value vattr, type tattr, value vsusp_attr, type tsusp_attr) 5330{ 5331 pword *attr1; 5332 pword *attr1vec, *attr2vec; 5333 5334 if (IsRef(tattr)) { 5335 /* 5336 ** Second variable has no IC attribute - only thing to do is 5337 ** wake the second variable's constrained list (if it has one) 5338 ** if the first term is an IC variable (other cases covered 5339 ** elsewhere, right?). 5340 */ 5341 if (IsStructure(tsusp_attr) && IsRef(tterm)) { 5342 IC_Var_Get_Attr(vterm.ptr, attr1); 5343 if (!IsRef(attr1->tag)) { 5344 ec_schedule_susps(vsusp_attr.ptr + CONSTRAINED_OFF); 5345 } 5346 } 5347 Succeed 5348 } 5349 if (!IsStructure(tattr)) { 5350 /* IC attribute of second var is not a structure! */ 5351 Fail 5352 } 5353 attr2vec = vattr.ptr; 5354 if (attr2vec->val.did != d_ic_attr_functor) { 5355 /* IC attribute of second var is not correct structure! */ 5356 Fail 5357 } 5358 5359 /* We now have a validated IC attribute for the second variable. */ 5360 5361 if (IsNumber(tterm)) { 5362 /* First var is a ground number. */ 5363 return unify_number_ic(vterm, tterm, attr2vec); 5364 } else if (IsRef(tterm)) { 5365 /* First var is a variable (and we're promised it's meta). */ 5366 IC_Var_Get_Attr(vterm.ptr, attr1); 5367 if (IsRef(attr1->tag)) { 5368 /* 5369 ** First var has no IC attribute, so just give it the 5370 ** one from the second variable. 5371 */ 5372 Bind_Var(attr1->val, attr1->tag, attr2vec, TCOMP); 5373 notify_constrained(vterm.ptr); 5374 } else { 5375 if (!IsStructure(attr1->tag)) { 5376 /* IC attribute of first var is not a structure! */ 5377 Fail 5378 } 5379 attr1vec = attr1->val.ptr; 5380 if (attr1vec->val.did != d_ic_attr_functor) { 5381 /* IC attribute of first var is not correct structure! */ 5382 Fail 5383 } 5384 5385 /* Have to merge attributes from both vars. */ 5386 return unify_ic_ic(attr1vec, attr2vec, vterm, tterm, 5387 vsusp_attr, tsusp_attr); 5388 } 5389 } else { 5390 /* First var is neither a number or a variable. */ 5391 Fail 5392 } 5393 5394 Succeed 5395} 5396 5397 5398/*---------------------------------------------------------------------- 5399** 5400** indomain/1 5401** 5402*/ 5403 5404 /* 5405 ** Give range error unless bounds are in the floating point range where 5406 ** integers are exactly representable _and_ the bounds can be 5407 ** represented as normal integers (rather than bignums). 5408 ** (Actually, for simplicity we restrict it to the valid range for 5409 ** bitmaps.) 5410 */ 5411int 5412p_indomain_init(value vx, type tx, value vlo, type tlo) 5413{ 5414 pword *attr; 5415 pword *tmp; 5416 word lo; 5417 5418 /* If it's already a ground integer, nothing to do. */ 5419 if (IsInteger(tx)) { 5420 /* Return_Unify_Integer(vlo, tlo, vx.nint) */ 5421 Succeed 5422 } 5423 5424 if (!IsMeta(tx)) { 5425 /* Not a variable or no attributes. */ 5426 Bip_Error(TYPE_ERROR) 5427 } 5428 IC_Var_Get_Attr(vx.ptr, attr); 5429 if (IsRef(attr->tag)) { 5430 /* No IC attribute. */ 5431 Bip_Error(TYPE_ERROR) 5432 } 5433 /* Get the attribute's vector. */ 5434 attr = attr->val.ptr; 5435 Dereference(attr); 5436 5437 tmp = attr + OFF_TYPE; 5438 Dereference(tmp); 5439 if (!Type_Is_Int(tmp->val.did)) { 5440 /* Not an integer IC variable. */ 5441 Bip_Error(TYPE_ERROR) 5442 } 5443 5444 /* 5445 ** Check for whether the lower bound is too small (or large) to make 5446 ** integer labelling sensible. We don't worry about the upper bound 5447 ** being too large, so that indomain/1 can be called for variables 5448 ** with (for example) an infinite upper bound. 5449 */ 5450 tmp = attr + OFF_LO; 5451 Dereference(tmp); 5452 if (Dbl(tmp->val) < MIN_BITMAP_RANGE 5453 || Dbl(tmp->val) > MAX_BITMAP_RANGE) { 5454 Bip_Error(RANGE_ERROR) 5455 } 5456 lo = (word) Dbl(tmp->val); 5457 5458 Return_Unify_Integer(vlo, tlo, lo) 5459} 5460 5461 5462 /* Assumes X has already been vetted by p_indomain_check (but may */ 5463 /* have become ground since). */ 5464 /* Try gives the next suggested integer to try. */ 5465int 5466p_indomain_try(value vx, type tx, value vtry, type ttry) 5467{ 5468 var_info vi; 5469 word try; 5470 word xl; 5471 word result; 5472 5473 if (!IsRef(tx)) { 5474 /* If it's ground already, nothing to do. */ 5475 Cut_External 5476 Succeed 5477 } 5478 5479 get_var_info(vx.ptr, &vi); 5480 5481 try = vtry.nint; 5482 5483 if (try > MAX_BITMAP_RANGE) { 5484 Bip_Error(RANGE_ERROR) 5485 } 5486 5487 if (!IsAtom(vi.bitmap->tag)) { 5488 /* If we have a bitmap, use that to choose the next value to try. */ 5489 result = next_greater_member(vi.bitmap->val.wptr, try - 1, &try); 5490 if (Result_Is_Empty(result)) { 5491 /* No remaining entry in bitmap. */ 5492 Cut_External 5493 Fail 5494 } 5495 } else { 5496 /* Make sure we don't try anything smaller than the lower bound. */ 5497 xl = (word) vi.tb.b.l; 5498 if (xl > try) { 5499 try = xl; 5500 } 5501 } 5502 5503 /* Don't leave choice point if this is the last value. */ 5504 /* Careful: upper bound may be too large to safely cast to a word. */ 5505 if (vi.tb.b.u <= MAX_BITMAP_RANGE && try == (word) vi.tb.b.u) { 5506 Cut_External 5507 } else { 5508 value v; 5509 v.nint = try+1; 5510 Remember(2, v, ttry) 5511 } 5512 5513 Return_Unify_Integer(vx, tx, try) 5514} 5515 5516 5517