Backends

The backends listed here are provided with clinguin. All available functions that can be referenced in the ui-state for each backend are listed below. Notice that all backends will also include the functionalities of the ones they extend.

The source code for the backends can be found in github.

ClingoBackend

Implements all basic clingo functionality for single-shot solving.

Examples

• sudoku_single_shot

Domain state constructors

The domain state also inclues domain constructors from the parent class.

ClingoMultishotBackend

Extends ClingoBackend with functionality for multi-shot solving. Adds options to access and store assumptions and externals.

Examples

• sudoku

• jobshop

• placement

Domain state constructors

The domain state also inclues domain constructors from the parent class.

ClingraphBackend

Extends ClingoMultishotBackend with functionality to render and interact with clingraph images.

Warning

To use this backend you might need to manually install Graphviz. See the clingraph instalaltion for details.

Examples

• graph_coloring

• tree_browser

• ast

This backend will allow the use of clingraph images inside a canvas element. To use this feature, the user must provide a clingraph visualization encoding via the command line in argument --clingraph-files. The input to this encoding will be the domain-state (same input as for the ui-files).

Tip

The clingraph encoding will also have information about brave, and cautious consequences. So dont be afraid to use it in the graphs!

A clinguin canvas is enhanced with an attribute image_type. When the value for this attirbute starts with clingraph it will be substituted by the ClingraphBackend for the svg representation of the graph. By default the graph named default will be used, another graph with name X can be used by setting the image type to clingraph__X

Note

To use this backend with the TkinterFrotend, you must provide the option --intermediate-format=png.

Examples

Creates a canvas in a window that will contain the default clingraph graph

elem(c, canvas, window).
attr(c, image_type, clingraph).

Interacting with the graph

To interact with the clingraph nodes/edges, additional steps must be made. Each node/edge must be added to the UI as an element inside the canvas using the type svg_node (svg_edge). This type of elements require the identifier of the clingraph node/edge in argument clingraph_id to link the interactivity with the svg element generated by clingraph.

Examples

Continuation of the previous example.

elem(n(X), svg_node, c).
attr(n(X), clingraph_id, X):- node(X).

node(X) is generated in the ui-files

Tip

Notice that the clingraph nodes are not accesible by the ui-files. Therefore, nodes of the clingraph images have to be generated again in this encoding.

Consider separating the clingraph node generation into a diferent encoding, and then including it in the UI and clingraph encodings.

Warning

The interactive feature only work in web based frontends, not in Tkinter.

Note

update actions applied to clingraph elements (svg_nodes) will update the html style, not the graphviz properties. Therefore, it can be used to set things like visibility and opacity but not internal clingraph values.

ExplanationBackend

Extends ClingoMultishotBackend with functionality to compute Minumal Unsatisfiable Cores (MUC) when there is an UNSAT output.

Examples

• sudoku_advanced

• sudoku_explained

When the domain-control produces an unsatisfiable output this backend will perform subsequents calls to find the subset minimal assumptions that caused the unsatisfiablity. These assuptions not only include those selected by the user, but also can be part of the input. This is needed when some of the input facts also want to be shown to the user. Therefore, this backend adds an argument to the command line: --assumption-signature in which the user can select which signatures will be considered as assumptions in the MUC computation.

Examples

The sudoku_advanced example provides the argument --assumption-signature=initial,3 so that all the initial values of the sudoku are also considered in the unsat core and therefore shown to the user.

attr(pos(X,Y),class,"bg-primary"):-pos(X,Y), not _clinguin_muc(sudoku(X,Y,_)), not _clinguin_muc(initial(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(sudoku(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(initial(X,Y,_)).

The domain-state is then enhanced by the MUC using predicate muc/1.

Examples

In the sudoku, the MUC information will show in red the faulty assumptions.

attr(pos(X,Y),class,"bg-primary"):-pos(X,Y), not _clinguin_muc(sudoku(X,Y,_)), not _clinguin_muc(initial(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(sudoku(X,Y,_)).
attr(pos(X,Y),class,"bg-danger"):-pos(X,Y), _clinguin_muc(initial(X,Y,_)).

Domain state constructors

The domain state also inclues domain constructors from the parent class.

ClingoDLBackend

Extends ClingoMultishotBackend with functionality to accept clingo-dl programs as input.

Examples

• jobshop

The domain-state is then enhanced by predicate _clinguin_assign/2.

Examples

In the jobshop example, the assignment is used for the label of the job.

elem(tctime(T,ST), label, tc(T,ST)):- _clinguin_assign((T,ST),Start).
attr(tctime(T,ST), label, @concat("","@",Start,"-",Start+ET)):- _clinguin_assign((T,ST),Start), executionTime(T,ST,ET).
attr(tctime(T,ST), class, "fw-light"):- _clinguin_assign((T,ST),Start).
attr(tctime(T,ST), fontSize, "8px"):- _clinguin_assign((T,ST),Start).

Warning

Notice that asisgnments are not part of the brave or cautious consequences

Domain state constructors

The domain state also inclues domain constructors from the parent class.

Creating your own backend

By creating your own backend you can extend functionality and edit the existing server workflow. If you are using clingo, we highly recomend extending the ClingoMultishotBackend to create your own. This backend contains multiple functionalities already built in wich can be overwritten and extended. The following explanation assumes that this is the backend that is being extended.

Note

If you will not use multi-shot functionalities, assumptions and exterals you can also extend the ClingoBackend.

Note

Using your backend

To make your custom backend avaliable to clinguin, you must provide the path via the command line argument --custom-classes.

In what follows we divide the possible extensions. For more implementation details, look at the source code All the presented methods can be overwritten to your desire.

Constructor

In the constructor one can add custom arguments and new domain-state constructors.

Examples

• explanation_backend

• clingraph_backend

• clingodl_backend

Register options

By overwritting this class method, one can add new arguments to the command line. These options will be added under a group for the created backend.

Examples

• explanation_backend

• clingraph_backend

Setups

These methods will handle the arguments depending on the clinguin state. Some are called at the start after a restart or when a change is done in the solving. When a custom argument is added to the backend if will likely need to be handled here.

Examples

• explanation_backend

• clingodl_backend

Solving

These methods are involved on how the domain control is solved. They can be ovweritten for theory extensions among other things.

Examples

• explanation_backend

• clingodl_backend

UI updates

If any changes want to be made in how the UI state is computed they can be made by overwritting this method.

Examples

• clingraph_backend

Domain state

These methods take care of generating the domain-state. When new information wants to be added a domain state constructor can be included. These domain constructors will be automatically called by the _domain_state property. But, they need to be previously registered in the constructor using the functions below.

Examples

• explanation_backend

• clingodl_backend

• clingraph_backend

Note

Some of the domain constructors involve extra work so they are handled as @cache_property.

Warning

Make sure any domain constructor added is a property with anotation @property

Note

Domain state constructors for this backend are showed in the section above. These constructors can also be overwritten if necessary.

Output

The propery method below is used to generate an output program for downloads

Public operations

Each backend can define any number public operations or overwrite the existing ones. These operations are any public method of the class and will be accessible to the UI.

Examples

• explanation_backend