mk_expr_aux(first_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
get_texpr_type(Couple, CoupleType),
mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, first, AE, CoupleType, Expr)).
mk_expr_aux(second_of_pair(Couple), _, TranslationType, Solver, LS, GS, Expr) :-
get_texpr_type(Couple, CoupleType),
mk_expr(Couple, TranslationType, Solver, LS, GS, AE),
smt_solver_interface_call(Solver, mk_op_couple_prj(TranslationType, second, AE, CoupleType, Expr)).
mk_expr_aux(interval(A1,A2), _, TranslationType, Solver, LS, GS, Expr) :-
!,
mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
smt_solver_interface_call(Solver, mk_op_interval(TranslationType, AE1, AE2, Expr)).
mk_expr_aux(direct_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleOutType),
CoupleOutType = couple(_,Couple2Type),
mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
Arg1 = b(_,set(CoupleType1),_),
Arg2 = b(_,set(CoupleType2),_),
smt_solver_interface_call(Solver, mk_op_direct_product(TranslationType, Arg1E, Arg2E, Couple2Type, CoupleType1, CoupleType2, CoupleOutType, Expr)).
mk_expr_aux(parallel_product(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleOutType),
mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
Arg1 = b(_,set(CoupleType1),_),
Arg2 = b(_,set(CoupleType2),_),
CoupleOutType = couple(ExistsCoupleType1,ExistsCoupleType2),
smt_solver_interface_call(Solver, mk_op_parallel_product(TranslationType, Arg1E, Arg2E, CoupleType1, CoupleType2, ExistsCoupleType1, ExistsCoupleType2, CoupleOutType, Expr)).
mk_expr_aux(composition(Arg1,Arg2), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleOutType),
Arg1 = b(_,set(CoupleType1),_),
CoupleType1 = couple(A,B),
Arg2 = b(_,set(CoupleType2),_),
CoupleType2 = couple(B,C),
CoupleOutType = couple(A,C),
mk_expr(Arg1, TranslationType, Solver, LS, GS, Arg1E),
mk_expr(Arg2, TranslationType, Solver, LS, GS, Arg2E),
smt_solver_interface_call(Solver, mk_op_composition(TranslationType, Arg1E, Arg2E, B, CoupleType1, CoupleType2, CoupleOutType, Expr)).
mk_expr_aux(cartesian_product(A1,A2), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleType),
mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
smt_solver_interface_call(Solver, mk_op_cartesian(TranslationType, AE1, AE2, CoupleType, Expr)).
mk_expr_aux(identity(A), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleType),
CoupleType = couple(InnerSetType,_),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
smt_solver_interface_call(Solver, mk_op_identity(TranslationType, AE, InnerSetType, CoupleType, Expr)).
mk_expr_aux(reverse(A), Type, TranslationType, Solver, LS, GS, Expr) :-
!,
Type = set(CoupleType),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
smt_solver_interface_call(Solver, mk_op_reverse(TranslationType, AE, CoupleType, Expr)).
mk_expr_aux(comprehension_set(Args,Body), Type, TranslationType, Solver, LS, GS, Expr) :-
LambdaId = b(identifier('_lambda_result_'),_,_),
select(LambdaId, Args, LambdaArgs),
create_bounded_smt_state(TranslationType, Solver, LambdaArgs, State, ArgsE),
ArgsE = [Arg],
append(State, LS, NLS),
conjunction_to_list(Body, ConjList),
select(b(equal(LambdaId,BodyExpr),pred,Info), ConjList, RestConjList),
member(prob_annotation('LAMBDA-EQUALITY'), Info),
conjunct_predicates(RestConjList, BodyPred),
Type = set(CoupleType),
!,
mk_expr(BodyExpr, TranslationType, Solver, NLS, GS, BodyE),
mk_expr(BodyPred, TranslationType, Solver, NLS, GS, BodyP),
smt_solver_interface_call(Solver, mk_op_lambda(TranslationType, Arg, BodyP, BodyE, CoupleType, Expr)).
mk_expr_aux(comprehension_set(Args,Body), _, TranslationType, Solver, LS, GS, Expr) :-
!,
create_bounded_smt_state(TranslationType, Solver, Args, State, ArgsE),
append(State, LS, NLS),
mk_expr(Body, TranslationType, Solver, NLS, GS, BodyE),
length(ArgsE, ArgAmount),
( ArgAmount == 1
-> ArgsE = [Arg],
smt_solver_interface_call(Solver, mk_op_comprehension_set_singleton(TranslationType, Arg, BodyE, Expr))
; get_couple_types_comp_args(Args, CoupleTypes),
smt_solver_interface_call(Solver, mk_op_comprehension_set_multi(TranslationType, ArgsE, CoupleTypes, BodyE, Expr))
).
mk_expr_aux(image(A,B), _, TranslationType, Solver, LS, GS, Expr) :-
!,
A = b(_,set(couple(Prj1Type,Prj2Type)),_),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
mk_expr(B, TranslationType, Solver, LS, GS, BE),
smt_solver_interface_call(Solver, mk_op_image(TranslationType, AE,BE,couple(Prj1Type,Prj2Type),Prj1Type,Prj2Type,Expr)).
mk_expr_aux(conjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
conjunction_to_list(b(conjunct(A,B),pred,[]),List),
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList), % apply mk_expr on List
% truth/0 are removed from the conjunction during list / from list
% the list might be empty now!
( ExprList = []
-> smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr))
; ( ExprList = [X]
-> Expr = X
; smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,ExprList,Expr))
)
).
mk_expr_aux(disjunct(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
disjunction_to_list(b(disjunct(A,B),pred,[]),List),
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,ExprList),
smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, disjunct,ExprList,Expr)).
mk_expr_aux(if_then_else(Pred,A,B),_,TranslationType, Solver,LS,GS,Expr) :-
!,
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),[Pred,A,B],ArgList),
smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, if_then_else,ArgList,Expr)).
mk_expr_aux(partition(S,Sets),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
% definition: sets are disjoint and S is the union
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),Sets,SetExprs),
pairwise_union(TranslationType,SetExprs,Solver,UnionOfSets),
mk_expr(S,TranslationType, Solver,LS,GS,SExpr),
smt_solver_interface_call(Solver,mk_op(TranslationType, equal,SExpr,UnionOfSets,EqualToUnion)), % S = Union(Sets)
% enforce sets pairwise disjoint (= intersection is empty)
get_texpr_type(S,Type),
smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,EmptySet)),
pairwise_disjoint(TranslationType,SetExprs,Solver,EmptySet,PWConstraint),
smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, conjunct,[EqualToUnion,PWConstraint],Expr)).
mk_expr_aux(forall(IDs,b(truth,pred,_),B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
append(State,LS,NLS),
mk_expr(B,TranslationType, Solver,NLS,GS,BE),
smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,BE,Expr)).
mk_expr_aux(forall(IDs,A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
append(State,LS,NLS),
mk_expr(A,TranslationType, Solver,NLS,GS,AE), mk_expr(B,TranslationType, Solver,NLS,GS,BE),
smt_solver_interface_call(Solver,mk_op(TranslationType, implication,AE,BE,InnerExpr)),
smt_solver_interface_call(Solver,mk_quantifier(TranslationType, forall,SMTExprs,InnerExpr,Expr)).
mk_expr_aux(exists(IDs,B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
create_bounded_smt_state(TranslationType, Solver,IDs,State,SMTExprs),
append(State,LS,NLS),
mk_expr(B,TranslationType, Solver,NLS,GS,InnerExpr),
smt_solver_interface_call(Solver,mk_quantifier(TranslationType, exists,SMTExprs,InnerExpr,Expr)).
mk_expr_aux(equal(A,B),pred,TranslationType, Solver,LS,GS,Expr) :-
!,
mk_expr(A,TranslationType, Solver,LS,GS,AE),
mk_expr(B,TranslationType, Solver,LS,GS,BE),
get_texpr_type(A,Type),
( Type = boolean
-> smt_solver_interface_call(Solver, mk_op(TranslationType, equivalence, AE, BE, Expr))
; smt_solver_interface_call(Solver, mk_op(TranslationType, equal, AE, BE, Expr))
).
mk_expr_aux(convert_int_floor(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
!,
number_codes(RealExpr, ECodes),
append([102,108,111,111,114], ECodes, EECodes),
atom_codes(EAtom, EECodes),
( is_ground_real(Real)
-> IsGroundArg = 1
; IsGroundArg = 0
),
smt_solver_interface_call(Solver,mk_op_floor(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).
mk_expr_aux(convert_int_ceiling(Real),integer,TranslationType, Solver,LS,GS,Expr) :-
mk_expr(Real, TranslationType, Solver, LS, GS, RealExpr),
!,
number_codes(RealExpr, ECodes),
append([99,101,105,108,105,110,103], ECodes, EECodes),
atom_codes(EAtom, EECodes),
( is_ground_real(Real)
-> IsGroundArg = 1
; IsGroundArg = 0
),
smt_solver_interface_call(Solver,mk_op_ceiling(TranslationType,IsGroundArg,EAtom,RealExpr,Expr)).
mk_expr_aux(rec(ListOfFields),Type,TranslationType, Solver,LS,GS,Expr) :-
!,
findall(FieldExpr, member(field(_,FieldExpr),ListOfFields), FieldExprs),
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),FieldExprs,SMTFieldExprs),
smt_solver_interface_call(Solver,mk_record_const(TranslationType, Type,SMTFieldExprs,Expr)).
mk_expr_aux(record_field(Record,FieldName),Type,TranslationType, Solver,LS,GS,Expr) :-
!,
get_texpr_type(Record,record(RFields)),
nth0(FieldNr,RFields,field(FieldName,Type)),
% debug_format(9,'Field: ~w Type: ~w~n-> FieldNr: ~w~n',[FieldName,RFields,FieldNr]),
mk_expr(Record,TranslationType, Solver,LS,GS,SMTRecordExpr),
smt_solver_interface_call(Solver,mk_record_field(TranslationType, SMTRecordExpr,FieldNr,Expr)).
mk_expr_aux(couple(A,B),Type,TranslationType, Solver,LS,GS,Expr) :-
!,
mk_expr(A,TranslationType, Solver,LS,GS,AE),
mk_expr(B,TranslationType, Solver,LS,GS,BE),
smt_solver_interface_call(Solver,mk_couple(TranslationType, Type,AE,BE,Expr)).
mk_expr_aux(identifier(Id),_,_,_Solver,LS,GS,Expr) :-
!,
lookup(Id,LS,GS,Expr).
mk_expr_aux(real(RealAtom),real,TranslationType, Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_real_const(TranslationType, RealAtom,Expr)).
mk_expr_aux(integer(Int),integer,TranslationType, Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_int_const(TranslationType, Int,Expr)).
mk_expr_aux(min_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
!,
get_preference(minint,MinInt),
smt_solver_interface_call(Solver,mk_int_const(TranslationType, MinInt,Expr)).
mk_expr_aux(max_int,integer,TranslationType, Solver,_LS,_GS,Expr) :-
!,
get_preference(maxint,MaxInt),
smt_solver_interface_call(Solver,mk_int_const(TranslationType, MaxInt,Expr)).
mk_expr_aux(boolean_true,boolean,_,Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
mk_expr_aux(boolean_false,boolean,_,Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
mk_expr_aux(string(S),string,TranslationType,Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_string_const(TranslationType, S,Expr)).
mk_expr_aux(truth,pred,_,Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_bool_const(boolean_true,Expr)).
mk_expr_aux(falsity,pred,_,Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_bool_const(boolean_false,Expr)).
mk_expr_aux(bool_set,set(boolean),TranslationType, Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_bool_const(boolean_true,True)),
smt_solver_interface_call(Solver,mk_bool_const(boolean_false,False)),
smt_solver_interface_call(Solver,mk_set(TranslationType, [True,False],Expr)).
mk_expr_aux(set_extension(List),set(T),TranslationType, Solver,LS,GS,Expr) :-
!,
maplist(mk_expr_maplist(TranslationType, Solver,LS,GS),List,SubExprs),
( SubExprs = []
-> smt_solver_interface_call(Solver,mk_empty_set(TranslationType, set(T),Expr))
; smt_solver_interface_call(Solver,mk_set(TranslationType, SubExprs,Expr))
).
mk_expr_aux(empty_set,Type,TranslationType, Solver,_LS,_GS,Expr) :-
!,
smt_solver_interface_call(Solver,mk_empty_set(TranslationType, Type,Expr)).
mk_expr_aux(value(V),Type,TranslationType, Solver,LS,GS,Expr) :-
!,
mk_value(Type,V,TranslationType, Solver,LS,GS,Expr).
mk_expr_aux(convert_bool(P),boolean,TranslationType, Solver,LS,GS,Expr) :-
!,
mk_expr(P,TranslationType, Solver,LS,GS,Expr).
mk_expr_aux(let_expression(ListOfIDs,ListOfDefinitions,LetExpression),_Type,TranslationType, Solver,LS,GS,Expr) :-
create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
!,
mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).
mk_expr_aux(let_predicate(ListOfIDs,ListOfDefinitions,LetExpression),pred,TranslationType, Solver,LS,GS,Expr) :-
create_let_state(ListOfIDs,ListOfDefinitions,TranslationType, Solver,LS,GS,NewLS),
!,
mk_expr(LetExpression,TranslationType, Solver,NewLS,GS,Expr).
mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
functor(Op, Functor, 1),
(Functor == pow_subset; Functor == pow1_subset; Functor == fin_subset; Functor == fin1_subset),
!,
arg(1, Op, A),
Type = set(set(InnerSetType)),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
( Functor == pow_subset
-> smt_solver_interface_call(Solver, mk_op_pow_subset(TranslationType, AE, set(InnerSetType), Expr))
; Functor == pow1_subset
-> smt_solver_interface_call(Solver, mk_op_pow1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
; Functor == fin_subset
-> smt_solver_interface_call(Solver, mk_op_fin_subset(TranslationType, AE, set(InnerSetType), Expr))
; smt_solver_interface_call(Solver, mk_op_fin1_subset(TranslationType, AE, set(InnerSetType), InnerSetType, Expr))
).
mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
functor(Op, Functor, 1),
(Functor == domain; Functor == range),
!,
arg(1, Op, A),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
A = b(_,set(CoupleType),_),
CoupleType = couple(Prj1Type,Prj2Type),
( Functor == domain
-> smt_solver_interface_call(Solver, mk_op_domain(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
; smt_solver_interface_call(Solver, mk_op_range(TranslationType, AE, CoupleType, Prj1Type, Prj2Type, Expr))
).
mk_expr_aux(Op, Type, TranslationType, Solver, LS, GS, Expr) :-
functor(Op, Functor, 2),
(Functor == domain_restriction; Functor == domain_subtraction; Functor == range_restriction; Functor == range_subtraction),
!,
Type = set(CoupleType),
arg(1, Op, A1),
arg(2, Op, A2),
mk_expr(A1, TranslationType, Solver, LS, GS, AE1),
mk_expr(A2, TranslationType, Solver, LS, GS, AE2),
( Functor == domain_restriction
-> smt_solver_interface_call(Solver, mk_op_dom_res(TranslationType, AE1, AE2, CoupleType, Expr))
; Functor == domain_subtraction
-> smt_solver_interface_call(Solver, mk_op_dom_sub(TranslationType, AE1, AE2, CoupleType, Expr))
; Functor == range_restriction
-> smt_solver_interface_call(Solver, mk_op_ran_res(TranslationType, AE1, AE2, CoupleType, Expr))
; smt_solver_interface_call(Solver, mk_op_ran_sub(TranslationType, AE1, AE2, CoupleType, Expr))
).
mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
functor(Op,Functor,1),
unary_operator(Functor),
!,
arg(1,Op,A),
mk_expr(A,TranslationType, Solver,LS,GS,AE),
smt_solver_interface_call(Solver,mk_op_arglist(TranslationType, Functor, [AE], Expr)).
mk_expr_aux(Op, _, TranslationType, Solver, LS, GS, Expr) :-
functor(Op, Functor, 1),
( Functor == general_union; Functor == general_intersection),
!,
arg(1, Op, A),
A = b(_,set(set(InnerType)),_),
mk_expr(A, TranslationType, Solver, LS, GS, AE),
( Functor == general_union
-> smt_solver_interface_call(Solver, mk_op_general_union(TranslationType, AE, set(InnerType), InnerType, Expr))
; store_explicit_set_unique_id(A, UniqueIdName),
smt_solver_interface_call(Solver, mk_op_general_intersection(TranslationType, UniqueIdName, AE, set(InnerType), InnerType, Expr))
).
mk_expr_aux(Op,_,TranslationType, Solver,LS,GS,Expr) :-
functor(Op,Functor,2),
binary_operator(Functor),
!,
arg(1,Op,A),
mk_expr(A,TranslationType, Solver,LS,GS,AE),
arg(2,Op,B),
mk_expr(B,TranslationType, Solver,LS,GS,BE),
smt_solver_interface_call(Solver,mk_op(TranslationType, Functor,AE,BE,Expr)).
mk_expr_aux(Expr,_,_,_,_,_,_) :- !,
add_error_fail(smt_solvers_interface,'mk_expr failed',Expr).