1		% (c) 2014-2015 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(smtlib2_environment,[empty_env/1,
6		add_identifier/4,
7
8		add_assertion/3,
9		get_assertions/2,
10		push_assertion_stack/3,
11		pop_assertion_stack/3,
12
13		get_type/3,
14		add_function/6,
15		get_function/5,
16		create_local_env/3,
17		get_custom_types/2,
18		is_custom_type/2,
19		add_custom_type/3]).
20
21		:- use_module(probsrc(module_information),[module_info/2]).
22		:- module_info(group,smtlib).
23		:- module_info(description,'The SMT-LIB 2 Interpreter - Environment').
24
25		:- use_module(library(lists)).
26		:- use_module(library(avl)).
27
28		% environment: env(Identifiers,Functions,Assertions,CustomTypes)
29		% identifiers: avl tree of b(identifier(ID),Type,[]) stored at ID
30		% functions: avl tree of function(Parameters,RetType,Definition) at ID
31		% Assertions: Stack (List) of Lists of predicates
32		% CustomTypes: List of custom types, i.e. deferred sets
33
34		empty_env(env(IDs,Funs,[[]],[])) :-
35		empty_avl(IDs),
36		empty_avl(Funs).
37
38		get_custom_types(env(_,_,_,Ct),Ct).
39		is_custom_type(env(_,_,_,Cts),Ct) :-
40		member(Ct,Cts).
41		add_custom_type(env(IDs,Funs,As,Ct),ID,env(IDs,Funs,As,[ID|Ct])).
42
43		create_local_env(env(IDs,Funs,As,Ct),LocalIDs,env(NIDs,Funs,As,Ct)) :-
44		avl_store_all_ids(LocalIDs,IDs,NIDs).
45
46		avl_store_all_ids([],A,A).
47		avl_store_all_ids([b(identifier(ID),Type,[])|T],AIn,AOut) :-
48		avl_store(ID,AIn,b(identifier(ID),Type,[]),ATemp),
49		avl_store_all_ids(T,ATemp,AOut).
50
51		add_function(env(IDs,Funs,As,Ct),ID,P,R,D,env(IDs,NFuns,As,Ct)) :-
52		avl_store(ID,Funs,function(P,R,D),NFuns).
53		get_function(ID,env(_,Funs,_,_),Params,Results,Definition) :-
54		avl_member(ID,Funs,function(Params,Results,Definition)).
55
56		pop_assertion_stack(Env,0,Env) :- !.
57		pop_assertion_stack(env(IDs,Funs,[_|Ass],Types),Count,EnvOut) :- Count > 0, !,
58		NCount is Count - 1,
59		pop_assertion_stack(env(IDs,Funs,Ass,Types),NCount,EnvOut).
60
61		push_assertion_stack(Env,0,Env) :- !.
62		push_assertion_stack(env(IDs,Funs,Ass,Types),Count,EnvOut) :- Count > 0, !,
63		NCount is Count - 1,
64		pop_assertion_stack(env(IDs,Funs,[[]|Ass],Types),NCount,EnvOut).
65
66		get_assertions(env(_,_,As,_),AllAssertions) :- append(As,AllAssertions).
67		add_assertion(env(IDs,Funs,[CurrentAssertionSet|AssertionSets],Ct),Term,env(IDs,Funs,[NAs|AssertionSets],Ct)) :-
68		NAs = [Term|CurrentAssertionSet].
69
70		add_identifier(env(IDs,Funs,As,Ct),ID,Type,env(NIDs,Funs,As,Ct)) :-
71		avl_store(ID,IDs,b(identifier(ID),Type,[]),NIDs).
72
73		get_type(Id,env(IDs,_,_,_),Type) :-
74		avl_member(Id,IDs,b(identifier(Id),Type,[])).