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,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 :- block bind_corresponding_var(?,-).
264 bind_corresponding_var(X,VarForSatSolver) :-
265 (integer(VarForSatSolver) -> true ; X=VarForSatSolver).
266
267 % convert equality:
268 %TODO: simplify arguments like inlining function applications of symbolic closures ...
269 b_to_cnf_equal_aux(A,B,State) -->
270 { get_integer(B,Card), get_card_as_sat_list(A,State,List) -> true
271 ; get_integer(A,Card), get_card_as_sat_list(B,State,List)},
272 !,
273 b_to_cnf_card_equal(Card,List).
274 b_to_cnf_equal_aux(A,B,State) -->
275 {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
276 ; get_boolean_value(A,VAL) -> LHS=B
277 )},
278 !,
279 ({VAL==pred_true}
280 -> b_to_cnf(LHS,State)
281 ; {VAL == pred_false} ->
282 {create_texpr(value(pred_true),boolean,[],True)},
283 b_neg_to_cnf_aux(equal(LHS,True),State,[])
284 ; % this must be two boolean variables that are compared
285 b_to_cnf_aux(equivalence(A,B),State)
286 ).
287 b_to_cnf_equal_aux(A,B,State) --> {simplify_equality(A,B,SA,SB)},!,
288 b_to_cnf_equal_aux(SA,SB,State).
289 b_to_cnf_equal_aux(A,B,_,_,_) :-
290 %write(eq(A,B)),nl,
291 add_translation_failure('Cannot convert equality to SAT variable: ',b(equal(A,B),pred,[])).
292
293 % simplify equalities like (int(1),pred_true) = (int(1),X) to pred_true=X
294 simplify_equality(b(value(V1),T,I1),b(value(V2),T,I2),TS1,TS2) :-
295 simplify_value_equality(V1,V2,T,Change,S1,S2,NewT),
296 Change==change,
297 !,
298 TS1=b(value(S1),NewT,I1),
299 TS2=b(value(S2),NewT,I2).
300
301 % needs to be improved to detect in-equality if cannot be unified and avoid re-trying the simplification a 2nd time
302 % we could also put this logic into b_compiler
303 simplify_value_equality(V1,V2,T,_,R1,R2,NewT) :- (var(V1);var(V2)),!, R1=V1, R2=V2, NewT=T.
304 simplify_value_equality((A1,B1),(A2,B2),couple(_,TB),change,R1,R2,NewT) :-
305 A1==A2,!,
306 simplify_value_equality(B1,B2,TB,_,R1,R2,NewT).
307 simplify_value_equality((A1,B1),(A2,B2),couple(TA,_),change,R1,R2,NewT) :-
308 B1==B2,!,
309 simplify_value_equality(A1,A2,TA,_,R1,R2,NewT).
310 simplify_value_equality(V1,V2,T,_,V1,V2,T).
311
312 % -----------------
313
314 % translate not_equal
315 b_neg_to_cnf_equal_aux(A,B,State) -->
316 {( get_boolean_value(B,VAL), nonvar(VAL) -> LHS=A
317 ; get_boolean_value(A,VAL) -> LHS=B
318 )},
319 !,
320 ({VAL==pred_true}
321 -> b_neg_to_cnf(LHS,State)
322 ; {VAL == pred_false} ->
323 {create_texpr(value(pred_true),boolean,[],True)},
324 b_to_cnf_aux(equal(LHS,True),State)
325 ; % this must be two boolean variables that are compared
326 b_neg_to_cnf_aux(equivalence(A,B),State,[])
327 ).
328 % does not cover all cases; other cases treated via negate_lit
329 % TODO: provide special cases in a treatment of equivalence?!
330
331 get_boolean_value(b(V,boolean,_),Value) :- getv_aux(V,Value).
332 getv_aux(value(Value),Value).
333 getv_aux(boolean_true,pred_true).
334 getv_aux(boolean_false,pred_fakse).
335
336 % convert in-equality:
337 b_to_cnf_less_equal_aux(A,B,State) --> % card(A) <= B
338 { get_integer(B,Card), get_card_as_sat_list(A,State,List) },
339 !,
340 b_to_cnf_card_less_equal(Card,List).
341 b_to_cnf_less_equal_aux(A,B,State) --> % A =< card(B)
342 { get_integer(A,Card), get_card_as_sat_list(B,State,List) },
343 !,
344 b_to_cnf_card_greater_equal(Card,List).
345 b_to_cnf_less_equal_aux(A,B,_,_,_) :-
346 add_translation_failure('Cannot convert inequality to SAT variable: ',b(less_equal(A,B),pred,[])).
347
348 % convert strict in-equality:
349 b_to_cnf_less_aux(A,B,State) --> % card(A) < B
350 { get_integer(B,Card), get_card_as_sat_list(A,State,List), C1 is Card-1 },
351 !,
352 b_to_cnf_card_less_equal(C1,List).
353 b_to_cnf_less_aux(A,B,State) --> % A < card(B)
354 { get_integer(A,Card), get_card_as_sat_list(B,State,List), C1 is Card+1 },
355 !,
356 b_to_cnf_card_greater_equal(C1,List).
357 b_to_cnf_less_aux(A,B,_,_,_) :-
358 add_translation_failure('Cannot convert inequality to SAT variable: ',b(less(A,B),pred,[])).
359
360
361 % card(Set)=Nr
362 b_to_cnf_card_equal(0,List) --> !, all_zero(List).
363 b_to_cnf_card_equal(1,List) --> !, % exactly one
364 at_least_one(List),
365 b_to_cnf_card_less_equal(1,List). % at most one
366 b_to_cnf_card_equal(Len,List) --> {length(List,Len)}, !, all_one(List).
367 b_to_cnf_card_equal(Nr,List) --> {length(List,Len), Nr > Len}, !, [[]]. % contradiction
368 b_to_cnf_card_equal(Nr,List) -->
369 b_to_cnf_card_less_equal(Nr,List),
370 b_to_cnf_card_greater_equal(Nr,List),!.
371 b_to_cnf_card_equal(_Card,A) -->
372 {add_translation_failure('Cannot convert card(.) equality to SAT:',A)}.
373
374 % card(Set) <= Nr
375 b_to_cnf_card_less_equal(0,List) --> !, all_zero(List).
376 %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
377 b_to_cnf_card_less_equal(Nr,_List) --> {Nr<0},!, [[]]. % contradiction
378 b_to_cnf_card_less_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_leq3(Nr,List,Len).
379 b_to_cnf_leq3(Nr,_List,Len) --> {Nr >= Len}, !, []. % tautology, TODO: register List
380 b_to_cnf_leq3(Nr,List,Len) --> {Nr is Len-1}, !, at_least_one_false(List).
381 b_to_cnf_leq3(Nr,List,_) --> {K is Nr+1}, no_k_true_at_same_time(List,K),!.
382
383 % card(Set) >= Nr
384 b_to_cnf_card_greater_equal(0,_List) --> !, []. % TODO: register variables in List to avoid pending co-routines
385 b_to_cnf_card_greater_equal(Nr,List) --> {length(List,Len)}, b_to_cnf_geq3(Nr,List,Len).
386 b_to_cnf_geq3(Len,List,Len) --> !, all_one(List). % all candidates must be in the set
387 b_to_cnf_geq3(Nr,_List,Len) --> {Nr > Len}, !, [[]]. % contradiction
388 b_to_cnf_geq3(1,List,_) --> !, at_least_one(List).
389 %b_to_cnf_geq3(Nr,List,Len) --> {Nr is Len-1}, !, at_most_one_false(List). % probably also not worth it
390 b_to_cnf_geq3(Nr,List,Len) --> {K is 1+Len-Nr}, no_k_false_at_same_time(List,K),!.
391
392
393 % ----------------
394
395
396
397 % convert disjunct:
398 b_to_cnf_disj_aux(D1,D2,State) -->
399 {get_texpr_expr(D1,conjunct(A,B))}, !,
400 {create_texpr(disjunct(A,D2),pred,[],DJ1),
401 create_texpr(disjunct(B,D2),pred,[],DJ2)},
402 b_to_cnf_aux(conjunct(DJ1,DJ2),State).
403 b_to_cnf_disj_aux(D1,D2,State) -->
404 {get_texpr_expr(D2,conjunct(A,B))}, !,
405 {create_texpr(disjunct(D1,A),pred,[],DJ1),
406 create_texpr(disjunct(D1,B),pred,[],DJ2)},
407 b_to_cnf_aux(conjunct(DJ1,DJ2),State).
408 b_to_cnf_disj_aux(D1,D2,State,Res,Acc) :-
409 b_to_cnf(D1,State,Res1),
410 !,
411 ( Res1 = [] -> Res=Acc % no clauses added
412 ; b_to_cnf(D2,State,Res2),
413 !,
414 ( Res1 = [[]] -> append(Res2,Acc,Res)
415 ; Res2 = [] -> Res = Acc % no clauses added
416 ; Res2 = [[]] -> append(Res1,Acc,Res)
417 ; Res1=[ResD1], Res2=[ResD2] -> Res = [Res12|Acc], append(ResD1,ResD2,Res12)
418 ; join_clauses(Res1,Res2,Res,Acc) -> true
419 ; add_error_fail(b_to_cnf_disj,'Cannot join clauses: ',Res1:Res2)
420 )
421 ).
422
423 join_clauses([],_) --> [].
424 join_clauses([Clause1|T],Clauses2) --> join_clauses2(Clause1,Clauses2), join_clauses(T,Clauses2).
425
426 join_clauses2(_,[]) --> [].
427 join_clauses2(Clause1,[Clause2|T]) --> {append(Clause1,Clause2,NewClause)}, [NewClause], join_clauses2(Clause1,T).
428
429
430 % convert negated conjunct
431 % not(D1&D2) <-> not(D1) or not(D2)
432 b_neg_to_cnf_conj_aux(D1,D2,State) -->
433 {negate_pred(D1,NegD1)},
434 {negate_pred(D2,NegD2)},
435 b_to_cnf_disj_aux(NegD1,NegD2,State).
436
437
438 % -------------------------------
439
440 % Set Cardinality Encodings
441
442
443 get_card_as_sat_list(b(card(Set),integer,_),State,List) :- expand_set_to_sat_variable_list(Set,State,List).
444
445 % expand a set/comprehension set into a list of Sat Variables: one for each candidate member of the set
446 expand_set_to_sat_variable_list(b(comprehension_set(Paras,Body),_,Info),State,SatVarList) :-
447 % write('CARD FOR: '),translate:print_bexpr(Body),nl,
448 instantiate_card_quantifier(Paras,Body, Info, ListOfCandidates),
449 %we have to ensure that disjunct in expansion corresponds really to one possible distinct candidate!
450 % :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
451 (maplist(b_disj_create_one_sat_var(State),ListOfCandidates,CNFList)
452 -> SatVarList=CNFList % ,write(list(CNFList)),nl
453 ; add_error(b_to_cnf,'Cannot convert comprehension set body to single clause:',Body,Info),fail
454 ).
455
456
457 b_disj_create_one_sat_var(State,Disjunct,OneSatVar) :-
458 WF = no_wf_available,
459 b_optimize(Disjunct,State,NewDisj,WF),
460 % write('disj: '),translate:print_bexpr(NewDisj),nl,
461 b_to_cnf(NewDisj,State,CNFList,[]),
462 (CNFList = [[]] -> OneSatVar=2 % candidate for certain in the set
463 ; CNFList=[[OneSatVar]] -> true % the sat var corresponds to one candidate in the set
464 ; CNFList = [] -> OneSatVar=1 % one candidate for certain not in the set
465 ; add_error_fail(b_to_cnf,'Cannot reify disjunct to one sat variable:',Disjunct)
466 ).
467
468 % cardinality constraints generated for list of candidate members
469
470 % card(List) >= 1
471 at_least_one(List) --> [List]. % disjunction of literals; at least one must be true
472
473 % card(List) < k where k is list of candidates
474 at_least_one_false(List) --> {maplist(negate_lit,List,NList)}, at_least_one(NList).
475
476 % card(List) <= 1
477 % quadratic version of at most one literal; TODO: linear encoding
478 % Note: findall does not work because the CNF contains variables !
479 %at_most_one([]) --> [].
480 %at_most_one([Lit1|Rest]) --> {negate_lit(Lit1,NLit1)}, at_most1(NLit1,Rest), at_most_one(Rest).
481
482 %at_most1(_,[]) --> [].
483 %at_most1(NLit1,[Lit2|T]) --> {negate_lit(Lit2,NLit2)}, [[NLit1,NLit2]], at_most1(NLit1,T).
484
485 % encoding of empty set:
486 all_zero([]) --> [].
487 all_zero([Lit1|T]) --> {negate_lit(Lit1,NLit1)}, [[NLit1]], all_zero(T).
488
489 % encoding of full set:
490 all_one([]) --> [].
491 all_one([Lit1|T]) --> [[Lit1]], all_one(T).
492
493
494
495 % use with K=1+length(List)-N for card(List) >= N
496 no_k_false_at_same_time(List,K) -->
497 {maplist(negate_lit,List,NList)},
498 no_k_true_at_same_time(NList,K).
499
500 no_k_true_at_same_time(List,K) -->
501 encode_k_true_at_same_time(List,[],K,LastRow),
502 % LastRow contains Sat variables which indicate whether a given cardinality was reached in the entire list
503 {last(LastRow,LastSatVar)},
504 [[neg(LastSatVar)]]. % this stipulates that cardinality K was not reached
505
506 % use with K=N+1 for card(List) <= N
507 % Sequential counter encoding
508 % we return the FinalRow, by setting the last variable of this row to false we force card(List)<K
509 % we can also use it to minimize, by setting earlier variables to false
510 encode_k_true_at_same_time([],LastRow,_,LastRow) --> [].
511 encode_k_true_at_same_time([X1|T],LastRow,K,FinalRow) -->
512 gen_new_row(LastRow,0,NewRow,X1,1,K),
513 encode_k_true_at_same_time(T,NewRow,K,FinalRow).
514
515 gen_new_row([],PrevSatVar,NewRow,Xi,Nr,K) --> {Nr =< K},!,
516 {NewRow = [NewSatVar]}, % this row has one more sat variable than before
517 gen_impl_clause(Xi,PrevSatVar,NewSatVar).
518 gen_new_row([],_,[],_,_,_) --> [].
519 gen_new_row([SatVar|LastRowT],PrevSatVar,[NewSatVar|NewRowT],Xi,Nr,K) -->
520 % NewSatVar: we have reached at least Nr 1s up to current row
521 {negate_lit(SatVar,NegSatVar)},
522 [[NegSatVar,NewSatVar]], % if we have reached Nr Elements in previous row then NewSatVar is also true
523 gen_impl_clause(Xi,PrevSatVar,NewSatVar),
524 {N1 is Nr + 1},
525 gen_new_row(LastRowT,SatVar,NewRowT,Xi,N1,K).
526
527 % generate implication clause
528 gen_impl_clause(Xi,PrevSatVar,NewSatVar) --> {PrevSatVar==0},!, {negate_lit(Xi,NXi)},
529 [[NXi,NewSatVar]].
530 gen_impl_clause(Xi,PrevSatVar,NewSatVar) -->
531 {negate_lit(Xi,NXi),negate_lit(PrevSatVar,NP)},
532 [[NXi,NP,NewSatVar]]. % if Xi is true and we have reached k-1 in last row we reach k now
533
534 %% ------------------------
535
536 % backend specific stuff
537
538 backend_truth --> [[1]]. % literal 1 stands for truth
539 backend_falsity --> [[2]]. % literal 2 stands for false
540 backend_sat_variable(VarForSatSolver) --> [[VarForSatSolver]].
541