ast_to_difference_logic

add_original_constraint_to_info(_, [], []).

add_original_constraint_to_info(Constraint, [DLConstraint|T], [NDLConstraint|NT]) :-
    DLConstraint = b(Node,Type,Info),
    NDLConstraint = b(Node,Type,[idl_origin(Constraint)|Info]),
    add_original_constraint_to_info(Constraint, T, NT).

get_args_of_add_or_minus_to_addition(b(add(Id,Constant),integer,_), Id, Constant) :-
    Id = b(identifier(_),integer,_),
    get_int_value(Constant, _).

get_args_of_add_or_minus_to_addition(b(minus(Id,Constant),integer,_), Id, b(integer(NCVal),integer,[])) :-
    % x-c -> x+-c
    Id = b(identifier(_),integer,_),
    get_int_value(Constant, CVal),
    NCVal is CVal * -1.

get_int_value(b(integer(Value),integer,_), Value).

get_int_value(b(value(int(Value)),integer,_), Value).

is_idl_candidate(negation(Pred)) :-
    Pred = b(Node,_,_),
    is_idl_candidate(Node).

is_idl_candidate(less(_,_)).

is_idl_candidate(less_equal(_,_)).

is_idl_candidate(greater(_,_)).

is_idl_candidate(greater_equal(_,_)).

is_idl_candidate(equal(_,_)).

is_idl_candidate(not_equal(_,_)).

remove_idl_origin_from_info(b(Node,Type,Info), NewNode) :-
    select(idl_origin(_), Info, NInfo),
    !,
    NewNode = b(Node,Type,NInfo).

remove_idl_origin_from_info(Ast, Ast).

remove_zero_var(b(less_equal(Sub,Cst),pred,Info), b(less_equal(NSub,Cst),pred,Info)) :-
    Sub = b(minus(_,_),integer,_),
    remove_zero_var_from_sub(Sub, NSub).

remove_zero_var(b(negation(Term),pred,Info), New) :-
    !,
    remove_zero_var(Term, NewTerm),
    New = b(negation(NewTerm),pred,Info).

remove_zero_var(b(conjunct(C1,C2),pred,Info), Out) :-
    !,
    remove_zero_var(C1, NC1),
    remove_zero_var(C2, NC2),
    Out = b(conjunct(NC1,NC2),pred,Info).

remove_zero_var(b(disjunct(C1,C2),pred,Info), Out) :-
    !,
    remove_zero_var(C1, NC1),
    remove_zero_var(C2, NC2),
    Out = b(disjunct(NC1,NC2),pred,Info).

remove_zero_var(Term, Term).

remove_zero_var_from_sub(b(minus(b(identifier('_zero'),integer,_),Rhs),integer,Info), NSub) :-
    !,
    NSub = b(unary_minus(Rhs),integer,Info).

remove_zero_var_from_sub(b(minus(Lhs, b(identifier('_zero'),integer,_)),integer,_), NSub) :-
    !,
    NSub = Lhs.

remove_zero_var_from_sub(Sub, Sub).

rewrite_inequality_to_idl_disj_no_zero(Inequality, DLConstraint) :-
    ( Inequality = b(not_equal(Lhs,Rhs),pred,ConjInfo)
    ; Inequality = b(negation(b(equal(Lhs,Rhs),pred,ConjInfo)),pred,[])
    ),
    rewrite_to_idl_pos(b(equal(Lhs,Rhs),pred,ConjInfo), ConjList),!,
    ConjList = [TArg1,TArg2],
    remove_zero_var(TArg1, Arg1),
    remove_zero_var(TArg2, Arg2),
    NArg1 = b(negation(Arg1),pred,[]),
    NArg2 = b(negation(Arg2),pred,[]),
    DLConstraint = b(disjunct(NArg1,NArg2),pred,[idl_origin(Inequality)]).

rewrite_to_difference(Id, Diff) :-
    % x -> x-_zero
    Id = b(identifier(_),integer,_),
    !,
    Diff = b(minus(Id,b(identifier('_zero'),integer,[])),integer,[]).

rewrite_to_difference(UId, Diff) :-
    % -x -> _zero-x
    UId = b(unary_minus(b(identifier(IdName),integer,IdInfo)),integer,_),
    !,
    Diff = b(minus(b(identifier('_zero'),integer,[]),b(identifier(IdName),integer,IdInfo)),integer,[]).

rewrite_to_difference(Add, Diff) :-
    % x+-y -> x-y
    Add = b(add(b(identifier(V1),integer,Info1),b(unary_minus(Id2),integer,_)),integer,InfoAdd),
    Id2 = b(identifier(_),integer,_),
    Diff = b(minus(b(identifier(V1),integer,Info1),Id2),integer,InfoAdd).

rewrite_to_difference(Diff, Diff) :-
    % difference of positive integer ids
    Diff = b(minus(b(identifier(_),integer,_),b(identifier(_),integer,_)),_,_).

rewrite_to_idl(Constraint, ConjList) :-
    Constraint = b(Node,pred,_),
    is_idl_candidate(Node),
    temporary_set_preference(normalize_ast_sort_commutative, true),
    clean_up_pred(Constraint, _, Clean),
    reset_temporary_preference(normalize_ast_sort_commutative),
    rewrite_to_idl_clean(Clean, TConjList),
    add_original_constraint_to_info(Constraint, TConjList, ConjList).

rewrite_to_idl_clean(b(negation(Inequality),pred,_), Out) :-
    % not(x/=y) -> x=y
    Inequality = b(not_equal(Lhs,Rhs),pred,EqInfo),
    !,
    Equality = b(equal(Lhs,Rhs),pred,EqInfo),
    rewrite_to_idl_pos(Equality, Out).

rewrite_to_idl_clean(b(negation(Constraint),pred,Info), Out) :-
    !,
    rewrite_to_idl_pos(Constraint, ConjList),
    % negation of /= is covered above, other operators provide singleton list
    ConjList = [DLConstraint],
    Out = [b(negation(DLConstraint),pred,Info)].

rewrite_to_idl_clean(Constraint, DLConstraint) :-
    rewrite_to_idl_pos(Constraint, DLConstraint).

rewrite_to_idl_no_zero(Constraint, ConjList) :-
    rewrite_to_idl(Constraint, TConjList),
    maplist(remove_zero_var, TConjList, ConjList).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c <= x-y -> y-x <= -c
    Constraint = b(less_equal(Constant,Rhs),pred,Info),
    get_int_value(Constant, CVal),
    rewrite_to_difference(Rhs, TRhs),
    switch_arguments_in_difference(TRhs, NRhs),
    !,
    NCVal is CVal * -1,
    NConstraint = b(less_equal(NRhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x+-y <= c -> x-y <= c | x-y <= c -> x-y <= c
    % x <= c -> x-_zero <= c | -x <= c -> _zero-x <= c
    Constraint = b(less_equal(Lhs,Constant),pred,Info),
    get_int_value(Constant, _),
    rewrite_to_difference(Lhs, NLhs),
    !,
    NConstraint = b(less_equal(NLhs,Constant),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x <= y -> x-y <= 0
    Constraint = b(less_equal(Id1,Id2),pred,Info),
    Id1 = b(identifier(_),_,_),
    Id2 = b(identifier(_),_,_),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NConstraint = b(less_equal(NLhs,b(integer(0),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % -x <= y -> y-x <= 0
    Constraint = b(less_equal(Id1,Id2),pred,Info),
    Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]),
    Id2 = b(identifier(_),_,_),
    !,
    NLhs = b(minus(Id2,Id1),integer,[]),
    NConstraint = b(less_equal(NLhs,b(integer(0),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c <= y -> _zero-y <= -c | c <= -y -> y-_zero <= -c
    Constraint = b(less_equal(Constant,Id2),pred,Info),
    get_int_value(Constant, CVal),
    ( Id2 = b(identifier(Id2Name),integer,Id2Info)
    -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[])
    ; Id2 = b(unary_minus(NegId2),integer,[])
    ),
    rewrite_to_difference(NegId2, Diff),
    !,
    NCVal is CVal * -1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c1 <= y-c2 -> _zero-y <= -c2-c1 | c1 <= -y-c2 -> y-_zero <= -c2-c1
    Constraint = b(less_equal(Constant1,AddOrSub),pred,Info),
    get_int_value(Constant1, CVal1),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2),
    get_int_value(Constant2, CVal2),
    ( Id2 = b(identifier(Id2Name),integer,Id2Info)
    -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[])
    ; Id2 = b(unary_minus(NegId2),integer,[])
    ),
    rewrite_to_difference(NegId2, Diff),
    !,
    NCVal is CVal2 + CVal1 * -1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x <= y-c -> x-y <= -c | x <= y+c -> x-y <= c
    Constraint = b(less_equal(Id1,AddOrSub),pred,Info),
    Id1 = b(identifier(_),_,_),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NConstraint = b(less_equal(NLhs,Constant),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x - c <= y -> x-y <= c | x + c <= y -> x-y <= -c
    Constraint = b(less_equal(AddOrSub,Id2),pred,Info),
    Id2 = b(identifier(_),_,_),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant),
    get_int_value(Constant, CVal),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NCVal is CVal * -1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x - c1 <= c2 -> x-_zero <= c2+c1 | x + c1 <= c2 -> x-_zero <= c2-c1
    Constraint = b(less_equal(AddOrSub,Constant2),pred,Info),
    get_int_value(Constant2, CVal2),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1),
    get_int_value(Constant1, CVal1),
    !,
    rewrite_to_difference(Id1, Diff),
    NCVal is CVal2 + CVal1 * -1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x+c1 <= y-c2 -> x-y <= -c2-c1 | x + c1 <= y+c2 -> x-y <= c2-c1
    % x-c1 <= y-c2 -> x-y <= -c2+c1 | x-c1 <= y+c2 -> x-y <= c2+c1
    Constraint = b(less_equal(AddOrSub1,AddOrSub2),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1),
    get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2),
    get_int_value(Constant1, CVal1),
    get_int_value(Constant2, CVal2),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NCVal is CVal2 + CVal1 * -1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c < x-y -> y-x <= -c-1
    Constraint = b(less(Constant,Rhs),pred,Info),
    get_int_value(Constant, CVal),
    rewrite_to_difference(Rhs, TRhs),
    switch_arguments_in_difference(TRhs, NRhs),
    !,
    NCVal is CVal * -1 - 1,
    NConstraint = b(less_equal(NRhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x+-y < c -> x-y <= c-1 | x-y < c -> x-y <= c-1
    % x < c -> x-_zero <= -c-1 | -x < c -> _zero-x <= -c-1
    Constraint = b(less(Lhs,Constant),pred,Info),
    get_int_value(Constant, CVal),
    rewrite_to_difference(Lhs, NLhs),
    !,
    NCVal is CVal - 1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x < y -> x-y <= -1
    Constraint = b(less(Id1,Id2),pred,Info),
    Id1 = b(identifier(_),_,_),
    Id2 = b(identifier(_),_,_),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NConstraint = b(less_equal(NLhs,b(integer(-1),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % -x < y -> y-x <= -1
    Constraint = b(less(Id1,Id2),pred,Info),
    Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]),
    Id2 = b(identifier(_),_,_),
    !,
    NLhs = b(minus(Id2,Id1),integer,[]),
    NConstraint = b(less_equal(NLhs,b(integer(-1),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c < y -> _zero-y <= -c-1 | c < -y -> y-_zero <= -c-1
    Constraint = b(less(Constant,Id2),pred,Info),
    get_int_value(Constant, CVal),
    ( Id2 = b(identifier(Id2Name),integer,Id2Info)
    -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[])
    ; Id2 = b(unary_minus(NegId2),integer,[])
    ),
    rewrite_to_difference(NegId2, Diff),
    !,
    NCVal is CVal * -1 - 1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % c1 < y-c2 -> _zero-y <= -c2-c1-1 | c1 <= -y-c2 -> y-_zero <= -c2-c1-1
    Constraint = b(less(Constant1,AddOrSub),pred,Info),
    get_int_value(Constant1, CVal1),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2),
    get_int_value(Constant2, CVal2),
    ( Id2 = b(identifier(Id2Name),integer,Id2Info)
    -> NegId2 = b(unary_minus(b(identifier(Id2Name),integer,Id2Info)),integer,[])
    ; Id2 = b(unary_minus(NegId2),integer,[])
    ),
    rewrite_to_difference(NegId2, Diff),
    !,
    NCVal is CVal2 + CVal1 * -1 - 1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x < y-c -> x-y <= -c-1 | x < y+c -> x-y <= c-1
    Constraint = b(less(Id1,AddOrSub),pred,Info),
    Id1 = b(identifier(_),_,_),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant),
    get_int_value(Constant, CVal),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NCVal is CVal - 1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x-c < y -> x-y <= c-1 | x+c < y -> x-y <= -c-1
    Constraint = b(less(AddOrSub,Id2),pred,Info),
    Id2 = b(identifier(_),_,_),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant),
    get_int_value(Constant, CVal),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NCVal is CVal * -1 - 1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x - c1 < c2 -> x-_zero <= c2+c1-1 | x + c1 < c2 -> x-_zero <= c2-c1-1
    Constraint = b(less(AddOrSub,Constant2),pred,Info),
    get_int_value(Constant2, CVal2),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1),
    rewrite_to_difference(Id1, Diff),
    get_int_value(Constant1, CVal1),
    !,
    rewrite_to_difference(Id1, Diff),
    NCVal is CVal2 + CVal1 * -1 - 1,
    NConstraint = b(less_equal(Diff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, [NConstraint]) :-
    % x+c1 < y-c2 -> x-y <= -c2-c1-1 | x+c1 < y+c2 -> x-y <= c2-c1-1
    % x-c1 < y-c2 -> x-y <= -c2+c1-1 | x-c1 < y+c2 -> x-y <= c2+c1-1
    Constraint = b(less(AddOrSub1,AddOrSub2),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1),
    get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2),
    get_int_value(Constant1, CVal1),
    get_int_value(Constant2, CVal2),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    NCVal is CVal2 + CVal1 * -1 - 1,
    NConstraint = b(less_equal(NLhs,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, ConjList) :-
    % c = _ -> rewrite(_ = c)
    Constraint = b(equal(Constant,Rhs),pred,Info),
    get_int_value(Constant, _),
    \+ get_int_value(Rhs, _),
    !,
    rewrite_to_idl_pos(b(equal(Rhs,Constant),pred,Info), ConjList).

rewrite_to_idl_pos(Constraint, [NC1,NC2]) :-
    % x-y = c -> x-y <= c & y-x <= -c | x+-y = c -> x-y <= c & y-x <= -c
    Constraint = b(equal(Lhs,Constant),pred,Info),
    get_int_value(Constant, CVal),
    !,
    rewrite_to_difference(Lhs, Diff),
    switch_arguments_in_difference(Diff, SDiff),
    NCVal is CVal * -1,
    NC1 = b(less_equal(Diff,Constant),pred,Info),
    NC2 = b(less_equal(SDiff,b(integer(NCVal),integer,[])),pred,Info).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x = y-c -> rewrite(x-y = -c) | x = y+c -> rewrite(x-y = c)
    Constraint = b(equal(Id1,AddOrSub),pred,Info),
    Id1 = b(identifier(_),_,_),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant),
    !,
    NLhs = b(minus(Id1,Id2),integer,[]),
    rewrite_to_idl_pos(b(equal(NLhs,Constant),pred,Info), NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x-c1 = y-c2 -> rewrite(x-y = -c2+c1) | x-c1 = y+c2 -> rewrite(x-y = c1+c2)
    % x+c1 = y-c2 -> rewrite(x-y = -c2-c1) | x+c1 = y+c2 -> rewrite(x-y = c1-c2)
    Constraint = b(equal(AddOrSub1,AddOrSub2),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub1, Id1, Constant1),
    get_args_of_add_or_minus_to_addition(AddOrSub2, Id2, Constant2),
    get_int_value(Constant1, CVal1),
    get_int_value(Constant2, CVal2),
    !,
    NCVal is CVal2 + CVal1 * -1,
    NLhs = b(minus(Id1,Id2),integer,[]),
    rewrite_to_idl_pos(b(equal(NLhs,b(integer(NCVal),integer,[])),pred,Info), NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x = y -> rewrite(x-y = 0)
    Constraint = b(equal(Id1,Id2),pred,Info),
    Id1 = b(identifier(_),_,_),
    Id2 = b(identifier(_),_,_),
    !,
    Constraint2 = b(equal(b(minus(Id1,Id2),integer,[]),b(integer(0),integer,[])),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % -x = -y -> rewrite(y-x = 0)
    Constraint = b(equal(Id1,Id2),pred,Info),
    Id1 = b(unary_minus(b(identifier(_),_,_)),integer,[]),
    Id2 = b(unary_minus(PosId2),integer,[]),
    !,
    Constraint2 = b(equal(b(minus(PosId2,Id1),integer,[]),b(integer(0),integer,[])),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x-c = y -> rewrite(x-y = c) | x+c = y -> rewrite(x-y = -c)
    Constraint = b(equal(AddOrSub,Id2),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant),
    Id2 = b(identifier(_),_,_),
    get_int_value(Constant, CVal),
    !,
    NCVal is CVal * -1,
    Constraint2 = b(equal(b(minus(Id1,Id2),integer,[]),b(integer(NCVal),integer,[])),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % c1 = y-c2 -> rewrite(y = c1+c2) | c1 = y+c2 -> rewrite(y = c1-c2)
    Constraint = b(equal(Constant1,AddOrSub),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id2, Constant2),
    get_int_value(Constant1, CVal1),
    get_int_value(Constant2, CVal2),
    !,
    NCVal is CVal1 + CVal2 * -1,
    Constraint2 = b(equal(Id2,b(integer(NCVal),integer,[])),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x-c1 = c2 -> rewrite(x = c2+c1) | x+c1 = c2 -> rewrite(x = c2-c1)
    Constraint = b(equal(AddOrSub,Constant2),pred,Info),
    get_args_of_add_or_minus_to_addition(AddOrSub, Id1, Constant1),
    get_int_value(Constant1, CVal1),
    get_int_value(Constant2, CVal2),
    !,
    NCVal is CVal2 + CVal1 * -1,
    Constraint2 = b(equal(Id1,b(integer(NCVal),integer,[])),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

rewrite_to_idl_pos(Constraint, NConstraint) :-
    % x = c -> rewrite(x-_zero = c) | -x = c -> rewrite(_zero-x = c)
    Constraint = b(equal(Id1,Constant),pred,Info),
    Id1 = b(identifier(_),_,_),
    get_int_value(Constant, _),
    !,
    rewrite_to_difference(Id1, Diff),
    Constraint2 = b(equal(Diff,Constant),pred,Info),
    rewrite_to_idl_pos(Constraint2, NConstraint).

switch_arguments_in_difference(b(minus(Lhs,Rhs),integer,Info), b(minus(Rhs,Lhs),integer,Info)).