- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ValidSAT/VSATNode.cpp

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00009 // Organization:        Model-based Embedded and Robotic Systems Group
    00010 //                                      Massachusetts Institute of Technology
    00011 //
    00013
    00014 #include "VSATNode.h"
    00015
    00017
    00018 using namespace Mers::Solvers::SAT::ValidSAT;
    00019 using Mers::Models::Base::BaseModelAssignment;
    00020 using Mers::Models::Base::BaseModelAssignmentArray;
    00021 using Mers::Models::Base::BaseModelSentence;
    00022 using Mers::Models::Base::BaseModelClause;
    00023 using Mers::Utils::Containers::DynamicArrayTemplate;
    00024 using std::cout;
    00025 using std::cerr;
    00026 using std::endl;
    00027
    00029 // Construction/Destruction
    00031
    00032 VSATNode::VSATNode(DynamicArrayTemplate<VSATVariable> const &myVariables,
    00033         BaseModelSentence const &myConstraint, bool myTestForValid)
    00034         : domains(true), allVariables(false), unassignedVariables(false),
    00035         constraints(myConstraint.getSentenceType(), true),
    00036         validAssignment(false), unsatAssignment(false),
    00037         debug(0)
    00038 {
    00039         unsigned int x;
    00040
    00041         testForValid = myTestForValid;
    00042         notValid = false;
    00043         solutionStatus = Unknown;
    00044         for(x = 0; x < myVariables.getLength(); x++){
    00045                 unassignedVariables.pushBack((VSATVariable *)myVariables[x]);
    00046                 allVariables.pushBack((VSATVariable *)myVariables[x]);
    00047         }
    00048         if(FAILED(unassignedVariableIndex.resize(allVariables.getLength()))){
    00049                 fprintf(stderr, "Error, unable to allocate the variable index\n");
    00050         }else{
    00051                 for(x = 0; x < unassignedVariableIndex.getLength(); x++){
    00052                         unassignedVariableIndex[x] = x;
    00053                 }
    00054         }
    00055         constraints.resize(myConstraint.getLength());
    00056         for(x = 0; x < myConstraint.getLength(); x++){
    00057                 BaseModelClause const &lcu = *(myConstraint[x]);
    00058                 BaseModelClause * vcu =
    00059                         new BaseModelClause(lcu.getClauseType(), false);
    00060                 constraints[x] = vcu;
    00061
    00062                 for(unsigned int a = 0; a < lcu.getLength(); a++){
    00063                         vcu->pushBack((BaseModelAssignment *)lcu[a]);
    00064                 }
    00065         }
    00066         domains.resize(allVariables.getLength());
    00067         for(x = 0; x < domains.getLength(); x++){
    00068                 BaseModelAssignmentArray &asgs = allVariables[x]->getAssignments();
    00069                 BaseModelAssignmentArray * vaa = new BaseModelAssignmentArray(false);
    00070                 domains[x] = vaa;
    00071
    00072                 for(unsigned int a = 0; a < asgs.getLength(); a++){
    00073                         vaa->pushBack(asgs[a]);
    00074                 }
    00075         }
    00076         numberOfExpandedNodes = 1;
    00077         // note that we do not want to unit propogate here since that
    00078         // might mark the whole thing as notValid even when we include
    00079         // the unit propogated values in our solution, which is undesirable
    00080 }
    00081
    00083
    00084 VSATNode::VSATNode(VSATNode const &other)
    00085         : domains(other.domains),
    00086         allVariables(other.allVariables),
    00087         unassignedVariableIndex(other.unassignedVariableIndex),
    00088         unassignedVariables(other.unassignedVariables),
    00089         constraints(other.constraints),
    00090         validAssignment(other.validAssignment), unsatAssignment(other.unsatAssignment),
    00091         debug(other.debug)
    00092 {
    00093         // we don't inherit notValid from our parents
    00094         notValid = false;
    00095
    00096         testForValid = other.testForValid;
    00097         solutionStatus = other.solutionStatus;
    00098         numberOfExpandedNodes = 1;
    00099 }
    00100
    00102
    00103 VSATNode::~VSATNode()
    00104 {
    00105 }
    00106
    00108
    00109 void VSATNode::addConstraint(BaseModelClause const * newConstraint)
    00110 {
    00111         BaseModelClause * clause =
    00112                 new BaseModelClause(newConstraint->getClauseType(), false);
    00113
    00114         for(unsigned int a = 0; a < newConstraint->getLength(); a++){
    00115                 clause->pushBack((BaseModelAssignment *)(*newConstraint)[a]);
    00116         }
    00117         constraints.pushBack(clause);
    00118 }
    00119
    00121
    00122 void VSATNode::propagate(BaseModelAssignment const &asg, bool positive,
    00123         bool ignoreConstraint, bool unitPropagate)
    00124 {
    00125         unsigned int x;
    00126         unsigned int varUID = asg.getVariable()->getUID();
    00127         VSATVariable * var = allVariables[varUID];
    00128         // get our domain and make sure this variable isn't already assigned
    00129         unsigned int uaVarIndex = unassignedVariableIndex[varUID];
    00130
    00131         if(uaVarIndex >= unassignedVariables.getLength()){
    00132                 // propagating a known variable
    00133                 if(positive != (asg == *((*(domains[varUID]))[0]))){
    00134                         // inconsistent
    00135                         solutionStatus = Unsatisfiable;
    00136                         validAssignment.makeEmpty();
    00137                 }
    00138                 // in any case, we don't want to process this assignment
    00139                 return;
    00140         }
    00141
    00142         // Find our value
    00143         BaseModelAssignmentArray &varDomain = *(domains[varUID]);
    00144         for(x = 0; x < varDomain.getLength(); x++){
    00145                 if(*(varDomain[x]->getValue()) == *(asg.getValue()))
    00146                         break;
    00147         }
    00148
    00149         if(positive){
    00150                 // reduce the domain
    00151                 {
    00152                         // remove the variable from the unassigned list since it
    00153                         // now has a single value (or NULL)
    00154                         unsigned int lastIndex = unassignedVariables.getLength() - 1;
    00155                         unassignedVariables[uaVarIndex] = unassignedVariables[lastIndex];
    00156                         unsigned int otherVarIndex =
    00157                                 unassignedVariables[uaVarIndex]->getUID();
    00158                         unassignedVariableIndex[otherVarIndex] = uaVarIndex;
    00159                         unassignedVariableIndex[varUID] = lastIndex;
    00160                         unassignedVariables.popBack();
    00161
    00162                         ConditionalDebugOut(debug >= 7,
    00163                                 if(!ignoreConstraint)
    00164                                         cout << "[Unit] ";
    00165                                 cout << "Propagating:  (" << asg.getVariable()->getName() << " = "
    00166                                         << asg.getValue()->getName() << ")" << endl;
    00167                         );
    00168
    00169                         // if we actually found the assignment, it's valid
    00170                         if(x == varDomain.getLength()){
    00171                                 // reducing the domain to the empty set
    00172                                 unsatAssignment.pushBack(varDomain[0]);
    00173                                 validAssignment.makeEmpty();
    00174                                 varDomain.makeEmpty();
    00175                                 solutionStatus = Unsatisfiable;
    00176                                 return;
    00177                         }else{
    00178                                 if(!ignoreConstraint && var->isDesignVariable() &&
    00179                                         varDomain.getLength() > 1){
    00180                                         notValid = true;
    00181                                         // The values being removed form an unsatisfiable assignment,
    00182                                         // so record it now.
    00183                                         if(x != 0)
    00184                                                 unsatAssignment.pushBack(varDomain[0]);
    00185                                         else
    00186                                                 unsatAssignment.pushBack(varDomain[1]);
    00187                                 }
    00188                                 if(x != 0){
    00189                                         varDomain[0] = varDomain[x];
    00190                                 }
    00191                                 varDomain.resize(1);
    00192                         }
    00193                         if(var->isDesignVariable()){
    00194                                 if(!notValid){
    00195                                         // If we're not already unsatisfiable, add some more assignments
    00196                                         unsatAssignment.pushBack(varDomain[0]);
    00197                                 }
    00198                                 // If we're here, we're not unsatisfiable, so add some more assignmens
    00199                                 validAssignment.pushBack(varDomain[0]);
    00200                         }
    00201                 }
    00202
    00203                 // find the applicable assignments
    00204                 for(x = 0; x < constraints.getLength();){
    00205                         BaseModelClause &cu = *(constraints[x]);
    00206                         unsigned int y;
    00207                         bool skip = true;
    00208
    00209                         for(y = 0; y < cu.getLength();){
    00210                                 BaseModelAssignment const * casg = cu[y];
    00211                                 unsigned int cVarUID = casg->getVariable()->getUID();
    00212
    00213                                 if(cVarUID == varUID){
    00214                                         if(casg->assignmentHolds(asg.getValue()->getDouble())){
    00215                                                 // clause is now satisfied
    00216                                                 unsigned int lastIndex = constraints.getLength() - 1;
    00217                                                 constraints[x] = constraints[lastIndex];
    00218                                                 constraints.popBack();
    00219                                                 delete &cu;
    00220                                                 skip = false;
    00221                                                 break;
    00222                                         }else{
    00223                                                 // clause is not satisfied by this, remove
    00224                                                 // this constraint unit
    00225                                                 unsigned int lastIndex = cu.getLength() - 1;
    00226                                                 cu[y] = cu[lastIndex];
    00227                                                 cu.popBack();
    00228                                         }
    00229                                 }else{
    00230                                         y++;
    00231                                 }
    00232                         }
    00233                         if(skip){
    00234                                 if(cu.getLength() == 0){
    00235                                         solutionStatus = Unsatisfiable;
    00236                                         validAssignment.makeEmpty();
    00237                                         return;
    00238                                 }
    00239                                 x++;
    00240                         }
    00241                 }
    00242         }else{ // negative
    00243                 // reduce the domain
    00244                 {
    00245                         // if we didn't find the assignment, it's valid
    00246                         if(x == varDomain.getLength()){
    00247                                 // nothing to reduce, just return
    00248                                 return;
    00249                         }else{
    00250                                 ConditionalDebugOut(debug >= 7,
    00251                                         if(!ignoreConstraint)
    00252                                                 cout << "[Unit] ";
    00253                                         cout << "Propagating:  NOT (" << asg.getVariable()->getName() << " = "
    00254                                                 << asg.getValue()->getName() << ")" << endl;
    00255                                 );
    00256
    00257                                 if(!ignoreConstraint && var->isDesignVariable()){
    00258                                         notValid = true;
    00259                                         // This assignment makes it unsatisfiable
    00260                                         unsatAssignment.pushBack(varDomain[x]);
    00261                                 }
    00262
    00263                                 if(x != varDomain.getLength() - 1){
    00264                                         varDomain[x] = varDomain[varDomain.getLength() - 1];
    00265                                 }
    00266                                 varDomain.popBack();
    00267                                 if(varDomain.getLength() == 0){
    00268                                         // reduced the domain to the empty set
    00269                                         solutionStatus = Unsatisfiable;
    00270                                         validAssignment.makeEmpty();
    00271                                         return;
    00272                                 }else if(varDomain.getLength() == 1){
    00273                                         propagate(*(varDomain[0]), true, ignoreConstraint);
    00274                                         return;
    00275                                 } // otherwise we still have options
    00276                         }
    00277                 }
    00278
    00279                 // find the applicable assignments
    00280                 for(x = 0; x < constraints.getLength();){
    00281                         BaseModelClause &cu = *(constraints[x]);
    00282                         unsigned int y;
    00283                         bool skip = true;
    00284
    00285                         for(y = 0; y < cu.getLength();){
    00286                                 BaseModelAssignment * casg = cu[y];
    00287                                 unsigned int cVarUID = casg->getVariable()->getUID();
    00288
    00289                                 if(cVarUID == varUID){
    00290                                         if(casg->getValue() == asg.getValue()){
    00291                                                 if(cu[y]->getOperator() == BaseModelAssignment::Positive){
    00292                                                         // clause is not satisfied by this, remove
    00293                                                         // this constraint unit
    00294                                                         unsigned int lastIndex = cu.getLength() - 1;
    00295                                                         cu[y] = cu[lastIndex];
    00296                                                         cu.popBack();
    00297                                                 }else{
    00298                                                         // clause is now satisfied
    00299                                                         unsigned int lastIndex = constraints.getLength() - 1;
    00300                                                         constraints[x] = constraints[lastIndex];
    00301                                                         constraints.popBack();
    00302                                                         delete &cu;
    00303                                                         skip = false;
    00304                                                         break;
    00305                                                 }
    00306                                         }else{
    00307                                                 y++;
    00308                                         }
    00309                                 }else{
    00310                                         y++;
    00311                                 }
    00312                         }
    00313                         if(skip){
    00314                                 if(cu.getLength() == 0){
    00315                                         solutionStatus = Unsatisfiable;
    00316                                         validAssignment.makeEmpty();
    00317                                         return;
    00318                                 }
    00319                                 x++;
    00320                         }
    00321                 }
    00322         }
    00323         ConditionalDebugOut(debug >= 10,
    00324                 cout << "Constraints now (" << constraints.getLength() << "):" << endl << constraints << endl;
    00325         );
    00326         if(unitPropagate){
    00327                 // look for unit clauses
    00328                 for(x = 0; x < constraints.getLength();){
    00329                         BaseModelClause &cu = *(constraints[x]);
    00330                         if(cu.getLength() == 1){
    00331                                 BaseModelAssignment &newAsg = *(cu[0]);
    00332                                 bool newPositive = cu[0]->getOperator() ==
    00333                                         BaseModelAssignment::Positive;
    00334
    00335                                 // clause (will now be) satisfied
    00336                                 unsigned int lastIndex = constraints.getLength() - 1;
    00337                                 constraints[x] = constraints[lastIndex];
    00338                                 constraints.popBack();
    00339                                 delete &cu;
    00340                                 propagate(newAsg, newPositive, false);
    00341                                 return;
    00342                         }else{
    00343                                 x++;
    00344                         }
    00345                 }
    00346         }
    00347         if(constraints.getLength() == 0){
    00348                 if(solutionStatus == Unknown){
    00349                         // We're done and need to adjust (don't need to adjust if Unsatisfiable).
    00350                         adjustValidAssignment();
    00351
    00352                         // If we're notValid then we're Satisfiable, otherwise we're valid
    00353                         if(notValid)
    00354                                 solutionStatus = Satisfiable;
    00355                         else{
    00356                                 solutionStatus = Valid;
    00357                                 unsatAssignment.makeEmpty();
    00358                         }
    00359                 }
    00360         }
    00361 }
    00362
    00364
    00365 VSATNode::SolutionType VSATNode::evaluate()
    00366 {
    00367         if(constraints.getLength() == 0 && solutionStatus == Unknown)
    00368         {
    00369                 if(notValid)
    00370                         solutionStatus = Satisfiable;
    00371                 else
    00372                         solutionStatus = Valid;
    00373         }
    00374         ConditionalDebugOut(debug > 5,
    00375                 cout << "Valid Assignment: ";
    00376                 validAssignment.printArray(cout, ", ");
    00377                 cout << endl;
    00378                 cout << "Unsat Assignment: ";
    00379                 unsatAssignment.printArray(cout, ", ");
    00380                 cout << endl;
    00381         );
    00382
    00383         if(solutionStatus == Unknown){
    00384                 SolutionType posSolution;
    00385                 SolutionType negSolution;
    00386                 // assign an unassigned variable from an unassigned clause
    00387                 // and then it's compliment
    00388                 if(constraints[0]->getLength() == 0){
    00389                         solutionStatus = Unsatisfiable;
    00390                         validAssignment.makeEmpty();
    00391                         return solutionStatus;
    00392                 }
    00393                 // find the first design variable in this constraint, if any
    00394                 BaseModelAssignmentArray * constraint = constraints[0];
    00395                 BaseModelAssignment * cu = NULL;
    00396                 for(unsigned int c = 0; c < constraint->getLength(); c++){
    00397                         BaseModelAssignment * cons = (*constraint)[c];
    00398                         if(allVariables[cons->getVariable()->getUID()]->isDesignVariable()){
    00399                                 cu = cons;
    00400                                 break;
    00401                         }
    00402                 }
    00403                 // If we didn't find anything, just take the first one.
    00404                 if(cu == NULL)
    00405                         cu = (*(constraints[0]))[0];
    00406                 BaseModelAssignmentArray posUnsatAssignment(false);
    00407                 BaseModelAssignmentArray posValidAssignment(false);
    00408                 bool designVariable = allVariables[cu->getVariable()->getUID()]->isDesignVariable();
    00409                 {
    00410                         VSATNode node(*this);
    00411                         node.propagate(*(cu), cu->getOperator() == BaseModelAssignment::Positive);
    00412                         posSolution = node.evaluate();
    00413                         numberOfExpandedNodes += node.getExpandCount();
    00414
    00415                         ConditionalDebugOut(debug > 5,
    00416                                 cout << "Tried assignment: " << *(cu) << endl;
    00417                                 cout << "  Assignment was ";
    00418                                 switch(posSolution){
    00419                                 case Satisfiable:
    00420                                         cout << "Satisfiable" << endl;
    00421                                         break;
    00422                                 case Unsatisfiable:
    00423                                         cout << "Unsatisfiable" << endl;
    00424                                         break;
    00425                                 case Valid:
    00426                                         cout << "Valid" << endl;
    00427                                         break;
    00428                                 case Unknown:
    00429                                         cout << "Unknown" << endl;
    00430                                         break;
    00431                                 }
    00432                                 cout << "  Valid Assignment: ";
    00433                                 node.getValidAssignment().printArray(cout, ", ");
    00434                                 cout << endl;
    00435                                 cout << "  Unsat Assignment: ";
    00436                                 node.getUnsatAssignment().printArray(cout, ", ");
    00437                                 cout << endl;
    00438                         );
    00439
    00440                         if(testForValid){
    00441                                 if(posSolution == Satisfiable){
    00442                                         solutionStatus = Satisfiable;
    00443                                         unsatAssignment = node.getUnsatAssignment();
    00444                                         validAssignment = node.getValidAssignment();
    00445                                         return solutionStatus;
    00446                                 }else if(notValid && posSolution == Valid){
    00447                                         solutionStatus = Satisfiable;
    00448                                         validAssignment = node.getValidAssignment();
    00449                                         return solutionStatus;
    00450                                 }else if(!designVariable && posSolution == Valid){
    00451                                         solutionStatus = Valid;
    00452                                         unsatAssignment.makeEmpty();
    00453                                         validAssignment = node.getValidAssignment();
    00454                                         return solutionStatus;
    00455                                 }
    00456                                 posUnsatAssignment = node.getUnsatAssignment();
    00457                                 posValidAssignment = node.getValidAssignment();
    00458                         }else{
    00459                                 if(!designVariable && !notValid && posSolution == Valid){
    00460                                         // if we don't care about this variable and this path was valid
    00461                                         // and we're not notValid, then we're valid (any solution works)
    00462                                         validAssignment = node.getValidAssignment();
    00463                                         unsatAssignment.makeEmpty();
    00464                                         solutionStatus = Valid;
    00465                                         return solutionStatus;
    00466                                 }else if(posSolution == Satisfiable){
    00467                                         // we know at least one solution exists, so just return satisfiable
    00468                                         validAssignment = node.getValidAssignment();
    00469                                         unsatAssignment = node.getUnsatAssignment();
    00470                                         solutionStatus = Satisfiable;
    00471                                         return solutionStatus;
    00472                                 }else if(posSolution == Valid){
    00473                                         // we know at least one solution exists, so just return satisfiable
    00474                                         validAssignment = node.getValidAssignment();
    00475                                         unsatAssignment.makeEmpty();
    00476                                         solutionStatus = Satisfiable;
    00477                                         return solutionStatus;
    00478                                 }
    00479                                 // posSolution == Unsatisfiable after this point for this branch
    00480                         }
    00481                 }
    00482                 {
    00483                         VSATNode node(*this);
    00484                         node.propagate(*(cu), cu->getOperator() !=
    00485                                 BaseModelAssignment::Positive);
    00486                         negSolution = node.evaluate();
    00487                         numberOfExpandedNodes += node.getExpandCount();
    00488
    00489                         ConditionalDebugOut(debug > 5,
    00490                                 cout << "Tried assignment: (NOT) " << *(cu) << endl;
    00491                                 cout << "Assignment was ";
    00492                                 switch(negSolution){
    00493                                 case Satisfiable:
    00494                                         cout << "Satisfiable" << endl;
    00495                                         break;
    00496                                 case Unsatisfiable:
    00497                                         cout << "Unsatisfiable" << endl;
    00498                                         break;
    00499                                 case Valid:
    00500                                         cout << "Valid" << endl;
    00501                                         break;
    00502                                 case Unknown:
    00503                                         cout << "Unknown" << endl;
    00504                                         break;
    00505                                 }
    00506                                 cout << "Valid Assignment: ";
    00507                                 node.getValidAssignment().printArray(cout, ", ");
    00508                                 cout << endl;
    00509                                 cout << "Unsat Assignment: ";
    00510                                 node.getUnsatAssignment().printArray(cout, ", ");
    00511                                 cout << endl;
    00512                         );
    00513
    00514                         if(negSolution == Satisfiable){
    00515                                 solutionStatus = Satisfiable;
    00516                                 unsatAssignment = node.getUnsatAssignment();
    00517                                 validAssignment = node.getValidAssignment();
    00518                                 if(posSolution == Valid){
    00519                                         if(posValidAssignment.getLength() < validAssignment.getLength())
    00520                                         {
    00521                                                 validAssignment = posValidAssignment;
    00522                                         }
    00523                                 }else{ // Unsatisfiable
    00524                                         if(posUnsatAssignment.getLength() < unsatAssignment.getLength())
    00525                                         {
    00526                                                 unsatAssignment = posUnsatAssignment;
    00527                                         }
    00528                                 }
    00529                         }else if(notValid && negSolution == Valid){
    00530                                 validAssignment = node.getValidAssignment();
    00531                                 solutionStatus = Satisfiable;
    00532                         }else if(!designVariable && negSolution == Valid){
    00533                                 unsatAssignment.makeEmpty();
    00534                                 // we're using our validAssignment, so adjust it.
    00535                                 adjustValidAssignment();
    00536                                 solutionStatus = Valid;
    00537                         }else if(posSolution == negSolution){
    00538                                 // they agree so we agree
    00539                                 solutionStatus = posSolution;
    00540                                 if(solutionStatus == Unsatisfiable){
    00541                                         validAssignment.makeEmpty();
    00542                                 }else{
    00543                                         // we're using our validAssignment, so adjust it.
    00544                                         adjustValidAssignment();
    00545                                         unsatAssignment.makeEmpty();
    00546                                 }
    00547                         }else{
    00548                                 // Valid + Unsatisfiable = Satisfiable
    00549                                 if(negSolution == Valid){
    00550                                         validAssignment = node.getValidAssignment();
    00551                                         unsatAssignment = posUnsatAssignment;
    00552                                 }else{
    00553                                         validAssignment = posValidAssignment;
    00554                                         unsatAssignment = node.getUnsatAssignment();
    00555                                 }
    00556                                 solutionStatus = Satisfiable;
    00557                         }
    00558                 }
    00559         }
    00560         return solutionStatus;
    00561 }
    00562
    00564
    00565 double VSATNode::getExpandCount()
    00566 {
    00567         return numberOfExpandedNodes;
    00568 }
    00569
    00571
    00572 BaseModelAssignmentArray & VSATNode::getUnsatAssignment()
    00573 {
    00574         return unsatAssignment;
    00575 }
    00576
    00578
    00579 BaseModelAssignmentArray & VSATNode::getValidAssignment()
    00580 {
    00581         return validAssignment;
    00582 }
    00583
    00585
    00586 void VSATNode::adjustValidAssignment()
    00587 {
    00588         // If we restricted one of the design
    00589         // variables (even if it was ok), and it wasn't given an exact assignment
    00590         // then we still need to choose among the valid solutions for the validAssignment.
    00591         // Thus we must select a remaining assignment from the remaining design variables
    00592         // that have had at least one assignment eliminated.
    00593         for(unsigned int u = 0; u < unassignedVariables.getLength(); u++){
    00594                 if(unassignedVariables[u]->isDesignVariable()){
    00595                         VSATVariable * uVar = unassignedVariables[u];
    00596                         BaseModelAssignmentArray &varDomain = *(domains[uVar->getUID()]);
    00597
    00598                         if(varDomain.getLength() < uVar->getAssignments().getLength()){
    00599                                 validAssignment.pushBack(varDomain[0]);
    00600                         }
    00601                 }
    00602         }
    00603 }
    00604
    00606