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 |