1 % (c) 2012-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(b_to_cnf, [b_to_cnf/3, b_to_cnf_wf/4]).
6
7 :- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2,create_texpr/4, get_integer/2, disjunction_to_list/2,
8 get_texpr_info/2,conjunct_predicates/2]).
9 :- use_module(probsrc(error_manager), [add_error_fail/3, add_error/4, add_error/3,
10 add_message/4, add_message/3]).
11 :- use_module(probsrc(tools_portability), [exists_source/1]).
12 :- use_module(probsrc(translate), [translate_bexpression/2]).
13 :- use_module(library(lists)).
14
15 % the sat solver can not just work on prob's own variables,
16 % as it relies on replacing them by integers using unification
17 % this is later undone, however coroutines will be triggered on the way
18 % to avoid side effects, we instead attach a dedicated variable
19 % to each B value variable using an attribute
20
21 % Portable attributed variable handling.
22 % Use SICStus-style library(atts) and verify_attributes/3 if available,
23 % otherwise the SWI/ECLiPSe-style attr builtins and attr_unify_hook/2.
24 :- if(exists_source(library(atts))).
25
26 :- use_module(library(atts)).
27
28 :- attribute corresponding_sat_var/1.
29 % BVar is a Prolog variable representing a B Boolean/Predicate value
30 % CorrespondingVar is the Prolog variable for the Satsolver
31 get_corresponding_var(BVar,CorrespondingVar) :-
32 get_atts(BVar,+(corresponding_sat_var(CorrespondingVar))), !.
33 get_corresponding_var(BVar,CorrespondingVar) :-
34 put_atts(BVar,+(corresponding_sat_var(CorrespondingVar))).
35
36 verify_attributes(_, Value, Goals) :- var(Value),!, Goals = [].
37 verify_attributes(_, pred_true, Goals) :- !, Goals = [].
38 verify_attributes(_, pred_false, Goals) :- !, Goals = [].
39 verify_attributes(_, Value, []) :-
40 add_error_fail(b_to_cnf_verify_attributes,'Tried to bind variable with attached SAT variable to non-boolean value', Value).
41
42 :- else.
43
44 get_corresponding_var(BVar,CorrespondingVar) :-
45 get_attr(BVar,b_to_cnf,corresponding_sat_var(CorrespondingVar)), !.
46 get_corresponding_var(BVar,CorrespondingVar) :-
47 put_attr(BVar,b_to_cnf,corresponding_sat_var(CorrespondingVar)).
48
49 attr_unify_hook(_, Value) :- var(Value),!.
50 attr_unify_hook(_, pred_true) :- !.
51 attr_unify_hook(_, pred_false) :- !.
52 attr_unify_hook(_, Value) :-
53 add_error_fail(b_to_cnf_attr_unify_hook,'Tried to bind variable with attached SAT variable to non-boolean value', Value).
54
55 :- endif.
56
57 :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
58 :- use_module(probsrc(kernel_waitflags),
59 [copy_wf_start/3,copy_wf_finish/2,
60 ground_det_wait_flag/1]).
61 :- use_module(probsrc(source_profiler),[add_source_location_hits/2]).
62 :- use_module(library(avl),[empty_avl/1]).
63
64 % a version of b_to_cnf which uses WF to call ProB's solver if conversion not possible
65 b_to_cnf_wf(Pred,State,Out,WF) :-
66 empty_avl(Ai),
67 conjunction_to_list(Pred,List),
68 %set_prolog_flag(profiling, on),
69 l_b_to_cnf_wf(List,State,WF,Ai,_,Out,[]). %, set_prolog_flag(profiling, off), print_profile.
70
71 l_b_to_cnf_wf([],_,_WF,A,A) --> [].
72 l_b_to_cnf_wf([Pred|T],State,WF,Ai,Ao) -->
73 b_pred_to_cnf_wf(Pred,State,WF,Ai,A2,sat),!,
74 l_b_to_cnf_wf(T,State,WF,A2,Ao).
75 l_b_to_cnf_wf([Pred|T],State,WF,Ai,Ao) -->
76 b_pred_to_cnf_wf(Pred,State,WF,Ai,A2,prob),
77 l_b_to_cnf_wf2(T,State,WF,A2,Ao).
78
79 l_b_to_cnf_wf2([],_,_WF,A,A) --> [].
80 l_b_to_cnf_wf2([Pred|T],State,WF,Ai,Ao) -->
81 {b_optimize(Pred,State,NewPred,WF)}, % optimize potentially useful as we executed a predicate to the left by ProB
82 b_pred_to_cnf_wf(NewPred,State,WF,Ai,A2,_),
83 l_b_to_cnf_wf2(T,State,WF,A2,Ao).
84
85 b_optimize(Expansion,State,NewTyped,WF) :-
86 %tools:start_ms_timer(T1),
87 b_compiler:b_optimize(Expansion,[],[],State,NewTyped,WF).
88 %tools:stop_ms_timer_with_msg(T1,b_optimize).
89 %translate:print_bexpr_with_limit(Expansion,80),nl.
90
91 b_pred_to_cnf_wf(b(Expr,_,Info),State,_WF,Ai,Ai,sat) -->
92 ? b_to_cnf_aux(Expr,State), % TODO: pass WF so that we can try and reify inner predicates)
93 !,
94 {add_source_location_hits(Info,1)}.
95 %b_pred_to_cnf_wf(TE,State,WF,Ai,Ai,sat) -->
96 % b_optimize(TE,State,NewTE,WF)}, % attempt to compile again
97 % {NewTE=b(Expr,_,_), translate:print_bexpr(NewTE),nl, TE \== NewTE, print(diff),nl},
98 % b_to_cnf_aux(Expr,State),!.
99 b_pred_to_cnf_wf(Pred,State,WF,Ai,Ao,prob) -->
100 {add_message(b_to_cnf,'Cannot convert to CNF, solving with ProB: ',Pred,Pred),
101 get_texpr_info(Pred,Info),add_source_location_hits(Info,0),
102 copy_wf_start(WF,l_b_to_cnf_wf,CWF),
103 b_interpreter:b_test_boolean_expression(Pred,[],State,CWF,Ai,Ao),
104 copy_wf_finish(WF,CWF),
105 ground_det_wait_flag(WF) % ground so that things are pre-computed for next conjunct
106 }.
107
108
109 b_to_cnf(b(Expr,_,Info),State,Out) :-
110 ? b_to_cnf_aux(Expr,State,Res,[]), !,
111 (Res=Out -> true
112 ; add_error(b_to_cnf,'CNF conversion result does not match template:', Res, Info),
113 fail).
114 b_to_cnf(In,_State,_) :- In = b(_,_,Info),
115 add_error(b_to_cnf,'CNF conversion failed', In, Info),
116 fail.
117
118 ?b_to_cnf(b(Expr,_,_Info),State) --> !, b_to_cnf_aux(Expr,State).
119 b_to_cnf(In,_,_,_) :-
120 add_error_fail(b_to_cnf,'Not properly wrapped:', In).
121
122 b_to_cnf_aux(truth,_) --> [].
123 b_to_cnf_aux(falsity,_) --> [[]].
124 b_to_cnf_aux(identifier(Name),State) -->
125 {lookup_id(Name,State,X)},
126 b_to_cnf_val_aux(X,Name).
127 b_to_cnf_aux(value(X),_) --> b_to_cnf_val_aux(X,unknown).
128 ?b_to_cnf_aux(equal(A,B),State) --> b_to_cnf_equal_aux(A,B,State).
129 b_to_cnf_aux(not_equal(A,B),State) --> b_neg_to_cnf_aux(equal(A,B),State,[]).
130 b_to_cnf_aux(less_equal(A,B),State) --> b_to_cnf_less_equal_aux(A,B,State).
131 b_to_cnf_aux(greater_equal(A,B),State) --> b_to_cnf_less_equal_aux(B,A,State).
132 b_to_cnf_aux(less(A,B),State) --> b_to_cnf_less_aux(A,B,State).
133 b_to_cnf_aux(greater(A,B),State) --> b_to_cnf_less_aux(B,A,State).
134 ?b_to_cnf_aux(negation(A),State) --> b_neg_to_cnf(A,State).
135 b_to_cnf_aux(implication(A,B),State) -->
136 {create_texpr(negation(A),pred,[],NotA)},
137 ? b_to_cnf_aux(disjunct(NotA,B),State).
138 b_to_cnf_aux(equivalence(A,B),State) -->
139 ? b_to_cnf_aux(implication(A,B),State),
140 ? b_to_cnf_aux(implication(B,A),State).
141 b_to_cnf_aux(disjunct(D1,D2),State) --> b_to_cnf_disj_aux(D1,D2,State).
142 b_to_cnf_aux(conjunct(A,B),State) -->
143 ? b_to_cnf(A,State),
144 ? b_to_cnf(B,State).
145 b_to_cnf_aux(let_predicate(Ids,Exprs,Body),State) --> {expand_let_predicate(Ids,Exprs,Body,NewBody)},!,
146 b_to_cnf_aux(NewBody,State).
147 b_to_cnf_aux(Quant,State) --> {is_quantifier2(Quant,Span)},
148 {instantiate_quantifier(Quant,[],Expansion,State)},
149 ({get_texpr_expr(Expansion,Q),\+ is_quantifier(Q)} ->
150 % {write('Expanded: '), translate:print_bexpr(Quant),nl},
151 % {write('Expansion: '), translate:print_bexpr(Expansion),nl},
152 {b_optimize(Expansion,State,NewTyped,no_wf_available)}, % maybe we can now pre-compile more
153 %{write('Compiled: '), translate:print_bexpr(NewTyped),nl},
154 ? (b_to_cnf(NewTyped,State) -> []
155 ; {add_translation_failure('Cannot translate body of expanded quantifier: ',NewTyped,Span)}
156 )
157 ; {add_translation_failure('Cannot expand quantifier: ',Expansion,Span)}
158 ).
159
160 expand_let_predicate(Ids,Exprs,Body,exists(Ids,NewBody)) :-
161 generate_let_equality_pred(Ids,Exprs,EqPreds),
162 append(EqPreds,[Body],AllPreds),
163 conjunct_predicates(AllPreds,NewBody).
164
165 generate_let_equality_pred([],[],[]).
166 generate_let_equality_pred([ID|T],[Exp|TE],[EqPred|TR]) :-
167 EqPred = b(equal(ID,Exp),pred,[]), % TO DO: update WD info
168 generate_let_equality_pred(T,TE,TR).
169
170 lookup_id(Name,State,Value) :-
171 (member(bind(Name,Val),State) -> Value=Val
172 ; add_error_fail(b_to_cnf,'Cannot find identifier in state:',Name),fail).
173
174 add_translation_failure(Msg,Arg,Span) :- add_message(b_to_cnf,Msg,Arg,Span),fail.
175 add_translation_failure(Msg,Arg) :- add_message(b_to_cnf,Msg,Arg),fail.
176 %add_translation_failure(Msg,Arg) :- add_error_fail(b_to_cnf,Msg,Arg).
177
178 :- use_module(smt_solvers_interface(quantifier_instantiation),
179 [instantiate_quantifiers/3, instantiate_exists_to_list/5]).
180 :- use_module(probsrc(preferences), [get_preference/2]).
181 instantiate_quantifier(Quant,Info,Expansion,_State) :-
182 %tools:start_ms_timer(T1),
183 % we could pass reference_state(State) option for compiling
184 get_instantiation_options(Options),
185 instantiate_quantifiers(Options, b(Quant,pred,Info), Expansion).
186 %tools:stop_ms_timer_with_msg(T1,instantiate_quantifier).
187
188 instantiate_card_quantifier(TIDs,LHS,Info,Bodies) :-
189 get_instantiation_options(Options),
190 instantiate_exists_to_list(TIDs,LHS,Info,Options,Bodies).
191
192 get_instantiation_options(Options) :-
193 Options = [instantiate_quantifier_limit(QLIM),instantiate_deferred_sets,
194 expansion_time_out(XTO),
195 instantiate_precisely_only],
196 % precise instantiation ensures we can make use of e.g. symmetry breaking constraints during expansion
197 get_preference(solver_strength,SS),
198 QLIM is 15000+SS*100,
199 XTO is 100 + SS.
200
201 is_quantifier(exists(_,_)).
202 is_quantifier(forall(_,_,_)).
203 is_quantifier2(exists(_,b(_,_,Span)),Span).
204 is_quantifier2(forall(_,b(_,_,Span),_),Span).
205
206 ?b_neg_to_cnf(b(Expr,_,Info),State) --> !,b_neg_to_cnf_aux(Expr,State,Info).
207 b_neg_to_cnf(In,_,_,_) :-
208 add_error_fail(b_neg_to_cnf,'Not properly wrapped:', In).
209
210 b_neg_to_cnf_aux(falsity,_,_) --> [].
211 b_neg_to_cnf_aux(truth,_,_) --> [[]].
212 b_neg_to_cnf_aux(disjunct(A,B),State,_) --> !, % not(A or B) --> not(A) & not(B)
213 b_neg_to_cnf(A,State),
214 b_neg_to_cnf(B,State).
215 b_neg_to_cnf_aux(implication(A,B),State,_) --> !, % not(A => B) --> A & not(B)
216 b_to_cnf(A,State),
217 b_neg_to_cnf(B,State).
218 ?b_neg_to_cnf_aux(equal(A,B),State,_) --> b_neg_to_cnf_equal_aux(A,B,State),!. % does not cover all cases
219 b_neg_to_cnf_aux(equivalence(A,B),State,_) --> !, % not(A<=>B) --> A <=> not(B)
220 {negate_pred(B,NotB)},
221 ? b_to_cnf_aux(equivalence(A,NotB),State).
222 b_neg_to_cnf_aux(conjunct(A,B),State,_) --> !, b_neg_to_cnf_conj_aux(A,B,State).
223 b_neg_to_cnf_aux(BOP,State,_) --> {negate_op(BOP,NBOP)}, !,b_to_cnf_aux(NBOP,State).
224 b_neg_to_cnf_aux(let_predicate(Ids,Exprs,Body),State,Info) --> {expand_let_predicate(Ids,Exprs,Body,NewBody)},!,
225 b_neg_to_cnf_aux(NewBody,State,Info).
226 b_neg_to_cnf_aux(Quant,State,Info) --> {is_quantifier(Quant)},!,
227 {instantiate_quantifier(Quant,Info,Expansion,State)},
228 ({get_texpr_expr(Expansion,Q),\+ is_quantifier(Q)} ->
229 {b_optimize(Expansion,State,NewTyped,no_wf_available)}, % maybe we can now pre-compile more
230 b_neg_to_cnf(NewTyped,State)
231 ;{add_error_fail(b_neg_to_cnf,'Cannot expand negated quantifier: ',b(Expansion,pred,[]))}
232 ).
233 b_neg_to_cnf_aux(A,State,_,[[Res]|Acc],Acc) :- % deals with equal
234 ? b_to_cnf_aux(A,State,[[V]],[]), % very limited form of treatment of negation: TODO: improve
235 negate_lit(V,Res).
236
237 negate_pred(B,NotB) :- create_texpr(negation(B),pred,[],NotB).
238
239 % negate a literal:
240 negate_lit(V,Res) :- var(V),!, Res=neg(V).
241 negate_lit(neg(V),Res) :- !, Res=V.
242 negate_lit(1,Res) :- !, Res=2. % true -> false
243 negate_lit(2,Res) :- !, Res=1. % false -> true
244 negate_lit(Lit,_) :- add_translation_failure('Cannot negate literal: ',Lit).
245
246 % negate a binary operator
247 negate_op(not_equal(A,B),equal(A,B)).
248 negate_op(less_equal(A,B),greater(A,B)).
249 negate_op(less(A,B),greater_equal(A,B)).
250 negate_op(greater(A,B),less_equal(A,B)).
251 negate_op(greater_equal(A,B),less(A,B)).
252
253 % convert value(X):
254 b_to_cnf_val_aux(X,_) --> {X==pred_true}, !, backend_truth.
255 b_to_cnf_val_aux(X,_) --> {X==pred_false}, !, backend_falsity.
256 b_to_cnf_val_aux(X,Name) --> {var(X)},!, backend_sat_variable(VarForSatSolver),
257 {get_corresponding_var(X,VarForSatSolver), %print(attaching_b2cnf(X,_Name,VarForSatSolver)),nl,
258 bind_corresponding_var(X,Name,VarForSatSolver)}.
259 %b_to_cnf_val_aux(fd(_,T),Name) -->
260 b_to_cnf_val_aux(X,Name) -->
261 {add_error(b_to_cnf,'Variable has non-ground non-boolean value:',X,Name)},
262 [[1]].
263
264
265 :- block bind_corresponding_var(-,?,-).
266 bind_corresponding_var(X,Name,VarForSatSolver) :- var(VarForSatSolver),
267 %format('Instantiated B variable for ~w: ~w --> SAT: ~w~n',[Name,X,VarForSatSolver]),
268 !,
269 (X=pred_true -> VarForSatSolver=pred_true
270 ; X=pred_false -> VarForSatSolver=pred_false
271 ; add_error(bind_corresponding_var,'Illegal B value: ',Name:X)
272 ).
273 bind_corresponding_var(X,_,VarForSatSolver) :-
274 (integer(VarForSatSolver) -> true % this happens in numbervars when numbering literals; will be backtracked
275 ; X=VarForSatSolver).
276
277 % convert equality:
278 %TODO: simplify arguments like inlining function applications of symbolic closures ...
279 b_to_cnf_equal_aux(A,B,State) -->
280 { get_integer(B,Card), get_card_as_sat_list(A,State,List) -> true
281 ; get_integer(A,Card), get_card_as_sat_list(B,State,List)},
282 !,
283 b_to_cnf_card_equal(Card,List).
284 b_to_cnf_equal_aux(A,B,State) -->
285 {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
286 ; get_boolean_value(A,VAL) -> LHS=B
287 )},
288 !,
289 ({VAL==pred_true}
290 ? -> b_to_cnf(LHS,State)
291 ; {VAL == pred_false} ->
292 {create_texpr(value(pred_true),boolean,[],True)},
293 b_neg_to_cnf_aux(equal(LHS,True),State,[])
294 ; % this must be two boolean variables that are compared
295 ? b_to_cnf_aux(equivalence(A,B),State)
296 ).
297 b_to_cnf_equal_aux(A,B,State) --> {simplify_equality(A,B,SA,SB)},!,
298 b_to_cnf_equal_aux(SA,SB,State).
299 b_to_cnf_equal_aux(A,B,_,_,_) :-
300 %write(eq(A,B)),nl,
301 add_translation_failure('Cannot convert equality to SAT variable: ',b(equal(A,B),pred,[])).
302
303 % simplify equalities like (int(1),pred_true) = (int(1),X) to pred_true=X
304 simplify_equality(b(value(V1),T,I1),b(value(V2),T,I2),TS1,TS2) :-
305 simplify_value_equality(V1,V2,T,Change,S1,S2,NewT),
306 Change==change,
307 !,
308 TS1=b(value(S1),NewT,I1),
309 TS2=b(value(S2),NewT,I2).
310
311 % needs to be improved to detect in-equality if cannot be unified and avoid re-trying the simplification a 2nd time
312 % we could also put this logic into b_compiler
313 simplify_value_equality(V1,V2,T,_,R1,R2,NewT) :- (var(V1);var(V2)),!, R1=V1, R2=V2, NewT=T.
314 simplify_value_equality((A1,B1),(A2,B2),couple(_,TB),change,R1,R2,NewT) :-
315 A1==A2,!,
316 simplify_value_equality(B1,B2,TB,_,R1,R2,NewT).
317 simplify_value_equality((A1,B1),(A2,B2),couple(TA,_),change,R1,R2,NewT) :-
318 B1==B2,!,
319 simplify_value_equality(A1,A2,TA,_,R1,R2,NewT).
320 simplify_value_equality(V1,V2,T,_,V1,V2,T).
321
322 % -----------------
323
324 % translate not_equal
325 b_neg_to_cnf_equal_aux(A,B,State) -->
326 {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
327 ; get_boolean_value(A,VAL) -> LHS=B
328 )},
329 !,
330 ({VAL==pred_true}
331 ? -> b_neg_to_cnf(LHS,State)
332 ; {VAL == pred_false} ->
333 {create_texpr(value(pred_true),boolean,[],True)},
334 ? b_to_cnf_aux(equal(LHS,True),State)
335 ; % this must be two boolean variables that are compared
336 ? b_neg_to_cnf_aux(equivalence(A,B),State,[])
337 ).
338 % does not cover all cases; other cases treated via negate_lit
339 % TODO: provide special cases in a treatment of equivalence?!
340
341 get_boolean_value(b(V,boolean,_),Value) :- getv_aux(V,Value).
342 getv_aux(value(Value),Value).
343 getv_aux(boolean_true,pred_true).
344 getv_aux(boolean_false,pred_false).
345
346 % convert in-equality:
347 b_to_cnf_less_equal_aux(A,B,State) --> % card(A) <= B
348 { get_integer(B,Card), get_card_as_sat_list(A,State,List) },
349 !,
350 b_to_cnf_card_less_equal(Card,List).
351 b_to_cnf_less_equal_aux(A,B,State) --> % A =< card(B)
352 { get_integer(A,Card), get_card_as_sat_list(B,State,List) },
353 !,
354 b_to_cnf_card_greater_equal(Card,List).
355 b_to_cnf_less_equal_aux(A,B,_,_,_) :-
356 add_translation_failure('Cannot convert inequality to SAT variable: ',b(less_equal(A,B),pred,[])).
357
358 % convert strict in-equality:
359 b_to_cnf_less_aux(A,B,State) --> % card(A) < B
360 { get_integer(B,Card), get_card_as_sat_list(A,State,List), C1 is Card-1 },
361 !,
362 b_to_cnf_card_less_equal(C1,List).
363 b_to_cnf_less_aux(A,B,State) --> % A < card(B)
364 { get_integer(A,Card), get_card_as_sat_list(B,State,List), C1 is Card+1 },
365 !,
366 b_to_cnf_card_greater_equal(C1,List).
367 b_to_cnf_less_aux(A,B,_,_,_) :-
368 add_translation_failure('Cannot convert inequality to SAT variable: ',b(less(A,B),pred,[])).
369
370
371 % card(Set)=Nr
372 b_to_cnf_card_equal(0,List) --> !, all_zero(List).
373 b_to_cnf_card_equal(1,List) --> !, % exactly one
374 at_least_one(List),
375 b_to_cnf_card_less_equal(1,List). % at most one
376 b_to_cnf_card_equal(Len,List) --> {length(List,Len)}, !, all_one(List).
377 b_to_cnf_card_equal(Nr,List) --> {length(List,Len), Nr > Len}, !, [[]]. % contradiction
378 b_to_cnf_card_equal(Nr,List) -->
379 b_to_cnf_card_less_equal(Nr,List),
380 b_to_cnf_card_greater_equal(Nr,List),!.
381 b_to_cnf_card_equal(_Card,A) -->
382 {add_translation_failure('Cannot convert card(.) equality to SAT:',A)}.
383
384 % card(Set) <= Nr
385 b_to_cnf_card_less_equal(0,List) --> !, all_zero(List).
386 %b_to_cnf_card_less_equal(1,List) --> !, at_most_one(List). % does not seem to pay off: :sat f:1..n --> BOOL & n=1000 & card({i|i:1..n & f(i)=TRUE})<2 -> 3.8 secs vs 0.046 secs with treatment below
387 b_to_cnf_card_less_equal(Nr,_List) --> {Nr<0},!, [[]]. % contradiction
388 b_to_cnf_card_less_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_leq3(Nr,List,Len).
389 b_to_cnf_leq3(Nr,_List,Len) --> {Nr >= Len}, !, []. % tautology, TODO: register List
390 b_to_cnf_leq3(Nr,List,Len) --> {Nr is Len-1}, !, at_least_one_false(List).
391 b_to_cnf_leq3(Nr,List,_) --> {K is Nr+1}, no_k_true_at_same_time(List,K),!.
392
393 % card(Set) >= Nr
394 b_to_cnf_card_greater_equal(0,_List) --> !, []. % TODO: register variables in List to avoid pending co-routines
395 b_to_cnf_card_greater_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_geq3(Nr,List,Len).
396 b_to_cnf_geq3(Len,List,Len) --> !, all_one(List). % all candidates must be in the set
397 b_to_cnf_geq3(Nr,_List,Len) --> {Nr > Len}, !, [[]]. % contradiction
398 b_to_cnf_geq3(1,List,_) --> !, at_least_one(List).
399 %b_to_cnf_geq3(Nr,List,Len) --> {Nr is Len-1}, !, at_most_one_false(List). % probably also not worth it
400 b_to_cnf_geq3(Nr,List,Len) --> {K is 1+Len-Nr}, no_k_false_at_same_time(List,K),!.
401
402
403 % ----------------
404
405
406
407 % convert disjunct:
408 b_to_cnf_disj_aux(D1,D2,State) -->
409 {get_texpr_expr(D1,conjunct(A,B))}, !,
410 {create_texpr(disjunct(A,D2),pred,[],DJ1),
411 create_texpr(disjunct(B,D2),pred,[],DJ2)},
412 b_to_cnf_aux(conjunct(DJ1,DJ2),State).
413 b_to_cnf_disj_aux(D1,D2,State) -->
414 {get_texpr_expr(D2,conjunct(A,B))}, !,
415 {create_texpr(disjunct(D1,A),pred,[],DJ1),
416 create_texpr(disjunct(D1,B),pred,[],DJ2)},
417 b_to_cnf_aux(conjunct(DJ1,DJ2),State).
418 b_to_cnf_disj_aux(D1,D2,State,Res,Acc) :-
419 b_to_cnf(D1,State,Res1),
420 !,
421 ( Res1 = [] -> Res=Acc % no clauses added
422 ; b_to_cnf(D2,State,Res2),
423 !,
424 ( Res1 = [[]] -> append(Res2,Acc,Res)
425 ; Res2 = [] -> Res = Acc % no clauses added
426 ; Res2 = [[]] -> append(Res1,Acc,Res)
427 ; Res1=[ResD1], Res2=[ResD2] -> Res = [Res12|Acc], append(ResD1,ResD2,Res12)
428 ? ; join_clauses(Res1,Res2,Res,Acc) -> true
429 ; add_error_fail(b_to_cnf_disj,'Cannot join clauses: ',Res1:Res2)
430 )
431 ).
432
433 join_clauses([],_) --> [].
434 ?join_clauses([Clause1|T],Clauses2) --> join_clauses2(Clause1,Clauses2), join_clauses(T,Clauses2).
435
436 join_clauses2(_,[]) --> [].
437 ?join_clauses2(Clause1,[Clause2|T]) --> {append(Clause1,Clause2,NewClause)}, [NewClause], join_clauses2(Clause1,T).
438
439
440 % convert negated conjunct
441 % not(D1&D2) <-> not(D1) or not(D2)
442 b_neg_to_cnf_conj_aux(D1,D2,State) -->
443 {negate_pred(D1,NegD1)},
444 {negate_pred(D2,NegD2)},
445 b_to_cnf_disj_aux(NegD1,NegD2,State).
446
447
448 % -------------------------------
449
450 % Set Cardinality Encodings
451
452
453 get_card_as_sat_list(b(card(Set),integer,_),State,List) :- expand_set_to_sat_variable_list(Set,State,List).
454
455 % expand a set/comprehension set into a list of Sat Variables: one for each candidate member of the set
456 expand_set_to_sat_variable_list(b(comprehension_set(Paras,Body),_,Info),State,SatVarList) :-
457 % write('CARD FOR: '),translate:print_bexpr(Body),nl,
458 instantiate_card_quantifier(Paras,Body, Info, ListOfCandidates),
459 %we have to ensure that disjunct in expansion corresponds really to one possible distinct candidate!
460 % :sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1)) & card({i|i:1..3 & (f(i)=TRUE or i=1)})=3
461 ? (maplist(b_disj_create_one_sat_var(State),ListOfCandidates,CNFList)
462 -> SatVarList=CNFList % ,write(list(CNFList)),nl
463 ; add_error(b_to_cnf,'Cannot convert comprehension set body to single clause:',Body,Info),fail
464 ).
465
466
467 b_disj_create_one_sat_var(State,Disjunct,OneSatVar) :-
468 WF = no_wf_available,
469 b_optimize(Disjunct,State,NewDisj,WF),
470 % write('disj: '),translate:print_bexpr(NewDisj),nl,
471 ? b_to_cnf(NewDisj,State,CNFList,[]),
472 (CNFList = [[]] -> OneSatVar=2 % candidate for certain in the set
473 ; CNFList=[[OneSatVar]] -> true % the sat var corresponds to one candidate in the set
474 ; CNFList = [] -> OneSatVar=1 % one candidate for certain not in the set
475 ; add_error_fail(b_to_cnf,'Cannot reify disjunct to one sat variable:',Disjunct)
476 ).
477
478 % cardinality constraints generated for list of candidate members
479
480 % card(List) >= 1
481 at_least_one(List) --> [List]. % disjunction of literals; at least one must be true
482
483 % card(List) < k where k is list of candidates
484 at_least_one_false(List) --> {maplist(negate_lit,List,NList)}, at_least_one(NList).
485
486 % card(List) <= 1
487 % quadratic version of at most one literal; TODO: linear encoding
488 % Note: findall does not work because the CNF contains variables !
489 %at_most_one([]) --> [].
490 %at_most_one([Lit1|Rest]) --> {negate_lit(Lit1,NLit1)}, at_most1(NLit1,Rest), at_most_one(Rest).
491
492 %at_most1(_,[]) --> [].
493 %at_most1(NLit1,[Lit2|T]) --> {negate_lit(Lit2,NLit2)}, [[NLit1,NLit2]], at_most1(NLit1,T).
494
495 % encoding of empty set:
496 all_zero([]) --> [].
497 all_zero([Lit1|T]) --> {negate_lit(Lit1,NLit1)}, [[NLit1]], all_zero(T).
498
499 % encoding of full set:
500 all_one([]) --> [].
501 all_one([Lit1|T]) --> [[Lit1]], all_one(T).
502
503
504
505 % use with K=1+length(List)-N for card(List) >= N
506 no_k_false_at_same_time(List,K) -->
507 {maplist(negate_lit,List,NList)},
508 no_k_true_at_same_time(NList,K).
509
510 no_k_true_at_same_time(List,K) -->
511 encode_k_true_at_same_time(List,[],K,LastRow),
512 % LastRow contains Sat variables which indicate whether a given cardinality was reached in the entire list
513 {last(LastRow,LastSatVar)},
514 [[neg(LastSatVar)]]. % this stipulates that cardinality K was not reached
515
516 % use with K=N+1 for card(List) <= N
517 % Sequential counter encoding
518 % we return the FinalRow, by setting the last variable of this row to false we force card(List)<K
519 % we can also use it to minimize, by setting earlier variables to false
520 encode_k_true_at_same_time([],LastRow,_,LastRow) --> [].
521 encode_k_true_at_same_time([X1|T],LastRow,K,FinalRow) -->
522 gen_new_row(LastRow,0,NewRow,X1,1,K),
523 encode_k_true_at_same_time(T,NewRow,K,FinalRow).
524
525 gen_new_row([],PrevSatVar,NewRow,Xi,Nr,K) --> {Nr =< K},!,
526 {NewRow = [NewSatVar]}, % this row has one more sat variable than before
527 gen_impl_clause(Xi,PrevSatVar,NewSatVar).
528 gen_new_row([],_,[],_,_,_) --> [].
529 gen_new_row([SatVar|LastRowT],PrevSatVar,[NewSatVar|NewRowT],Xi,Nr,K) -->
530 % NewSatVar: we have reached at least Nr 1s up to current row
531 {negate_lit(SatVar,NegSatVar)},
532 [[NegSatVar,NewSatVar]], % if we have reached Nr Elements in previous row then NewSatVar is also true
533 gen_impl_clause(Xi,PrevSatVar,NewSatVar),
534 {N1 is Nr + 1},
535 gen_new_row(LastRowT,SatVar,NewRowT,Xi,N1,K).
536
537 % generate implication clause
538 gen_impl_clause(Xi,PrevSatVar,NewSatVar) --> {PrevSatVar==0},!, {negate_lit(Xi,NXi)},
539 [[NXi,NewSatVar]].
540 gen_impl_clause(Xi,PrevSatVar,NewSatVar) -->
541 {negate_lit(Xi,NXi),negate_lit(PrevSatVar,NP)},
542 [[NXi,NP,NewSatVar]]. % if Xi is true and we have reached k-1 in last row we reach k now
543
544 %% ------------------------
545
546 % backend specific stuff
547
548 backend_truth --> [[1]]. % literal 1 stands for truth
549 backend_falsity --> [[2]]. % literal 2 stands for false
550 backend_sat_variable(VarForSatSolver) --> [[VarForSatSolver]].
551