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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATTester.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 //# CHECKED MJP 08-07-2002
    00014
    00015 #include <cstdlib>
    00016 #include <cassert>
    00017 #include <iostream>
    00018
    00019 #include "ISATProposition.h"
    00020 #include "ISATPropositionDescription.h"
    00021 #include "ISATClause.h"
    00022 #include "ISATClauses.h"
    00023 #include "ISATClausesSet.h"
    00024 #include "ISATTheory.h"
    00025 #include "ISATBaseModelAssignmentDescription.h"
    00026 #include "ISATTester.h"
    00027 #include <Mers/Models/Base/BaseModelSentence.h>
    00028 #include <Mers/Models/Base/BaseModelClause.h>
    00029 #include <Mers/Models/Base/BaseModelDomain.h>
    00030
    00032
    00033 using namespace Mers::Solvers::SAT::ISAT;
    00034 using Mers::Models::Base::BaseModelVariableArray;
    00035 using Mers::Models::Base::BaseModelSentence;
    00036 using Mers::Models::Base::BaseModelClause;
    00037 using Mers::Models::Base::BaseModelVariable;
    00038 using Mers::Models::Base::BaseModelDomain;
    00039 using Mers::Models::Base::BaseModelValue;
    00040 using Mers::Models::Base::BaseModelAssignment;
    00041 using Mers::Models::Base::BaseModelAssignmentArray;
    00042 using std::ostream;
    00043 using std::cerr;
    00044 using std::cout;
    00045 using std::endl;
    00046
    00048 // Public Constructors, Copy Constructors, & Destructors
    00050
    00051 ISATTester::ISATTester(BaseModelVariableArray const & variableSet,
    00052         BaseModelVariableArray const & searchVariableSet,
    00053         BaseModelSentence const & constraintSet)
    00054 : useDPLL(true), mUseFilter(true), propositionVariables(variableSet),
    00055         allAssignments(true), mSearchVariables(searchVariableSet)
    00056 {
    00057         for(unsigned int var = 0; var < propositionVariables.getLength(); var++){
    00058                 BaseModelVariable * variable = propositionVariables[var];
    00059                 unsigned int variableUID = variable->getUID();
    00060                 BaseModelDomain &domain = *(variable->getDomain());
    00061
    00062                 BaseModelClause * positiveClause =
    00063                         new BaseModelClause(BaseModelClause::DISJUNCTIVE, true);
    00064                 BaseModelClause * negativeClause =
    00065                         new BaseModelClause(BaseModelClause::DISJUNCTIVE, true);
    00066
    00067                 for(unsigned int val = 0; val < domain.getLength(); val++){
    00068                         BaseModelValue * value = domain[val];
    00069
    00070                         positiveClause->pushBack(new BaseModelAssignment(variable,
    00071                                 value, BaseModelAssignment::Positive));
    00072                         negativeClause->pushBack(new BaseModelAssignment(variable,
    00073                                 value, BaseModelAssignment::Negative));
    00074                 }
    00075                 unsigned int newLength = (variableUID << 1) + 2;
    00076                 while(allAssignments.getLength() < newLength)
    00077                         allAssignments.pushBack(NULL);
    00078                 assert(allAssignments[newLength - 2] == NULL &&
    00079                         allAssignments[newLength - 1] == NULL);
    00080                 allAssignments[newLength - 2] = positiveClause;
    00081                 allAssignments[newLength - 1] = negativeClause;
    00082         }
    00083
    00084         init(constraintSet, BaseModelSentence(BaseModelSentence::CNF, true),
    00085                 BaseModelSentence(BaseModelSentence::CNF, true));
    00086
    00087         addDomainConstraints();
    00088 }
    00089
    00091
    00092 ISATTester::~ISATTester()
    00093 {
    00094
    00095 }
    00096
    00098
    00099 //----------------------------------------------------------------------------------------
    00100 // Public Function Members
    00101 //----------------------------------------------------------------------------------------
    00102
    00103 ISATTester::SolutionType ISATTester::tryAssignment(
    00104         BaseModelAssignmentArray const * candidate,
    00105         int group, bool satisfy, BaseModelAssignmentArray &conflict)
    00106 {
    00107         (void) group;
    00108         ISATClausesSet const * conflicts_p;
    00109         ISATClauses const * conflict_p;
    00110         ISATClauses::const_iterator     cIter;
    00111         BaseModelAssignment const * assignment_p;
    00112         SolutionType solutionStatus;
    00113
    00114         //cout << "Trying candidate of : " << constraintToisatClause(candidate, false) << endl;
    00115         insert_conjunctive_constraint_as_candidate(candidate);
    00116
    00117
    00118
    00119         if (debug)
    00120         {
    00121                 cout << endl;
    00122                 cout << "[ISATTester] FACT: " << fact_clauses << endl;
    00123                 cout << "[ISATTester] CANDIDATE: " << candidate_clauses << endl;
    00124                 cout << "[ISATTester] CANDIDATE: ";
    00125                 candidate->printArray(cout, ", ");
    00126                 cout << endl;
    00127                 cout << "[ISATTester] Current ISAT:" << endl << SAT_engine << endl;
    00128         }
    00129
    00130         // Then test satisfiability and gather conflict
    00131         if(satisfy)
    00132         {
    00133                 if(debug)
    00134                         cout << "[ISATTester] Checking SAT" << endl;
    00135                 if (fact_clauses.empty()){
    00136                         conflicts_p = SAT_engine.get_SAT_conflicts_p(useDPLL);
    00137                 }else{
    00138                         if(debug)
    00139                                 cout << "[ISATTester] Using fact clauses: " << fact_clauses << endl;
    00140                         conflicts_p = SAT_engine.get_SAT_conflicts_p_using_fact(useDPLL, &fact_clauses);
    00141                 }
    00142                 if(SAT_consistent(useDPLL, true))
    00143                         solutionStatus = Satisfiable;
    00144                 else
    00145                         solutionStatus = Unsatisfiable;
    00146         }
    00147         else
    00148         {
    00149                 if(debug)
    00150                         cout << "[ISATTester] Checking UNSAT" << endl;
    00151                 if (fact_clauses.empty())
    00152                 {
    00153                         conflicts_p = SAT_engine.get_UNSAT_conflicts_p(useDPLL);
    00154                 }
    00155                 else
    00156                 {
    00157                         if(debug)
    00158                                 cout << "[ISATTester] Using fact clauses: " << fact_clauses << endl;
    00159                         conflicts_p = SAT_engine.get_UNSAT_conflicts_p_using_fact(useDPLL, &fact_clauses);
    00160                 }
    00161                 if(UNSAT_inconsistent(useDPLL, true))
    00162                         solutionStatus = Unsatisfiable;
    00163                 else
    00164                         solutionStatus = Satisfiable;
    00165         }
    00166         if (debug)
    00167         {
    00168                 cout << "[ISATTester] Conflict from ISAT: " << *conflicts_p << endl;
    00169         }
    00170
    00171         // Return the conflict by converting inconsistent literals into Assignments
    00172         // List of inconsistent Assignments
    00173         // However, if the candidate is a partial candidate and we're doing unsat,
    00174         // ignore the conflict, since ISAT doesn't return correct conflicts in this
    00175         // case.
    00176         if (!conflicts_p->is_empty()
    00177                 && (candidate->getLength() == mSearchVariables.size() || satisfy))
    00178         {
    00179                 assert(conflicts_p->front() != NULL);
    00180                 conflict_p = conflicts_p->front();
    00181                 for (cIter = conflict_p->begin(); cIter != conflict_p->end(); cIter++)
    00182                 {
    00183                         assert((*cIter)->get_numb_of_literals() == 1);
    00184                         assert((*cIter)->front() != NULL);
    00185                         // Find the Assignment Corresponding to this Literal
    00186                         assignment_p = ((ISATBaseModelAssignmentDescription *)(*cIter)->front()->
    00187                                 get_proposition_p()->get_description_p())->get_assignment_p();
    00188                         //#assignment_p->getVariable()->conflicts.push_back(assignment_p);
    00189                         //# What was meant by this??? It's not valid!!!
    00190                         //#assignment_p->getVariable()->conflicts.push_back(assignment_p);
    00191
    00192                         // Verify that this variable is within the search variables.
    00193                         if(mUseFilter) {
    00194                                 bool found = false;
    00195                                 for(unsigned int i = 0; i < mSearchVariables.size(); ++i) {
    00196                                         if((*assignment_p->getVariable()) == (*mSearchVariables[i])) {
    00197                                                 found = true;
    00198                                                 break;
    00199                                         }
    00200                                 }
    00201
    00202                                 if(found) {
    00203                                         conflict += *assignment_p;
    00204                                 } else {
    00205                                         // This conflict is invalid.
    00206                                         if(!noWarn) {
    00207                                                 cerr << "Warning, pruning conflict: " << *conflict_p << endl;
    00208                                         }
    00209                                         conflict.makeEmpty();
    00210                                         break;
    00211                                 }
    00212                         } else {
    00213                                         conflict += *assignment_p;
    00214                         }
    00215                 }
    00216         }
    00217 /*#
    00218         cout << endl;
    00219         cout << "*********" << endl;
    00220         cout << "THEORY:" << endl;
    00221         cout << SAT_engine << endl;
    00222         cout << "FACT: " << fact_clauses << endl;
    00223         cout << "CANDIDATE: " << candidate_clauses << endl;
    00224         cout << "Theory is " << SAT_engine.get_consistency(useDPLL) << endl;
    00225         cout << "SAT CONFLICT: " << endl;
    00226         if (fact_clauses.empty())
    00227         {
    00228                 cout << *SAT_engine.get_SAT_conflicts_p(useDPLL) << endl;;
    00229         }
    00230         else
    00231         {
    00232                 cout << *SAT_engine.get_SAT_conflicts_p_using_fact(useDPLL, &fact_clauses) << endl;
    00233         }
    00234         cout << "UNSAT CONFLICT: " << endl;
    00235         if (fact_clauses.empty())
    00236         {
    00237                 cout << *SAT_engine.get_UNSAT_conflicts_p(useDPLL) << endl;;
    00238         }
    00239         else
    00240         {
    00241                 cout << *SAT_engine.get_UNSAT_conflicts_p_using_fact(useDPLL, &fact_clauses) << endl;
    00242         }
    00243         cout << "*********" << endl << endl;
    00244 */
    00245
    00246         // remove candidate:
    00247         clear_candidate();
    00248
    00249         return solutionStatus;
    00250 }
    00251
    00253
    00254 void ISATTester::printStatistics(bool verbose) const
    00255 {
    00256         (void) verbose;
    00257         cout << "ISAT:" << endl;
    00258         cout << "\ttime to propagate: " << SAT_engine.get_total_time() << endl;
    00259         cout << "\tnumber of proposition assignments: " << SAT_engine.get_assign_proposition_counter()<< endl;
    00260         cout << "\tnumber of proposition unassignments: " << SAT_engine.get_unassign_proposition_counter() << endl;
    00261 }
    00262
    00263 double ISATTester::getNumberOfSteps() const
    00264 {
    00265         //below is the number of proposition assignments plus the number of proposition unassignments made by ISAT
    00266         //both numbers should be considered because sometimes ISAT may flip the value of a proposition without unassigning
    00267         //the only reason the numbers are added together is because this function only returns 1 value.
    00268         return (SAT_engine.get_assign_proposition_counter() + SAT_engine.get_unassign_proposition_counter());
    00269 }
    00270
    00272
    00273 void
    00274 ISATTester::setDebug(unsigned int state)
    00275 {
    00276         debug = state;
    00277 #ifdef _DEBUG
    00278         SAT_engine.set_debug_level(state);
    00279 #endif
    00280 }
    00281
    00283
    00284 void
    00285 ISATTester::suppressWarnings(bool off)
    00286 {
    00287         noWarn = off;
    00288 }
    00289
    00291
    00292 void
    00293 ISATTester::addConstraint(BaseModelClause const * c)
    00294 {
    00295         assert(c);
    00296         insert_disjunctive_constraint(c);
    00297 }
    00298
    00300
    00301 void
    00302 ISATTester::addTemporaryConstraint(BaseModelClause const * c)
    00303 {
    00304         ISATClause *clause_p;
    00305         assert(c);
    00306 //      if (!hasTemporary)
    00307 //      {
    00308 //              setTemporaryConstraint(c);
    00309                 hasTemporary = true;
    00310 //              return;
    00311 //      }
    00312         clause_p = insert_disjunctive_constraint(c);
    00313         fact_clauses.push_back(clause_p);
    00314 }
    00315
    00317
    00318 void
    00319 ISATTester::setTemporaryConstraint(BaseModelClause const * c)
    00320 {
    00321         clearTemporaryConstraint();
    00322         addTemporaryConstraint(c);
    00323 //      ISATClause *clause_p;
    00324 //      assert(c);
    00325 //      hasTemporary = true;
    00326 //      clause_p = insert_disjunctive_constraint(c);
    00327 //      fact_clauses.push_back(clause_p);
    00328 }
    00329
    00331
    00332 void
    00333 ISATTester::clearTemporaryConstraint()
    00334 {
    00335         ISATClause *clause_p;
    00336         while (!fact_clauses.empty())
    00337         {
    00338                 clause_p = fact_clauses.front();
    00339                 fact_clauses.pop_front();
    00340                 SAT_engine.remove_clause(clause_p);
    00341         }
    00342         hasTemporary = false;
    00343 }
    00344
    00346
    00347 #if 0
    00348 void
    00349 ISATTester::constrainByReachability()
    00350 {
    00351         convertVariables();
    00352         BaseModelVariableArray::const_iterator varIter;
    00353         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00354              varIter++)
    00355         {
    00356                 // create constraint based on this variable's reachable domain
    00357                         // skip if all values are reachable:
    00358                 if ((*varIter).allReachable())
    00359                         continue;
    00360
    00361                 Constraint c;
    00362                 list<Assignment const *> assigns = (*varIter)->getAssignments();
    00363                 list<Assignment const *>::const_iterator aIter;
    00364                 for (aIter = assigns.begin(); aIter != assigns.end(); aIter++)
    00365                 {
    00366                         c.addUnit((*aIter), true);
    00367                 }
    00368                 if (c.empty())
    00369                         continue;  // shouldn't ever happen - only for a null domain
    00370                 addTemporaryConstraint(&c);
    00371         }
    00372 }
    00373
    00375
    00376 void
    00377 ISATTester::constrainByNextValue()
    00378 {
    00379         convertVariables();
    00380         list<Variable const *>::const_iterator varIter;
    00381         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00382              varIter++)
    00383         {
    00384                 // create constraint based on this variable's current value
    00385                 Assignment const * nex = (*varIter)->getNextAssignment();
    00386                         // skip if no current:
    00387                 if (nex == NULL)
    00388                         continue;
    00389
    00390                 Constraint c;
    00391                 c.addUnit(nex, true);
    00392                 addTemporaryConstraint(&c);
    00393         }
    00394 }
    00395
    00396 #endif
    00397
    00399
    00400 // modifies: this (for efficiency)
    00401 // effects : Returns true IF the current Theory is satisfiable
    00402 //           If useDPLL == true, SAT is complete (IFF). Otherwise, SAT is
    00403 //           incomplete (yet sound).
    00404 bool
    00405 ISATTester::SAT_consistent(bool newUseDPLL, bool certain)
    00406 {
    00407         ISATTheory::ConsistencyType res = SAT_engine.get_consistency(newUseDPLL);
    00408         if (newUseDPLL)
    00409                 if (res == ISATTheory::INDETERMINATE && !noWarn)
    00410                         cerr << "Warning: INDETERMINATE with DPLL!!" << endl;
    00411         return (res == ISATTheory::CONSISTENT) || (!certain && (res == ISATTheory::INDETERMINATE));
    00412 }
    00413
    00415
    00416 // modifies: this (for efficiency)
    00417 // effects : Returns true IFF the current Theory is INconsistent
    00418 //           If useDPLL == true, UNSAT is complete. Otherwise, SAT is
    00419 //           incomplete (yet sound).
    00420 bool
    00421 ISATTester::UNSAT_inconsistent(bool newUseDPLL, bool certain)
    00422 {
    00423         ISATTheory::ConsistencyType res = SAT_engine.get_consistency(newUseDPLL);
    00424         if (newUseDPLL)
    00425                 if (res == ISATTheory::INDETERMINATE && !noWarn)
    00426                         cerr << "Warning: INDETERMINATE with DPLL!!" << endl;
    00427         return (res == ISATTheory::INCONSISTENT) || (!certain && (res == ISATTheory::INDETERMINATE));
    00428 }
    00429
    00431
    00432 bool
    00433 ISATTester::consistent(bool satisfy, bool newUseDPLL)
    00434 {
    00435         return satisfy ? SAT_consistent(newUseDPLL) : UNSAT_inconsistent(newUseDPLL);
    00436 }
    00437
    00439
    00440 bool
    00441 ISATTester::consistentMaybe(bool satisfy, bool newUseDPLL)
    00442 {
    00443         return satisfy ? SAT_consistent(newUseDPLL, false) : UNSAT_inconsistent(newUseDPLL, false);
    00444 }
    00445
    00447
    00448 void
    00449 ISATTester::addDomainConstraints()
    00450 {
    00451         BaseModelVariableArray::Iterator varIter;
    00452         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00453         varIter++)
    00454         {
    00455                 BaseModelVariable * var = &(*varIter);
    00456                 unsigned int varUID = var->getUID();
    00457                 BaseModelDomain &domain = *(var->getDomain());
    00458                 if (domain.isEmpty())  // skip empty domains?
    00459                         continue;
    00460
    00461                 BaseModelClause c(BaseModelClause::DISJUNCTIVE, false);
    00462
    00464                 // domain exhaustion:
    00465                 unsigned int d;
    00466                 for(d = 0; d < domain.getLength(); d++)
    00467                 {
    00468                         c.pushBack((*(allAssignments[(varUID << 1)]))[d]);
    00469                 }
    00470                 addConstraint(&c);
    00471
    00472
    00474                 // mutual exclusion:
    00475                 for(d = 0; d < domain.getLength(); d++)
    00476                 {
    00477                         BaseModelAssignment * a1 =
    00478                                 (*(allAssignments[(varUID << 1) + 1]))[d];
    00479                         for (unsigned int d2 = d + 1; d2 < domain.getLength(); d2++)
    00480                         {
    00481                                 BaseModelClause c2(BaseModelClause::DISJUNCTIVE, false);
    00482                                 c2.pushBack(a1);
    00483                                 c2.pushBack((*(allAssignments[(varUID << 1) + 1]))[d2]);
    00484                                 addConstraint(&c2);
    00485                         }
    00486                 }
    00487         }
    00488 }
    00489
    00491
    00492 void ISATTester::setDPLLFlag(bool dpll_flag)
    00493 {
    00494         useDPLL = dpll_flag;
    00495 }
    00496
    00498
    00499 /*#
    00500 void
    00501 ISATTester::constrainByNextValuePermanent()
    00502 {
    00503         convertVariables();
    00504         list<Variable const *>::const_iterator varIter;
    00505         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00506              varIter++)
    00507         {
    00508                 // create constraint based on this variable's current value
    00509                 Assignment const * nex = (*varIter)->getNextAssignment();
    00510                         // skip if no current:
    00511                 if (nex == NULL)
    00512                         continue;
    00513
    00514                 Constraint c;
    00515                 c.addUnit(nex, true);
    00516                 SAT_engine.addClause(constraintToisatClause(&c));
    00517         }
    00518 }
    00519
    00521
    00522 void
    00523 ISATTester::constrainByCurrentValuePermanent()
    00524 {
    00525         convertVariables();
    00526         list<Variable const *>::const_iterator varIter;
    00527         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00528              varIter++)
    00529         {
    00530                 // create constraint based on this variable's current value
    00531                 Assignment const * cur = (*varIter)->getCurrentAssignment();
    00532                         // skip if no current:
    00533                 if (cur == NULL)
    00534                         continue;
    00535
    00536                 Constraint c;
    00537                 c.addUnit(cur, true);
    00538                 SAT_engine.addClause(constraintToisatClause(&c));
    00539         }
    00540 }
    00541
    00543
    00544 void
    00545 ISATTester::constrainByCurrentValue()
    00546 {
    00547         convertVariables();
    00548         list<Variable const *>::const_iterator varIter;
    00549         for (varIter = propositionVariables.begin(); varIter != propositionVariables.end();
    00550              varIter++)
    00551         {
    00552                 // create constraint based on this variable's current value
    00553                 Assignment const * cur = (*varIter)->getCurrentAssignment();
    00554                         // skip if no current:
    00555                 if (cur == NULL)
    00556                         continue;
    00557
    00558                 Constraint c;
    00559                 c.addUnit(cur, true);
    00560                 addTemporaryConstraint(&c);
    00561         }
    00562 }
    00563
    00565
    00566 void
    00567 ISATTester::dumpProblem(string basename)
    00568 {
    00569         string varname = basename + "_variables.dat";
    00570         //string conname = basename + "_constraints.dat";
    00571         //string extname = basename + "_extras.dat";
    00572
    00573         ofstream varout(varname.c_str());
    00574         convertVariables();
    00575         list<Variable const *>::const_iterator varIter;
    00576         for (varIter = propositionVariables.begin();
    00577              varIter != propositionVariables.end(); varIter++)
    00578         {
    00579                 varout << (*varIter)->getNameString();
    00580                 list<Assignment const *> assigns = (*varIter)->getAssignments(); // only reachable
    00581                 list<Assignment const *>::const_iterator aIter;
    00582                 for (aIter = assigns.begin(); aIter != assigns.end(); aIter++)
    00583                 {
    00584                         varout << " " << (*aIter)->getValueString()
    00585                                << " " << (*aIter)->getTrueCost();  // only based on current values
    00586                 }
    00587         }
    00588         varout.close();
    00589
    00590         //ofstream conout(conname);
    00591         //list<Constraint const *>::const_iterator conIter;
    00592         //for (conIter = .begin();
    00593         //     conIter != .end(); conIter++)
    00594         //{
    00595         //      conout << (*varIter)->getNameString();
    00596         //      list<Assignment const *> assigns = (*varIter)->getAssignments(); // only reachable
    00597         //      list<Assignment const *>::const_iterator aIter;
    00598         //      for (aIter = assigns.begin(); aIter != assigns.end(); aIter++)
    00599         //      {
    00600         //              conout << " " << (*aIter)->getValueString()
    00601         //                     << " " << (*aIter)->getTrueCost();  // only based on current values
    00602         //      }
    00603         //}
    00604         //conout.close();
    00605
    00606 }
    00607 */
    00608 //----------------------------------------------------------------------------------------
    00609 // Private Function Members
    00610 //----------------------------------------------------------------------------------------
    00611
    00612 void
    00613 ISATTester::init(BaseModelSentence const & baseConstraintSet,
    00614            BaseModelSentence const & satConstraintSet,
    00615            BaseModelSentence const & unsatConstraintSet)
    00616 {
    00617         hasTemporary = false;
    00618         debug = false;
    00619         noWarn = false;
    00620
    00621         // Each base constraint is an Theory Clause in the Theory.
    00622         // Add all of the Clauses to the Theory
    00623         unsigned int c;
    00624
    00625         for(c = 0; c < baseConstraintSet.getLength(); c++)
    00626         {
    00627                 BaseModelClause const * clause = baseConstraintSet[c];
    00628                 assert(clause != NULL);
    00629                 //cout << "init adding clause... " << endl;
    00630                 insert_disjunctive_constraint(clause);
    00631                 //cout << "done." << endl;
    00632         }
    00633
    00634         // Each sat constraint is also an Sat Clause in the Theory.
    00635         // Add all of the Clauses to the Theory
    00636         for(c = 0; c < satConstraintSet.getLength(); c++)
    00637         {
    00638                 BaseModelClause const * clause = satConstraintSet[c];
    00639                 assert(clause != NULL);
    00640                 insert_disjunctive_constraint(clause);
    00641         }
    00642
    00643         // Each unsat constraint is also an unsat Clause in the Theory.
    00644         // Add all of the Clauses to the Theory
    00645         for(c = 0; c < unsatConstraintSet.getLength(); c++)
    00646         {
    00647                 BaseModelClause const * clause = unsatConstraintSet[c];
    00648                 assert(clause != NULL);
    00649                 insert_disjunctive_constraint(clause);
    00650         }
    00651
    00652         // ** Perhaps add code that ensures unique variable assignments **
    00653         // **** Expected to be incorporated into theory, for now.
    00654 }
    00655
    00657
    00658 /*#
    00659 isatClause
    00660 ISATTester::constraintToisatClause(Constraint const * con, bool disjunctive)
    00661 {
    00662         assert(con);
    00665         isatClause ic(disjunctive ? isatClause::DISJUNCTIVE : isatClause::CONJUNCTIVE);
    00666         list<ConstraintUnit> constraintUnits = con->getConstraintUnits();
    00667         list<ConstraintUnit>::const_iterator cIter;
    00668         for (cIter = constraintUnits.begin(); cIter != constraintUnits.end(); cIter++)
    00669         {
    00670                 if (! (*cIter).getAssignment() )
    00671                 {
    00672                         cerr << "Warning: Constraint skipping unit because of null assignment!" << endl;
    00673                         continue;
    00674                 }
    00675                 isatProposition * prop = SAT_engine.isatProposition_p((*cIter).getAssignment());
    00676                 if (! prop )
    00677                 {
    00678                         cerr << "Warning: Constraint skipping unit because of null isatProposition!" << endl;
    00679                         continue;
    00680                 }
    00681                 isatLiteral lit(*prop, (*cIter).getParity() ? isatLiteral::POSITIVE :
    00682                                                               isatLiteral::NEGATIVE);
    00683                 ic.insert_isatLiteral(lit);
    00684         }
    00685         return ic;
    00686 }
    00687 */
    00688
    00690
    00691 ISATClause *
    00692 ISATTester::insert_disjunctive_constraint(BaseModelAssignmentArray const *constraint_p)
    00693 {
    00694         assert(constraint_p != NULL);
    00695
    00696         ISATClause *                                    clause_p = SAT_engine.insert_new_empty_clause();
    00697         ISATBaseModelAssignmentDescription*     prop_desc_p;
    00698         unsigned int a;
    00699
    00700         for (a = 0; a < constraint_p->getLength(); a++)
    00701         {
    00702                 BaseModelAssignment const * asg = (*constraint_p)[a];
    00703
    00704                 if (asg == NULL)
    00705                 {
    00706                         cerr << "Warning: Constraint skipping unit because of null assignment!" << endl;
    00707                         continue;
    00708                 }
    00709                 prop_desc_p = new ISATBaseModelAssignmentDescription(asg);
    00710                 SAT_engine.add_literal_to_new_clause(prop_desc_p,
    00711                         asg->getOperator() == BaseModelAssignment::Positive ?
    00712                         ISATLiteral::POSITIVE : ISATLiteral::NEGATIVE);
    00713         }
    00714         SAT_engine.activate_clause(clause_p);
    00715         return clause_p;
    00716 }
    00717
    00719
    00720 void
    00721 ISATTester::insert_conjunctive_constraint_as_candidate(BaseModelAssignmentArray const *constraint_p)
    00722 {
    00723         assert(constraint_p != NULL);
    00724
    00725         ISATClause *                                    clause_p;
    00726         ISATBaseModelAssignmentDescription*     prop_desc_p;
    00727         unsigned int a;
    00728
    00729         for (a = 0; a < constraint_p->getLength(); a++)
    00730         {
    00731                 BaseModelAssignment const * asg = (*constraint_p)[a];
    00732
    00733                 clause_p = SAT_engine.insert_new_empty_clause();
    00734                 if (asg == NULL)
    00735                 {
    00736                         cerr << "Warning: Constraint skipping unit because of null assignment!" << endl;
    00737                         continue;
    00738                 }
    00739                 prop_desc_p = new ISATBaseModelAssignmentDescription(asg);
    00740                 SAT_engine.add_literal_to_new_clause(prop_desc_p,
    00741                         asg->getOperator() == BaseModelAssignment::Positive ?
    00742                         ISATLiteral::POSITIVE : ISATLiteral::NEGATIVE);
    00743                 if(debug)
    00744                         cout << "Activating Candidate Clause: " << *clause_p << endl;
    00745                 SAT_engine.activate_clause(clause_p);
    00746                 candidate_clauses.push_back(clause_p);
    00747         }
    00748 }
    00749
    00751
    00752 void
    00753 ISATTester::clear_candidate()
    00754 {
    00755         ISATClause *clause_p;
    00756         while (!candidate_clauses.empty())
    00757         {
    00758                 clause_p = candidate_clauses.front();
    00759                 candidate_clauses.pop_front();
    00760                 SAT_engine.remove_clause(clause_p);
    00761         }
    00762 }
    00763
    00765
    00766 //----------------------------------------------------------------------------------------
    00767 // Public Operators
    00768 //----------------------------------------------------------------------------------------
    00769
    00770 ostream&
    00771 Mers::Solvers::SAT::ISAT::operator<<(ostream& os, ISATTester const & v)
    00772 {
    00773         //# not complete, for now:
    00774         os << v.SAT_engine;
    00775         return os;
    00776 }
    00777
    00779