create_state_preds_aux(Name,integer,Infos,int(Value),Pred,_) :- !,
(number(Value) ->
safe_create_texpr(integer(Value),integer,TVal),
safe_create_texpr(equal(b(identifier(Name),integer,Infos),TVal),pred,Pred)
;
clpfd_domain(Value,Min,Max),
(number(Min)
-> safe_create_texpr(integer(Min),integer,MinValue),
safe_create_texpr(greater_equal(b(identifier(Name),integer,Infos),MinValue),pred,Greater)
; Greater = b(truth,pred,[])),
(number(Max)
-> safe_create_texpr(integer(Max),integer,MaxValue),
safe_create_texpr(less_equal(b(identifier(Name),integer,Infos),MaxValue),pred,Less)
; Less = b(truth,pred,[])),
conjunct_predicates([Less,Greater],Pred)
).
create_state_preds_aux(Name,Type,Infos,Value,Pred,_) :-
ground_value(Value),
useful_value_for_state_pred(Value), !,
Pred = b(equal(b(identifier(Name),Type,Infos),b(value(Value),Type,[])),pred,[]).
create_state_preds_aux(ID,_,_,Val,b(truth,pred,[]),Opts) :-
(var(Val) % for :z3 these are the quantified variables themselves; in general we should ensure there are no constraints, co-routines pending on Val
; member(allow_to_skip_vars(true),Opts)
-> debug_format(19,'Not creating state predicate for ~w (value too complex)~n',[ID])
; member(skipped_variables(L),Opts), member(ID,L)
-> debug_format(19,'Not creating state predicate for ~w (value too complex)~n',[ID])
),
!.
create_state_preds_aux(ID,_,Infos,Val,b(truth,pred,[]),_) :-
translate:print_bvalue(Val),nl,
add_error(create_state_pred,'Ignoring value (too complex) for identifier',ID,Infos). % TO DO: enum warning ; if no solution found ok