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

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

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

`#include <ISAT.h>`

Collaboration diagram for Mers::Solvers::SAT::ISAT::ISAT:

[legend]
List of all members.

## Public Member Functions
| ISAT ()
virtual | ~ISAT ()
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)
void | propagate_clauses (bool use_DPLL)
ISATPropositionDB const * | get_propositions_p () const
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)
ISATInconsistentClauses const * | get_inconsistent_clauses_p () const
void | reset_time_and_counters ()
double | get_assign_proposition_counter () const
double | get_unassign_proposition_counter () const
double | get_total_time () const
## Friends
std::ostream & | operator<< (std::ostream &stream, ISAT const &SAT_engine)

## Detailed Description

Author:
  Seung H. Chung

Definition at line 48 of file ISAT.h.

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

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