| 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 | remove_wd_pos_introduced_for_cdclt_keep_toplevel/2, | |
| 9 | get_all_top_level_wd_pos/2, | |
| 10 | add_wd_pos_to_pred/8, | |
| 11 | get_amount_of_sat_variables/1, | |
| 12 | next_sat_var_name/1, | |
| 13 | reset_sat_var_id/0]). | |
| 14 | ||
| 15 | :- use_module(library(sets), [subtract/3]). | |
| 16 | :- use_module(library(avl)). | |
| 17 | :- use_module(library(lists)). | |
| 18 | :- use_module(wdsrc(well_def_hyps), [empty_hyps/1,push_hyps/4]). | |
| 19 | :- use_module(wdsrc(well_def_analyser), [compute_wd/4]). | |
| 20 | :- use_module(probsrc(debug)). | |
| 21 | :- use_module(probsrc(translate), [print_bexpr/1]). | |
| 22 | :- use_module(probsrc(preferences), [get_preference/2]). | |
| 23 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 24 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 25 | :- use_module(probsrc(error_manager),[add_internal_error/2,add_error_fail/3]). | |
| 26 | :- use_module(probsrc(b_interpreter_check),[norm_pred_check/2]). | |
| 27 | :- use_module(probsrc(bsyntaxtree), [add_texpr_infos/3, | |
| 28 | find_identifier_uses/3, | |
| 29 | safe_create_texpr/4, | |
| 30 | conjunct_predicates/2, | |
| 31 | conjunction_to_list/2, | |
| 32 | disjunct_predicates/2, | |
| 33 | disjunction_to_list/2]). | |
| 34 | :- use_module(cdclt_solver('cdclt_preprocessing')). | |
| 35 | :- use_module(cdclt_solver('cdclt_settings')). | |
| 36 | ||
| 37 | :- module_info(group, cdclt). | |
| 38 | :- module_info(description, 'This module provides the conversion from B predicates to SAT formulae and vice-versa to be used for CDCL(T).'). | |
| 39 | ||
| 40 | :- dynamic sat_var_id/1. | |
| 41 | ||
| 42 | sat_var_id(0). | |
| 43 | ||
| 44 | %% get_amount_of_sat_variables(-AmountOfVars). | |
| 45 | get_amount_of_sat_variables(AmountOfVars) :- | |
| 46 | sat_var_id(AmountOfVars). | |
| 47 | ||
| 48 | %% reset_sat_var_id. | |
| 49 | reset_sat_var_id :- | |
| 50 | retractall(sat_var_id(_)), | |
| 51 | asserta(sat_var_id(0)). | |
| 52 | ||
| 53 | debug_format_pred(_, _, _) :- | |
| 54 | print_logs(false), | |
| 55 | !. | |
| 56 | debug_format_pred(Msg, Vars, Pred) :- | |
| 57 | format(Msg, Vars), | |
| 58 | print_bexpr(Pred), nl, !. | |
| 59 | ||
| 60 | %% predicate_to_sat(+Type, +Pred, -NewEnv, -WDPOs, -BoolFormula, -NVarAcc). | |
| 61 | % Same as predicate_to_sat/9 but initializing an empty environment and accumulator for variables. | |
| 62 | predicate_to_sat(Type, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :- | |
| 63 | empty_predicate_env(Env), | |
| 64 | predicate_to_sat(Type, [], [], Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc). | |
| 65 | ||
| 66 | %% predicate_to_sat(+ReuseType, +WDAcc, +Type, +VarAcc, +Env, +Pred, -NewEnv, -BoolFormula, -NVarAcc). | |
| 67 | % Create a boolean formula from a B predicate, e.g., return 'A=TRUE & B=TRUE' for 'x:INT & x>1'. | |
| 68 | % Introduces fresh unique identifiers if ReuseType is not equal to 'only_reuse'. | |
| 69 | % If ReuseType is 'only_reuse': do not introduce new SAT variables but skip parts that need a new SAT variable | |
| 70 | % (some unsat core computations might deduce new constraints and we do not want to introduce new SAT variables during CDCL). | |
| 71 | % Env stores pairs of B ASTs (without info field) and its assigned SAT variables. | |
| 72 | % Add corresponding SAT variable names to AST's info fields (returned in NewPred). | |
| 73 | % Each SAT variable contains a term smt_formula/1 in its info field providing the corresponding SMT formula. | |
| 74 | % Note: SMT formula is split on the level of conjunction, disjunction, implication and equivalence. | |
| 75 | predicate_to_sat(ReuseType, WDAcc, Acc, Env, Pred, NewEnv, WDPOs, BoolFormula, VarAcc) :- | |
| 76 | Pred = b(Expr, Type, Info), | |
| 77 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc). | |
| 78 | ||
| 79 | %predicate_to_sat_e(E, _, _, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- functor(E,F,N),print(F/N),nl,nl,fail. | |
| 80 | predicate_to_sat_e(negation(Expr), _, _, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc) :- | |
| 81 | predicate_to_sat_neg(Expr, ReuseType, WDAcc, Acc, Env, NewEnv, WDPOs, BoolFormula, VarAcc). | |
| 82 | predicate_to_sat_e(truth, 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(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- | |
| 89 | !, | |
| 90 | EnvOut = Env, | |
| 91 | VarAccOut = Acc, | |
| 92 | NWDAcc = WDAcc, | |
| 93 | Falsity = b(falsity,pred,Info). | |
| 94 | ||
| 95 | predicate_to_sat_e(conjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 96 | conjunction_to_list(b(conjunct(A,B),pred,[]), PList), | |
| 97 | !, | |
| 98 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc), | |
| 99 | conjunct_predicates(SatList, BoolFormula). | |
| 100 | /*predicate_to_sat(_, VarAcc, Env, Pred, NewEnv, BoolFormula, NVarAcc) :- | |
| 101 | Pred = b(disjunct(_,_),_,_), | |
| 102 | fetch_predicate(Pred,Env,_,SatVar), | |
| 103 | % equality from symmetry breaking is a disjunction | |
| 104 | !, | |
| 105 | NewEnv = Env, | |
| 106 | safe_create_texpr(equal(SatVar,b(boolean_true,boolean,[])), pred, [], BoolFormula), | |
| 107 | NVarAcc = VarAcc.*/ | |
| 108 | predicate_to_sat_e(disjunct(A,B), _, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 109 | disjunction_to_list(b(disjunct(A,B),pred,[]), PList), | |
| 110 | !, | |
| 111 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, PList, NewEnv, WDPOs, SatList, NVarAcc), | |
| 112 | disjunct_predicates(SatList, BoolFormula). | |
| 113 | /*predicate_to_sat(ReuseType, VarAcc, Env, b(negation(Pred),pred,_), NewEnv, NewPred, BoolFormula, NVarAcc) :- | |
| 114 | predicate_to_sat(ReuseType, VarAcc, Env, Pred, NewEnv, TNewPred, BoolFormula, NVarAcc), | |
| 115 | ( TNewPred \== b(truth,pred,_) | |
| 116 | -> safe_create_texpr(negation(TNewPred),pred,[], NewPred) | |
| 117 | ; safe_create_texpr(truth,pred,[], NewPred) | |
| 118 | ).*/ | |
| 119 | predicate_to_sat_e(Expr, _, _, _, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, VarAccOut) :- | |
| 120 | ( Expr == value(pred_true) | |
| 121 | ; Expr == value(pred_false) | |
| 122 | ), | |
| 123 | !, | |
| 124 | WDPOs = WDAcc, | |
| 125 | VarAccOut = VarAcc, | |
| 126 | safe_create_texpr(Expr, pred, [], BoolFormula), | |
| 127 | NewEnv = Env. | |
| 128 | predicate_to_sat_e(implication(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 129 | !, | |
| 130 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc), | |
| 131 | NSatArgs = [NSatLhs,NSatRhs], | |
| 132 | safe_create_texpr(implication(NSatLhs,NSatRhs), pred, [smt_formula(b(implication(Lhs,Rhs),pred,Info))], BoolFormula). | |
| 133 | predicate_to_sat_e(equivalence(Lhs,Rhs), pred, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 134 | !, | |
| 135 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Lhs,Rhs], NewEnv, WDPOs, NSatArgs, NVarAcc), | |
| 136 | NSatArgs = [NSatLhs,NSatRhs], | |
| 137 | safe_create_texpr(equivalence(NSatLhs,NSatRhs), pred, [smt_formula(b(equivalence(Lhs,Rhs),pred,Info))], BoolFormula). | |
| 138 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 139 | functor(Expr, _, Arity), | |
| 140 | ( Arity == 2 | |
| 141 | ; Arity == 3 | |
| 142 | ), | |
| 143 | !, | |
| 144 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 145 | predicate_to_sat_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 146 | % formula is a singleton pred which is not splitted such as a subset | |
| 147 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_true, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 148 | % TO DO: if going into quantifications, we have to watch out for local identifier scopes | |
| 149 | % (i.e., x<7 might not be the same x<7 within a quantification if x is a local id) | |
| 150 | % Note that we currently do not go into quantifications so this is not an issue. | |
| 151 | ||
| 152 | predicate_to_sat_neg(Ast, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut) :- | |
| 153 | Ast = b(Expr,Type,Info), | |
| 154 | predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, Acc, Env, EnvOut, NWDAcc, NAst, VarAccOut). | |
| 155 | ||
| 156 | predicate_to_sat_neg_e(truth, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Falsity, VarAccOut) :- | |
| 157 | !, | |
| 158 | EnvOut = Env, VarAccOut = Acc, | |
| 159 | NWDAcc = WDAcc, | |
| 160 | Falsity = b(falsity,pred,Info). | |
| 161 | predicate_to_sat_neg_e(falsity, pred, Info, _, WDAcc, Acc, Env, EnvOut, NWDAcc, Truth, VarAccOut) :- | |
| 162 | !, | |
| 163 | EnvOut = Env, VarAccOut = Acc, | |
| 164 | NWDAcc = WDAcc, | |
| 165 | Truth = b(truth,pred,Info). | |
| 166 | predicate_to_sat_neg_e(negation(Pred), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 167 | !, | |
| 168 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, NewEnv, WDPOs, BoolFormula, NVarAcc). | |
| 169 | predicate_to_sat_neg_e(Expr, Type, Info, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 170 | reuse_or_introduce_bool_var(ReuseType, WDAcc, VarAcc, Env, b(Expr,Type,Info), boolean_false, TNewEnv, TWDPOs, TBoolFormula, TNVarAcc), | |
| 171 | !, | |
| 172 | NewEnv = TNewEnv, | |
| 173 | WDPOs = TWDPOs, | |
| 174 | BoolFormula = TBoolFormula, | |
| 175 | NVarAcc = TNVarAcc. | |
| 176 | predicate_to_sat_neg_e(disjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 177 | !, | |
| 178 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 179 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 180 | % conjunct_predicate/ ensures that truth and falsity are simplified (1) | |
| 181 | conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 182 | predicate_to_sat_neg_e(conjunct(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 183 | !, | |
| 184 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(A),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 185 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 186 | % see above comment (1) for conjunct_predicates/2 | |
| 187 | disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 188 | predicate_to_sat_neg_e(implication(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 189 | !, | |
| 190 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, A, NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 191 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(B),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 192 | % see (1) | |
| 193 | conjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 194 | predicate_to_sat_neg_e(equivalence(A,B), pred, _, ReuseType, WDAcc, VarAcc, Env, NewEnv, WDPOs, BoolFormula, NVarAcc) :- | |
| 195 | !, | |
| 196 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, b(negation(b(implication(A,B),pred,[])),pred,[]), NewEnv1, WDAcc1, ABoolFormula, NVarAcc1), | |
| 197 | predicate_to_sat(ReuseType, WDAcc1, NVarAcc1, NewEnv1, b(negation(b(implication(B,A),pred,[])),pred,[]), NewEnv, WDPOs, BBoolFormula, NVarAcc), | |
| 198 | % see (1) | |
| 199 | disjunct_predicates([ABoolFormula,BBoolFormula], BoolFormula). | |
| 200 | ||
| 201 | map_predicate_to_sat(_, WDAcc, VarAcc, Env, [], Env, WDAcc, BoolFormulas, VarAcc) :- !, BoolFormulas=[]. | |
| 202 | map_predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, [Pred|T], NewEnv, WDPOs, [BoolFormula|NT], NVarAcc) :- | |
| 203 | predicate_to_sat(ReuseType, WDAcc, VarAcc, Env, Pred, TempEnv, TWDAcc, BoolFormula, TVarAcc), | |
| 204 | map_predicate_to_sat(ReuseType, TWDAcc, TVarAcc, TempEnv, T, NewEnv, WDPOs, NT, NVarAcc). | |
| 205 | ||
| 206 | negate_pred(greater_equal(A,B), less(A,B)). | |
| 207 | negate_pred(greater(A,B), less_equal(A,B)). | |
| 208 | negate_pred(less_equal(A,B), less(B,A)). | |
| 209 | negate_pred(less(A,B), less_equal(B,A)). | |
| 210 | ||
| 211 | negate_bool_atom(boolean_true, boolean_false). | |
| 212 | negate_bool_atom(boolean_false, boolean_true). | |
| 213 | ||
| 214 | % Note: BoolFormula is 'a = TRUE' or 'a = FALSE' for (negated) literal a. | |
| 215 | /*reuse_or_introduce_bool_var(_, VarAcc, Env, Pred, boolean_true, NewEnv, BoolFormula, NVarAcc) :- | |
| 216 | % ensure that the same SAT variable is used for boolean equalities such as x=TRUE & x=FALSE | |
| 217 | % we would usually introduce two different SAT variables for both equalities but don't want to do so for | |
| 218 | % boolean equalities | |
| 219 | Pred = b(equal(Bool,BoolId),pred,_), | |
| 220 | BoolId = b(identifier(BoolIdName),boolean,_), | |
| 221 | (Bool = b(boolean_true,boolean,[]); Bool = b(boolean_false,boolean,[])), | |
| 222 | fetch_predicate(b(equal(BoolPred,b(identifier(BoolIdName),boolean,[])),pred,[]),Env,_,SatVar), | |
| 223 | ( (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_true,boolean,_)) | |
| 224 | -> BoolAtom = boolean_true | |
| 225 | ; (Bool = b(boolean_true,boolean,_), BoolPred = b(boolean_false,boolean,_)) | |
| 226 | -> BoolAtom = boolean_false | |
| 227 | ; (Bool = b(boolean_false,boolean,_), BoolPred = b(boolean_false,boolean,_)) | |
| 228 | -> BoolAtom = boolean_true | |
| 229 | ; BoolAtom = boolean_false | |
| 230 | ), | |
| 231 | !, | |
| 232 | safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 233 | NewEnv = Env, | |
| 234 | NVarAcc = VarAcc.*/ | |
| 235 | reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 236 | fetch_predicate(Pred, Env, _, SatVar), | |
| 237 | !, | |
| 238 | safe_create_texpr(equal(SatVar,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 239 | NewEnv = Env, | |
| 240 | NWDAcc = WDAcc, | |
| 241 | NVarAcc = VarAcc. | |
| 242 | reuse_or_introduce_bool_var(_, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 243 | Pred = b(Expr,Type,Info), | |
| 244 | negate_pred(Expr, NExpr), | |
| 245 | fetch_predicate(b(NExpr,Type,Info), Env, _, SatVar), | |
| 246 | !, | |
| 247 | negate_bool_atom(BoolAtom, NBoolAtom), | |
| 248 | safe_create_texpr(equal(SatVar,b(NBoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 249 | NewEnv = Env, | |
| 250 | NWDAcc = WDAcc, | |
| 251 | NVarAcc = VarAcc. | |
| 252 | reuse_or_introduce_bool_var(Type, WDAcc, VarAcc, Env, Pred, BoolAtom, NewEnv, NWDAcc, BoolFormula, NVarAcc) :- | |
| 253 | Type \== only_reuse, | |
| 254 | !, | |
| 255 | next_sat_var_name(SatVarName), | |
| 256 | add_wd_pos_to_pred(Pred, [], WDAcc, true, true, NWDAcc, WDPred, TopLevelWdPred), | |
| 257 | debug_format_pred("Introduce sat var ~w for pred~n", [SatVarName], WDPred), | |
| 258 | safe_create_texpr(identifier(SatVarName), boolean, [], TUniqueId), | |
| 259 | %find_identifier_uses(Pred, [], UsedIds), | |
| 260 | ( ground(TopLevelWdPred) | |
| 261 | -> add_texpr_infos(TUniqueId, [smt_formula(WDPred),contains_top_level_wd_condition(TopLevelWdPred,Pred)], UniqueId) | |
| 262 | ; add_texpr_infos(TUniqueId, [smt_formula(WDPred)], UniqueId) | |
| 263 | ), | |
| 264 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv), | |
| 265 | safe_create_texpr(equal(UniqueId,b(BoolAtom,boolean,[])), pred, [], BoolFormula), | |
| 266 | NVarAcc = [UniqueId|VarAcc]. | |
| 267 | reuse_or_introduce_bool_var(Type, _, _, _, Pred, _, _, _, _, _) :- | |
| 268 | Type == only_reuse, | |
| 269 | 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]). | |
| 270 | ||
| 271 | next_sat_var_name(SatVarName) :- | |
| 272 | retract(sat_var_id(Old)), | |
| 273 | New is Old + 1, | |
| 274 | asserta(sat_var_id(New)), | |
| 275 | number_codes(New, NC), | |
| 276 | atom_codes(Index, NC), | |
| 277 | atom_concat('sat', Index, SatVarName). | |
| 278 | ||
| 279 | quantified_binary_expr(exists). | |
| 280 | quantified_binary_expr(comprehension_set). | |
| 281 | ||
| 282 | quantified_ternary_expr_nonpred_body(lambda). | |
| 283 | quantified_ternary_expr_nonpred_body(general_sum). | |
| 284 | quantified_ternary_expr_nonpred_body(general_product). | |
| 285 | quantified_ternary_expr_nonpred_body(quantified_union). | |
| 286 | quantified_ternary_expr_nonpred_body(quantified_intersection). | |
| 287 | ||
| 288 | is_typing_pred_without_wd(b(member(Id,B),pred,_)) :- | |
| 289 | B \= b(domain(_),_,_), | |
| 290 | B \= b(empty_set,_,_), | |
| 291 | B \= b(value([]),_,_), | |
| 292 | B \= b(seq(_),_,_), % seq typing has a wd condition | |
| 293 | B \= b(seq1(_),_,_), | |
| 294 | Id = b(identifier(_),_,_). | |
| 295 | is_typing_pred_without_wd(b(subset(Id,B),pred,_)) :- | |
| 296 | B \= b(domain(_),_,_), | |
| 297 | B \= b(empty_set,_,_), | |
| 298 | B \= b(value([]),_,_), | |
| 299 | B \= b(seq(_),_,_), | |
| 300 | B \= b(seq1(_),_,_), | |
| 301 | Id = b(identifier(_),_,_). | |
| 302 | is_typing_pred_without_wd(b(subset_strict(Id,B),pred,_)) :- | |
| 303 | B \= b(domain(_),_,_), | |
| 304 | B \= b(empty_set,_,_), | |
| 305 | B \= b(value([]),_,_), | |
| 306 | B \= b(seq(_),_,_), | |
| 307 | B \= b(seq1(_),_,_), | |
| 308 | Id = b(identifier(_),_,_). | |
| 309 | % from rewriting let-expressions | |
| 310 | is_typing_pred_without_wd(b(member(b(comprehension_set([b(identifier('_zzzz_unary'),boolean,[]),b(identifier('_zzzz_binary'),integer,[])],_),_,_),_),pred,_)). | |
| 311 | is_typing_pred_without_wd(b(exists([b(identifier('_zzzz_binary'),integer,_)],_),pred,_)). | |
| 312 | ||
| 313 | clean_up_and_preprocess(Pred, Clean) :- | |
| 314 | clean_up_pred(Pred, _, TClean), | |
| 315 | remove_wd_pos_introduced_for_cdclt(true, TClean, TTClean), % there can be an added WD condition inside a WD condition for nested expressions; cleaning infos would work here too | |
| 316 | get_preference(cdclt_use_idl_theory_solver, RewriteToIdl), % possibly rewrite WD condition to IDL | |
| 317 | preprocess_predicate(false, RewriteToIdl, TTClean, LiftedPred, _, _), | |
| 318 | !, | |
| 319 | rewrite_emptyset(LiftedPred, TTTClean), | |
| 320 | rewrite_falsity_or_truth(TTTClean, Clean). | |
| 321 | ||
| 322 | %% rewrite_falsity_or_truth(+In, -Out). | |
| 323 | % Static contradictions or truths might be rewritten to falsity or truth. | |
| 324 | % This is a problem if the predicate is added inside a quantified formula since the | |
| 325 | % WD condition will then be found for the top-level predicate and will be added outside the quantified formula. | |
| 326 | % For instance, PI(id1).(-1 >= 0 |3 ** -1) where the WD condition is -1 >= 0. | |
| 327 | rewrite_falsity_or_truth(b(TruthOrFalsity,Type,Info), Clean) :- | |
| 328 | ( TruthOrFalsity == truth | |
| 329 | ; TruthOrFalsity == falsity | |
| 330 | ), | |
| 331 | select(was(Expr), Info, NInfo), | |
| 332 | !, | |
| 333 | Clean = b(Expr,Type,NInfo). | |
| 334 | rewrite_falsity_or_truth(Clean, Clean). | |
| 335 | ||
| 336 | rewrite_emptyset(b(negation(b(equal(A,b(empty_set,Type,Info)),pred,Info2)),pred,Info3), Out) :- | |
| 337 | % important if we use b_compile on the full predicate in cdclt_solver.pl | |
| 338 | % since empty_set is compiled to value([]) | |
| 339 | !, | |
| 340 | Out = b(negation(b(equal(A,b(value([]),Type,Info)),pred,Info2)),pred,Info3). | |
| 341 | rewrite_emptyset(Out, Out). | |
| 342 | ||
| 343 | get_top_level_wd_po_no_typing(Pred, Hypotheses, WDPo) :- | |
| 344 | empty_hyps(IHyps), | |
| 345 | ( Hypotheses == [] | |
| 346 | -> Hyps = IHyps | |
| 347 | ; push_hyps(IHyps, Hypotheses, [], Hyps) | |
| 348 | ), | |
| 349 | find_identifier_uses(Pred, [], TopLevelIds), | |
| 350 | compute_wd(Pred, Hyps, [discharge_po], TWDPo), % choicepoint | |
| 351 | TWDPo \= b(unknown_truth_value(_),_,_), % e.g., from external predicate calls such as RPOW | |
| 352 | find_identifier_uses(TWDPo, [], WDIds), | |
| 353 | subtract(WDIds, TopLevelIds, QIds), | |
| 354 | QIds == [], % is top-level | |
| 355 | TWDPo = b(_,_,TWDInfo), | |
| 356 | ( member(discharged(true, _), TWDInfo) | |
| 357 | -> debug_format_pred('Removed discharged predicate from WD POs: ', [], TWDPo), | |
| 358 | fail | |
| 359 | ; true | |
| 360 | ), | |
| 361 | % important to use b_ast_cleanup:clean_up_pred/3 for WD POs collected by compute_wd/4 since | |
| 362 | % typing constraints are optimized to 'typeset' nodes, which is undone by the cleanup. | |
| 363 | clean_up_and_preprocess(TWDPo, TTWDPo), | |
| 364 | ( is_typing_pred_without_wd(TTWDPo) | |
| 365 | -> debug_format_pred('Removed typing predicate from WD POs: ', [], TTWDPo), | |
| 366 | fail | |
| 367 | ; % WD POs might be conjunctions | |
| 368 | conjunction_to_list(TTWDPo, WDPo) | |
| 369 | ). | |
| 370 | ||
| 371 | remove_duplicate_preds(Constraints, NoDups) :- | |
| 372 | remove_duplicate_preds(Constraints, [], NoDups). | |
| 373 | ||
| 374 | remove_duplicate_preds([], _, []). | |
| 375 | remove_duplicate_preds([Pred|T], NormAcc, NoDups) :- | |
| 376 | norm_pred_check(Pred, NPred), | |
| 377 | ( memberchk(NPred, NormAcc) | |
| 378 | -> NoDups = NT, | |
| 379 | NNormAcc = NormAcc | |
| 380 | ; NoDups = [Pred|NT], | |
| 381 | NNormAcc = [NPred|NormAcc] | |
| 382 | ), | |
| 383 | remove_duplicate_preds(T, NNormAcc, NT). | |
| 384 | ||
| 385 | %% get_all_top_level_wd_pos(+Pred, -WDPos). | |
| 386 | get_all_top_level_wd_pos(Pred, WDPos) :- | |
| 387 | get_all_top_level_wd_pos(Pred, [], WDPos). | |
| 388 | ||
| 389 | %% get_all_top_level_wd_pos(+Pred, +Hypotheses, -WDPos). | |
| 390 | get_all_top_level_wd_pos(Pred, Hypotheses, WDPos) :- | |
| 391 | findall(WDPo, get_top_level_wd_po_no_typing(Pred, Hypotheses, WDPo), TWDPos), !, | |
| 392 | append(TWDPos, TTWDPos), | |
| 393 | remove_duplicate_preds(TTWDPos, WDPos). | |
| 394 | ||
| 395 | % 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. | |
| 396 | % We don't use a single implication A => (c1 & c2 & .. & cn) since we have to create a CNF anyway. | |
| 397 | create_wd_impls([], _, Acc, Acc). | |
| 398 | create_wd_impls([WDPo|T], Pred, Acc, WDImpls) :- | |
| 399 | % don't use added info is_wd_po_for_cdclt here | |
| 400 | NegP = b(negation(Pred),pred,[]), | |
| 401 | safe_create_texpr(disjunct(NegP,WDPo), pred, [], WDImpl1), | |
| 402 | safe_create_texpr(disjunct(WDPo,NegP), pred, [], WDImpl2), | |
| 403 | create_wd_impls(T, Pred, [WDImpl1,WDImpl2|Acc], WDImpls). | |
| 404 | ||
| 405 | add_wd_impls_to_acc([], WDAcc, WDAcc). | |
| 406 | add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :- | |
| 407 | member(WDImpl, WDAcc), | |
| 408 | !, | |
| 409 | add_wd_impls_to_acc(T, WDAcc, NWDAcc). | |
| 410 | add_wd_impls_to_acc([WDImpl|T], WDAcc, NWDAcc) :- | |
| 411 | add_wd_impls_to_acc(T, [WDImpl|WDAcc], NWDAcc). | |
| 412 | ||
| 413 | %% add_wd_pos_to_pred(+Pred, +Hyps, +WDAcc, +IsTopLevel, +AddToTopLevel, -NWDAcc, -WDPred, -WDPoConj). | |
| 414 | % Add all necessary WD POs to make +Pred well-defined for SMT solving. | |
| 415 | % That means, each predicate that is abstracted to a SAT variable is well-defined. | |
| 416 | % For quantified formulas, WD POs are nested inside a quantifier. | |
| 417 | % Only add WD POs to WDAcc if +IsTopLevel is true. | |
| 418 | % Note: let-expressions and if-then-else expressions have to be rewritten beforehand | |
| 419 | add_wd_pos_to_pred(Pred, Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc, WDPred, WDPoConj) :- | |
| 420 | Pred = b(Expr, Type, Info), | |
| 421 | add_wd_pos_to_pred_e(Expr, Type, Info, Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc, WDPred, WDPoConj). | |
| 422 | ||
| 423 | % 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. | |
| 424 | % 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 | |
| 425 | % to our top-level WD POs. | |
| 426 | add_wd_pos_to_pred_e(conjunct(A,B), pred, Info, Hyps, WDAcc, IsTopLevel, true, NWDAcc, WDPred, WDPoConj) :- | |
| 427 | !, | |
| 428 | add_wd_pos_to_pred(A, Hyps, WDAcc, IsTopLevel, true, NWDAcc1, WDA, WDAConj), | |
| 429 | NHyps = [WDA|Hyps], | |
| 430 | add_wd_pos_to_pred(B, NHyps, NWDAcc1, IsTopLevel, true, NWDAcc, WDB, WDBConj), | |
| 431 | NExpr = conjunct(WDA,WDB), | |
| 432 | conjunct_predicates([WDAConj,WDBConj], WDPoConj), | |
| 433 | safe_create_texpr(NExpr, pred, Info, WDPred). | |
| 434 | add_wd_pos_to_pred_e(Expr, pred, Info, Hyps, WDAcc, IsTopLevel, true, NWDAcc, WDPred, WDPoConj) :- | |
| 435 | functor(Expr, Functor, 2), | |
| 436 | (Functor == disjunct; Functor == implication; Functor == equivalence), | |
| 437 | !, | |
| 438 | arg(1, Expr, A), | |
| 439 | arg(2, Expr, B), | |
| 440 | add_wd_pos_to_pred(A, Hyps, WDAcc, IsTopLevel, true, NWDAcc1, WDA, WDAConj), | |
| 441 | add_wd_pos_to_pred(B, Hyps, NWDAcc1, IsTopLevel, true, NWDAcc, WDB, WDBConj), | |
| 442 | functor(NExpr, Functor, 2), | |
| 443 | arg(1, NExpr, WDA), | |
| 444 | arg(2, NExpr, WDB), | |
| 445 | conjunct_predicates([WDAConj,WDBConj], WDPoConj), | |
| 446 | safe_create_texpr(NExpr, pred, Info, WDPred). | |
| 447 | add_wd_pos_to_pred_e(negation(Pred), pred, Info, Hyps, WDAcc, IsTopLevel, _, NWDAcc, WDNeg, WDPoConj) :- | |
| 448 | !, | |
| 449 | add_wd_pos_to_pred(Pred, Hyps, WDAcc, IsTopLevel, true, NWDAcc, WDPred, WDPoConj), | |
| 450 | WDNeg = b(negation(WDPred),pred,Info). | |
| 451 | add_wd_pos_to_pred_e(if_then_else(Cond,Lhs,Rhs), pred, Info, Hyps, WDAcc, IsTopLevel, true, NWDAcc, WDPred, WDPoConj) :- | |
| 452 | !, | |
| 453 | add_wd_pos_to_pred(Cond, Hyps, WDAcc, IsTopLevel, true, NWDAcc1, WDCond, WDPoConj1), | |
| 454 | add_wd_pos_to_pred(Lhs, Hyps, NWDAcc1, IsTopLevel, true, NWDAcc2, WDLhs, WDPoConj2), | |
| 455 | add_wd_pos_to_pred(Rhs, Hyps, NWDAcc2, IsTopLevel, true, NWDAcc, WDRhs, WDPoConj3), | |
| 456 | safe_create_texpr(if_then_else(WDCond,WDLhs,WDRhs), pred, Info, WDPred), | |
| 457 | conjunct_predicates([WDPoConj1,WDPoConj2,WDPoConj3], WDPoConj). | |
| 458 | add_wd_pos_to_pred_e(Expr, Type, Info, Hyps, WDAcc, _, _, NWDAcc, WDPred, _) :- | |
| 459 | Expr =.. [Functor,Ids,Lhs,Rhs], | |
| 460 | ( Functor == forall; Functor == event_b_comprehension_set), | |
| 461 | !, | |
| 462 | add_wd_pos_to_pred(Rhs, Hyps, WDAcc, false, true, NWDAcc, WDRhs, _), | |
| 463 | NExpr =.. [Functor,Ids,Lhs,WDRhs], | |
| 464 | safe_create_texpr(NExpr, Type, Info, WDPred). | |
| 465 | add_wd_pos_to_pred_e(Expr, Type, Info, Hyps, WDAcc, _, _, NWDAcc, WDPred, _) :- | |
| 466 | Expr =.. [Functor,Ids,Lhs,Rhs], | |
| 467 | quantified_ternary_expr_nonpred_body(Functor), | |
| 468 | !, | |
| 469 | % get WD POs from RHS expression but add to LHS predicate | |
| 470 | get_all_top_level_wd_pos(Rhs, [Lhs|Hyps], WDPos), | |
| 471 | maplist(map_add_texpr_infos([is_wd_po_for_cdclt]), WDPos, NWDPos), | |
| 472 | conjunct_predicates(NWDPos, WDPoConj), | |
| 473 | safe_create_texpr(conjunct(WDPoConj,Lhs), pred, [], WDLhs), | |
| 474 | NExpr =.. [Functor,Ids,WDLhs,Rhs], | |
| 475 | % don't add to WDAcc since it's not at the top-level | |
| 476 | NWDAcc = WDAcc, | |
| 477 | safe_create_texpr(NExpr, Type, Info, WDPred). | |
| 478 | add_wd_pos_to_pred_e(Expr, pred, Info, Hyps, WDAcc, _, _, NWDAcc, WDPred, _) :- | |
| 479 | Expr =.. [Functor,Ids,Eqs,Body], | |
| 480 | (Functor == let; Functor == let_predicate), | |
| 481 | !, | |
| 482 | add_wd_pos_to_pred(Body, Hyps, WDAcc, false, true, NWDAcc, WDBody, _), | |
| 483 | NExpr =.. [Functor,Ids,Eqs,WDBody], | |
| 484 | safe_create_texpr(NExpr, pred, Info, WDPred). | |
| 485 | add_wd_pos_to_pred_e(Expr, Type, Info, Hyps, WDAcc, _, _, NWDAcc, WDPred, _) :- | |
| 486 | Expr =.. [Functor,Ids,Body], | |
| 487 | quantified_binary_expr(Functor), | |
| 488 | !, | |
| 489 | add_wd_pos_to_pred(Body, Hyps, WDAcc, false, true, NWDAcc, WDBody, _), | |
| 490 | NExpr =.. [Functor,Ids,WDBody], | |
| 491 | safe_create_texpr(NExpr, Type, Info, WDPred). | |
| 492 | add_wd_pos_to_pred_e(Expr, Type, Info, Hyps, WDAcc, IsTopLevel, true, NWDAcc, WDAst, WDPoConj) :- | |
| 493 | % e.g., for a = b - {some set comprehension with WD}, we want to add WD POs to the set comprehension but not the equality | |
| 494 | functor(Expr, Functor, _), | |
| 495 | Functor \== identifier, | |
| 496 | Functor \== integer, | |
| 497 | Functor \== value, | |
| 498 | Functor \== string, | |
| 499 | Functor \== partition, | |
| 500 | Functor \== external_pred_call, | |
| 501 | Expr =.. [Functor|Args], | |
| 502 | map_add_wd_pos_to_pred(Args, Hyps, WDAcc, false, true, NWDAcc1, WDArgs, _), | |
| 503 | NExpr =.. [Functor|WDArgs], | |
| 504 | Ast = b(Expr,Type,Info), | |
| 505 | NAst = b(NExpr,Type,Info), | |
| 506 | !, | |
| 507 | top_level_wd_post_processing(Type, Hyps, Ast, NAst, NWDAcc1, IsTopLevel, NWDAcc, WDAst, WDPoConj). | |
| 508 | add_wd_pos_to_pred_e(Expr, Type, Info, _, WDAcc, _, _, WDAcc, b(Expr,Type,Info), _). | |
| 509 | ||
| 510 | %% top_level_wd_post_processing(+Type, +Hyps, +Ast, +NAst, +WDAcc, +IsTopLevel, -NWDAcc, -WDAst). | |
| 511 | % Create top-level WD implications and WD PO conjunction if is predicate. | |
| 512 | % Only add WD POs to WDAcc if +IsTopLevel is true. | |
| 513 | top_level_wd_post_processing(pred, Hyps, Ast, NAst, WDAcc, IsTopLevel, NWDAcc, WDAst, WDPoConj) :- | |
| 514 | get_all_top_level_wd_pos(NAst, Hyps, WDPos), | |
| 515 | WDPos \== [], | |
| 516 | create_wd_impls(WDPos, Ast, [], WDImpls), % use Ast here, not NAst where WD POs have potentially been added | |
| 517 | conjunct_predicates(WDPos, WDPoConj), % don't use added info is_wd_po_for_cdclt here | |
| 518 | !, | |
| 519 | debug_format_pred("--------------------------Add WD PO for AST~n", [], NAst), | |
| 520 | ( IsTopLevel == true | |
| 521 | -> add_wd_impls_to_acc(WDImpls, WDAcc, NWDAcc) | |
| 522 | ; NWDAcc = WDAcc | |
| 523 | ), | |
| 524 | maplist(map_add_texpr_infos([is_wd_po_for_cdclt]), WDPos, NWDPos), | |
| 525 | conjunct_predicates(NWDPos, WDPo), | |
| 526 | conjunct_predicates([WDPo,NAst], WDAst). | |
| 527 | top_level_wd_post_processing(_, _, _, NAst, WDAcc, _, WDAcc, NAst, _). | |
| 528 | ||
| 529 | map_add_wd_pos_to_pred([Arg|T], Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc, [WDArg|TWDArgs], WDConj) :- | |
| 530 | add_wd_pos_to_pred(Arg, Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc1, WDArg, WDConjArg), | |
| 531 | map_add_wd_po_to_pred_acc(T, Hyps, NWDAcc1, IsTopLevel, AddToTopLevel, NWDAcc, WDConjArg, TWDArgs, WDConj). | |
| 532 | ||
| 533 | map_add_wd_po_to_pred_acc([], _, WDAcc, _, _, WDAcc, WDConjAcc, [], WDConjAcc). | |
| 534 | map_add_wd_po_to_pred_acc([Arg|T], Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc, WDConjAcc, [WDArg|TWDArgs], WDConj) :- | |
| 535 | add_wd_pos_to_pred(Arg, Hyps, WDAcc, IsTopLevel, AddToTopLevel, NWDAcc1, WDArg, WDConjArg), | |
| 536 | ( ground(WDConjArg) | |
| 537 | -> safe_create_texpr(conjunct(WDConjArg,WDConjAcc),pred,[],NWDConjAcc) | |
| 538 | ; NWDConjAcc = WDConjAcc | |
| 539 | ), | |
| 540 | map_add_wd_po_to_pred_acc(T, Hyps, NWDAcc1, IsTopLevel, AddToTopLevel, NWDAcc, NWDConjAcc, TWDArgs, WDConj). | |
| 541 | % ---------------- | |
| 542 | ||
| 543 | ||
| 544 | quantified_expr(forall(Ids,Lhs,Rhs), forall, Ids, [Lhs,Rhs]). | |
| 545 | quantified_expr(exists(Ids,Body), exists, Ids, [Body]). | |
| 546 | quantified_expr(comprehension_set(Ids,Body), comprehension_set, Ids, [Body]). | |
| 547 | quantified_expr(event_b_comprehension_set(Ids,T,Body), event_b_comprehension_set, Ids, [T,Body]). | |
| 548 | quantified_expr(lambda(Ids,Pred,Body), lambda, Ids, [Pred,Body]). | |
| 549 | quantified_expr(general_sum(Ids,Pred,Body), general_sum, Ids, [Pred,Body]). | |
| 550 | quantified_expr(general_product(Ids,Pred,Body), general_product, Ids, [Pred,Body]). | |
| 551 | quantified_expr(quantified_union(Ids,Pred,Body), quantified_union, Ids, [Pred,Body]). | |
| 552 | quantified_expr(quantified_intersection(Ids,Pred,Body), quantified_intersection, Ids, [Pred,Body]). | |
| 553 | ||
| 554 | %% remove_wd_pos_introduced_for_cdclt_keep_toplevel(+Conj, -NConj). | |
| 555 | % 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. | |
| 556 | remove_wd_pos_introduced_for_cdclt_keep_toplevel(Conj, NConj) :- | |
| 557 | remove_wd_pos_introduced_for_cdclt(false, Conj, NConj). | |
| 558 | ||
| 559 | %% remove_wd_pos_introduced_for_cdclt(+Remove, +Conj, -NConj). | |
| 560 | % Remove WD POs introduced for cdclt if +Remove is true. | |
| 561 | remove_wd_pos_introduced_for_cdclt(Remove, Conj, NConj) :- | |
| 562 | conjunction_to_list(Conj, List), | |
| 563 | !, | |
| 564 | remove_wd_pos_introduced_for_cdclt_l(Remove, List, NList), | |
| 565 | conjunct_predicates(NList, NConj). | |
| 566 | remove_wd_pos_introduced_for_cdclt(_, Node, Node). | |
| 567 | ||
| 568 | % TODO: first argument indexing | |
| 569 | remove_wd_pos_introduced_for_cdclt_l(_, [], []). | |
| 570 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], Out) :- | |
| 571 | Pred = b(_,_,Info), | |
| 572 | memberchk(is_wd_po_for_cdclt, Info), | |
| 573 | !, | |
| 574 | ( ( Remove == true | |
| 575 | ; % disjunction only occurs for WD condition x/=0 of y/x if IDL solver is used | |
| 576 | % inequality results in disjunction but conflict has to be conjunction | |
| 577 | % so remove this WD condition in this specific case | |
| 578 | Pred = b(disjunct(_,_),_,_) | |
| 579 | ) | |
| 580 | -> Out = NT, | |
| 581 | debug_format_pred("-----------------------removed wd po from unsat core: ", [], Pred) | |
| 582 | ; Out = [Pred|NT] | |
| 583 | ), | |
| 584 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 585 | remove_wd_pos_introduced_for_cdclt_l(Remove, [b(negation(Pred),pred,NInfo)|T], [Out|NT]) :- | |
| 586 | !, | |
| 587 | remove_wd_pos_introduced_for_cdclt(true, Pred, NPred), | |
| 588 | safe_create_texpr(negation(NPred), pred, NInfo, Out), | |
| 589 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 590 | remove_wd_pos_introduced_for_cdclt_l(Remove, [b(convert_bool(Pred),boolean,NInfo)|T], [Out|NT]) :- | |
| 591 | !, | |
| 592 | remove_wd_pos_introduced_for_cdclt(true, Pred, NPred), | |
| 593 | safe_create_texpr(convert_bool(NPred), boolean, NInfo, Out), | |
| 594 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 595 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 596 | Pred = b(Expr,Type,Info), | |
| 597 | Expr =.. [Functor,Ids,Eqs,Body], | |
| 598 | (Functor == let; Functor == let_predicate; Functor == lazy_let_pred), | |
| 599 | !, | |
| 600 | remove_wd_pos_introduced_for_cdclt(true, Body, NBody), | |
| 601 | NExpr =.. [Functor,Ids,Eqs,NBody], | |
| 602 | safe_create_texpr(NExpr, Type, Info, Out), | |
| 603 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 604 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 605 | Pred = b(Expr,Type,Info), | |
| 606 | quantified_expr(Expr, Functor, Ids, Subs), | |
| 607 | !, | |
| 608 | maplist(remove_wd_pos_introduced_for_cdclt(true), Subs, NSubs), | |
| 609 | NExpr =.. [Functor,Ids|NSubs], | |
| 610 | safe_create_texpr(NExpr, Type, Info, Out), | |
| 611 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 612 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 613 | Pred = b(Expr,Type,Info), | |
| 614 | functor(Expr, Functor, 1), | |
| 615 | !, | |
| 616 | arg(1, Expr, Arg), | |
| 617 | remove_wd_pos_introduced_for_cdclt(Remove, Arg, NArg), | |
| 618 | functor(NExpr, Functor, 1), | |
| 619 | arg(1, NExpr, NArg), | |
| 620 | Out = b(NExpr,Type,Info), | |
| 621 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 622 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], [Out|NT]) :- | |
| 623 | Pred = b(Expr,Type,Info), | |
| 624 | functor(Expr, Functor, 2), | |
| 625 | Functor \== external_pred_call, | |
| 626 | Functor \== partition, | |
| 627 | !, | |
| 628 | arg(1, Expr, Arg1), | |
| 629 | arg(2, Expr, Arg2), | |
| 630 | remove_wd_pos_introduced_for_cdclt(Remove, Arg1, NArg1), | |
| 631 | remove_wd_pos_introduced_for_cdclt(Remove, Arg2, NArg2), | |
| 632 | functor(NExpr, Functor, 2), | |
| 633 | arg(1, NExpr, NArg1), | |
| 634 | arg(2, NExpr, NArg2), | |
| 635 | Out = b(NExpr,Type,Info), | |
| 636 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 637 | remove_wd_pos_introduced_for_cdclt_l(Remove, [Pred|T], [Pred|NT]) :- | |
| 638 | remove_wd_pos_introduced_for_cdclt_l(Remove, T, NT). | |
| 639 | ||
| 640 | map_add_texpr_infos(ToBeAdded, Ast, NAst) :- | |
| 641 | add_texpr_infos(Ast, ToBeAdded, NAst). | |
| 642 | ||
| 643 | % managing link from predicates to SAT variables | |
| 644 | ||
| 645 | empty_predicate_env(E) :- empty_avl(E). | |
| 646 | ||
| 647 | % TO DO: maybe we should also store SatVarName? | |
| 648 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- | |
| 649 | ( var(Env) | |
| 650 | ; \+ is_avl(Env) | |
| 651 | ), | |
| 652 | !, | |
| 653 | add_internal_error('Illegal env:', register_predicate(Pred,WDPred,Env,UniqueId,NewEnv)), | |
| 654 | NewEnv = Env. | |
| 655 | register_predicate(Pred,WDPred,Env,UniqueId,NewEnv) :- %print('storing: '), writeq(WDPred),nl, | |
| 656 | norm_pred_check(Pred, NPred), | |
| 657 | avl_store(NPred,Env,pred2satvar(WDPred,UniqueId),NewEnv). | |
| 658 | ||
| 659 | fetch_predicate(Pred,Env,StoredPred,SatVar) :- (var(Env) ; \+ is_avl(Env)),!, | |
| 660 | add_internal_error('Illegal env:',fetch_predicate(Pred,Env,StoredPred,SatVar)), fail. | |
| 661 | fetch_predicate(Pred,Env,StoredPred,SatVar) :- | |
| 662 | norm_pred_check(Pred, NPred), | |
| 663 | avl_fetch(NPred,Env,pred2satvar(StoredPred,SatVar)), !. | |
| 664 | %fetch_predicate(Pred,_,_,_SatVar) :- print('not found: '), print_bexpr(Pred),nl,fail. | |
| 665 | ||
| 666 | % --------------- | |
| 667 | ||
| 668 | ||
| 669 | %% sat_to_predicate_from_solution(+SatBindings, +SatVars, -Conjunction). | |
| 670 | % Create conjunction of SAT bindings using their corresponding SMT formulae | |
| 671 | % which are stored in the bool variables' information fields. | |
| 672 | sat_to_predicate_from_solution([], _, b(truth,pred,[])). | |
| 673 | sat_to_predicate_from_solution([Binding|T], SatVars, Conjunction) :- | |
| 674 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars), | |
| 675 | !, | |
| 676 | sat_to_predicate_from_solution(T, SMT, RestSatVars, Conjunction). | |
| 677 | sat_to_predicate_from_solution([_|T], SatVars, Conjunction) :- | |
| 678 | % skip: binding might be a variable if instantiation is not required | |
| 679 | sat_to_predicate_from_solution(T, SatVars, Conjunction). | |
| 680 | ||
| 681 | sat_to_predicate_from_solution([], SmtAcc, _, SmtAcc). | |
| 682 | sat_to_predicate_from_solution([Binding|T], SmtAcc, SatVars, Conjunction) :- | |
| 683 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars), | |
| 684 | !, | |
| 685 | safe_create_texpr(conjunct(SMT,SmtAcc), pred, [], NewSmtAcc), | |
| 686 | sat_to_predicate_from_solution(T, NewSmtAcc, RestSatVars, Conjunction). | |
| 687 | sat_to_predicate_from_solution([_|T], SmtAcc, SatVars, Conjunction) :- | |
| 688 | sat_to_predicate_from_solution(T, SmtAcc, SatVars, Conjunction). | |
| 689 | ||
| 690 | get_var_and_value_from_binding(bind(SatVarName,Value), SatVarName, Value). | |
| 691 | get_var_and_value_from_binding(binding(SatVarName,Value,_), SatVarName, Value). | |
| 692 | ||
| 693 | get_smt_formula_from_binding(Binding, SatVars, SMT, RestSatVars) :- | |
| 694 | ground(Binding), | |
| 695 | get_var_and_value_from_binding(Binding, SatVarName, Value), | |
| 696 | !, | |
| 697 | select(b(identifier(SatVarName),_,Info), SatVars, RestSatVars), | |
| 698 | member(smt_formula(TSMT), Info),!, | |
| 699 | ( Value == pred_true | |
| 700 | -> SMT = TSMT | |
| 701 | ; Value == pred_false, | |
| 702 | TSMT = b(_,_,TSMTInfo), | |
| 703 | safe_create_texpr(negation(TSMT), pred, TSMTInfo, SMT) | |
| 704 | ). | |
| 705 | /*get_smt_formula_from_binding(Binding, _, _, _) :- | |
| 706 | add_error(get_smt_formula_from_binding, 'SAT binding not ground:', [Binding]), | |
| 707 | fail.*/ |