1:- use_module(prolog_version).    2:- use_module(library(clpfd)).    3:- use_module(library(terms)).    4:- use_module(reified_unif,[if_unary_substitute/4,inst/1]).    5:- (is_dialect(swi)
    6    -> compile(swi_clpfd)
    7    ;  compile(sicstus_clpfd)).    8
    9neq(A,B):- A#\=B.
   10lt(A,B):- A#<B.
   11eq(A,B):- A=B.
   12gt(A,B):- A#>B.
   13leq(A,B):- A#=<B.
   14geq(A,B):- A#>=B.
   15
   16is_identical(A,X):- A==X.
   17
   18term_unify(X,X).
   19
   20%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% used in ics_quant %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   21rel2clp(<>,#\=).
   22rel2clp(<,#<).
   23rel2clp(=,#=).
   24rel2clp(>,#>).
   25rel2clp(=<,#=<).
   26rel2clp(>=,#>=).
   27rel2clp(clp_constraint,clp_constraint).
   28rel2clp(st,st). /* MG: This is necessary because in Unfolding we call
   29this module. Since there might remain some st, we have to recognize
   30it as a constraint, otherwise the quantification will be wrong */
   31
   32is_clp_functor(C):- rel2clp(C,_).
   33
   34solver_rewrite_constraint(Constraint,Constraint1):-
   35	Constraint=..[F,Arg1,Arg2],
   36	rel2clp(F,F1),
   37	Constraint1=..[F1,Arg1,Arg2].
   38
   39% used in sokb_parser
   40is_constraint_functor(F):-
   41	atom_concat(#,_,F).
   42
   43%%% Used in quantif
   44% Checks if the restriction is entailed by a set
   45% of restrictions.
   46% It is by far not complete!!!
   47% Just a collection of simple rules in which entailment
   48% is easy.
   49
   50% A restriction is entailed if it was already imposed
   51restriction_entailed(R,[R1|_]):-
   52    R == R1, !.
   53%restriction_entailed(R, [R1|_]):-
   54%   is_unary(R), is_unary(R1),
   55%   unary_restriction_entailed(R,R1).
   56restriction_entailed(X in LowX..HighX,[X1 in Low1 .. High1|_]):-
   57    X == X1,
   58    leq_infty(Low1,LowX),
   59    leq_infty(HighX,High1),!.
   60restriction_entailed(R,[_|T]):-
   61    restriction_entailed(R,T).
   62
   63is_unary(R):-
   64    term_variables_bag(R,[_]).
   65
   66leq_infty(inf,_):-!.
   67leq_infty(_,sup):-!.
   68leq_infty(A,B):-
   69    number(A), number(B), A=<B.
   70
   71rewrite_restriction(R,Rew):-
   72    (is_unary(R)
   73      ->    rewrite_restr_rules(R,Rew)
   74      ; R=Rew).
   75
   76% Others can be added
   77rewrite_restr_rules((X #< Y),(X in inf..Y1)):-
   78    var(X), ground(Y),!,
   79    Y1 is Y-1.
   80rewrite_restr_rules((X #> Y),(X in Y1..sup)):-
   81    var(X), ground(Y),!,
   82    Y1 is Y+1.
   83rewrite_restr_rules((X #< Y),Rew):-
   84    var(Y), ground(X),!,
   85    rewrite_restr_rules((Y #> X),Rew).
   86rewrite_restr_rules((X #> Y),Rew):-
   87    var(Y), ground(X),!,
   88    rewrite_restr_rules((Y #< X),Rew).
   89rewrite_restr_rules(R,R).
   90
   91%%%%%%%%%%%%%%%%%%%%%%%%%%% Used in reified_unif %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   92fd_or_num(X) :- fd_var(X),!.
   93fd_or_num(X) :- number(X).
   94
   95cstr_var(X) :- clpfd:fd_var(X).
   96
   97is_number(X) :- number(X).
   98
   99term_equality(A,A).
  100
  101binary_domain(B):- B in 0..1.
  102
  103% MarcoG 10 may 2005
  104% changed because or some reason the choice point gets lost.
  105% I upgrade to a better version (with reified constraints).
  106impose_neg_constraints(X,R,Y):-
  107    impose_neg_constraints(X,R,Y,0).
  108
  109impose_neg_constraints(_,[],_,1):- !. % SICStus non ottimizza questo cut
  110impose_neg_constraints(X,[R|T],Y,B):-
  111    negate(X,R,Y,B1),
  112    (B1 == 0 -> B=0
  113    ;   solver_and(B,B1,B2),
  114        impose_neg_constraints(X,T,Y,B2)
  115    ).
  116
  117
  118%impose_neg_constraints(X,[R|_],Y):-
  119%    negate(X,R,Y).
  120%impose_neg_constraints(X,[_|T],Y):-
  121%    impose_neg_constraints(X,T,Y).
  122%negate(X,R,Y):- negate(X,R,Y,0).
  123
  124negate(X,R,Y,B):-
  125    if_unary_substitute(X,R,Y,T),
  126    reification(T,B),
  127    inst(B).
  128
  129solver_search(LT1):- labeling([ffc],LT1).
  130
  131%%%%%%%%%%%%%%%%%%%%%%%%%%%%% used in sciff.pl %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  132add_default_domain(T):-
  133    (fd_var(T) -> true ; T