embed.pl -- Embed sCASP programs in Prolog sources

This module allows embedding sCASP programs inside a Prolog module. Currently the syntax is:

:- begin_scasp(UnitName[, Exports]).

<sCASP program>

:- end_scasp.

The idea is to create wrappers for the sCASP user predicates in the target module that evaluate an sCASP query as a normal Prolog query, providing access to the model and justification. The bindings come available as normal Prolog bindings.

This is an alternative interface to defining the user accessible predicates using e.g., `:- scasp p/1, q/2.`, which will then establish the reachable predicates and perform the sCASP conversion on them. I think both have their value and the above one is simpler to start with.

To be done

- : incomplete

 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.

 scasp_call(:Query)

Solve an sCASP goal from the interactive toplevel

 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

 pce_xref_gui:gxref_called(?Source, ?Callable)[multifile]

Hook into gxref/0 that may extend the notion of predicates being called by some infrastructure. Here, do two things:

• We silence called s(CASP) hooks
• If a predicate is defined using scasp_dynamic/1 and either the positive or negative version is called, we consider it called.

Undocumented predicates

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

 begin_scasp(Arg1, Arg2)

 scasp_model(Arg1, Arg2)