This
manual describes the syntax of external builtins, which provide the
opportunity to perform calls to external C++ functions. This feature is realized
by introducing “parametric” external predicates, whose extension is not
specified through a logic program but explicitly computed through external
code.
Within a dlv
program, the name of an external builtin is preceded by the conventional
‘#’
symbol. For instance, #fatt(X,N) or
#sum(X,Y) are
supposed to be (external defined) builtins. An external builtin can appear
inside bodies and constraints only, and cannot be negated nor true
negated.
Each
external builtin #p of
arity n, has a C++ boolean function p’ (called
“oracle”) associated, taking
n “constant” arguments. This function is defined by the user. This
roughly means that a ground atom #p(a1,...,an) is true
iff the value returned by p’(a1,…,an) is
true.
Example.
Consider the
external predicate #fatt(X,Y)
implementing the external computation of the factorial function. Its oracle
fatt’
should
be implemented such
that fatt’(a,b) is true
iff b is the factorial of a,
when X is
bounded to a and
Y to
b.
Definition: We
call pattern a list of i’s and o’s. An i
(input value) is a placeholder for a constant or a bounded variable,
whereas an o (output value) is a placeholder for a (still)
unbounded variable. Given a list of terms, the corresponding pattern will be a
proper row of o’s and i’s.
Note: It
should be intuitive that a builtin may have associated many different patterns
depending on the list of its terms; and even the same list may induce different
patterns, depending on the actual binding of the variables. So the user can
define more than one oracle function, each one associated to a particular
pattern.
o
#fatt_ii –
oracle ii invoked when X and Y are
both bound (input).
o
#fatt_io –
oracle io invoked when X is bound
(input) and Y not (output).
o
#fatt_oi –
oracle oi invoked when X is not bound
(output) while Y is (output).
Definition: The oracle expecting only input
terms is called “base oracle”, while others are called “talkative oracles”.
Every external builtin MUST have associated at least its base
oracle.
NOTE: It is worth remember that our builtins are
intended to be functional with respect to the same function. This means that
each oracle must be consistent with the base one. More formally, if f is the function implemented by the
oracles defining a given builtin, the following must hold:
i
o
i
i
f(a,X) = b ó
f(a,b) =
true
Safety
While
writing dlv programs containing external builtins a couple of things must be
regarded in order to write safe rules. A builtin atom is NOT SAFE
if:
q
There are no proper
oracles defined corresponding to the actual pattern induced by the binding
within the rule in which appears. (weak
safety).
q
When the builtin
belongs to the body of a rule which is inside a recursive cycle: among the list
of its terms there is a variable appearing also in the head of the rule and not
appearing in some positive standard predicate in the body (strong safety).
Strong
safeness constraints are introduced in order to deal with cases which may lead
to the generation of an infinite Herbrand universe when employed in recursive
rules. Imagine to define an oracle for the builtin #succ such that #succ(A,B) is
true if and only if A and B are integers and B = A +
1. The grounding algorithm launched on the rule
int(X)
:- int(Y), #succ(X,Y).
would
never reach a fixed point.
are
safe, since there are proper oracles defined w.r.t. the actual pattern io
induced by the binding for both
atoms. The
following rules, vice versa, are unsafe:
In
order to build builtin libraries there are three files
needed:
Further
details follow.
The
semantic of a builtin is given by the operational definition of all its oracles,
grouped in one or more libraries. Libraries have to be built such that they can
be dynamically linked to dlv executable. An header file (namely "extpred.h") is
provided as it contains all things needed to exchange data from/to dlv.
More
in detail, the C++ source code
should appear as in the following.
NOTE:
files defining oracles MUST have “.C” (uppercase)
extension.
//////////////////////////////////////////////////////////////////////////////
//Dynamic Library for the external
predicate
#include
"extpred.h"
#ifdef
__cplusplus
extern "C" {
#endif
BUILTIN( external_predicate , pattern
)
{
< C++ instructions
>
}
. . .Other Oracles. .
.
#ifdef
__cplusplus
}
#endif
//////////////////////////////////////////////////////////////////////////////
It
is worth noting that including “extpred.h”
is
mandatory. This header contains some directives and the definition of the
CONSTANT class,
which is used in order to give parameters to the C++-defined oracles and manage
base-types from/to dlv/C++. Implementations must be enclosed inside the
directive
#ifdef
__cplusplus
extern "C" {
#endif
. . . . .
#ifdef
__cplusplus
}
#endif
Each
oracle function is declared by such an header:
BUILTIN( external_predicate , pattern
)
Where BUILTIN is a macro which is defined (in extpred.h) as:
#define BUILTIN(name,pattern) bool name##_## pattern
(CONSTANT *argv)
where name is the external predicate name, and pattern is
the pattern of the oracle being implemented. Remember that pattern is
essentially a string constituted by “i” (lowercase) and “o” (lowercase); the
succession is positional: the j-th position of the pattern string is occupied by
an “i” if for the
oracle being defined the j-th term is in “input”; and as it can be easily imagined an “o” means that the
j-th term is in “output”.
Each oracle is a boolean function whose only parameter
argv
is
an array of CONSTANTs, and the positions
contain “input” or “output” parameters depending on the corresponding pattern.
Each function name thus encodes the name of the associated
external builtin it implements and the pattern which it responds to.
NOTE: in order to try to guarantee a correct execution, dlv
catches possible exceptions arising while executing an oracle; this means that
whatever goes wrong while the code of the oracle is running will be ignored, and
the final result will be assumed as FALSE w.r.t. the matching phase. A message
will be put on the standard error, alerting the user about both the (possibly)
wrong oracle and the possibly inconsistent answer sets.
The
CONSTANT
class.
CONSTANT is a
public class defined in extpred.h and, as
already said, it provides what is needed in order to manage
parameters for the C++ defined oracles and manage base-types from/to dlv/C++.
The methods provided are the following:
First method returns an integer of according
value, while the second and third methods are used to
cast from strings (encoded by dlv) to standard C++ string
(i.e. char*) types.
Below a simple example try to clarify the difference between
a DLV string and a DLV symbolic string.
In order to create a DLV string (quoted or symbolic), the
CONSTANT class has a proper constructor receiving two arguments. The first one
is the name of the string, the second one is a boolean (false by default):
CONSTANT(const char *name2, bool quoted = false);
If the user wishes to define a DLV string, she must pass true as the second argument. By default, a symbolic DLV string (i.e. a constant) is created. For instance, if the user writes:
…CONSTANT(string, true)
string is considered as quoted string (like “ExtendedBuiltin”), while with
…CONSTANT(string) or CONSTANT(string, false)
string is considered as constant (symbolic string, like red).
The rest of the methods within the CONSTANT class are the
following:
In order to cast from C++ types back to
dlv it is enough to pass the object as parameter to the
constructor. Please note that the default constructor builds a CONSTANT as NullConst.
Moreover comparison and
assignment operators for CONSTANT objects
are
supplied.
Example. Suppose we have defined the external predicate #fatt(X,Y) implementing the external
computation of the factorial function. The user must encode and include a
library source file similar to the following:
//////////////////////////////////////////////////////////////////////////////
//Shared Library for the external builtin #fatt
//fatt_builtin.C
#include "extpred.h"
#ifdef __cplusplus
extern "C" {
#endif
BUILTIN(fatt,ii)
{
if(
argv[0].isInt() && argv[1].isInt() )
{
// Convert the CONSTANT data to what we do have
to compute
int x=
argv[0].toInt();
int y=
argv[1].toInt();
// Just perform
the computation...
int fatt=1;
for(int i = 1;
i <= x; i++)
fatt=fatt*i;
if( fatt == y)
return true;
}
return false;
}
BUILTIN(fatt,io)
{
if( argv[0].isInt() )
{
// Convert the CONSTANT data to what we do have to compute
int x = argv[0].toInt();
// Just perform the computation...
int fatt = 1;
for(int i = 1; i <= x; i++)
fatt=fatt*i;
// Convert the result into the proper CONSTANT data
// Save the result onto the output vector
argv[1] = CONSTANT( fatt );
return true;
}
return false;
}
BUILTIN(fatt,oi)
{
if( argv[1].isInt() )
{
// Convert the CONSTANT data to
what we do have to compute
int x = argv[1].toInt();
// Just perform the computation...
int fatt = 1;
for(int i = 1; i <= x; i++)
{
fatt=fatt*i;
if( fatt == x )
{
// Convert the result into
the proper CONSTANT data
// Save the result onto the
output vector
argv[0]=CONSTANT(i);
return true;
}
}
}
return false;
}
#ifdef __cplusplus
}
#endif
NOTE: the builtin developer should pay attention to the type of
each element within argv, in order to proper manipulate data. Please notice that in the examples the type check at the
very beginning of each oracle is performed only with respect to the input
variables; the output ones will be properly set within the oracle itself, since
they result as Null constants, at first.
Compiling
$ ./dynamic
fatt_builtin
where dynamic is a provided script which executes what is needed in order
to build the library. Note as no extension is given, compiling will result in a
“.so” file, which constitutes a dynamic library.
It is worth noting that “.C” extension is omitted.
Furthermore multiple files can be compiled, and an unique library file (named as
the first file in the list) will be created. For instance:
$ ./dynamic prova1 prova2 prova3
will produce the file prova1.so which will contain all oracles defined within the three
source files.
Symbols vs Strings
In order to better clarify the difference between symbols
and strings in DLV, some examples follow.
containing characters which are not normally allowed. This
means that a fact like
ip(160.97.47.136).
cannot be handled. So the term may be defined as quoted
string:
ip(“160.97.47.136”).
where ip predicate represents a
valid IP address. Please note as the term is a string here, instead of a
symbolic name or an integer.
Example
2. This suggests how, for instance, distinguish different
concepts, as showed in the following.
graph( red ) :
red
is a symbolic
name for the color ‘red’.
The user may exploit the former or the latter depending on
the meaning she wants to give express.
1.
#include < mylib >
or
2.
#include “/PATH/TO/mylib”
Thus the system will import only the “mylib” library (the
“.so” extension when is omitted).
In the first case DLV looks for the specified library into
the default folder (i.e. ./LIB), while in the second the user has to provide the
full path.
A command line option can be specified in order to set a different
path (folders separated by colons):
$ dlv [....]
-libpath=/usr/local/lib/dlv:/home/myuser/lib
Of course, DLV will look for the path of the libraries
specified whithin the DLV program among those provided by the command
line.
NOTE: default
folder is LIB, so, if the user defines her own lib folder, it will be considered
as different from LIB.
It is worth remembering that not including appropriate
libraries when exploiting external builtins into DLV programs will cause an
execution abortion.
Some Cares. The user should pay
attention to the following.
Overloading DLV “factory” Builtins
Library
developers may redefine “internal” DLV builtins. In order to do that, it is
simply enough to define a library containing proper oracles, and import it. The
actual names of the oracles are:
#less_builtin
stands for
<
#less_or_equal_builtin
stands for
<=
#greater_builtin
stands for
>
#greater_or_equal_builtin
stands for
>=
#not_equal_builtin
stands for
!= and <>
#plus_builtin
stands for
+
#times_builtin
stands for
*
#succ
stands for
#succ
For instance,
the (final) user may write the following DLV program:
#include
<my_lib>
ok :- p(X), p(Y), X !=
Y.
provided that
my_lib.so contains a definition such as:
BUILTIN(not_equal_builtin,ii)
{
…
}
In fact, DLV
will look for a proper oracle for !=(ii), and will adopt the
“factory” one only if no other is found within the imported libraries.
Last modified
2004-oct-28