View source with raw comments or as raw

    1/*  Part of ClioPatria SeRQL and SPARQL server
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        J.Wielemaker@cs.vu.nl
    5    WWW:           http://www.swi-prolog.org
    6    Copyright (C): 2010, University of Amsterdam,
    7		   VU University Amsterdam
    8
    9    This program is free software; you can redistribute it and/or
   10    modify it under the terms of the GNU General Public License
   11    as published by the Free Software Foundation; either version 2
   12    of the License, or (at your option) any later version.
   13
   14    This program is distributed in the hope that it will be useful,
   15    but WITHOUT ANY WARRANTY; without even the implied warranty of
   16    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   17    GNU General Public License for more details.
   18
   19    You should have received a copy of the GNU General Public
   20    License along with this library; if not, write to the Free Software
   21    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
   22
   23    As a special exception, if you link this library with other files,
   24    compiled with a Free Software compiler, to produce an executable, this
   25    library does not by itself cause the resulting executable to be covered
   26    by the GNU General Public License. This exception does not however
   27    invalidate any other reasons why the executable file might be covered by
   28    the GNU General Public License.
   29*/
   30
   31:- module(count,
   32	  [ proof_count/2,		% :Goal, -Count
   33	    proof_count/3,		% :Goal, +Max, -Count
   34	    answer_count/3,		% ?Var, :Goal, -Count
   35	    answer_count/4,		% ?Var, :Goal, +Max -Count
   36	    answer_set/3,		% ?Var, :Goal, -Answers
   37	    answer_set/4,		% ?Var, :Goal, +Max, -Answers
   38	    answer_pair_set/5,		% ?Pair, :Goal, +MaxKeys, +MaxPerKey, -Answers
   39	    unique_solution/2		% :Goal, -Solution
   40	  ]).   41:- use_module(library(nb_set)).   42:- use_module(library(rbtrees)).   43:- use_module(library(nb_rbtrees)).

This module provides various ways to count solutions

This module is based on a similar collection introduces in the first ClioPatria release. Most names have been changed to describe the semantics more accurately.

The predicates in this library provide space-efficient solutions, avoiding findall/setof. Most predicates come with a variant that allows limiting the number of answers.

To be done: -
The current implementation is often based on library(nb_set), which implements unbalanced binary trees. We should either provide a balanced version or use Paul Tarau's interactors to solve these problems without destructive datastructures. */

   62:- meta_predicate
   63	proof_count(0, -),
   64	proof_count(0, +, -),
   65	answer_count(?, 0, -),
   66	answer_count(?, 0, +, -),
   67	answer_set(?, 0, -),
   68	answer_set(?, 0, +, -),
   69	answer_pair_set(?, 0, +, +, -),
   70	unique_solution(0, -).

proof_count(:Goal, -Count) is det

proof_count(:Goal, +Max, -Count) is det

True if Count is the number of times Goal succeeds. Note that this is not the same as the number of answers. E.g, repeat/0 has infinite proofs that all have the same -empty- answer substitution.

See also: - answer_count/3

   82proof_count(Goal, Count) :-
   83	proof_count(Goal, infinite, Count).
   84
   85proof_count(Goal, Max, Count) :-
   86	State = count(0),
   87	(   Goal,
   88	    arg(1, State, N0),
   89	    N is N0 + 1,
   90	    nb_setarg(1, State, N),
   91	    N == Max
   92	->  Count = Max
   93	;   arg(1, State, Count)
   94	).

answer_count(?Var, :Goal, -Count) is det
answer_count(?Var, :Goal, +Max, -Count) is det: Count number of unique answers of Var Goal produces. Enumeration stops if Max solutions have been found, unifying Count to Max.

  102answer_count(T, G, Count) :-
  103	answer_count(T, G, infinite, Count).
  104
  105answer_count(T, G, Max, Count) :-
  106	empty_nb_set(Set),
  107	C = c(0),
  108	(   G,
  109	    add_nb_set(T, Set, true),
  110	    arg(1, C, C0),
  111	    C1 is C0+1,
  112	    nb_setarg(1, C, C1),
  113	    C1 == Max
  114	->  Count = Max
  115	;   arg(1, C, Count)
  116	).

answer_set(?Var, :Goal, -SortedSet) is det
answer_set(?Var, :Goal, +MaxResults, -SortedSet) is det: SortedSet is the set of bindings for Var for which Goal is true. The predicate answer_set/3 is the same as findall/3 followed by sort/2. The predicate answer_set/4 limits the result to the first MaxResults. Note that this is not the same as the first MaxResults from the entire answer set, which would require computing the entire set.

  128answer_set(T, G, Ts) :-
  129	findall(T, G, Raw),
  130	sort(Raw, Ts).
  131
  132answer_set(T, G, Max, Ts) :-
  133	empty_nb_set(Set),
  134	State = count(0),
  135	(   G,
  136	    add_nb_set(T, Set, true),
  137	    arg(1, State, C0),
  138	    C is C0 + 1,
  139	    nb_setarg(1, State, C),
  140	    C == Max
  141	->  true
  142	;   true
  143	),
  144	nb_set_to_list(Set, Ts).

answer_pair_set(Var, :Goal, +MaxKeys, +MaxPerKey, -Group): Bounded find of Key-Value pairs. MaxKeys bounds the maximum number of keys. MaxPerKey bounds the maximum number of answers per key.

  152answer_pair_set(P, G, MaxKeys, MaxPerKey, Groups) :-
  153        P = K-V,
  154        (   MaxPerKey = inf
  155        ->  true
  156        ;   TooMany is MaxPerKey+1,
  157            dif(New, values(TooMany))
  158        ),
  159        rb_empty(Tree),
  160        State = keys(0),
  161        (   G,
  162            add_pair(Tree, K, V, New),
  163            New == new_key,
  164            arg(1, State, C0),
  165            C is C0+1,
  166            nb_setarg(1, State, C),
  167            C == MaxKeys
  168        ->  true
  169        ;   true
  170        ),
  171        groups(Tree, Groups).
  172
  173add_pair(T, K, V, New) :-
  174        nb_rb_get_node(T, K, N), !,
  175        nb_rb_node_value(N, NV),
  176        NV = k(Count, VT),
  177        (   nb_rb_get_node(VT, V, _)
  178        ->  New = false
  179        ;   NewCount is Count + 1,
  180            New = values(NewCount),
  181            nb_rb_insert(VT, V, true),
  182            nb_setarg(1, NV, NewCount)
  183        ).
  184add_pair(T, K, V, new_key) :-
  185        rb_one(V, true, RB),
  186        nb_rb_insert(T, K, k(1, RB)).
  187
  188rb_one(K, V, Tree) :-
  189        rb_empty(T0),
  190        rb_insert(T0, K, V, Tree).
  191
  192groups(Tree, Groups) :-
  193        rb_visit(Tree, Pairs),
  194        maplist(expand_values, Pairs, Groups).
  195
  196expand_values(K-k(_Count,T), K-Vs) :-
  197        rb_keys(T, Vs).

unique_solution(:Goal, -Solution) is semidet

True if Goal produces exactly one solution for Var. Multiple solutions are compared using =@=/2. This is semantically the same as the code below, but fails early if a second nonequal solution for Var is found.

findall(Var, Goal, Solutions), sort(Solutions, [Solution]).

  210unique_solution(Goal, Solution) :-
  211	State = state(false, _),
  212	(   Goal,
  213	    (	arg(1, State, false)
  214	    ->	nb_setarg(1, State, true),
  215		nb_setarg(2, State, Solution),
  216		fail
  217	    ;	arg(2, State, Answer),
  218		Answer =@= Solution
  219	    ->  fail
  220	    ;	!, fail				% multiple answers
  221	    )
  222	;   arg(1, State, true),
  223	    arg(2, State, Solution)
  224	)