1		:- module(b_to_cnf, [b_to_cnf/3]).
2
3		:- use_module(library(atts)).
4
5		:- use_module(probsrc(bsyntaxtree),[get_texpr_expr/2,create_texpr/4]).
6		:- use_module(probsrc(error_manager), [add_error_fail/3]).
7		:- use_module(probsrc(translate), [translate_bexpression/2]).
8
9		% the sat solver can not just work on prob's own variables,
10		% as it relies on replacing them by integers using unification
11		% this is later undone, however coroutines will be triggered on the way
12		% to avoid side effects, we instead attach a dedicated variables
13		% to each B value variable using an attribute
14		:- attribute corresponding_sat_var/1.
15		get_corresponding_var(BVar,CorrespondingVar) :-
16		get_atts(BVar,+(corresponding_sat_var(CorrespondingVar))), !.
17		get_corresponding_var(BVar,CorrespondingVar) :-
18		put_atts(BVar,+(corresponding_sat_var(CorrespondingVar))).
19
20		verify_attributes(_, Value, []) :-
21		Value == pred_true, !.
22		verify_attributes(_, Value, []) :-
23		Value == pred_false, !.
24		verify_attributes(_, Value, []) :-
25		add_error_fail(b_to_cnf_verify_attributes,'Tried to bind variable with attached SAT variable to non-boolean value', Value).
26
27		b_to_cnf(In,State,Out) :-
28		get_texpr_expr(In,Expr),
29		b_to_cnf_aux(Expr,State,Out), !.
30		b_to_cnf(In,_,_) :-
31		translate_bexpression(In,PPIn), !,
32		add_error_fail(b_to_cnf,'CNF conversion failed', PPIn).
33
34		b_to_cnf_aux(identifier(Name),State,[[Res]]) :-
35		member(bind(Name,Res),State).
36		b_to_cnf_aux(value(X),_,[[1]]) :- X==pred_true.
37		b_to_cnf_aux(value(X),_,[[2]]) :- X==pred_false.
38		b_to_cnf_aux(value(X),_,[[VarForSatSolver]]) :-
39		var(X), get_corresponding_var(X,VarForSatSolver),
40		when(ground(VarForSatSolver),(integer(VarForSatSolver) -> true ; X=VarForSatSolver)).
41
42		b_to_cnf_aux(equal(A,B),State,CNF) :-
43		ground(B),
44		get_texpr_expr(B,value(pred_true)),
45		b_to_cnf(A,State,CNF).
46		b_to_cnf_aux(equal(A,B),State,CNF) :-
47		ground(B),
48		get_texpr_expr(B,value(pred_false)),
49		create_texpr(value(pred_true),boolean,[],True),
50		create_texpr(equal(A,True),pred,[],EqualTrue),
51		b_to_cnf_aux(negation(EqualTrue),State,CNF).
52
53		b_to_cnf_aux(negation(A),State,[[Res]]) :-
54		b_to_cnf(A,State,[[V]]),
55		(var(V) -> Res = neg(V) ;
56		V = neg(X) -> Res = X). % negated literal
57
58		b_to_cnf_aux(implication(A,B),State,CNF) :-
59		create_texpr(negation(A),pred,[],NotA),
60		b_to_cnf_aux(disjunct(NotA,B),State,CNF).
61
62		b_to_cnf_aux(disjunct(D1,D2),State,Res) :-
63		get_texpr_expr(D1,conjunct(A,B)), !,
64		create_texpr(disjunct(A,D2),pred,[],DJ1),
65		create_texpr(disjunct(B,D2),pred,[],DJ2),
66		b_to_cnf_aux(conjunct(DJ1,DJ2),State,Res).
67		b_to_cnf_aux(disjunct(D1,D2),State,Res) :-
68		get_texpr_expr(D2,conjunct(A,B)), !,
69		create_texpr(disjunct(D1,A),pred,[],DJ1),
70		create_texpr(disjunct(D1,B),pred,[],DJ2),
71		b_to_cnf_aux(conjunct(DJ1,DJ2),State,Res).
72
73		b_to_cnf_aux(disjunct(D1,D2),State,[Res]) :-
74		b_to_cnf(D1,State,[ResD1]),
75		b_to_cnf(D2,State,[ResD2]),
76		append(ResD1,ResD2,Res).
77
78		b_to_cnf_aux(conjunct(A,B),State,Res) :-
79		b_to_cnf(A,State,RA),
80		b_to_cnf(B,State,RB),
81		append(RA,RB,Res).