rewrite_pre(if_then_else(If,Then,Else),IsWd,Type,I,NExpr,Type,NI,multi/rewrite_if_then_else_expr,[],[]) :-
IsWd == 'FALSE',
Type \== pred,
!, % rewrite if-then-else expression in order to add WD POs afterwards; all other WD POs are handled by add_wd_pos_to_pred/7
% this has nothing to do with seq rewriting but is faster since the AST is already traversed here and seq rewriting is the first step of preprocessing for Z3
rewrite_if_then_else_expr_to_b(if_then_else(If,Then,Else), NExpr),
NI = I.
rewrite_pre(let_expression(Ids,Exprs,Body),IsWd,Type,_,Unfolded,Type,NI,multi/unfold_let_expression,[],[]) :-
IsWd == 'FALSE',
!, % expand LET expression as a special case in order to add WD POs afterwards; all other WD POs are handled by add_wd_pos_to_pred/7
% see above
replace_ids_by_exprs(Body, Ids, Exprs, b(Unfolded,_,NI)).
rewrite_pre(empty_sequence,_,seq(T),I,empty_set,set(couple(integer,T)),I,multi/empty_sequence_to_set,[],[]).
rewrite_pre(general_concat(A),_,Type,I,empty_set,set(couple(integer,T)),I,multi/empty_general_concat,[],[]) :-
( A = b(empty_sequence,_,_); A = b(empty_set,_,_)),
( Type = seq(T); Type = set(couple(integer,T))).
rewrite_pre(sequence_extension(SeqExtValues),_,SType,I,set_extension(SetExtValues),set(couple(integer,Type)),I,multi/seq_ext_to_set_ext,[],[]) :-
( SType = seq(Type)
; SType = set(couple(integer,Type))
),
seq_ext_to_set_ext(SeqExtValues,1,Type,SetExtValues).
rewrite_pre(seq(S),_,set(seq(Type)),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
unique_typed_id("_smt_tmp",integer,N),
unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
% f : NATURAL1 +-> S
safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
safe_create_texpr(member(F,PartFunc),pred,FMember),
safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
safe_create_texpr(domain(F),set(integer),Dom),
safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
create_exists([N],ExistsInner,Exists),
conjunct_predicates([Exists,FMember],Pred).
rewrite_pre(seq1(S),_,set(seq(Type)),I,comprehension_set([F],Pred),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
unique_typed_id("_smt_tmp",integer,N),
unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
% f : NATURAL1 +-> S
safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
safe_create_texpr(member(F,PartFunc),pred,FMember),
safe_create_texpr(member(N,b(integer_set('NATURAL1'),set(integer),[])),pred,NMember),
safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
safe_create_texpr(domain(F),set(integer),Dom),
safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
create_exists([N],ExistsInner,Exists),
conjunct_predicates([Exists,FMember],Pred).
rewrite_pre(iseq(S),_,set(seq(Type)),I,intersection(CompSet,PartInj),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
unique_typed_id("_smt_tmp",integer,N),
unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
% f : NATURAL1 +-> S
safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
safe_create_texpr(member(F,PartFunc),pred,FMember),
safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
safe_create_texpr(domain(F),set(integer),Dom),
safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
create_exists([N],ExistsInner,Exists),
conjunct_predicates([Exists,FMember],Pred),
safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet),
safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj).
rewrite_pre(perm(S),_,set(seq(Type)),I,intersection(CompSet,Intersec),set(set(couple(integer,Type))),I,multi/rewrite_seq,[],[]) :-
unique_typed_id("_smt_tmp",integer,N),
unique_typed_id("_smt_tmp",set(couple(integer,Type)),F),
% f : NATURAL1 +-> S
safe_create_texpr(partial_function(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartFunc),
safe_create_texpr(member(F,PartFunc),pred,FMember),
safe_create_texpr(member(N,b(integer_set('NATURAL'),set(integer),[])),pred,NMember),
safe_create_texpr(interval(b(integer(1),integer,[]),N),set(integer),Interval),
safe_create_texpr(domain(F),set(integer),Dom),
safe_create_texpr(equal(Dom,Interval),pred,DomIsEqualToInterval),
conjunct_predicates([NMember,DomIsEqualToInterval],ExistsInner),
create_exists([N],ExistsInner,Exists),
conjunct_predicates([Exists,FMember],Pred),
safe_create_texpr(comprehension_set([F],Pred),set(set(couple(integer,Type))),CompSet),
safe_create_texpr(partial_injection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),PartInj),
safe_create_texpr(partial_surjection(b(integer_set('NATURAL1'),set(integer),[]),S),set(set(couple(integer,Type))),TotalSurj),
safe_create_texpr(intersection(PartInj,TotalSurj),pred,Intersec).
rewrite_pre(size(S),_,integer,I,UnwrappedId,integer,I,multi/rewrite_size,[AC1,AC2],[UId]) :-
unique_typed_id("_smt_tmp",integer,UId),
get_texpr_expr(UId,UnwrappedId),
% two axioms:
% !(i,v).((i,v) : Set => uid >= x)
% uid=0 or #(i,v).((i,v) : Set & uid = x)
% Note: #(i,v) FAILS if set is empty
unique_typed_id("_smt_tmp",integer,Index),
get_texpr_type(S,Type),
get_set_type(Type,couple(integer,SeqType)),
unique_typed_id("_smt_tmp",SeqType,Value),
safe_create_texpr(couple(Index,Value),couple(integer,SeqType),QuantifiedVar),
safe_create_texpr(greater_equal(UId,Index),pred,GreaterEqual),
safe_create_texpr(equal(UId,Index),pred,Equal),
safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet),
safe_create_texpr(integer(0),integer,Zero),
safe_create_texpr(equal(UId,Zero),pred,EqualZero),
conjunct_predicates([QuantifiedInSet,Equal],ExistsInner),
create_implication(QuantifiedInSet,GreaterEqual,ForallInner),
create_exists([Index,Value],ExistsInner,AC0),
disjunct_predicates([EqualZero,AC0],AC1),
create_forall([Index,Value],ForallInner,AC2).
rewrite_pre(first(A),_,Type,I,function(A,b(integer(1),integer,[])),Type,I,multi/rewrite_first,[],[]).
rewrite_pre(last(A),_,Type,I,function(A,Card),Type,I,multi/rewrite_last,[],[]) :-
safe_create_texpr(size(A),integer,Card).
rewrite_pre(rev(S),_,seq(Type),I,comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),I,multi/rewrite_rev,[AC1],[TmpCard]) :-
% {(i,v) | (card(S)-i+1,b) : x}
safe_create_texpr(size(S),integer,Card),
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
% size is stored outside of the set comprehension using a temp. identifier
% to increase performance
unique_typed_id("_smt_tmp",integer,TmpCard),
safe_create_texpr(equal(TmpCard,Card),pred,AC1),
safe_create_texpr(minus(TmpCard,Index),integer,TmpIndex),
safe_create_texpr(add(TmpIndex,b(integer(1),integer,[])),integer,NIndex),
safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet).
rewrite_pre(concat(S1,S2),_,seq(Type),I,comprehension_set([Index,Value],Disjunct),set(couple(integer,Type)),I,multi/rewrite_concat,[AC1],[TmpCard]) :-
% {(i,v) | (i,v) : S1 or (i-card(S1),v) : S2}
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
safe_create_texpr(size(S1),integer,Card1),
% size is stored outside of the set comprehension using a temp. identifier
% to increase performance
unique_typed_id("_smt_tmp",integer,TmpCard),
safe_create_texpr(equal(TmpCard,Card1),pred,AC1),
safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar),
% (i,v) : S1
safe_create_texpr(member(QuantifiedVar,S1),pred,QuantifiedInSet1),
% (i-card(S1),v) : S2
safe_create_texpr(minus(Index,TmpCard),integer,NIndex),
safe_create_texpr(couple(NIndex,Value),couple(integer,Type),QuantifiedVar2),
safe_create_texpr(member(QuantifiedVar2,S2),pred,QuantifiedInSet2),
disjunct_predicates([QuantifiedInSet1,QuantifiedInSet2],Disjunct).
rewrite_pre(restrict_front(S,N),_,seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_front,[],[]) :-
% {(i,v) | (i,v) : S & i <= N}
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
safe_create_texpr(couple(Index,Value),couple(integer,Type),QuantifiedVar),
% (i,v) : S
safe_create_texpr(member(QuantifiedVar,S),pred,QuantifiedInSet),
% i <= N
safe_create_texpr(less_equal(Index,N),pred,LessEqual),
conjunct_predicates([QuantifiedInSet,LessEqual],Conjunct).
rewrite_pre(restrict_tail(S,N),_,seq(Type),I,SExpr,set(couple(integer,Type)),I,multi/rewrite_restrict_tail_special,[],[]) :-
get_texpr_expr(N,integer(0)), !,
get_texpr_expr(S,SExpr).
rewrite_pre(restrict_tail(S,N),_,seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_restrict_tail,[],[]) :-
% {(i,v) | (i+N,v) : S & i > 0}
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
%create_texpr(couple(Index,Value),couple(integer,Type),[],AC),
% NIndex = i+N
create_texpr(add(N,Index),integer,[],NIndex),
safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
% i > 0
safe_create_texpr(integer(0),integer,Null),
safe_create_texpr(greater(Index,Null),pred,GreaterEqual),
conjunct_predicates([QuantifiedInSet,GreaterEqual],Conjunct).
rewrite_pre(insert_front(E,S),_,seq(Type),I,union(AC,CompSet),set(couple(integer,Type)),I,multi/rewrite_insert_front,[],[]) :-
% {(i,v) | (i-1,v) : S or (i = 1 & v = E)}
% easier to code: {(i,v) | (i-1,v) : S} \/ {(1,E)}
% {(1,E)}
safe_create_texpr(set_extension([b(couple(b(integer(1),integer,[]),E),couple(integer,Type),[])]),set(couple(integer,Type)),AC),
% {(i,v) | (i-1,v) : S}
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
safe_create_texpr(minus(Index,b(integer(1),integer,[])),integer,NIndex),
safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
safe_create_texpr(comprehension_set([Index,Value],QuantifiedInSet),set(couple(integer,Type)),CompSet).
rewrite_pre(insert_tail(S,E),_,seq(Type),I,union(S,AC),set(couple(integer,Type)),I,multi/rewrite_insert_tail,[],[]) :-
% NIndex = size(S)+1
safe_create_texpr(size(S),integer,Card),
safe_create_texpr(add(Card,b(integer(1),integer,[])),integer,NIndex),
% AC = {(NIndex,E)}
safe_create_texpr(set_extension([b(couple(NIndex,E),couple(integer,Type),[])]),set(couple(integer,Type)),AC).
rewrite_pre(front(A),_,seq(Type),I,set_subtraction(A,AC),set(couple(integer,Type)),I,multi/rewrite_front,[],[]) :-
safe_create_texpr(size(A),integer,Card),
safe_create_texpr(function(A,Card),Type,Last),
% AC = {(size(A),function(A,size(A)))}
safe_create_texpr(set_extension([b(couple(Card,Last),couple(integer,Type),[])]),set(couple(integer,Type)),AC).
rewrite_pre(tail(S),_,seq(Type),I,comprehension_set([Index,Value],Conjunct),set(couple(integer,Type)),I,multi/rewrite_tail,[],[]) :-
% {(i,v) | (i+1,v) : S & i > 0}
unique_typed_id("_smt_tmp",integer,Index),
unique_typed_id("_smt_tmp",Type,Value),
% (i+1,v) : S
safe_create_texpr(add(Index,b(integer(1),integer,[])),integer,NIndex),
safe_create_texpr(couple(NIndex,Value),couple(integer,Type),TheCouple),
safe_create_texpr(member(TheCouple,S),pred,QuantifiedInSet),
% i > 0
safe_create_texpr(greater(Index,b(integer(0),integer,[])),pred,Greater),
conjunct_predicates([QuantifiedInSet,Greater],Conjunct).
rewrite_pre(A,_,TypeIn,I,A,TypeOut,I,multi/replace_seq_type_by_set_type,[],[]) :-
normalize_type(TypeIn,TypeOut), TypeIn \= TypeOut.