smtlib2_environment

add_assertion(env(IDs,Funs,[CurrentAssertionSet|AssertionSets],Ct),Term,env(IDs,Funs,[NAs|AssertionSets],Ct)) :-
    NAs = [Term|CurrentAssertionSet].

add_custom_type(env(IDs,Funs,As,Ct),ID,env(IDs,Funs,As,[ID|Ct])).

add_function(env(IDs,Funs,As,Ct),ID,P,R,D,env(IDs,NFuns,As,Ct)) :-
    avl_store(ID,Funs,function(P,R,D),NFuns).

add_identifier(env(IDs,Funs,As,Ct),ID,Type,env(NIDs,Funs,As,Ct)) :-
    avl_store(ID,IDs,b(identifier(ID),Type,[]),NIDs).

avl_store_all_ids([],A,A).

avl_store_all_ids([b(identifier(ID),Type,[])|T],AIn,AOut) :-
    avl_store(ID,AIn,b(identifier(ID),Type,[]),ATemp),
    avl_store_all_ids(T,ATemp,AOut).

create_local_env(env(IDs,Funs,As,Ct),LocalIDs,env(NIDs,Funs,As,Ct)) :-
    avl_store_all_ids(LocalIDs,IDs,NIDs).

empty_env(env(IDs,Funs,[[]],[])) :-
    empty_avl(IDs),
    empty_avl(Funs).

get_assertions(env(_,_,As,_),AllAssertions) :- append(As,AllAssertions).

get_custom_types(env(_,_,_,Ct),Ct).

get_function(ID,env(_,Funs,_,_),Params,Results,Definition) :- atomic(ID),!,
    avl_fetch(ID,Funs,function(Params,Results,Definition)).

get_function(ID,env(_,Funs,_,_),Params,Results,Definition) :-
    print(var_get_function(ID)),nl,
    avl_member(ID,Funs,function(Params,Results,Definition)).

get_type(Id,env(IDs,_,_,_),Type) :- atomic(Id),!,
    avl_fetch(Id,IDs,b(identifier(Id),Type,[])).

get_type(Id,env(IDs,_,_,_),Type) :-
    print(var_get_type(Id)),nl,
    avl_member(Id,IDs,b(identifier(Id),Type,[])).

is_custom_type(env(_,_,_,Cts),Ct) :-
    member(Ct,Cts).

pop_assertion_stack(Env,0,Env) :- !.

pop_assertion_stack(env(IDs,Funs,[_|Ass],Types),Count,EnvOut) :- Count > 0, !,
    NCount is Count - 1,
    pop_assertion_stack(env(IDs,Funs,Ass,Types),NCount,EnvOut).

push_assertion_stack(Env,0,Env) :- !.

push_assertion_stack(env(IDs,Funs,Ass,Types),Count,EnvOut) :- Count > 0, !,
    NCount is Count - 1,
    pop_assertion_stack(env(IDs,Funs,[[]|Ass],Types),NCount,EnvOut).