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.

 stack_tree(+Stack, -Tree) is det[private]

Translate the solver Stack into a tree. The solver stack is represented as a flat list of proved goals where [] indicates this branch is complete. Here are some examples

[p, []] p-[] [p, q, [], []] p-[q-[]] [p, q, [], r, [], []] p-[q-[],r-[]]

We maintain a stack of difference lists in the 4th argument. On encountering a [] we pop this stack.

 filter_tree(+Children, +Module, -FilteredChildren, +Options)[private]

Clean the tree from less interesting details. By default removes auxiliary nodes created as part of the compilation and the NMR proof if this is empty. Additional filtering is based on Options:

pos(true)

Remove all not(_) nodes from the tree.

long(true)

Keep the full tree, including forall() and intermediate nodes.

 filter_pos(+Node, +Options) is semidet[private]

Filter negated nodes when --pos is active. We should not filter the global constraint nodes.

 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.

 plain_output(+FilterChildren, +Options)[private]

 term(+Node, +Options) is det[private]

Print a, possibly annotated, stack 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.