/* Part of ClioPatria SeRQL and SPARQL server Author: Jan Wielemaker E-mail: J.Wielemaker@cs.vu.nl WWW: http://www.swi-prolog.org Copyright (C): 2010, University of Amsterdam, VU University Amsterdam This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this library; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA As a special exception, if you link this library with other files, compiled with a Free Software compiler, to produce an executable, this library does not by itself cause the resulting executable to be covered by the GNU General Public License. This exception does not however invalidate any other reasons why the executable file might be covered by the GNU General Public License. */ :- module(count, [ proof_count/2, % :Goal, -Count proof_count/3, % :Goal, +Max, -Count answer_count/3, % ?Var, :Goal, -Count answer_count/4, % ?Var, :Goal, +Max -Count answer_set/3, % ?Var, :Goal, -Answers answer_set/4, % ?Var, :Goal, +Max, -Answers answer_pair_set/5, % ?Pair, :Goal, +MaxKeys, +MaxPerKey, -Answers unique_solution/2 % :Goal, -Solution ]). :- use_module(library(nb_set)). :- use_module(library(rbtrees)). :- 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. @tbd 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. */ :- meta_predicate proof_count(0, -), proof_count(0, +, -), answer_count(?, 0, -), answer_count(?, 0, +, -), answer_set(?, 0, -), answer_set(?, 0, +, -), answer_pair_set(?, 0, +, +, -), 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 answer_count/3 proof_count(Goal, Count) :- proof_count(Goal, infinite, Count). proof_count(Goal, Max, Count) :- State = count(0), ( Goal, arg(1, State, N0), N is N0 + 1, nb_setarg(1, State, N), N == Max -> Count = Max ; arg(1, State, Count) ). %% 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. answer_count(T, G, Count) :- answer_count(T, G, infinite, Count). answer_count(T, G, Max, Count) :- empty_nb_set(Set), C = c(0), ( G, add_nb_set(T, Set, true), arg(1, C, C0), C1 is C0+1, nb_setarg(1, C, C1), C1 == Max -> Count = Max ; arg(1, C, Count) ). %% 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. answer_set(T, G, Ts) :- findall(T, G, Raw), sort(Raw, Ts). answer_set(T, G, Max, Ts) :- empty_nb_set(Set), State = count(0), ( G, add_nb_set(T, Set, true), arg(1, State, C0), C is C0 + 1, nb_setarg(1, State, C), C == Max -> true ; true ), 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. answer_pair_set(P, G, MaxKeys, MaxPerKey, Groups) :- P = K-V, ( MaxPerKey = inf -> true ; TooMany is MaxPerKey+1, dif(New, values(TooMany)) ), rb_empty(Tree), State = keys(0), ( G, add_pair(Tree, K, V, New), New == new_key, arg(1, State, C0), C is C0+1, nb_setarg(1, State, C), C == MaxKeys -> true ; true ), groups(Tree, Groups). add_pair(T, K, V, New) :- nb_rb_get_node(T, K, N), !, nb_rb_node_value(N, NV), NV = k(Count, VT), ( nb_rb_get_node(VT, V, _) -> New = false ; NewCount is Count + 1, New = values(NewCount), nb_rb_insert(VT, V, true), nb_setarg(1, NV, NewCount) ). add_pair(T, K, V, new_key) :- rb_one(V, true, RB), nb_rb_insert(T, K, k(1, RB)). rb_one(K, V, Tree) :- rb_empty(T0), rb_insert(T0, K, V, Tree). groups(Tree, Groups) :- rb_visit(Tree, Pairs), maplist(expand_values, Pairs, Groups). expand_values(K-k(_Count,T), K-Vs) :- 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]). % == unique_solution(Goal, Solution) :- State = state(false, _), ( Goal, ( arg(1, State, false) -> nb_setarg(1, State, true), nb_setarg(2, State, Solution), fail ; arg(2, State, Answer), Answer =@= Solution -> fail ; !, fail % multiple answers ) ; arg(1, State, true), arg(2, State, Solution) ).