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). |