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

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

# Mers::Solvers::SAT::AssignmentTesterInterface Class Reference

`#include <AssignmentTesterInterface.h>`

Inheritance diagram for Mers::Solvers::SAT::AssignmentTesterInterface:

[legend]
List of all members.

## Public Types
enum | SolutionType { Unsatisfiable, Satisfiable, Valid, Unsatisfiable, Satisfiable, Valid, Unknown }
## Public Member Functions
| AssignmentTesterInterface ()
virtual | ~AssignmentTesterInterface ()
virtual void | addConstraint (Mers::Models::Base::BaseModelClause const *constraint)=0
virtual void | addTemporaryConstraint (Mers::Models::Base::BaseModelClause const *constraint)=0
virtual void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *constraint)=0
virtual void | clearTemporaryConstraint ()=0
virtual SolutionType | tryAssignment (Mers::Models::Base::BaseModelAssignmentArray const *candidate, int group, bool satisfy, Mers::Models::Base::BaseModelAssignmentArray &conflict)=0
virtual void | printStatistics (bool verbose=false) const =0
virtual double | getNumberOfSteps () const=0
virtual void | setDebug (unsigned int state)
## Protected Attributes
unsigned int | debug

## Detailed Description

An interface object for a verifier component to the SAT process. The generator generates possible solutions for this tester to test against the model. The tester determines if the solution is either Valid (all solutions are valid), Satisfiable (at least one solution exists, but not all extensions are valid), or Unsatisfiable (no solution exists).

Author:
  Paul H. Elliott

Definition at line 44 of file AssignmentTesterInterface.h.

## Member Enumeration Documentation

enum Mers::Solvers::SAT::AssignmentTesterInterface::SolutionType

An assignment tester generates one of three answers when trying an assignment.

Definition at line 49 of file AssignmentTesterInterface.h.

## Member Function Documentation

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[pure 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.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::addConstraint(), and Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::addConstraint().

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::addTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[pure 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.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::addTemporaryConstraint().

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::setTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[pure 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.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::setTemporaryConstraint(), Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::setTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::setTemporaryConstraint().

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::clearTemporaryConstraint | ( |  | ) | `[pure virtual]`

Clears all previously set temporary constraints.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::clearTemporaryConstraint(), Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::clearTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::clearTemporaryConstraint().

virtual SolutionType Mers::Solvers::SAT::AssignmentTesterInterface::tryAssignment | ( | Mers::Models::Base::BaseModelAssignmentArray const * | candidate,
|  | int | group,
|  | bool | satisfy,
|  | Mers::Models::Base::BaseModelAssignmentArray & | conflict |
| ) |  |  | `[pure 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.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::GATSAT::findSatisfyingSolution(), Mers::Solvers::SAT::GATSAT::GATSAT::findUnsatisfyingSolution(), Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::testTheory(), and Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::testTheory().

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::printStatistics | ( | bool | verbose = `false` | ) | const`[pure 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.

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Referenced by Mers::Solvers::SAT::GATSAT::GATSAT::printStatistics().

virtual double Mers::Solvers::SAT::AssignmentTesterInterface::getNumberOfSteps | ( |  | ) | const`[pure virtual]`

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

Implemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

virtual void Mers::Solvers::SAT::AssignmentTesterInterface::setDebug | ( | unsigned int | state | ) | `[inline, virtual]`

Sets the debug state of this tester.

Parameters:

  | state | the new debug state of the tester.

Reimplemented in Mers::Solvers::SAT::ISAT::ISATTester, and Mers::Solvers::SAT::ValidSAT::ValidSAT.

Definition at line 153 of file AssignmentTesterInterface.h.

References debug.

Referenced by Mers::Solvers::SAT::ValidSAT::ValidSAT::setDebug(), and Mers::Solvers::SAT::GATSAT::GATSAT::setDebug().

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

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