1 % (c) 2019-2022 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(cdclt_pred_to_sat, [predicate_to_sat/9,
6 predicate_to_sat/6,
7 sat_to_predicate_from_solution/3,
8 get_amount_of_sat_variables/1,
9 next_sat_var_name/1,
10 reset_sat_var_id/0]).
11
12 :- use_module(library(sets), [subtract/3]).
13 :- use_module(library(avl)).
14 :- use_module(library(lists)).
15 :- use_module(wdsrc(well_def_hyps), [empty_hyps/1,push_hyps/4]).
16 :- use_module(wdsrc(well_def_analyser), [compute_wd/4]).
17 :- use_module(probsrc(debug)).
18 :- use_module(probsrc(translate), [print_bexpr/1]).
19 :- use_module(probsrc(preferences), [get_preference/2]).
20 :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
21 :- use_module(probsrc(module_information), [module_info/2]).
22 :- use_module(probsrc(error_manager),[add_internal_error/2,add_error_fail/3]).
23 :- use_module(probsrc(b_interpreter_check),[norm_pred_check/2]).
24 :- use_module(probsrc(bsyntaxtree), [add_texpr_infos/3,
25 find_identifier_uses/3,
26 safe_create_texpr/4,
27 conjunct_predicates/2,
28 conjunction_to_list/2,
29 disjunct_predicates/2,
30 disjunction_to_list/2]).
31 :- use_module(cdclt_solver('cdclt_preprocessing')).
32 :- use_module(cdclt_solver('cdclt_settings')).
33 :- use_module(extension('banditfuzz/welldef'), [ensure_wd/2]).
34
35 :- module_info(group, cdclt).
36 :- module_info(description, 'This module provides the conversion from B predicates to SAT formulae and vice-versa to be used for CDCL(T).').
37
38 :- dynamic sat_var_id/1.
39
40 sat_var_id(0).
41
42 %% get_amount_of_sat_variables(-AmountOfVars).
43 get_amount_of_sat_variables(AmountOfVars) :-
44 sat_var_id(AmountOfVars).
45
46 %% reset_sat_var_id.
47 reset_sat_var_id :-
48 retractall(sat_var_id(_)),
49 asserta(sat_var_id(0)).
50
51 debug_format_pred(_, _, _) :-
52 print_logs(false),
53 !.
54 debug_format_pred(Msg, Vars, Pred) :-
55 format(Msg, Vars),
56 print_bexpr(Pred), nl, !.
57
58 %% predicate_to_sat(+Type, +Pred, -NewEnv, -WDPOs, -BoolFormula, -NVarAcc).
59 % Same as predicate_to_sat/9 but initializing an empty environment and accumulator for variables.
60 predicate_to_sat(Type, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :-
61 empty_predicate_env(Env),
62 ? predicate_to_sat(Type, [], [], Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc).
63
64 %% predicate_to_sat(+ReuseType, +WDAcc, +Type, +VarAcc, +Env, +Pred, -NewEnv, -BoolFormula, -NVarAcc).
65 % Create a boolean formula from a B predicate, e.g., return 'A=TRUE & B=TRUE' for 'x:INT & x>1'.
66 % Introduces fresh unique identifiers if ReuseType is not equal to 'only_reuse'.
67 % If ReuseType is 'only_reuse': do not introduce new SAT variables but skip parts that need a new SAT variable
68 % (some unsat core computations might deduce new constraints and we do not want to introduce new SAT variables during CDCL).
69 % Env stores pairs of B ASTs (without info field) and its assigned SAT variables.
70 % Add corresponding SAT variable names to AST's info fields (returned in NewPred).
71 % Each SAT variable contains a term smt_formula/1 in its info field providing the corresponding SMT formula.
72 % Note: SMT formula is split on the level of conjunction, disjunction, implication and equivalence.
73 predicate_to_sat(ReuseType, WDAcc, Acc, Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :-
74 Pred = b(Expr, Type, Info),
75 ? predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc).
76
77 %predicate_to_sat_e(E, _, _, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- functor(E,F,N),print(F/N),nl,nl,fail.
78 predicate_to_sat_e(negation(Expr), _, _, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc) :-
79 predicate_to_sat_neg(Expr, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc).
80 predicate_to_sat_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :-
81 !,
82 EnvOut = Env,
83 VarAccOut = Acc,
84 NWDAcc = WDAcc,
85 Truth = b(truth,pred,Info).
86 predicate_to_sat_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :-
87 !,
88 EnvOut = Env,
89 VarAccOut = Acc,
90 NWDAcc = WDAcc,
91 Falsity = b(falsity,pred,Info).
92
93 predicate_to_sat_e(conjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
94 conjunction_to_list(b(conjunct(A,B),pred,[]), PList),
95 !,
96 ? map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc),
97 conjunct_predicates(SatList, BoolFormula).
98 /*predicate_to_sat(_, VarAcc, Env, Pred, NewEnv, BoolFormula, NVarAcc) :-
99 Pred = b(disjunct(_,_),_,_),
100 fetch_predicate(Pred,Env,_,SatVar),
101 % equality from symmetry breaking is a disjunction
102 !,
103 NewEnv = Env,
104 safe_create_texpr(equal(SatVar,b(boolean_true,boolean,[])), pred, [], BoolFormula),
105 NVarAcc = VarAcc.*/
106 predicate_to_sat_e(disjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
107 disjunction_to_list(b(disjunct(A,B),pred,[]), PList),
108 !,
109 ? map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc),
110 disjunct_predicates(SatList, BoolFormula).
111 /*predicate_to_sat(ReuseType, VarAcc, Env, b(negation(Pred),pred,_), NewEnv, NewPred, BoolFormula, NVarAcc) :-
112 predicate_to_sat(ReuseType, VarAcc, Env, Pred, NewEnv, TNewPred, BoolFormula, NVarAcc),
113 ( TNewPred \== b(truth,pred,_)
114 -> safe_create_texpr(negation(TNewPred),pred,[], NewPred)
115 ; safe_create_texpr(truth,pred,[], NewPred)
116 ).*/
117 predicate_to_sat_e(Expr, _, _, _, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, VarAccOut) :-
118 ( Expr == value(pred_true)
119 ; Expr == value(pred_false)
120 ),
121 !,
122 WDPOs = WDAcc,
123 VarAccOut = VarAcc,
124 safe_create_texpr(Expr, pred, [], BoolFormula),
125 NewEnv = Env.
126 predicate_to_sat_e(implication(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
127 !,
128 map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc),
129 NSatArgs = [NSatLhs,NSatRhs],
130 safe_create_texpr(implication(NSatLhs,NSatRhs), pred, [smt_formula(b(implication(Lhs,Rhs),pred,Info))], BoolFormula).
131 predicate_to_sat_e(equivalence(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
132 !,
133 map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc),
134 NSatArgs = [NSatLhs,NSatRhs],
135 safe_create_texpr(equivalence(NSatLhs,NSatRhs), pred, [smt_formula(b(equivalence(Lhs,Rhs),pred,Info))], BoolFormula).
136 predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
137 functor(Expr, _, Arity),
138 ( Arity == 2
139 ; Arity == 3
140 ),
141 !,
142 reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc).
143 predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
144 % formula is a singleton pred which is not splitted such as a subset
145 reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc).
146 % TO DO: if going into quantifications, we have to watch out for local identifier scopes
147 % (i.e., x<7 might not be the same x<7 within a quantification if x is a local id)
148 % Note that we currently do not go into quantifications so this is not an issue.
149
150 predicate_to_sat_neg(Ast, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut) :-
151 Ast = b(Expr,Type,Info),
152 predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut).
153
154 predicate_to_sat_neg_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :-
155 !,
156 EnvOut = Env, VarAccOut = Acc,
157 NWDAcc = WDAcc,
158 Falsity = b(falsity,pred,Info).
159 predicate_to_sat_neg_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :-
160 !,
161 EnvOut = Env, VarAccOut = Acc,
162 NWDAcc = WDAcc,
163 Truth = b(truth,pred,Info).
164 predicate_to_sat_neg_e(negation(Pred), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
165 !,
166 predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, NewEnv, WDPOs, BoolFormula, NVarAcc).
167 predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
168 reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_false, TNewEnv, TWDPOs, TBoolFormula, TNVarAcc),
169 !,
170 NewEnv = TNewEnv,
171 WDPOs = TWDPOs,
172 BoolFormula = TBoolFormula,
173 NVarAcc = TNVarAcc.
174 predicate_to_sat_neg_e(disjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
175 !,
176 predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
177 predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
178 % conjunct_predicate/ ensures that truth and falsity are simplified (1)
179 conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).
180 predicate_to_sat_neg_e(conjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
181 !,
182 predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
183 predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
184 % see above comment (1) for conjunct_predicates/2
185 disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).
186 predicate_to_sat_neg_e(implication(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
187 !,
188 predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, A, NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
189 predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
190 % see (1)
191 conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).
192 predicate_to_sat_neg_e(equivalence(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :-
193 !,
194 predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(b(implication(A,B),pred,[])),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1),
195 predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(b(implication(B,A),pred,[])),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc),
196 % see (1)
197 disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula).
198
199 map_predicate_to_sat(_, WDAcc, VarAcc, Env, [], Env, WDAcc, BoolFormulas, VarAcc) :- !, BoolFormulas=[].
200 map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Pred|T], NewEnv, WDPOs, [BoolFormula|NT], NVarAcc) :-
201 ? predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, TempEnv, TWDAcc, BoolFormula, TVarAcc),
202 ? map_predicate_to_sat(ReuseType, TWDAcc, TVarAcc, TempEnv, T, NewEnv, WDPOs, NT, NVarAcc).
203
204 negate_pred(greater_equal(A,B), less(A,B)).
205 negate_pred(greater(A,B), less_equal(A,B)).
206 negate_pred(less_equal(A,B), less(B,A)).
207 negate_pred(less(A,B), less_equal(B,A)).
208
209 negate_bool_atom(boolean_true, boolean_false).
210 negate_bool_atom(boolean_false, boolean_true).
211
212 % Note: BoolFormula is 'a = TRUE' or 'a = FALSE' for (negated) literal a.
213 /*reuse_or_introduce_bool_var(_, VarAcc, Env, Pred, boolean_true, NewEnv, BoolFormula, NVarAcc) :-
214 % ensure that the same SAT variable is used for boolean equalities such as x=TRUE & x=FALSE
215 % we would usually introduce two different SAT variables for both equalities but don't want to do so for
216 % boolean equalities
217 Pred = b(equal(Bool,BoolId),pred,_),
218 BoolId = b(identifier(BoolIdName),boolean,_),
219 (Bool = b(boolean_true,boolean,[]); Bool = b(boolean_false,boolean,[])),
220 fetch_predicate(b(equal(BoolPred,b(identifier(BoolIdName),boolean,[])),pred,[]),Env,_,SatVar),
221 ( (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_true,boolean,_))
222 -> BoolAtom = boolean_true
223 ; (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_false,boolean,_))
224 -> BoolAtom = boolean_false
225 ; (Bool = b(boolean_false,boolean,_), BoolPred = b(boolean_false,boolean,_))
226 -> BoolAtom = boolean_true
227 ; BoolAtom = boolean_false
228 ),
229 !,
230 safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
231 NewEnv = Env,
232 NVarAcc = VarAcc.*/
233 reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
234 fetch_predicate(Pred, Env, _, SatVar),
235 !,
236 safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
237 NewEnv = Env,
238 NWDAcc = WDAcc,
239 NVarAcc = VarAcc.
240 reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
241 Pred = b(Expr,Type,Info),
242 negate_pred(Expr, NExpr),
243 fetch_predicate(b(NExpr,Type,Info), Env, _, SatVar),
244 !,
245 negate_bool_atom(BoolAtom, NBoolAtom),
246 safe_create_texpr(equal(SatVar,b(NBoolAtom,boolean,[])), pred, [], BoolFormula),
247 NewEnv = Env,
248 NWDAcc = WDAcc,
249 NVarAcc = VarAcc.
250 reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
251 Type == normal,
252 !,
253 next_sat_var_name(SatVarName),
254 debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], Pred),
255 safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId),
256 add_texpr_infos(TUniqueId, [smt_formula(Pred)], UniqueId),
257 register_predicate(Pred,Pred,Env,UniqueId,NewEnv),
258 safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
259 NWDAcc = WDAcc,
260 NVarAcc = [UniqueId|VarAcc].
261 reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :-
262 Type == normal_make_wd,
263 !,
264 next_sat_var_name(SatVarName),
265 ensure_wd(Pred, WDPred),
266 collect_toplevel_wd_preds(WDPred, TopLevelWdPred, WDAcc, NWDAcc),
267 debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], WDPred),
268 safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId),
269 %find_identifier_uses(Pred, [], UsedIds),
270 ( TopLevelWdPred \= b(truth,_,_)
271 -> add_texpr_infos(TUniqueId, [smt_formula(WDPred),contains_top_level_wd_condition(TopLevelWdPred,Pred)], UniqueId)
272 ; add_texpr_infos(TUniqueId, [smt_formula(WDPred)], UniqueId)
273 ),
274 register_predicate(Pred,WDPred,Env,UniqueId,NewEnv),
275 safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula),
276 NVarAcc = [UniqueId|VarAcc].
277 reuse_or_introduce_bool_var(Type, _, _, _, Pred, _, _, _, _, _) :-
278 Type == only_reuse,
279 add_error_fail(reuse_or_introduce_bool_var, 'Missing SAT variable for SMT constraint. b_interpreter_check:norm_pred_check/2 might be inconsistent.', [Pred]).
280
281 collect_toplevel_wd_preds(b(Node,Type,Info), TopLevelWdPred, WDAcc, NWDAcc) :-
282 collect_toplevel_wd_preds_e(Node, Type, Info, TopLevelWdPred, WDAcc, NWDAcc).
283
284 collect_toplevel_wd_preds_e(conjunct(A,B), _, Info, A, WDAcc, NWDAcc) :-
285 member(fuzzed_with_wd_po_included, Info),
286 conjunction_to_list(A, WDPOs),
287 create_wd_impls(WDPOs, B, [], WDImpls),
288 add_wd_impls_to_acc(WDImpls, WDAcc, NWDAcc).
289 collect_toplevel_wd_preds_e(Node, _, _, TopLevelWdPred, WDAcc, NWDAcc) :-
290 Node =.. [_,A,B],
291 collect_toplevel_wd_preds(A, TopLevelWdPred1, WDAcc, NWDAcc1),
292 collect_toplevel_wd_preds(B, TopLevelWdPred2, NWDAcc1, NWDAcc),
293 safe_create_texpr(conjunct(TopLevelWdPred1,TopLevelWdPred2), pred, [], TopLevelWdPred).
294 collect_toplevel_wd_preds_e(_, _, _, b(truth,pred,[]), WDAcc, WDAcc).
295
296 next_sat_var_name(SatVarName) :-
297 retract(sat_var_id(Old)),
298 New is Old + 1,
299 asserta(sat_var_id(New)),
300 number_codes(New, NC),
301 atom_codes(Index, NC),
302 atom_concat('sat', Index, SatVarName).
303
304 % Let A be a predicate with a set of WD conditions C. We create an implication A => c & not(c) => not(A) for each c in C.
305 % We don't use a single implication A => (c1 & c2 & .. & cn) since we have to create a CNF anyway.
306 create_wd_impls([], _, Acc, Acc).
307 create_wd_impls([WDPo|T], Pred, Acc, WDImpls) :-
308 % don't use added info is_wd_po_for_cdclt here
309 NegP = b(negation(Pred),pred,[]),
310 safe_create_texpr(disjunct(NegP,WDPo), pred, [], WDImpl1),
311 safe_create_texpr(disjunct(WDPo,NegP), pred, [], WDImpl2),
312 create_wd_impls(T, Pred, [WDImpl1,WDImpl2|Acc], WDImpls).
313
314 add_wd_impls_to_acc([], WDAcc, WDAcc).
315 add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :-
316 member(WDImpl, WDAcc),
317 !,
318 add_wd_impls_to_acc(T, WDAcc, NWDAcc).
319 add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :-
320 add_wd_impls_to_acc(T, [WDImpl|WDAcc], NWDAcc).
321
322 % managing link from predicates to SAT variables
323
324 empty_predicate_env(E) :- empty_avl(E).
325
326 % TO DO: maybe we should also store SatVarName?
327 register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :-
328 ( var(Env)
329 ; \+ is_avl(Env)
330 ),
331 !,
332 add_internal_error('Illegal env:', register_predicate(Pred,WDPred,Env,UniqueId,NewEnv)),
333 NewEnv = Env.
334 register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- %print('storing: '), writeq(WDPred),nl,
335 norm_pred_check(Pred, NPred),
336 avl_store(NPred,Env,pred2satvar(WDPred,UniqueId),NewEnv).
337
338 fetch_predicate(Pred,Env,StoredPred,SatVar) :- (var(Env) ; \+ is_avl(Env)),!,
339 add_internal_error('Illegal env:',fetch_predicate(Pred,Env,StoredPred,SatVar)), fail.
340 fetch_predicate(Pred,Env,StoredPred,SatVar) :-
341 norm_pred_check(Pred, NPred),
342 avl_fetch(NPred,Env,pred2satvar(StoredPred,SatVar)), !.
343 %fetch_predicate(Pred,_,_,_SatVar) :- print('not found: '), print_bexpr(Pred),nl,fail.
344
345 % ---------------
346
347
348 %% sat_to_predicate_from_solution(+SatBindings, +SatVars, -Conjunction).
349 % Create conjunction of SAT bindings using their corresponding SMT formulae
350 % which are stored in the bool variables' information fields.
351 sat_to_predicate_from_solution([], _, b(truth,pred,[])).
352 sat_to_predicate_from_solution([Binding|T], SatVars, Conjunction) :-
353 get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars),
354 !,
355 sat_to_predicate_from_solution(T, SMT, RestSatVars, Conjunction).
356 sat_to_predicate_from_solution([_|T], SatVars, Conjunction) :-
357 % skip: binding might be a variable if instantiation is not required
358 sat_to_predicate_from_solution(T, SatVars, Conjunction).
359
360 sat_to_predicate_from_solution([], SmtAcc, _, SmtAcc).
361 sat_to_predicate_from_solution([Binding|T], SmtAcc, SatVars, Conjunction) :-
362 get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars),
363 !,
364 safe_create_texpr(conjunct(SMT,SmtAcc), pred, [], NewSmtAcc),
365 sat_to_predicate_from_solution(T, NewSmtAcc, RestSatVars, Conjunction).
366 sat_to_predicate_from_solution([_|T], SmtAcc, SatVars, Conjunction) :-
367 sat_to_predicate_from_solution(T, SmtAcc, SatVars, Conjunction).
368
369 get_var_and_value_from_binding(bind(SatVarName,Value), SatVarName, Value).
370 get_var_and_value_from_binding(binding(SatVarName,Value,_), SatVarName, Value).
371
372 get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars) :-
373 ground(Binding),
374 get_var_and_value_from_binding(Binding, SatVarName, Value),
375 !,
376 select(b(identifier(SatVarName),_,Info), SatVars, RestSatVars),
377 member(smt_formula(TSMT), Info),!,
378 ( Value == pred_true
379 -> SMT = TSMT
380 ; Value == pred_false,
381 TSMT = b(_,_,TSMTInfo),
382 safe_create_texpr(negation(TSMT), pred, TSMTInfo, SMT)
383 ).
384 /*get_smt_formula_from_binding(Binding, _, _, _) :-
385 add_error(get_smt_formula_from_binding, 'SAT binding not ground:', [Binding]),
386 fail.*/