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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATTheory.cpp

    00001 //========================================================================================
    00002 //
    00003 // Copyright (c) 2001           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 (MERS) group
    00007 // does not assume any responsibility.
    00008 //
    00009 // Author:                      Seung H. Chung
    00010 //
    00011 // Organization:        Model-based Embedded and Robotic Systems Group
    00012 //                                      Massachusetts Institute of Technology
    00013 //
    00014 // File:                        ISATTheory.cpp
    00015 //
    00016 // Description:         Circularly linked list of clause pointers. It follows the C++
    00017 //                                      Standard Template Library specifications. It is in charge of
    00018 //                                      deallocating the clauses.
    00019 //
    00020 //========================================================================================
    00021
    00022 #include "ISATTheory.h"
    00023
    00024 #include <cassert>
    00025 #include <cstdio>
    00026 #include <time.h>
    00027 #include "ISATPropositionDescription.h"
    00028 #include "ISATProposition.h"
    00029 #include "ISATPropositions.h"
    00030 #include "ISATUnassignedPropositions.h"
    00031 #include "ISATPropositionDB.h"
    00032 #include "ISATLiteral.h"
    00033 #include "ISATLiterals.h"
    00034 #include "ISATClause.h"
    00035 #include "ISATClauses.h"
    00036 #include "ISATUnitClauses.h"
    00037 #include "ISATInconsistentClauses.h"
    00038 #include "ISATClauseDB.h"
    00039 #include "ISATClausesSet.h"
    00040
    00042
    00043 using namespace Mers::Solvers::SAT::ISAT;
    00044 using std::ostream;
    00045 using std::endl;
    00046 using std::cerr;
    00047
    00049 // Public Constructors, Copy Constructors, & Destructors
    00051
    00052 ISATTheory::ISATTheory()
    00053 {
    00054         assign_proposition_count        = 0;
    00055         unassign_proposition_count  = 0;
    00056         total_time                                      = 0.0;
    00057
    00058 //      proposition_database_p          = new ISATPropositionDB();
    00059         clause_database_p                       = new ISATClauseDB();
    00060 //      assigned_propositions_p         = new ISATPropositions();
    00061         searched_propositions_p         = new ISATPropositions();
    00062         unassigned_propositions_p       = new ISATUnassignedPropositions();
    00063         unit_clauses_p                          = new ISATUnitClauses();
    00064         inconsistent_clauses_p          = new ISATInconsistentClauses();
    00065         SAT_conflicts_p                         = new ISATClausesSet();
    00066         UNSAT_conflicts_p                       = new ISATClausesSet();
    00067         searched_path_length            = 0;
    00068 #if defined _DEBUG
    00069         debug_level                                     = 0;
    00070 #endif // #if defined _DEBUG
    00071 }
    00072
    00073 ISATTheory::ISATTheory(ISATTheory const &other)
    00074 : ISATPropositionDB(other)
    00075 {
    00076         cerr << "Warning: ISATTheory copy constructor looks defective!" << endl;
    00077 }
    00078
    00079 ISATTheory::~ISATTheory()
    00080 {
    00081 //      delete proposition_database_p;
    00082         delete clause_database_p;
    00083 //      delete assigned_propositions_p;
    00084         delete searched_propositions_p;
    00085         delete unassigned_propositions_p;
    00086         delete unit_clauses_p;
    00087         delete inconsistent_clauses_p;
    00088         delete SAT_conflicts_p;
    00089         delete UNSAT_conflicts_p;
    00090 }
    00091
    00092 //----------------------------------------------------------------------------------------
    00093 // Public Function Members
    00094 //----------------------------------------------------------------------------------------
    00095 ISATTheory::ConsistencyType
    00096 ISATTheory::get_consistency(bool use_DPLL)
    00097 {
    00098         /*if (get_current_consistency() == INDETERMINATE && use_DPLL)
    00099         {
    00100                 clear_DPLL_search();
    00101                 propagate_using_DPLL();
    00102         }
    00103         else if (!use_DPLL)
    00104         {
    00105                 clear_DPLL_search();
    00106         }*/
    00107
    00108 // This doesn't seem to be true. There are unit clauses when searching using DPLL. If
    00109 // an inconsistent clause is incountered while propagating unit clauses, and there are
    00110 // unit clauses left, this would result in a none empty unit clauses. This problem only
    00111 // exists for DPLL because as it unassigned wrong guesses the unit clauses are poped into
    00112 // the list of unit clauses. However, in the case of no DPLL, the left over unit clauses
    00113 // are thrown out.
    00114 //
    00115 //      assert(unit_clauses_p->is_empty());
    00116
    00117         propagate_clauses(use_DPLL);
    00118
    00119         return get_current_consistency();
    00120 }
    00121
    00122
    00123 ISATClause *
    00124 ISATTheory::insert_new_empty_clause()
    00125 {
    00126         new_clause_p = new ISATClause();
    00127         (*clause_database_p) += new_clause_p;
    00128         // The new clause should not be active when created. Inserting it into the
    00129         // clause database should not active it either. But for now we set it
    00130         // deactive anyway.
    00131         new_clause_p->set_active(false);
    00132         return new_clause_p;
    00133 }
    00134
    00135 void
    00136 ISATTheory::add_literal_to_new_clause(ISATPropositionDescription *description_p,
    00137                                                                           ISATLiteral::PolarityType polarity)
    00138 {
    00139         ISATProposition *proposition_p;
    00140         ISATLiteral             *literal_p;
    00141         bool                    clause_was_active = false;
    00142         bool                    successfully_added;
    00143
    00144         if (new_clause_p->is_active())
    00145         {
    00146                 clause_was_active = true;
    00147                 deactivate_clause(new_clause_p);
    00148         }
    00149
    00150         // Check if the proposition with the matching description already exists.
    00151         proposition_p = find_proposition_p(description_p);
    00152
    00153         // If the matching proposition is found, delete the description.
    00154         if (proposition_p != NULL)
    00155         {
    00156                 delete description_p;
    00157         }
    00158         // Otherwise, a new proposition with the description must be created.
    00159         else
    00160         {
    00161                 // Create a new proposition with the description.
    00162                 proposition_p = new ISATProposition(description_p);
    00163
    00164                 // Insert the new proposition into the database.
    00165                 push_back(proposition_p);
    00166
    00167                 // Since this is a new proposition, it's value should be unknown.
    00168                 assert(proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    00169
    00170                 unassigned_propositions_p->insert_proposition(proposition_p);
    00171         }
    00172
    00173         literal_p = new ISATLiteral(proposition_p, polarity);
    00174         successfully_added = new_clause_p->add_literal(literal_p);
    00175         if (successfully_added)
    00176         {
    00177                 proposition_p->insert_literal(literal_p);
    00178         }
    00179
    00180         if (clause_was_active)
    00181         {
    00182                 activate_clause(new_clause_p);
    00183         }
    00184 }
    00185 void
    00186 ISATTheory::remove_clause(ISATClause *clause_p)
    00187 {
    00188         ISATProposition *proposition_p;
    00189         ISATClause::const_iterator const_it;
    00190
    00191         deactivate_clause(clause_p);
    00192
    00193         // For each literal in the clause:
    00194         for (const_it = clause_p->begin(); const_it != clause_p->end(); const_it++)
    00195         {
    00196                 // Get the literal's proposition.
    00197                 proposition_p = (*const_it)->get_proposition_p();
    00198
    00199                 // Remove the literal from the proposition's list of literals.
    00200                 proposition_p->remove_literal(*const_it);
    00201
    00202                 // If no literals in the clause database uses this proposition:
    00203                 if (proposition_p->get_positive_literals_p()->empty() &&
    00204                         proposition_p->get_negative_literals_p()->empty())
    00205                 {
    00206                         //before a proposition gets removed from the database,
    00207                         //all pointers to it should be removed.
    00208
    00209                         /*  Commenting out the searched_propositions' code
    00210                                 for now, clearing dpll search before clause activate/deactivate
    00211                         //since dpll search is no longer cleared prior to clause removed
    00212                         //searched propositions list, and searched path length must be updated
    00213                         if(proposition_p->was_guessed() == true)
    00214                         {
    00215                                 searched_propositions_p->remove_proposition(proposition_p);
    00216
    00217                                 if(proposition_p->get_truth_value() == true)
    00218                                 {
    00219                                         searched_path_length -= 1;
    00220                                 }
    00221                                 else
    00222                                 {
    00223                                         //since the proposition was guessed, it can't have truth value of unknown
    00224                                         //this assertion does not always work for some reason.
    00225                                         //assert(proposition_p->get_truth_value() == false);
    00226
    00227                                         searched_path_length -= 2;
    00228                                 }
    00229
    00230                                 proposition_p->set_guessed(false);
    00231                         }
    00232
    00233                         if(searched_propositions_p->is_empty())
    00234                         {
    00235                                 searched_path_length = 0;
    00236                         }
    00237                         */
    00238
    00239                         unassigned_propositions_p->remove_proposition(proposition_p);
    00240
    00241                         // Delete this proposition.
    00242                         ISATPropositionDB::remove_proposition(proposition_p);
    00243                 }
    00244         }
    00245
    00246 //      ISATClauseDB::remove_clause(clause_p);
    00247         clause_database_p->remove_clause(clause_p);
    00248 }
    00249
    00250
    00251 ISATPropositionDB const *
    00252 ISATTheory::get_propositions_p() const
    00253 {
    00254 //      return proposition_database_p;
    00255         return (ISATPropositionDB const *)this;
    00256 }
    00257
    00258 ISATInconsistentClauses const *
    00259 ISATTheory::get_inconsistent_clauses_p() const
    00260 {
    00261         return inconsistent_clauses_p;
    00262 }
    00263
    00264 ISATUnassignedPropositions const *
    00265 ISATTheory::get_unassigned_propositions_p() const
    00266 {
    00267         return unassigned_propositions_p;
    00268 }
    00269
    00270 #if defined _DEBUG
    00271 void
    00272 ISATTheory::set_debug_level(int debug_level_numb)
    00273 {
    00274         debug_level = debug_level_numb;
    00275 }
    00276 #endif // #if defined _DEBUG
    00277
    00278 void
    00279 ISATTheory::propagate_using_DPLL()
    00280 {
    00281         ISATTheory::ConsistencyType     consistency;
    00282         ISATProposition                         *proposition_p;
    00283         ISATUnitClauses                         *current_unit_clauses_p = NULL;
    00284         //int                                                   dpll_guess = 0; //xxused for testing
    00285         //int                                                   dpll_unguess = 0; //xx
    00286
    00287         consistency = get_current_consistency();
    00288 #if defined(_DEBUG)
    00289         if (debug_level > 0)
    00290         {
    00291                 if (consistency == INDETERMINATE)
    00292                 {
    00293                         cerr << "DPLL SEARCH: in progress..." << endl;
    00294                 }
    00295                 if (debug_level == 1)
    00296                 {
    00297                         cerr << "-- Theory is " << consistency << " by unit propagation." << endl;
    00298                 }
    00299         }
    00300 #endif // #if defined(_DEBUG)
    00301
    00302         do
    00303         {
    00304                 if (consistency == INDETERMINATE)
    00305                 {
    00306                         assert(!unassigned_propositions_p->is_empty());
    00307                         assert(unassigned_propositions_p->get_proposition_p() != NULL);
    00308                         proposition_p = unassigned_propositions_p->get_proposition_p();
    00309                         assert(proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    00310 #if defined(_DEBUG)
    00311                         if (debug_level > 2)
    00312                         {
    00313                                 cerr << "-- Guessing (";
    00314                                 proposition_p->get_description_p()->print(cerr);
    00315                                 cerr << " = true)." << endl;
    00316                         }
    00317 #endif // #if defined(_DEBUG)
    00318                         current_unit_clauses_p = assign_proposition_truth_value(proposition_p, true);
    00319                         //dpll_guess++; //xx
    00320
    00321                         proposition_p->set_guessed(true);
    00322                         searched_path_length = searched_path_length + 1;
    00323                         searched_propositions_p->push_front(proposition_p);
    00324                 }
    00325                 else if (consistency == INCONSISTENT && !searched_propositions_p->is_empty())
    00326                 {
    00327                         assert(searched_path_length < 2*searched_propositions_p->get_size());
    00328                         assert(!inconsistent_clauses_p->is_empty());
    00329                         proposition_p = searched_propositions_p->get_front();
    00330                         while (proposition_p->get_truth_value() == ISATProposition::FALSEVAL)
    00331                         {
    00332 #if defined(_DEBUG)
    00333                         if (debug_level > 2)
    00334                         {
    00335                                 cerr << "-- Neither (";
    00336                                 proposition_p->get_description_p()->print(cerr);
    00337                                 cerr << " = ture) nor (";
    00338                                 proposition_p->get_description_p()->print(cerr);
    00339                                 cerr << ") works... Removing guessed value." << endl;
    00340                         }
    00341 #endif // #if defined(_DEBUG)
    00342                                 unassign_proposition(proposition_p);
    00343                                 //dpll_unguess++; //xx
    00344
    00345                                 proposition_p->set_guessed(false);
    00346                                 searched_propositions_p->pop_front();
    00347                                 assert(!searched_propositions_p->is_empty());
    00348                                 searched_path_length = searched_path_length - 2;
    00349                                 assert(searched_path_length != 0);
    00350                                 assert(!searched_propositions_p->is_empty());
    00351                                 proposition_p = searched_propositions_p->get_front();
    00352                         }
    00353 #if defined(_DEBUG)
    00354                         if (debug_level > 2)
    00355                         {
    00356                                 cerr << "-- Guessing (";
    00357                                 proposition_p->get_description_p()->print(cerr);
    00358                                 cerr << " = false)." << endl;
    00359                         }
    00360 #endif // #if defined(_DEBUG)
    00361                         current_unit_clauses_p = assign_proposition_truth_value(proposition_p, false);
    00362                         //dpll_guess++; //xx
    00363                         //dpll_unguess++; //xx
    00364
    00365                         searched_path_length = searched_path_length + 1;
    00366                 }
    00367 #if defined(_DEBUG)
    00368                 else
    00369                 {
    00370                         cerr << "*** ERROR: Problem in DPLL search! ***" << endl;
    00371                 }
    00372 #endif // #if defined(_DEBUG)
    00373                 propagate_unit_clauses(current_unit_clauses_p);
    00374                 if (current_unit_clauses_p != NULL)
    00375                 {
    00376                         delete current_unit_clauses_p;
    00377                         current_unit_clauses_p = NULL;
    00378                 }
    00379                 consistency = get_current_consistency();
    00380 #if defined(_DEBUG)
    00381                 if (debug_level > 2)
    00382                 {
    00383                         cerr << "-- Theory is " << consistency << "." << endl;
    00384                 }
    00385 #endif // #if defined(_DEBUG)
    00386         } while ((consistency == INCONSISTENT &&
    00387                      searched_path_length < 2*searched_propositions_p->get_size()) ||
    00388                          consistency == INDETERMINATE);
    00389         assert(get_current_consistency() == CONSISTENT ||
    00390                    get_current_consistency() == INCONSISTENT);
    00391
    00392 #if defined(_DEBUG)
    00393         if (debug_level > 0)
    00394         {
    00395                 cerr << "DPLL SEARCH: done!" << endl;
    00396         }
    00397 #endif // #if defined(_DEBUG)
    00398
    00399         //cout << "DPLL guess: " << dpll_guess << endl; //xx
    00400         //cout << "DPLL unguess:" << dpll_unguess << endl; //xx
    00401 }
    00402
    00403 void
    00404 ISATTheory::clear_DPLL_search()
    00405 {
    00406         ISATProposition *proposition_p;
    00407         while (!searched_propositions_p->is_empty())
    00408         {
    00409                 proposition_p = searched_propositions_p->get_front();
    00410                 unassign_proposition(proposition_p);
    00411                 proposition_p->set_guessed(false);
    00412                 searched_propositions_p->pop_front();
    00413         }
    00414         searched_path_length = 0;
    00415 }
    00416
    00417 void
    00418 ISATTheory::propagate_clauses(bool use_DPLL)
    00419 {
    00420         double start_time = 0.0;
    00421         double end_time = 0.0;
    00422
    00423         start_time = clock();
    00424
    00425         if (!use_DPLL)
    00426         {
    00427                 clear_DPLL_search();
    00428         }
    00429
    00430         //clear_DPLL_search(); //xx
    00431
    00432         propagate_unit_clauses();
    00433
    00434         /*xxif(use_DPLL && get_current_consistency()!=CONSISTENT)
    00435         {
    00436                 //clear_DPLL_search();
    00437                 propagate_using_DPLL();
    00438         }*/
    00439
    00440         if(use_DPLL && get_current_consistency()==INDETERMINATE)
    00441         {
    00442                 clear_DPLL_search(); //xx
    00443                 propagate_unit_clauses();
    00444                 propagate_using_DPLL();
    00445         }
    00446
    00447         end_time = clock();
    00448         total_time += ((end_time-start_time)/CLOCKS_PER_SEC);
    00449
    00450         return;
    00451 }
    00452
    00453 // Propagates the unit clauses of the theory until the set of unit clauses becomes
    00454 // empty, or an inconsistency is detected. If the set of unit  clauses becomes empty,
    00455 // then all propositions have truth values that are "unit propagation entailed" by
    00456 // the theory. If no unit clauses are provided, it defaults to the thoery's list of
    00457 // unit clauses.
    00458 void
    00459 ISATTheory::propagate_unit_clauses(ISATUnitClauses *current_unit_clauses_p /* = NULL */)
    00460 {
    00461         // If no unit clause was provided, then use the theory's list of unit clause.
    00462         if (current_unit_clauses_p == NULL)
    00463         {
    00464                 current_unit_clauses_p = unit_clauses_p;
    00465         }
    00466
    00467 #if defined _DEBUG
    00468         if (debug_level > 1)
    00469         {
    00470                 if (current_unit_clauses_p == unit_clauses_p)
    00471                 {
    00472                         cerr << "UNIT PROPAGATION: in progress..." << endl;
    00473                 }
    00474                 else if (debug_level > 3)
    00475                 {
    00476                         cerr << "UNIT PROPAGATION: in progress..." << endl;
    00477                 }
    00478         }
    00479 #endif // #if defined(_DEBUG)
    00480
    00481         // Continue to propagate the unit clauses until at least one inconsistent clause was
    00482         // found or there are no more unit clauses to propagate.
    00483         while (get_current_consistency() != INCONSISTENT && !current_unit_clauses_p->is_empty())
    00484         {
    00485                 assert(current_unit_clauses_p->get_clause_p() != NULL);
    00486                 propagate_unit_clause(current_unit_clauses_p->get_clause_p());
    00487         }
    00488 #if defined _DEBUG
    00489         if (debug_level > 1)
    00490         {
    00491                 if (current_unit_clauses_p == unit_clauses_p)
    00492                 {
    00493                         cerr << "-- The theory is " << get_current_consistency()
    00494                                  << " by unit propagation." << endl;
    00495                         cerr << "UNIT PROPAGATION: done!" << endl;
    00496                 }
    00497                 else if (debug_level > 3)
    00498                 {
    00499                         cerr << "-- The theory is " << get_current_consistency()
    00500                                  << " by unit propagation." << endl;
    00501                         cerr << "UNIT PROPAGATION: done!" << endl;
    00502                 }
    00503         }
    00504 #endif // #if defined _DEBUG
    00505 }
    00506
    00507 // Propagates the unit clause.
    00508 void
    00509 ISATTheory::propagate_unit_clause(ISATClause *clause_p)
    00510 {
    00511         assert(clause_p != NULL);
    00512         assert(clause_p->is_unit_clause());
    00513         assert(clause_p->get_unresolved_literal_p() != NULL);
    00514
    00515 #if defined _DEBUG
    00516         ISATLiteral const *unresolved_literal_p = clause_p->get_unresolved_literal_p();
    00517
    00518         assert(unresolved_literal_p->get_proposition_p() != NULL);
    00519         assert(unresolved_literal_p->get_polarity() == ISATLiteral::POSITIVE ||
    00520                    unresolved_literal_p->get_polarity() == ISATLiteral::NEGATIVE);
    00521 #endif
    00522
    00523         if (clause_p->is_active())
    00524         {
    00525 #if defined _DEBUG
    00526                 if (debug_level > 4)
    00527                 {
    00528                         cerr << "-- Propagating unit clause " << *clause_p << "..." << endl;
    00529                         cerr << "-- Setting " << *clause_p->get_unresolved_literal_p()
    00530                                  << " as the consequent of " << *clause_p << "." << endl;
    00531                 }
    00532 #endif // #if defined(_DEBUG)
    00533
    00534                 // Set the clause as unit resolved.
    00535                 clause_p->set_unit_resolved(true);
    00536
    00537                 // Assign the proposition of the one unresolved literal true if the literal is
    00538                 // positive and false if it is negative. This function should return the new unit
    00539                 // clauses generated from this proposition assignment.
    00540                 ISATUnitClauses *current_unit_clauses_p = assign_proposition_truth_value(
    00541                         clause_p->get_unresolved_literal_p()->get_proposition_p(),
    00542                         clause_p->get_unresolved_literal_p()->get_polarity() == ISATLiteral::POSITIVE);
    00543
    00544                 // Now the clause should be consistent.
    00545                 assert(clause_p->is_consistent());
    00546
    00547                 // Propagate all unit clauses that were generated from the above assignment.
    00548                 propagate_unit_clauses(current_unit_clauses_p);
    00549
    00550                 delete current_unit_clauses_p;
    00551
    00552 #if defined _DEBUG
    00553                 if (debug_level > 4)
    00554                 {
    00555                         cerr << "-- Completed propagating unit clause " << *clause_p << "." << endl;
    00556                 }
    00557 #endif // #if defined(_DEBUG)
    00558         }
    00559 }
    00560
    00561 // Undoes all current truth assignments and support that resulted from propagating
    00562 // "clause_p" in theory. It also updates any clause status of the theory that has
    00563 // changed.
    00564 void
    00565 ISATTheory::unpropagate_clause(ISATClause *clause_p)
    00566 {
    00567         assert(clause_p != NULL);
    00568
    00569         // Unpropagate the "clause" only if it was unit resolved.
    00570         if (clause_p->was_unit_resolved())
    00571         {
    00572 #if defined _DEBUG
    00573                 if (debug_level > 4)
    00574                 {
    00575                         cerr << "-- Unpropagating clause " << *clause_p << "..." << endl;
    00576                         cerr << "-- Removing " << *clause_p->get_consequent_literal_p()
    00577                                  << " from consequent of " << *clause_p << "." << endl;
    00578                 }
    00579 #endif // #if defined(_DEBUG)
    00580
    00581                 assert(clause_p->is_active());
    00582
    00583                 // If the clause was unit resolved, the clause should have a consequent
    00584                 // literal.
    00585                 assert(clause_p->get_consequent_literal_p() != NULL);
    00586
    00587                 // If the clause was unit reoslved, the clause should have a consequent
    00588                 // proposition.
    00589                 assert(clause_p->get_consequent_literal_p()->get_proposition_p() != NULL);
    00590
    00591                 // The consequent literal's truth value should be TRUEVAL.
    00592                 assert(clause_p->get_consequent_literal_p()->get_truth_value() ==
    00593                         ISATLiteral::TRUEVAL);
    00594
    00595                 ISATProposition *proposition_p =
    00596                         clause_p->get_consequent_literal_p()->get_proposition_p();
    00597
    00598                 ISATProposition::TruthValueType old_truth_value =
    00599                         proposition_p->get_truth_value();
    00600
    00601                 // Set the clause not unit resolved.
    00602                 clause_p->set_unit_resolved(false);
    00603
    00604                 // Unassign the truth value of the consequent proposition.
    00605                 unassign_proposition(proposition_p);
    00606
    00607                 ISATLiterals::const_iterator const_it;
    00608
    00609                 // Unpropagates all clauses that were propagated as the result of the truth value
    00610                 // of the proposition.
    00611                 if (old_truth_value == ISATProposition::TRUEVAL)
    00612                 {
    00613                         // If the old truth value was TRUEVAL, then for the clauses that have negative
    00614                         // literal with the proposition may have been either unit propagated or
    00615                         // inserted into the set of inconsistent clauses.
    00616                         for (const_it = proposition_p->get_negative_literals_p()->begin();
    00617                         const_it != proposition_p->get_negative_literals_p()->end(); const_it++)
    00618                         {
    00619                                 assert((*const_it)->get_parent_clause_p() != NULL);
    00620
    00621                                 // If the clause was unit resolved, unpropagate it.
    00622                                 if ((*const_it)->get_parent_clause_p()->was_unit_resolved())
    00623                                 {
    00624                                         unpropagate_clause((*const_it)->get_parent_clause_p());
    00625                                 }
    00626                                 // Otherwise, if the clause was inconsistent, remove it from the list
    00627                                 // of inconsistent clauses.
    00628                                 else if ((*const_it)->get_parent_clause_p()->is_inconsistent())
    00629                                 {
    00630                                         inconsistent_clauses_p->remove_clause(
    00631                                                 (*const_it)->get_parent_clause_p());
    00632                                 }
    00633                         }
    00634                 }
    00635                 else
    00636                 {
    00637                         // If the old truth value was FALSEVAL, then for the clauses that have positive
    00638                         // literal with the proposition may have been either unit propagated or
    00639                         // inserted into the set of inconsistent clauses.
    00640                         for (const_it = proposition_p->get_positive_literals_p()->begin();
    00641                         const_it != proposition_p->get_positive_literals_p()->end(); const_it++)
    00642                         {
    00643                                 assert((*const_it)->get_parent_clause_p());
    00644
    00645                                 // If the clause was unit resolved, unpropagate it.
    00646                                 if ((*const_it)->get_parent_clause_p()->was_unit_resolved())
    00647                                 {
    00648                                         unpropagate_clause((*const_it)->get_parent_clause_p());
    00649                                 }
    00650                                 // Otherwise, if the clause was inconsistent, remove it from the list
    00651                                 // of inconsistent clauses.
    00652                                 else if ((*const_it)->get_parent_clause_p()->is_inconsistent())
    00653                                 {
    00654                                         inconsistent_clauses_p->remove_clause(
    00655                                                 (*const_it)->get_parent_clause_p());
    00656                                 }
    00657                         }
    00658                 }
    00659 #if defined _DEBUG
    00660                 if (debug_level > 4)
    00661                 {
    00662                         cerr << "-- Completed unpropagating clause " << *clause_p << "." << endl;
    00663                 }
    00664 #endif // #if defined(_DEBUG)
    00665         }
    00666 }
    00667
    00668 ISATUnitClauses *
    00669 ISATTheory::assign_proposition_truth_value(ISATProposition *proposition_p,
    00670                                                                                    bool truth_value)
    00671 {
    00672         if (truth_value == true)
    00673         {
    00674                 return assign_proposition_true(proposition_p);
    00675         }
    00676         else
    00677         {
    00678                 return assign_proposition_false(proposition_p);
    00679         }
    00680 }
    00681
    00682 void
    00683 ISATTheory::activate_clause(ISATClause *clause_p)
    00684 {
    00685         if (!clause_p->is_active())
    00686         {
    00687                 if (get_current_consistency() == ISATTheory::INCONSISTENT ||
    00688                         !searched_propositions_p->is_empty())
    00689                 {
    00690                         clear_DPLL_search(); //xx
    00691                 }
    00692                 clause_p->reset_status();
    00693                 clause_p->set_active(true);
    00694                 if (clause_p->is_unit_clause())
    00695                 {
    00696                         unit_clauses_p->insert_clause(clause_p);
    00697 //                      propagate_unit_clauses(); //xx
    00698                 }
    00699                 else if (clause_p->is_inconsistent())
    00700                 {
    00701                         inconsistent_clauses_p->insert_clause(clause_p);
    00702                 }
    00703                 //if (get_current_consistency() == ISATTheory::INCONSISTENT)
    00704                 //{
    00705                 //      clear_DPLL_search();
    00706                 //}
    00707         }
    00708 }
    00709
    00710 void
    00711 ISATTheory::deactivate_clause(ISATClause *clause_p)
    00712 {
    00713         if (clause_p->is_active())
    00714         {
    00715                 clear_DPLL_search(); //xx
    00716
    00717                 double start_time = 0.0;
    00718                 double end_time = 0.0;
    00719
    00720                 start_time = clock();
    00721                 unpropagate_clause(clause_p);
    00722                 end_time = clock();
    00723
    00724                 total_time += ((end_time-start_time)/CLOCKS_PER_SEC);
    00725
    00726                 /*Clauses that are not unit or inconsistent can still be
    00727                 in these lists because the code does not update the list
    00728                 until right before propagation when the is_empty() function is called.
    00729
    00730                 may change code so that ONLY unit or inconsisent clauses are in their
    00731                 respective lists at anytime.
    00732
    00733                 if (clause_p->is_unit_clause())
    00734                 {
    00735                         unit_clauses_p->remove_clause(clause_p);
    00736                 }
    00737
    00738                 else if (clause_p->is_inconsistent())
    00739                 {
    00740                         inconsistent_clauses_p->remove_clause(clause_p);
    00741                 }*/
    00742
    00743                 unit_clauses_p->remove_clause(clause_p);
    00744
    00745                 inconsistent_clauses_p->remove_clause(clause_p);
    00746
    00747
    00748                 clause_p->set_active(false);
    00749 //              propagate_unit_clauses(); //xx
    00750         }
    00751 }
    00752
    00753
    00754 //........................................................................................
    00755
    00756 ISATTheory::ConsistencyType
    00757 ISATTheory::get_current_consistency() const
    00758 {
    00759         if (inconsistent_clauses_p->is_empty())
    00760         {
    00761                 if (unassigned_propositions_p->is_empty())
    00762                 {
    00763                         return CONSISTENT;
    00764                 }
    00765                 else
    00766                 {
    00767                         return INDETERMINATE;
    00768                 }
    00769         }
    00770         else
    00771         {
    00772                 return INCONSISTENT;
    00773         }
    00774 }
    00775
    00776
    00777 ISATClauses const *
    00778 ISATTheory::get_supporting_clauses_p(ISATProposition *proposition_p) const
    00779 {
    00780         ISATLiterals const                              *supporting_literals_p = NULL;
    00781         ISATLiterals::const_iterator    literals_const_it;
    00782         ISATClause                                              *parent_clause_p = NULL;
    00783         ISATClauses                                             *supporting_clauses_p = new ISATClauses;
    00784         ISATClauses const                               *temp_supporting_clauses_p;
    00785
    00786         // Only search for supports only if proposition_p's truth value is known and
    00787         // proposition_p is not marked. If the proposition_p is marked, that implies that this
    00788         // proposition was searched before.
    00789         if (proposition_p->get_truth_value() != ISATProposition::UNKNOWNVAL &&
    00790                 !proposition_p->is_marked())
    00791         {
    00792 #if defined(_DEBUG)
    00793                 if (debug_level > 3)
    00794                 {
    00795                         cerr << "SEARCHING SUPPORT: Searching support for " << *proposition_p
    00796                                  << " in progress..." << endl;
    00797                 }
    00798 #endif // #if defined(_DEBUG)
    00799
    00800                 // Mark the proposition before starting to search for its support. This will imply
    00801                 // that this proposition has been visited before.
    00802                 proposition_p->set_marked(true);
    00803
    00804                 // If the proposition_p's truth value was guessed and it hasn't been marked, it's
    00805                 // support is itself.
    00806                 if (proposition_p->was_guessed())
    00807                 {
    00808 #if defined(_DEBUG)
    00809                         if (debug_level > 4)
    00810                         {
    00811 //                              cerr << "-- Found support: " << *proposition_p << "." << endl;
    00812                                 cerr << "-- DPLL guessed the value of " << *proposition_p << "."        << endl;
    00813                                 cerr << "   Assuming no support is available for " << *proposition_p << "." << endl;
    00814                         }
    00815 #endif // #if defined(_DEBUG)
    00816 //                      (*supporting_clauses_p) += *proposition_p;
    00817 //                      assert(!supporting_clauses_p->is_empty());
    00818                 }
    00819                 // Otherwise, proposition_p was not guessed, so some clause must support it.
    00820                 else
    00821                 {
    00822                         assert(proposition_p->get_positive_literals_p() != NULL);
    00823                         assert(proposition_p->get_negative_literals_p() != NULL);
    00824
    00825                         // Depending on the truth value of proposition_p, the search for support
    00826                         // will be different.
    00827                         switch (proposition_p->get_truth_value())
    00828                         {
    00829                         case ISATProposition::TRUEVAL:
    00830                                 // If the truth value is TRUEVAL, it's support must be from the positive
    00831                                 // literals.
    00832                                 supporting_literals_p = proposition_p->get_positive_literals_p();
    00833                                 break;
    00834                         case ISATProposition::FALSEVAL:
    00835                                 // If the truth value is FALSEVAL, it's support must be from the negative
    00836                                 // literals.
    00837                                 supporting_literals_p = proposition_p->get_negative_literals_p();
    00838                                 break;
    00839                         case ISATProposition::UNKNOWNVAL:
    00840                         default:
    00841 #if defined(_DEBUG)
    00842                                 cerr << "*** ERROR: Something is wrong with proposition truth value. ***"
    00843                                          << endl;
    00844 #endif // #if defined(_DEBUG)
    00845                                 break;
    00846                         }
    00847
    00848                         assert(supporting_literals_p != NULL);
    00849
    00850                         // Search through the supporting literals to find the support;
    00851                         for(literals_const_it = supporting_literals_p->begin();
    00852                         literals_const_it != supporting_literals_p->end();
    00853                         literals_const_it++)
    00854                         {
    00855                                 assert((*literals_const_it) != NULL);
    00856                                 assert((*literals_const_it)->get_parent_clause_p() != NULL);
    00857
    00858                                 parent_clause_p = (*literals_const_it)->get_parent_clause_p();
    00859
    00860                                 if (parent_clause_p->was_unit_resolved() &&
    00861                                         parent_clause_p->get_consequent_literal_p()->get_proposition_p()
    00862                                         == proposition_p)
    00863                                 {
    00864                                         // The clause that contains this literal supports the proposition.
    00865                                         temp_supporting_clauses_p =     get_supporting_clauses_p(parent_clause_p);
    00866                                         (*supporting_clauses_p) += (*temp_supporting_clauses_p);
    00867                                         delete temp_supporting_clauses_p;
    00868                                 }
    00869                                 // Otherwise, if the clause has only one literal, then the clause supports
    00870                                 // the proposition. This can be another set of supports. For now don't do
    00871                                 // anything with it.
    00872                                 // Note: The theory didn't use this clause to support the proposition_p,
    00873                                 //               but this clause could have been used to support the
    00874                                 //               proposition_p.
    00875                                 else if (parent_clause_p->get_numb_of_literals() == 1)
    00876                                 {
    00877 #if defined(_DEBUG)
    00878 //                                      if (debug_level > 4)
    00879 //                                      {
    00880 //                                              cerr << "-- Found support: (" << *clause_p << ")." << endl;
    00881 //                                      }
    00882 #endif // #if defined(_DEBUG)
    00883 //                                      (*supporting_clauses_p) += (*clause_p);
    00884                                 }
    00885                                 // Other single literal clauses or unit resolved clauses that
    00886                                 // support the proposition may exist. Could branch and search for
    00887                                 // other sets of support, but for now, just get one support.
    00888                                 if (!supporting_clauses_p->is_empty())
    00889                                 {
    00890                                         break;
    00891                                 }
    00892                         }
    00893                 }
    00894 #if defined(_DEBUG)
    00895                 if (debug_level > 3)
    00896                 {
    00897                         cerr << "SEARCHING SUPPORT: Searching support for " << *proposition_p
    00898                                  << " done!" << endl;
    00899                 }
    00900 #endif // #if defined(_DEBUG)
    00901
    00902         }
    00903 #if defined(_DEBUG)
    00904         else if (debug_level > 3)
    00905         {
    00906                 cerr << "-- Searhing support for " << *proposition_p << " is unnecessary." << endl;
    00907         }
    00908 #endif // #if defined(_DEBUG)
    00909
    00910         return supporting_clauses_p;
    00911 }
    00912
    00913 ISATClauses const *
    00914 ISATTheory::get_supporting_clauses_p(ISATClause *clause_p) const
    00915 {
    00916         ISATClause::const_iterator      clause_const_it;
    00917         ISATClauses                                     *supporting_clauses_p = new ISATClauses;
    00918         ISATClauses const                       *temp_supporting_clauses_p;
    00919
    00920 #if defined(_DEBUG)
    00921         if (debug_level > 3)
    00922         {
    00923                 cerr << "SEARCHING SUPPORT: Searching support for (" << *clause_p
    00924                          << ") in progress..." << endl;
    00925         }
    00926 #endif // #if defined(_DEBUG)
    00927
    00928         // The clause supports the proposition_p only if the clause was unit
    00929         // resolved.
    00930         if(clause_p->was_unit_resolved())
    00931         {
    00932                 assert(clause_p->get_consequent_literal_p() != NULL);
    00933
    00934                 // If the clause has only one literal, then the clause support
    00935                 // proposition_p.
    00936                 if (clause_p->get_numb_of_literals() == 1)
    00937                 {
    00938 #if defined(_DEBUG)
    00939                         if (debug_level > 4)
    00940                         {
    00941                                 cerr << "-- Found support: (" << *clause_p << ")." << endl;
    00942                         }
    00943 #endif // #if defined(_DEBUG)
    00944                         (*supporting_clauses_p) += (*clause_p);
    00945                 }
    00946                 // Otherwise, must determine the support for the each literal in the clause.
    00947                 else
    00948                 {
    00949                         // Search through the literals in the clause to find clause's
    00950                         // support.
    00951                         for (clause_const_it = clause_p->begin();
    00952                         clause_const_it != clause_p->end(); clause_const_it++)
    00953                         {
    00954                                 assert((*clause_const_it)->get_proposition_p() != NULL);
    00955
    00956                                 // Search for the support of the literal only if its
    00957                                 // proposition has not been searched, i.e. marked.
    00958                                 if (!(*clause_const_it)->get_proposition_p()->is_marked())
    00959                                 {
    00960                                         temp_supporting_clauses_p =     get_supporting_clauses_p(
    00961                                                 (*clause_const_it)->get_proposition_p());
    00962                                         (*supporting_clauses_p) += (*temp_supporting_clauses_p);
    00963                                         delete temp_supporting_clauses_p;
    00964                                 }
    00965                         }
    00966                 }
    00967         }
    00968         // Otherwise, the clause's satisfying literals supports it. Though each supporting
    00969         // literals can be a different support, for now just return one.
    00970         else
    00971         {
    00972                 assert (clause_p->get_satisfying_literal_p() != NULL || clause_p->get_numb_of_literals() == 0);
    00973
    00974                 if (clause_p->get_numb_of_literals() > 0)
    00975                 {
    00976                         assert (clause_p->get_satisfying_literal_p()->get_proposition_p() != NULL);
    00977
    00978                         temp_supporting_clauses_p =     get_supporting_clauses_p(
    00979                                 clause_p->get_satisfying_literal_p()->get_proposition_p());
    00980                         (*supporting_clauses_p) += (*temp_supporting_clauses_p);
    00981                         delete temp_supporting_clauses_p;
    00982                 }
    00983         }
    00984
    00985 #if defined(_DEBUG)
    00986         if (debug_level > 3)
    00987         {
    00988                 cerr << "SEARCHING SUPPORT: Searching support for (" << *clause_p
    00989                          << ") done!" << endl;
    00990         }
    00991 #endif // #if defined(_DEBUG)
    00992         return supporting_clauses_p;
    00993 }
    00994
    00995
    00996 ISATUnitClauses *
    00997 ISATTheory::assign_proposition_true(ISATProposition *proposition_p)
    00998 {
    00999         ISATUnitClauses *                               current_unit_clauses_p = new ISATUnitClauses();
    01000         ISATLiterals::const_iterator    const_it;
    01001         ISATClause *                                    clause_p;
    01002
    01003         // Proceed only if the truth value is not TRUEVAL.
    01004         if (proposition_p->get_truth_value() != ISATProposition::TRUEVAL)
    01005         {
    01006                 //keeping track of # time a proposition is assigned new value
    01007                 assign_proposition_count++;
    01008
    01009                 ISATProposition::TruthValueType const old_truth_value =
    01010                         proposition_p->get_truth_value();
    01011
    01012                 if (proposition_p->get_truth_value() == ISATProposition::FALSEVAL)
    01013                 {
    01014                         unassign_proposition(proposition_p);
    01015                 }
    01016
    01017 #if defined(_DEBUG)
    01018                 if (debug_level > 4)
    01019                 {
    01020                         cerr << "-- Assigning " << *proposition_p << " to " << ISATProposition::TRUEVAL
    01021                                  << "." << endl;
    01022                 }
    01023 #endif // #if defined(_DEBUG)
    01024
    01025                 // Set the proposition's truth value to TRUEVAL.
    01026                 proposition_p->set_truth_value(ISATProposition::TRUEVAL);
    01027
    01028                 if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01029                 {
    01030 //                      unassigned_propositions_p->remove(proposition_p);
    01031 //                      assigned_propositions_p->push_front(proposition_p);
    01032                 }
    01033
    01034                 // Update the status of all clauses that contain the proposition. Status
    01035                 // involves updating the satisfying literal and the number of unassigned
    01036                 // literal of the clauses, and the set of unit clauses and inconstisent
    01037                 // clauses of the theory.
    01038                 for (const_it = proposition_p->get_positive_literals_p()->begin();
    01039                 const_it != proposition_p->get_positive_literals_p()->end(); const_it++)
    01040                 {
    01041                         clause_p = (*const_it)->get_parent_clause_p();
    01042
    01043                         // Literal should be owned by some clause.
    01044                         assert(clause_p != NULL);
    01045
    01046                         if (clause_p->is_active())
    01047                         {
    01048                                 // Since the literal is positive and the truth value of the propostion is
    01049                                 // TRUEVAL, the literal's truth value should also be TRUEVAL.
    01050                                 assert((*const_it)->get_truth_value() == ISATLiteral::TRUEVAL);
    01051
    01052                                 // Set literal as the literal that satisfies the clause.
    01053                                 clause_p->set_satisfying_literal(*const_it);
    01054
    01055                                 /* Question */
    01056                                 /* If the clause is in the inconsistent clause list, do I need to pop it? */
    01057                                 /* Do I need to pop it off of the list of unit clauses? */
    01058
    01059                                 // If the old truth value was UNKNOWNVAL then the number of unresolved
    01060                                 // literals in the clause needs to be updated.
    01061 //                              if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01062 //                              {
    01063 //                                      // Decrement the number of unresolved literals in the clause.
    01064 //                                      clause_p->decrement_numb_of_unresolved_literals();
    01065 //                              }
    01066                                 clause_p->decrement_numb_of_unresolved_literals();
    01067                         }
    01068                 }
    01069                 for (const_it = proposition_p->get_negative_literals_p()->begin();
    01070                 const_it != proposition_p->get_negative_literals_p()->end(); const_it++)
    01071                 {
    01072                         clause_p = (*const_it)->get_parent_clause_p();
    01073
    01074                         if (clause_p->is_active())
    01075                         {
    01076                                 // Literal should be owned by some clause.
    01077                                 assert(clause_p != NULL);
    01078
    01079                                 // Since the literal is negative and the truth value of the propostion is
    01080                                 // TRUEVAL, the literal's truth value should also be FALSEVAL.
    01081                                 assert((*const_it)->get_truth_value() == ISATLiteral::FALSEVAL);
    01082
    01083                                 clause_p->decrement_numb_of_unresolved_literals();
    01084
    01085                                 // If the old truth value was UNKNOWNVAL then the number of unresolved
    01086                                 // literals in the clause needs to be updated.
    01087 //                              if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01088 //                              {
    01089 //                                      // Decrement the number of unresolved literals in the clause.
    01090 //                                      clause_p->decrement_numb_of_unresolved_literals();
    01091 //                              }
    01092                                 // Otherwise, the old truth value was FALSEVAL. This implies that the
    01093                                 // proposition has satisfied the clauses in the past.
    01094 //                              else
    01095 //                              {
    01096                                         // Remove the literal from the set of satisfying literals in the
    01097                                         // clause.
    01098 //                                      clause_p->remove_from_satisfying_literals(*const_it);
    01099 //                              }
    01100
    01101                                 // Since the literal has truth value of FALSEVAL, the clause may be a unit
    01102                                 // clause or an inconsistent clause. Update as necessary.
    01103
    01104                                 // If the clause is a unit clause, insert it into the stack of unit
    01105                                 // clauses.
    01106                                 if (clause_p->is_unit_clause())
    01107                                 {
    01108                                         current_unit_clauses_p->insert_clause(clause_p);
    01109                                 }
    01110                                 // Otherwise, if the clause is inconsistent, insert it into the queue of
    01111                                 // inconsistent clauses.
    01112                                 else if (clause_p->is_inconsistent())
    01113                                 {
    01114                                         inconsistent_clauses_p->insert_clause(clause_p);
    01115                                 }
    01116                         }
    01117                 }
    01118         }
    01119         return current_unit_clauses_p;
    01120 }
    01121
    01122 ISATUnitClauses *
    01123 ISATTheory::assign_proposition_false(ISATProposition *proposition_p)
    01124 {
    01125         ISATUnitClauses *                               current_unit_clauses_p = new ISATUnitClauses();
    01126         ISATLiterals::const_iterator    const_it;
    01127         ISATClause *                                    clause_p;
    01128
    01129         // Proceed only if the truth value is not FALSEVAL.
    01130         if (proposition_p->get_truth_value() != ISATProposition::FALSEVAL)
    01131         {
    01132                 //keeping track of # time a proposition is assigned new value
    01133                 assign_proposition_count++;
    01134
    01135                 ISATProposition::TruthValueType const old_truth_value =
    01136                         proposition_p->get_truth_value();
    01137
    01138                 if (proposition_p->get_truth_value() == ISATProposition::TRUEVAL)
    01139                 {
    01140                         unassign_proposition(proposition_p);
    01141                 }
    01142
    01143 #if defined(_DEBUG)
    01144                 if (debug_level > 4)
    01145                 {
    01146                         cerr << "-- Assigning " << *proposition_p << " to " << ISATProposition::FALSEVAL;
    01147                         cerr << "." << endl;
    01148                 }
    01149 #endif
    01150
    01151                 // Set the proposition's truth value to FALSEVAL.
    01152                 proposition_p->set_truth_value(ISATProposition::FALSEVAL);
    01153
    01154                 if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01155                 {
    01156 //                      unassigned_propositions_p->remove(proposition_p);
    01157 //                      assigned_propositions_p->push_front(proposition_p);
    01158                 }
    01159
    01160                 // Update the status of all clauses that contain the proposition. Status
    01161                 // involves updating the satisfying literal and the number of unassigned
    01162                 // literal of the clauses, and the set of unit clauses and inconsistent
    01163                 // clauses of the theory.
    01164                 for (const_it = proposition_p->get_positive_literals_p()->begin();
    01165                 const_it != proposition_p->get_positive_literals_p()->end(); const_it++)
    01166                 {
    01167                         clause_p = (*const_it)->get_parent_clause_p();
    01168
    01169                         // Literal should be owned by some clause.
    01170                         assert(clause_p != NULL);
    01171
    01172                         if (clause_p->is_active())
    01173                         {
    01174                                 // Since the literal is positive and the truth value of the propostion is
    01175                                 // FALSEVAL, the literal's truth value should also be FALSEVAL.
    01176                                 assert((*const_it)->get_truth_value() == ISATLiteral::FALSEVAL);
    01177
    01178                                 clause_p->decrement_numb_of_unresolved_literals();
    01179
    01180                                 // If the old truth value was UNKNOWNVAL then the number of unresolved
    01181                                 // literals in the clause needs to be updated.
    01182 //                              if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01183 //                              {
    01184 //                                      // Decrement the number of unresolved literals in the clause.
    01185 //                                      clause_p->decrement_numb_of_unresolved_literals();
    01186 //                              }
    01187                                 // Otherwise, the old truth value was TURE. This implies that the
    01188                                 // proposition has satisfied the clauses in the past.
    01189 //                              else
    01190 //                              {
    01191                                         // Remove the literal from the set of satisfying literals in the
    01192                                         // clause.
    01193 //                                      clause_p->remove_from_satisfying_literals(*const_it);
    01194 //                              }
    01195
    01196                                 // Since the literal has truth value of FALSEVAL, the clause may be a unit
    01197                                 // clause or an inconsistent clause. Update as necessary.
    01198
    01199                                 // If the clause is a unit clause, insert it into the stack of unit
    01200                                 // clauses.
    01201                                 if (clause_p->is_unit_clause())
    01202                                 {
    01203                                         current_unit_clauses_p->insert_clause(clause_p);
    01204                                 }
    01205                                 // Otherwise, if the clause is inconsistent, insert it into the queue of
    01206                                 // inconsistent clauses.
    01207                                 else if (clause_p->is_inconsistent())
    01208                                 {
    01209                                         inconsistent_clauses_p->insert_clause(clause_p);
    01210                                 }
    01211                         }
    01212                 }
    01213                 for (const_it = proposition_p->get_negative_literals_p()->begin();
    01214                 const_it != proposition_p->get_negative_literals_p()->end(); const_it++)
    01215                 {
    01216                         clause_p = (*const_it)->get_parent_clause_p();
    01217
    01218                         // Literal should be owned by some clause.
    01219                         assert(clause_p != NULL);
    01220
    01221                         if (clause_p->is_active())
    01222                         {
    01223                                 // Since the literal is negative and the truth value of the propostion is
    01224                                 // FALSEVAL, the literal's truth value should also be TRUEVAL.
    01225                                 assert((*const_it)->get_truth_value() == ISATLiteral::TRUEVAL);
    01226
    01227                                 // Set literal as the literal that satisfies the clause.
    01228                                 clause_p->set_satisfying_literal(*const_it);
    01229
    01230                                 clause_p->decrement_numb_of_unresolved_literals();
    01231
    01232                                 // If the old truth value was UNKNOWNVAL then the number of unresolved
    01233                                 // literals in the clause needs to be updated.
    01234 //                              if (old_truth_value == ISATProposition::UNKNOWNVAL)
    01235 //                              {
    01236                                         // Decrement the number of unresolved literals in the clause.
    01237 //                                      clause_p->decrement_numb_of_unresolved_literals();
    01238 //                              }
    01239                         }
    01240                 }
    01241         }
    01242         return current_unit_clauses_p;
    01243 }
    01244
    01245 // Removes the truth value assigned to the "proposition" (i.e. sets the truth value to
    01246 // UNKNOWNVAL), and updates the status of all clauses that contains the proposition.
    01247 void
    01248 ISATTheory::unassign_proposition(ISATProposition *proposition_p)
    01249 {
    01250         // Proceed only if the truth value is not UNKNOWNVAL.
    01251         if (proposition_p->get_truth_value() != ISATProposition::UNKNOWNVAL)
    01252         {
    01253                 //keeping track of # time a proposition is unassigned
    01254                 unassign_proposition_count++;
    01255
    01256 #if defined(_DEBUG)
    01257                 if (debug_level > 4)
    01258                 {
    01259                         cerr << "-- Removing assignment " << proposition_p->get_truth_value() << " from ";
    01260                         cerr << *proposition_p << "." << endl;
    01261                 }
    01262 #endif
    01263                 // Set the proposition's truth value to UNKNOWNVAL.
    01264                 proposition_p->set_truth_value(ISATProposition::UNKNOWNVAL);
    01265
    01266                 //can't set guessed to false here because when dpll assigns proposition from true to false,
    01267                 //assign_proposition_false first calls unassign.
    01268                 //thus setting guessed to false here would mark such propositions not guessed,
    01269                 //eventhough they are guessed false by dpll
    01270                 //moved this into clear dpll search instead
    01271                 //proposition_p->set_guessed(false);
    01272
    01273                 unassigned_propositions_p->insert_proposition(proposition_p);
    01274 //              assigned_propositions_p->remove(proposition_p);
    01275
    01276                 ISATLiterals::const_iterator    const_it;
    01277                 ISATClause *                                    clause_p;
    01278
    01279                 // Update the status of all clauses that contain the proposition. Status involves
    01280                 // updating the satisfying literal and the number of unassigned literal of the
    01281                 // clauses, and the set of unit clauses and inconsistent clauses of the theory.
    01282                 for (const_it = proposition_p->get_positive_literals_p()->begin();
    01283                 const_it != proposition_p->get_positive_literals_p()->end(); const_it++)
    01284                 {
    01285                         clause_p = (*const_it)->get_parent_clause_p();
    01286
    01287                         assert(clause_p != NULL);
    01288
    01289                         if (clause_p->is_active())
    01290                         {
    01291                                 // Increment the number of unresolved literals in the clause.
    01292                                 clause_p->increment_numb_of_unresolved_literals();
    01293
    01294                                 // Remove the literal from the set of satisfying literals in the clause.
    01295                                 clause_p->remove_from_satisfying_literals(*const_it);
    01296
    01297                                 // If the clause is a unit clause, insert it into the stack of unit clauses.
    01298                                 if (clause_p->is_unit_clause())
    01299                                 {
    01300                                         unit_clauses_p->insert_clause(clause_p);
    01301                                 }
    01302                                 else if (clause_p->was_unit_resolved() &&
    01303                                         clause_p->get_consistency() == ISATClause::CONSISTENT)
    01304                                 {
    01305                                         unpropagate_clause(clause_p);
    01306                                 }
    01307                         }
    01308                 }
    01309                 for (const_it = proposition_p->get_negative_literals_p()->begin();
    01310                 const_it != proposition_p->get_negative_literals_p()->end(); const_it++)
    01311                 {
    01312                         clause_p = (*const_it)->get_parent_clause_p();
    01313
    01314                         assert(clause_p != NULL);
    01315
    01316                         if (clause_p->is_active())
    01317                         {
    01318                                 // Increment the number of unresolved literals in the clause.
    01319                                 clause_p->increment_numb_of_unresolved_literals();
    01320
    01321                                 // Remove the literal from the set of satisfying literals in the clause.
    01322                                 clause_p->remove_from_satisfying_literals(*const_it);
    01323
    01324                                 // If the clause is a unit clause, insert it into the stack of unit clauses.
    01325                                 if (clause_p->is_unit_clause())
    01326                                 {
    01327                                         unit_clauses_p->insert_clause(clause_p);
    01328                                 }
    01329                                 else if (clause_p->was_unit_resolved() &&
    01330                                         clause_p->get_consistency() == ISATClause::CONSISTENT)
    01331                                 {
    01332                                         unpropagate_clause(clause_p);
    01333                                 }
    01334                         }
    01335                 }
    01336         }
    01337 }
    01338
    01339
    01340 //----------------------------------------------------------------------------------------
    01341 // Public Operators
    01342 //----------------------------------------------------------------------------------------
    01343
    01344
    01345 namespace Mers {
    01346         namespace Solvers {
    01347                 namespace SAT {
    01348                         namespace ISAT {
    01349                                 ostream &
    01350                                 operator <<(ostream &stream, ISATTheory const &theory)
    01351                                 {
    01352                                         stream << *theory.clause_database_p;
    01353                                 /*      ISATPropositionDB::const_iterator const_it = theory.begin();
    01354                                         if (const_it != theory.end())
    01355                                         {
    01356                                                 stream << **const_it;
    01357                                                 const_it++;
    01358                                                 while (const_it != theory.end())
    01359                                                 {
    01360                                                         stream << endl << **const_it;
    01361                                                         const_it++;
    01362                                                 }
    01363                                         }
    01364                                 */      return stream;
    01365                                 }
    01366
    01367                                 ostream &
    01368                                 operator <<(ostream &stream, ISATTheory::ConsistencyType const &theory_consistency)
    01369                                 {
    01370                                         switch (theory_consistency)
    01371                                         {
    01372                                         case ISATTheory::CONSISTENT:
    01373                                                 stream << "consistent";
    01374                                                 break;
    01375                                         case ISATTheory::INCONSISTENT:
    01376                                                 stream << "inconsistent";
    01377                                                 break;
    01378                                         case ISATTheory::INDETERMINATE:
    01379                                                 stream << "indeterminate";
    01380                                                 break;
    01381                                         default:
    01382                                                 cerr << "*** ERROR: operator <<(ostream, ISATTheory::ConsistencyType)" << endl;
    01383                                                 cerr << "           - Invalid theory consistency type. ***" << endl;
    01384                                                 break;
    01385                                         }
    01386                                         return stream;
    01387                                 }
    01388                         }
    01389                 }
    01390         }
    01391 }
    01392
    01393 ISATClausesSet const *
    01394 ISATTheory::get_SAT_conflicts_p(bool use_DPLL)
    01395 {
    01396         ISATClause                      *inconsistent_clause_p = NULL;
    01397         ISATClauses const       *supporting_clauses_p = NULL;
    01398         ISATClauses                     *conflict_p = NULL;
    01399
    01400         if (!SAT_conflicts_p->is_empty())
    01401         {
    01402                 SAT_conflicts_p->clear();
    01403         }
    01404
    01405         if (get_consistency(use_DPLL) == INCONSISTENT)
    01406         {
    01407 #if defined _DEBUG
    01408                 if (debug_level > 0)
    01409                 {
    01410                         cerr << "SEARCHING SAT CONFLICTS: in progress..." << endl;
    01411                 }
    01412 #endif // #if defined _DEBUG
    01413
    01414                 // At least one inconsistent clause must exist.
    01415                 assert(!inconsistent_clauses_p->is_empty());
    01416                 assert(inconsistent_clauses_p->get_clause_p() != NULL);
    01417                 assert(inconsistent_clauses_p->get_clause_p()->is_inconsistent());
    01418
    01419                 inconsistent_clause_p = inconsistent_clauses_p->get_clause_p();
    01420                 conflict_p = new ISATClauses();
    01421
    01422 #if defined _DEBUG
    01423                 if (debug_level > 1)
    01424                 {
    01425                         cerr << "-- Inconsistent clause: " << *inconsistent_clauses_p << "." << endl;
    01426                 }
    01427 #endif // #if defined _DEBUG
    01428
    01429                 // If the inconsistent clause has only one literal, the clause is a part
    01430                 // of the conflict.
    01431                 if (inconsistent_clause_p->get_numb_of_literals() == 1)
    01432                 {
    01433                         conflict_p->insert_clause(inconsistent_clause_p);
    01434                 }
    01435
    01436                 // Use an inconsistent clause to trace the cause of the inconsistency, i.e.
    01437                 // trace why all literals in an inconsistent clause is false.
    01438                 unmark_all_propositions();
    01439
    01440                 ISATClause::const_iterator clause_const_it;
    01441
    01442                 for (clause_const_it = inconsistent_clause_p->begin();
    01443                 clause_const_it != inconsistent_clause_p->end(); clause_const_it++)
    01444                 {
    01445                         assert((*clause_const_it)->get_proposition_p() != NULL);
    01446                         assert((*clause_const_it)->get_truth_value() == ISATLiteral::FALSEVAL);
    01447 //                      unmark_all_propositions();
    01448
    01449                         supporting_clauses_p =
    01450                                 get_supporting_clauses_p((*clause_const_it)->get_proposition_p());
    01451                         assert(supporting_clauses_p != NULL);
    01452                         (*conflict_p) += (*supporting_clauses_p);
    01453                         delete supporting_clauses_p;
    01454                 }
    01455
    01456                 (*SAT_conflicts_p) += (*conflict_p);
    01457     //delete conflict_p;
    01458     //conflict_p = NULL;
    01459
    01460 #if defined _DEBUG
    01461                 if (debug_level > 0)
    01462                 {
    01463                         cerr << "SEARCHING SAT CONFLICTS: done!" << endl;
    01464                 }
    01465 #endif // #if defined _DEBUG
    01466 //              assert(!conflicting_propositions.is_empty());
    01467 //              cout << "Conflict: " << *SAT_conflicts_p << endl;
    01468                 return SAT_conflicts_p;
    01469         }
    01470         else
    01471         {
    01472 #if defined _DEBUG
    01473                 if (debug_level > 0)
    01474                 {
    01475                         cerr << "-- Theory is not inconsistent... No SAT conflict exists!" << endl;
    01476                 }
    01477 #endif // #if defined _DEBUG
    01478                 return SAT_conflicts_p;
    01479         }
    01480 }
    01481
    01482 ISATClausesSet const *
    01483 ISATTheory::get_SAT_conflicts_p_using_fact(bool use_DPLL, ISATClauses *clauses_p)
    01484 {
    01485         if (clauses_p == NULL)
    01486         {
    01487                 return get_SAT_conflicts_p(use_DPLL);
    01488         }
    01489         else
    01490         {
    01491                 ISATClause                                      *inconsistent_clause_p = NULL;
    01492                 ISATClause::const_iterator      clause_const_it;
    01493                 ISATClauses const                       *supporting_clauses_p = NULL;
    01494                 ISATClauses                                     *conflict_p = NULL;
    01495                 ISATClauses::iterator           clauses_iter;
    01496
    01497                 for (clauses_iter = clauses_p->begin(); clauses_iter != clauses_p->end(); clauses_iter++)
    01498                 {
    01499                         deactivate_clause(*clauses_iter);
    01500                         activate_clause(*clauses_iter);
    01501                 }
    01502
    01503                 if (!SAT_conflicts_p->is_empty())
    01504                 {
    01505                         SAT_conflicts_p->clear();
    01506                 }
    01507
    01508                 if (get_consistency(use_DPLL) == INCONSISTENT)
    01509                 {
    01510 #if defined _DEBUG
    01511                         if (debug_level > 0)
    01512                         {
    01513                                 cerr << "SEARCHING SAT CONFLICTS: in progress..." << endl;
    01514                         }
    01515 #endif // #if defined _DEBUG
    01516
    01517                         // At least one inconsistent clause must exist.
    01518                         assert(!inconsistent_clauses_p->is_empty());
    01519                         assert(inconsistent_clauses_p->get_clause_p() != NULL);
    01520                         assert(inconsistent_clauses_p->get_clause_p()->is_inconsistent());
    01521
    01522                         inconsistent_clause_p = inconsistent_clauses_p->get_clause_p();
    01523                         conflict_p = new ISATClauses();
    01524
    01525 #if defined _DEBUG
    01526                         if (debug_level > 1)
    01527                         {
    01528                                 cerr << "-- Inconsistent clause: " << *inconsistent_clauses_p << "." << endl;
    01529                         }
    01530 #endif // #if defined _DEBUG
    01531
    01532                         // Unmark all propositions so that the search is started from fresh.
    01533                         unmark_all_propositions();
    01534
    01535                         // Mark all fact clauses that have only one literal. This is done to assure
    01536                         // that the fact is not included as a part of the conflict.
    01537                         // *** This causes the support search to stop immediately... so the following
    01538                         // is removed for now ***
    01539                         //for (clauses_iter = clauses_p->begin();       clauses_iter != clauses_p->end();
    01540                         //clauses_iter++)
    01541                         //{
    01542                                 // Check to see if the clause has only one literal. If it has only one
    01543                                 // mark the proposition of the literal.
    01544                                 //if ((*clauses_iter)->get_numb_of_literals() == 1)
    01545                                 //{
    01546                                 //      (*clauses_iter)->front()->get_proposition_p()->set_marked(true);
    01547                                 //}
    01548                         //}
    01549
    01550                         // Use an inconsistent clause to trace the cause of the inconsistency, i.e.
    01551                         // trace why all literals in an inconsistent clause is false.
    01552                         for (clause_const_it = inconsistent_clause_p->begin();
    01553                         clause_const_it != inconsistent_clause_p->end(); clause_const_it++)
    01554                         {
    01555                                 assert((*clause_const_it)->get_proposition_p() != NULL);
    01556                                 assert((*clause_const_it)->get_truth_value() == ISATLiteral::FALSEVAL);
    01557                                 //                              unmark_all_propositions();
    01558
    01559                                 supporting_clauses_p =
    01560                                         get_supporting_clauses_p((*clause_const_it)->get_proposition_p());
    01561                                 assert(supporting_clauses_p != NULL);
    01562                                 (*conflict_p) += (*supporting_clauses_p);
    01563                                 delete supporting_clauses_p;
    01564                         }
    01565
    01566                         // If the inconsistent clause includes only one literal, then it too is a
    01567                         // part of the conflict. However, if this clause is one of the facts, then it
    01568                         // is not the cause of the conflict. Thus, in such case, we do not want to
    01569                         // include it as a part of the conflict.
    01570                         if (inconsistent_clause_p->get_numb_of_literals() == 1)
    01571                         {
    01572                                 bool is_in_fact = false;
    01573                                 for (clauses_iter = clauses_p->begin(); clauses_iter != clauses_p->end(); clauses_iter++)
    01574                                 {
    01575                                         if (*clauses_iter == inconsistent_clause_p)
    01576                                         {
    01577                                                 is_in_fact = true;
    01578                                                 break;
    01579                                         }
    01580                                 }
    01581                                 if (!is_in_fact)
    01582                                 {
    01583                                         (*conflict_p) += (*inconsistent_clause_p);
    01584                                 }
    01585                         }
    01586
    01587                         (*SAT_conflicts_p) += (*conflict_p);
    01588       //delete conflict_p;
    01589       //conflict_p = NULL;
    01590
    01591 #if defined _DEBUG
    01592                         if (debug_level > 0)
    01593                         {
    01594                                 cerr << "SEARCHING SAT CONFLICTS: done!" << endl;
    01595                         }
    01596 #endif // #if defined _DEBUG
    01597                         return SAT_conflicts_p;
    01598                 }
    01599                 else
    01600                 {
    01601 #if defined _DEBUG
    01602                         if (debug_level > 0)
    01603                         {
    01604                                 cerr << "-- Theory is not inconsistent... No SAT conflict exists!" << endl;
    01605                         }
    01606 #endif // #if defined _DEBUG
    01607                         return SAT_conflicts_p;
    01608                 }
    01609         }
    01610 }
    01611
    01612 ISATClausesSet const *
    01613 ISATTheory::get_UNSAT_conflicts_p(bool use_DPLL)
    01614 {
    01615         ISATClauses const       *temp_conflict_p;
    01616
    01617         if (!UNSAT_conflicts_p->is_empty())
    01618         {
    01619                 UNSAT_conflicts_p->clear();
    01620         }
    01621
    01622         if (get_consistency(use_DPLL) == CONSISTENT)
    01623         {
    01624         ISATClauses                     *conflict_p = new ISATClauses();
    01625 #if defined _DEBUG
    01626                 if (debug_level > 0)
    01627                 {
    01628                         cerr << "SEARCHING UNSAT CONFLICTS: in progress..." << endl;
    01629                 }
    01630 #endif // #if defined _DEBUG
    01631
    01632                 ISATClauseDB::const_iterator clause_database_const_it;
    01634
    01635                 // No inconsistent clause should exist.
    01636                 assert(inconsistent_clauses_p->is_empty());
    01637
    01638                 unmark_all_propositions();
    01639
    01640                 for (clause_database_const_it = clause_database_p->begin();
    01641                 clause_database_const_it != clause_database_p->end(); clause_database_const_it++)
    01642                 {
    01643                         if ((*clause_database_const_it)->is_active())
    01644                         {
    01645                                 assert((*clause_database_const_it)->is_consistent());
    01646                                 assert((*clause_database_const_it)->get_satisfying_literal_p() != NULL || (*clause_database_const_it)->get_numb_of_literals() == 0);
    01647
    01648                                 if ((*clause_database_const_it)->get_numb_of_literals() > 0)
    01649                                 {
    01650                                         assert((*clause_database_const_it)->get_satisfying_literal_p()->
    01651                                                 get_proposition_p() != NULL);
    01652
    01653                                         if (!(*clause_database_const_it)->get_satisfying_literal_p()->
    01654                                                 get_proposition_p()->is_marked())
    01655                                         {
    01656                                                 temp_conflict_p = get_supporting_clauses_p((*clause_database_const_it)->
    01657                                                         get_satisfying_literal_p()->get_proposition_p());
    01658                                                 (*conflict_p) += (*temp_conflict_p);
    01659                                                 delete temp_conflict_p;
    01660                                         }
    01661                                 }
    01662                         }
    01663                 }
    01664                 if (!conflict_p->is_empty())
    01665                 {
    01666                         (*UNSAT_conflicts_p) += *conflict_p;
    01667       //delete conflict_p;
    01668       //conflict_p = NULL;
    01669                 }
    01670                 else
    01671                 {
    01672                         delete conflict_p;
    01673                 }
    01674 //              assert(!conflict_p->is_empty());
    01675 #if defined _DEBUG
    01676                 if (debug_level > 0)
    01677                 {
    01678                         cerr << "SEARCHING UNSAT CONFLICTS: done!" << endl;
    01679                 }
    01680 #endif // #if defined _DEBUG
    01681         }
    01682         else
    01683         {
    01684 #if defined _DEBUG
    01685                 if (debug_level > 0)
    01686                 {
    01687                         cerr << "-- Theory is not consistent... No UNSAT conflict exists." << endl;
    01688                 }
    01689 #endif // #if defined _DEBUG
    01690         }
    01691         return UNSAT_conflicts_p;
    01692 }
    01693
    01694 ISATClausesSet const *
    01695 ISATTheory::get_UNSAT_conflicts_p_using_fact(bool use_DPLL, ISATClauses *clauses_p)
    01696 {
    01697         if (clauses_p == NULL)
    01698         {
    01699                 return get_UNSAT_conflicts_p(use_DPLL);
    01700         }
    01701         else
    01702         {
    01703                 ISATClauses const               *temp_conflict_p;
    01704                 ISATClauses::iterator   iter;
    01705
    01706                 for (iter = clauses_p->begin(); iter != clauses_p->end(); iter++)
    01707                 {
    01708                         deactivate_clause(*iter);
    01709                         activate_clause(*iter);
    01710                 }
    01711
    01712                 if (!UNSAT_conflicts_p->is_empty())
    01713                 {
    01714                         UNSAT_conflicts_p->clear();
    01715                 }
    01716
    01717                 if (get_consistency(use_DPLL) == CONSISTENT)
    01718                 {
    01719                 ISATClauses                             *conflict_p = new ISATClauses();
    01720 #if defined _DEBUG
    01721                         if (debug_level > 0)
    01722                         {
    01723                                 cerr << "SEARCHING UNSAT CONFLICTS: in progress..." << endl;
    01724                         }
    01725 #endif // #if defined _DEBUG
    01726
    01727                         // No inconsistent clause should exist.
    01728                         assert(inconsistent_clauses_p->is_empty());
    01729
    01730                         // Unmark all propositions so that the search is started from fresh.
    01731                         unmark_all_propositions();
    01732
    01733 // This was removed because, the proposition in the fact can also be the conflict
    01734 /*                      // Mark all fact clauses that have only one literal. This is done to assure
    01735                         // that the fact is not included as a part of the conflict.
    01736                         for (iter = clauses_p->begin(); iter != clauses_p->end(); iter++)
    01737                         {
    01738                                 assert((*iter)->is_consistent());
    01739                                 assert((*iter)->get_satisfying_literal_p() != NULL || (*iter)->get_numb_of_literals() == 0);
    01740 #if defined(_DEBUG)
    01741                                 if ((*iter)->get_numb_of_literals() > 0)
    01742                                 {
    01743                                         assert((*iter)->get_satisfying_literal_p()->get_proposition_p() != NULL);
    01744                                 }
    01745 #endif // #if defined(_DEBUG)
    01746
    01747                                 // Check to see if the clause has only one literal. If it has only one
    01748                                 // mark the proposition of the literal.
    01749                                 if ((*iter)->get_numb_of_literals() == 1)
    01750                                 {
    01751                                         (*iter)->
    01752                                                 get_satisfying_literal_p()->get_proposition_p()->set_marked(true);
    01753                                 }
    01754                         }
    01755 */
    01756                         for (iter = clauses_p->begin(); iter != clauses_p->end(); iter++)
    01757                         {
    01758                                 assert((*iter)->is_consistent());
    01759                                 assert((*iter)->get_satisfying_literal_p() != NULL || (*iter)->get_numb_of_literals() == 0);
    01760
    01761                                 if (!(*iter)->was_unit_resolved())
    01762                                 {
    01763                                         assert((*iter)->get_numb_of_literals() > 0);
    01764                                         assert((*iter)->get_satisfying_literal_p()->get_proposition_p() != NULL);
    01765
    01766                                         temp_conflict_p = get_supporting_clauses_p((*iter)->
    01767                                                 get_satisfying_literal_p()->get_proposition_p());
    01768                                         (*conflict_p) += (*temp_conflict_p);
    01769                                         delete temp_conflict_p;
    01770                                 }
    01771                         }
    01772                         if (!conflict_p->is_empty())
    01773                         {
    01774                                 (*UNSAT_conflicts_p) += *conflict_p;
    01775         //delete conflict_p;
    01776         //conflict_p = NULL;
    01777                         }
    01778                         else
    01779                         {
    01780                                 delete conflict_p;
    01781                         }
    01782 //                      assert(!conflict_p->is_empty());
    01783 #if defined _DEBUG
    01784                         if (debug_level > 0)
    01785                         {
    01786                                 cerr << "SEARCHING UNSAT CONFLICTS: done!" << endl;
    01787                         }
    01788 #endif // #if defined _DEBUG
    01789                 }
    01790                 else
    01791                 {
    01792 #if defined _DEBUG
    01793                         if (debug_level > 0)
    01794                         {
    01795                                 cerr << "-- Theory is not consistent... No UNSAT conflict exists." << endl;
    01796                         }
    01797 #endif // #if defined _DEBUG
    01798                 }
    01799                 return UNSAT_conflicts_p;
    01800         }
    01801 }
    01802
    01803
    01804 /*
    01805 void
    01806 ISATTheory::insert_clause(ISATClause *clause_p)
    01807 {
    01808         ISATProposition *proposition_p;
    01809         for (ISATClause::iterator it = clause_p->begin(); it != clause_p->end(); it++)
    01810         {
    01811                 // The proposition of the literal in the new clause.
    01812                 proposition_p = const_cast<ISATProposition *> ((*it)->get_proposition_p());
    01813
    01814                 // The proposition of the literal in the new clause should not be NULL.
    01815                 assert(proposition_p != NULL);
    01816
    01817                 // The proposition of the literal in the new clause should be in the theory.
    01818                 assert(find_proposition_p(proposition_p->get_description_p()) == proposition_p);
    01819
    01820                 // Insert the literal of the new clause as one of the literals that contain this
    01821                 // proposition.
    01822                 proposition_p->insert_literal(*it);
    01823         }
    01824
    01825         // Insert the clause into the theory's database.
    01826         clause_database_p->insert_clause(clause_p);
    01827
    01828         // Set the clause as inactive.
    01829         clause_p->set_active(false);
    01830 }
    01831
    01832 void
    01833 ISATTheory::insert_clauses(ISATClauses *clauses_p)
    01834 {
    01835         for (ISATClauses::iterator it = clauses_p->begin(); it != clauses_p->end(); it++)
    01836         {
    01837                 insert_clause(*it);
    01838         }
    01839 }
    01840 */
    01841
    01842 /*
    01843 ISATProposition const *
    01844 ISATTheory::get_proposition_p(ISATPropositionDescription const *description_p)
    01845 {
    01846         // Check if the proposition with the matching descprition already exists.
    01847         ISATProposition const *existing_proposition_p = find_proposition_p(description_p);
    01848
    01849         // If found proposition is not NULL, return it.
    01850         if (existing_proposition_p != NULL)
    01851         {
    01852                 delete description_p;
    01853                 return existing_proposition_p;
    01854         }
    01855         // Otherwise, a new proposition with the description must be created.
    01856         else
    01857         {
    01858                 // Create a new proposition with the description.
    01859                 ISATProposition *new_proposition_p = new ISATProposition(description_p);
    01860
    01861                 // Insert the new proposition into the database.
    01862                 push_back(new_proposition_p);
    01863
    01864                 assert(new_proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    01865
    01866                 unassigned_propositions_p->push_back(new_proposition_p);
    01867
    01868                 // Return the new proposition.
    01869                 return new_proposition_p;
    01870         }
    01871 }
    01872 */
    01873
    01874 //ISATProposition const *
    01875 //ISATTheory::get_propostion_p(ISATPropositionDescription const * description_p)
    01876 //{
    01877 //      return propagation_database_p->get_proposition_p()
    01878 //}
    01879
    01880 /*
    01881 // Recursive algorithm for DPLL
    01882 void
    01883 ISATTheory::propagate_using_DPLL()
    01884 {
    01885         propagate_unit_clauses();
    01886         ISATProposition *proposition_p;
    01887         if (inconsistent_clauses_p->is_empty())
    01888         {
    01889                 if (!unassigned_propositions_p->empty())
    01890                 {
    01891                         assert(unassigned_propositions_p->front());
    01892                         proposition_p = unassigned_propositions_p->front();
    01893                         assert(proposition_p->get_truth_value() == ISATProposition::UNKNOWNVAL);
    01894                         assign_proposition_truth_value(proposition_p, true);
    01895                         propagate_using_DPLL();
    01896                         if (!inconsistent_clauses_p->is_empty())
    01897                         {
    01898                                 assign_proposition_truth_value(proposition_p, false);
    01899                                 propagate_using_DPLL();
    01900                         }
    01901                 }
    01902         }
    01903 }
    01904 */