15#ifndef CPROVER_SOLVERS_BDD_BDD_CUDD_H
16#define CPROVER_SOLVERS_BDD_BDD_CUDD_H
18#include <cplusplus/cuddObj.hh>
32 return Cudd_IsConstant(
node) != 0;
37 return Cudd_IsComplement(
node) != 0;
46 return Cudd_NodeReadIndex(
node);
Manager for BDD creation.
bdd_nodet bdd_node(const bddt &bdd) const
bdd_managert(const bdd_managert &)=delete
bddt bdd_variable(bdd_nodet::indext index)
Low level access to the structure of the BDD, read-only.
indext index() const
Label on the node, corresponds to the index of a Boolean variable.
unsigned int indext
Type of indexes of Boolean variables.
DdNode * idt
Return type for id()
bool is_complement() const
idt id() const
Unique identifier of the node.
bdd_nodet then_branch() const
friend class bdd_managert
bdd_nodet else_branch() const
Logical operations on BDDs.
bool equals(const bddt &other) const
bddt bdd_xor(const bddt &other) const
bddt constrain(const bddt &other)
static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
bddt bdd_or(const bddt &other) const
bddt & operator=(const bddt &other)=default
bddt bdd_and(const bddt &other) const
friend class bdd_managert
output_type narrow_cast(input_type value)
Alias for static_cast intended to be used for numeric casting Rationale: Easier to grep than static_c...