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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISAT.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:                        ISAT.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 "ISAT.h"
    00023
    00024 #include <cassert>
    00025 #include <cstdio>
    00026 #include "ISATPropositionDescription.h"
    00027 #include "ISATPropositionDB.h"
    00028 #include "ISATClausesSet.h"
    00029 #include "ISATClause.h"
    00030 #include "ISATInconsistentClauses.h"
    00031
    00033
    00034 using namespace Mers::Solvers::SAT::ISAT;
    00035 using std::ostream;
    00036 using std::endl;
    00037
    00039 // Public Constructors, Copy Constructors, & Destructors
    00041
    00042 ISAT::ISAT()
    00043 {
    00044 }
    00045
    00046 ISAT::~ISAT()
    00047 {
    00048 }
    00049
    00050 //----------------------------------------------------------------------------------------
    00051 // Public Function Members
    00052 //----------------------------------------------------------------------------------------
    00053 ISATClause *
    00054 ISAT::insert_new_empty_clause()
    00055 {
    00056         return theory.insert_new_empty_clause();
    00057 }
    00058
    00059 void
    00060 ISAT::add_literal_to_new_clause(ISATPropositionDescription *description_p,
    00061                                                                 ISATLiteral::PolarityType polarity)
    00062 {
    00063         theory.add_literal_to_new_clause(description_p, polarity);
    00064         return;
    00065 }
    00066 void
    00067 ISAT::remove_clause(ISATClause *clause_p)
    00068 {
    00069         theory.remove_clause(clause_p);
    00070         return;
    00071 }
    00072
    00073 void
    00074 ISAT::activate_clause(ISATClause *clause_p)
    00075 {
    00076         theory.activate_clause(clause_p);
    00077         return;
    00078 }
    00079
    00080 void
    00081 ISAT::deactivate_clause(ISATClause *clause_p)
    00082 {
    00083         theory.deactivate_clause(clause_p);
    00084         return;
    00085 }
    00086
    00087 //ITMS ->
    00088 void
    00089 ISAT::propagate_clauses(bool use_DPLL)
    00090 {
    00091         theory.propagate_clauses(use_DPLL);
    00092         return;
    00093 }
    00094 //<- ITMS
    00095
    00096 ISATPropositionDB const *
    00097 ISAT::get_propositions_p() const
    00098 {
    00099         return theory.get_propositions_p();
    00100 }
    00101
    00102 ISATTheory::ConsistencyType
    00103 ISAT::get_consistency(bool use_DPLL)
    00104 {
    00105         return theory.get_consistency(use_DPLL);
    00106 }
    00107
    00108 ISATClausesSet const *
    00109 ISAT::get_SAT_conflicts_p(bool use_DPLL)
    00110 {
    00111         return theory.get_SAT_conflicts_p(use_DPLL);
    00112 }
    00113
    00114 ISATClausesSet const *
    00115 ISAT::get_SAT_conflicts_p_using_fact(bool use_DPLL, ISATClauses *clauses_p)
    00116 {
    00117         return theory.get_SAT_conflicts_p_using_fact(use_DPLL, clauses_p);
    00118 }
    00119
    00120 ISATClausesSet const *
    00121 ISAT::get_UNSAT_conflicts_p(bool use_DPLL)
    00122 {
    00123         return theory.get_UNSAT_conflicts_p(use_DPLL);
    00124 }
    00125
    00126 ISATClausesSet const *
    00127 ISAT::get_UNSAT_conflicts_p_using_fact(bool use_DPLL, ISATClauses *clauses_p)
    00128 {
    00129         return theory.get_UNSAT_conflicts_p_using_fact(use_DPLL, clauses_p);
    00130 }
    00131
    00132 ISATInconsistentClauses const *
    00133 ISAT::get_inconsistent_clauses_p() const
    00134 {
    00135         return theory.get_inconsistent_clauses_p();
    00136 }
    00137
    00138 //ITMS ->
    00139 double
    00140 ISAT::get_assign_proposition_counter() const
    00141 {
    00142         return theory.assign_proposition_count;
    00143 }
    00144
    00145 double
    00146 ISAT::get_unassign_proposition_counter() const
    00147 {
    00148         return theory.unassign_proposition_count;
    00149 }
    00150
    00151 void
    00152 ISAT::reset_time_and_counters()
    00153 {
    00154         theory.assign_proposition_count = 0;
    00155         theory.unassign_proposition_count = 0;
    00156         theory.total_time = 0;
    00157
    00158         return;
    00159 }
    00160
    00161 double
    00162 ISAT::get_total_time() const
    00163 {
    00164         return theory.total_time;
    00165 }
    00166 //<- ITMS
    00167
    00168 #if defined _DEBUG
    00169 void
    00170 ISAT::set_debug_level(int debug_level_numb)
    00171 {
    00172         theory.set_debug_level(debug_level_numb);
    00173         return;
    00174 }
    00175 #endif // #if defined _DEBUG
    00176
    00177 //----------------------------------------------------------------------------------------
    00178 // Public Operators
    00179 //----------------------------------------------------------------------------------------
    00180
    00181
    00182 namespace Mers {
    00183         namespace Solvers {
    00184                 namespace SAT {
    00185                         namespace ISAT {
    00186
    00187                                 ostream &
    00188                                 operator <<(ostream &stream, ISAT const &SAT_engine)
    00189                                 {
    00190                                         stream << SAT_engine.theory << endl;;
    00191                                         return stream;
    00192                                 }
    00193                         }
    00194                 }
    00195         }
    00196 }