Clingo{f} Home Page
Clingo{f} is an inference engine for language ASP{f}.
It is derived from clingo 2.0.2.
The ASP{f} language allows for a direct representation
of nonHerbrand functions in ASP. For more
details, refer to [bal12,bal12b].
The latest version is 0.4.4.
Installation and Usage
To install Clingo{f}
 Ensure that cmake
is installed on your computer and accessible from commandline without specifying any path.
 Ensure that re2c
is installed on your computer and accessible from commandline without specifying any path.
The latest version of re2c can be found here.
 Download clingo{f} using the links below.
 If you with to compile clingo{f} from sources:
 Uncompress the archive and change directory to the newly created directory.
 Run ./init.sh
 cd build/clingof/release
 Run make
 Copy the executable bin/clingof to the desired location.
To run clingo{f}
Usage: clingof [<number of models; default: 1>] [[<input file 1>] [<input file 2>...]]
E.g.: clingof 0 instance1 main_program
Finds all the answer sets of the program consisting of files instance1 and main_program.
Command clingof v shows the complete list of commandline options.
Some clingospecific options are not supported by clingof and will
be removed soon.
Syntax

Tliterals from [bal12,bal12b] are specified in clingo{f} with symbol '#'. For example,
f(x) #= f(y)
says that f(x)
is equal to
f(y).
Similarly, f(x) #!= f(y)
says that f(x)
is different
from f(y).

Symbols for nonHerbrand functions must be
declared explicitly. In the example above, function f should be declared
with:
#nherb f/1.
An equivalent, alternative declaration is:
#nherb f(X).
Functions that are not declared as nonHerbrand are treated
by the #connectives as having value identical to themselves.
For example, in the program:
#nherb f/1.
f(a) #= k(1).
f/1 is a nonHerbrand function, but k/1 is not.
Therefore, the meaning of the program is that
f(a) has value k(1).
Similarly, the program:
#nherb f/1.
f(a) #= 2.
p : f(a) #= k(1).
does not yield p because the value of f(a) is 2 and
not k(1).
On the other hand, the program:
#nherb f/1.
#nherb k/1.
f(a) #= 2.
k(1) #= 2.
p : f(a) #= k(1).
yields p. In fact, the body of the last rule checks
if the value of f(a) is equal to the value
of k(1), which is set to 2 by the second rule of the
program.

If one wants all the function symbols to be
interpreted by the #connectives as nonHerbrand,
this can be accomplished by the single declaration:
#nherb.
as in the program:
#nherb.
f(a) #= 2.
k(1) #= 2.
p : f(a) #= k(1).

Note that only #connectives are affected by whether
a function symbol is Herbrand or nonHerbrand.
All occurrences of function symbols in the rest of
the program are treated as usual. For example,
the program:
#nherb.
f(a) #= 2.
k(1) #= 2.
p : f(a) #= k(1).
non_negative(k(1)).
: non_negative(F), F #< 0.
yields non_negative(k(1)) but does not yield
non_negative(2), which would happen if k were
to be treated as a nonHerbrand function symbol
throughout the program.
Incidentally, the program:
#nherb.
f(a) #= 2.
k(1) #= 2.
p : f(a) #= k(1).
non_negative(k(1)).
: non_negative(F), F #< 0.
is inconsistent because k(1)'s value of 2 triggers
the constraint.

The clingo directive "#hide." also applies to
seed tatoms. Therefore, for the program:
#nherb.
f(a) #= 2.
p : f(a) #> 1.
#hide.
clingof will display an empty answer set.
To hide only the seed tatoms, directive
"#hide #nherb." can be used. For the program:
#nherb.
f(a) #= 2.
p : f(a) #> 1.
#hide #nherb.
clingof displays an answer set containing only p.

A directive such as "#hide #nherb f/1." can be used
to selectively hide the seed tatoms for nonHerbrand
function symbol f, as in:
#nherb.
f(a) #= 2.
p : f(a) #> 1.
#hide #nherb f/1.
Similarly, "#show #nherb f/1." can be used to
selectively show the seed tatoms for f:
#nherb.
f(a) #= 2.
p : f(a) #> 1.
#hide.
#show #nherb f/1.
For these latter #hide and #show directives, the
equivalent, alternative form "#hide #nherb f(X).",
"#show #nherb f(X)." exists.
Syntax restrictions:

Variables occurring in dependent tliterals must satisfy the same safety requirements as those occurring in literals under default negation.
For example, the following programs are syntactically correct:
P1:
#nherb.
p(X,Y) : l(X)#=Y.
P2:
#nherb.
l(a)#=3.
p(X,Y) : l(X)#=Y.
P3:
#nherb.
d(a;b).
l(a)#=3.
p(X) : d(X), l(X)#!=2.
while these ones are not:
P4:
#nherb.
l(a)#=3.
p(X) : l(X)#!=2.
P5:
#nherb.
l(a)#=3.
p(X,Y) : l(X)#!=Y.
Example of use
Let ex1.aspf be the program:
#nherb.
dom(1..10).
x(0) #= 1.
x(1) #= V :
dom(V),
x(0) #= V,
not x(1) #!= x(0).
x(1) #= 2 : change(x,0).
change(x,0).
Executing clingof 0 ex1.aspf produces:
Warning: #!=/2 is never defined.
Answer: 1
dom(0) dom(1) dom(2) dom(3) dom(4) dom(5) dom(6) dom(7) dom(8) dom(9) dom(10) change(x,0) x(0)#=1 x(1)#=2
Models : 1
Time : 0.000
(The warning about #!=/2 not being defined should be ignored.)
Let ex2.aspf be the program:
#nherb.
cod(a;b).
dom(1..2).
0{ f(X)#=V : dom(V) }1 : cod(X).
num(N) : N=count{ f(X)#=V : dom(V) : cod(X) }.
num(V,N) : dom(V), N=count{ f(X)#=V : cod(X) }.
tot(S) : S=sum[ f(X)#=V : dom(V) : cod(X) = V ].
p #= 1 : not p #!= 1.
p #= 2 : f(a) #= f(b).
Executing clingof 0 ex2.aspf produces:
Warning: #!=/2 is never defined.
Answer: 1
cod(a) dom(1) dom(2) cod(b) num(2) num(1,1) num(2,1) tot(3) p#=1 f(a)#=1 f(b)#=2
Answer: 2
cod(a) dom(1) dom(2) cod(b) num(1) num(1,1) num(2,0) tot(1) p#=1 f(a)#=1
Answer: 3
cod(a) dom(1) dom(2) cod(b) num(2) num(1,2) num(2,0) tot(2) p#=2 f(a)#=1 f(b)#=1
Answer: 4
cod(a) dom(1) dom(2) cod(b) num(1) num(1,1) num(2,0) tot(1) p#=1 f(b)#=1
Answer: 5
cod(a) dom(1) dom(2) cod(b) num(2) num(1,1) num(2,1) tot(3) p#=1 f(a)#=2 f(b)#=1
Answer: 6
cod(a) dom(1) dom(2) cod(b) num(0) num(1,0) num(2,0) tot(0) p#=1
Answer: 7
cod(a) dom(1) dom(2) cod(b) num(1) num(1,0) num(2,1) tot(2) p#=1 f(a)#=2
Answer: 8
cod(a) dom(1) dom(2) cod(b) num(1) num(1,0) num(2,1) tot(2) p#=1 f(b)#=2
Answer: 9
cod(a) dom(1) dom(2) cod(b) num(2) num(1,0) num(2,2) tot(4) p#=2 f(a)#=2 f(b)#=2
Models : 9
Time : 0.000
Downloads
Clingo{f} should run
without problems under most Unix variants and C/C++ compilers. It was tested under
Linux Fedora 11 and 16, and compiled using gcc 4.4 and 4.6.
Questions, Bugs, etc.
Send emails to marcello.balduccini@gmail.com.
Authors
Clingo{f} was written by Marcello Balduccini.
Clasp and Clingo were written by Roland Kaminski.
References
[bal12] Marcello Balduccini,
A ``Conservative'' Approach to Extending Answer Set Programming with NonHerbrand Functions, 2012.
To appear.
[bal12b] Marcello Balduccini,
Answer Set Solving and NonHerbrand Functions, 2012.
Back to my home page
Author: Marcello Balduccini (marcello.balduccini@gmail.com)
Last Update: 01/16/15