00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050
00051
00052
00053
00054
00055
00056
00057
00058
00059 #ifndef SCV_CONSTRAINT_H
00060 #define SCV_CONSTRAINT_H
00061
00062
00063 #include "scv/scv_introspection.h"
00064
00065 #include "scv/scv_report.h"
00066 #include <string.h>
00067
00068
00069
00070
00071
00072
00073
00074 class BDD;
00075 class Cudd;
00076 class BDDvector;
00077 struct DdNode;
00078
00079 typedef BDD bddNodeT;
00080 typedef Cudd bddManagerT;
00081 typedef BDDvector bddVectorT;
00082 typedef DdNode ddNodeT;
00083
00084
00085 class _scv_constraint_manager;
00086 class _scv_expr;
00087
00088 #define MAX_MESSAGE_SIZE 1024
00089 #define SIZE_HINT 100000
00090
00091
00092
00093
00094
00095 class _scv_hash {
00096 unsigned long ** _factor;
00097 public:
00098 _scv_hash()
00099 : _factor(new unsigned long * [sizeof(void*)])
00100 {
00101 unsigned long b = 1;
00102 for (int i = sizeof(void*)-1; i>=0 ; i--) {
00103 _factor[i] = new unsigned long [256];
00104 for (int j = 0; j<256; j++) {
00105 _factor[i][j] = b*j;
00106 b *= 131;
00107 }
00108 }
00109 }
00110 ~_scv_hash() {
00111 for (unsigned i = 0; i<sizeof(void*); i++)
00112 delete[] _factor[i];
00113 delete[] _factor;
00114 }
00115 unsigned long operator()(const void * key) const {
00116 unsigned char * byteP = (unsigned char *) &key;
00117 unsigned long sum;
00118 sum = 0;
00119 for (int i = sizeof(void*)-1; i>=0; i--) {
00120 sum += _factor[i][*byteP++];
00121 }
00122 return sum;
00123 }
00124 };
00125
00126
00127
00128
00129 static bool isPrime(unsigned long n) {
00130 unsigned long i = 3;
00131 if ( n < 3 ) return true;
00132 if ( n % 2 == 0 ) return false;
00133 while( i * i <= n ) {
00134 if( n % i == 0 ) return false;
00135 i += 2;
00136 }
00137 return true;
00138 }
00139
00140 static unsigned long nextPrime(unsigned long n) {
00141 while( !isPrime(n) ) n++;
00142 return n;
00143 }
00144
00145
00146
00147
00148 template <class eltT>
00149 class _scv_open_table {
00150 class bucketT {
00151 public:
00152 const void * _key;
00153 eltT _element;
00154 bucketT * _nextP;
00155 bucketT(const void * key, const eltT& element, bucketT * nextP)
00156 : _key(key), _element(element), _nextP(nextP) {}
00157 bool update(const void * key, const eltT& element) {
00158 if (_key == key) { _element = element; return true; }
00159 if (_nextP) return _nextP->update(key,element);
00160 return false;
00161 }
00162 bool get(const void * key, eltT *& elementP) {
00163 if (_key == key) { elementP = &_element; return true; }
00164 if (_nextP) return _nextP->get(key,elementP);
00165 return false;
00166 }
00167 bool removeNextBucket(const void * key) {
00168 if (_nextP && _nextP->_key == key) {
00169 bucketT * matchP = _nextP;
00170 _nextP = _nextP->_nextP;
00171 delete matchP;
00172 return true;
00173 }
00174 if (_nextP) return _nextP->removeNextBucket(key);
00175 return false;
00176 }
00177 static void remove(bucketT * chainP) {
00178 if (chainP) {
00179 remove(chainP->_nextP);
00180 delete chainP;
00181 }
00182 }
00183 #if 0
00184 inline static tb_memory_manager& _mm() { static tb_memory_manager mm(sizeof(bucketT)); return mm; }
00185 inline static void * operator new(size_t size, void * p) { return p; }
00186 inline static void * operator new(size_t size) { return _mm().alloc(size); }
00187 inline static void operator delete(void *p, size_t size) { _mm().free(p,size); }
00188 #endif
00189 };
00190 _scv_hash _hash;
00191 unsigned long _numElts;
00192 unsigned long _numBuckets;
00193 bucketT ** _arrayP;
00194 public:
00195 _scv_open_table(long sizeHint)
00196 : _hash(),
00197 _numElts(0),
00198 _numBuckets(nextPrime(sizeHint)),
00199 _arrayP(new bucketT*[_numBuckets])
00200 {
00201 for (unsigned long i=0; i<_numBuckets; ++i) {
00202 _arrayP[i] = NULL;
00203 }
00204 }
00205 ~_scv_open_table() {
00206 reset();
00207 delete[] _arrayP;
00208 }
00209 inline long numElts() const { return _numElts; }
00210 inline long numBuckets() const { return _numBuckets; }
00211
00212 inline void reset() {
00213 for (unsigned long i=0; i<_numBuckets; ++i) {
00214 bucketT::remove(_arrayP[i]);
00215 _arrayP[i] = NULL;
00216 }
00217 _numElts = 0;
00218 }
00219 inline bool remove(const void * key) {
00220 if (_remove(key)) { --_numElts; return true; }
00221 return false;
00222 }
00223 inline bool _remove(const void * key) {
00224 long location = _hash(key) % _numBuckets;
00225 if (_arrayP[location]) {
00226 if (_arrayP[location]->_key == key) {
00227 bucketT * matchP = _arrayP[location];
00228 _arrayP[location] = matchP->_nextP;
00229 delete matchP;
00230 return true;
00231 } else {
00232 return _arrayP[location]->removeNextBucket(key);
00233 }
00234 } else {
00235 return false;
00236 }
00237 }
00238
00239 inline bool update(const void * key, const eltT& element) {
00240 long location = _hash(key) % _numBuckets;
00241 if (_arrayP[location] && _arrayP[location]->update(key,element))
00242 return true;
00243 else {
00244 _arrayP[location] = new bucketT(key, element, _arrayP[location]);
00245 ++_numElts;
00246 return false;
00247 }
00248 }
00249 inline bool get(const void * key, eltT *& elementP) {
00250 long location = _hash(key) % _numBuckets;
00251 if (_arrayP[location]) {
00252 return _arrayP[location]->get(key,elementP);
00253 } else {
00254 return false;
00255 }
00256 }
00257 };
00258
00259 class scv_constraint_base;
00260
00261
00262
00263
00264
00265
00266
00267
00268
00269
00270
00271
00272
00273 class scv_constraint_manager {
00274 friend void scv_constraint_startup();
00275 static _scv_constraint_manager *globalConstraintManagerP;
00276 public:
00277 static void set_value(scv_extensions_if* s, bddNodeT* b, _scv_constraint_data * cdata_);
00278 static void set_value(scv_constraint_base* c, bool simplify=false);
00279 static bddNodeT& get_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint);
00280 static void init_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint);
00281 static void init_maxvar(const scv_expression & he, const scv_expression &se);
00282 static void reset(void);
00283 static void wrapup(scv_extensions_if* s, void *argP);
00284 static _scv_constraint_manager * getConstraintManagerP(void);
00285 static void add_extension(scv_extensions_if* s);
00286 };
00287
00288
00289
00290
00291
00292
00293
00294
00295
00296 class _scv_expr {
00297 public:
00298 typedef enum valueType {
00299 EMPTY,
00300 INT,
00301 UNSIGNED,
00302 SC_BV_BASE,
00303 BOOLEAN,
00304 DOUBLE,
00305 STRING,
00306 UNSIGNED_64BIT,
00307 BDD,
00308 BDDVECTOR,
00309 BDDVECTOR_SIGNED,
00310 DOUBLE_VAR,
00311 STRING_VAR,
00312 RECORD,
00313 ARRAY
00314 } ExprValueType;
00315 private:
00316 ExprValueType type;
00317 union {
00318 long long ivalue;
00319 unsigned long long uvalue;
00320 bool bvalue;
00321 double dvalue;
00322 char* cvalue;
00323 bddNodeT* bdd;
00324 bddVectorT* bddvec;
00325 scv_extensions_if* ext;
00326 } value;
00327 scv_shared_ptr<sc_bv_base> sc_data;
00328 int vecsize;
00329 int sigLsb;
00330 int sigMsb;
00331 int isVar;
00332 int bit_width;
00333 public:
00334 _scv_expr();
00335 _scv_expr(const _scv_expr& other);
00336 ~_scv_expr();
00337 public:
00338 void setType(ExprValueType type);
00339 void setBddNodeP(bddNodeT*);
00340 void setIntValue(long long);
00341 void setUnsignedValue(unsigned long long);
00342 void setBigValue(sc_bv_base& v, int bw);
00343 void setBooleanValue(bool);
00344 void setDoubleValue(double);
00345 void setStringValue(const char*);
00346 void setBddVectorP(bddVectorT*);
00347 void setExtensionP(scv_extensions_if*);
00348 void setVecSize(int s);
00349 void setBitWidth(int bit_width);
00350 void setSigWidth(int lsb, int msb);
00351 void setSigLsb(int lsb);
00352 void setSigMsb(int msb);
00353 void setIsVar(void) {
00354 isVar = 1;
00355 };
00356 const ExprValueType get_type(void) const;
00357 bddNodeT* getBddNodeP(void) const;
00358 long long getIntValue(void) const;
00359 unsigned long long getUnsignedValue(void) const;
00360 bool getBoolValue(void) const;
00361 double getDoubleValue(void) const;
00362 sc_bv_base getBigValue(void) const;
00363 char* getStringValue(void) const;
00364 bddVectorT* getBddVectorP(void) const;
00365 scv_extensions_if* getExtensionP(void) const;
00366 int getVecSize(void) const;
00367 int getBitWidth(void) const;
00368 int getSigLsb(void) const;
00369 int getSigMsb(void) const;
00370 int isConstant(void) const {
00371 return (type == UNSIGNED || type == UNSIGNED_64BIT ||
00372 type == DOUBLE || type == INT || type == BOOLEAN ||
00373 type == SC_BV_BASE);
00374 };
00375 int isBddVector(void) const {
00376 return (type == BDDVECTOR || type == BDDVECTOR_SIGNED);
00377 };
00378 int isBdd(void) const {
00379 return (type == BDD);
00380 };
00381 int isRecord(void) const {
00382 return (type == RECORD);
00383 }
00384 int isArray(void) const {
00385 return (type == ARRAY);
00386 }
00387 int isSigned(void) const {
00388 return (type == BDDVECTOR_SIGNED);
00389 }
00390 int isVarExpr(void) const {
00391 return isVar;
00392 }
00393 int isDouble(void) const {
00394 return (type == DOUBLE_VAR);
00395 }
00396 int isString(void) const {
00397 return (type == STRING_VAR);
00398 }
00399 int isEmpty(void) const {
00400 return (type == EMPTY);
00401 }
00402 public:
00403 _scv_expr& operator=(const _scv_expr& rhs);
00404 };
00405
00406 void _scv_remove(_scv_expr* e);
00407
00408
00409
00410
00411
00412
00413 class _smartDataRecordT {
00414 public:
00415 _scv_expr * smartDataBddVector;
00416
00417 int startIndex;
00418 int numvar;
00419 int bSize;
00420 public:
00421 _smartDataRecordT() {
00422 bSize = 0;
00423 startIndex = 0;
00424 numvar = 0;
00425 smartDataBddVector = NULL;
00426 }
00427 ~_smartDataRecordT() {
00428 if (smartDataBddVector) {
00429 _scv_remove(smartDataBddVector);
00430 }
00431 }
00432 };
00433
00434
00435
00436
00437
00438
00439 class _nodeRecordT {
00440 public:
00441 double pthenBranch;
00442 double pelseBranch;
00443 double nodeWeight;
00444 int wasVisited;
00445 public:
00446 _nodeRecordT() {
00447 pthenBranch = 0;
00448 pelseBranch = 0;
00449 nodeWeight = 0;
00450 wasVisited = 0;
00451 }
00452 ~_nodeRecordT() {}
00453 };
00454
00455
00456
00457
00458
00459
00460
00461
00462
00463
00464
00465
00466
00467
00468
00469
00470
00471
00472
00473 #define ROUNDTO 65536
00474 #define ROUNDTO_BASE 32768
00475
00476 class _scv_constraint_manager
00477 {
00478 private:
00479 bddManagerT* _mgr;
00480 scv_shared_ptr<scv_random> _gen;
00481
00482 _scv_open_table<int> *nodeHashP;
00483 _scv_associative_array<ddNodeT*, double> *nodeWeightHash;
00484 _scv_associative_array<ddNodeT*, int> *wasVisited;
00485
00486 _scv_open_table<_smartDataRecordT> *extHash;
00487 _scv_associative_array<scv_extensions_if*, int> *countExtHash;
00488 _scv_associative_array<scv_constraint_base*, bddNodeT*> *avoidDuplicateHash;
00489 _scv_associative_array<scv_extensions_if*, bddNodeT*> *avoidDuplicateExtHash;
00490 list<scv_extensions_if*>* enumVarList;
00491
00492 _scv_expr* exprRepZero;
00493 _scv_expr* exprRepOne;
00494 int maxTime;
00495
00496 int maxMemory;
00497
00498 int verboseLevel;
00499
00500 int nthvar;
00501 int maxvar;
00502 int numBddVar;
00503 int maxNumBits;
00504 int multiple;
00505 int iteration;
00506 int numBitsUnsigned;
00507 int numBitsSigned;
00508 int numBitsUInt64T;
00509 int *eProb;
00510 unsigned* valueIndex;
00511 scv_extensions_if::mode_t mode;
00512 unsigned randomnext;
00513 DdNode* oneNode;
00514 DdNode* zeroNode;
00515 public:
00516 _scv_constraint_manager();
00517 ~ _scv_constraint_manager();
00518 public:
00519 friend void _scv_set_value(scv_extensions_if* e, scv_constraint_base* c, scv_shared_ptr<scv_random> g);
00520 friend void _scv_set_value(scv_extensions_if* e, _scv_constraint_data* cdata_);
00521 friend bddNodeT& _scv_bdd_and(bddNodeT& bh, bddNodeT& bs, const scv_constraint_base* c);
00522 bddNodeT& get_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint);
00523 void init_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint);
00524 void countMaxVar(const scv_expression& e);
00525 void add_sparse_var(scv_extensions_if* e, bddNodeT* b);
00526 void check_sparse_var(scv_constraint_base* c, bddNodeT* b);
00527 void reset(void);
00528 bddManagerT* getManagerP(void) {return _mgr;}
00529 void assignRandomValue(scv_extensions_if* s, bddNodeT* argP, _scv_constraint_data* cdata_);
00530 void assignRandomValue(scv_extensions_if* s, bddNodeT* argP, scv_shared_ptr<scv_random> g);
00531 void assignRandomValue(scv_constraint_base* c, bool simplify);
00532 void wrapup(scv_extensions_if* s);
00533 void add_extension(scv_extensions_if* s);
00534 bool has_complex_constraint(scv_extensions_if* s);
00535 private:
00536 _scv_expr assignValueMember(scv_extensions_if* s, bool ad);
00537 _scv_expr simplifyMember(scv_extensions_if* s, _scv_expr t, scv_constraint_base* c,
00538 bool& remove_, bool& over_constraint);
00539 void initMember(scv_extensions_if* s);
00540 bddNodeT* simplifyConstraint(scv_constraint_base* c, bool& remove_, bddNodeT* b=NULL);
00541 _scv_expr simplifyField(_scv_expr e, scv_extensions_if* s, bool& remove_);
00542 void setDoubleValue(scv_extensions_if* e, scv_constraint_base * c, scv_shared_ptr<scv_random> g);
00543 void generateWeight(bddNodeT* b);
00544 double getWeightNode(ddNodeT* node);
00545 void setRandomGen(scv_shared_ptr<scv_random> g) {_gen = g; randomnext = 0;}
00546 bool isOverConstrained(const _scv_expr& e);
00547 scv_shared_ptr<scv_random> getRandomGenP(void) const{return _gen;}
00548 _scv_expr getConstantExprRep(_scv_expr e, int signExtend=-1) const;
00549 _scv_expr getExpressionRep(const scv_expression& e);
00550 void initExpression(const scv_expression& e);
00551 _scv_expr getExprRepZero(void);
00552 _scv_expr getExprRepOne(void);
00553 _scv_expr exprAnd(const _scv_expr& e1, const _scv_expr& e2);
00554 _scv_expr _exprAnd(const _scv_expr& e1, const _scv_expr& e2);
00555 _scv_expr exprOr(const _scv_expr& e1, const _scv_expr& e2);
00556 _scv_expr _exprOr(const _scv_expr& e1, const _scv_expr& e2);
00557 _scv_expr exprNot(const _scv_expr& e1);
00558 _scv_expr _exprNot(const _scv_expr& e1);
00559 _scv_expr exprPlus(const _scv_expr& e1, const _scv_expr& e2);
00560 _scv_expr _exprPlus(const _scv_expr& e1, const _scv_expr& e2);
00561 _scv_expr exprMinus(const _scv_expr& e1, const _scv_expr& e2);
00562 _scv_expr _exprMinus(const _scv_expr& e1, const _scv_expr& e2);
00563 _scv_expr exprMultiply(const _scv_expr& e1, const _scv_expr& e2);
00564 _scv_expr _exprMultiply(const _scv_expr& e1, const _scv_expr& e2);
00565 _scv_expr exprEqual(const _scv_expr& e1, const _scv_expr& e2);
00566 _scv_expr _exprEqual(const _scv_expr& e1, const _scv_expr& e2);
00567 _scv_expr exprNEqual(const _scv_expr& e1, const _scv_expr& e2);
00568 _scv_expr exprGThan(const _scv_expr& e1, const _scv_expr& e2);
00569 _scv_expr exprLThan(const _scv_expr& e1, const _scv_expr& e2);
00570 _scv_expr exprGEq(const _scv_expr& e1, const _scv_expr& e2);
00571 _scv_expr exprLEq(const _scv_expr& e1, const _scv_expr& e2);
00572 _scv_expr _exprLEq(const _scv_expr& e1, const _scv_expr& e2);
00573 _scv_expr twosCompliment(const _scv_expr& e);
00574 _scv_expr getBasicEnumConstraint(void);
00575 _scv_expr createExprRep(long long v, int bit_width);
00576 _scv_expr createExprRep(unsigned long long v, int bit_width);
00577 _scv_expr createExprRep(sc_bv_base& v, int bit_width);
00578 _scv_expr createExprRep(bool v, int bit_width);
00579 _scv_expr createExprRep(double v);
00580 _scv_expr createExprRep(const char* v);
00581 _scv_expr createExprRep(scv_extensions_if* s);
00582 void checkExprRep(scv_extensions_if* s);
00583 _scv_expr createBddVec(int msize);
00584
00585 void setExprRep(scv_extensions_if* s, _scv_expr& e);
00586 _scv_expr* getExprRepP(scv_extensions_if* s) const;
00587
00588 int getVecSize(scv_extensions_if* s) const;
00589 unsigned getStartIndex(scv_extensions_if* s) const;
00590 unsigned getEndIndex(scv_extensions_if* s) const;
00591 int getSizeOfBddVec(_scv_expr& e) const;
00592 int getSizeOfBddVec(scv_extensions_if* s) const;
00593
00594 void getVectorFromBdd(ddNodeT*);
00595 void getVector(_scv_expr e, unsigned* v) const;
00596 void setValue(scv_extensions_if* s, int starti, int msize, int numvar);
00597 template<typename T>
00598 void _setValue(T value, scv_extensions_if* s, int starti, int msize, int numvar);
00599 void _setBigValue(scv_extensions_if* s, int starti, int msize, int numvar);
00600
00601 void updateRandomNext(void) {
00602 if (mode == scv_extensions_if::SCAN) {
00603 randomnext = randomnext >> 1;
00604 } else {
00605 randomnext = randomnext >> 1;
00606 if (randomnext==0) {
00607 randomnext = getRandomGenP()->next();
00608 }
00609 }
00610 }
00611 void update16BitValue(void) {
00612 if (randomnext <= ROUNDTO) {
00613 randomnext = getRandomGenP()->next();
00614 } else {
00615 randomnext = randomnext >> 16;
00616 }
00617 }
00618 };
00619
00620
00622
00623
00624
00625
00626
00627
00629
00630 class scv_constraint_base;
00631 extern bddNodeT& _scv_bdd_and(bddNodeT& bh, bddNodeT& bs, const scv_constraint_base* c);
00632
00633 class scv_constraint_base : public scv_object_if {
00634 public:
00635 scv_constraint_base();
00636 virtual ~scv_constraint_base();
00637 public:
00638
00639
00640
00641
00642
00643
00644 virtual void next();
00645
00646
00647
00648
00649
00650
00651
00652
00653
00654
00655
00656 void set_mode(scv_extensions_if::mode_t m);
00657
00658
00659 scv_extensions_if::mode_t get_mode(void) const;
00660
00661
00662 void set_random(scv_shared_ptr<scv_random> g);
00663
00664
00665 scv_shared_ptr<scv_random> get_random(void);
00666
00667
00668 void get_members(list<scv_smart_ptr_if*>& vlist);
00669
00670 public:
00671 const char *get_name() const;
00672 const string& get_name_string() const;
00673 virtual const char *kind() const;
00674 void print(ostream& o=scv_out, int details=0, int indent=0) const;
00675 virtual void show(int details=0, int indent=0) const;
00676 static int get_debug();
00677 static void set_debug(int i);
00678
00679 protected:
00680
00681
00682 virtual scv_expression get_constraint() const;
00683
00684
00685 virtual scv_expression get_soft_constraint() const;
00686
00687 private:
00688
00689
00690
00691 void uninitialize();
00692
00693
00694
00695 void initialize();
00696
00697
00698 void set_up_members(list<scv_smart_ptr_if*>& members);
00699
00700
00701
00702 virtual scv_constraint_base* get_copy(scv_constraint_base * from);
00703
00704
00705 virtual bddNodeT& get_bdd();
00706
00707
00708 virtual void init_bdd() ;
00709
00710
00711 virtual scv_expression& eh() const;
00712
00713
00714 virtual scv_expression& es() const;
00715
00716
00717 virtual scv_expression& ebh() const;
00718
00719
00720 virtual scv_expression& ebs() const;
00721
00722
00723 void ignore_soft_constraint(void);
00724
00725
00726 bool is_ignored_soft_constraint(void);
00727
00728
00729 int get_scan_counter(void);
00730
00731
00732 void set_expression_string(const char * e, bool hard_constraint);
00733
00734
00735 list<scv_smart_ptr_if*>& get_members(void);
00736
00737
00738 private:
00739 friend class _scv_constraint_manager;
00740 friend void _scv_pop_constraint();
00741 friend scv_extensions_if * _scv_find_extension(scv_constraint_base * c,
00742 scv_extensions_if* e);
00743 friend void _scv_copy_values(scv_constraint_base* to,
00744 scv_constraint_base* from);
00745 friend scv_constraint_base * _scv_new_constraint(
00746 scv_constraint_base * from);
00747
00748 private:
00749 list<scv_smart_ptr_if*> pointers_;
00750 scv_shared_ptr<scv_random> gen_;
00751 scv_extensions_if::mode_t mode_;
00752 static int debug_;
00753 int scan_counter_;
00754 protected:
00755 bool ignore_;
00756 string name_;
00757 string _hard_constraints;
00758 string _soft_constraints;
00759 };
00760
00761
00762 #define GET_BDD() \
00763 static bddNodeT& d = get_bdd(); \
00764 if (0) cout << &d << endl;
00765
00767
00768
00769
00770
00771
00773
00774 #define SCV_CONSTRAINT_CTOR(class_name) \
00775 protected: \
00776 class_name() { init(); } \
00777 public: \
00778 class_name(const char* name) { name ? name_ = name : name = "<anonymous>"; \
00779 _scv_pop_constraint(); init(); init_bdd(); GET_BDD(); next();} \
00780 virtual const char *kind() const { \
00781 static const char *name = #class_name; return name; } \
00782 private: \
00783 virtual void init_bdd() { \
00784 scv_constraint_manager::init_maxvar(class_name::get_constraint(), \
00785 class_name::get_soft_constraint()); \
00786 scv_constraint_manager::init_bdd(class_name::get_constraint(), this, true); \
00787 scv_constraint_manager::init_bdd(class_name::get_soft_constraint(), this, false); \
00788 } \
00789 virtual bddNodeT& get_bdd() { \
00790 static bddNodeT& bh = scv_constraint_manager::get_bdd( \
00791 class_name::get_constraint(), this, true); \
00792 static bddNodeT& bs = scv_constraint_manager::get_bdd( \
00793 class_name::get_soft_constraint(), this, false); \
00794 static bddNodeT& b = _scv_bdd_and(bh, bs, this); \
00795 if (ignore_) return bh; else return b; } \
00796 virtual scv_expression& eh() const { static scv_expression e; return e; } \
00797 virtual scv_expression& es() const { static scv_expression e; return e; } \
00798 virtual scv_expression& ebh() const { static scv_expression e; return e; } \
00799 virtual scv_expression& ebs() const { static scv_expression e; return e; } \
00800 virtual scv_constraint_base* get_copy(scv_constraint_base * from) { \
00801 scv_constraint_base* obj = new class_name("class_name"); \
00802 _scv_copy_values(obj, from); \
00803 return obj; \
00804 } \
00805 protected: \
00806 virtual scv_expression get_constraint() const { \
00807 return class_name::eh() && class_name::ebh(); } \
00808 virtual scv_expression get_soft_constraint() const { \
00809 return class_name::es() && class_name::ebs(); } \
00810 private: \
00811 bool init() { \
00812 eh() = es() = ebh() = ebs() = true; \
00813 init_core(); return true; \
00814 } \
00815 void init_core() \
00816
00817 #define SCV_CONSTRAINT(expr) eh() &= expr;
00818
00819 #define SCV_SOFT_CONSTRAINT(expr) es() &= expr;
00820
00821 #define SCV_BASE_CONSTRAINT(base_class) \
00822 ebh() &= base_class::get_constraint(); \
00823 ebs() &= base_class::get_soft_constraint(); \
00824
00825
00827
00828
00829
00831
00832 public:
00833 static void notImplementedYet(const char * messageP) {
00834 _scv_message::message(_scv_message::CONSTRAINT_ERROR_NOTIMPLEMENTED,
00835 messageP);
00836 }
00837 static void ignoreDoubleConstraints(void);
00838 static void ignoreStringConstraints(void);
00839 static void internalError(const char * messageP) {
00840 _scv_message::message(_scv_message::CONSTRAINT_ERROR_INTERNAL,
00841 messageP);
00842 }
00843 static void cannotMeetConstraint(const string name) {
00844 _scv_message::message(_scv_message::CONSTRAINT_ERROR_OVER_CONSTRAINED,
00845 name.c_str());
00846 }
00847 static void ignoredLevel(const string name) {
00848 _scv_message::message(_scv_message::CONSTRAINT_WARNING_IGNORE_SOFT_CONSTRAINT,
00849 name.c_str());
00850 }
00851 static void internalWarning(const char * messageP, const char * name) {
00852 _scv_message::message(_scv_message::CONSTRAINT_WARNING_EQUAL_4_STATE,
00853 messageP, name);
00854 }
00855 static void typeCheckError(const char * messageP) {
00856 _scv_message::message(_scv_message::CONSTRAINT_EXPRESSION_TYPEMISMATCHED,
00857 messageP);
00858 }
00859 };
00860
00861 extern void scv_constraint_startup();
00862
00863 #endif
00864
00865
00866