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

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

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

`#include <VsatBfig.h>`

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

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

[legend]
List of all members.

## Public Types
typedef Mers::Utils::Containers::DynamicArrayTemplate< Mers::Models::Base::BaseModelSentence const > | GuardArray
## Public Member Functions
| VsatBfig (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, double cutoffCost)
| VsatBfig (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model)
| VsatBfig (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, Mers::Models::Base::BaseModelSentence const &constraintSet, double cutoffCost)
| VsatBfig (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, Mers::Models::Base::BaseModelSentence const &constraintSet)
| VsatBfig (Mers::Models::Base::BaseModelVariableArray const &designVariables, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, double cutoffCost)
| VsatBfig (Mers::Models::Base::BaseModelVariableArray const &designVariables, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet)
| VsatBfig (Mers::Models::Base::BaseModelVariableArray const &variableSet, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelSentence const &constraintSet, double cutoffCost)
| VsatBfig (Mers::Models::Base::BaseModelVariableArray const &variableSet, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelSentence const &constraintSet)
| VsatBfig (Mers::Generators::AssignmentGeneratorInterface *myGenerator, Mers::Models::Base::BaseModelVariableArray const &searchVariables, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet)
| ~VsatBfig ()
void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | constrainByReachability ()
void | constrainByNextState ()
void | clearTemporaryConstraint ()
void | addConstraint (Mers::Models::Base::BaseModelClause const *c)
void | skipExpanding (bool doSkip)
## Protected Member Functions
void | testTheory ()
## Friends
std::ostream & | operator<< (std::ostream &out, VsatBfig const &other)

## Detailed Description

This class represents the toplevel interface to the VsatBfig reasoning engine. This engine uses ValidSAT and BFIG as tester and generator, respectively.

It produces, in best first order, solutions to problems represented as propositional constraints (the theory).

Definition at line 54 of file VsatBfig.h.

## Constructor & Destructor Documentation

VsatBfig::VsatBfig | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | double | cutoffCost |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with VsatBfig. VsatBfig will extract the constraints and the probability model from this model and use them to create ValidSAT and BFIG.

Definition at line 55 of file VsatBfig.cpp.

References Mers::Models::CCA::CCAModel::get_all_constraints(), Mers::Models::CCA::CCAModel::get_variables_p(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

VsatBfig::VsatBfig | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with VsatBfig. VsatBfig will extract the constraints and the probability model from this model and use them to create ValidSAT and BFIG.

Definition at line 70 of file VsatBfig.cpp.

References Mers::Models::CCA::CCAModel::get_all_constraints(), Mers::Models::CCA::CCAModel::get_variables_p(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

VsatBfig::VsatBfig | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | double | cutoffCost |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with VsatBfig. VsatBfig will extract the probability model from this model and use it to create BFIG.
  | constraintSet | The set of constraints to use with ValidSAT.
  | cutoffCost | The cost above which candidates are no longer considered.

Definition at line 85 of file VsatBfig.cpp.

References Mers::Models::CCA::CCAModel::get_variables_p(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

VsatBfig::VsatBfig | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with VsatBfig. VsatBfig will extract the probability model from this model and use it to create BFIG.
  | constraintSet | The set of constraints to use with ValidSAT.

Definition at line 101 of file VsatBfig.cpp.

References Mers::Models::CCA::CCAModel::get_variables_p(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::VsatBfig | ( | Mers::Models::Base::BaseModelVariableArray const & | designVariables,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | double | cutoffCost |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | cutoffCost | The cost above which candidates are no longer considered.

Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::VsatBfig | ( | Mers::Models::Base::BaseModelVariableArray const & | designVariables,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::VsatBfig | ( | Mers::Models::Base::BaseModelVariableArray const & | variableSet,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | double | cutoffCost |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

Parameters:

  | cutoffCost | The cost above which candidates are no longer considered.

Mers::Solvers::SAT::GATSAT::VsatBfig::VsatBfig::VsatBfig | ( | Mers::Models::Base::BaseModelVariableArray const & | variableSet,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Creates a new VsatBfig object using the ValidSAT and BFIG components.

VsatBfig::VsatBfig | ( | Mers::Generators::AssignmentGeneratorInterface * | myGenerator,
|  | Mers::Models::Base::BaseModelVariableArray const & | searchVariables,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Creates an new VsatBfig object using ValidSAT and the supplied generator.

Parameters:

  | myGenerator | the assignment generator to be used by this VsatBfig engine.
  | searchVariables | the set of all variables in the model that are being searched over.
  | allVariables | the set of all variables in the model and constraint set.
  | constraintSet | the set of all SAT constraints that describe the system.

Definition at line 191 of file VsatBfig.cpp.

References Mers::Solvers::SAT::SATInterface::debug, Mers::Solvers::SAT::GATSAT::GATSAT::generator, and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

## Member Function Documentation

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

This method is used to specify the current temporary constraint. Temporary constraints are those which are not expected to persist throughout the life of the engine. For example, an anti-goal may be asserted as a temporary constraint.

Caution should be exercised when modifying temporary constraints, as doing so may disrupt the support tree for other clauses or other cached data. This in turn may lead to inefficiency.

Parameters:

  | c | The temporary constraint to set.

Definition at line 223 of file VsatBfig.cpp.

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

Here is the call graph for this function:

void VsatBfig::constrainByReachability | ( |  | ) |

Calling this method causes the engine to produce temporary constraints prohibiting assigments that are not reachable from the current state.

In this context, I believe "reachable" really refers to "reachable via an explicit command". In other words, fault transitions or transitions whose guard clause contains observations would technically not be reachable.

WARNING: This method should not be called twice in succession, as it will introduce redundant constraints.

Definition at line 242 of file VsatBfig.cpp.

void VsatBfig::constrainByNextState | ( |  | ) |

This method is a direct pass through to ValidSAT::constrainByNextValue(). It is used to specify the value of a variable in the "next" state (e.g. for observations, whose "next" value is known).

Definition at line 250 of file VsatBfig.cpp.

void VsatBfig::clearTemporaryConstraint | ( |  | ) |

Invoking this method clears/removes the temporary constraint. See the comment for setTemporaryConstraint() with regard to efficiency.

Definition at line 258 of file VsatBfig.cpp.

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

Here is the call graph for this function:

void VsatBfig::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) |

Inserts a new (non-temporary) constraint into the theory. A wrapper around ValidSAT::addConstraint().

Parameters:

  | c | The constraint to add

Definition at line 232 of file VsatBfig.cpp.

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

Here is the call graph for this function:

void VsatBfig::testTheory | ( |  | ) | `[protected]`

Tests the theory to see if it's consistent.

Definition at line 265 of file VsatBfig.cpp.

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

Here is the call graph for this function:

## Friends And Related Function Documentation

std::ostream& operator<< | ( | std::ostream & | out,
|  | VsatBfig const & | other |
| ) |  |  | `[friend]`

Prints out the current state of VsatBfig.

Parameters:

  | out | the ostream being written to.
  | other | The VsatBfig being printed.

Returns:
  the out ostream.

Definition at line 289 of file VsatBfig.cpp.

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

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