dyncall.pl --

This predicate assembles the clauses that are reachable from a given goal.

Issues:

• Represent classical negation as -Term? Alternatives:
  • Just use -Term. Disadvantage is program analysis and module dependencies.
  • Provide goal- and term-expansion to intern the - into the functor name. Disadvantage is that we need scasp_assert/1, etc.

 scasp_show(:Query, +What)

Show some aspect of the translated s(CASP) program. Currently What is one of:

code(Options)

Show the collected program. By default shows the query and user program. To show only the integrity constraints, use:

?- scasp_show(Query, code(user(false), constraints(true))).

 scasp_query_clauses(:Query, -Clauses) is det

Arguments:

Clauses

- is a list of source(ClauseRef, Clause).

 scasp_dynamic(:Spec) is det

Declare a predicates as dynamic or thread_local. Usage patterns:

:- scasp_dynamic p/1. :- scasp_dynamic p/1 as shared.

 scasp_assert(:Clause) is det

 scasp_retract(:Clause) is nondet

 scasp_retractall(:Head) is det

Wrappers for assertz/1, retract/1 and retractall/1 that deal with sCASP terms which may have a head or body terms that are wrapped in -(Term), indicating classical negation. Also deals with global constraints written in any of these formats:

• false :- Constraint.
• :- Constraint.

 scasp_abolish(:PredicateIndicator) is det

Remove all facts for both PredicateIndicator and its classical negation.

 #(:Directive)

Handle s(CASP) directives. Same as :- Directive.. Provides compatibility with sCASP sources as normally found.

 abducible(:Spec)

Declare Spec, a comma list of heads to be abducible, meaning they can both be in or outside the model.

 #=(?A, ?B)

 #<>(?A, ?B)

 #<(?A, ?B)

 #>(?A, ?B)

 #>=(?A, ?B)

 #=<(?A, ?B)

Implementation of the s(CASP) constraints. This implementation is normally not used and mostly makes the program analysis work.

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.

 scasp(:Query) is nondet

 scasp(:Query, +Options) is nondet

Prove query using s(CASP) semantics. This performs the following steps:

• Collect (transitively) all clauses that are reachable from Query.
• Collect all global constraints whose call-tree overlaps with the query call tree.
• Establish the compiled s(CASP) representation in a temporary module
• Run the s(CASP) solver
• Optionally extract the model and justification tree.

Options are passed to scasp_compile/2. Other options processed:

model(-Model)

Unify Model with the s(CASP) model, a list of model terms. See scasp_model/1.

tree(-Tree)

Unify Tree with the s(CASP) justification tree. See scasp_justification/2 for details.

source(Boolean)

When false, do not include source origin terms into the final tree.

 scasp_model(:Model) is semidet

 scasp_model(:Model, +Options) is semidet

True when Model represents the current set of true and false literals.

 scasp_justification(:Tree, +Options) is semidet

Justification for the current sCASP answer.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 #(Arg1, Arg2)

 abducible(Arg1, Arg2)

 pred(Arg1)

 scasp_assert(Arg1, Arg2)

 show(Arg1)