welcome: please sign in
location: attachment:usermanual.html of dlvex

Attachment 'usermanual.html'

Download

DLV 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 (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 (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.

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

r1: head1(S) :- number(N), #sqr(N,S).

r2: head2(S1) :- number(N), #fatt(N,S), #sqr(S,S1).

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:

r1: head3(S) :- number(S), #sqr(N, S).

r2: head2(S1) :- number(S), #fatt(N,S), #sqr(S,S1).

In fact, there are no oracles w.r.t. the pattern oi. Thus, in order to make the rule safe, the user should define the oracles #sqr_oi and #fatt_oi in some library, and then import it within the dlv program.

We call this weak safety, and it’s applied to non-recursive rules having at least an external builtin atom in the body. When an external builtin atom belongs to the body of a rule which is inside a recursive cycle, the strong safety has to be checked. The following rule:

r1: lessthan(Z) :- lessthan(Y), #succ(Y,Z).

is not safe, since the variable Z appears in the head of the rule r1 but does not appear in any positive standard predicate of the body. It would be necessary to write, for instance:

r1: lessthan(Z) :- lessthan(Y), #succ(Y,Z), saving(Z).

If there is some unsafe rule, the system exits giving an error message.

Relaxing Safety

The user can, under her responsibility, force the evaluation of even non-safe (w.r.t. external  builtins) rules, specifying the "-RBS" (Relaxed Builtin Safety) option at the command line. There are two ways:

1.    -RBS = ALL

2.    -RBS = builtin_name1[, builtin_name2[,. . ., builtin_namen]]  

In the first case all the external builtins defined in the dlv program are relaxed. Therefore, all the non-strongly-safe rules containing external builtins in the body will be evaluated anyway. In the second case the "-RBS" option is used specifying the list of the builtins to be relaxed. Builtin names are separated by commas (","). In this case only the non-safe rules containing the external builtins specified in the list are forced to be evaluated.

Roughly, the "-RBS" option will force the system to evaluate the non-safe rules w.r.t. external builtins, while other lacks of safety will still cause the (usual) abnormal termination.

The same behaviour can be obtained within the program, using the #relaxsafety directive. As for the -RBS option, we have two possible uses: 

1.    #relaxsafety = ALL

2.    #relaxsafety = builtin_name1[, builtin_name2[,. . ., builtin_namen]]

The effect is of course the same.

Note: The two usages of the option are exclusive; and the specification by the command line or within the program are exclusive.

Creating Builtins Libraries

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.