| 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(dpllt_pred_to_sat, [predicate_to_sat/9, | |
| 6 | predicate_to_sat/6, | |
| 7 | sat_to_predicate_from_solution/3, | |
| 8 | remove_wd_pos_introduced_for_dpllt_keep_toplevel/2, | |
| 9 | get_all_top_level_wd_pos/2, | |
| 10 | get_amount_of_sat_variables/1, | |
| 11 | next_sat_var_name/1, | |
| 12 | reset_sat_var_id/0]). | |
| 13 | ||
| 14 | :- use_module(library(sets), [subtract/3]). | |
| 15 | :- use_module(library(avl)). | |
| 16 | :- use_module(library(lists)). | |
| 17 | :- use_module(wdsrc(well_def_hyps), [empty_hyps/1]). | |
| 18 | :- use_module(wdsrc(well_def_analyser), [compute_wd/4]). | |
| 19 | :- use_module(probsrc(debug)). | |
| 20 | :- use_module(probsrc(translate), [print_bexpr/1]). | |
| 21 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 22 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 23 | :- use_module(probsrc(error_manager),[add_internal_error/2]). | |
| 24 | :- use_module(probsrc(b_interpreter_check),[norm_pred_check/2]). | |
| 25 | :- use_module(probsrc(bsyntaxtree), [add_texpr_infos/3, | |
| 26 | find_identifier_uses/3, | |
| 27 | safe_create_texpr/4, | |
| 28 | conjunct_predicates/2, | |
| 29 | conjunction_to_list/2, | |
| 30 | disjunct_predicates/2, | |
| 31 | disjunction_to_list/2]). | |
| 32 | ||
| 33 | :- module_info(group, dpllt). | |
| 34 | :- module_info(description, 'This module provides the conversion from B predicates to SAT formulae and vice-versa to be used for DPLL(T).'). | |
| 35 | ||
| 36 | :- dynamic sat_var_id/1. | |
| 37 | :- volatile sat_var_id/1. | |
| 38 | ||
| 39 | sat_var_id(0). | |
| 40 | ||
| 41 | %% get_amount_of_sat_variables(-AmountOfVars). | |
| 42 | get_amount_of_sat_variables(AmountOfVars) :- | |
| 43 | sat_var_id(AmountOfVars). | |
| 44 | ||
| 45 | reset_sat_var_id :- | |
| 46 | retractall(sat_var_id(_)), | |
| 47 | asserta(sat_var_id(0)). | |
| 48 | ||
| 49 | debug_format_pred(_, _, _) :- | |
| 50 | debug_mode(off), | |
| 51 | !. | |
| 52 | debug_format_pred(Msg, Vars, Pred) :- | |
| 53 | format(Msg, Vars), | |
| 54 | print_bexpr(Pred), nl, !. | |
| 55 | ||
| 56 | %% predicate_to_sat(+Type, +Pred, -NewEnv, -WDPOs, -BoolFormula, -NVarAcc). | |
| 57 | % Same as predicate_to_sat/7 but initializing an empty environment and accumulator for variables. | |
| 58 | predicate_to_sat(Type, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :- | |
| 59 | empty_predicate_env(Env), | |
| 60 | predicate_to_sat(Type, [], [], Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc). | |
| 61 | ||
| 62 | %% predicate_to_sat(+Type, +VarAcc, +Env, +Pred, -NewEnv, -BoolFormula, -NVarAcc). | |
| 63 | % Create a boolean formula from a B predicate, e.g., return 'A=TRUE & B=TRUE' for 'x:INT & x>1'. | |
| 64 | % Introduces fresh unique identifiers if ReuseType is not equal to 'only_reuse'. | |
| 65 | % If ReuseType is 'only_reuse': do not introduce new SAT variables but skip parts that need a new SAT variable | |
| 66 | % (some unsat core computations might deduce new constraints and we do not want to introduce new SAT variables during CDCL). | |
| 67 | % Env stores pairs of B ASTs (without info field) and its assigned SAT variables. | |
| 68 | % Add corresponding SAT variable names to AST's info fields (returned in NewPred). | |
| 69 | % Each SAT variable contains a term smt_formula/1 in its info field providing the corresponding SMT formula. | |
| 70 | % Note: SMT formula is split on the level of conjunction, disjunction, implication and equivalence. | |
| 71 | predicate_to_sat(ReuseType, WDAcc, Acc, Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :- | |
| 72 | Pred = b(Expr, Type, Info), | |
| 73 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc). | |
| 74 | ||
| 75 | ||
| 76 | predicate_to_sat_e(negation(b(truth,pred,Info)), _, _, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- | |
| 77 | !, | |
| 78 | EnvOut = Env, | |
| 79 | VarAccOut = Acc, | |
| 80 | NWDAcc = WDAcc, | |
| 81 | Falsity = b(falsity,pred,Info). | |
| 82 | predicate_to_sat_e(negation(b(falsity,pred,Info)), _, _, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :- | |
| 83 | !, | |
| 84 | EnvOut = Env, | |
| 85 | VarAccOut = Acc, | |
| 86 | NWDAcc = WDAcc, | |
| 87 | Truth = b(truth,pred,Info). | |
| 88 | predicate_to_sat_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :- | |
| 89 | !, | |
| 90 | EnvOut = Env, | |
| 91 | VarAccOut = Acc, | |
| 92 | NWDAcc = WDAcc, | |
| 93 | Truth = b(truth,pred,Info). | |
| 94 | predicate_to_sat_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- | |
| 95 | !, | |
| 96 | EnvOut = Env, | |
| 97 | VarAccOut = Acc, | |
| 98 | NWDAcc = WDAcc, | |
| 99 | Falsity = b(falsity,pred,Info). | |
| 100 | predicate_to_sat_e(negation(b(negation(Pred),pred,_)), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 101 | !, | |
| 102 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 103 | predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 104 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, Pred, boolean_false, TNewEnv, TWDPOs, TBoolFormula, TNVarAcc), | |
| 105 | !, | |
| 106 | NewEnv = TNewEnv, | |
| 107 | WDPOs = TWDPOs, | |
| 108 | BoolFormula = TBoolFormula, | |
| 109 | NVarAcc = TNVarAcc. | |
| 110 | predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 111 | Pred = b(disjunct(A,B),pred,_), | |
| 112 | !, | |
| 113 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 114 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 115 | % conjunct_predicate/ ensures that truth and falsity are simplified (1) | |
| 116 | conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 117 | predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 118 | Pred = b(conjunct(A,B),pred,_), | |
| 119 | !, | |
| 120 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 121 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 122 | % see above comment (1) for conjunct_predicates/2 | |
| 123 | disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 124 | predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 125 | Pred = b(implication(A,B),pred,_), | |
| 126 | !, | |
| 127 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, A, NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 128 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 129 | % see (1) | |
| 130 | conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 131 | predicate_to_sat_e(negation(Pred), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 132 | Pred = b(equivalence(A,B),pred,_), | |
| 133 | !, | |
| 134 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(b(implication(A,B),pred,[])),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 135 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(b(implication(B,A),pred,[])),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 136 | % see (1) | |
| 137 | disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 138 | predicate_to_sat_e(conjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 139 | conjunction_to_list(b(conjunct(A,B),pred,[]), PList), | |
| 140 | !, | |
| 141 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc), | |
| 142 | conjunct_predicates(SatList, BoolFormula). | |
| 143 | /*predicate_to_sat(_, VarAcc, Env, Pred, NewEnv, BoolFormula, NVarAcc) :- | |
| 144 | Pred = b(disjunct(_,_),_,_), | |
| 145 | fetch_predicate(Pred,Env,_,SatVar), | |
| 146 | % equality from symmetry breaking is a disjunction | |
| 147 | !, | |
| 148 | NewEnv = Env, | |
| 149 | safe_create_texpr(equal(SatVar,b(boolean_true,boolean,[])), pred, [], BoolFormula), | |
| 150 | NVarAcc = VarAcc.*/ | |
| 151 | predicate_to_sat_e(disjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 152 | disjunction_to_list(b(disjunct(A,B),pred,[]), PList), | |
| 153 | !, | |
| 154 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc), | |
| 155 | disjunct_predicates(SatList, BoolFormula). | |
| 156 | /*predicate_to_sat(ReuseType, VarAcc, Env, b(negation(Pred),pred,_), NewEnv, NewPred, BoolFormula, NVarAcc) :- | |
| 157 | predicate_to_sat(ReuseType, VarAcc, Env, Pred, NewEnv, TNewPred, BoolFormula, NVarAcc), | |
| 158 | ( TNewPred \== b(truth,pred,_) | |
| 159 | -> safe_create_texpr(negation(TNewPred),pred,[], NewPred) | |
| 160 | ; safe_create_texpr(truth,pred,[], NewPred) | |
| 161 | ).*/ | |
| 162 | predicate_to_sat_e(Expr, _, _, _, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, VarAccOut) :- | |
| 163 | ( Expr == value(pred_true) | |
| 164 | ; Expr == value(pred_false) | |
| 165 | ), | |
| 166 | !, | |
| 167 | WDPOs = WDAcc, | |
| 168 | VarAccOut = VarAcc, | |
| 169 | safe_create_texpr(Expr, pred, [], BoolFormula), | |
| 170 | NewEnv = Env. | |
| 171 | predicate_to_sat_e(implication(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 172 | !, | |
| 173 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc), | |
| 174 | NSatArgs = [NSatLhs,NSatRhs], | |
| 175 | safe_create_texpr(implication(NSatLhs,NSatRhs), pred, [smt_formula(b(implication(Lhs,Rhs),pred,Info))], BoolFormula). | |
| 176 | predicate_to_sat_e(equivalence(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 177 | !, | |
| 178 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc), | |
| 179 | NSatArgs = [NSatLhs,NSatRhs], | |
| 180 | safe_create_texpr(equivalence(NSatLhs,NSatRhs), pred, [smt_formula(b(equivalence(Lhs,Rhs),pred,Info))], BoolFormula). | |
| 181 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 182 | functor(Expr, _, Arity), | |
| 183 | ( Arity == 2 | |
| 184 | ; Arity == 3 | |
| 185 | ), | |
| 186 | !, | |
| 187 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 188 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 189 | % formula is a singleton pred which is not splitted such as a subset | |
| 190 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 191 | % TO DO: if going into quantifications, we have to watch out for local identifier scopes | |
| 192 | % (i.e., x<7 might not be the same x<7 within a quantification if x is a local id) | |
| 193 | % Note that we currently do not go into quantifications so this is not an issue. | |
| 194 | ||
| 195 | map_predicate_to_sat(_, WDAcc, VarAcc, Env, [], Env, WDAcc, [], VarAcc). | |
| 196 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Pred|T], NewEnv, WDPOs, [BoolFormula|NT], NVarAcc) :- | |
| 197 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, TempEnv, TWDAcc, BoolFormula, TVarAcc), | |
| 198 | map_predicate_to_sat(ReuseType, TWDAcc, TVarAcc, TempEnv, T, NewEnv, WDPOs, NT, NVarAcc). | |
| 199 | ||
| 200 | negate_pred(greater_equal(A,B), less(A,B)). | |
| 201 | negate_pred(greater(A,B), less_equal(A,B)). | |
| 202 | negate_pred(less_equal(A,B), less(B,A)). | |
| 203 | negate_pred(less(A,B), less_equal(B,A)). | |
| 204 | ||
| 205 | negate_bool_atom(boolean_true, boolean_false). | |
| 206 | negate_bool_atom(boolean_false, boolean_true). | |
| 207 | ||
| 208 | % Note: BoolFormula is 'a = TRUE' or 'a = FALSE' for (negated) literal a. | |
| 209 | /*reuse_or_introduce_bool_var(_, VarAcc, Env, Pred, boolean_true, NewEnv, BoolFormula, NVarAcc) :- | |
| 210 | % ensure that the same SAT variable is used for boolean equalities such as x=TRUE & x=FALSE | |
| 211 | % we would usually introduce two different SAT variables for both equalities but don't want to do so for | |
| 212 | % boolean equalities | |
| 213 | Pred = b(equal(Bool,BoolId),pred,_), | |
| 214 | BoolId = b(identifier(BoolIdName),boolean,_), | |
| 215 | (Bool = b(boolean_true,boolean,[]); Bool = b(boolean_false,boolean,[])), | |
| 216 | fetch_predicate(b(equal(BoolPred,b(identifier(BoolIdName),boolean,[])),pred,[]),Env,_,SatVar), | |
| 217 | ( (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_true,boolean,_)) | |
| 218 | -> BoolAtom = boolean_true | |
| 219 | ; (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_false,boolean,_)) | |
| 220 | -> BoolAtom = boolean_false | |
| 221 | ; (Bool = b(boolean_false,boolean,_), BoolPred = b(boolean_false,boolean,_)) | |
| 222 | -> BoolAtom = boolean_true | |
| 223 | ; BoolAtom = boolean_false | |
| 224 | ), | |
| 225 | !, | |
| 226 | safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 227 | NewEnv = Env, | |
| 228 | NVarAcc = VarAcc.*/ | |
| 229 | reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 230 | fetch_predicate(Pred, Env, _, SatVar), | |
| 231 | !, | |
| 232 | safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 233 | NewEnv = Env, | |
| 234 | NWDAcc = WDAcc, | |
| 235 | NVarAcc = VarAcc. | |
| 236 | reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 237 | Pred = b(Expr,Type,Info), | |
| 238 | negate_pred(Expr, NExpr), | |
| 239 | fetch_predicate(b(NExpr,Type,Info), Env, _, SatVar), | |
| 240 | !, | |
| 241 | negate_bool_atom(BoolAtom, NBoolAtom), | |
| 242 | safe_create_texpr(equal(SatVar,b(NBoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 243 | NewEnv = Env, | |
| 244 | NWDAcc = WDAcc, | |
| 245 | NVarAcc = VarAcc. | |
| 246 | reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 247 | Type \== only_reuse, | |
| 248 | !, | |
| 249 | next_sat_var_name(SatVarName), | |
| 250 | add_wd_po_to_pred(Pred, WDAcc, true, NWDAcc, WDPred, TopLevelWdPred), | |
| 251 | debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], WDPred), | |
| 252 | safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId), | |
| 253 | %find_identifier_uses(Pred, [], UsedIds), | |
| 254 | ( ground(TopLevelWdPred) | |
| 255 | -> add_texpr_infos(TUniqueId, [smt_formula(WDPred),contains_top_level_wd_condition(TopLevelWdPred,Pred)], UniqueId) | |
| 256 | ; add_texpr_infos(TUniqueId, [smt_formula(WDPred)], UniqueId) | |
| 257 | ), | |
| 258 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv), | |
| 259 | safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 260 | NVarAcc = [UniqueId|VarAcc]. | |
| 261 | ||
| 262 | next_sat_var_name(SatVarName) :- | |
| 263 | retract(sat_var_id(Old)), | |
| 264 | New is Old + 1, | |
| 265 | asserta(sat_var_id(New)), | |
| 266 | number_codes(New, NC), | |
| 267 | atom_codes(Index, NC), | |
| 268 | atom_concat('sat', Index, SatVarName). | |
| 269 | ||
| 270 | quantified_binary_expr(exists). | |
| 271 | quantified_binary_expr(comprehension_set). | |
| 272 | quantified_binary_expr(event_b_comprehension_set). | |
| 273 | quantified_binary_expr(lambda). | |
| 274 | quantified_binary_expr(general_sum). | |
| 275 | quantified_binary_expr(general_product). | |
| 276 | quantified_binary_expr(quantified_union). | |
| 277 | quantified_binary_expr(quantified_intersection). | |
| 278 | ||
| 279 | is_typing_pred_without_wd(b(member(Id,B),pred,_)) :- | |
| 280 | B \= b(domain(_),_,_), | |
| 281 | B \= b(seq(_),_,_), % seq typing has a wd condition | |
| 282 | Id = b(identifier(_),_,_). | |
| 283 | is_typing_pred_without_wd(b(subset(Id,B),pred,_)) :- | |
| 284 | B \= b(domain(_),_,_), | |
| 285 | B \= b(seq(_),_,_), | |
| 286 | Id = b(identifier(_),_,_). | |
| 287 | is_typing_pred_without_wd(b(subset_strict(Id,B),pred,_)) :- | |
| 288 | B \= b(domain(_),_,_), | |
| 289 | B \= b(seq(_),_,_), | |
| 290 | Id = b(identifier(_),_,_). | |
| 291 | ||
| 292 | clean_up_pred_cut(Pred, Clean) :- | |
| 293 | clean_up_pred(Pred, _, TClean), !, | |
| 294 | Clean = TClean. | |
| 295 | ||
| 296 | get_top_level_wd_po_no_typing(Pred, WDPo) :- | |
| 297 | empty_hyps(Hyps), | |
| 298 | find_identifier_uses(Pred, [], TopLevelIds), | |
| 299 | compute_wd(Pred, Hyps, [discharge_po,skip_finite_po], TWDPo), % choicepoint | |
| 300 | find_identifier_uses(TWDPo, [], WDIds), | |
| 301 | subtract(WDIds, TopLevelIds, QIds), | |
| 302 | QIds == [], % is top-level | |
| 303 | TWDPo = b(_,_,TWDInfo), | |
| 304 | ( member(discharged(true, _), TWDInfo) | |
| 305 | -> debug_format_pred('Removed discharged predicate from WD POs: ', [], TWDPo), | |
| 306 | fail | |
| 307 | ; true | |
| 308 | ), | |
| 309 | % important to use b_ast_cleanup:clean_up_pred/3 for WD POs collected by compute_wd/4 since | |
| 310 | % typing constraints are optimized to 'typeset' nodes, which is undone by the cleanup. | |
| 311 | clean_up_pred_cut(TWDPo, WDPo), | |
| 312 | ( is_typing_pred_without_wd(WDPo) | |
| 313 | -> debug_format_pred('Removed typing predicate from WD POs: ', [], WDPo), | |
| 314 | fail | |
| 315 | ; true | |
| 316 | ). | |
| 317 | ||
| 318 | remove_duplicate_preds(Constraints, NoDups) :- | |
| 319 | remove_duplicate_preds(Constraints, [], [], NoDups). | |
| 320 | ||
| 321 | remove_duplicate_preds([], _, Acc, Acc). | |
| 322 | remove_duplicate_preds([Pred|T], NormAcc, Acc, NoDups) :- | |
| 323 | norm_pred_check(Pred, NPred), | |
| 324 | ( memberchk(NPred, NormAcc) | |
| 325 | -> NAcc = Acc, | |
| 326 | NNormAcc = NormAcc | |
| 327 | ; NAcc = [Pred|Acc], | |
| 328 | NNormAcc = [NPred|NormAcc] | |
| 329 | ), | |
| 330 | remove_duplicate_preds(T, NNormAcc, NAcc, NoDups). | |
| 331 | ||
| 332 | get_all_top_level_wd_pos(Pred, WDPos) :- | |
| 333 | findall(WDPo, get_top_level_wd_po_no_typing(Pred, WDPo), TWDPos), !, | |
| 334 | remove_duplicate_preds(TWDPos, WDPos). | |
| 335 | ||
| 336 | % Let A be a predicate with a set of WD conditions C. We create an implication A => c for each c in C. | |
| 337 | % We don't use a single implication A => (c1 & c2 & .. & cn) since we have to create a CNF anyway. | |
| 338 | create_wd_impls([], _, Acc, Acc). | |
| 339 | create_wd_impls([WDPo|T], Pred, Acc, WDImpls) :- | |
| 340 | % don't use added info is_wd_po_for_dpllt here | |
| 341 | safe_create_texpr(disjunct(b(negation(Pred),pred,[]),WDPo), pred, [], WDImpl), | |
| 342 | create_wd_impls(T, Pred, [WDImpl|Acc], WDImpls). | |
| 343 | ||
| 344 | add_wd_impls_to_acc([], WDAcc, WDAcc). | |
| 345 | add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :- | |
| 346 | member(WDImpl, WDAcc), | |
| 347 | !, | |
| 348 | add_wd_impls_to_acc(T, WDAcc, NWDAcc). | |
| 349 | add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :- | |
| 350 | add_wd_impls_to_acc(T, [WDImpl|WDAcc], NWDAcc). | |
| 351 | ||
| 352 | %% add_wd_po_to_pred(+Pred, +WDAcc, +IsTopLevel, -NWDAcc, -WDPred, -WDPoConj). | |
| 353 | % Add all necessary WD POs to make +Pred well-defined for SMT solving. | |
| 354 | % That means, each predicate that is abstracted to a SAT variable is well-defined. | |
| 355 | % For quantified formulas, WD POs are nested inside a quantifier. | |
| 356 | add_wd_po_to_pred(Pred, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :- | |
| 357 | Pred = b(Expr, Type, Info), | |
| 358 | add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj). | |
| 359 | ||
| 360 | % Stores top-level WD POs, not WD POs of quantified formulas since they will be abstracted as a single SAT variable on the top-level. | |
| 361 | % For instance, we introduce one SAT variable for a universal quantifier. We thus don't want to add the WD POs that are necessary in the quantifier | |
| 362 | % to our top-level WD POs. | |
| 363 | add_wd_po_to_pred_e(Expr, pred, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :- | |
| 364 | functor(Expr, Functor, 2), | |
| 365 | (Functor == conjunct; Functor == disjunct; Functor == implication; Functor == equivalence), | |
| 366 | !, | |
| 367 | arg(1, Expr, A), | |
| 368 | arg(2, Expr, B), | |
| 369 | add_wd_po_to_pred(A, WDAcc, IsTopLevel, NWDAcc1, WDA, WDAConj), | |
| 370 | add_wd_po_to_pred(B, NWDAcc1, IsTopLevel, NWDAcc, WDB, WDBConj), | |
| 371 | functor(NExpr, Functor, 2), | |
| 372 | arg(1, NExpr, WDA), | |
| 373 | arg(2, NExpr, WDB), | |
| 374 | conjunct_predicates([WDAConj,WDBConj], WDPoConj), | |
| 375 | safe_create_texpr(NExpr, pred, Info, WDPred). | |
| 376 | add_wd_po_to_pred_e(if_then_else(Cond,Lhs,Rhs), pred, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :- | |
| 377 | !, | |
| 378 | add_wd_po_to_pred(Cond, WDAcc, IsTopLevel, NWDAcc1, WDCond, WDPoConj1), | |
| 379 | add_wd_po_to_pred(Lhs, NWDAcc1, IsTopLevel, NWDAcc2, WDLhs, WDPoConj2), | |
| 380 | add_wd_po_to_pred(Rhs, NWDAcc2, IsTopLevel, NWDAcc, WDRhs, WDPoConj3), | |
| 381 | safe_create_texpr(if_then_else(WDCond,WDLhs,WDRhs), pred, Info, WDPred), | |
| 382 | conjunct_predicates([WDPoConj1,WDPoConj2,WDPoConj3], WDPoConj). | |
| 383 | add_wd_po_to_pred_e(forall(Ids,Lhs,Rhs), pred, Info, WDAcc, _, NWDAcc, WDPred, _) :- | |
| 384 | !, | |
| 385 | add_wd_po_to_pred(Rhs, WDAcc, false, NWDAcc, WDRhs, _), | |
| 386 | safe_create_texpr(forall(Ids,Lhs,WDRhs), pred, Info, WDPred). | |
| 387 | add_wd_po_to_pred_e(Expr, pred, Info, WDAcc, _, NWDAcc, WDPred, _) :- | |
| 388 | Expr =.. [Functor,Ids,Eqs,Body], | |
| 389 | (Functor == let; Functor == let_predicate), | |
| 390 | !, | |
| 391 | add_wd_po_to_pred(Body, WDAcc, false, NWDAcc, WDBody, _), | |
| 392 | NExpr =.. [Functor,Ids,Eqs,WDBody], | |
| 393 | safe_create_texpr(NExpr, pred, Info, WDPred). | |
| 394 | add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, _, NWDAcc, WDPred, _) :- | |
| 395 | Expr =.. [Functor,Ids,Body], | |
| 396 | quantified_binary_expr(Functor), | |
| 397 | !, | |
| 398 | add_wd_po_to_pred(Body, WDAcc, false, NWDAcc, WDBody, _), | |
| 399 | NExpr =.. [Functor,Ids,WDBody], | |
| 400 | safe_create_texpr(NExpr, Type, Info, WDPred). | |
| 401 | add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, IsTopLevel, NWDAcc, WDPred, WDPoConj) :- | |
| 402 | % e.g., for a = b - {some set comprehension with WD}, we want to add WD POs to the set comprehension but not the equality | |
| 403 | functor(Expr, Functor, 2), | |
| 404 | Functor \== partition, | |
| 405 | Expr =.. [Functor|Args], | |
| 406 | map_add_wd_po_to_pred(Args, WDAcc, false, NWDAcc1, WDArgs, _), | |
| 407 | NExpr =.. [Functor|WDArgs], | |
| 408 | NPred = b(NExpr,Type,Info), | |
| 409 | !, | |
| 410 | ( Type == pred, | |
| 411 | get_all_top_level_wd_pos(NPred, WDPos), | |
| 412 | WDPos \== [], | |
| 413 | create_wd_impls(WDPos, NPred, [], WDImpls), | |
| 414 | conjunct_predicates(WDPos, WDPoConj) % don't use added info is_wd_po_for_dpllt here | |
| 415 | -> debug_format_pred("--------------------------Add WD PO for pred~n", [], NPred), | |
| 416 | ( IsTopLevel == true | |
| 417 | -> add_wd_impls_to_acc(WDImpls, NWDAcc1, NWDAcc) | |
| 418 | ; NWDAcc = NWDAcc1 | |
| 419 | ), | |
| 420 | maplist(map_add_texpr_infos([is_wd_po_for_dpllt]), WDPos, NWDPos), | |
| 421 | conjunct_predicates(NWDPos, WDPo), | |
| 422 | conjunct_predicates([WDPo,NPred], WDPred) | |
| 423 | ; WDPred = NPred, | |
| 424 | NWDAcc = NWDAcc1 | |
| 425 | ). | |
| 426 | add_wd_po_to_pred_e(Expr, Type, Info, WDAcc, _, WDAcc, b(Expr,Type,Info), _). | |
| 427 | ||
| 428 | map_add_wd_po_to_pred([Arg|T], WDAcc, IsTopLevel, NWDAcc, [WDArg|TWDArgs], WDConj) :- | |
| 429 | add_wd_po_to_pred(Arg, WDAcc, IsTopLevel, NWDAcc1, WDArg, WDConjArg), | |
| 430 | map_add_wd_po_to_pred_acc(T, NWDAcc1, IsTopLevel, NWDAcc, WDConjArg, TWDArgs, WDConj). | |
| 431 | ||
| 432 | map_add_wd_po_to_pred_acc([], WDAcc, _, WDAcc, WDConjAcc, [], WDConjAcc). | |
| 433 | map_add_wd_po_to_pred_acc([Arg|T], WDAcc, IsTopLevel, NWDAcc, WDConjAcc, [WDArg|TWDArgs], WDConj) :- | |
| 434 | add_wd_po_to_pred(Arg, WDAcc, IsTopLevel, NWDAcc1, WDArg, WDConjArg), | |
| 435 | ( ground(WDConjArg) | |
| 436 | -> safe_create_texpr(conjunct(WDConjArg,WDConjAcc),pred,[],NWDConjAcc) | |
| 437 | ; NWDConjAcc = WDConjAcc | |
| 438 | ), | |
| 439 | map_add_wd_po_to_pred_acc(T, NWDAcc1, IsTopLevel, NWDAcc, NWDConjAcc, TWDArgs, WDConj). | |
| 440 | % ---------------- | |
| 441 | ||
| 442 | ||
| 443 | quantified_expr(forall(Ids,Lhs,Rhs), forall, Ids, [Lhs,Rhs]). | |
| 444 | quantified_expr(exists(Ids,Body), exists, Ids, [Body]). | |
| 445 | quantified_expr(comprehension_set(Ids,Body), comprehension_set, Ids, [Body]). | |
| 446 | quantified_expr(event_b_comprehension_set(Ids,Body), event_b_comprehension_set, Ids, [Body]). | |
| 447 | quantified_expr(lambda(Ids,Body), lambda, Ids, [Body]). | |
| 448 | quantified_expr(general_sum(Ids,Body), general_sum, Ids, [Body]). | |
| 449 | quantified_expr(general_product(Ids,Body), general_product, Ids, [Body]). | |
| 450 | quantified_expr(quantified_union(Ids,Body), quantified_union, Ids, [Body]). | |
| 451 | quantified_expr(quantified_intersection(Ids,Body), quantified_intersection, Ids, [Body]). | |
| 452 | ||
| 453 | %% remove_wd_pos_introduced_for_dpllt_keep_toplevel(+Conj, -NConj). | |
| 454 | % We possibly add WD POs which have to be removed prior to predicate_to_sat/9 in order to abstract constraints to the same SAT variable. | |
| 455 | remove_wd_pos_introduced_for_dpllt_keep_toplevel(Conj, NConj) :- | |
| 456 | remove_wd_pos_introduced_for_dpllt(false, Conj, NConj). | |
| 457 | ||
| 458 | %% remove_wd_pos_introduced_for_dpllt(+Remove, +Conj, -NConj). | |
| 459 | % Remove WD POs introduced for dpllt if +Remove is true. | |
| 460 | remove_wd_pos_introduced_for_dpllt(Remove, Conj, NConj) :- | |
| 461 | conjunction_to_list(Conj, List), | |
| 462 | remove_wd_pos_introduced_for_dpllt_l(Remove, List, NList), | |
| 463 | conjunct_predicates(NList, NConj). | |
| 464 | ||
| 465 | remove_wd_pos_introduced_for_dpllt_l(_, [], []). | |
| 466 | remove_wd_pos_introduced_for_dpllt_l(Remove, [b(negation(Pred),pred,NInfo)|T], [Out|NT]) :- | |
| 467 | !, | |
| 468 | remove_wd_pos_introduced_for_dpllt(true, Pred, NPred), | |
| 469 | Out = b(negation(NPred),pred,NInfo), | |
| 470 | remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT). | |
| 471 | remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 472 | Pred = b(Expr,Type,Info), | |
| 473 | quantified_expr(Expr, Functor, Ids, Subs), | |
| 474 | !, | |
| 475 | maplist(remove_wd_pos_introduced_for_dpllt(true), Subs, NSubs), | |
| 476 | NExpr =.. [Functor,Ids|NSubs], | |
| 477 | Out = b(NExpr,Type,Info), | |
| 478 | remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT). | |
| 479 | remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], Out) :- | |
| 480 | Pred = b(_,_,Info), | |
| 481 | memberchk(is_wd_po_for_dpllt, Info), | |
| 482 | !, | |
| 483 | ( Remove == true | |
| 484 | -> Out = NT, | |
| 485 | debug_format_pred("-----------------------removed wd po from unsat core: ", [], Pred) | |
| 486 | ; Out = [Pred|NT] | |
| 487 | ), | |
| 488 | remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT). | |
| 489 | remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 490 | Pred = b(Expr,Type,Info), | |
| 491 | functor(Expr, Functor, 2), | |
| 492 | !, | |
| 493 | arg(1, Expr, Arg1), | |
| 494 | arg(2, Expr, Arg2), | |
| 495 | remove_wd_pos_introduced_for_dpllt(Remove, Arg1, NArg1), | |
| 496 | remove_wd_pos_introduced_for_dpllt(Remove, Arg2, NArg2), | |
| 497 | functor(NExpr, Functor, 2), | |
| 498 | arg(1, NExpr, NArg1), | |
| 499 | arg(2, NExpr, NArg2), | |
| 500 | Out = b(NExpr,Type,Info), | |
| 501 | remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT). | |
| 502 | remove_wd_pos_introduced_for_dpllt_l(Remove, [Pred|T], [Pred|NT]) :- | |
| 503 | remove_wd_pos_introduced_for_dpllt_l(Remove, T, NT). | |
| 504 | ||
| 505 | map_add_texpr_infos(ToBeAdded, Ast, NAst) :- | |
| 506 | add_texpr_infos(Ast, ToBeAdded, NAst). | |
| 507 | ||
| 508 | % managing link from predicates to SAT variables | |
| 509 | ||
| 510 | empty_predicate_env(E) :- empty_avl(E). | |
| 511 | ||
| 512 | % TO DO: maybe we should also store SatVarName? | |
| 513 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- (var(Env) ; \+ is_avl(Env)),!, | |
| 514 | add_internal_error('Illegal env:',register_predicate(Pred,WDPred,Env,UniqueId,NewEnv)), | |
| 515 | NewEnv=Env. | |
| 516 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- %print('storing: '), writeq(WDPred),nl, | |
| 517 | norm_pred_check(Pred,NPred), | |
| 518 | avl_store(NPred,Env,pred2satvar(WDPred,UniqueId),NewEnv). | |
| 519 | ||
| 520 | fetch_predicate(Pred,Env,StoredPred,SatVar) :- (var(Env) ; \+ is_avl(Env)),!, | |
| 521 | add_internal_error('Illegal env:',fetch_predicate(Pred,Env,StoredPred,SatVar)), fail. | |
| 522 | fetch_predicate(Pred,Env,StoredPred,SatVar) :- | |
| 523 | norm_pred_check(Pred,NPred), | |
| 524 | avl_fetch(NPred,Env,pred2satvar(StoredPred,SatVar)), !. | |
| 525 | %fetch_predicate(Pred,_,_,_SatVar) :- print('not found: '), print_bexpr(Pred),nl,fail. | |
| 526 | ||
| 527 | % --------------- | |
| 528 | ||
| 529 | ||
| 530 | %% sat_to_predicate_from_solution(+SatBindings, +SatVars, -Conjunction). | |
| 531 | % Create conjunction of SAT bindings using their corresponding SMT formulae | |
| 532 | % which are stored in the bool variables' information fields. | |
| 533 | sat_to_predicate_from_solution([], _, b(truth,pred,[])). | |
| 534 | sat_to_predicate_from_solution([Binding|T], SatVars, Conjunction) :- | |
| 535 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars), | |
| 536 | !, | |
| 537 | sat_to_predicate_from_solution(T, SMT, RestSatVars, Conjunction). | |
| 538 | sat_to_predicate_from_solution([_|T], SatVars, Conjunction) :- | |
| 539 | % skip: binding might be a variable if instantiation is not required | |
| 540 | sat_to_predicate_from_solution(T, SatVars, Conjunction). | |
| 541 | ||
| 542 | sat_to_predicate_from_solution([], SmtAcc, _, SmtAcc). | |
| 543 | sat_to_predicate_from_solution([Binding|T], SmtAcc, SatVars, Conjunction) :- | |
| 544 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars), | |
| 545 | !, | |
| 546 | safe_create_texpr(conjunct(SMT,SmtAcc), pred, [], NewSmtAcc), | |
| 547 | sat_to_predicate_from_solution(T, NewSmtAcc, RestSatVars, Conjunction). | |
| 548 | sat_to_predicate_from_solution([_|T], SmtAcc, SatVars, Conjunction) :- | |
| 549 | sat_to_predicate_from_solution(T, SmtAcc, SatVars, Conjunction). | |
| 550 | ||
| 551 | get_var_and_value_from_binding(bind(SatVarName,Value), SatVarName, Value). | |
| 552 | get_var_and_value_from_binding(binding(SatVarName,Value,_), SatVarName, Value). | |
| 553 | ||
| 554 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars) :- | |
| 555 | ground(Binding), | |
| 556 | get_var_and_value_from_binding(Binding, SatVarName, Value), | |
| 557 | !, | |
| 558 | select(b(identifier(SatVarName),_,Info), SatVars, RestSatVars), | |
| 559 | member(smt_formula(TSMT), Info),!, | |
| 560 | ( Value == pred_true | |
| 561 | -> SMT = TSMT | |
| 562 | ; Value == pred_false, | |
| 563 | TSMT = b(_,_,TSMTInfo), | |
| 564 | safe_create_texpr(negation(TSMT), pred, TSMTInfo, SMT) | |
| 565 | ). | |
| 566 | /*get_smt_formula_from_binding(Binding, _, _, _) :- | |
| 567 | add_error(get_smt_formula_from_binding, 'SAT binding not ground:', [Binding]), | |
| 568 | fail.*/ |