Creates a new context with a newly created Cudd Manager. The context has a
reference count of zero. You should you the reference counting mechanism to
destroy the context.
Creates a new context with the given Cudd Manager. The context has a
reference count of zero. You should you the reference counting mechanism to
destroy the context.
In most situations, reference counting is irrelevant with a
\ref KureContext. Like usual, there are operations to increase and decrease
the counts and if it reaches 0, the object is destroyed. Alternatively, one
can use \ref kure_context_destroy to immediately destroy a context. In such
a situation, if the reference count is greater than one, a warning is
printed on the screen.
Sets the current random number generator or resets it if random_func is
NULL. In the latter case, udata is ignored completely. Otherwise udata is
passed to the random function on each call.
Returns the sum of two relations. The relations arg1 and arg2 need to have
the same number of columns. The result contains arg1 at the top and arg2
below.
Returns the size of the i-th component of the given domain. The parameter
size has to be initialized. Returns TRUE if the size is returned and FALSE
in case of an error, e.g. i is an invalid compoenent of self is NULL.
Same as \ref kure_get_entries, except that the number of entries is returned
as a integer of limited size. If the number of entries is doesn’t fit into
an integer, psuccess is set to FALSE. A(ny) non-negative number is returned
anyway.
Tests if a given line is complete. The line is defined using a single point
(x,y). In contrast to most other functions, the column (here x) is the first
argument and the rows are the second one. The direction is passed as a
\ref KureDirection.
Similar to \ref kure_lang_exec, but stores the result in a global Lua
variable of the given name. If the global variable is non-NULL it is
overwritten. If the call fails, the global Lua variable remains unchanged.
Executes the given expression in the embedded language and returns the
resulting relation. Expressions are built from ‘|’,‘&’,‘[.,.]’,‘(’,‘)’, etc.
and functions calls. Neither assignments nor definitions of other objects
(functions, programs) are allowed. Expressions always return a relation if
successful. Otherwise, NULL is returned and *perr is set if perr is
different from NULL.
Loads a given translation unit written in the embedded language into the
given \ref lua_State which has to be created using \ref kure_lua_new.
Translations units may only contain function and program definitions.
Parses the given translation unit. Each time a function or program is parsed
the corresponding callback function (if non-NULL) is called and provided the
original code as well as the generated Lua code.
Sets the current callback function which is called if an assertion fails.
The function is directly called from within Lua and has to take the
assertions name as first argument.
Returns the left tupling of two relations. The argument rop is set as follows:
\f[
\llbracket arg1,arg2]{(a,b),x} \iff arg1{a,x}\land arg2_{b,x},.
\f]
Is computed using the formula:
\f[
\llbracket R,S] = \pi R \cap \rho S,.
\f]
Creates a cardinality comparison relation of a given size. Let n be the
number of rows of arg. Then it creates a Relation R with \f$2^n\f$ rows and
\f$2^n\f$ columns such that for each pair of vectors v,w with one column
we have \f$(v,w)\in R \iff |v| < |w|\f$.
Creates a new \ref lua_State which can be used with the Kure-Lua binding
and the embedded language afterwards. The returned \ref lua_State has the
following properties:
Sets the current global \ref KureContext. The context is used in operations
where no context is passed explicitly and where it cannot derived from
operands. This is mainly the case in the domain-specific embedded language.
Creates a global Lua variable which points to a copy of the given relation.
In the special case where the given relation has the name $, it is replaced
by __dollar. This is a convention to be compatible with RelView. This also
holds for \ref kure_lua_get_rel and $.
Computes the maximum elements in the vector arg w.r.t. to the is-subset-of
relation. The vector has to represent a down-set for this to work. If this
is not the case or you are unsure, use \ref kure_maxsets instead.
Computes the minimum elements in the vector arg w.r.t. to the is-subset-of
relation. The vector has to represent an up-set for this to work. If this
is not the case or you are unsure, use \ref kure_minsets instead.
Multiplies two relations. The relations have to be compatible in dimension.
That it, cols(arg1)=rows(arg2). The result has a size rows(arg1) x cols(arg2).
Multiplies two relations and transposes the second of them. The relations
have to be compatible in dimension. That it, cols(arg1)=cols(arg2). The
result has a size rows(arg1) x rows(arg2).
Multiplies two relations and transposes the first of them. The relations
have to be compatible in dimension. That it, rows(arg1)=rows(arg2). The
result has a size cols(arg1) x cols(arg2).
Multiplies two relations and transposes both of them. The relations
have to be compatible in dimension. That it, rows(arg1)=cols(arg2). The
result has a size cols(arg1) x rows(arg2).
Returns the number of variables necessary for the given number of rows/cols.
This function is rarely used outside library. If a relation is present, you
should use \ref kure_rel_get_vars_rows and \ref kure_rel_get_vars_cols
instead.
Creates the product order relation, that is,
\f$ \pi\cdot arg1\cdot \pi^{T} \land \rho\cdot arg2\cdot \rho^T \f$ where
\f$\pi,\rho\f$ are the projection relations of arg1 and arg2 respectively.
Creates an arbitrary random relation using the given \ref KureRandomFunc and
the given size. The result has the specified dimension. See \ref kure_random
for details.
Creates an arbitrary random relation using the given \ref KureRandomFunc and
the given size. The result has the specified dimension. Same as
\ref kure_random_full for integer numbers.
Creates a random relation without cycles using the given \ref KureRandomFunc and
the given size. The result has the specified dimension. See
\ref kure_random_no_cycles for details.
Create a random relation without cycles using the given \ref KureRandomFunc
and the given size. The result has the specified dimension. Same as
\ref kure_random_no_cycles_full for integer numbers.
Creates a random relation without cycles using the given \ref KureRandomFunc and
the given size. The result is homogeneous and has the specified dimension.
Creates a random relation without cycles using the given \ref KureRandomFunc and
the given size. The result is homogeneous and has the specified dimension.
Same as \ref kure_random_perm_full for integers numbers.
Creates a random permutation using the random function of the
relation’s \ref KureContext. The result has the same dimension as the
input. The relation has to be homogeneous.
Computes the reflexive hull (closure) of the given argument. That is:
\code
rop := arg | I
\endcode
\param rop The relation to store the result in. Has to be initialized.
\param arg The argument.
\return Returns TRUE on success and FALSE on error.
Returns the BDD node currently in use. The node has to be referenced in
order to be used externally. Use \ref Cudd_Ref to reference it and use
Cudd_RecursiveDeref to dereference it. The \ref DdManager is available
from the context (\ref kure_rel_get_context and
\ref kure_context_get_manager).
Creates a relation from the given string data which must not be NULL. The
relation is created with the given size. Its contents is set w.r.t the
characters in s. The relation is filled line-wise, i.e. the first ‘cols’
relevant characters in s determine the first row of the relation and so on.
Only characters one_ch and zero_ch are relevant. Consequently, all others
are ignored. This allows to use formating characters like spaces and
newlines. Whenever a one_ch character appears in s, the current bit is set
in the relation. All other bits remain unset.
Sets the current BDD node of the given relation. Recursively dereferences
to old BDD node and references the given node. The caller should dereference
the node after this call if it is no longer needed. Use \ref Cudd_Deref if
you now what you do and \ref Cudd_RecursiveDeref or \ref Cudd_IterDerefBdd
otherwise.
Converts the given relation into a string of length rows*cols+rows.
Each row is terminated by a newline (‘\n’). If a bit is set one_ch
is used and zero_ch otherwise.
Returns the right tupling of two relations. The argument rop is set as follows:
\f[
[arg1,arg2\rrbracket_{a,(x,y)} \iff arg1_{a,x}\land arg2_{a,y},.
\f]
Is computed using the formula:
\f[
[R,S\rrbracket = R \pi^t \cap S \rho^t,.
\f]
Sets an error if perr is non-NULL. Does nothing otherwise. A \ref gmp_printf
compatible operation is used to create the message. The fmt argument may be
NULL. In this case the message would be set to “Unknown”.
Filters a sets w.r.t. to a given cardinality contraint. Argument pot has to
be a vector of size \f$2^k\f$. Then \f$rop_{w}\f$ iff \f$vec_{w}\land |w|<rows(vec)\f$.
E.g. if vec has just 1 row, and pot is L, then only \f$\emptyset\f$ is in rop. If
vec is equal to k+1 all elements pass the filter.
Creates the sum order relation, that is,
\f$ \iota^{T}\cdot arg1\cdot \iota \land \kappa^{T}\cdot arg2\cdot \iota \f$ where
\f$\iota,\kappa\f$ are the injections relations of arg1 and arg2 respectively.
Returns the number of entries in a vector. This is different from the number
of entries in a relation if the vector has more than one column. For a
vector an entry is a filled row.
Sets v to the successor of the given argument. If arg is a point and the
i-th row is set than v will be a point with the (i+1)-th row set. If there
is no such row v is set to the empty relation.