b2asp

add_b2asp_error(Msg,Args) :-
    write(user_error,Msg), write(user_error,Args), nl(user_error).

add_b2asp_warning(Msg,Args) :-
    add_b2asp_error(Msg,Args).

add_indices([],_,[]).

add_indices([H|T],Nr,[couple(integer(Nr),H)|CT]) :- N1 is Nr+1,
    add_indices(T,N1,CT).

answer_nr_rest([X|T]) --> digit(X), !, answer_nr_rest(T).

answer_nr_rest([]) --> "".

anything --> [_],!,anything.

anything --> "".

assert_gen_id(ID,Pred,Kind,BaseType,TL) :-
    (TL=top_level
    -> assert(generated_id(ID,Pred)),
    assert(clingo_generated_id(Pred,Kind,BaseType,ID)),
    debug_format(19,'Generating clingo pred. ~w for B ~w id ~w (type ~w)~n',[Pred,Kind,ID,BaseType])
    ; true). % these are intermediate ids, e.g., generated for pair left/right hand sides

b2asp_portray('#clingo_range'(Low,Call,Up)) :- format('~w{~w}~w',[Low,Call,Up]).

b2asp_portray('#aggregate'(ClingoAggr,Pred)) :- format('~w{Var : ~w(Var)}',[ClingoAggr,Pred]).

b2asp_portray('#string'(S)) :- format('"~w"',[S]).

b2asp_portray(not(P)) :- write(' not '), print(P).

b2asp_portray(BOP) :- clingo_bin_op(BOP,A,B,COP),print_clingo_val(A), format(' ~w ',[COP]), print_clingo_val(B).

b_get_fd_type_bounds(_,_,_) :- fail.

bin_op(A+B,A,B,+).

bin_op(add(A,B),A,B,+).

bin_op(A-B,A,B,-).

bin_op(minus(A,B),A,B,-).

bin_op(A*B,A,B,*).

bin_op(multiplication(A,B),A,B,*).

bin_op(power_of(A,B),A,B,'**').

bin_op(A/B,A,B,/).

bin_op(div(A,B),A,B,/).

bin_op(A mod B,A,B,\).

bin_op(modulo(A,B),A,B,\).

bin_op((A,B),A,B,',').

bin_op(couple(A,B),A,B,',').

bin_op_pred_single_call(equal(A,B),A,B,'='). % equality for scalar

bin_op_pred_single_call(not_equal(A,B),A,B,'!=').

clingo_answer_line(Nr) --> "Answer: ",clingo_number(Nr), anything.

clingo_args([A|T]) --> clingo_constant(A),!, clingo_args2(T).

clingo_args([(A,B)|T]) --> clingo_pair(A,B),!, clingo_args2(T).

clingo_args2(T) --> ",", clingo_args(T).

clingo_args2([]) --> "".

clingo_atom(Pred,Args) --> clingo_identifier(Pred), clingo_opt_args(Args).

clingo_bin_op('<='(A,B),A,B,'<=').

clingo_bin_op('!='(A,B),A,B,'!=').

clingo_bin_op(':='(A,B),A,B,':=').

clingo_bin_op('..'(A,B),A,B,'..').

clingo_comment(Comment) :- format('%~w~n',[Comment]).

clingo_constant(A) --> clingo_number(A).

clingo_constant(A) --> clingo_identifier(A).

clingo_format_comment(FormatStr,Args) :- format(FormatStr,Args).

clingo_identifier(ID) --> letter(H), !, id2(T), {atom_codes(ID,[H|T])}.

clingo_model(M) --> " ", !, clingo_model(M).

clingo_model(Model) --> clingo_atom(Pred,Args),
    {(clingo_generated_id(Pred,_,_,_) -> Model = [Pred-Args|T] ; Model = T)},
    clingo_model(T).

clingo_model([]) --> "".

clingo_number(Nr) --> digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R])}.

clingo_number(MinusNr) --> "-", digit(X), !, answer_nr_rest(R), {number_codes(Nr,[X|R]),MinusNr is -Nr}.

clingo_opt_args(Args) --> "(", !, clingo_args(Args),")".

clingo_opt_args([]) --> "". % for propositions without arguments

clingo_pair(A,B) --> "(", clingo_constant(A),",", clingo_constant(B),")".

counter(0).

debug_format(_,FS,A) :- format(user_output,FS,A).

debug_mode(on).

detect_set_summation(Expr,SET) :- % detect special pattern SIGMA(ID).(ID:SET|ID)
    Expr = general_sum([TID1],b(member(TID2,SET),pred,_),TID3),
    get_texpr_id(TID1,ID), get_texpr_id(TID2,ID), get_texpr_id(TID3,ID).

digit(X) :- X >= 48, X =< 57.

digit(X) --> [X], {digit(X)}.

gen_clingo_base_set(integer,Atom,MaxCard,Prefix) :- !,
    get_min_int(MinInt), get_max_int(MaxInt),
    add_b2asp_warning('Restricting infinite integer base type to:',(MinInt,MaxInt)),
    gen_clingo_base_set(interval(MinInt,MaxInt),Atom,MaxCard,Prefix).

gen_clingo_base_set(interval(Low,Up),Atom,MaxCard,id_int) :- !,
    (Up >= Low -> MaxCard is 1+Up-Low ; MaxCard=0),
    format_to_codes('~w..~w',[Low,Up],Codes),
    atom_codes(Atom,Codes).

gen_clingo_base_set(boolean,Atom,2,id_bool) :- !, Atom = 'pred_true;pred_false'.

gen_clingo_base_set(global(GS),Atom,MaxCard,id_glob) :- % user-defined enumerated sets or deferred sets
    b_get_fd_type_bounds(GS,Low,Up), !,
    gen_clingo_base_set(interval(Low,Up),Atom,MaxCard,_). % we translate those sets as integers

gen_clingo_base_set(couple(A,B),Atom,MaxCard,id_pair) :- !,
    gen_clingo_base_set(A,AAtom,CardA,_),
    gen_clingo_base_set(B,BAtom,CardB,_),
    MaxCard is CardA*CardB,
    format_to_codes('((~w),(~w))',[AAtom,BAtom],Codes), % TODO: this is not very efficient for scalars, but necessary for sets; there seems to be a parsing problem when we use booleans below
    atom_codes(Atom,Codes).

gen_clingo_base_set(BaseType,error,1,id_error) :- add_b2asp_error('Unknown base type: ',BaseType).

gen_clingo_clause(Pred,ArgList,Body) :-
    Head =.. [Pred|ArgList],
    simplify_body(Body, SimplifiedBody),
    my_portray_clause( ( Head :- SimplifiedBody ) ).

gen_clingo_count_aggregate(Aggr,Pred,'#aggregate'(Aggr,Pred)).

gen_clingo_fact(Pred,ArgList) :-
    Head =.. [Pred|ArgList],
    my_portray_clause( Head ).

gen_clingo_ic_constraint(Body) :-
    simplify_body(Body, SimplifiedBody),
    nl,
    my_portray_clause( ( :- SimplifiedBody ) ).

gen_clingo_pred_clause(Source,Pred,ArgList,Body) :-
    gensym_if_necessary(Source,Pred),
    nl,
    gen_clingo_clause(Pred,ArgList,Body).

gen_clingo_scalar_identifier(IDB,B,PredB) :-
    gen_clingo_scalar_identifier(IDB,B,PredB,top_level).

gen_clingo_scalar_identifier(ID,_,Pred,_) :- nonvar(Pred),
    add_b2asp_warning('Identifier Clingo Result should be unbound: ',ID:Pred),fail.

gen_clingo_scalar_identifier(ID,_,Pred,_) :- % check if we have already created a Clingo predicate for ID
    generated_id(ID,P),!, Pred=P. % TODO: pass as environment and check bounds unchanged

gen_clingo_scalar_identifier(ID,couple(A,B),Pred,TopLevel) :- !,
    % improved translation of pairs, instead of 1 { id_pair_scalar_0((-127..128,-127..128))} 1. we generate:
    % id_pair_scalar_0((A,B)) :- id_A(A), id_B(B).
    % 1{id_A(-127..128)}1. 1{id_B(-127..128)}1.
    gensym(ID,IDA),
    gen_clingo_scalar_identifier(IDA,A,PredA,left_pair),
    gensym(ID,IDB),
    gen_clingo_scalar_identifier(IDB,B,PredB,right_pair),
    gensym_if_necessary(pair,Pred),
    CallA =.. [PredA,XA], CallB =.. [PredB,XB],
    clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,couple(A,B)]),
    gen_clingo_clause(Pred,[(XA,XB)], (CallA,CallB) ), % create clause Pred((XA,XB) :- PredA(XA), PredB(XB))
    assert_gen_id(ID,Pred,scalar,couple(A,B),TopLevel).

gen_clingo_scalar_identifier(ID,BaseType,Pred,TL) :- % generate: 1{Pred(Low..Up)}1.
    gen_clingo_base_set(BaseType,ClingoType,_MaxCard,Prefix),
    atom_concat(Prefix,'_scalar',Prefix2),
    gensym_if_necessary(Prefix2,Pred),
    clingo_format_comment('~n% clingo encoding of scalar identifier ~w of type ~w:~n',[ID,BaseType]),
    format('1 { ~w(~w)} 1.~n',[Pred,ClingoType]),
    assert_gen_id(ID,Pred,scalar,BaseType,TL).

gen_clingo_set_identifier(IDB,B,PredB) :-
    gen_clingo_set_identifier(IDB,B,PredB,top_level).

gen_clingo_set_identifier(ID,_,Pred,_) :- % check if we have already created a Clingo predicate for ID
    generated_id(ID,P),!,
    % TODO: pass as environment and check bounds unchanged
    (Pred=P -> true ; add_b2asp_error('Identifier already instantiated: ',ID:Pred),fail).

gen_clingo_set_identifier(ID,BaseType,Pred,TL) :- % generate: 1{Pred(Low..Up)}1.
    gen_clingo_base_set(BaseType,ClingoType,MaxCard,Prefix),
    atom_concat(Prefix,'_set',Prefix2),
    gensym_if_necessary(Prefix2,Pred),
    clingo_format_comment('~n% clingo encoding of set identifier ~w of type ~w:~n',[ID,BaseType]),
    format('0 { ~w(~w)} ~w.~n',[Pred,ClingoType,MaxCard]),
    assert_gen_id(ID,Pred,set,BaseType,TL).

gensym(Prefix,Symbol) :- retract(counter(N)), N1 is N+1,
    assert(counter(N1)),
    atom_codes(Prefix,PC),
    number_codes(N,NC),
    append(PC,[0'_|NC],PCNC),
    atom_codes(Symbol,PCNC).

gensym_if_necessary(Prefix,Symbol) :- var(Symbol), !, gensym(Prefix,Symbol).

gensym_if_necessary(_,_).

get_clingo_out_file('out.lp').

get_clingo_path('C:/Users/hhuri/Desktop/stage/clingo-5.4.0-win64/clingo.exe').

get_clingo_path('/opt/homebrew/bin/clingo').

get_first_sol([Sol|_],R) :- !, R=Sol.

get_first_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].

get_max_int(127).

get_min_int(-128).

get_sol([Sol|T],R) :- !, member(R,[Sol|T]).

get_sol(L,R) :- add_b2asp_error('Unexpected clingo solution: ',L), R=[].

get_texpr_id(identifier(X,_),X).

id2([H|T]) --> letter(H),!, id2(T).

id2([H|T]) --> digit(H),!, id2(T).

id2([95|T]) --> "_",!, id2(T).

id2([]) --> "".

is_predicate(b(_,pred,_)). % ProB typed AST node

is_predicate(BOP) :- bin_op_pred_single_call(BOP,_,_,_).

is_predicate(X) :- negate_pred(X,_) ; negate_pred(NX,X), NX \= negation(_).

is_predicate(BOP) :- negate_scalar_binary_pred(BOP,_,_,_).

is_predicate(conjunct(_,_)).

is_predicate(disjunct(_,_)).

is_predicate(implication(_,_)).

is_predicate(equivalence(_,_)).

is_set(set(BaseType),BaseType).

is_set(seq(Type),couple(integer,Type)).

letter(X) :- (X >= 97, X =< 122) ; (X >= 65, X=< 90). % underscore = 95, minus = 45

letter(X) --> [X], {letter(X)}.

lookup_global_constant(_,_) :- fail.

my_portray_clause(C) :- numbervars(C,0,_),print(C), write('.'),nl,fail.

my_portray_clause(_).

negate_pred(negation(Pred),Pred).

negate_pred(not_set_equal(A,B),set_equal(A,B)).

negate_pred(not_subset(A,B),subset(A,B)).

negate_pred(not_subset_strict(A,B),subset_strict(A,B)).

negate_pred(not_member(A,B),member(A,B)).

negate_scalar_binary_pred(less(A,B),A,B,'>=').

negate_scalar_binary_pred(greater(A,B),A,B,'<='). % note this is different from Prolog =< comparison syntax

negate_scalar_binary_pred(less_equal(A,B),A,B,'>').

negate_scalar_binary_pred(greater_equal(A,B),A,B,'<').

negate_scalar_binary_pred(equal(A,B),A,B,'!=').

negate_scalar_binary_pred(not_equal(A,B),A,B,'=').

print_clingo_val((A,B)) :- !, write('('), print(A), write(','), print(B), write(')'). % we need to print parentheses

print_clingo_val(A) :- print(A).

process_clingo_model_line([[0'\n]|T],Nr,Models) :- !, process_clingo_model_line(T,Nr,Models).

process_clingo_model_line([ModelLine|T],Nr,[BSolution|TM]) :- clingo_model(Model,ModelLine,[]), !,
    debug_format(19,'>>> ~s~n',[ModelLine]),
    length(Model,Len),
    format('Parsed clingo model ~w with ~w relevant atoms~n',[Nr,Len]),
    sort(Model,SModel), % TODO: extract solution for registered identifiers
    keyclumped(SModel,Groups),
    %write(Groups),nl,
    translate_clingo_model_to_bindings(Groups,BSolution),
    %write(BSolution),nl,
    process_clingo_output(T,TM).

process_clingo_model_line(T,Nr,Models) :-
    add_b2asp_error('Could not parse clingo model answer: ',Nr),
    process_clingo_output(T,Models).

process_clingo_output([],[]).

process_clingo_output([[0'\n]|T],Models) :- !, process_clingo_output(T,Models).

process_clingo_output([Line|T],Models) :- debug_format(19,'>>> ~s~n',[Line]),
    clingo_answer_line(Nr,Line,[]), !,
    process_clingo_model_line(T,Nr,Models).

process_clingo_output([_|T],Models) :- process_clingo_output(T,Models).

read_all(S,Command,Pipe,Lines) :-
    call_cleanup(read_all1(S,Command,Pipe,Lines),
    close(S)).

read_all1(S,Command,Pipe,Lines) :-
    catch(read_all2(S,Lines), error(_,E), ( % E could be system_error('SPIO_E_ENCODING_INVALID')
    ajoin(['Error reading ',Pipe,' for "',Command,'" due to exception: '],Msg),
    add_error(system_call,Msg,E),
    fail
)).

read_all2(S,Text) :-
    read_line(S,Line),
    ( Line==end_of_file -> Text=[[]]
    ;
    Text = [Line, [0'\n] | Rest],
    read_all2(S,Rest)).

reset_b2asp :-
    retractall(counter(_)), assert(counter(0)),
    retractall(generated_id(_,_)),
    retractall(clingo_generated_id(_,_,_,_)).

run_clingo(File,Result) :- run_clingo(File,1,_,Result,_).

run_clingo(File,MaxNrModels,WT,Result,Exhaustive) :-
    statistics(walltime,[Start,_]),
    (debug_mode(on) -> DOpt=['-V'] ; DOpt=[]),
    (MaxNrModels<2 -> ModelsOpt='--models=1' % so that code works without ajoin
    ; ajoin(['--models=',MaxNrModels],ModelsOpt)),
    OtherOptions = [ModelsOpt|DOpt] , % =0 outputs all models
    debug_format(19,' Running CLINGO on ~w (options=~w)~n',[File,OtherOptions]),flush_output,
    Options = [process(Process),stdout(pipe(JStdout,[encoding(utf8)])),
    stderr(pipe(JStderr,[encoding(utf8)]))],
    (get_clingo_path(Clingo), file_exists(Clingo)-> true
    ; get_clingo_path(Clingo) -> add_b2asp_error('Cannot find Clingo binary at (be sure to set path_to_clingo preference to point to clingo binary): ',Clingo),fail
    ; add_b2asp_error('Cannot find Clingo binary (be sure to set path_to_clingo preference to point to clingo binary)',''),fail
    ),
    safe_process_create(Clingo, [File|OtherOptions], Options),
    read_all(JStdout,Clingo,stdout,OutLines), % read before process_wait; avoid blocking clingo
    read_all(JStderr,Clingo,stderr,ErrLines),
    process_wait(Process,Exit),
    % above almost corresponds to: system_call_with_options(Clingo,[File|OtherOptions],[],OutLines,ErrLines,ExitCode)
    % except that here we do not call append/2 on OutLines and ErrLines
    statistics(walltime,[Stop,_]), WT is Stop-Start,
    format(' CLINGO walltime: ~w ms, ~w~n',[WT,Exit]),flush_output,
    debug_format(19,'--- CLINGO OUTPUT ----~n',[]),flush_output,
    process_clingo_output(OutLines,Models),
    if((Exit=exit(Code), ErrText = [],
    translate_clingo_exit_code(Code,Models,Result,Exhaustive)),
    debug_format(19,'Clingo exit code = ~w -> ~w (~w)~n',[Code,Result,Exhaustive]),
    (append(ErrLines,ErrText),
    format('STD-ERROR (~w):~n~s~n',[Exit,ErrText]),
    Result=no_solution_found(Exit))
).

run_clingo_on_formula(Formula) :- run_clingo_on_formula(Formula,1,_,_).

run_clingo_on_formula(Formula,MaxNrModels,Result,Exhaustive) :-
    % write(user_output,Formula),nl(user_output),
    reset_b2asp,
    get_clingo_out_file(OutFile),
    catch(tell(OutFile), % TODO: use streams and pass in environment
    error(existence_error(_,_),_),
    (add_b2asp_error('Path does not exist, be sure to set tmpdir preference correctly: ',OutFile),
    fail)),
    call_cleanup(top_level_trans(Formula),told),
    !,
    (debug_mode(on) -> show_file(OutFile) ; true),
    run_clingo(OutFile,MaxNrModels,_,Result,Exhaustive).

run_clingo_on_formula(_,_,Result,non_exhaustive) :-
    Result=no_solution_found(translation_failed).

safe_process_create(Cmd,Args,Opts) :- process_create(Cmd,Args,Opts).

scalar_type(boolean).

scalar_type(integer).

scalar_type(global(_)).

scalar_type(couple(A,B)) :- scalar_type(A), scalar_type(B).

set_aggregate(card(Set),Set,'#count',count).

set_aggregate(min(Set),Set,'#min',min).

set_aggregate(max(Set),Set,'#max',max).

set_aggregate(GeneralSum,Set,'#sum',sum) :- detect_set_summation(GeneralSum,Set).

show_file(File) :-
    format('Contents of file ~w:~n',[File]),
    format('% --------------~n',[]),
    open(File,read,Stream),
    call_cleanup(show_stream(Stream),close(Stream)),
    format('% --------------~n',[]).

show_stream(Stream) :-
    read_line(Stream,Line),
    Line \= end_of_file,!,
    format('~s~n',[Line]),
    show_stream(Stream).

show_stream(_).

simplify_body(X,R) :- var(X),!,R=X.

simplify_body((A,B),Res) :- !,
    ( A=true -> simplify_body(B,Res)
    ; B=true -> simplify_body(A,Res)
    ; Res=(SA,SB), simplify_body(A,SA), simplify_body(B,SB)).

simplify_body(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg].

simplify_body(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2].

simplify_body(not(B),not(SB)) :- !, simplify_body(B,SB). % TODO: remove double not ?

simplify_body('=='(A,B),'=='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB).

simplify_body('!='(A,B),'!='(SA,SB)) :- !, simplify_expr(A,SA), simplify_expr(B,SB).

simplify_body(B,B).

simplify_expr(X,R) :- var(X),!,R=X.

simplify_expr(call(Pred,Arg),Call) :- !, Call =.. [Pred,Arg].

simplify_expr(call(Pred,Arg1,Arg2),Call) :- !, Call =.. [Pred,Arg1,Arg2].

simplify_expr(B,B).

solve_pred_with_clingo(BPred,MaxNrSols,_LocalState,Res,Exhaustive) :-
    run_clingo_on_formula(BPred,MaxNrSols,Res,Exhaustive).

specific_trans_not_member_pred(pow_subset(B),A,Prop) :- !,
    trans_not_pred(subset(A,B),Prop). % A:POW(B) <=> A <: B

specific_trans_not_member_pred(pow1_subset(B),A,Prop) :- !,
    trans_not_pred(conjunct(subset(A,B),not_equal(A,empty_set)),Prop). % A:POW1(B) <=> A <: B & A /= {}

specific_trans_not_member_pred(relations(Dom,Ran),A,Prop) :- !,
    trans_not_pred(subset(A,cartesian_product(Dom,Ran)),Prop). % A: Dom <-> Ran <=> A <: (Dom*Ran)

specific_trans_not_member_pred(partial_function(Dom,Ran),A,Prop) :- !,
    % A : Dom +-> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan
    trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
    is_partial_function(A)), % TODO avoid translating A twice
    Prop).

specific_trans_not_member_pred(partial_injection(Dom,Ran),A,Prop) :- !,
    % A : Dom >+> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & A~:TypeRan +-> TypeDom
    trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
    conjunct(is_partial_function(A),
    is_injective(A))), % TODO avoid translating A three times
    Prop).

specific_trans_not_member_pred(total_function(Dom,Ran),A,Prop) :- !,
    % A : Dom --> Ran <=> A <: (Dom*Ran) & A: TypeDom +-> TypeRan & Dom <: domain(A)
    trans_not_pred(conjunct(subset(A,cartesian_product(Dom,Ran)),
    conjunct(is_partial_function(A),
    subset(Dom,domain(A)))), % TODO avoid translating A three times
    Prop).

specific_trans_not_member_pred(seq(Ran),A,Prop) :- !,
    % A : seq(Ran) <=> ran(A) <: Ran & A: INTEGER +-> TypeRan & domain(A) = 1..N (for some N = size(A))
    trans_not_pred(conjunct(is_sequence_domain(domain(A)),
    conjunct(is_partial_function(A),
    subset(range(A),Ran))), % TODO avoid translating A three times
    Prop).

test(0) :-trans_set(union(empty_set, intersection(set_extension([1,2]), set_extension([2,3]))), main).

test(1) :-trans_set(union(empty_set, set_subtraction(set_extension([1,2]), set_extension([2,3]))), main).

test(2) :- tell('out2.lp'),
    trans_set(union(set_extension([4]), intersection(set_extension([1,2]), set_extension([2,3]))), main),
    told.

test(3) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,5 mod 2]), set_extension([2,4])) ).

test(4) :- run_clingo_on_formula( set_subtraction(set_extension([1,2+2,2+4]), interval(2,4)) ).

test(5) :- run_clingo_on_formula( set_subtraction(interval(1,100), interval(3,98)) ).

test(6) :- run_clingo_on_formula( set_extension([card(set_subtraction(interval(1,100), interval(3,98)))]) ).

test(7) :- run_clingo_on_formula( equal(add(identifier(x,interval(1,10)),integer(5)), integer(11))).

test(8) :- run_clingo_on_formula( subset(interval(1,5),
    union(identifier(x,interval(2,6)),set_extension([1])))).

test(9) :- run_clingo_on_formula( set_equal(interval(1,5),
    union(identifier(x,interval(2,6)),set_extension([1])))).

test(10) :- run_clingo_on_formula( not_set_equal(interval(1,5),
    union(identifier(x,interval(2,6)),interval(1,5)))).

test(11) :- run_clingo_on_formula( conjunct( subset(interval(1,5),identifier(x,interval(0,6))),
    subset(identifier(x,interval(0,6)), interval(1,6)))).

test(12) :- run_clingo_on_formula( conjunct( conjunct( member(3,identifier(x,interval(0,4))),
    member(4,identifier(x,interval(0,4)))),
    not_member(1,identifier(x,interval(0,4))))).

test(13) :- run_clingo_on_formula( conjunct( equivalence( member(3,identifier(x,interval(0,4))),
    member(4,identifier(x,interval(0,4)))),
    member(4,identifier(x,interval(0,4))))).

test(14) :- run_clingo_on_formula( set_equal( union(interval(1,100),set_extension([identifier(x,interval(0,200))])),
    interval(1,101))). % small performance test

test(15) :- run_clingo_on_formula( set_equal( union(identifier(s,boolean),set_extension([identifier(x,boolean)])),
    set_extension([pred_true,pred_false]))).

test(16) :- run_clingo_on_formula( conjunct( less(integer(3),identifier(x,interval(0,6))),
    greater(integer(5),identifier(x,interval(0,6))))).

test(17) :- run_clingo_on_formula( conjunct( less(integer(1),card(identifier(x,interval(0,6)))),
    greater(integer(3),card(identifier(x,interval(0,6)))))).

test(18) :- run_clingo_on_formula( b(equal(b(card(b(identifier(x),set(boolean),'.'(nodeid(p4(-1,1,6,7)),[]))),
    integer,'.'(nodeid(p4(-1,1,1,8)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,9,10)),[]))),
    pred,'.'(removed_typing,'.'(nodeid(p4(-1,1,1,10)),[])))). % ProB AST example

test(19) :- run_clingo_on_formula( conjunct(equal(max(identifier(x,interval(1,10))),integer(3)),
    equal(card(identifier(x,interval(1,10))),integer(2)))).

test(20) :- run_clingo_on_formula(set_extension([string(test1),string(test2)])).

test(21) :- run_clingo_on_formula(set_extension([(1,2)])).

test(22) :- run_clingo_on_formula(reverse(set_extension([(1,2)]))).

test(23) :- run_clingo_on_formula(b(exists('.'(b(identifier(f),set(couple(boolean,boolean)),[]),[]),b(conjunct(b(member(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,1,2)),[])),b(partial_function(b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,3,7)),[])),b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,10,14)),[]))),set(set(couple(boolean,boolean))),'.'(nodeid(p4(-1,1,3,14)),[]))),pred,'.'(nodeid(p4(-1,1,1,14)),[])),b(equal(b(card(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,22,23)),[]))),integer,'.'(nodeid(p4(-1,1,17,24)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,25,26)),[]))),pred,'.'(nodeid(p4(-1,1,17,26)),[]))),pred,'.'(nodeid(p4(-1,1,1,26)),[]))),pred,'.'(used_ids([]),'.'(nodeid(p4(-1,1,1,26)),[])))).

test(24) :- run_clingo_on_formula(b(exists('.'(b(identifier(f),set(couple(boolean,boolean)),[]),[]),b(conjunct(b(member(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,1,2)),[])),b(total_function(b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,3,7)),[])),b(bool_set,set(boolean),'.'(nodeid(p4(-1,1,10,14)),[]))),set(set(couple(boolean,boolean))),'.'(nodeid(p4(-1,1,3,14)),[]))),pred,'.'(nodeid(p4(-1,1,1,14)),[])),b(equal(b(card(b(identifier(f),set(couple(boolean,boolean)),'.'(nodeid(p4(-1,1,22,23)),[]))),integer,'.'(nodeid(p4(-1,1,17,24)),[])),b(integer(2),integer,'.'(nodeid(p4(-1,1,25,26)),[]))),pred,'.'(nodeid(p4(-1,1,17,26)),[]))),pred,'.'(nodeid(p4(-1,1,1,26)),[]))),pred,'.'(used_ids([]),'.'(nodeid(p4(-1,1,1,26)),[])))).

top_level_trans(Formula) :-
    version_str(V),format('% Clingo encoding of B formula created by ProB ~w~n',[V]),
    % we could call datime(datime(Yr,Mon,Day,Hr,Min,_Sec)),
    (is_predicate(Formula) -> top_level_translate_predicate(Formula) ; trans_set(Formula,main)),!.

top_level_trans(Formula) :- add_b2asp_error('Could not translate: ',Formula).

top_level_translate_predicate(Formula) :-
    trans_not_pred(Formula,Prop),
    gen_clingo_ic_constraint( Prop ).

trans_not_member_pred(A,TB,Prop) :- (TB=b(B,_,_) -> true ; TB=B),
    specific_trans_not_member_pred(B,A,Prop),!.

trans_not_member_pred(A,B,Prop) :- % generic translation rule:
    translate_scalar(A,X1,CallA),
    trans_set(B,P2),
    gen_clingo_pred_clause(not_member,Prop,[], (CallA, not(call(P2,X1)) )). % :- P1(X), not P2(X). (same as subset)

trans_not_pred(b(Pred,pred,_Infos),Prop) :- !, % format(user_output,' pred --> ~w~n',[Pred]),
    trans_not_pred(Pred,Prop).

trans_not_pred(truth,Prop) :- !,
    gen_clingo_pred_clause(falsity,Prop,[], 1=2 ).

trans_not_pred(falsity,Prop) :- !,
    gensym_if_necessary(truth,Prop),
    gen_clingo_fact(Prop,[]).

trans_not_pred(exists(Paras,Pred),Prop) :- !,
    % TODO: properly pass environment around and register paras, rather than using generated_id/2 facts
    (member(b(identifier(ID),_,_),Paras), generated_id(ID,_),
    add_b2asp_error('Identifier clash (B2ASP does not yet support multiple uses of same id): ',ID),fail
    ; true),
    trans_not_pred(Pred,Prop).

trans_not_pred(subset(A,B),Prop) :- !,
    trans_set(A,P1), trans_set(B,P2),
    gen_clingo_pred_clause(not_subset,Prop,[], (call(P1,X), not(call(P2,X)) )). % :- P1(X), not P2(X).

trans_not_pred(subset_strict(A,B),Prop) :- !,
    trans_not_pred(conjunct(subset(A,B),not_set_equal(A,B)),Prop).

trans_not_pred(member(A,B),Prop) :- !,
    trans_not_member_pred(A,B,Prop). % dedicated code for translating membership

trans_not_pred(set_equal(A,B),Prop) :- !, % could be also translated into conjunction of subset
    % Note: does not exist as such in B AST: is equal with typing info = set(_)
    % this could also works with scalars (i.e., if P1/P2 have exactly one solution)
    trans_set(A,P1), trans_set(B,P2),
    CallA =..[P1,X], CallB=..[P2,X],
    gen_clingo_pred_clause(not_set_equal,Prop,[], (CallA, not(CallB) )), % :- P1(X), not P2(X).
    gen_clingo_clause(Prop,[], (CallB, not(CallA) )). % :- P2(X), not P1(X).

trans_not_pred(equal(A,B),Prop) :- A = b(_,set(_),_),!,
    trans_not_pred(set_equal(A,B),Prop).

trans_not_pred(not_equal(A,B),Prop) :- A = b(_,set(_),_),!,
    trans_not_pred(not_set_equal(A,B),Prop).

trans_not_pred(is_partial_function(A),Prop) :- !,
    trans_set(A,P1),
    gen_clingo_pred_clause(not_pfun,Prop,[], (call(P1,(X,Y)), call(P1,(X,Z)), '!='(Y,Z)) ). % :- P1((X,Y)),P1((X,Z)), Y!=Z.

trans_not_pred(is_injective(A),Prop) :- !,
    trans_set(A,P1),
    gen_clingo_pred_clause(not_inj,Prop,[], (call(P1,(Y,X)), call(P1,(Z,X)), '!='(Y,Z)) ). % :- P1((Y,X)),P1((Z,X)), Y!=Z.

trans_not_pred(is_sequence_domain(A),Prop) :- !,
    trans_set(A,P1),
    gen_clingo_pred_clause(not_seq,Prop,[], (call(P1,X), '<'(X,1) )), % :- P1(X), X < 1. (sequences start at 1)
    gen_clingo_clause(Prop,[], (call(P1,X), '>'(X,1), '='(X1,X-1), not(call(P1,X1))) ). % :- P1(X), not P1(X-1).

trans_not_pred(Arith,Prop) :-
    negate_scalar_binary_pred(Arith,A,B,ClingoOp),!,
    translate_scalar(A,X1,CallA),
    translate_scalar(B,X2,CallB),
    gen_clingo_pred_clause(arith,Prop,[], (CallA, CallB, call(ClingoOp,X1,X2) )).

trans_not_pred(conjunct(P1,P2),Prop) :- !, % not(P1 & P2) <=> not(P1) or not(P2)
    trans_not_pred(P1,NotP1),
    trans_not_pred(P2,NotP2),
    gen_clingo_pred_clause(not_conjunct,Prop,[], NotP1 ),
    gen_clingo_clause(Prop,[], NotP2 ).

trans_not_pred(disjunct(P1,P2),Prop) :- !, % not(P1 or P2) <=> not(P1) & not(P2)
    trans_not_pred(P1,NotP1),
    trans_not_pred(P2,NotP2),
    gen_clingo_pred_clause(not_disjunct,Prop,[], (NotP1 , NotP2) ).

trans_not_pred(implication(P1,P2),Prop) :- !, % not(P1 => P2) <=> P1 & not(P2)
    trans_not_pred(P1,NotP1), % TODO: translate P1 positively?
    trans_not_pred(P2,NotP2),
    gen_clingo_pred_clause(not_implicatin,Prop,[], (not(NotP1) , NotP2) ).

trans_not_pred(equivalence(P1,P2),Prop) :- !, % not(P1 <=> P2) <=> (P1 & not(P2)) or (not(P1) & P2)
    trans_not_pred(P1,NotP1),
    trans_not_pred(P2,NotP2),
    gensym_if_necessary(not_equiv,Prop),
    gen_clingo_clause(Prop,[], (not(NotP1) , NotP2) ),
    gen_clingo_clause(Prop,[], (NotP1 , not(NotP2)) ).

trans_not_pred(Pred,Prop) :-
    negate_pred(Pred,NotPred),!,
    trans_not_pred(NotPred,NegProp), % translate negation and create auxiliary proposition for it
    gen_clingo_pred_clause(negated,Prop,[], not(NegProp) ). % negate the proposition

trans_not_pred(X,Prop) :-
    add_b2asp_error('Ignoring unsupported predicate: ',X),
    trans_not_pred(truth,Prop).