Main Page | Namespace List | Class Hierarchy | Alphabetical List | Class List | File List | Class Members | File Members

con_type Class Reference

#include <constraint.hpp>

List of all members.

Public Member Functions

 con_type (bool val=true)
 con_type (const std::string &var)
con_type operator & (const con_type &rhs) const
con_type operator| (const con_type &rhs) const
con_type operator^ (const con_type &rhs) const
con_type operator! () const
bool is_false () const
bool is_true () const
void project (const std::set< std::string > &to_keep)
std::set< std::string > get_cvars ()

Private Attributes

bdd constraint
std::set< std::string > cvars

Friends

class conaux
std::ostream & operator<< (std::ostream &os, const con_type &con)


Detailed Description

This is our constraint type. It uses BDDs from the BuDDy library internally. All methods in this class needs to be defined for any constraint type to be used in the program.


Constructor & Destructor Documentation

con_type::con_type bool  val = true  ) 
 

Creates a constraint representing the inclusion of every solution (true, default) or the exclusion of every solution (false).

Parameters:
val the value denoting which extreme constraint to model.

con_type::con_type const std::string &  var  ) 
 

Creates a constraint representing a variable (will be created if it doesn't exist). The solutions to this constraint will be those where the variable is solved.

Parameters:
var the name of the variable to model.


Member Function Documentation

std::set< std::string > con_type::get_cvars  ) 
 

Gets the names of the constraint variables used by this constraint.

Returns:
The set of variable names.

bool con_type::is_false  )  const
 

Returns true if this constraint has no solutions, false otherwise.

Returns:
Truth value.

bool con_type::is_true  )  const
 

Returns false if this constraint has no solutions, true otherwise.

Returns:
Truth value.

con_type con_type::operator & const con_type rhs  )  const
 

Returns the conjunction of two constraints. The solutions of the returned constraint will be the intersection of the solutions to both constraints.

Parameters:
rhs the constraint on the right hand side of the expression.
Returns:
The conjuncted constraint.

con_type con_type::operator!  )  const
 

Returns the complement of a constraint. The solutions of the returned constraint will be those not solving the given constraint.

Returns:
The complement constraint.

con_type con_type::operator^ const con_type rhs  )  const
 

Returns the symmetric difference of two constraints. The solutions of the returned constraint will be the solutions in one of the constraints, but not both.

Parameters:
rhs the constraint on the right hand side of the expression.
Returns:
The XOR:ed constraint.

con_type con_type::operator| const con_type rhs  )  const
 

Returns the disjunction of two constraints. The solutions of the returned constraint will be the union of the solutions to both constraints.

Parameters:
rhs the constraint on the right hand side of the expression.
Returns:
The disjuncted constraint.

void con_type::project const std::set< std::string > &  to_keep  ) 
 

Projects this constraint onto the given variables.

Parameters:
to_keep the set of names of variables to keep.


Friends And Related Function Documentation

friend class conaux [friend]
 

std::ostream& operator<< std::ostream &  os,
const con_type con
[friend]
 

Write a text representation of this constraint to an ostream.

Parameters:
os the ostream to write to.
con the constraint to write.


Member Data Documentation

bdd con_type::constraint [private]
 

The internal BDD of this constraint.

std::set<std::string> con_type::cvars [private]
 

The names of the variables used in this constraint.


The documentation for this class was generated from the following files:
Generated on Mon Mar 21 00:08:23 2005 for Fixpoint Engine by  doxygen 1.3.9.1