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

conaux Class Reference

#include <constraint.hpp>

List of all members.

Static Public Member Functions

void init (const std::string &constraint_settings)
void finalise ()
bdd get_variable (const std::string &name)
std::string get_varname (const int num)
con_type resolve_sat (const class c_term *t)
con_type build_tree (const class c_term *term, std::set< std::string > &cvars)
void allsathandler (char *varset, int size)
void reindex (con_type &con)
con_type relate (const std::string &var1, const std::string &var2)
void report_answer (const con_type &con)
bool subsumes (const con_type &large, const con_type &small)

Static Private Attributes

int max_var_amount
std::map< std::string, bdd > varmap
std::vector< std::string > varnames


Detailed Description

This class holds static methods for manipulation constraints. Some knowledge of the internal representation of the constraint class is used.


Member Function Documentation

void conaux::allsathandler char *  varset,
int  size
[static]
 

The function used for printing the solutions to a constraint. Used by BuDDy.

Parameters:
varset array of assigned values to the variables in a particular solution.
size the number of variables (size of varset)

con_type conaux::build_tree const class c_term term,
std::set< std::string > &  cvars
[static]
 

Resolves a subtree of a sat-expression (from the program input).

Parameters:
term the subtree of the sat-expression (from the program input).
cvars the set of variables containing the variable names traversed so far.
Returns:
The resolved subexpression.

void conaux::finalise  )  [static]
 

Finalise the constraint-related functionality. This method should be called to clean up the constraint biproducts.

bdd conaux::get_variable const std::string &  name  )  [static]
 

Gets the variable with the given name. If it does not exist, it is created first.

Parameters:
name the variable name.
Returns:
The variable, in the internal constraint format.

string conaux::get_varname const int  num  )  [static]
 

Gets the name of the variable with a given internal number.

Parameters:
num the number of the variable.
Returns:
The variable name.

void conaux::init const std::string &  constraint_settings  )  [static]
 

Initialise the constraint-related functionality. This method must be called before any constraint activity takes place.

void conaux::reindex con_type con  )  [static]
 

Reindexes the variables in the given constraint with the current global variable index. This will change the variable names to include a suffix of "#<index>" and change the underlying variables themselves accordingly.

Parameters:
con the constraint to reindex.

con_type conaux::relate const std::string &  var1,
const std::string &  var2
[static]
 

Returns a biimplication between the given variables, effectively making them equal.

Parameters:
var1 the first variable name.
var2 the second variable name.
Returns:
The constraint representing "<var1> <-> <var2>".

void conaux::report_answer const con_type con  )  [static]
 

Report (all) the solutions of the given constraint to stdout.

Parameters:
con the constraint to report solutions to.

con_type conaux::resolve_sat const class c_term t  )  [static]
 

Resolves the constraint denoted by a sat-expression (from the program input).

Parameters:
t the tree of the sat-expression.
Returns:
The resolved constraint.

bool conaux::subsumes const con_type large,
const con_type small
[static]
 

Determine if the solutions of one constraint is a subset of the solutions to another constraint.

Parameters:
large the constraint expected to subsume the other.
small the constraint expected to have its solutions as a subset of the other's.
Returns:
Truth value denoting whether the solutions of the second constraint is a subset of the solutions to the first.


Member Data Documentation

int conaux::max_var_amount [static, private]
 

The number of variables allocated.

map< string, bdd > conaux::varmap [static, private]
 

The mapping from variable name to variable.

vector< string > conaux::varnames [static, private]
 

The names of the variables, in order of creation.


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