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)). 44 45 46/** <module> This module provides various ways to count solutions 47 48This module is based on a similar collection introduces in the first 49ClioPatria release. Most names have been changed to describe the 50semantics more accurately. 51 52The predicates in this library provide space-efficient solutions, 53avoiding findall/setof. Most predicates come with a variant that allows 54limiting the number of answers. 55 56@tbd The current implementation is often based on library(nb_set), which 57 implements _unbalanced_ binary trees. We should either provide a 58 balanced version or use Paul Tarau's interactors to solve these 59 problems without destructive datastructures. 60*/ 61 62:- meta_predicate 63 proof_count(, ), 64 proof_count(, , ), 65 answer_count(, , ), 66 answer_count(, , , ), 67 answer_set(, , ), 68 answer_set(, , , ), 69 answer_pair_set(, , , , ), 70 unique_solution(, ). 71 72%% proof_count(:Goal, -Count) is det. 73%% proof_count(:Goal, +Max, -Count) is det. 74% 75% True if Count is the number of times Goal succeeds. Note that 76% this is not the same as the number of answers. E.g, repeat/0 has 77% infinite proofs that all have the same -empty- answer 78% substitution. 79% 80% @see answer_count/3 81 82proof_count(Goal, Count) :- 83 proof_count(, infinite, Count). 84 85proof_count(Goal, Max, Count) :- 86 State = count(0), 87 ( , 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 ). 95 96%% answer_count(?Var, :Goal, -Count) is det. 97%% answer_count(?Var, :Goal, +Max, -Count) is det. 98% 99% Count number of unique answers of Var Goal produces. Enumeration 100% stops if Max solutions have been found, unifying Count to Max. 101 102answer_count(T, G, Count) :- 103 answer_count(T, , infinite, Count). 104 105answer_count(T, G, Max, Count) :- 106 empty_nb_set(Set), 107 C = c(0), 108 ( , 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 ). 117 118%% answer_set(?Var, :Goal, -SortedSet) is det. 119%% answer_set(?Var, :Goal, +MaxResults, -SortedSet) is det. 120% 121% SortedSet is the set of bindings for Var for which Goal is true. 122% The predicate answer_set/3 is the same as findall/3 followed by 123% sort/2. The predicate answer_set/4 limits the result to the 124% first MaxResults. Note that this is *not* the same as the first 125% MaxResults from the entire answer set, which would require 126% computing the entire set. 127 128answer_set(T, G, Ts) :- 129 findall(T, , Raw), 130 sort(Raw, Ts). 131 132answer_set(T, G, Max, Ts) :- 133 empty_nb_set(Set), 134 State = count(0), 135 ( , 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). 145 146%% answer_pair_set(Var, :Goal, +MaxKeys, +MaxPerKey, -Group) 147% 148% Bounded find of Key-Value pairs. MaxKeys bounds the maximum 149% number of keys. MaxPerKey bounds the maximum number of answers 150% per key. 151 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 ( , 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). 198 199%% unique_solution(:Goal, -Solution) is semidet. 200% 201% True if Goal produces exactly one solution for Var. Multiple 202% solutions are compared using =@=/2. This is semantically the 203% same as the code below, but fails early if a second nonequal 204% solution for Var is found. 205% 206% == 207% findall(Var, Goal, Solutions), sort(Solutions, [Solution]). 208% == 209 210unique_solution(Goal, Solution) :- 211 State = state(false, _), 212 ( , 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 )