Clingo{f} Home Page

Installation and Usage

1. Ensure that cmake is installed on your computer and accessible from command-line without specifying any path.
2. Ensure that re2c is installed on your computer and accessible from command-line without specifying any path. The latest version of re2c can be found here.
3. Download clingo{f} using the links below.
4. 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.

• T-literals 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 non-Herbrand 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 non-Herbrand 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 non-Herbrand 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 non-Herbrand, 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 non-Herbrand. 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 non-Herbrand 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 t-atoms. 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 t-atoms, 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 t-atoms for non-Herbrand 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 t-atoms 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.

#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).

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 

#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).

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} sources (version 0.1.3)
• clingo{f} Windows binary (version 0.1.3)

Questions, Bugs, etc.

Authors

References