smtlib2_translation

binary_to_binary_couples(Bits,Couples) :-
    length(Bits,L), FirstL is L - 1,
    binary_to_binary_couples(FirstL,Bits,Couples).

binary_to_binary_couples(-1,[],[]).

binary_to_binary_couples(L,[Bit|Bits],[Couple|Couples]) :-
    A = b(integer(L),integer,[]),
    B = b(integer(Bit),integer,[]),
    Couple = b(couple(A,B),couple(integer,integer),[]),
    L2 is L - 1,
    binary_to_binary_couples(L2,Bits,Couples).

bool_to_pred(Bool,Pred) :-
    get_texpr_expr(Bool,convert_bool(Pred)), !.

bool_to_pred(Bool,Pred) :-
    get_texpr_type(Bool,boolean), !,
    safe_create_texpr(equal(Bool,b(boolean_true,boolean,[])),pred,Pred).

bool_to_pred(Bool,Bool) :-
    get_texpr_type(Bool,pred), !.

bv2nat(BV,Nat) :-
    IntOne = b(integer(1),integer,[]),
    IntTwo = b(integer(2),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]),
    Nat = b(general_sum([IdX1,IdX2],b(member(b(couple(IdX1,IdX2),couple(integer,integer),[]),BV),pred,[]),b(multiplication(IdX2,PowerOf),integer,[])),integer,[]).

bv_to_nat_and_compare(A,B,Op,Env,Out) :-
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Operation =.. [Op,BANat,BBNat],
    Out = b(Operation,pred,[]).

bvwidth(BV,Width) :-
    Width = b(max(b(domain(BV),set(integer),[])),integer,[]).

chain(Op,[A,B],BPred) :- !,
    Pred =.. [Op,A,B],
    BPred = b(Pred,pred,[]).

chain(Op,[First,Second|Further],TermOut) :-
    chain(Op,[First,Second],Pred),
    chain(Op,[Second|Further],FurtherPred),
    conjunct_predicates([Pred,FurtherPred],TermOut).

integer_to_binary_couples(Value,Length,Couples) :-
    PLength is Length - 1,
    integer_to_binary_couples(Value,0,PLength,Couples).

integer_to_binary_couples(Value,Current,Current,[b(couple(A,B),couple(integer,integer),[])]) :- !,
    A = b(integer(Current),integer,[]),
    BVal is mod(Value,2),
    B = b(integer(BVal),integer,[]).

integer_to_binary_couples(Value,Current,PLength,[b(couple(A,B),couple(integer,integer),[])|Cs]) :-
    A = b(integer(Current),integer,[]),
    BVal is mod(Value,2),
    B = b(integer(BVal),integer,[]),
    NValue is Value // 2,
    NCurrent is Current + 1,
    integer_to_binary_couples(NValue,NCurrent,PLength,Cs).

interleave(_Op,[A],TermOut) :- !, TermOut=A.

interleave(Op,[First|Further],TermOut) :-
    interleave(Op,Further,FurtherPred),
    get_texpr_type(FurtherPred,FurtherType),
    Pred =.. [Op,First,FurtherPred],
    safe_create_texpr(Pred,FurtherType,TermOut).

is_function_constraint(Id,FullType,Constraint) :-
    FullType = set(couple(From,To)),
    Identifier = b(identifier(Id),FullType,[]),
    type_to_expr(From,FromExpr),
    type_to_expr(To,ToExpr),
    Constraint = b(member(Identifier,b(partial_function(FromExpr,ToExpr),set(FullType),[])),pred,[]).

let_equalities_and_bids([bind(ID,Term)],[IDTerm],[AssOut],Env) :- !,
    smt_term_to_prob_term(Term,Env,Ass),
    get_texpr_type(Ass,IdentifierType),
    (IdentifierType == pred
    -> IDTerm = b(identifier(ID),boolean,[]),
    safe_create_texpr(convert_bool(Ass),boolean,AssOut)
    ; IDTerm = b(identifier(ID),IdentifierType,[]),
    AssOut = Ass).

let_equalities_and_bids([bind(ID,Term)|Further],[IDTerm|FurtherIdentifiers],Assignments,Env) :-
    let_equalities_and_bids([bind(ID,Term)],[IDTerm],FirstAssignment,Env),
    let_equalities_and_bids(Further,FurtherIdentifiers,FurtherAssignments,Env),
    append(FirstAssignment,FurtherAssignments,Assignments).

nat2bv(Nat,Width,BV) :-
    IntOne = b(integer(1),integer,[]),
    IntTwo = b(integer(2),integer,[]),
    % todo: make sure identifiers do not collide
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeId1 = b(member(IdX1,b(interval(b(integer(1),integer,[]),Width),set(integer),[])),pred,[]),
    TypeId2 = b(member(IdX2,b(interval(b(integer(0),integer,[]),b(integer(1),integer,[])),set(integer),[])),pred,[]),
    PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]),
    ValueOfId2 = b(equal(IdX2,b(modulo(b(div(Nat,PowerOf),integer,[]),IntTwo),integer,[])),pred,[]),
    conjunct_predicates([TypeId1,TypeId2,ValueOfId2],InnerPred),
    BV = b(comprehension_set([IdX1,IdX2],InnerPred),set(couple(integer,integer)),[]).

replace_identifiers([],[],D,D,_Env).

replace_identifiers([b(identifier(I),_,_)|T1],[Term|Terms],In,Out,Env) :-
    smt_term_to_prob_term(Term,Env,BTerm),
    replace_id_by_expr(In,I,BTerm,TOut),
    replace_identifiers(T1,Terms,TOut,Out,Env).

signed_bv2nat(BV,Nat) :-
    IntOne = b(integer(1),integer,[]),
    IntTwo = b(integer(2),integer,[]),
    IntMinusOne = b(integer(-1),integer,[]),
    % todo: make sure identifiers do not collide
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    NotZeroIndex = b(not_equal(IdX1,b(integer(0),integer,[])),pred,[]),
    MemberConstraint = b(member(b(couple(IdX1,IdX2),couple(integer,integer),[]),BV),pred,[]),
    conjunct_predicates([NotZeroIndex,MemberConstraint],Const),
    PowerOf = b(power_of(IntTwo,b(minus(IdX1,IntOne),integer,[])),integer,[]),
    Sum = b(general_sum([IdX1,IdX2],Const,b(multiplication(IdX2,PowerOf),integer,[])),integer,[]),
    ZeroIndex = b(function(BV,b(integer(0),integer,[])),integer,[]),
    Sign = b(power_of(IntMinusOne,ZeroIndex),integer,[]),
    Nat = b(multiplication(Sign,Sum),integer,[]).

signed_bv_to_nat_and_compare(A,B,Op,Env,Out) :-
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    signed_bv2nat(BA,BANat),
    signed_bv2nat(BB,BBNat),
    Operation =.. [Op,BANat,BBNat],
    Out = b(Operation,pred,[]).

smt_id_to_prob_id('<=',less_equal,chain).

smt_id_to_prob_id('>=',greater_equal,chain).

smt_id_to_prob_id('<',less,chain).

smt_id_to_prob_id('>',greater,chain).

smt_id_to_prob_id('distinct',not_equal,chain).

smt_id_to_prob_id('*',multiplication,interleave).

smt_id_to_prob_id('+',add,interleave).

smt_id_to_prob_id('-',minus,interleave).

smt_id_to_prob_id_preds('or',disjunct).

smt_id_to_prob_id_preds('and',conjunct).

smt_id_to_prob_id_preds('=>',implication).

smt_term_to_prob_term(attributed_term(Term,_Attr),Env,Out) :- !,
    smt_term_to_prob_term(Term,Env,Out).

smt_term_to_prob_term(id_term(id('not'),[Arg]),Env,Out) :- !,
    smt_term_to_prob_term(Arg,Env,BArg),
    get_texpr_type(BArg,Type),
    (Type = pred
    -> Out = b(negation(BArg),pred,[])
    ; Out = b(equal(BArg,b(boolean_false,boolean,[])),pred,[])).

smt_term_to_prob_term(id_term(id('-'),[SingleArg]),Env,Out) :- !,
    % special case for unary minus: can not be interleaved
    smt_term_to_prob_term(SingleArg,Env,BArg),
    Out = b(unary_minus(BArg),integer,[]).

smt_term_to_prob_term(id_term(id('='),Args),Env,Out) :- !,
    maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs),
    maplist(get_texpr_type,BArgs,Types),
    (member(pred,Types)
    -> maplist(bool_to_pred,BArgs,BArgsPreds),
    chain(equivalence,BArgsPreds,Out)
    ; chain(equal,BArgs,Out)).

smt_term_to_prob_term(id_term(id('ite'),[Test,If,Then]),Env,Out) :- !,
    smt_term_to_prob_term(Test,Env,BTestT),
    smt_term_to_prob_term(If,Env,BIfT),
    smt_term_to_prob_term(Then,Env,BThenT),
    bool_to_pred(BTestT,BTest),
    to_bool_if_necessary(BIfT,BIf),
    to_bool_if_necessary(BThenT,BThen),
    get_texpr_type(BIf,Type),
    Out = b(if_then_else(BTest,BIf,BThen),Type,[]).

smt_term_to_prob_term(id_term(id(member),[Element,Set]),Env,Out) :- !,
    smt_term_to_prob_term(Set,Env,BSet),
    smt_term_to_prob_term(Element,Env,BElement),
    Out = b(member(BElement,BSet),pred,[]).

smt_term_to_prob_term(id_term(id(card),[Set]),Env,Out) :- !,
    smt_term_to_prob_term(Set,Env,BSet),
    Out = b(card(BSet),integer,[]).

smt_term_to_prob_term(id_term(id(singleton),[Element]),Env,Out) :- !,
    smt_term_to_prob_term(Element,Env,BElement),
    get_texpr_type(BElement,ElementType),
    Out = b(set_extension([BElement]),set(ElementType),[]).

smt_term_to_prob_term(id_term(id(union),[SetA,SetB]),Env,Out) :- !,
    smt_term_to_prob_term(SetA,Env,BSetA),
    smt_term_to_prob_term(SetB,Env,BSetB),
    get_texpr_type(BSetB,Type),
    Out = b(union(BSetA,BSetB),Type,[]).

smt_term_to_prob_term(id_term(id(intersection),[SetA,SetB]),Env,Out) :- !,
    smt_term_to_prob_term(SetA,Env,BSetA),
    smt_term_to_prob_term(SetB,Env,BSetB),
    get_texpr_type(BSetB,Type),
    Out = b(intersection(BSetA,BSetB),Type,[]).

smt_term_to_prob_term(id_term(id(subset),[SetA,SetB]),Env,Out) :- !,
    smt_term_to_prob_term(SetA,Env,BSetA),
    smt_term_to_prob_term(SetB,Env,BSetB),
    Out = b(subset(BSetA,BSetB),pred,[]).

smt_term_to_prob_term(id_term(id('store'),[Array,Index,Element]),Env,Out) :- !,
    smt_term_to_prob_term(Array,Env,BArray),
    get_texpr_type(BArray,ArrayType),
    ArrayType = set(CoupleType),
    smt_term_to_prob_term(Index,Env,BIndex),
    smt_term_to_prob_term(Element,Env,BElement),
    % TO DO: generate union or set_difference depending on Element=true or false when smtlib2b_arrays_as_sets
    % store(X,Index,El) = IF El=TRUE THEN X \/ {Index} ELSE X \ {Index} END
    SetEx = b(set_extension([b(couple(BIndex,BElement),CoupleType,[])]),ArrayType,[]),
    Out = b(overwrite(BArray,SetEx),ArrayType,[]).

smt_term_to_prob_term(id_term(id('select'),[Array,Index]),Env,Out) :- !,
    smt_term_to_prob_term(Array,Env,BArray),
    smt_term_to_prob_term(Index,Env,BIndex),
    get_texpr_type(BArray,ArrayType),
    %format('select of array ~w (type: ~w) at index ~w~n',[Array,ArrayType,Index]),
    (ArrayType = set(couple(_From,To)) % Array was translated as total function From --> To
    -> Out = b(function(BArray,BIndex),To,[])
    ; ArrayType = set(_From), % Array was translated as set (smtlib2b_arrays_as_sets=true)
    MEM = b(member(BIndex,BArray),pred,[]),
    Out = b(convert_bool(MEM),boolean,[])
).

smt_term_to_prob_term(id_term(id('concat'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,WidthA),
    bvwidth(BB,WidthB),
    WidthBP1 = b(add(WidthB,Int1),integer,[]),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    FullWidth = b(add(b(add(WidthA,WidthB),integer,[]),Int1),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthB),pred,[]),
    b(function(BB,IdX1),integer,[]),
    b(function(BA,b(minus(IdX1,WidthBP1),integer,[])),integer,[])),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id(zero_extend(NewLength)),[A]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    bvwidth(BA,WidthA),
    WidthAP1 = b(add(WidthA,Int1),integer,[]),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    FullWidth = b(add(WidthA,b(integer(NewLength),integer,[])),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthA),pred,[]),
    b(integer(0),integer,[]),
    b(function(BA,b(minus(IdX1,WidthAP1),integer,[])),integer,[])),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id(sign_extend(NewLength)),[A]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    bvwidth(BA,WidthA),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    WidthAP1 = b(add(WidthA,Int1),integer,[]),
    FullWidth = b(add(WidthA,b(integer(NewLength),integer,[])),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,FullWidth),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(less_equal(IdX1,WidthA),pred,[]),
    b(function(BA,IdX1),integer,[]),
    b(function(BA,b(minus(IdX1,WidthAP1),integer,[])),integer,[])),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id(extract(I,J)),[S]),Env,Out) :- !,
    BI = b(integer(I),integer,[]),
    BJ = b(integer(J),integer,[]),
    smt_term_to_prob_term(S,Env,BS),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    DomX1 = b(add(b(minus(BI,BJ),integer,[]),Int1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,DomX1),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(function(BS,IdX1),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id('bvnot'),[A]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    bvwidth(BA,Width),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int1,Int0),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id('bvand'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int0),pred,[]),Int0,b(function(BB,IdX1),integer,[])),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id('bvor'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),Int1),pred,[]),Int1,b(function(BB,IdX1),integer,[])),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id('bvxor'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    Int0 = b(integer(0),integer,[]),
    Int1 = b(integer(1),integer,[]),
    IdX1 = b(identifier('\\tmp1'),integer,[]),
    IdX2 = b(identifier('\\tmp2'),integer,[]),
    TypeOfX1 = b(member(IdX1,b(interval(Int0,Width),set(integer),[])),pred,[]),
    TypeOfX2 = b(member(IdX2,b(interval(Int0,Int1),set(integer),[])),pred,[]),
    ValOfX2 = b(if_then_else(b(equal(b(function(BA,IdX1),integer,[]),b(function(BB,IdX1),integer,[])),pred,[]),Int0,Int1),integer,[]),
    conjunct_predicates([TypeOfX1,TypeOfX2,b(equal(IdX2,ValOfX2),pred,[])],Pred),
    Out = b(comprehension_set([IdX1,IdX2],Pred),set(couple(integer,integer)),[]).

smt_term_to_prob_term(id_term(id('bvult'),[A,B]),Env,Out) :- !,
    bv_to_nat_and_compare(A,B,less,Env,Out).

smt_term_to_prob_term(id_term(id('bvule'),[A,B]),Env,Out) :- !,
    bv_to_nat_and_compare(A,B,less_equal,Env,Out).

smt_term_to_prob_term(id_term(id('bvuge'),[A,B]),Env,Out) :- !,
    bv_to_nat_and_compare(A,B,greater_equal,Env,Out).

smt_term_to_prob_term(id_term(id('bvugt'),[A,B]),Env,Out) :- !,
    bv_to_nat_and_compare(A,B,greater,Env,Out).

smt_term_to_prob_term(id_term(id('bvslt'),[A,B]),Env,Out) :- !,
    signed_bv_to_nat_and_compare(A,B,less,Env,Out).

smt_term_to_prob_term(id_term(id('bvsle'),[A,B]),Env,Out) :- !,
    signed_bv_to_nat_and_compare(A,B,less_equal,Env,Out).

smt_term_to_prob_term(id_term(id('bvsge'),[A,B]),Env,Out) :- !,
    signed_bv_to_nat_and_compare(A,B,greater_equal,Env,Out).

smt_term_to_prob_term(id_term(id('bvsgt'),[A,B]),Env,Out) :- !,
    signed_bv_to_nat_and_compare(A,B,greater,Env,Out).

smt_term_to_prob_term(id_term(id('bvneg'),[A]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    bvwidth(BA,Width),
    WidthP1 = b(add(Width,b(integer(1),integer,[])),integer,[]),
    bv2nat(BA,BANat),
    Int2 = b(integer(2),integer,[]),
    Pow = b(power_of(Int2,WidthP1),integer,[]),
    Differenz = b(minus(Pow,BANat),integer,[]),
    nat2bv(Differenz,Width,Out).

smt_term_to_prob_term(id_term(id('bvadd'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Sum = b(add(BANat,BBNat),integer,[]),
    nat2bv(Sum,Width,Out).

smt_term_to_prob_term(id_term(id('bvsub'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Sum = b(minus(BANat,BBNat),integer,[]),
    nat2bv(Sum,Width,Out).

smt_term_to_prob_term(id_term(id('bvmul'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Prod = b(multiplication(BANat,BBNat),integer,[]),
    nat2bv(Prod,Width,Out).

smt_term_to_prob_term(id_term(id('bvudiv'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Div = b(div(BANat,BBNat),integer,[]),
    nat2bv(Div,Width,Out).

smt_term_to_prob_term(id_term(id('bvurem'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Rem = b(modulo(BANat,BBNat),integer,[]),
    nat2bv(Rem,Width,Out).

smt_term_to_prob_term(id_term(id('bvshl'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Int2 = b(integer(2),integer,[]),
    Exp = b(power_of(Int2,BBNat),integer,[]),
    Res = b(multiplication(BANat,Exp),integer,[]),
    nat2bv(Res,Width,Out).

smt_term_to_prob_term(id_term(id('bvlshr'),[A,B]),Env,Out) :- !,
    smt_term_to_prob_term(A,Env,BA),
    smt_term_to_prob_term(B,Env,BB),
    bvwidth(BA,Width),
    bv2nat(BA,BANat),
    bv2nat(BB,BBNat),
    Int2 = b(integer(2),integer,[]),
    Exp = b(power_of(Int2,BBNat),integer,[]),
    Res = b(div(BANat,Exp),integer,[]),
    nat2bv(Res,Width,Out).

smt_term_to_prob_term(id_term(id(div),[Dividend|Divisors]),Env,Out) :- !,
    smt_term_to_prob_term(id_term(id('*'),Divisors),Env,BDivisor),
    smt_term_to_prob_term(Dividend,Env,BDividend),
    Zero = b(integer(0),integer,[]),
    DividendLessZero = b(less(BDividend,Zero),pred,[]),
    DivisorLessZero = b(less(BDivisor,Zero),pred,[]),
    DivisorGreaterZero = b(greater(BDivisor,Zero),pred,[]),
    DivisorMinusOne = b(minus(BDivisor,b(integer(1),integer,[])),integer,[]),
    DivisorPlusOne = b(add(BDivisor,b(integer(1),integer,[])),integer,[]),
    MinusDivisorPlusOne = b(unary_minus(DivisorPlusOne),integer,[]),
   
    conjunct_predicates([DividendLessZero,DivisorGreaterZero],If1),
    conjunct_predicates([DividendLessZero,DivisorLessZero],If2),
   
    FixInner = b(if_then_else(If2,MinusDivisorPlusOne,Zero),integer,[]),
    Fix = b(if_then_else(If1,DivisorMinusOne,FixInner),integer,[]),
    NewBDividend = b(minus(BDividend,Fix),integer,[]),
    Out = b(div(NewBDividend,BDivisor),integer,[]).

smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :-
    smt_id_to_prob_id_preds(Id,BId), !,
    maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs),
    maplist(bool_to_pred,BArgs,PredBArgs),
    interleave(BId,PredBArgs,Out).

smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :-
    smt_id_to_prob_id(Id,BId,ConnectingPred), !,
    maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs),
    call(ConnectingPred,BId,BArgs,Out).

smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :-
    get_function(Id,Env,Params,_Results,Definition), !,
    replace_identifiers(Params,Args,Definition,Out,Env).

smt_term_to_prob_term(id_term(id(Id),Args),Env,Out) :-
    get_type(Id,Env,set(couple(_X,Y))), !,
    smt_term_to_prob_term(id(Id),Env,BId),
    maplist(smt_term_to_prob_term_maplist(Env),Args,BArgs),
    create_couple(BArgs,BArg),
    Out = b(function(BId,BArg),Y,[]).

smt_term_to_prob_term(id(true),_,b(boolean_true,boolean,[])) :- !.

smt_term_to_prob_term(id(false),_,b(boolean_false,boolean,[])) :- !.

smt_term_to_prob_term(id(Id),Env,OutId) :- !,
    get_type(Id,Env,Type),
    OutId = b(identifier(Id),Type,[]).%,

smt_term_to_prob_term(id(Id,Sort),Env,OutId) :- !,
    smt_type_to_prob_type(Sort,Env,Type),
    OutId = b(identifier(Id),Type,[]).

smt_term_to_prob_term(svar(Id,Sort),Env,Out) :- !,
    smt_type_to_prob_type(Sort,Env,Type),
    Out = b(identifier(Id),Type,[]).

smt_term_to_prob_term(integer(I),_,b(integer(I),integer,[])) :- !.

smt_term_to_prob_term(let(Bindings,Term),Env,BTerm) :- !,
    let_equalities_and_bids(Bindings,BIDs,Assignments,Env),
    create_local_env(Env,BIDs,LocalEnv),
    smt_term_to_prob_term(Term,LocalEnv,InnerBTerm),
    get_texpr_type(InnerBTerm,InnerType),
    (InnerType = pred
    -> safe_create_texpr(let_predicate(BIDs,Assignments,InnerBTerm),pred,BTerm)
    ; safe_create_texpr(let_expression(BIDs,Assignments,InnerBTerm),InnerType,BTerm)).

smt_term_to_prob_term(forall(IDs,Term),Env,Forall) :- !,
    maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers),
    create_local_env(Env,Identifiers,LocalEnv),
    smt_term_to_prob_term(Term,LocalEnv,InnerTerm),
    convlist(typing_constraint,IDs,InnerConstraints),
    bool_to_pred(InnerTerm,InnerTermAsPred), % necessary ??
    conjunct_predicates(InnerConstraints,LHS),
    create_implication(LHS,InnerTermAsPred,Body),
    create_forall(Identifiers,Body,Forall).

smt_term_to_prob_term(exists(IDs,Term),Env,Forall) :- !,
    maplist(smt_term_to_prob_term_maplist(Env),IDs,Identifiers),
    create_local_env(Env,Identifiers,LocalEnv),
    smt_term_to_prob_term(Term,LocalEnv,InnerTerm),
    convlist(typing_constraint,IDs,InnerConstraints),
    append(InnerConstraints,[InnerTerm],IList),
    conjunct_predicates(IList,Inner),
    bool_to_pred(Inner,InnerAsPred),
    create_exists(Identifiers,InnerAsPred,Forall).

smt_term_to_prob_term(bitvector(Value,Length),_Env,Out) :- !,
    integer_to_binary_couples(Value,Length,Couples),
    Out = b(set_extension(Couples),set(couple(integer,integer)),[]).

smt_term_to_prob_term(bitvector(Bits),_Env,Out) :- !,
    binary_to_binary_couples(Bits,Couples),
    Out = b(set_extension(Couples),set(couple(integer,integer)),[]).

smt_term_to_prob_term(X,_,_) :-
    add_error(smtlib2_translation,'Unsupported term in smt_term_to_prob_term:',X), fail.

smt_term_to_prob_term_maplist(E,I,O) :-
    smt_term_to_prob_term(I,E,O).

smt_type_to_prob_type(sort('Int'),_,integer) :- !.

smt_type_to_prob_type(sort('Bool'),_,boolean) :- !.

smt_type_to_prob_type(sort('Array',[From,sort('Bool')]),E,Out) :-
    get_preference(smtlib2b_arrays_as_sets,true),
    !, % we could translate arrays to Bool as sets
    smt_type_to_prob_type(From,E,FromType),
    Out = set(FromType).

smt_type_to_prob_type(sort('Array',[From,To]),E,Out) :- !,
    %format('Sort Array ~w to ~w~n',[From,To]),nl,
    smt_type_to_prob_type(From,E,FromType),
    smt_type_to_prob_type(To,E,ToType),
    Out = set(couple(FromType,ToType)).

smt_type_to_prob_type(sort('BitVec',[_Length]),_E,Out) :- !,
    Out = set(couple(integer,integer)).

smt_type_to_prob_type(sort('Set',[Sub]),E,Out) :- !,
    smt_type_to_prob_type(Sub,E,SubType),
    Out = set(SubType).

smt_type_to_prob_type(sort(X),E,global(X)) :-
    is_custom_type(E,X), !.

smt_type_to_prob_type(X,_,_) :- !,
    add_error(smtlib2_translation,'Unsupported sort in smt_type_to_prob_type:',X), fail.

smt_type_to_prob_type_maplist(E,I,O) :-
    smt_type_to_prob_type(I,E,O).

to_bool_if_necessary(PossiblePred,Bool) :-
    get_texpr_type(PossiblePred,pred), !,
    safe_create_texpr(convert_bool(PossiblePred),boolean,Bool).

to_bool_if_necessary(NonPred,NonPred).

type_to_expr(set(A),Res) :- !, Res = b(pow_subset(AE),set(set(A)),[]),
    type_to_expr(A,AE).

type_to_expr(couple(A,B),b(cartesian_product(AE,BE),set(couple(AET,BET)),[])) :- !,
    type_to_expr(A,AE), type_to_expr(B,BE),
    get_texpr_type(AE,AET), get_texpr_type(BE,BET).

type_to_expr(integer,b(integer_set('INTEGER'),set(integer),[])) :- !.

type_to_expr(boolean,b(bool_set,set(boolean),[])) :- !.

type_to_expr(global(E),b(identifier(E),set(global(E)),[])) :- !.

type_to_expr(T,_) :-
    add_error(smtlib2_translation,'Unsupported type in type_to_expr:',T), fail.

typing_constraint(svar(Name,sort('Array',[Index,Element])),Constraint) :-
    smt_type_to_prob_type(Index,EIn,BIndex),
    smt_type_to_prob_type(Element,EIn,BElement),
    Identifier = b(identifier(Name),FullType,[]),
    Constraint = b(member(Identifier,b(EXPR,set(FullType),[])),pred,[]),
    type_to_expr(BIndex,From),
    (BElement=boolean,get_preference(smtlib2b_arrays_as_sets,true) % we translate boolean Array as Set
    -> EXPR = pow_subset(From),
    FullType = set(BIndex)
    ; type_to_expr(BElement,To),
    EXPR=total_function(From,To),
    FullType = set(couple(BIndex,BElement))
).

typing_constraint(svar(Name,sort('BitVec',[Length])),Constraint) :-
    Zero = b(integer(0),integer,[]),
    One = b(integer(1),integer,[]),
    L2 is Length - 1,
    LengthMinusOne = b(integer(L2),integer,[]),
    FullType = set(couple(integer,integer)),
    Identifier = b(identifier(Name),FullType,[]),
    From = b(interval(Zero,LengthMinusOne),set(integer),[]),
    To = b(interval(Zero,One),set(integer),[]),
    Constraint = b(member(Identifier,b(total_function(From,To),set(FullType),[])),pred,[]).