Attachment 'usermanual.html'
DownloadDLV EXTERNAL BUILTINS USER MANUAL (pre-release, evolving - please check home page for latest news and releases)
Overview
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.
Syntax
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.
Semantics
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 is and os. 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 os and is.
Example. The corresponding pattern for the list of terms X,b,Y is o,i ,o, supposing that X and Y are unbound.
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.
Example. Consider the external builtin #fatt(X,Y) which implements the external computation of the factorial. The user may have defined three oracle functions. The one actually invoked will depend on the actual pattern, as told above.
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.
Example. Suppose that oracles #sqr_io and #fatt_io are defined in some library. The following rules
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:
- extpred.h (containing signatures of all needed methods)
- extpred.o (the object file that will be linked to the user object code)
- dynamic (a script helping the user compiling and linking the code)
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:
- toInt()
- toString()
- toSymbol()
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:
- getType(): returns the type of a CONSTANT object, as enumerated: Integer, Symbol, String, NullConst;
- isInt(): returns true if the current object is an Integer, false otherwise;
- isString(): returns true if the current object is a quoted string, false otherwise;
- isSymbol(): returns true if the type of the current object is a symbolic string, and false otherwise;
- isNull(): returns true if the type of the current object is NullConst, and false otherwise. In particular an object is NullConst if the base constructor is invocated;
- toString(): returns the string as non-quoted;
- toQuotedString(): returns the string as quoted;
- toSymbol(): returns the symbol (non-quoted);
- toInt(): returns the integer value of CONSTANT object;
- CONSTANT(): default constructor. Creates a CONSTANT object of NullConst type;
- CONSTANT( const CONSTANT & );
- operator=( const CONSTANT & );
- CONSTANT( const char *, bool = false): see above;
- CONSTANT( const int & ): see above;
- ~CONSTANT();
- operator!= ( const CONSTANT & );
- operator== ( const CONSTANT & ).
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
Once it is completed, it is sufficient to compile the source file:
$ ./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.
Example 1. Suppose having to manage IP addresses. An IP address appear like
160.97.47.136
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 the 3-character string containing r, e and d.
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.
Using Externally Defined Predicates into dlv Programs
In order to write dlv programs containing one or more external builtins, you have simply to tell where to find libraries containing oracles, using the #include directive. If you want to import a specific library just write down the name:
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.
- If multiple definitions for the same oracle are imported, only the first encountered will be adopted.
- More than one #include directive can be given, but all of them have to be put at the beginning of the file containing the dlv program.
- The user can freely define standard predicates having the same name of some builtin. For instance the same program may contain p(...) and #p(...), and they will be distinguished. On the other hand, the user cannot override some identifiers; think about predefined aggregates (#sum, #count, etc.) or keywords like #template.
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.
Attached Files
You are not allowed to attach a file to this page.