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

- Alphabetical List
- Class List
- Class Hierarchy
- Class Members

# Mers::Solvers::SAT::ISAT::ISATTheory Class Reference

`#include <ISATTheory.h>`

Inheritance diagram for Mers::Solvers::SAT::ISAT::ISATTheory:

[legend]
Collaboration diagram for Mers::Solvers::SAT::ISAT::ISATTheory:

[legend]
List of all members.

## Public Types
enum | ConsistencyType { CONSISTENT, INCONSISTENT, INDETERMINATE, CONSISTENT, INCONSISTENT, INDETERMINATE }
## Public Member Functions
| ISATTheory ()
| ISATTheory (ISATTheory const &other)
virtual | ~ISATTheory ()
ConsistencyType | get_consistency (bool use_DPLL)
ISATClausesSet const * | get_SAT_conflicts_p (bool use_DPLL)
ISATClausesSet const * | get_SAT_conflicts_p_using_fact (bool use_DPLL, ISATClauses *clauses_p=NULL)
ISATClausesSet const * | get_UNSAT_conflicts_p (bool use_DPLL)
ISATClausesSet const * | get_UNSAT_conflicts_p_using_fact (bool use_DPLL, ISATClauses *clauses_p=NULL)
ConsistencyType | get_current_consistency () const
ISATClause * | insert_new_empty_clause ()
void | add_literal_to_new_clause (ISATPropositionDescription *description_p, ISATLiteral::PolarityType polarity)
void | remove_clause (ISATClause *clause_p)
void | activate_clause (ISATClause *clause_p)
void | deactivate_clause (ISATClause *clause_p)
ISATPropositionDB const * | get_propositions_p () const
ISATInconsistentClauses const * | get_inconsistent_clauses_p () const
ISATUnassignedPropositions const * | get_unassigned_propositions_p () const
void | propagate_clauses (bool use_DPLL)
void | propagate_using_DPLL ()
void | clear_DPLL_search ()
void | propagate_unit_clauses (ISATUnitClauses *unit_clauses_p=NULL)
## Public Attributes
double | assign_proposition_count
double | unassign_proposition_count
double | total_time
## Protected Member Functions
ISATClauses const * | get_supporting_clauses_p (ISATProposition *proposition_p) const
ISATClauses const * | get_supporting_clauses_p (ISATClause *clause_p) const
void | propagate_unit_clause (ISATClause *clause_p)
void | unpropagate_clause (ISATClause *clause_p)
ISATUnitClauses * | assign_proposition_truth_value (ISATProposition *proposition_p, bool truth_value)
ISATUnitClauses * | assign_proposition_true (ISATProposition *proposition_p)
ISATUnitClauses * | assign_proposition_false (ISATProposition *proposition_p)
void | unassign_proposition (ISATProposition *proposition_p)
## Protected Attributes
ISATClauseDB * | clause_database_p
ISATClause * | new_clause_p
ISATPropositions * | searched_propositions_p
long int | searched_path_length
ISATUnassignedPropositions * | unassigned_propositions_p
ISATUnitClauses * | unit_clauses_p
ISATInconsistentClauses * | inconsistent_clauses_p
ISATClausesSet * | SAT_conflicts_p
ISATClausesSet * | UNSAT_conflicts_p
## Friends
std::ostream & | operator<< (std::ostream &stream, ISATTheory const &theory)
std::ostream & | operator<< (std::ostream &stream, ISATTheory::ConsistencyType const &theory_consistency)

## Detailed Description

Author:
  Seung H. Chung

Definition at line 58 of file ISATTheory.h.

## Member Function Documentation

ISATClausesSet const * ISATTheory::get_UNSAT_conflicts_p | ( | bool | use_DPLL | ) |

Definition at line 1613 of file ISATTheory.cpp.

References clause_database_p, Mers::Solvers::SAT::ISAT::ISATClausesSet::clear(), get_consistency(), Mers::Solvers::SAT::ISAT::ISATPropositionDB::get_proposition_p(), get_supporting_clauses_p(), inconsistent_clauses_p, Mers::Solvers::SAT::ISAT::ISATClauses::is_empty(), Mers::Solvers::SAT::ISAT::ISATInconsistentClauses::is_empty(), Mers::Solvers::SAT::ISAT::ISATClausesSet::is_empty(), Mers::Solvers::SAT::ISAT::ISATProposition::is_marked(), Mers::Solvers::SAT::ISAT::ISATPropositionDB::unmark_all_propositions(), and UNSAT_conflicts_p.

Referenced by Mers::Solvers::SAT::ISAT::ISAT::get_UNSAT_conflicts_p(), and get_UNSAT_conflicts_p_using_fact().

Here is the call graph for this function:

The documentation for this class was generated from the following files:

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