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

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

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

`#include <ISATTester.h>`

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

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

[legend]
List of all members.

## Public Member Functions
| ISATTester (Mers::Models::Base::BaseModelVariableArray const &variableSet, Mers::Models::Base::BaseModelVariableArray const &searchVariableSet, Mers::Models::Base::BaseModelSentence const &constraintSet)
virtual | ~ISATTester ()
virtual SolutionType | tryAssignment (Mers::Models::Base::BaseModelAssignmentArray const *candidate, int group, bool satisfy, Mers::Models::Base::BaseModelAssignmentArray &conflict)
virtual void | printStatistics (bool verbose=false) const
virtual void | setDebug (unsigned int state)
void | setDPLLFlag (bool dpll_flag)
void | filterSearchVariables (bool filterFlag)
void | suppressWarnings (bool off=true)
void | addConstraint (Mers::Models::Base::BaseModelClause const *c)
void | addTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | clearTemporaryConstraint ()
void | constrainByReachability ()
void | constrainByNextValue ()
void | addDomainConstraints ()
virtual double | getNumberOfSteps () const
bool | SAT_consistent (bool useDPLL, bool certain=true)
bool | UNSAT_inconsistent (bool useDPLL, bool certain=true)
bool | consistent (bool satisfy, bool useDPLL)
bool | consistentMaybe (bool satisfy, bool useDPLL)
## Public Attributes
bool | hasTemporary
## Friends
std::ostream & | operator<< (std::ostream &, ISATTester const &)

## Detailed Description

ISATTester is a layer that sits upon ISAT in order to interface as a tester to OPSAT.

Author:
  Seung H. Chung

Definition at line 52 of file ISATTester.h.

## Constructor & Destructor Documentation

ISATTester::ISATTester | ( | Mers::Models::Base::BaseModelVariableArray const & | variableSet,
|  | Mers::Models::Base::BaseModelVariableArray const & | searchVariableSet,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Constructs a tester object for ISAT.

Parameters:

  | variableSet | The set of all variables that are mentioned in the constraintSet.
  | searchVariableSet | The subset of variableSet that are being searched over by a generator algorithm. The conflicts generated by this class will only include the searchVariables.
  | constraintSet | The set of constraints that make of the theory for ISAT.

Definition at line 51 of file ISATTester.cpp.

References addDomainConstraints(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Models::Base::BaseModelClauseArray::pushBack(), and Mers::Models::Base::BaseModelAssignmentArray::pushBack().

Here is the call graph for this function:

ISATTester::~ISATTester | ( |  | ) | `[virtual]`

Destroys this object.

Definition at line 92 of file ISATTester.cpp.

## Member Function Documentation

ISATTester::SolutionType ISATTester::tryAssignment | ( | Mers::Models::Base::BaseModelAssignmentArray const * | candidate,
|  | int | group,
|  | bool | satisfy,
|  | Mers::Models::Base::BaseModelAssignmentArray & | conflict |
| ) |  |  | `[virtual]`

This tests the candidate against the model and determines if the candidate is either Unsatisfiable, Satisfiable, or Valid. The result of this test is returned.

Parameters:

  | candidate | The current candidate being tested against the model.
  | group | The UID of the search group that the candidate belongs to. The group should be 0 by default (It is provided by the Assignment Generator). Note that the tester should have either 1 group or the same number of groups as the generator.
  | satisfy | true if this is a satisfaction query, false if it is an unsatisfaction query. This will only effect the conflict returned.
  | conflict | The conflict generated by this test is returned here.

Returns:
  Valid if all extension of the candidate are valid, Unsatisfiable if no solution exists, or Satisfiable if one solution exists, but not all extensions are valid.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 103 of file ISATTester.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::debug, Mers::Solvers::SAT::ISAT::ISAT::get_SAT_conflicts_p(), Mers::Solvers::SAT::ISAT::ISAT::get_SAT_conflicts_p_using_fact(), Mers::Solvers::SAT::ISAT::ISAT::get_UNSAT_conflicts_p(), Mers::Solvers::SAT::ISAT::ISAT::get_UNSAT_conflicts_p_using_fact(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Solvers::SAT::ISAT::ISATClausesSet::is_empty(), Mers::Utils::Containers::DynamicArray::makeEmpty(), Mers::Utils::Containers::DynamicArray::printArray(), SAT_consistent(), Mers::Utils::Containers::DynamicArray::size(), and UNSAT_inconsistent().

Referenced by Mers::Solvers::Entailment::GI::GoalInterpreter::generateGoalState().

Here is the call graph for this function:

void ISATTester::printStatistics | ( | bool | verbose = `false` | ) | const`[virtual]`

Prints out the performance statistics of the assignment tester.

Parameters:

  | verbose | True if detailed statistics should be printed, otherwise only a summary is printed.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 254 of file ISATTester.cpp.

References Mers::Solvers::SAT::ISAT::ISAT::get_assign_proposition_counter(), Mers::Solvers::SAT::ISAT::ISAT::get_total_time(), and Mers::Solvers::SAT::ISAT::ISAT::get_unassign_proposition_counter().

Here is the call graph for this function:

void ISATTester::setDebug | ( | unsigned int | state | ) | `[virtual]`

Sets the debug state of this generator.

Parameters:

  | state | the new debug state of the generator

Reimplemented from Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 274 of file ISATTester.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::debug.

void ISATTester::setDPLLFlag | ( | bool | dpll_flag | ) |

Sets a flag indicating that DPLL should or should not be used.

Parameters:

  | dpll_flag | true when DPLL should be used when searching, otherwise, only unit propagation is used.

Definition at line 492 of file ISATTester.cpp.

Referenced by Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::Opsat().

void Mers::Solvers::SAT::ISAT::ISATTester::filterSearchVariables | ( | bool | filterFlag | ) | `[inline]`

Turns on or off the search-variables filter.

Parameters:

  | filterFlag | True if we should enable filtering conflicts that include variables other than the search variables or false if all conflicts should be returned (no filter).

Definition at line 155 of file ISATTester.h.

void ISATTester::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) | `[virtual]`

Adds an additional temporary constraint to the current model constraints. This constraint will be included in all tests until clearTemporaryConstraint is called.

Parameters:

  | constraint | the new constraint being added to the model.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 293 of file ISATTester.cpp.

Referenced by addDomainConstraints().

void ISATTester::addTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) | `[virtual]`

Adds an additional temporary constraint to the current model constraints. This constraint will be included in all tests until clearTemporaryConstraint is called.

Parameters:

  | constraint | the new constraint being added to the model.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 302 of file ISATTester.cpp.

References hasTemporary.

Referenced by setTemporaryConstraint().

void ISATTester::setTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) | `[virtual]`

Replaces the current temporary constraint with the new constraint. This involves a call to clearTemporaryConstraint and addTemporaryConstraint.

Parameters:

  | constraint | the new constraint that will now be the only temporary constraint.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 319 of file ISATTester.cpp.

References addTemporaryConstraint(), and clearTemporaryConstraint().

Here is the call graph for this function:

void ISATTester::clearTemporaryConstraint | ( |  | ) | `[virtual]`

Clears all previously set temporary constraints.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 333 of file ISATTester.cpp.

References hasTemporary, and Mers::Solvers::SAT::ISAT::ISAT::remove_clause().

Referenced by setTemporaryConstraint().

Here is the call graph for this function:

double ISATTester::getNumberOfSteps | ( |  | ) | const`[virtual]`

Returns the number of steps taken by this interface towards solving the problem.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 263 of file ISATTester.cpp.

References Mers::Solvers::SAT::ISAT::ISAT::get_assign_proposition_counter(), and Mers::Solvers::SAT::ISAT::ISAT::get_unassign_proposition_counter().

Here is the call graph for this function:

bool ISATTester::SAT_consistent | ( | bool | useDPLL,
|  | bool | certain = `true` |
| ) |  |  |

modifies: this (for efficiency)

effects : Returns true IFF the current Theory is consistent If useDPLL == true, SAT is complete. Otherwise, SAT is incomplete (yet sound).

Definition at line 405 of file ISATTester.cpp.

References Mers::Solvers::SAT::ISAT::ISAT::get_consistency().

Referenced by consistent(), consistentMaybe(), and tryAssignment().

Here is the call graph for this function:

bool ISATTester::UNSAT_inconsistent | ( | bool | useDPLL,
|  | bool | certain = `true` |
| ) |  |  |

modifies: this (for efficiency)

effects : Returns true IFF the current Theory is INconsistent If useDPLL == true, UNSAT is complete. Otherwise, SAT is incomplete (yet sound).

Definition at line 421 of file ISATTester.cpp.

References Mers::Solvers::SAT::ISAT::ISAT::get_consistency().

Referenced by consistent(), consistentMaybe(), and tryAssignment().

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/ISATTester.h
- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATTester.cpp