difference_logic_solver

add_edge(GraphMut, DLConstraint, In, Out, Value) :-
    get_mutable(graph(Nodes,edges(Edges),SPs), GraphMut),
    add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges),
    update_mutable(graph(Nodes,edges(NewEdges),SPs), GraphMut).

add_edge_for_polarity(GraphMut, pos, DLConstraint, MinuendVar, SubtrahendVar, Value) :-
    % edge (y,c,x) for x-y<=c
    add_edge(GraphMut, DLConstraint, SubtrahendVar, MinuendVar, Value),
    bt_asserta(constraint_store(SubtrahendVar,MinuendVar,DLConstraint)).

add_edge_for_polarity(GraphMut, neg, DLConstraint, MinuendVar, SubtrahendVar, Value) :-
    % edge (x,-c-1,y) for not(x-y<=c)
    NValue is Value * -1 - 1,
    add_edge(GraphMut, DLConstraint, MinuendVar, SubtrahendVar, NValue),
    bt_asserta(constraint_store(MinuendVar,SubtrahendVar,DLConstraint)).

add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :-
    select(In:Adjacent, Edges, REdges),
    !,
    ( select((In,OldValue,Out,_), Adjacent, RAdjacent)
    -> ( Value < OldValue
    -> NewEdges = [In:[(In,Value,Out,DLConstraint)|RAdjacent]|REdges],
    register_negative_weight(Value)
    ; NewEdges = Edges
    )
    ; NewEdges = [In:[(In,Value,Out,DLConstraint)|Adjacent]|REdges],
    register_negative_weight(Value)
).

add_to_edges(Edges, DLConstraint, In, Out, Value, NewEdges) :-
    NewEdges = [In:[(In,Value,Out,DLConstraint)]|Edges],
    register_negative_weight(Value).

assert_contains_zero :-
    \+ contains_zero,
    !,
    bt_asserta(contains_zero).

assert_contains_zero.

assert_distance(GraphMut, Node, NDNode, DiffToOld) :-
    get_mutable(graph(Nodes,Edges,shortest_paths(SPs)), GraphMut),
    select((Node,Old), SPs, Rest),
    NewSPs = [(Node,NDNode)|Rest],
    update_mutable(graph(Nodes,Edges,shortest_paths(NewSPs)), GraphMut),
    DiffToOld is Old - NDNode.

assert_predecessor(Node, PreNode) :-
    bt_retract(predecessor(Node,_)),
    bt_asserta(predecessor(Node,PreNode)).

assert_predecessor(Node, PreNode) :-
    \+ predecessor(Node,_),
    bt_asserta(predecessor(Node,PreNode)).

bt_asserta(Term) :-
    asserta(Term); (retract(Term), fail).

bt_retract(Assertion) :-
    ( retract(Assertion)
    -> ( true
    ; asserta(Assertion),
    fail
    )
    ; fail
).

detect_negative_cycle_inc(GraphMut, Queue, In, Out, Weight, NegativeCycle) :-
    ( relax_edge_cond(GraphMut, In, Out, Weight, NDOut)
    -> relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld),
    insertion_sort(Queue, Out, DiffToOld, NQueue)
    ; NQueue = Queue
    ),
    detect_negative_cycle_inc(GraphMut, In, Out, NQueue, NegativeCycle).

detect_negative_cycle_inc(_, _, _, [], none).

detect_negative_cycle_inc(GraphMut, StartIn, StartOut, [(CurNode,_)|T], NegativeCycle) :-
    get_adjacent_edges(GraphMut, CurNode, Adjacent),
    detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, Adjacent, T, NQueue, TNegativeCycle),
    (TNegativeCycle \== none
    -> NegativeCycle = TNegativeCycle
    ; detect_negative_cycle_inc(GraphMut, StartIn, StartOut, NQueue, NegativeCycle)
).

detect_negative_cycle_inc_process_edges(_, _, _, [], Queue, Queue, none).

detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, [(In,Weight,Out,_)|T], Queue, NQueue, NegativeCycle) :-
    ( relax_edge_cond(GraphMut, In, Out, Weight, NDOut)
    -> ( (In == StartIn, Out == StartOut)
    -> get_negative_cycle_from_predecessors(Out, NegativeCycle)
    ; relax_node_distance(GraphMut, In, Out, NDOut, DiffToOld),
    insertion_sort(Queue, Out, DiffToOld, TQueue),
    detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, TQueue, NQueue, NegativeCycle)
    )
    ; detect_negative_cycle_inc_process_edges(GraphMut, StartIn, StartOut, T, Queue, NQueue, NegativeCycle)
).

empty_graph_state(GraphMut) :-
    \+ negative_weight,
    \+ contains_zero,
    get_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut),
    \+ constraint_store(_,_,_).

exclude_solution_bt(GraphMut, [binding(VarName,int(Val),_)|T]) :-
    % register inequality constraint VarName /= Val with choicepoint since rewriting yields a disjunction
    % i.e., x/=c -> x-_zero<=c-1 or _zero-x<=-c-1
    ( exclude_solution_from_binding(GraphMut, VarName, Val)
    ; remove_unsat_core,
    Val1 is Val * -1,
    % equality
    LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]),
    LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
    register_constraints(GraphMut, [LEQ1,LEQ2]),
    exclude_solution_bt(GraphMut, T)
).

exclude_solution_from_binding(GraphMut, VarName, Val) :-
    DisjVal1 is Val - 1,
    DisjVal2 is Val * -1 - 1,
    VarId = b(identifier(VarName),integer,[]),
    ZeroId = b(identifier('_zero'),integer,[]),
    Disj1 = b(less_equal(b(minus(VarId,ZeroId),integer,[]),b(integer(DisjVal1),integer,[])),pred,[]),
    Disj2 = b(less_equal(b(minus(ZeroId,VarId),integer,[]),b(integer(DisjVal2),integer,[])),pred,[]),
    ( remove_unsat_core,
    register_constraint(GraphMut, Disj1)
    ; remove_unsat_core,
    register_constraint(GraphMut, Disj2)
).

get_adjacent_edges(GraphMut, Node, Adjacent) :-
    get_mutable(graph(_,edges(Edges),_), GraphMut),
    memberchk(Node:TAdjacent, Edges),
    !,
    Adjacent = TAdjacent.

get_adjacent_edges(_, _, []).

get_all_solutions_on_bt(GraphMut, SolverResult) :-
    % TO DO: randomized enumeration order, log upper and lower bounded vars?
    get_solver_result(GraphMut, TSolverResult),
    TSolverResult = solution(Bindings),
    ( SolverResult = TSolverResult
    ; exclude_solution_bt(GraphMut, Bindings),
    get_all_solutions_on_bt(GraphMut, SolverResult)
).

get_edge_from_dl_constraint(b(less_equal(Sub,Constant),pred,_), In, Out, Weight) :-
    % edge (y,c,x) for x-y<=c
    get_id_names_from_idl_minus(Sub, Out, In),
    get_int_value(Constant, Weight).

get_edge_from_dl_constraint(b(negation(Constraint),pred,_), In, Out, Weight) :-
    % edge (x,-c-1,y) for not(x-y<=c)
    Constraint = b(less_equal(Sub,Constant),pred,_),
    get_id_names_from_idl_minus(Sub, In, Out),
    get_int_value(Constant, TWeight),
    Weight is TWeight * -1 - 1.

get_id_names_from_idl_minus(b(minus(Id1,Id2),integer,_), In, Out) :-
    Id1 = b(identifier(In),integer,_),
    Id2 = b(identifier(Out),integer,_).

get_int_var_name(b(identifier(VarName),integer,_), VarName).

get_negative_cycle_from_predecessors(Out, NegativeCycle) :-
    get_negative_cycle_from_predecessors(Out, Out, [], NegativeCycle).

get_negative_cycle_from_predecessors(Start, Start, Acc, Acc) :-
    Acc \== [].

get_negative_cycle_from_predecessors(Start, CurNode, Acc, NegativeCycle) :-
    retract(predecessor(CurNode, PreNode)),
    get_negative_cycle_from_predecessors(Start, PreNode, [PreNode|Acc], NegativeCycle).

get_original_constraint(b(_,_,Info), Constraint) :-
    member(idl_origin(TConstraint), Info),
    !,
    Constraint = TConstraint.

get_original_constraint(b(negation(b(_,_,Info)),_,_), Constraint) :-
    member(idl_origin(TConstraint), Info),
    !,
    Constraint = b(negation(TConstraint),pred,[]).

get_original_constraint(DLConstraint, DLConstraint) :-
    is_idl_constraint(DLConstraint).

get_registered_vars(GraphMut, Vars) :-
    get_mutable(graph(nodes(Vars),_,_), GraphMut).

get_solver_result(_, SolverResult) :-
    unsat_core(_),
    !,
    SolverResult = contradiction_found.

get_solver_result(GraphMut, SolverResult) :-
    get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut),
    shortest_paths_to_bindings(SPs, [], TempBindings), % TO DO: shift at the same time?
    ground(TempBindings),
    possibly_shift_solution_for_zero(TempBindings, Bindings),!,
    SolverResult = solution(Bindings).

get_unsat_core(UnsatCore) :-
    unsat_core(UnsatCore).

get_unsat_core_from_negative_cycle(GraphMut, [SrcNode|T], UnsatCore) :-
    get_mutable(graph(_,edges(Edges),_), GraphMut),
    get_unsat_core_from_negative_cycle(Edges, [SrcNode|T], SrcNode, [], UnsatCoreList),
    conjunct_predicates(UnsatCoreList, UnsatCore), !.

get_unsat_core_from_negative_cycle(Edges, [CurNode], SrcNode, Acc, NewAcc) :-
    !,
    member(CurNode:Adjacent, Edges),
    member((CurNode,_,SrcNode,DLConstraint), Adjacent),
    get_original_constraint(DLConstraint, Constraint),
    %nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl,
    %write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl,
    NewAcc = [Constraint|Acc].

get_unsat_core_from_negative_cycle(Edges, [CurNode,NextNode|T], SrcNode, Acc, UnsatCoreList) :-
    member(CurNode:Adjacent, Edges),
    member((CurNode,_,NextNode,DLConstraint), Adjacent),
    get_original_constraint(DLConstraint, Constraint),
    %nl,write('Constraint: '), nl, translate:print_bexpr(DLConstraint),nl,
    %write('Original Constraint: '), nl, translate:print_bexpr(Constraint),nl,
    get_unsat_core_from_negative_cycle(Edges, [NextNode|T], SrcNode, [Constraint|Acc], UnsatCoreList).

infer_constraints_for_idl_solver(MemberNat, [Constraint]) :-
    % x:NAT -> _zero-x <= 0
    % x:NAT1 -> _zero-x <= -1
    MemberNat = b(member(Id,Natural),pred,_),
    Id = b(identifier(_),integer,_),
    ( Natural = b(integer_set('NATURAL'),set(integer),_),
    Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(MemberNat)])
    ; Natural = b(integer_set('NATURAL1'),set(integer),_),
    Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),Id),integer,[]),b(integer(-1),integer,[])),pred,[idl_origin(MemberNat)])
).

infer_constraints_for_idl_solver(MemberInterval, [LEQ1,LEQ2]) :-
    % x:min..max -> _zero-x<=-min & x<=max
    MemberInterval = b(member(Id,Interval),pred,_),
    Id = b(identifier(_),integer,_),
    Interval = b(interval(Min,Max),set(integer),_),
    Min = b(integer(MinVal),integer,MinInfo),
    Max = b(integer(_),integer,_),
    MinVal1 is MinVal * -1,
    LEQ1 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(MinVal1),integer,MinInfo)),pred,[idl_origin(MemberInterval)]),
    LEQ2 = b(less_equal(b(minus(Id,b(identifier('_zero'),integer,[])),integer,[]),Max),pred,[idl_origin(MemberInterval)]).

infer_constraints_for_idl_solver(EqualCard, [Constraint]) :-
    % x=card(s) -> _zero-x<=0
    % x=size(s) -> _zero-x<=0
    ( EqualCard = b(equal(Id,CardOrSize),pred,_)
    ; EqualCard = b(equal(CardOrSize,Id),pred,_)
    ),
    Id = b(identifier(_),integer,_),
    ( CardOrSize = b(card(_),integer,_)
    ; CardOrSize = b(size(_),integer,_)
    ),
    Constraint = b(less_equal(b(minus(b(identifier('_zero'),integer,[]), Id),integer,[]),b(integer(0),integer,[])),pred,[idl_origin(EqualCard)]).

init_idl_solver(GraphMut) :-
    create_mutable(graph(nodes([]),edges([]),shortest_paths([])), GraphMut),
    set_preference(normalize_ast, true),
    retractall(predecessor(_,_)),
    retractall(unsat_core(_)),
    retractall(constraint_store(_,_,_)),
    retractall(negative_weight),
    retractall(contains_zero).

insertion_sort([], Node, Dist, [(Node,Dist)]).

insertion_sort([(Node1,Dist1)|T], Node, Dist, Sorted) :-
    Dist1 < Dist,
    !,
    Sorted = [(Node,Dist),(Node1,Dist1)|T].

insertion_sort([(Node1,Dist1)|T], Node, Dist, [(Node1,Dist1)|NT]) :-
    insertion_sort(T, Node, Dist, NT).

is_idl_constraint(Constraint) :-
    ( Constraint = b(less_equal(Sub,Constant),pred,_)
    ; Constraint = b(negation(b(less_equal(Sub,Constant),pred,_)),pred,_)
    ),
    Sub = b(minus(Id1,Id2),integer,_),
    get_int_value(Constant, _),
    Id1 = b(identifier(_),integer,_),
    Id2 = b(identifier(_),integer,_).

negate_dl_constraint(b(equal(A,B),pred,Info), NegDL) :-
    !,
    NegDL = b(not_equal(A,B),pred,Info).

negate_dl_constraint(b(not_equal(A,B),pred,Info), NegDL) :-
    !,
    NegDL = b(equal(A,B),pred,Info).

negate_dl_constraint(b(negation(Constraint),pred,[]), Constraint).

negate_dl_constraint(Constraint, b(negation(Constraint),pred,[])).

number_to_atom(Number, Atom) :-
    number_codes(Number, Codes),
    atom_codes(Atom, Codes).

possibly_shift_solution_for_zero(TempBindings, Bindings) :-
    \+ contains_zero,
    !,
    Bindings = TempBindings.

possibly_shift_solution_for_zero(TempBindings, Bindings) :-
    select(binding('_zero',int(ZeroVal),_), TempBindings, Rest),
    ( ZeroVal == 0
    -> Bindings = Rest
    ; shift_solution(ZeroVal, Rest, [], Bindings)
).

register_constraint(GraphMut, Constraint) :-
    %write('Register Constraint..'),nl,
    %translate:print_bexpr(Constraint),nl,
    ( is_idl_constraint(Constraint)
    -> register_idl_constraint(GraphMut, Constraint),
    solve_incremental_constraint(GraphMut, Constraint)
    ; rewrite_to_idl(Constraint, DLConstraints),
    register_constraints_from_conj_list(GraphMut, DLConstraints),
    solve_incremental_list(GraphMut, DLConstraints)
).

register_constraints(_, []).

register_constraints(GraphMut, [Constraint|T]) :-
    register_constraint(GraphMut, Constraint),
    register_constraints(GraphMut, T).

register_constraints_from_conj_list(_, []).

register_constraints_from_conj_list(GraphMut, [DLConstraint|T]) :-
    register_idl_constraint(GraphMut, DLConstraint),
    register_constraints_from_conj_list(GraphMut, T).

register_idl_constraint(GraphMut, DLConstraint) :-
    ( DLConstraint = b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_),
    Pol = pos
    ; DLConstraint = b(negation(b(less_equal(b(minus(Minuend,Subtrahend),integer,_),Constant),pred,_)),pred,_),
    Pol = neg
    ),
    get_int_value(Constant, Value),
    get_int_var_name(Minuend, MinuendVar),
    get_int_var_name(Subtrahend, SubtrahendVar),
    register_node_for_var(GraphMut, MinuendVar),
    register_node_for_var(GraphMut, SubtrahendVar),
    add_edge_for_polarity(GraphMut, Pol, DLConstraint, MinuendVar, SubtrahendVar, Value).

register_negative_weight(Value) :-
    \+ negative_weight,
    Value < 0,
    !,
    bt_asserta(negative_weight).

register_negative_weight(_).

register_node_for_var(GraphMut, VarName) :-
    get_mutable(graph(nodes(Nodes),_,_), GraphMut),
    member(VarName, Nodes),
    !.

register_node_for_var(GraphMut, VarName) :-
    ( VarName == '_zero'
    -> assert_contains_zero
    ; true
    ),
    get_mutable(graph(nodes(Nodes),Edges,shortest_paths(SPs)), GraphMut),
    update_mutable(graph(nodes([VarName|Nodes]),Edges,shortest_paths([(VarName,0)|SPs])), GraphMut).

relax_edge_cond(GraphMut, In, Out, Weight, ND) :-
    get_mutable(graph(_,_,shortest_paths(SPs)), GraphMut),
    member((In,DIn), SPs),
    member((Out,DOut), SPs),
    ND is DIn + Weight,
    ND < DOut.

relax_node_distance(GraphMut, In, Out, ND, DiffToOld) :-
    assert_distance(GraphMut, Out, ND, DiffToOld),
    assert_predecessor(Out, In).

remove_unsat_core :-
    retract(unsat_core(_)),
    !.

remove_unsat_core.

shift_solution(_, [], Acc, Acc).

shift_solution(ZeroVal, [binding(VarName,int(Value),_)|T], Acc, Shifted) :-
    NValue is Value - ZeroVal,
    number_to_atom(NValue, NValueAtom),
    shift_solution(ZeroVal, T, [binding(VarName,int(NValue),NValueAtom)|Acc], Shifted).

shortest_paths_to_bindings([], Acc, Acc).

shortest_paths_to_bindings([(VarName,Val)|T], Acc, Bindings) :-
    number_to_atom(Val, ValAtom),
    shortest_paths_to_bindings(T, [binding(VarName,int(Val),ValAtom)|Acc], Bindings).

solve_idl_conj(Pred, Result) :-
    init_idl_solver(GraphMut),
    conjunction_to_list(Pred, ConjList),
    ( register_constraints(GraphMut, ConjList),
    !,
    get_solver_result(GraphMut, Result)
    ; get_solver_result(GraphMut, TResult),
    TResult == contradiction_found,
    !,
    get_unsat_core(Core),
    Result = contradiction_found(Core)
    ; Result = no_solution_found(no_idl_constraint)
).

solve_incremental(_, _, _, _) :-
    % no negative cycle without a negative weight
    \+ negative_weight.

solve_incremental(GraphMut, In, Out, Weight) :-
    negative_weight,
    detect_negative_cycle_inc(GraphMut, [], In, Out, Weight, NegativeCycle),
    ( NegativeCycle == none
    -> % shortest paths stored in dis/2 are a solution
    true
    ; get_unsat_core_from_negative_cycle(GraphMut, NegativeCycle, UnsatCore),
    %nl, write('Unsat Core: '), nl,translate:print_bexpr(UnsatCore),nl,
    %writeq(UnsatCore),nl,
    asserta(unsat_core(UnsatCore)),
    fail
).

solve_incremental_constraint(GraphMut, DLConstraint) :-
    get_edge_from_dl_constraint(DLConstraint, In, Out, Weight),
    solve_incremental(GraphMut, In, Out, Weight).

solve_incremental_list(_, []).

solve_incremental_list(GraphMut, [DLConstraint|T]) :-
    solve_incremental_constraint(GraphMut, DLConstraint),
    solve_incremental_list(GraphMut, T).

test(simple_sat1, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-c<=1 & c-b<=-3
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    ground(Res),
    Res = solution(Bindings),
    member(binding(a,int(-2),'-2'), Bindings),
    member(binding(b,int(0),'0'), Bindings),
    member(binding(c,int(-3),'-3'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat2, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-c<=-1 & c-b<=3
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    ground(Res),
    Res = solution(Bindings),
    member(binding(a,int(-1),'-1'), Bindings),
    member(binding(b,int(0),'0'), Bindings),
    member(binding(c,int(0),'0'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat3, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-c<=1 & c-b<=3
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(3),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    ground(Res),
    Res = solution(Bindings),
    member(binding(a,int(0),'0'), Bindings),
    member(binding(b,int(0),'0'), Bindings),
    member(binding(c,int(0),'0'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat4, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-1<=1 & 3<=b & 2<=b-1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(integer(1),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(integer(3),integer,[]),b(identifier(b),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(integer(2),integer,[]),b(minus(b(identifier(b),integer,[]),b(integer(1),integer,[])),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    ground(Res),
    Res = solution(Bindings),
    member(binding(a,int(2),'2'), Bindings),
    member(binding(b,int(3),'3'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat_introduce_zero, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-b<=-1 & a<=-1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    ground(Res),
    Res = solution(Bindings),
    member(binding(a,int(-1),'-1'), Bindings),
    member(binding(b,int(0),'0'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat_rewrite_equality, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-b<=-1 & a=1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(equal(b(identifier(a),integer,[]),b(integer(1),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    Res = solution(Bindings),
    member(binding(a,int(1),'1'), Bindings),
    member(binding(b,int(2),'2'), Bindings),
    \+ get_unsat_core(_).

test(simple_sat_all_solutions_single_var, [nondet]) :-
    init_idl_solver(GraphMut),
    % all solutions for x>0 & x<5
    register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])),
    !,
    findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
    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')])].

test(simple_sat_all_solutions_two_vars, [nondet]) :-
    init_idl_solver(GraphMut),
    % all solutions for x>0 & x<4 & y>0 & y<4
    register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(4),integer,[])),pred,[])),
    register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(4),integer,[])),pred,[])),
    !,
    findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
    length(SolverResults, Length),
    Length == 9,
    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')])].

test(simple_sat_all_solutions_two_vars_subtraction, [nondet]) :-
    init_idl_solver(GraphMut),
    % all solutions for x>0 & x<10 & y>0 & y<10 & x-y>5
    register_constraint(GraphMut, b(greater(b(identifier(x),integer,[]),b(integer(0),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less(b(identifier(x),integer,[]),b(integer(10),integer,[])),pred,[])),
    register_constraint(GraphMut, b(greater(b(identifier(y),integer,[]),b(integer(0),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less(b(identifier(y),integer,[]),b(integer(10),integer,[])),pred,[])),
    register_constraint(GraphMut, b(greater(b(minus(b(identifier(x),integer,[]),b(identifier(y),integer,[])),integer,[]),b(integer(5),integer,[])),pred,[])),
    !,
    findall(Res, get_all_solutions_on_bt(GraphMut, Res), SolverResults),
    length(SolverResults, Length),
    Length == 6,
    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')])].

test(simple_unsat1, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-c<=1 & c-b<=-3 & b-a<=1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
    \+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    Res == contradiction_found,
    get_unsat_core(UnsatCore),
    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,_).

test(simple_unsat2, [nondet]) :-
    init_idl_solver(GraphMut),
    % c-c<=1 & a-c<=1 & c-b<=-3 & b-a<=1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(c),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(c),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-3),integer,[])),pred,[])),
    \+ register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(b),integer,[]),b(identifier(a),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    Res == contradiction_found,
    get_unsat_core(UnsatCore),
    % c-c<=1 is not part of the unsat core
    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,_).

test(simple_unsat_negation, [nondet]) :-
    init_idl_solver(GraphMut),
    % a-b<=-1 & a<=-1 & b<=10 & not(a<=-1)
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[])),
    \+ register_constraint(GraphMut, b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[])),
    !,
    get_solver_result(GraphMut, Res),
    Res = contradiction_found,
    get_unsat_core(UnsatCore),
    % not(a<=-1) & a<=-1
    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,_).

test(simple_unsat_negation_rewrite_beforehand, [nondet]) :-
    init_idl_solver(GraphMut),
    % we receive the same unsat core containing the original constraints when rewriting constraints before registering them
    % a-b<=-1 & a<=-1 & b<=10 & not(a<=-1)
    C2 = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]),
    C3 = b(less_equal(b(identifier(b),integer,[]),b(integer(10),integer,[])),pred,[]),
    C4 = b(negation(b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[])),pred,[]),
    rewrite_to_idl(C2, C2IdlConjList),
    rewrite_to_idl(C3, C3IdlConjList),
    rewrite_to_idl(C4, C4IdlConjList),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    register_constraints(GraphMut, C2IdlConjList),
    register_constraints(GraphMut, C3IdlConjList),
    \+ register_constraints(GraphMut, C4IdlConjList),
    !,
    get_solver_result(GraphMut, Res),
    Res = contradiction_found,
    get_unsat_core(UnsatCore),
    % not(a<=-1) & a<=-1
    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,_).

test(register_constraint_undone_on_bt1, []) :-
    init_idl_solver(GraphMut),
    empty_graph_state(GraphMut),
    Constraint = b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[]),
    ( register_constraint(GraphMut, Constraint),
    get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut),
    memberchk(a, Nodes),
    memberchk(b, Nodes),
    memberchk(b:[(b,1,a,_)], Edges),
    memberchk((a,0), SPs),
    memberchk((b,0), SPs),
    constraint_store(b,a,Constraint),
    \+ negative_weight,
    \+ contains_zero,
    fail
    ; empty_graph_state(GraphMut)
).

test(register_constraint_undone_on_bt2, []) :-
    init_idl_solver(GraphMut),
    empty_graph_state(GraphMut),
    Constraint = b(less_equal(b(identifier(a),integer,[]),b(integer(-1),integer,[])),pred,[]),
    ( register_constraint(GraphMut, Constraint),
    get_mutable(graph(nodes(Nodes),edges(Edges),shortest_paths(SPs)), GraphMut),
    memberchk(a, Nodes),
    memberchk('_zero', Nodes),
    memberchk('_zero':[('_zero',-1,a,_)], Edges),
    memberchk((a,-1), SPs),
    memberchk(('_zero',0), SPs),
    constraint_store('_zero',a,b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(-1),integer,[])),pred,[])),
    negative_weight,
    contains_zero,
    fail
    ; empty_graph_state(GraphMut)
).

test(register_constraint_overwrite_old, [nondet]) :-
    init_idl_solver(GraphMut),
    empty_graph_state(GraphMut),
    % a-b<=2 is replaced by a-b<=1
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])),
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut),
    memberchk('b':[('b',1,a,_)], Edges),
    memberchk((a,0), SPs),
    memberchk((b,0), SPs).

test(register_constraint_overwrite_old_undone_on_bt, [nondet]) :-
    init_idl_solver(GraphMut),
    empty_graph_state(GraphMut),
    % a-b<=2 is replaced by a-b<=1 but effect is undone on backtracking
    register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(2),integer,[])),pred,[])),
    ( register_constraint(GraphMut, b(less_equal(b(minus(b(identifier(a),integer,[]),b(identifier(b),integer,[])),integer,[]),b(integer(1),integer,[])),pred,[])),
    fail
    ; get_mutable(graph(nodes(_),edges(Edges),shortest_paths(SPs)), GraphMut),
    memberchk('b':[('b',2,a,_)], Edges),
    memberchk((a,0), SPs),
    memberchk((b,0), SPs)
).

try_candidate_bounds(GraphMut, CandidateTuples, SolverResult) :-
    try_candidate_bounds(GraphMut, none, CandidateTuples, Diff-Diff, SolverResult).

try_candidate_bounds(GraphMut, Solution, [], L-Diff, SolverResult) :-
    Diff = [],
    L \== [],
    try_candidate_bounds(GraphMut, Solution, L, NDiff-NDiff, SolverResult).

try_candidate_bounds(GraphMut, Solution, [(_,[])|T], L-Diff, SolverResult) :-
    try_candidate_bounds(GraphMut, Solution, T, L-Diff, SolverResult).

try_candidate_bounds(GraphMut, none, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
    % x=val
    LEQ1 = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val),integer,[])),pred,[]),
    NVal is Val * -1,
    LEQ2 = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(NVal),integer,[])),pred,[]),
    remove_unsat_core,
    register_constraints(GraphMut, [LEQ1,LEQ2]),
    get_solver_result(GraphMut, TSolverResult),
    TSolverResult = solution(_),
    ( SolverResult = TSolverResult
    ; Diff = [(VarName,TVals)|NDiff],
    try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
).

try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
    ( Solution == none
    ; ground(Solution),
    Solution = solution(Bindings),
    member(binding(VarName,int(OldVal),_), Bindings),
    Val < OldVal
    ),
    Val1 is Val - 1,
    % x
    LEQ = b(less_equal(b(minus(b(identifier(VarName),integer,[]),b(identifier('_zero'),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
    remove_unsat_core,
    register_constraint(GraphMut, LEQ),
    get_solver_result(GraphMut, TSolverResult),
    TSolverResult = solution(_),
    ( SolverResult = TSolverResult
    ; Diff = [(VarName,TVals)|NDiff],
    try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
).

try_candidate_bounds(GraphMut, Solution, [(VarName,[Val|TVals])|T], L-Diff, SolverResult) :-
    ( Solution == none
    ; ground(Solution),
    Solution = solution(Bindings),
    member(binding(VarName,int(OldVal),_), Bindings),
    Val > OldVal
    ),
    Val1 is Val * -1 - 1,
    % x>val
    LEQ = b(less_equal(b(minus(b(identifier('_zero'),integer,[]),b(identifier(VarName),integer,[])),integer,[]),b(integer(Val1),integer,[])),pred,[]),
    remove_unsat_core,
    register_constraint(GraphMut, LEQ),
    get_solver_result(GraphMut, TSolverResult),
    TSolverResult = solution(_),
    ( SolverResult = TSolverResult
    ; Diff = [(VarName,TVals)|NDiff],
    try_candidate_bounds(GraphMut, TSolverResult, T, L-NDiff, SolverResult)
).

try_candidate_bounds(GraphMut, Solution, [(VarName,[_|TVals])|T], L-Diff, SolverResult) :-
    Diff = [(VarName,TVals)|NDiff],
    try_candidate_bounds(GraphMut, Solution, T, L-NDiff, SolverResult).