| 1 | % (c) 2020-2026 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 | :- module(difference_logic_solver, [init_idl_solver/1, | |
| 5 | register_constraint/2, | |
| 6 | register_constraints/2, | |
| 7 | solve_idl_conj/2, | |
| 8 | is_idl_constraint/1, | |
| 9 | get_solver_result/2, | |
| 10 | get_all_solutions_on_bt/2, | |
| 11 | try_candidate_bounds/3, | |
| 12 | get_registered_vars/2, | |
| 13 | get_unsat_core/1, | |
| 14 | infer_constraints_for_idl_solver/2, | |
| 15 | negate_dl_constraint/2, | |
| 16 | remove_unsat_core/0]). | |
| 17 | ||
| 18 | :- use_module(library(lists), [select/3]). | |
| 19 | :- use_module(library(plunit)). | |
| 20 | ||
| 21 | :- use_module(probsrc(preferences), [set_preference/2]). | |
| 22 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, conjunction_to_list/2]). | |
| 23 | :- use_module(cdclt_solver('difference_logic/ast_to_difference_logic')). | |
| 24 | ||
| 25 | :- dynamic predecessor/2, negative_weight/0, contains_zero/0, constraint_store/3, unsat_core/1. | |
| 26 | :- volatile predecessor/2, negative_weight/0, contains_zero/0, constraint_store/3, unsat_core/1. | |
| 27 | ||
| 28 | % A graph based solver for difference logic, i.e., constraints of the form Minuend - Subtrahend <= Constant. | |
| 29 | % Each node represents a variable. For a constraint x-y<=c a weighted edge (y,c,x) is added, while not(x-y<=c) yields | |
| 30 | % the edge (x,-c-1,y). | |
| 31 | % A difference logic constraint system is satisfiable if its corresponding graph does not contain a negative cycle. | |
| 32 | % If satisfiable, the shortest path to a variable yields its solution. | |
| 33 | % Otherwise, the conjunction of constraints corresponding to the edges of the negative cycle are an unsat core. | |
| 34 | % Note: Integer inequality has to be rewritten beforehand since it yields a disjunction in difference logic. | |
| 35 | ||
| 36 | %% solve_idl_conj(+Pred, -Result). | |
| 37 | solve_idl_conj(Pred, Result) :- | |
| 38 | init_idl_solver(GraphMut), | |
| 39 | conjunction_to_list(Pred, ConjList), | |
| 40 | ( register_constraints(GraphMut, ConjList), | |
| 41 | !, | |
| 42 | get_solver_result(GraphMut, Result) | |
| 43 | ; get_solver_result(GraphMut, TResult), | |
| 44 | TResult == contradiction_found, | |
| 45 | !, | |
| 46 | get_unsat_core(Core), | |
| 47 | Result = contradiction_found(Core) | |
| 48 | ; Result = no_solution_found(no_idl_constraint) | |
| 49 | ). | |
| 50 | ||
| 51 | %% init_idl_solver. | |
| 52 | init_idl_solver(GraphMut) :- | |
| 53 | create_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut), | |
| 54 | set_preference(normalize_ast, true), | |
| 55 | retractall(predecessor(_,_)), | |
| 56 | retractall(unsat_core(_)), | |
| 57 | retractall(constraint_store(_,_,_)), | |
| 58 | retractall(negative_weight), | |
| 59 | retractall(contains_zero). | |
| 60 | ||
| 61 | negate_dl_constraint(b(equal(A,B),pred,Info), NegDL) :- | |
| 62 | !, | |
| 63 | NegDL = b(not_equal(A,B),pred,Info). | |
| 64 | negate_dl_constraint(b(not_equal(A,B),pred,Info), NegDL) :- | |
| 65 | !, | |
| 66 | NegDL = b(equal(A,B),pred,Info). | |
| 67 | negate_dl_constraint(b(negation(Constraint),pred,[]), Constraint). | |
| 68 | negate_dl_constraint(Constraint, b(negation(Constraint),pred,[])). | |
| 69 | ||
| 70 | %% get_registered_vars(+GraphMut, -Vars). | |
| 71 | get_registered_vars(GraphMut, Vars) :- | |
| 72 | get_mutable(graph(nodes(Vars),_,_), GraphMut). | |
| 73 | ||
| 74 | %% register_constraints(+GraphMut, +ListOfConstraints). | |
| 75 | register_constraints(_, []). | |
| 76 | register_constraints(GraphMut, [Constraint|T]) :- | |
| 77 | register_constraint(GraphMut, Constraint), | |
| 78 | register_constraints(GraphMut, T). | |
| 79 | ||
| 80 | %% register_constraint(+GraphMut, +Constraint). | |
| 81 | % Accepted top level operators are <,<=,= and its negations. | |
| 82 | % Fails if constraint can not be transformed to difference logic | |
| 83 | % or produces a contradiction with existing constraints. | |
| 84 | register_constraint(GraphMut, Constraint) :- | |
| 85 | %write('Register Constraint..'),nl, | |
| 86 | %translate:print_bexpr(Constraint),nl, | |
| 87 | ( is_idl_constraint(Constraint) | |
| 88 | -> register_idl_constraint(GraphMut, Constraint), | |
| 89 | solve_incremental_constraint(GraphMut, Constraint) | |
| 90 | ; rewrite_to_idl(Constraint, DLConstraints), | |
| 91 | register_constraints_from_conj_list(GraphMut, DLConstraints), | |
| 92 | solve_incremental_list(GraphMut, DLConstraints) | |
| 93 | ). | |
| 94 | ||
| 95 | %% relax_edge_cond(+GraphMut, +In, +Out, +Weight, -ND). | |
| 96 | relax_edge_cond(GraphMut, In, Out, Weight, ND) :- | |
| 97 | get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut), | |
| 98 | member((In,DIn), SPs), | |
| 99 | member((Out,DOut), SPs), | |
| 100 | ND is DIn + Weight, | |
| 101 | ND < DOut. | |
| 102 | ||
| 103 | %% relax_node_distance(+GraphMut, +In, +Out, +ND, -DiffToOld). | |
| 104 | relax_node_distance(GraphMut, In, Out, ND, DiffToOld) :- | |
| 105 | assert_distance(GraphMut, Out, ND, DiffToOld), | |
| 106 | assert_predecessor(Out, In). | |
| 107 | ||
| 108 | solve_incremental_constraint(GraphMut, DLConstraint) :- | |
| 109 | get_edge_from_dl_constraint(DLConstraint, In, Out, Weight), | |
| 110 | solve_incremental(GraphMut, In, Out, Weight). | |
| 111 | ||
| 112 | solve_incremental_list(_, []). | |
| 113 | solve_incremental_list(GraphMut, [DLConstraint|T]) :- | |
| 114 | solve_incremental_constraint(GraphMut, DLConstraint), | |
| 115 | solve_incremental_list(GraphMut, T). | |
| 116 | ||
| 117 | %% solve_incremental(+In, +Out, +Weight). | |
| 118 | % Update shortest paths while searching for a negative cycle. | |
| 119 | solve_incremental(_, _, _, _) :- | |
| 120 | % no negative cycle without a negative weight | |
| 121 | \+ negative_weight. | |
| 122 | solve_incremental(GraphMut, In, Out, Weight) :- | |
| 123 | negative_weight, | |
| 124 | detect_negative_cycle_inc(GraphMut, [], In, Out, Weight, NegativeCycle), | |
| 125 | ( NegativeCycle == none | |
| 126 | -> % shortest paths stored in dis/2 are a solution | |
| 127 | true | |
| 128 | ; get_unsat_core_from_negative_cycle(GraphMut, NegativeCycle, UnsatCore), | |
| 129 | %nl, write('Unsat Core: '), nl,translate:print_bexpr(UnsatCore),nl, | |
| 130 | %writeq(UnsatCore),nl, | |
| 131 | asserta(unsat_core(UnsatCore)), | |
| 132 | fail | |
| 133 | ). | |
| 134 | ||
| 135 | %% get_edge_from_dl_constraint(+Node, -In, -Out, -Weight). | |
| 136 | get_edge_from_dl_constraint(b(less_equal(Sub,Constant),pred,_), In, Out, Weight) :- | |
| 137 | % edge (y,c,x) for x-y<=c | |
| 138 | get_id_names_from_idl_minus(Sub, Out, In), | |
| 139 | get_int_value(Constant, Weight). | |
| 140 | get_edge_from_dl_constraint(b(negation(Constraint),pred,_), In, Out, Weight) :- | |
| 141 | % edge (x,-c-1,y) for not(x-y<=c) | |
| 142 | Constraint = b(less_equal(Sub,Constant),pred,_), | |
| 143 | get_id_names_from_idl_minus(Sub, In, Out), | |
| 144 | get_int_value(Constant, TWeight), | |
| 145 | Weight is TWeight * -1 - 1. | |
| 146 | ||
| 147 | get_id_names_from_idl_minus(b(minus(Id1,Id2),integer,_), In, Out) :- | |
| 148 | Id1 = b(identifier(In),integer,_), | |
| 149 | Id2 = b(identifier(Out),integer,_). | |
| 150 | ||
| 151 | %% get_all_solutions_on_bt(+GraphMut, -SolverResult). | |
| 152 | get_all_solutions_on_bt(GraphMut, SolverResult) :- | |
| 153 | % TO DO: randomized enumeration order, log upper and lower bounded vars? | |
| 154 | get_solver_result(GraphMut, TSolverResult), | |
| 155 | TSolverResult = solution(Bindings), | |
| 156 | ( SolverResult = TSolverResult | |
| 157 | ; exclude_solution_bt(GraphMut, Bindings), | |
| 158 | get_all_solutions_on_bt(GraphMut, SolverResult) | |
| 159 | ). | |
| 160 | ||
| 161 | exclude_solution_bt(GraphMut, [binding(VarName,int(Val),_)|T]) :- | |
| 162 | % register inequality constraint VarName /= Val with choicepoint since rewriting yields a disjunction | |
| 163 | % i.e., x/=c -> x-_zero<=c-1 or _zero-x<=-c-1 | |
| 164 | ( exclude_solution_from_binding(GraphMut, VarName, Val) | |
| 165 | ; remove_unsat_core, | |
| 166 | Val1 is Val * -1, | |
| 167 | % equality | |
| 168 | LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]), | |
| 169 | LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]), | |
| 170 | register_constraints(GraphMut, [LEQ1,LEQ2]), | |
| 171 | exclude_solution_bt(GraphMut, T) | |
| 172 | ). | |
| 173 | ||
| 174 | exclude_solution_from_binding(GraphMut, VarName, Val) :- | |
| 175 | DisjVal1 is Val - 1, | |
| 176 | DisjVal2 is Val * -1 - 1, | |
| 177 | VarId = b(identifier(VarName),integer,[]), | |
| 178 | ZeroId = b(identifier('_zero'),integer,[]), | |
| 179 | Disj1 = b(less_equal(b(minus(VarId,ZeroId),integer,[]),b(integer(DisjVal1),integer,[])),pred,[]), | |
| 180 | Disj2 = b(less_equal(b(minus(ZeroId,VarId),integer,[]),b(integer(DisjVal2),integer,[])),pred,[]), | |
| 181 | ( remove_unsat_core, | |
| 182 | register_constraint(GraphMut, Disj1) | |
| 183 | ; remove_unsat_core, | |
| 184 | register_constraint(GraphMut, Disj2) | |
| 185 | ). | |
| 186 | ||
| 187 | %% try_candidate_bounds(+GraphMut, +CandidateTuples, -SolverResult). | |
| 188 | % Try candidate bounds obtained by syntactic analysis of non idl constraints when backtracking from ProB to IDL solver. | |
| 189 | % CandidateTuples is a list of tuples of variable and possible bounding values. | |
| 190 | try_candidate_bounds(GraphMut, CandidateTuples, SolverResult) :- | |
| 191 | try_candidate_bounds(GraphMut, none, CandidateTuples, Diff-Diff, SolverResult). | |
| 192 | ||
| 193 | % Successively try one value for each variable with choicepoints to find all combinations on backtracking. | |
| 194 | try_candidate_bounds(GraphMut, Solution, [], L-Diff, SolverResult) :- | |
| 195 | Diff = [], | |
| 196 | L \== [], | |
| 197 | try_candidate_bounds(GraphMut, Solution, L, NDiff-NDiff, SolverResult). | |
| 198 | try_candidate_bounds(GraphMut, Solution, [(_,[])|T], L-Diff, SolverResult) :- | |
| 199 | try_candidate_bounds(GraphMut, Solution, T, L-Diff, SolverResult). | |
| 200 | try_candidate_bounds(GraphMut, none, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :- | |
| 201 | % x=val | |
| 202 | LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]), | |
| 203 | NVal is Val * -1, | |
| 204 | LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(NVal),integer,[])),pred,[]), | |
| 205 | remove_unsat_core, | |
| 206 | register_constraints(GraphMut, [LEQ1,LEQ2]), | |
| 207 | get_solver_result(GraphMut, TSolverResult), | |
| 208 | TSolverResult = solution(_), | |
| 209 | ( SolverResult = TSolverResult | |
| 210 | ; Diff = [(VarName,TVals)|NDiff], | |
| 211 | try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult) | |
| 212 | ). | |
| 213 | try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :- | |
| 214 | ( Solution == none | |
| 215 | ; ground(Solution), | |
| 216 | Solution = solution(Bindings), | |
| 217 | member(binding(VarName,int(OldVal),_), Bindings), | |
| 218 | Val < OldVal | |
| 219 | ), | |
| 220 | Val1 is Val - 1, | |
| 221 | % x<val | |
| 222 | LEQ = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]), | |
| 223 | remove_unsat_core, | |
| 224 | register_constraint(GraphMut, LEQ), | |
| 225 | get_solver_result(GraphMut, TSolverResult), | |
| 226 | TSolverResult = solution(_), | |
| 227 | ( SolverResult = TSolverResult | |
| 228 | ; Diff = [(VarName,TVals)|NDiff], | |
| 229 | try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult) | |
| 230 | ). | |
| 231 | try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :- | |
| 232 | ( Solution == none | |
| 233 | ; ground(Solution), | |
| 234 | Solution = solution(Bindings), | |
| 235 | member(binding(VarName,int(OldVal),_), Bindings), | |
| 236 | Val > OldVal | |
| 237 | ), | |
| 238 | Val1 is Val * -1 - 1, | |
| 239 | % x>val | |
| 240 | LEQ = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]), | |
| 241 | remove_unsat_core, | |
| 242 | register_constraint(GraphMut, LEQ), | |
| 243 | get_solver_result(GraphMut, TSolverResult), | |
| 244 | TSolverResult = solution(_), | |
| 245 | ( SolverResult = TSolverResult | |
| 246 | ; Diff = [(VarName,TVals)|NDiff], | |
| 247 | try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult) | |
| 248 | ). | |
| 249 | try_candidate_bounds(GraphMut, Solution, [(VarName,[_|TVals])|T], L-Diff, SolverResult) :- | |
| 250 | Diff = [(VarName,TVals)|NDiff], | |
| 251 | try_candidate_bounds(GraphMut, Solution, T, L-NDiff, SolverResult). | |
| 252 | ||
| 253 | remove_unsat_core :- | |
| 254 | retract(unsat_core(_)), | |
| 255 | !. | |
| 256 | remove_unsat_core. | |
| 257 | ||
| 258 | %% get_solver_result(+GraphMut, -SolverResult). | |
| 259 | get_solver_result(_, SolverResult) :- | |
| 260 | unsat_core(_), | |
| 261 | !, | |
| 262 | SolverResult = contradiction_found. | |
| 263 | get_solver_result(GraphMut, SolverResult) :- | |
| 264 | get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut), | |
| 265 | shortest_paths_to_bindings(SPs, [], TempBindings), % TO DO: shift at the same time? | |
| 266 | ground(TempBindings), | |
| 267 | possibly_shift_solution_for_zero(TempBindings, Bindings),!, | |
| 268 | SolverResult = solution(Bindings). | |
| 269 | ||
| 270 | shortest_paths_to_bindings([], Acc, Acc). | |
| 271 | shortest_paths_to_bindings([(VarName,Val)|T], Acc, Bindings) :- | |
| 272 | number_to_atom(Val, ValAtom), | |
| 273 | shortest_paths_to_bindings(T, [binding(VarName,int(Val),ValAtom)|Acc], Bindings). | |
| 274 | ||
| 275 | %% detect_negative_cycle_inc(+GraphMut, +Queue, +In, +Out, +Weight, -NegativeCycle). | |
| 276 | % Incremental negative cycle detection and shortest path computation as suggested by Chao Wang et al. | |
| 277 | % Queue is sorted by maximal node value changes. | |
| 278 | detect_negative_cycle_inc(GraphMut, Queue, In, Out, Weight, NegativeCycle) :- | |
| 279 | ( relax_edge_cond(GraphMut, In, Out, Weight, NDOut) | |
| 280 | -> relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld), | |
| 281 | insertion_sort(Queue, Out, DiffToOld, NQueue) | |
| 282 | ; NQueue = Queue | |
| 283 | ), | |
| 284 | detect_negative_cycle_inc(GraphMut, In, Out, NQueue, NegativeCycle). | |
| 285 | ||
| 286 | detect_negative_cycle_inc(_, _, _, [], none). | |
| 287 | detect_negative_cycle_inc(GraphMut, StartIn, StartOut, [(CurNode,_)|T], NegativeCycle) :- | |
| 288 | get_adjacent_edges(GraphMut, CurNode, Adjacent), | |
| 289 | detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, Adjacent, T, NQueue, TNegativeCycle), | |
| 290 | (TNegativeCycle \== none | |
| 291 | -> NegativeCycle = TNegativeCycle | |
| 292 | ; detect_negative_cycle_inc(GraphMut, StartIn, StartOut, NQueue, NegativeCycle) | |
| 293 | ). | |
| 294 | ||
| 295 | detect_negative_cycle_inc_process_edges(_, _, _, [], Queue, Queue, none). | |
| 296 | detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, [(In,Weight,Out,_)|T], Queue, NQueue, NegativeCycle) :- | |
| 297 | ( relax_edge_cond(GraphMut, In, Out, Weight, NDOut) | |
| 298 | -> ( (In == StartIn, Out == StartOut) | |
| 299 | -> get_negative_cycle_from_predecessors(Out, NegativeCycle) | |
| 300 | ; relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld), | |
| 301 | insertion_sort(Queue, Out, DiffToOld, TQueue), | |
| 302 | detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, TQueue, NQueue, NegativeCycle) | |
| 303 | ) | |
| 304 | ; detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, Queue, NQueue, NegativeCycle) | |
| 305 | ). | |
| 306 | ||
| 307 | get_adjacent_edges(GraphMut, Node, Adjacent) :- | |
| 308 | get_mutable(graph(_,edges(Edges),_), GraphMut), | |
| 309 | memberchk(Node:TAdjacent, Edges), | |
| 310 | !, | |
| 311 | Adjacent = TAdjacent. | |
| 312 | get_adjacent_edges(_, _, []). | |
| 313 | ||
| 314 | %% get_negative_cycle_from_predecessors(+Out, -NegativeCycle). | |
| 315 | get_negative_cycle_from_predecessors(Out, NegativeCycle) :- | |
| 316 | get_negative_cycle_from_predecessors(Out, Out, [], NegativeCycle). | |
| 317 | ||
| 318 | get_negative_cycle_from_predecessors(Start, Start, Acc, Acc) :- | |
| 319 | Acc \== []. | |
| 320 | get_negative_cycle_from_predecessors(Start, CurNode, Acc, NegativeCycle) :- | |
| 321 | retract(predecessor(CurNode, PreNode)), | |
| 322 | get_negative_cycle_from_predecessors(Start, PreNode, [PreNode|Acc], NegativeCycle). | |
| 323 | ||
| 324 | %% get_unsat_core_from_negative_cycle(+GraphMut, +NegativeCycle, -UnsatCore). | |
| 325 | % Conjunct the constraints corresponding to the negative cycle in the constraint graph. | |
| 326 | get_unsat_core_from_negative_cycle(GraphMut, [SrcNode|T], UnsatCore) :- | |
| 327 | get_mutable(graph(_,edges(Edges),_), GraphMut), | |
| 328 | get_unsat_core_from_negative_cycle(Edges, [SrcNode|T], SrcNode, [], UnsatCoreList), | |
| 329 | conjunct_predicates(UnsatCoreList, UnsatCore), !. | |
| 330 | ||
| 331 | %% get_unsat_core_from_negative_cycle(+Edges, +NegativeCycleNodes, +SrcNode, +Acc, -UnsatCoreList). | |
| 332 | get_unsat_core_from_negative_cycle(Edges, [CurNode], SrcNode, Acc, NewAcc) :- | |
| 333 | !, | |
| 334 | member(CurNode:Adjacent, Edges), | |
| 335 | member((CurNode,_,SrcNode,DLConstraint), Adjacent), | |
| 336 | get_original_constraint(DLConstraint, Constraint), | |
| 337 | %nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl, | |
| 338 | %write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl, | |
| 339 | NewAcc = [Constraint|Acc]. | |
| 340 | get_unsat_core_from_negative_cycle(Edges, [CurNode,NextNode|T], SrcNode, Acc, UnsatCoreList) :- | |
| 341 | member(CurNode:Adjacent, Edges), | |
| 342 | member((CurNode,_,NextNode,DLConstraint), Adjacent), | |
| 343 | get_original_constraint(DLConstraint, Constraint), | |
| 344 | %nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl, | |
| 345 | %write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl, | |
| 346 | get_unsat_core_from_negative_cycle(Edges, [NextNode|T], SrcNode, [Constraint|Acc], UnsatCoreList). | |
| 347 | ||
| 348 | get_original_constraint(b(_,_,Info), Constraint) :- | |
| 349 | member(idl_origin(TConstraint), Info), | |
| 350 | !, | |
| 351 | Constraint = TConstraint. | |
| 352 | get_original_constraint(b(negation(b(_,_,Info)),_,_), Constraint) :- | |
| 353 | member(idl_origin(TConstraint), Info), | |
| 354 | !, | |
| 355 | Constraint = b(negation(TConstraint),pred,[]). | |
| 356 | get_original_constraint(DLConstraint, DLConstraint) :- | |
| 357 | is_idl_constraint(DLConstraint). | |
| 358 | ||
| 359 | %% get_unsat_core(-UnsatCore). | |
| 360 | % Return asserted unsat core or fail. | |
| 361 | get_unsat_core(UnsatCore) :- | |
| 362 | unsat_core(UnsatCore). | |
| 363 | ||
| 364 | %% possibly_shift_solution_for_zero(+TempBindings, -Bindings). | |
| 365 | % Constraints of the form x<=c are transformed to x-_zero<=c where _zero is an artificial variable | |
| 366 | % which is not part of the solution. If _zero is used, the resulting solution has to be shifted by -_zero for each variable | |
| 367 | % so that _zero=0 holds. | |
| 368 | possibly_shift_solution_for_zero(TempBindings, Bindings) :- | |
| 369 | \+ contains_zero, | |
| 370 | !, | |
| 371 | Bindings = TempBindings. | |
| 372 | possibly_shift_solution_for_zero(TempBindings, Bindings) :- | |
| 373 | select(binding('_zero',int(ZeroVal),_), TempBindings, Rest), | |
| 374 | ( ZeroVal == 0 | |
| 375 | -> Bindings = Rest | |
| 376 | ; shift_solution(ZeroVal, Rest, [], Bindings) | |
| 377 | ). | |
| 378 | ||
| 379 | %% shift_solution(+ZeroVal, +TempBindings, +Acc, -Shifted). | |
| 380 | shift_solution(_, [], Acc, Acc). | |
| 381 | shift_solution(ZeroVal, [binding(VarName,int(Value),_)|T], Acc, Shifted) :- | |
| 382 | NValue is Value - ZeroVal, | |
| 383 | number_to_atom(NValue, NValueAtom), | |
| 384 | shift_solution(ZeroVal, T, [binding(VarName,int(NValue),NValueAtom)|Acc], Shifted). | |
| 385 | ||
| 386 | number_to_atom(Number, Atom) :- | |
| 387 | number_codes(Number, Codes), | |
| 388 | atom_codes(Atom, Codes). | |
| 389 | ||
| 390 | register_constraints_from_conj_list(_, []). | |
| 391 | register_constraints_from_conj_list(GraphMut, [DLConstraint|T]) :- | |
| 392 | register_idl_constraint(GraphMut, DLConstraint), | |
| 393 | register_constraints_from_conj_list(GraphMut, T). | |
| 394 | ||
| 395 | register_idl_constraint(GraphMut, DLConstraint) :- | |
| 396 | ( DLConstraint = b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_), | |
| 397 | Pol = pos | |
| 398 | ; DLConstraint = b(negation(b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_)),pred,_), | |
| 399 | Pol = neg | |
| 400 | ), | |
| 401 | get_int_value(Constant, Value), | |
| 402 | get_int_var_name(Minuend, MinuendVar), | |
| 403 | get_int_var_name(Subtrahend, SubtrahendVar), | |
| 404 | register_node_for_var(GraphMut, MinuendVar), | |
| 405 | register_node_for_var(GraphMut, SubtrahendVar), | |
| 406 | add_edge_for_polarity(GraphMut, Pol, DLConstraint, MinuendVar, SubtrahendVar, Value). | |
| 407 | ||
| 408 | add_edge_for_polarity(GraphMut, pos, DLConstraint, MinuendVar, SubtrahendVar, Value) :- | |
| 409 | % edge (y,c,x) for x-y<=c | |
| 410 | add_edge(GraphMut, DLConstraint, SubtrahendVar, MinuendVar, Value), | |
| 411 | bt_asserta(constraint_store(SubtrahendVar,MinuendVar,DLConstraint)). | |
| 412 | add_edge_for_polarity(GraphMut, neg, DLConstraint, MinuendVar, SubtrahendVar, Value) :- | |
| 413 | % edge (x,-c-1,y) for not(x-y<=c) | |
| 414 | NValue is Value * -1 - 1, | |
| 415 | add_edge(GraphMut, DLConstraint, MinuendVar, SubtrahendVar, NValue), | |
| 416 | bt_asserta(constraint_store(MinuendVar,SubtrahendVar,DLConstraint)). | |
| 417 | ||
| 418 | /*print_graph(GraphMut) :- | |
| 419 | get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut), | |
| 420 | format("Graph:~nNodes: ~w~nEdges: ~w~nShortest Paths: ~w~n~n", [Nodes,Edges,SPs]).*/ | |
| 421 | ||
| 422 | %% add_edge(+GraphMut, +DLConstraint, +In, +Out, +Value). | |
| 423 | % Possibly replace edge since there can be only one edge between two nodes in integer difference logic. | |
| 424 | % For instance, x-y<=2 => x-y<=3. | |
| 425 | add_edge(GraphMut, DLConstraint, In, Out, Value) :- | |
| 426 | get_mutable(graph(Nodes,edges(Edges),SPs), GraphMut), | |
| 427 | add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges), | |
| 428 | update_mutable(graph(Nodes,edges(NewEdges),SPs), GraphMut). | |
| 429 | ||
| 430 | add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :- | |
| 431 | select(In:Adjacent, Edges, REdges), | |
| 432 | !, | |
| 433 | ( select((In,OldValue,Out,_), Adjacent, RAdjacent) | |
| 434 | -> ( Value < OldValue | |
| 435 | -> NewEdges = [In:[(In,Value,Out,DLConstraint)|RAdjacent]|REdges], | |
| 436 | register_negative_weight(Value) | |
| 437 | ; NewEdges = Edges | |
| 438 | ) | |
| 439 | ; NewEdges = [In:[(In,Value,Out,DLConstraint)|Adjacent]|REdges], | |
| 440 | register_negative_weight(Value) | |
| 441 | ). | |
| 442 | add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :- | |
| 443 | NewEdges = [In:[(In,Value,Out,DLConstraint)]|Edges], | |
| 444 | register_negative_weight(Value). | |
| 445 | ||
| 446 | %% assert_contains_zero. | |
| 447 | assert_contains_zero :- | |
| 448 | \+ contains_zero, | |
| 449 | !, | |
| 450 | bt_asserta(contains_zero). | |
| 451 | assert_contains_zero. | |
| 452 | ||
| 453 | %% register_negative_weight(+Value). | |
| 454 | register_negative_weight(Value) :- | |
| 455 | \+ negative_weight, | |
| 456 | Value < 0, | |
| 457 | !, | |
| 458 | bt_asserta(negative_weight). | |
| 459 | register_negative_weight(_). | |
| 460 | ||
| 461 | %% register_node_for_var(+GraphMut, +VarName). | |
| 462 | register_node_for_var(GraphMut, VarName) :- | |
| 463 | get_mutable(graph(nodes(Nodes),_,_), GraphMut), | |
| 464 | member(VarName, Nodes), | |
| 465 | !. | |
| 466 | register_node_for_var(GraphMut, VarName) :- | |
| 467 | ( VarName == '_zero' | |
| 468 | -> assert_contains_zero | |
| 469 | ; true | |
| 470 | ), | |
| 471 | get_mutable(graph(nodes(Nodes),Edges,shortest_paths(SPs)), GraphMut), | |
| 472 | update_mutable(graph(nodes([VarName|Nodes]),Edges,shortest_paths([(VarName,0)|SPs])), GraphMut). | |
| 473 | ||
| 474 | is_idl_constraint(Constraint) :- | |
| 475 | ( Constraint = b(less_equal(Sub,Constant),pred,_) | |
| 476 | ; Constraint = b(negation(b(less_equal(Sub,Constant),pred,_)),pred,_) | |
| 477 | ), | |
| 478 | Sub = b(minus(Id1,Id2),integer,_), | |
| 479 | get_int_value(Constant, _), | |
| 480 | Id1 = b(identifier(_),integer,_), | |
| 481 | Id2 = b(identifier(_),integer,_). | |
| 482 | ||
| 483 | %% get_int_var_name(+IdentifierAst, -VarName). | |
| 484 | get_int_var_name(b(identifier(VarName),integer,_), VarName). | |
| 485 | ||
| 486 | %% insertion_sort(+List, +Node, +DiffToOld, -Sorted) :- | |
| 487 | % Sort by largest change in distance. | |
| 488 | insertion_sort([], Node, Dist, [(Node,Dist)]). | |
| 489 | insertion_sort([(Node1,Dist1)|T], Node, Dist, Sorted) :- | |
| 490 | Dist1 < Dist, | |
| 491 | !, | |
| 492 | Sorted = [(Node,Dist),(Node1,Dist1)|T]. | |
| 493 | insertion_sort([(Node1,Dist1)|T], Node, Dist, [(Node1,Dist1)|NT]) :- | |
| 494 | insertion_sort(T, Node, Dist, NT). | |
| 495 | ||
| 496 | assert_distance(GraphMut, Node, NDNode, DiffToOld) :- | |
| 497 | get_mutable(graph(Nodes,Edges,shortest_paths(SPs)), GraphMut), | |
| 498 | select((Node,Old), SPs, Rest), | |
| 499 | NewSPs = [(Node,NDNode)|Rest], | |
| 500 | update_mutable(graph(Nodes,Edges,shortest_paths(NewSPs)), GraphMut), | |
| 501 | DiffToOld is Old - NDNode. | |
| 502 | ||
| 503 | assert_predecessor(Node, PreNode) :- | |
| 504 | bt_retract(predecessor(Node,_)), | |
| 505 | bt_asserta(predecessor(Node,PreNode)). | |
| 506 | assert_predecessor(Node, PreNode) :- | |
| 507 | \+ predecessor(Node,_), | |
| 508 | bt_asserta(predecessor(Node,PreNode)). | |
| 509 | ||
| 510 | bt_asserta(Term) :- | |
| 511 | asserta(Term); (retract(Term), fail). | |
| 512 | ||
| 513 | bt_retract(Assertion) :- | |
| 514 | ( retract(Assertion) | |
| 515 | -> ( true | |
| 516 | ; asserta(Assertion), | |
| 517 | fail | |
| 518 | ) | |
| 519 | ; fail | |
| 520 | ). | |
| 521 | ||
| 522 | % TO DO: are there more constraints? x:{1,3,7}? | |
| 523 | infer_constraints_for_idl_solver(MemberNat, [Constraint]) :- | |
| 524 | % x:NAT -> _zero-x <= 0 | |
| 525 | % x:NAT1 -> _zero-x <= -1 | |
| 526 | MemberNat = b(member(Id,Natural),pred,_), | |
| 527 | Id = b(identifier(_),integer,_), | |
| 528 | ( Natural = b(integer_set('NATURAL'),set(integer),_), | |
| 529 | Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(MemberNat)]) | |
| 530 | ; Natural = b(integer_set('NATURAL1'),set(integer),_), | |
| 531 | Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(-1),integer,[])),pred,[idl_origin(MemberNat)]) | |
| 532 | ). | |
| 533 | infer_constraints_for_idl_solver(MemberInterval, [LEQ1,LEQ2]) :- | |
| 534 | % x:min..max -> _zero-x<=-min & x<=max | |
| 535 | MemberInterval = b(member(Id,Interval),pred,_), | |
| 536 | Id = b(identifier(_),integer,_), | |
| 537 | Interval = b(interval(Min,Max),set(integer),_), | |
| 538 | Min = b(integer(MinVal),integer,MinInfo), | |
| 539 | Max = b(integer(_),integer,_), | |
| 540 | MinVal1 is MinVal * -1, | |
| 541 | LEQ1 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(MinVal1),integer,MinInfo)),pred,[idl_origin(MemberInterval)]), | |
| 542 | LEQ2 = b(less_equal(b(minus(Id,b(identifier('_zero'),integer,[])),integer,[]),Max),pred,[idl_origin(MemberInterval)]). | |
| 543 | infer_constraints_for_idl_solver(EqualCard, [Constraint]) :- | |
| 544 | % x=card(s) -> _zero-x<=0 | |
| 545 | % x=size(s) -> _zero-x<=0 | |
| 546 | ( EqualCard = b(equal(Id,CardOrSize),pred,_) | |
| 547 | ; EqualCard = b(equal(CardOrSize,Id),pred,_) | |
| 548 | ), | |
| 549 | Id = b(identifier(_),integer,_), | |
| 550 | ( CardOrSize = b(card(_),integer,_) | |
| 551 | ; CardOrSize = b(size(_),integer,_) | |
| 552 | ), | |
| 553 | Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(EqualCard)]). | |
| 554 | ||
| 555 | ||
| 556 | :- begin_tests(difference_logic_solver). | |
| 557 | ||
| 558 | test(simple_sat1, [nondet]) :- | |
| 559 | init_idl_solver(GraphMut), | |
| 560 | % a-c<=1 & c-b<=-3 | |
| 561 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 562 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])), | |
| 563 | !, | |
| 564 | get_solver_result(GraphMut, Res), | |
| 565 | ground(Res), | |
| 566 | Res = solution(Bindings), | |
| 567 | member(binding(a,int(-2),'-2'), Bindings), | |
| 568 | member(binding(b,int(0),'0'), Bindings), | |
| 569 | member(binding(c,int(-3),'-3'), Bindings), | |
| 570 | \+ get_unsat_core(_). | |
| 571 | ||
| 572 | test(simple_sat2, [nondet]) :- | |
| 573 | init_idl_solver(GraphMut), | |
| 574 | % a-c<=-1 & c-b<=3 | |
| 575 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 576 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])), | |
| 577 | !, | |
| 578 | get_solver_result(GraphMut, Res), | |
| 579 | ground(Res), | |
| 580 | Res = solution(Bindings), | |
| 581 | member(binding(a,int(-1),'-1'), Bindings), | |
| 582 | member(binding(b,int(0),'0'), Bindings), | |
| 583 | member(binding(c,int(0),'0'), Bindings), | |
| 584 | \+ get_unsat_core(_). | |
| 585 | ||
| 586 | test(simple_sat3, [nondet]) :- | |
| 587 | init_idl_solver(GraphMut), | |
| 588 | % a-c<=1 & c-b<=3 | |
| 589 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 590 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])), | |
| 591 | !, | |
| 592 | get_solver_result(GraphMut, Res), | |
| 593 | ground(Res), | |
| 594 | Res = solution(Bindings), | |
| 595 | member(binding(a,int(0),'0'), Bindings), | |
| 596 | member(binding(b,int(0),'0'), Bindings), | |
| 597 | member(binding(c,int(0),'0'), Bindings), | |
| 598 | \+ get_unsat_core(_). | |
| 599 | ||
| 600 | test(simple_sat4, [nondet]) :- | |
| 601 | init_idl_solver(GraphMut), | |
| 602 | % a-1<=1 & 3<=b & 2<=b-1 | |
| 603 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(integer(1),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 604 | register_constraint(GraphMut, b(less_equal(b(integer(3),integer,[]),b(identifier(b),integer,[])),pred,[])), | |
| 605 | register_constraint(GraphMut, b(less_equal(b(integer(2),integer,[]),b(minus(b(identifier(b),integer,[]),b(integer(1),integer,[])),integer,[])),pred,[])), | |
| 606 | !, | |
| 607 | get_solver_result(GraphMut, Res), | |
| 608 | ground(Res), | |
| 609 | Res = solution(Bindings), | |
| 610 | member(binding(a,int(2),'2'), Bindings), | |
| 611 | member(binding(b,int(3),'3'), Bindings), | |
| 612 | \+ get_unsat_core(_). | |
| 613 | ||
| 614 | test(simple_sat_introduce_zero, [nondet]) :- | |
| 615 | init_idl_solver(GraphMut), | |
| 616 | % a-b<=-1 & a<=-1 | |
| 617 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 618 | register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 619 | !, | |
| 620 | get_solver_result(GraphMut, Res), | |
| 621 | ground(Res), | |
| 622 | Res = solution(Bindings), | |
| 623 | member(binding(a,int(-1),'-1'), Bindings), | |
| 624 | member(binding(b,int(0),'0'), Bindings), | |
| 625 | \+ get_unsat_core(_). | |
| 626 | ||
| 627 | test(simple_sat_rewrite_equality, [nondet]) :- | |
| 628 | init_idl_solver(GraphMut), | |
| 629 | % a-b<=-1 & a=1 | |
| 630 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 631 | register_constraint(GraphMut, b(equal(b(identifier(a),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 632 | !, | |
| 633 | get_solver_result(GraphMut, Res), | |
| 634 | Res = solution(Bindings), | |
| 635 | member(binding(a,int(1),'1'), Bindings), | |
| 636 | member(binding(b,int(2),'2'), Bindings), | |
| 637 | \+ get_unsat_core(_). | |
| 638 | ||
| 639 | test(simple_sat_all_solutions_single_var, [nondet]) :- | |
| 640 | init_idl_solver(GraphMut), | |
| 641 | % all solutions for x>0 & x<5 | |
| 642 | register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])), | |
| 643 | register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])), | |
| 644 | !, | |
| 645 | findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults), | |
| 646 | SolverResults == [solution([binding(x,int(1),'1')]),solution([binding(x,int(2),'2')]),solution([binding(x,int(3),'3')]),solution([binding(x,int(4),'4')]),solution([binding(x,int(5),'5')]),solution([binding(x,int(6),'6')]),solution([binding(x,int(7),'7')]),solution([binding(x,int(8),'8')]),solution([binding(x,int(9),'9')])]. | |
| 647 | ||
| 648 | test(simple_sat_all_solutions_two_vars, [nondet]) :- | |
| 649 | init_idl_solver(GraphMut), | |
| 650 | % all solutions for x>0 & x<4 & y>0 & y<4 | |
| 651 | register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])), | |
| 652 | register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(4),integer,[])),pred,[])), | |
| 653 | register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])), | |
| 654 | register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(4),integer,[])),pred,[])), | |
| 655 | !, | |
| 656 | findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults), | |
| 657 | length(SolverResults, Length), | |
| 658 | Length == 9, | |
| 659 | SolverResults == [solution([binding(y,int(1),'1'),binding(x,int(1),'1')]),solution([binding(y,int(2),'2'),binding(x,int(2),'2')]),solution([binding(y,int(3),'3'),binding(x,int(3),'3')]),solution([binding(x,int(2),'2'),binding(y,int(3),'3')]),solution([binding(x,int(1),'1'),binding(y,int(3),'3')]),solution([binding(x,int(1),'1'),binding(y,int(2),'2')]),solution([binding(y,int(2),'2'),binding(x,int(3),'3')]),solution([binding(y,int(1),'1'),binding(x,int(2),'2')]),solution([binding(y,int(1),'1'),binding(x,int(3),'3')])]. | |
| 660 | ||
| 661 | test(simple_sat_all_solutions_two_vars_subtraction, [nondet]) :- | |
| 662 | init_idl_solver(GraphMut), | |
| 663 | % all solutions for x>0 & x<10 & y>0 & y<10 & x-y>5 | |
| 664 | register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])), | |
| 665 | register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])), | |
| 666 | register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])), | |
| 667 | register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(10),integer,[])),pred,[])), | |
| 668 | register_constraint(GraphMut, b(greater(b(minus(b(identifier(x),integer,[]),b(identifier(y),integer,[])),integer,[]),b(integer(5),integer,[])),pred,[])), | |
| 669 | !, | |
| 670 | findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults), | |
| 671 | length(SolverResults, Length), | |
| 672 | Length == 6, | |
| 673 | SolverResults == [solution([binding(y,int(1),'1'),binding(x,int(7),'7')]),solution([binding(y,int(2),'2'),binding(x,int(8),'8')]),solution([binding(y,int(3),'3'),binding(x,int(9),'9')]),solution([binding(y,int(2),'2'),binding(x,int(9),'9')]),solution([binding(y,int(1),'1'),binding(x,int(8),'8')]),solution([binding(y,int(1),'1'),binding(x,int(9),'9')])]. | |
| 674 | ||
| 675 | test(simple_unsat1, [nondet]) :- | |
| 676 | init_idl_solver(GraphMut), | |
| 677 | % a-c<=1 & c-b<=-3 & b-a<=1 | |
| 678 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 679 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])), | |
| 680 | \+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 681 | !, | |
| 682 | get_solver_result(GraphMut, Res), | |
| 683 | Res == contradiction_found, | |
| 684 | get_unsat_core(UnsatCore), | |
| 685 | UnsatCore = b(conjunct(b(conjunct(b(less_equal(b(minus(b(identifier(b),integer,_),b(identifier(a),integer,_)),integer,_),b(integer(1),integer,_)),pred,_),b(less_equal(b(minus(b(identifier(a),integer,_),b(identifier(c),integer,_)),integer,_),b(integer(1),integer,_)),pred,_)),pred,_),b(less_equal(b(minus(b(identifier(c),integer,_),b(identifier(b),integer,_)),integer,_),b(integer(-3),integer,_)),pred,_)),pred,_). | |
| 686 | ||
| 687 | test(simple_unsat2, [nondet]) :- | |
| 688 | init_idl_solver(GraphMut), | |
| 689 | % c-c<=1 & a-c<=1 & c-b<=-3 & b-a<=1 | |
| 690 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 691 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 692 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])), | |
| 693 | \+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 694 | !, | |
| 695 | get_solver_result(GraphMut, Res), | |
| 696 | Res == contradiction_found, | |
| 697 | get_unsat_core(UnsatCore), | |
| 698 | % c-c<=1 is not part of the unsat core | |
| 699 | UnsatCore = b(conjunct(b(conjunct(b(less_equal(b(minus(b(identifier(b),integer,_),b(identifier(a),integer,_)),integer,_),b(integer(1),integer,_)),pred,_),b(less_equal(b(minus(b(identifier(a),integer,_),b(identifier(c),integer,_)),integer,_),b(integer(1),integer,_)),pred,_)),pred,_),b(less_equal(b(minus(b(identifier(c),integer,_),b(identifier(b),integer,_)),integer,_),b(integer(-3),integer,_)),pred,_)),pred,_). | |
| 700 | ||
| 701 | test(simple_unsat_negation, [nondet]) :- | |
| 702 | init_idl_solver(GraphMut), | |
| 703 | % a-b<=-1 & a<=-1 & b<=10 & not(a<=-1) | |
| 704 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 705 | register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 706 | register_constraint(GraphMut, b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[])), | |
| 707 | \+ register_constraint(GraphMut, b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[])), | |
| 708 | !, | |
| 709 | get_solver_result(GraphMut, Res), | |
| 710 | Res = contradiction_found, | |
| 711 | get_unsat_core(UnsatCore), | |
| 712 | % not(a<=-1) & a<=-1 | |
| 713 | UnsatCore = b(conjunct(b(negation(b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_),b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_). | |
| 714 | ||
| 715 | test(simple_unsat_negation_rewrite_beforehand, [nondet]) :- | |
| 716 | init_idl_solver(GraphMut), | |
| 717 | % we receive the same unsat core containing the original constraints when rewriting constraints before registering them | |
| 718 | % a-b<=-1 & a<=-1 & b<=10 & not(a<=-1) | |
| 719 | C2 = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]), | |
| 720 | C3 = b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[]), | |
| 721 | C4 = b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[]), | |
| 722 | rewrite_to_idl(C2, C2IdlConjList), | |
| 723 | rewrite_to_idl(C3, C3IdlConjList), | |
| 724 | rewrite_to_idl(C4, C4IdlConjList), | |
| 725 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 726 | register_constraints(GraphMut, C2IdlConjList), | |
| 727 | register_constraints(GraphMut, C3IdlConjList), | |
| 728 | \+ register_constraints(GraphMut, C4IdlConjList), | |
| 729 | !, | |
| 730 | get_solver_result(GraphMut, Res), | |
| 731 | Res = contradiction_found, | |
| 732 | get_unsat_core(UnsatCore), | |
| 733 | % not(a<=-1) & a<=-1 | |
| 734 | UnsatCore = b(conjunct(b(negation(b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_),b(less_equal(b(identifier(a),integer,_),b(integer(-1),integer,_)),pred,_)),pred,_). | |
| 735 | ||
| 736 | :- end_tests(difference_logic_solver). | |
| 737 | ||
| 738 | :- begin_tests(dynamic_state). | |
| 739 | ||
| 740 | empty_graph_state(GraphMut) :- | |
| 741 | \+ negative_weight, | |
| 742 | \+ contains_zero, | |
| 743 | get_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut), | |
| 744 | \+ constraint_store(_,_,_). | |
| 745 | ||
| 746 | test(register_constraint_undone_on_bt1, []) :- | |
| 747 | init_idl_solver(GraphMut), | |
| 748 | empty_graph_state(GraphMut), | |
| 749 | Constraint = b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[]), | |
| 750 | ( register_constraint(GraphMut, Constraint), | |
| 751 | get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut), | |
| 752 | memberchk(a, Nodes), | |
| 753 | memberchk(b, Nodes), | |
| 754 | memberchk(b:[(b,1,a,_)], Edges), | |
| 755 | memberchk((a,0), SPs), | |
| 756 | memberchk((b,0), SPs), | |
| 757 | constraint_store(b,a,Constraint), | |
| 758 | \+ negative_weight, | |
| 759 | \+ contains_zero, | |
| 760 | fail | |
| 761 | ; empty_graph_state(GraphMut) | |
| 762 | ). | |
| 763 | ||
| 764 | test(register_constraint_undone_on_bt2, []) :- | |
| 765 | init_idl_solver(GraphMut), | |
| 766 | empty_graph_state(GraphMut), | |
| 767 | Constraint = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]), | |
| 768 | ( register_constraint(GraphMut, Constraint), | |
| 769 | get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut), | |
| 770 | memberchk(a, Nodes), | |
| 771 | memberchk('_zero', Nodes), | |
| 772 | memberchk('_zero':[('_zero',-1,a,_)], Edges), | |
| 773 | memberchk((a,-1), SPs), | |
| 774 | memberchk(('_zero',0), SPs), | |
| 775 | constraint_store('_zero',a,b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])), | |
| 776 | negative_weight, | |
| 777 | contains_zero, | |
| 778 | fail | |
| 779 | ; empty_graph_state(GraphMut) | |
| 780 | ). | |
| 781 | ||
| 782 | test(register_constraint_overwrite_old, [nondet]) :- | |
| 783 | init_idl_solver(GraphMut), | |
| 784 | empty_graph_state(GraphMut), | |
| 785 | % a-b<=2 is replaced by a-b<=1 | |
| 786 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])), | |
| 787 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 788 | get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut), | |
| 789 | memberchk('b':[('b',1,a,_)], Edges), | |
| 790 | memberchk((a,0), SPs), | |
| 791 | memberchk((b,0), SPs). | |
| 792 | ||
| 793 | test(register_constraint_overwrite_old_undone_on_bt, [nondet]) :- | |
| 794 | init_idl_solver(GraphMut), | |
| 795 | empty_graph_state(GraphMut), | |
| 796 | % a-b<=2 is replaced by a-b<=1 but effect is undone on backtracking | |
| 797 | register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])), | |
| 798 | ( register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])), | |
| 799 | fail | |
| 800 | ; get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut), | |
| 801 | memberchk('b':[('b',2,a,_)], Edges), | |
| 802 | memberchk((a,0), SPs), | |
| 803 | memberchk((b,0), SPs) | |
| 804 | ). | |
| 805 | ||
| 806 | :- end_tests(dynamic_state). |