stack.pl

 justification_tree(:Stack, -JustificationTree, +Options)

Process Stack as produced by solve/4 into a justification tree. Options include:

<none yet>

The tree format is defined as follows.

• The tree as a whole is module-qualified with the same module as the input Stack.
• Each node takes the shape Node-Children, where Node is an atom (in the logical sense) and Children is a (possibly empty) list of sub-trees that justify the Node.
• Nodes (atom) may be wrapped in one or more of

  not(Node)

  NAF negation

  - Node

  Classical negation

  chs(Node)

  Node was proven by co-induction ("it is assumed that ...")

  proved(Node)

  Node was proven before ("justified above")

  assume(Node)

  Node was assumed (matching chs(Node)).

The root node has the atom query and has two children: the actual query and the atom o_nmr_check which represents the global constraints.

 print_justification_tree(:Tree) is det

 print_justification_tree(:Tree, +Options) is det

Print the justification tree as returned by justification_tree/3 or scasp_justification/2. The tree is printed to the current output stream. Options:

format(+Format)

One of unicode (default) or ascii.

depth(+Integer)

Initial indentation (0)

indent(+Integer)

Indent increment per level (3).

full_stop(+Bool)

End the tree with a full stop and newline. If false, it ends with the last atom.

 unqualify_justitication_tree(:TreeIn, +Module, -TreeOut) is det

Unqualify the nodes in TreeIn, turning the nodes qualified to module Module into plain nodes.

Re-exported predicates

The following predicates are exported from this file while their implementation is defined in imported modules or non-module files loaded by this module.

 print_justification_tree(:Tree) is det

 print_justification_tree(:Tree, +Options) is det

Print the justification tree as returned by justification_tree/3 or scasp_justification/2. The tree is printed to the current output stream. Options:

format(+Format)

One of unicode (default) or ascii.

depth(+Integer)

Initial indentation (0)

indent(+Integer)

Indent increment per level (3).

full_stop(+Bool)

End the tree with a full stop and newline. If false, it ends with the last atom.