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

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

# Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT Class Reference

`#include <CompileSAT.h>`

Inheritance diagram for Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT:

[legend]
Collaboration diagram for Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT:

[legend]
List of all members.

## Public Member Functions
| CompileSAT (Mers::Models::Base::BaseModelVariableArrayArray const &searchGroups, Mers::Models::Base::BaseModelVariableArray const &decisionVariables, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool testForValid)
| CompileSAT (Mers::Models::Base::BaseModelVariableArray const &decisionVariables, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool testForValid=true)
| CompileSAT (Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool testForValid=true)
| CompileSAT (Mers::Generators::AssignmentGeneratorInterface *myGenerator, Mers::Solvers::SAT::AssignmentTesterInterface *myTester)
| ~CompileSAT ()
void | addTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | clearTemporaryConstraint ()
## Protected Attributes
Mers::Models::Base::BaseModelVariableArray | decisionVars
Mers::Models::Base::BaseModelVariableArray | allVars
Mers::Models::Base::BaseModelSentence | constraints
Mers::Models::Base::BaseModelVariableArrayArray | searchSet
| the set of decision variables being searched over
## Friends
std::ostream & | operator<< (std::ostream &, CompileSAT const &)

## Detailed Description

CompileSAT defines an default SAT engine interface and allows the use of Assignment Testers that can test for Valid.

Definition at line 35 of file CompileSAT.h.

## Constructor & Destructor Documentation

CompileSAT::CompileSAT | ( | Mers::Models::Base::BaseModelVariableArrayArray const & | searchGroups,
|  | Mers::Models::Base::BaseModelVariableArray const & | decisionVariables,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | testForValid |
| ) |  |  |

Creates a new sat engine

Parameters:

  | searchGroups | The set of search groups that should be generated over.
  | decisionVariables | the variables that should be covered by generation. Every variable in searchGroups should be included in decisionVariables.
  | allVariables | all of the variables in the constraintSet and decisionVariables. Note that allVariables may contain extra variables but must minimally contain all of the decisionVariables and all variables used in the constraintSet.
  | constraintSet | the set of all SAT constraints that describe the problem being explored.
  | testForValid | true if we're going to test for valid, false if the sat engine should only test for satisfiability.

Definition at line 39 of file CompileSAT.cpp.

References allVars, constraints, decisionVars, Mers::Solvers::SAT::GATSAT::GATSAT::generator, searchSet, and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

CompileSAT::CompileSAT | ( | Mers::Models::Base::BaseModelVariableArray const & | decisionVariables,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | testForValid = `true` |
| ) |  |  |

Creates a new sat engine.

Parameters:

  | decisionVariables | the variables that should be covered by generation.
  | allVariables | all of the variables in the constraintSet and decisionVariables. Note that allVariables may contain extra variables but must minimally contain all of the decisionVariables and all variables used in the constraintSet.
  | constraintSet | the set of all SAT constraints that describe the problem being explored.
  | testForValid | true if we're going to test for valid, false if the sat engine should only test for satisfiability.

Definition at line 59 of file CompileSAT.cpp.

References allVars, constraints, decisionVars, Mers::Solvers::SAT::GATSAT::GATSAT::generator, Mers::Models::Base::BaseModelVariableArrayArray::pushBack(), searchSet, and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

CompileSAT::CompileSAT | ( | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | testForValid = `true` |
| ) |  |  |

Creates a new sat engine.

Parameters:

  | allVariables | all of the variables in the constraintSet. Note that allVariables may contain extra variables but must minimally contain all variables used in the constraintSet. Also note that all variables will be used as the decision variables.
  | constraintSet | the set of all SAT constraints that describe the problem being explored.
  | testForValid | true if we're going to test for valid, false if the sat engine should only test for satisfiability.

Definition at line 79 of file CompileSAT.cpp.

References allVars, constraints, decisionVars, Mers::Solvers::SAT::GATSAT::GATSAT::generator, Mers::Models::Base::BaseModelVariableArrayArray::pushBack(), searchSet, and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

CompileSAT::CompileSAT | ( | Mers::Generators::AssignmentGeneratorInterface * | myGenerator,
|  | Mers::Solvers::SAT::AssignmentTesterInterface * | myTester |
| ) |  |  |

Creates a new sat engine.

Parameters:

  | myGenerator | the generator that should be used by this engine. This object assumes ownership of the generator and will destroy it upon it's own destruction.
  | myTester | the tester that should be used by this engine. This object assumes ownership of the generator and will destroy it upon it's own destruction.

Definition at line 98 of file CompileSAT.cpp.

CompileSAT::~CompileSAT | ( |  | ) |

Destroys the sat engine

Definition at line 107 of file CompileSAT.cpp.

## Member Function Documentation

void CompileSAT::addTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) |

Adds a temporary constraint to the satisfaction problem.

Parameters:

  | c | the new constraint being added.

Definition at line 113 of file CompileSAT.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::addTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

void CompileSAT::setTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) |

Sets the temporary constraint to the satisfaction problem.

Parameters:

  | c | the new constraint that will replace any old constraints.

Definition at line 120 of file CompileSAT.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::setTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

void CompileSAT::clearTemporaryConstraint | ( |  | ) |

Deletes all temporary constraints that have been added.

Definition at line 127 of file CompileSAT.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::clearTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

## Member Data Documentation

Mers::Models::Base::BaseModelVariableArray Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::decisionVars`[protected]`

the set of all decision variables being used by this engine

Definition at line 172 of file CompileSAT.h.

Referenced by CompileSAT().

Mers::Models::Base::BaseModelVariableArray Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::allVars`[protected]`

the set of all variables being used by this engine

Definition at line 175 of file CompileSAT.h.

Referenced by CompileSAT().

Mers::Models::Base::BaseModelSentence Mers::Solvers::SAT::GATSAT::CompileSAT::CompileSAT::constraints`[protected]`

the sat constraints that this engine is exploring

Definition at line 178 of file CompileSAT.h.

Referenced by CompileSAT().

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

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