scasp.pl -- Using s(CASP) from Prolog

While library(scasp/main) is used to build the scasp executable, this library (library(scasp)) is used to embed or dynamically create s(CASP) programs in Prolog and query them from Prolog.

 ?--(:Query)

 ?+-(:Query)

 ?-+(:Query)

 ?++(:Query)

 ?+++(:Query)

 ??+-(:Query)

 ??-+(:Query)

 ??++(:Query)

Shortcuts for scasp/1 that control printing the model and/or tree and the format. The +/- control whether the model and/or tree are printed (in that order). The ?? versions print the human version.

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.

 ∉(?X, +G)

Constraint that expresses that X is not a member of the list of ground elements in G.

 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_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_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_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_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.

 #=(?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.

 #=(?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.

 #=(?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.

 #=(?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.

 #=(?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.

 begin_scasp(+Unit)

 begin_scasp(+Unit, +Exports)

Start an embedded sCASP program. Exports is a list if predicate indicators as use_module/2 that defines the sCASP predicates that are made visible from the enclosing module as Prolog predicates. These predicates modify the Prolog syntax by:

• Defining appropriate operators
• Disable singleton checking

Otherwise the read clauses are asserted verbatim. Directives are terms #(Directive). Prolog directives (:- Directive) are interpreted as sCASP global constraints. The matching end_scasp/0 compiles the sCASP program and creates wrappers in the enclosing module that call the sCASP solver.

The sCASP code must be closed using end_scasp/0. Both begin_scasp/1,2 and end_scasp/0 must be used as directives.

 begin_scasp(+Unit)

 begin_scasp(+Unit, +Exports)

Start an embedded sCASP program. Exports is a list if predicate indicators as use_module/2 that defines the sCASP predicates that are made visible from the enclosing module as Prolog predicates. These predicates modify the Prolog syntax by:

• Defining appropriate operators
• Disable singleton checking

Otherwise the read clauses are asserted verbatim. Directives are terms #(Directive). Prolog directives (:- Directive) are interpreted as sCASP global constraints. The matching end_scasp/0 compiles the sCASP program and creates wrappers in the enclosing module that call the sCASP solver.

The sCASP code must be closed using end_scasp/0. Both begin_scasp/1,2 and end_scasp/0 must be used as directives.

 end_scasp

Close begin_scasp/1,2. See begin_scasp/1,2 for details.

 not(:Query)

sCASP NaF negation. Note that this conflicts with the deprecated standard Prolog not/1 predicate which is a synonym for \+/1. Make sure to load sCASP into a module where you want sCASP negation and use \+/1 for Prolog negation in this model.

 - :Query

sCASP classical negation.

 scasp_model(:Model) is semidet

 scasp_model(:Model, +Options) is semidet

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

 scasp_stack(-Stack) is det

True when Stack represents the justification of the current sCASP answer.

 scasp_justification(:Tree, +Options) is semidet

Justification for the current sCASP answer.

 scasp_listing(+Unit, +Options)

List the transformed program for Unit

Undocumented predicates

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

 pred(Arg1)

 ?(Arg1)

 #(Arg1, Arg2)

 show(Arg1)

 abducible(Arg1, Arg2)

 scasp_assert(Arg1, Arg2)

 ??(Arg1)