Getting started with JINC is easy.

1. Download the package
2. Extract it
3. Modify makefile.common to your needs (usually not needed)
4. Type make
5. Done

To follow the tutorials below, just create a new file in src/bin. It will be automatically compiled and started when typing make. The executable can be found under bin. To compile just the binary without starting, type make bin.

E.g.:

1. Create file src/bin/test.cpp
2. Edit src/bin/test.cpp

    1: #include <iostream>
    2: #include <add/add.hpp>
    3:
    4: int main(){
    5:   std::cout << (ADD::size()) << std::endl;
    6: }

3. Type make bin to compile binary
4. Type bin/test


The example code above doesn't do much. It creates an empty ADD (#include ) and ask for the size (number of nodes). In that case we have not created any node so that the answer is 0.

The last tutorial covered just the basics needed to start using JINC. Now we want to cover the basic usage.
In all our tutorials we will just use ADDs as the OBDD variant. If you want to use another variant, just replace every appearance of ADD with your chosen variant name. To see all provided variants look into src/lib (common is the common library party and does not represent a variant).


Creating variables

There are many ways to create variables.

    1: #include <iostream>
    2: #include <add/addvarorder.hpp> //needed for direct variable manipulation
    3:
    4: int main(){
    5:   std::cout << (ADDVarOrder::size()) << std::endl;
    6:   //prints 0 as there are no variables
    7:
    8:   ADDVarOrder::addVariable("x");
    9:   //creates a variable with name "x"
   10:
   11:   std::cout << (ADDVarOrder::size()) << std::endl;
   12:   //prints 1 as there is one variable
   13:
   14:   std::cout << (ADDVarOrder::getVarOrder()) << std::endl;
   15:   //prints the current variable ordering
   16:   // in this case (x)
   17:
   18:   ADDVarOrder::insertVariable("y",0);
   19:   //creates a variable with name "y" before "x"  
   20:
   21:   std::cout << (ADDVarOrder::getVarOrder()) << std::endl;
   22:   //prints (y,x)
   23: }

The above example showed how to create variables with ADDVarOrder. For more function have a look in src/lib/add/addvarorder.hpp.
The creation of named variables is supported but usually not recommended. Creating and accessing unnamed variables is much faster.

    1: #include <iostream>
    2: #include <add/addvarorder.hpp>
    3:
    4: int main(){
    5:   std::cout << (ADDVarOrder::size()) << std::endl;
    6:   //prints 0 as there are no variables
    7:
    8:   ADDVarOrder::insertVariables(0,100);
    9:   //creates 100 unnamed variables
   10:
   11:   std::cout << (ADDVarOrder::size()) << std::endl;
   12:   //prints 100
   13: }

The example above showed how to create 100 unnamed variables at once.

Removing variables

    1: #include <iostream>
    2: #include <add/addvarorder.hpp>
    3:
    4: int main(){
    5:   ADDVarOrder::insertVariables(0,2);
    6:   //creates 2 unnamed variables
    7:
    8:   std::cout << (ADDVarOrder::size()) << std::endl;
    9:   //prints 2
   10:
   11:   ADDVarOrder::removeVariable(1);
   12:   //remove the second variable
   13:   //counting starts from 0
   14:
   15:   std::cout << (ADDVarOrder::size()) << std::endl;
   16:   //prints 1
   17: }

Note, variable removal is only possible if there are no nodes on this variable level.
It is only possible to remove one variable level at a time.

WARNING

When using JINC with its multi-threading features, variable ordering modifications should only be done at a single threaded execution path. Usually in symbolic calculations variables are inserted at start-time (or while modeling a system) and not removed during run-time. JINC is optimized for this use case.

Reordering should also only be done on the main thread as the reordering algorithms are using multiple threads to speed-up the calculation.

Functions are the basic data structure in JINC. Almost all functionality can be accessed through the function class.

    1: #include <iostream>
    2: #include <add/addvarorder.hpp>
    3: #include <add/addfunction.hpp> //function class
    4:
    5: int main(){
    6:   ADDFunction constantFunction=10.5;
    7:   //creates a constant function with value 10.5
    8:   //... constantFunction=ADDFunction::createConstantFunction(10.5)
    9:   //does the same
   10:
   11:   std::cout << constantFunction.getValue() << std::endl;
   12:   //print 10.5
   13:   //if the function is not constant it prints 0.0
   14:   //to check if a function is constant
   15:   //just call function.isConstant()
   16:
   17:   ADDFunction x=ADDFunction::projection("x",true);
   18:   //creates variable "x" and assigns the positive projection
   19:   //to the function object
   20:   //... x=ADDFunction("x",true) does the same
   21:
   22:   std::cout << (ADDVarOrder::size()) << std::endl;
   23:   //prints 1
   24:
   25:   std::cout << (x==!!x) << std::endl;
   26:   std::cout << ((x&!x)==0.0) << std::endl;
   27:   //operators behave like the should
   28: }

JINC provides a wide range of overloaded operators plus a feature rich API. See src/lib/add/addfunction.hpp for more details.

Functions like cofactor, exists, ... take an ADDFunction as parameter. JINC uses cube sets for these functions. Cube sets are the conjunction of positive or negative projection functions.

    1: #include <iostream>
    2: #include <add/addvarorder.hpp>
    3: #include <add/addfunction.hpp>
    4:
    5: int main(){
    6:   ADDFunction x=ADDFunction::projection("x",true);
    7:   ADDFunction y=ADDFunction::projection("y",true);
    8:
    9:   ADDFunction f=x&!y;
   10:
   11:   std::cout << (f.cofactor(!y)==x) << std::endl;
   12:   //prints 1
   13:
   14:   std::cout << (f.cofactor(x)==!y) << std::endl;
   15:   //prints 1
   16:
   17:   std::cout << (f.cofactor(f)==1.0) << std::endl;
   18:   //prints 1
   19:
   20:   std::cout << (f.cofactor(!f)==1.0) << std::endl;
   21:   //prints 0
   22:   //!f does not make sense as f=x&!y and
   23:   //!f=!x|y which is not a cube set
   24:   //if you want to negate a cube set use
   25:   //function.change()
   26:   //f.change() results in !x&y
   27:   //you could also use change() with a cubeset to change
   28:   //only a subset of assignments
   29: }

    1: #include <iostream>
    2: #include <add/add.hpp>
    3: #include <add/addfunction.hpp>
    4:
    5: int main(){
    6:   ADDFunction x=ADDFunction("x",true);
    7:   ADDFunction y=ADDFunction("y",true);
    8:
    9:   ADDFunction f=x&y;
   10:
   11:   std::cout << (ADD::size()) << std::endl;
   12:   //prints 5 (for 5 nodes)
   13:
   14:   std::cout << (ADD::size()==f.size()) << std::endl;
   15:   //prints 0 as function x contains one node that is
   16:   //not represented in f
   17:
   18:   x=0.0;
   19:   std::cout << (ADD::size()==f.size()) << std::endl;
   20:   //prints 0 as the node is still available (but not reachable)
   21:   //deleting the node immediately would reduce the cache performance
   22:   //ADDFunction("x",true) would not create a new node as it is
   23:   //still available
   24:  
   25:   ADD::garbageCollect();
   26:   //starts multi-threading garbage collection
   27:   //this should only be used in JINC's main thread
   28:
   29:   std::cout << (ADD::size()==f.size()) << std::endl;
   30:   //prints 1 as there are no dead/garbage nodes
   31: }

The garbage collection method has to be used by manually as JINC cannot determine if all computations are done and if it is reasonable to perform a garbage collection.
The concept of a delayed garbage collection is that the cache rebuilds are only done when performing the garbage collection.

The path concept is can be used to iterate over function assignments/paths and also for creating functions. This tutorial will cover the basic usage for JINC's path feature.

    1: #include <iostream>
    2: #include <add/addtraversalhelper.hpp> //to use iterator
    3: #include <add/addfunction.hpp>
    4:
    5: int main(){
    6:   ADDVarOrder::insertVariables(0,2);
    7:   ADDFunction f=ADDFunction::projection(0,false);
    8:   //or whatever you like
    9:
   10:   ADDFunction::iterator it=f.begin();
   11:   while(it!=f.end()){
   12:     std::cout << *it << std::endl;
   13:     ++it;
   14:   }
   15: }

The example above shows the iterator usage when iterating over paths (ways from root to terminal node which is not equal 0)
Iterating over assignments is also easy as the next example shows.

    1: #include <iostream>
    2: #include <add/addtraversalhelper.hpp>
    3: #include <add/addfunction.hpp>
    4: #include <add/addvarorder.hpp>
    5: #include <common/assignment_iterator.hpp>
    6:
    7: int main(){
    8:   ADDVarOrder::insertVariables(0,2);
    9:   ADDFunction f=ADDFunction::projection(0,false);
   10:   //or whatever you like
   11:
   12:   Assignment_Iterator<ADDFunction::iterator> it=f.begin();
   13:   while(it!=f.end()){
   14:     std::cout << *it << std::endl;
   15:     ++it;
   16:   }
   17: }

The path itself can be used to create functions. The path class provides an API for modifying values. Note, the path class depends on the value range of the underlying OBDD variant (the traversal helper covers these details). The next example shows an example how to copy a function with iterators. It is not recommended to do it this way but it illustrates the usage. It is, e.g., possible to skip or alter some values.

    1: #include <iostream>
    2: #include <add/addtraversalhelper.hpp>
    3: #include <add/addfunction.hpp>
    4: #include <add/addvarorder.hpp>
    5:
    6: int main(){
    7:   ADDVarOrder::insertVariables(0,2);
    8:   ADDFunction f=ADDFunction::projection(0,false);
    9:   //or whatever you like
   10:
   11:   ADDFunction copyOfF=0.0;
   12:   ADDFunction::iterator it=f.begin();
   13:   while(it!=f.end()){
   14:     copyOfF+=*it;
   15:     ++it;
   16:   }
   17:   std::cout << (copyOfF==f) << std::endl;
   18:   //prints 1
   19: }

Futures are used to implement concurrent behavior. common/future.hpp provides support for multi-threaded calculations.

The new data-types Helper::Future and Helper::FutureContainer can be used with an appropriate BDD function type.
The constructor takes an function object (which takes zero arguments and returns the corresponding BDD function) as an argument. The Future object starts the calculation
immediately (limited by the number of threads in common/constants.hpp or the value of the enviroment variable THREADS). The creation of this object does not block the
remaining program flow. To get the BDD function from Helper::Future f just call f.getValue().
This function blocks until the result is available. This is all that is needed to work with parallel calculations in JINC.

JINC provides a novel multi-operand APPLY algorithm. This, in combination with the multi-threading approaches can group different function calls to one logical unit.
To group several function calls to one unit. Each function has to be assigned to an Expression.
The operators are overloaded for the expression type so that the logical unit can be written as before. It is important to note, that all calls have to be defined before calling apply so that
the compiler can create the complete syntax tree. With the complete information JINC can optimize the memory usage so that no temporary node will be created. Please have a look at the benchmarks to see the effect of this multi-operand APPLY algorithm. For more details of the algorithm please have a look in the publications.