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