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

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

# Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester Class Reference

`#include <GatsatTester.h>`

Inheritance diagram for Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester:

[legend]
Collaboration diagram for Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester:

[legend]
List of all members.

## Public Member Functions
| GatsatTester ()
virtual | ~GatsatTester ()
## Protected Member Functions
template<int n>
void | initGATSAT (unsigned int numDomains, const struct BMDomainEntry *domains, unsigned int numVariables, const struct BMVariableEntry *variables, unsigned int numSearchVariables, const unsigned int *searchVariables, unsigned int numClauses, const int clauseData[][n], const Mers::Solvers::SAT::GATSAT::GatsatFactory &factory) throw ()
void | getSearchVarData (unsigned int numVariables, const unsigned int *sVarData, Mers::Models::Base::BaseModelVariableArray &allVars, Mers::Models::Base::BaseModelVariableArray &searchVars)
template<int n, int v>
void | testGATSAT (unsigned int numberOfIClauses, const int initialClauseData[][n], unsigned int numberOfResults, const unsigned int expectedResultsData[][v], bool sat, bool verifyTermination=true)
## Protected Attributes
Mers::Solvers::SAT::GATSAT::GATSAT * | m_GAT
| The SAT engine for this set of unit tests.
Mers::Models::Base::BaseModelVariableArray | m_Variables
Mers::Models::Base::BaseModelVariableArray | m_SearchVariables
Mers::Models::Base::BaseModelDomainArray | m_Domains
Mers::Models::Base::BaseModelSentence | m_Theory

## Detailed Description

This class defines the basic structure needed to setup a generator and tester pair as well as a set of routines to test the pair with a minimum amount of work to add test cases.

Author:
  Paul Elliott

Definition at line 38 of file GatsatTester.h.

## Constructor & Destructor Documentation

GatsatTester::GatsatTester | ( |  | ) |

Creates a new tester.

Definition at line 20 of file GatsatTester.cpp.

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

Destroys this tester.

Definition at line 28 of file GatsatTester.cpp.

References m_GAT.

## Member Function Documentation

template<int n>

void Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::initGATSAT | ( | unsigned int | numDomains,
|  | const struct BMDomainEntry * | domains,
|  | unsigned int | numVariables,
|  | const struct BMVariableEntry * | variables,
|  | unsigned int | numSearchVariables,
|  | const unsigned int * | searchVariables,
|  | unsigned int | numClauses,
|  | const int | clauseData[][n],
|  | const Mers::Solvers::SAT::GATSAT::GatsatFactory & | factory |
| ) |  |  | throw ()`[inline, protected]`

Initializes the engine with a new GATSAT engine suitable for testing.

Parameters:

  | numDomains |

Definition at line 59 of file GatsatTester.h.

References getSearchVarData(), tut::BMHelper::loadClauses(), tut::BMHelper::loadDomainData(), tut::BMHelper::loadVariableData(), m_Domains, m_GAT, m_SearchVariables, m_Theory, and m_Variables.

Referenced by Mers::Solvers::SAT::GATSAT::unit_tests::c_TestNamespace::UniformUnsat1Data::UniformUnsat1Data().

Here is the call graph for this function:

void Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::getSearchVarData | ( | unsigned int | numVariables,
|  | const unsigned int * | sVarData,
|  | Mers::Models::Base::BaseModelVariableArray & | allVars,
|  | Mers::Models::Base::BaseModelVariableArray & | searchVars |
| ) |  |  | `[inline, protected]`

Loads a subset of the variables based on a set of indices into the list of all variables.

Parameters:

  | numSubsetVars | The number of variables that are present in the subsetVarData list.
  | subsetVarData | The set of indices into the list of all variables that should be copied to the subset variable list.
  | allVars | The set of all variables that can be used in the subset. Note that the data in subsetVarData is an index into this array, as opposed to a set of UIDs. They will only be the same if the set of allVars is ordered from 0.
  | subsetVars | The variables matching the subsetVarData will be loaded into this list.

Definition at line 107 of file GatsatTester.h.

References tut::BMHelper::getVariableSubset().

Referenced by initGATSAT().

Here is the call graph for this function:

template<int n, int v>

void Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::testGATSAT | ( | unsigned int | numberOfIClauses,
|  | const int | initialClauseData[][n],
|  | unsigned int | numberOfResults,
|  | const unsigned int | expectedResultsData[][v],
|  | bool | sat,
|  | bool | verifyTermination = `true` |
| ) |  |  | `[inline, protected]`

This function runs GATSAT with the specified initial temporary clauses and compares the answers returned against the expected output.

Parameters:

  | numberOfIClauses | The number of initial clauses present.
  | initialClauseData | The list of initial conflicts, inserted immediately. The list is organized in BM variable order and has a single value index for each variable. A value of ((unsigned int)-1) indicates that this variable is not included in the list.
  | numberOfResults | The number of results expected. This should be the length of expectedResults, runtimeConflicts, and acceptList.
  | expectedResultsData | The list of expected results, in the order expected. The list is organized in BM variable order and has a single value index for each variable. A value of ((unsigned int)-1) indicates that this variable is not included in the list.
  | sat | True if we should perform SAT. False if we should perform Unsat.
  | verifyTermination | True (default) if this procedure should verify that exactly those results expected are returned and that no further results are available. False if this function is merely testing the first N results and one expects additional results to be available.

Definition at line 146 of file GatsatTester.h.

References Mers::Solvers::SAT::GATSAT::GATSAT::findSatisfyingSolution(), Mers::Solvers::SAT::GATSAT::GATSAT::findUnsatisfyingSolution(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Solvers::SAT::GATSAT::GATSAT::getTester(), tut::BMHelper::loadAssignments(), tut::BMHelper::loadClauses(), m_GAT, m_SearchVariables, m_Variables, Mers::Utils::Containers::DynamicArray::printArray(), and Mers::Utils::Containers::DynamicArray::size().

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/GATSAT/unit-tests/GatsatTester.h
- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/unit-tests/GatsatTester.cpp