#include <constraint.h>
Static Public Member Functions | |
void | init (const string &constraint_settings) |
void | finalise () |
bdd | get_variable (const string &name) |
string | get_varname (const int num) |
con_type | resolve_sat (const struct c_term *t) |
con_type | build_tree (const struct c_term *term, set< string > &cvars) |
void | allsathandler (char *varset, int size) |
void | reindex (con_type &con) |
con_type | relate (const string &var1, const 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 |
map< string, bdd > | varmap |
vector< string > | varnames |
|
The function used for printing the solutions to a constraint. Used by BuDDy.
|
|
Resolves a subtree of a sat-expression (from the program input).
|
|
Finalise the constraint-related functionality. This method should be called to clean up the constraint biproducts. |
|
Gets the variable with the given name. If it does not exist, it is created first.
|
|
Gets the name of the variable with a given internal number.
|
|
Initialise the constraint-related functionality. This method must be called before any constraint activity takes place. |
|
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.
|
|
Returns a biimplication between the given variables, effectively making them equal.
|
|
Report (all) the solutions of the given constraint to stdout.
|
|
Resolves the constraint denoted by a sat-expression (from the program input).
|
|
Determine if the solutions of one constraint is a subset of the solutions to another constraint.
|
|
The number of variables allocated. |
|
The mapping from variable name to variable. |
|
The names of the variables, in order of creation. |