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