using DecisionDiagrams;

// create a manager that uses traditional binary decision diagrams.
// alternatively use `new DDManager<CBDDNode>()` for the chain-reduced variant.
var manager = new DDManager<BDDNode>();

// allocate three variables, two booleans and one 32-bit integer
// the internal ordering will match the order allocated from the manager.
var a = manager.CreateBool();
var b = manager.CreateBool();
var c = manager.CreateInt32();

// take the logical or of two variables.
// the Id() method returns the identity DD for the variable.
DD f1 = manager.Or(a.Id(), b.Id());

// create a DD representing whether 1 <= c <= 4 and c != 1.
// a bitvector represents a set of integers by using one DD per bit in the integer.
DD f2 = manager.GreaterOrEqual(c.ToBitvector(), manager.CreateBitvector(1));
DD f3 = manager.LessOrEqual(c.ToBitvector(), manager.CreateBitvector(4));
DD f4 = manager.And(f1, manager.And(f2, f3));

// get a satisfying assignment for a formula.
// will be null if no assignment exists.
var assignment = manager.Sat(f4);

// get the values back as C# objects
bool valuea = assignment.Get(a);  // valuea = false
bool valueb = assignment.Get(b);  // valueb = true
int valuec = assignment.Get(c);   // valuec = 1

var a = manager.CreateBool();
var b = manager.CreateBool();
var c = manager.CreateBool();

DD f1 = manager.And(a.Id(), b.Id());         // a and b
DD f2 = manager.Or(a.Id(), b.Id());          // a or b
DD f3 = manager.Not(a.Id());                 // not a
DD f4 = manager.Implies(a.Id(), b.Id());     // a implies b
DD f5 = manager.Iff(a.Id(), b.Id());         // a == b
DD f6 = manager.Ite(a.Id(), b.Id(), c.Id()); // If a then b else c.

var a = manager.CreateBool();
var b = manager.CreateBool();
var c = manager.CreateBool();

// a and b and c
DD f1 = manager.And(a.Id(), manager.And(b.Id(), c.Id()));
// existential quantification. result = c
DD f2 = manager.Exists(f1, manager.CreateVariableSet(a, b));
// replace a with c. result = b and c
DD f3 = manager.Replace(f1, manager.CreateVariableMap(new Dictionary<Variable<BDDNode>, Variable<BDDNode>> { { a, c } }));

// create a single boolean variable.
var g = manager.CreateBool();

// create two 16-bit integer variables with an interleaved variable ordering.
// an interleaved ordering tends to perform the best for integer variables that are
// combined with other variables using arithmetic or comparision operations.
var intvars = manager.CreateInterleavedInt16(2);
var a = intvars[0];
var b = intvars[1];

BitVector<BDDNode> bv1 = manager.And(a.ToBitvector(), b.ToBitvector());         // bitwise and (&)
BitVector<BDDNode> bv2 = manager.Or(a.ToBitvector(), b.ToBitvector());          // bitwise or (|)
BitVector<BDDNode> bv3 = manager.Not(a.ToBitvector());                          // bitwise negation (~)
BitVector<BDDNode> bv4 = manager.Add(a.ToBitvector(), b.ToBitvector());         // addition (+)
BitVector<BDDNode> bv5 = manager.Subtract(a.ToBitvector(), b.ToBitvector());    // subtraction (-)
BitVector<BDDNode> bv6 = manager.Ite(g.Id(), a.ToBitvector(), b.ToBitvector()); // if g then a else b

DD bv7 = manager.Eq(a.ToBitvector(), b.ToBitvector());                          // equality (=)
DD bv8 = manager.Less(a.ToBitvector(), b.ToBitvector());                        // less than (<)
DD bv9 = manager.LessOrEqual(a.ToBitvector(), b.ToBitvector());                 // less than or eq (<=)
DD bv10 = manager.LessOrEqualSigned(a.ToBitvector(), b.ToBitvector());          // less than or eq signed (<=)
DD bv11 = manager.Greater(a.ToBitvector(), b.ToBitvector());                    // greater than (>)
DD bv12 = manager.GreaterOrEqual(a.ToBitvector(), b.ToBitvector());             // greater than or eq (>=)
DD bv13 = manager.GreaterOrEqualSigned(a.ToBitvector(), b.ToBitvector());       // greater than or eq signed (>=)

// create a manager that uses traditional binary decision diagrams.
var manager = new DDManager<BDDNode>();

// the order will be 'a' before 'b'.
var a = manager.CreateBool();
var b = manager.CreateBool();

// all bit variables for 'c' will be after 'a' and 'b'.
// the variables in 'c' will be allocated in order of most significant bits first.
var c = manager.CreateInt64(BitOrder.MSB_FIRST);

// all bit variables for 'd' will be after all variables for 'c'.
// the variables in 'd' will be in order of least significat bits first.
var d = manager.CreateInt64(BitOrder.LSB_FIRST);

// the ith variable in 'e' will be in the (i + 3) % 64 position.
var e = manager.CreateInt64((i) => (i + 3) % 64);

// there will be two integers in 'f', each is a 64 bit integer.
// the bit ordering will alternate between the two variables with the MSB ordering.
// x0, y0, x1, y1, ..., x63, y63
var f = manager.CreateInterleavedInt64(2, BitOrder.MSB_FIRST);
var f0 = f[0];
var f1 = f[1];