/*
    Copyright (C) 2013  E.Albert, P.Arenas, S.Genaim, and G.Puebla
                        https://costa.ls.fi.upm.es

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/


:- module(ub_checker,[run_test_ub/1,run_test_lb/1,compare_ubs/5,compare_lbs/5]).

:- use_module(library(clpq)).


%% SYNTAX:
%%
%%   e := n | nat(l) | e+e | e*e | log(a,nat(l)+1) | pow(a,nat(l)) |
%%        pow(nat(l),a) | max([e1,...,en]) | min([e1,...,en])
%%
%%     n and a are non-negative integers such that n>=0 and a>=2 l is
%%     a linear expression with integer coefficients.
%%
%%       ** ALL COEFFICIENTS MUST BE INTEGER ***
%%
%%       ** You cannot mix expressions with min and max. The max are
%%          supported only when comparing UBs, and the min when
%%          comparing min.
%%
%% USAGE:
%%
%%   compare_ubs(+Exp1, +Exp2, +Phi, +Options, -Result)
%%   compare_lbs(+Exp1, +Exp2, +Phi, +Options, -Result)
%%
%%      Exp1 and Exp2 are cost expressions according to the above
%%      syntax. Phi is a list of linear constraints. Result will be
%%      'yes' if Exp1=<Exp2, otherwise 'no'.
%%
%%      Options is a list of options, where each option is given as
%%      name=value (see possible option/values below).
%%
%%      At the end of this file you can find some examples.
%%
%%     
%% OPTIONS:
%%
%%   The available options are
%%
%%    1. sum_alg=X: when X=general the checker will use Definition 11
%%       for comparing sums, and when X=basic it will use Definition 9.
%%
%%    2. check_strict_pos=X: when X=yes, the check will check that
%%       every basic cost expression is >=1, and that every product is
%%       >=2. When X=no this check is ignored, in such case the result
%%       might not be correct for extreme cases.
%%
%%    3. pow_norm_scheme=X: when X=split, then expression like
%%       pow(nat(l),2) are split into nat(l)*nat(l). When X=merge, it
%%       does the opposite. Using split can handle more cases,
%%       however, using merge might be more efficient.
%%



%% upper bounds main engine
%%
compare_ubs(Exp1, Exp2, Phi, Options, Result) :-
	set_default_options,
	set_options(Options),
	input_exps_to_normal_form(Exp1, Exp2, E1, E2, Nats),
	compare_ubs_1(E1, E2, Phi, Nats, Result).

compare_ubs_1(E1, E2, Phi, Nats, Result) :-
	tell_cs(Phi),
	build_context(Nats),
	simplify_products(E1,NE1),
	simplify_products(E2,NE2),
	( check_strict_positiveness(NE1,NE2) ->
	    ( compare_ubs_2(NE1, NE2) -> Succ = yes ; Succ = no )
	;
	    Succ = no
	),
	Succ = no,
	Result = no,
	!.
compare_ubs_1(_E1, _E2, _Phi, _Nats, Result) :-
	Result = yes,
	!.

compare_ubs_2([], _E2).
compare_ubs_2([E|Es], E2) :-
	ut_member(Ep,E2),
	( get_option(sum_alg,general) -> lte_general_sum(E,Ep,_) ; lte_sum(E,Ep,_) ),
	!,
	compare_ubs_2(Es, E2).



%% lower bounds main engine
%%
compare_lbs(Exp1, Exp2, Phi, Options, Result) :-
	set_default_options,
	set_options(Options),
	input_exps_to_normal_form(Exp1, Exp2, E1, E2, Nats),
	compare_lbs_1(E1, E2, Phi, Nats, Result).

compare_lbs_1(E1, E2, Phi, Nats, Result) :-
	tell_cs(Phi),
	build_context(Nats),
	simplify_products(E1,NE1),
	simplify_products(E2,NE2),
	( check_strict_positiveness(NE1,NE2) ->
	    ( compare_lbs_2(NE1, NE2) -> Succ = yes ; Succ = no )
	;
	    Succ = no
	),
	Succ = no,
	Result = no,
	!.
compare_lbs_1(_E1, _E2, _Phi, _Nats, Result) :-
	Result = yes,
	!.


compare_lbs_2(E1,E2) :-
	ut_member(E,E1),
	compare_lbs_3(E2,E).

compare_lbs_3([], _Ep).
compare_lbs_3([Ep|Es], E) :-
	( get_option(sum_alg,general) -> lte_general_sum(E,Ep,_) ; lte_sum(E,Ep,_) ),
	!,
	compare_lbs_3(Es, E).




%%
check_strict_positiveness(_,_) :-
	get_option(check_strict_pos,no),
	!.
check_strict_positiveness(E1,E2) :-
	get_option(check_strict_pos,yes),
	check_strict_positiveness_1(E1),
	check_strict_positiveness_1(E2).
	

check_strict_positiveness_1([]).
check_strict_positiveness_1([S|Ss]) :-
	check_strict_positiveness_2(S),
	check_strict_positiveness_1(Ss).

check_strict_positiveness_2([]).
check_strict_positiveness_2([P|Ps]) :-
	check_strict_positiveness_3(P,R),
	!,
	R == yes,
	check_strict_positiveness_2(Ps).

check_strict_positiveness_3([],_).
check_strict_positiveness_3([E|Es],R) :-
	check_strict_positiveness_4(E,R),
	check_strict_positiveness_3(Es,R).

check_strict_positiveness_4(num(X),R) :-
	!,
	X>=1,
	( X>=2 -> R = yes).
check_strict_positiveness_4(lin(L),R) :-
	!,
	(is_entailed([L>=2]) -> R=yes ; true).

check_strict_positiveness_4(pow(lin(L),num(M)),R) :-
	!,
	((is_entailed([L>=2]),M>=1) -> R=yes ; true).

check_strict_positiveness_4(pow(num(M),lin(_L)),R) :-
	!,
	(M>=2 -> R=yes ; true).

check_strict_positiveness_4(log(Base,lin(L)+1),R) :-
	!,
	is_entailed([L+1>=Base]),
	C is Base^2,
	(is_entailed([L+1>=C]) -> R=yes ; true).




% later should be replaced by simpler code, it is not necessary to
% normalize, but rather to introduce the new constant when setting some
% of nats to 0
%
simplify_products(A,B) :-
	normalize_products(A,B). 


%
% builds a context, by choosing for every linear expression (that
% comes from nat) if it is positive or non-positive. Note that
% positive means >= 1 since all coefficients are integer, and the
% variables are integer as well.
%
build_context([]).
build_context([L=V|Ns]) :-
	V = 0,
	{L =< 0},
	build_context(Ns).
build_context([L=V|Ns]) :-
	{L>=1, L=V},
	build_context(Ns).


%
% general-sum comparison -- fp_+^g -- Definition 11 applied iteratively
%
lte_general_sum([],S2,S2).
lte_general_sum(Ss,S2,Remainder) :-
	ut_select(S2,M,S2_a),
	ut_subset(Ss,S1,Ss_a), S1 \= [],
	lte_sum_product(S1,M,_),
	extend_with_adiff(S2_a, S1, M, S2_b),
	lte_general_sum(Ss_a,S2_b,Remainder).


%
% sum-product comparison -- fp_{+,*} -- Definition 10 applied iteratively
%
lte_sum_product([],M2,M2).
lte_sum_product(S1,M2,Remainder) :-
	ut_select(S1,M2p,S1_a),
	lte_product(M2p,M2,M2pp),
	lte_sum_product(S1_a,M2pp,Remainder).


%
% sum comparison -- fp_+ -- Definition 9 applied iteratively
%
lte_sum([],S2, S2).
lte_sum([M1|S1],S2,Remainder) :-
	ut_select(S2,M2,S2_a),
	lte_product(M1,M2,_M2_rem),
	extend_with_adiff(S2_a,[M1],M2,S2_b),
	lte_sum(S1,S2_b,Remainder).

extend_with_adiff(SumToExtend, S, M, NewSum ) :-
	get_product_constants([M|S],[C1|Cs]),
	ut_sum(Cs,C2),
	C is C1 - C2,
	( C =< 0 ->
	    NewSum = SumToExtend
	;
	    replace_constant_factor(M,C,Mp),
	    NewSum = [Mp | SumToExtend]
	).
	
replace_constant_factor([],C,[num(C)]).
replace_constant_factor([num(_)|Xs],C,[num(C)|Xs]) :- !.
replace_constant_factor([X|Xs],C,[X|Ys]) :-
	replace_constant_factor(Xs,C,Ys).


get_product_constants([],[]).
get_product_constants([M|Ms],[C|Cs]) :-
	( ut_member(num(C),M) -> true ; C=1 ),
	!,
	get_product_constants(Ms,Cs).


%
% product comparison -- fp_* -- Definition 8 applied iteratively
%
lte_product(M1,M2,Remainder) :-
	lte_product_aux(M1,M2,Remainder).

lte_product_aux([],M2,M2).
lte_product_aux([E1|Es],M2,Remainder) :-
	ut_select(M2,E2,M2_a),
	lte_basic_cexpr(E1,E2,ADiff),
	normalize_one_product([ADiff|M2_a],M2_b),
	lte_product_aux(Es,M2_b,Remainder).


% lte_basic_cexpr(+E1,+E2,-Adiff)
%
%  This predicate implements the comparison of basic cost
%  expressions as in Table 1 of the paper. It succeeds if it can
%  decide that Phi |= E1<=E2. It also returns the 'reminder' in
%  Adiff. The reminder is the part of E2 that is not required for
%  proving E1=<E2 (which can then be used for other comparisons)
%

% n  n'
%
lte_basic_cexpr(num(N),num(Np),num(1)) :-
	integer(N),
	integer(Np),
	N =< Np,
	!.

% n  log_a(A+1)
%
lte_basic_cexpr(num(N),log(Base,lin(A)+1),num(1)) :-
	C is Base^N,
	is_entailed([ C =< A+1 ]),
	!.

% n  A^m
%
lte_basic_cexpr(num(N),pow(lin(A),num(M)),ADiff) :-
	M > 1,
	is_entailed([ N =< A ]),
	M1 is M-1,
	( M1 = 1 ->
	    ADiff = lin(A)
	;
	    ADiff = pow(lin(A),num(M1))
	),
	!.

% n   m^l 
%
lte_basic_cexpr(num(N),pow(num(M),lin(L)),pow(num(M),lin(L-N))) :-
	M > 1,
	is_entailed([ N =< L ]),
	!.

% l1 l2
%
lte_basic_cexpr(lin(L1),lin(L2),num(1)) :- 
	is_entailed([ L1 > 0, L1 =< L2 ]),
	!.

% l  A^n
%
lte_basic_cexpr(lin(L),pow(lin(A),num(N)),ADiff) :-
	N>1,
	is_entailed([ L =< A ]),
	N1 is N-1,
	( N1 = 1 ->
	    ADiff = lin(A)
	;
	    ADiff = pow(lin(A),num(N1))
	),
	!.

% l  n^l'
%
lte_basic_cexpr(lin(L),pow(num(N),lin(Lp)),pow(num(N),lin(Lp-L))) :-
	N > 1,
	is_entailed([ L =< Lp ]),
	!.

% log_a(A+1)   l
%
lte_basic_cexpr(log(_Base,lin(A)+1),lin(L),num(1)) :-
	is_entailed([ L > 0, A+1 =< L ]),
	!.

% log_a(A+1)   log_a(B+1)
%
lte_basic_cexpr(log(Base1,lin(A)+1),log(Base2,lin(B)+1),num(1)) :- 
	Base1 >= Base2,
	is_entailed([ A =< B ]),
	!.

% log_a(A+1)   B^n
%
lte_basic_cexpr(log(_Base,lin(A)+1),pow(lin(B),num(N)),ADiff) :- 
	N > 1,
	is_entailed([ A+1 =< B ]),
	N1 is N-1,
	( N1 = 1 ->
	    ADiff = lin(B)
	;
	    ADiff = pow(lin(B),num(N1))
	),
	!.

% log_a(A+1)   n^l
%
lte_basic_cexpr(log(_Base,lin(A)+1),pow(num(N),lin(L)),pow(num(N),lin(L-A))) :- 
	N > 1,
	is_entailed([ L > 0 , A+1 =< L ]),
	!.

% A^n  B^m
%
lte_basic_cexpr(pow(lin(A),num(N)),pow(lin(B),num(M)),Adiff) :- 
	N > 1,
	M > 1,
	N =< M,
	is_entailed([ A =< B ]), % uses >
	M1 is M-N,
	( M1=0 ->
	    Adiff = num(1)
	;
	  M1=1 ->
	    Adiff = lin(B)
	;
	     Adiff = pow(lin(B),num(M1))
	),
	!.

% A^n  m^l
%
lte_basic_cexpr(pow(lin(A),num(N)),pow(num(M),lin(L)),pow(num(N),lin(L-N*A))) :- 
	M > 1,
	is_entailed([ N*A =< L ]),
	!.


% n^l   m^l'
%
lte_basic_cexpr(pow(num(N),lin(L)),pow(num(M),lin(Lp)),pow(num(M),lin(Lp-L))) :- 
	N =< M,
	is_entailed([ L =< Lp ]),
	!.





%%%%%%%%
%%%%%%%% This part converts the input expression into some internal
%%%%%%%% representation.
%%%%%%%%

input_exps_to_normal_form(Exp1, Exp2, NormFlatMaxFree_E1, NormFlatMaxFree_E2, Nats_Bindings) :-
	parse_cost_expression(Exp1, E1, Ns-T),
	parse_cost_expression(Exp2, E2, T-[]),
	unify_identical_nats(Ns,Vs,Nats_Bindings),      
	minmax_free(E1, Vs, FlatMaxFree_E1),                    
	minmax_free(E2, Vs, FlatMaxFree_E2),
	normalize_products(FlatMaxFree_E1,NormFlatMaxFree_E1),
	normalize_products(FlatMaxFree_E2,NormFlatMaxFree_E2),
	!.

%
unify_identical_nats(Nats,Vs,ReducedNats) :-
	sort(Nats,Nats_aux),
	unify_identical_nats_1(Nats_aux,Vs,ReducedNats). 

unify_identical_nats_1([],[],[]).
unify_identical_nats_1([L1=V1,L2=V2|Ns],Vs,Nsp) :-
	L1 == L2,
	!,
	V1=V2,   
	unify_identical_nats_1([L2=V2|Ns],Vs,Nsp).
unify_identical_nats_1([L=V|Ns],[V|Vs],[L=V|Nsp]) :-
	unify_identical_nats_1(Ns,Vs,Nsp).


%
parse_cost_expression(Exp, Exp_1, NatsH-NatsT) :-
	parse_cost_expression_1(Exp, Exp_1, NatsH-NatsT),
	!.
parse_cost_expression(_, _, _) :-
	throw('UBC: failed to parse the ub expression').

parse_cost_expression_1(V,_,_) :- % cost expression do not have variables directly, only inside nat
	var(V),
	!,
	throw('UBC: there is a free variable inside the ub expression').

parse_cost_expression_1(N,num(N),T-T) :-  
	integer(N),
	!.

parse_cost_expression_1(nat(L),lin(V),[L=V|T]-T) :-
	valid_nat_expression(L),
	!.

parse_cost_expression_1(log(Base,nat(L)+1),log(Base,lin(V)+1),[L=V|T]-T) :- % log must always have the +1
	integer(Base),
	Base >= 2,
	valid_nat_expression(L),
	!.

parse_cost_expression_1(pow(nat(L),Exp),pow(lin(V),num(Exp)),[L=V|T]-T) :-
	integer(Exp),
	Exp >= 2,
	valid_nat_expression(L),
	!.
			 
parse_cost_expression_1(pow(Base,nat(L)),pow(num(Base),lin(V)),[L=V|T]-T) :-
	integer(Base),
	Base >= 2,
	valid_nat_expression(L),
	!.

parse_cost_expression_1(E1+E2,NE1+NE2,H-T) :-
	parse_cost_expression_1(E1,NE1,H-T1),
	parse_cost_expression_1(E2,NE2,T1-T),
	!.

parse_cost_expression_1(E1*E2,NE1*NE2,H-T) :-
	parse_cost_expression_1(E1,NE1,H-T1),
	parse_cost_expression_1(E2,NE2,T1-T),
	!.

parse_cost_expression_1(max(As),max(AsExps),H-T) :-
	parse_cost_expression_2(As,AsExps,H-T),
	!.

parse_cost_expression_1(min(As),min(AsExps),H-T) :-
	parse_cost_expression_2(As,AsExps,H-T),
	!.

parse_cost_expression_2([],[],T-T).
parse_cost_expression_2([A|As],[AExp|AsExps],H-T) :-
	parse_cost_expression_1(A,AExp,H-T1),
	parse_cost_expression_2(As,AsExps,T1-T).

valid_nat_expression(_).


% convert an expression into flat max-free form -- max is split
% into several cases, and each case is normalized to sum of
% products. The second parameter Vs is the list of variables that
% appear in Exp, it is needed to unify all names, since the different
% cases for max are generated with findall/3
%
minmax_free(Exp, Vs, MaxFreeExps) :-
	findall((MaxFreeExp,Vs), minmax_free_1(Exp,MaxFreeExp), MaxFreeExps_aux),
	minmax_free_unify_vars(MaxFreeExps_aux,Vs,MaxFreeExps).

minmax_free_1(max(Es),FE) :-
	ut_member(E,Es),
	minmax_free_1(E,FE).
minmax_free_1(min(Es),FE) :-
	ut_member(E,Es),
	minmax_free_1(E,FE).
minmax_free_1(E1*E2,FE) :-
	minmax_free_1(E1,FE1),
	minmax_free_1(E2,FE2),
	merge_flat_exps(FE1,FE2,FE).
minmax_free_1(E1+E2,FE) :-
	minmax_free_1(E1,FE1),
	minmax_free_1(E2,FE2),
	ut_append(FE1,FE2,FE).
minmax_free_1(E,[[E]]) :-
	functor(E,F,N),
	ut_member(F/N,[num/1,lin/1,log/2,pow/2]).

merge_flat_exps([],_NFE2,[]).
merge_flat_exps([A|As],Bs,Cs) :-
	merge_flat_exps_1(Bs,A,As,Bs,Cs).

merge_flat_exps_1([],_,As,Bs,Cs) :-
	merge_flat_exps(As,Bs,Cs).
merge_flat_exps_1([X|Xs],A,As,Bs,[C|Cs]) :-
	ut_append(X,A,C),
	merge_flat_exps_1(Xs,A,As,Bs,Cs).

minmax_free_unify_vars([],_Vs,[]).
minmax_free_unify_vars([(E,Vs)|Es],Vs,[E|UEs]) :-
	minmax_free_unify_vars(Es,Vs,UEs).



% normalizes the produces in flat max-free expressions, it tries to
% merge similar expressions, etc.
%
normalize_products([],[]).
normalize_products([Ps|Ss],[NPs|NSs]) :-
	normalize_products_1(Ps,NPs),
	!,
	normalize_products(Ss,NSs).

normalize_products_1([],[]).
normalize_products_1([BEs|Ps],NPs) :-
	normalize_one_product(BEs,NBEs),
	( NBEs = [] -> NPs = NPs_1 ; NPs = [NBEs|NPs_1] ), % check if the product is zero
	!,
	normalize_products_1(Ps,NPs_1).

% normalizes only one produce, used in normalize products and in some
% other places above
%

normalize_one_product(P,[]) :-
	ut_member( lin(X), P),
	X == 0,
	!.
normalize_one_product(P,[]) :-
	ut_member( log(_,lin(X)+1), P),
	X == 0+1,
	!.
normalize_one_product(P,NP) :-
	sort(P,SortedP),
	( get_option(pow_norm_scheme,merge) ->
	    normalize_one_product_2(SortedP,NP)
	;
	    normalize_one_product_1(SortedP,NP)
	).

normalize_one_product_1([],[]).
normalize_one_product_1([pow(lin(X),_)|BEs],NBEs) :-
	X == 0,
	!,
	normalize_one_product_1(BEs,NBEs).

normalize_one_product_1([pow(_,lin(X))|BEs],NBEs) :-
	X == 0,
	!,
	normalize_one_product_1([num(1)|BEs],NBEs).

normalize_one_product_1([num(A),num(B)|BEs],NBEs) :-
	C is A*B,
	!,
	normalize_one_product_1([num(C)|BEs],NBEs).

normalize_one_product_1([pow(lin(A),num(C))|BEs],[lin(A)|NBEs]) :-
	C>=1,
	!,
	C1 is C-1,
	(C1 > 0 ->
	   normalize_one_product_1([pow(lin(A),num(C1))|BEs],NBEs)
	;
	   normalize_one_product_1(BEs,NBEs)
	).

normalize_one_product_1([E|BEs],[E|NBEs]) :-
	normalize_one_product_1(BEs,NBEs).




normalize_one_product_2([],[]).
normalize_one_product_2([pow(lin(X),_)|BEs],NBEs) :-
	X == 0,
	!,
	normalize_one_product_2(BEs,NBEs).

normalize_one_product_2([pow(_,lin(X))|BEs],NBEs) :-
	X == 0,
	!,
	normalize_one_product_2([num(1)|BEs],NBEs).

normalize_one_product_2([num(A),num(B)|BEs],NBEs) :-
	C is A*B,
	!,
	normalize_one_product_2([num(C)|BEs],NBEs).

normalize_one_product_2([lin(A),lin(B)|BEs],NBEs) :-
	A == B,
	!,
	normalize_one_product_2([pow(lin(A),num(2))|BEs],NBEs).

normalize_one_product_2([pow(lin(A),num(C)),lin(B)|BEs],NBEs) :-
	A == B,
	!,
	D is C+1,
	normalize_one_product_2([pow(lin(A),num(D))|BEs],NBEs).

normalize_one_product_2([pow(lin(A),num(C)),pow(lin(B),num(D))|BEs],NBEs) :-
	A == B,
	!,
	E is C+D,
	normalize_one_product_2([pow(lin(A),num(E))|BEs],NBEs).

normalize_one_product_2([E|BEs],[E|NBEs]) :-
	normalize_one_product_2(BEs,NBEs).




%%%%%%%%
%%%%%%%% miscellaneous predicates required for implementing the checker
%%%%%%%% above.
%%%%%%%%

%
is_entailed(Cs) :-
	all_entailed(Cs).

all_entailed([]).
all_entailed([C|Cs]) :-
	entailed(C),
	!,
	all_entailed(Cs).

%
tell_cs([]).
tell_cs([C|Cs]) :-
	{C},
	!,
	tell_cs(Cs).

%
ut_select([X|Xs],X,Xs).
ut_select([X|Xs],A,[X|Ys]) :-
        ut_select(Xs,A,Ys).

%
ut_subset([],[],[]).
ut_subset([X|Xs],Ys,[X|Zs]) :-
	ut_subset(Xs,Ys,Zs).
ut_subset([X|Xs],[X|Ys],Zs) :-
	ut_subset(Xs,Ys,Zs).

%
ut_sum(Xs,S) :-
	ut_sum_1(Xs,0,S).

ut_sum_1([],Accm,Accm).
ut_sum_1([X|Xs],Accm,S) :-
	Accm_1 is Accm+X,
	ut_sum_1(Xs,Accm_1,S).

%
ut_member(X,[X|_]).
ut_member(X,[_|Xs]) :-
	ut_member(X,Xs).

%
ut_append([],X,X).
ut_append([X|Xs],Ys,[X|Zs]) :-
	ut_append(Xs,Ys,Zs).

%%%%%%%%
%%%%%%%% This part handles the different options of the checker
%%%%%%%%

:- dynamic opt/2.

option(sum_alg,general,[basic,general]).
option(check_strict_pos,no,[yes,no]).
option(pow_norm_scheme,merge,[split,merge]).

set_default_options :-
	retractall(opt(_,_)).

set_option(Name,Val) :-
	option(Name,_,Vals),
	ut_member(Val,Vals),
	retractall(opt(Name,_)),
	assertz(opt(Name,Val)),
	!.

set_options([]).
set_options([Name=Val|Os]) :-
	set_option(Name,Val),
	set_options(Os).

get_option(Name,Val) :-
	opt(Name,Value),
	!,
	Value = Val.
get_option(Name,Val) :-
	option(Name,Val,_),
	!.




%%%%%%%%
%%%%%%%% This part includes some test cases, including the examples that appear 
%%%%%%%% in the paper.
%%%%%%%%


test(1,
     3*log(2,nat(A)+1),
     10*nat(C),
     [A>=4,C>=0,A+1=<C],
     []).

test(2,
     pow(nat(A),3)+pow(nat(A),2)+nat(A),
     pow(nat(A),6),
     [A>=2],
     []).

test(3,
     max([nat(A),nat(B)]),
     nat(C),
     [C>=A, C>=B],
     []).

test(4,
     pow(nat(A),2),
     nat(B)*nat(C),
     [C>=A, B>=A, A>=0, B>=0, C>=0],
     [pow_norm_scheme=split]).

test(5,
     pow(2,nat(N))
     *(31+
       (8*log(2,(nat(2*N-1)+1))
       +nat(A)*(10+6*nat(B))))
     + 3*pow(2,nat(N)),
     pow(2,nat(N))
     *(31+
       (8*log(2,(nat(2*N-1)+1))
       +nat(A)*(10+6*nat(B))))
     + 3*pow(2,nat(N)),
     [],
     []).

test(6,
     pow(2,nat(N))
     *(31+
       max([8*log(2,(nat(2*N-1)+1)),
       nat(A)*(10+6*nat(B))]))
     + 3*pow(2,nat(N)),
     pow(2,nat(N))
     *(31+
       (8*log(2,(nat(2*N-1)+1))
       +nat(A)*(10+6*nat(B))))
     + 3*pow(2,nat(N)),
     [],
     []).

test(7,Exp,Mexp,[],[]):-
	test(6,Exp1,Exp2,_,_),
	mirror(Exp1,Exp),
	mirror(Exp2,Mexp).

test(8,
     pow(2,nat(N))
     *(31+
       max([8*log(2,(nat(2*N-1)+1)),
       3+nat(A)*(10+6*nat(B))]))
     + 9*pow(2,nat(N)),
     pow(2,nat(N))
     *(31+
       max([8*log(2,(nat(2*N-1)+1)),
       3+nat(A)*(10+6*nat(B))]))
     + 9*pow(2,nat(N)),
     [],
     []).

test(9,Exp,Mexp,[],[]):-
	test(8,Exp1,Exp2,_,_),
	mirror(Exp1,Exp),
	mirror(Exp2,Mexp).

test(10,
     min([nat(A),nat(B)]),
     nat(C),
     [C>=A, B>=2*C],
     []).



mirror(A1+A2,B2+B1):-!,
	mirror(A1,B1),
	mirror(A2,B2).
mirror(A1*A2,B2*B1):-!,
	mirror(A1,B1),
	mirror(A2,B2).
mirror(A,A).

run_test_ub(I) :-
	test(I,S1,S2,Cs,Options),
	compare_ubs(S1,S2,Cs,Options,Result),
	format("The checker says '~p'~n",[Result]).

run_test_lb(I) :-
	test(I,S1,S2,Cs,Options),
	compare_lbs(S1,S2,Cs,Options,Result),
	format("The checker says '~p'~n",[Result]).